|
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:
898 bytes
|
| Rev | Line | |
|---|
| [1378] | 1 | include "LIN/joint_LTL_LIN.ma". |
|---|
| [722] | 2 | |
|---|
| [2286] | 3 | definition LTL ≝ mk_graph_params LTL_LIN. |
|---|
| [1168] | 4 | |
|---|
| [2286] | 5 | (* aid unification *) |
|---|
| 6 | unification hint 0 ≔ |
|---|
| 7 | (*---------------*) ⊢ |
|---|
| 8 | acc_a_reg LTL ≡ unit. |
|---|
| 9 | unification hint 0 ≔ |
|---|
| 10 | (*---------------*) ⊢ |
|---|
| 11 | acc_a_arg LTL ≡ unit. |
|---|
| 12 | unification hint 0 ≔ |
|---|
| 13 | (*---------------*) ⊢ |
|---|
| 14 | acc_b_reg LTL ≡ unit. |
|---|
| 15 | unification hint 0 ≔ |
|---|
| 16 | (*---------------*) ⊢ |
|---|
| 17 | acc_a_arg LTL ≡ unit. |
|---|
| 18 | unification hint 0 ≔ |
|---|
| 19 | (*---------------*) ⊢ |
|---|
| 20 | snd_arg LTL ≡ hdw_argument. |
|---|
| 21 | unification hint 0 ≔ |
|---|
| 22 | (*---------------*) ⊢ |
|---|
| 23 | ext_seq LTL ≡ ltl_lin_seq. |
|---|
| 24 | unification hint 0 ≔ |
|---|
| 25 | (*---------------*) ⊢ |
|---|
| 26 | pair_move LTL ≡ registers_move. |
|---|
| [1271] | 27 | |
|---|
| [2286] | 28 | definition ltl_program ≝ joint_program LTL. |
|---|
| 29 | |
|---|
| 30 | coercion byte_to_ltl_argument : ∀b: Byte.snd_arg LTL ≝ |
|---|
| 31 | hdw_argument_from_byte on _b : Byte to snd_arg LTL. |
|---|
| 32 | coercion reg_to_ltl_argument : ∀r: Register.snd_arg LTL ≝ |
|---|
| 33 | hdw_argument_from_reg on _r : Register to snd_arg LTL. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
