source: src/LIN/LIN.ma @ 2760

Last change on this file since 2760 was 2286, checked in by tranquil, 7 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 
1include "LIN/joint_LTL_LIN.ma".
2
3definition LIN ≝ mk_lin_params LTL_LIN.
4
5(* aid unification *)
6unification hint 0 ≔
7(*---------------*) ⊢
8acc_a_reg LIN ≡ unit.
9unification hint 0 ≔
10(*---------------*) ⊢
11acc_a_arg LIN ≡ unit.
12unification hint 0 ≔
13(*---------------*) ⊢
14acc_b_reg LIN ≡ unit.
15unification hint 0 ≔
16(*---------------*) ⊢
17acc_a_arg LIN ≡ unit.
18unification hint 0 ≔
19(*---------------*) ⊢
20snd_arg LIN ≡ hdw_argument.
21unification hint 0 ≔
22(*---------------*) ⊢
23ext_seq LIN ≡ ltl_lin_seq.
24unification hint 0 ≔
25(*---------------*) ⊢
26pair_move LIN ≡ registers_move.
27
28definition lin_program ≝ joint_program LIN.
Note: See TracBrowser for help on using the repository browser.