source: src/LIN/LIN.ma @ 2952

Last change on this file since 2952 was 2952, checked in by tranquil, 7 years ago
  • corrected all back-end premains to not pass any arguments to the main
  • premain fetching is made by fetch_function in joint_semantics.ma
  • reorganised some definition between Traces.ma and joint_fullexec.ma
File size: 1.6 KB
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.
29unification hint 0 ≔ ⊢ lin_program ≡ joint_program LIN.
30
31definition LIN_premain : ∀p : lin_program.joint_closed_internal_function LIN (prog_var_names ?? p) ≝
32λp.
33let l3 : label ≝ an_identifier … (p1 one) in
34let code ≝
35  [〈None ?, sequential … (COST_LABEL LIN ? (init_cost_label … p)) it〉 ;
36   〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 0 it) it〉 ;
37   〈Some ? l3, GOTO ? l3〉 ] in
38mk_joint_internal_function LIN (prog_var_names … p)
39  (mk_universe … (p0 (p0 one)))
40  (mk_universe … one)
41  it it 0 0 code 0.
42%
43[ * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%?→?); #EQ destruct
44  % try @I
45  [ %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct
46  |*: % whd in ⊢ (??%%→?); #EQ destruct
47  ]
48| * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
49| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
50| * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%%→?); #EQ destruct @I
51| %{it} %{(init_cost_label … p)} %
52]
53qed.
Note: See TracBrowser for help on using the repository browser.