Last change
on this file since 3037 was
3037,
checked in by tranquil, 8 years ago

 ADDRESS joint instruction now has also an offset
 corrected call to pointer (needed to clear the accumulator)
 now we make sure globals contain also function names
LINToASM will be fixed in an upcoming commit

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  

[3037]  31  definition LIN_premain : ∀p : lin_program. 

 32  joint_closed_internal_function LIN (prog_names … p) ≝ 

[2946]  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〉 ; 

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

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

[3037]  39  mk_joint_internal_function LIN (prog_names … p) 

[2946]  40  (mk_universe … (p0 (p0 one))) 

 41  (mk_universe … one) 

 42  it it 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.