Last change
on this file since 2952 was
2952,
checked in by tranquil, 7 years ago

 corrected all backend 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  

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. 

29  unification hint 0 ≔ ⊢ lin_program ≡ joint_program LIN. 

30  

31  definition LIN_premain : ∀p : lin_program.joint_closed_internal_function LIN (prog_var_names ?? p) ≝ 

32  λp. 

33  let l3 : label ≝ an_identifier … (p1 one) in 

34  let 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 

38  mk_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  ] 

53  qed. 

Note: See
TracBrowser
for help on using the repository browser.