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

main novelties:
 there is an inbuilt stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
 a premain is added semantically to the global env, so initial cost label and main call and return are observed
 proper initialization is now in LINToASM (to be sure, endianess should be checked ;)
The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File size:
1.6 KB

Rev  Line  

[1378]  1  include "LIN/joint_LTL_LIN.ma". 

[491]  2  

[2286]  3  definition LIN ≝ mk_lin_params LTL_LIN. 

[1168]  4  

[2286]  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. 

[1168]  27  

[2946]  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)) 4 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.