|
Last change
on this file since 2304 was
2286,
checked in by tranquil, 9 years ago
|
|
Big update!
- merge of all _paolo variants
- reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
- split I8051.ma spawning new BackEndOps?.ma
compiler.ma broken at the moment, but not by these changes as far as I can tell
|
|
File size:
662 bytes
|
| Line | |
|---|
| 1 | include "LIN/joint_LTL_LIN.ma". |
|---|
| 2 | |
|---|
| 3 | definition LIN ≝ mk_lin_params LTL_LIN. |
|---|
| 4 | |
|---|
| 5 | (* aid unification *) |
|---|
| 6 | unification hint 0 ≔ |
|---|
| 7 | (*---------------*) ⊢ |
|---|
| 8 | acc_a_reg LIN ≡ unit. |
|---|
| 9 | unification hint 0 ≔ |
|---|
| 10 | (*---------------*) ⊢ |
|---|
| 11 | acc_a_arg LIN ≡ unit. |
|---|
| 12 | unification hint 0 ≔ |
|---|
| 13 | (*---------------*) ⊢ |
|---|
| 14 | acc_b_reg LIN ≡ unit. |
|---|
| 15 | unification hint 0 ≔ |
|---|
| 16 | (*---------------*) ⊢ |
|---|
| 17 | acc_a_arg LIN ≡ unit. |
|---|
| 18 | unification hint 0 ≔ |
|---|
| 19 | (*---------------*) ⊢ |
|---|
| 20 | snd_arg LIN ≡ hdw_argument. |
|---|
| 21 | unification hint 0 ≔ |
|---|
| 22 | (*---------------*) ⊢ |
|---|
| 23 | ext_seq LIN ≡ ltl_lin_seq. |
|---|
| 24 | unification hint 0 ≔ |
|---|
| 25 | (*---------------*) ⊢ |
|---|
| 26 | pair_move LIN ≡ registers_move. |
|---|
| 27 | |
|---|
| 28 | definition lin_program ≝ joint_program LIN. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
