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

moved callee saved saving and restoring to ERTL > LTL pass (untrusted
colourer and interference graph creator still need to be updated)
joint now has the stack size split in three (referenced locals, params
and spilled)

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. 

32  joint_closed_internal_function LIN (prog_names … p) ≝ 

33  λp. 

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

35  let code ≝ 

36  [〈None ?, sequential … (COST_LABEL LIN ? (init_cost_label … p)) it〉 ; 

37  〈None ?, sequential … (CALL LIN ? (inl … (prog_main … p)) 0 it) it〉 ; 

38  〈Some ? l3, GOTO ? l3〉 ] in 

39  mk_joint_internal_function LIN (prog_names … p) 

40  (mk_universe … (p0 (p0 one))) 

41  (mk_universe … one) 

42  it it 0 0 0 code 0. 

43  % 

44  [ * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%?→?); #EQ destruct 

45  % try @I 

46  [ %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct 

47  *: % whd in ⊢ (??%%→?); #EQ destruct 

48  ] 

49   * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I} 

50   ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); // 

51   * [2: * [2: * [2: #n ]]] #s whd in ⊢ (??%%→?); #EQ destruct @I 

52   %{it} %{(init_cost_label … p)} % 

53  ] 

54  qed. 

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