Changeset 3577
- Timestamp:
- Jun 19, 2015, 6:31:59 PM (6 years ago)
- Location:
- LTS
- Files:
-
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/frame_variable_pass.ma
r3575 r3577 19 19 definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝ 20 20 λA,B,f,a,b,x.if x == a then b else f x. 21 22 let rec get_expr_bound (e : expr) on e : ℕ ≝ 23 match e with 24 [ Var v ⇒ S v 25 | Const n ⇒ O 26 | Plus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2) 27 | Minus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2) 28 ]. 29 30 let rec get_cond_bound (c : condition) on c : ℕ ≝ 31 match c with 32 [Eq e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2) 33 | Not c ⇒ get_cond_bound c 34 ]. 35 36 let rec get_instr_bound (i : frame_Instructions) ≝ 37 match i with 38 [ EMPTY ⇒ O 39 | RETURN exp ⇒ get_expr_bound exp 40 | SEQ seq opt_l instr ⇒ 41 let c_bound ≝ get_instr_bound instr in 42 match seq with 43 [ Seq_i seq' ⇒ 44 match seq' with [ sAss v e ⇒ max (get_expr_bound e) c_bound ] 45 | PopReg v ⇒ max (S v) c_bound 46 ] 47 | COND cond ltrue i_true lfalse i_false instr ⇒ 48 let i_true_bound ≝ get_instr_bound i_true in 49 let i_false_bound ≝ get_instr_bound i_false in 50 let c_bound ≝ get_instr_bound instr in 51 max (get_cond_bound cond) (max i_true_bound (max i_false_bound c_bound)) 52 | LOOP cond ltrue i_true lfalse instr ⇒ 53 let i_true_bound ≝ get_instr_bound i_true in 54 let c_bound ≝ get_instr_bound instr in 55 max (get_cond_bound cond) (max i_true_bound c_bound) 56 | CALL f act_p opt_l instr ⇒ 57 let c_bound ≝ get_instr_bound instr in 58 max (get_expr_bound act_p) c_bound 59 | IO lin io lout instr ⇒ ? 60 ]. 61 cases io 62 qed. 21 63 22 64 let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝ … … 92 134 (foldr … 93 135 (λx,tail.(mk_env_item … 94 (mk_signature frame_env_params … (f_name … (f_sig … x)) it?(*(f_ret …(f_sig … x))*))136 (mk_signature frame_env_params … (f_name … (f_sig … x)) 14 ?(*(f_ret …(f_sig … x))*)) 95 137 (f_lab … x) (trans_imp_instr (f_body ? imp_instr_params ? x) map)) :: tail) (nil ?) (env … prog)) 96 138 (trans_imp_instr (main … prog) map). -
LTS/stack.ma
r3575 r3577 130 130 131 131 132 let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝133 match n with134 [ O ⇒ nil ?135 | S m ⇒ a :: list_n … a m136 ].137 138 132 definition stack_signature≝signature stack_state_params stack_state_params. 139 133 -
LTS/variable.ma
r3575 r3577 119 119 definition frame_store_t≝ DeqProd (DeqSet_List activation_frame) (DeqProd DeqNat DeqNat). (*frame_pointer e return register*) 120 120 121 definition frame_env_params ≝ mk_env_params unit.121 definition frame_env_params ≝ mk_env_params ℕ. 122 122 123 123 inductive frame_seq_i : Type[0] ≝ … … 185 185 definition frame_signature≝signature frame_state_params frame_state_params. 186 186 187 let rec list_n (A :Type[0]) (a : A) (n :ℕ) on n : list A ≝ 188 match n with 189 [ O ⇒ nil ? 190 | S m ⇒ a :: list_n … a m 191 ]. 192 187 193 definition frame_eval_call:frame_signature→ expr → frame_store_t → (option frame_store_t)≝ 188 194 λsgn,e,st. 189 195 !env ← frame_current_env … st; 190 196 !n ← frame_sem_expr env e; 191 frame_assign_var 〈(( nil ?)::(\fst st)),(\snd st)〉 to_shift n.197 frame_assign_var 〈((list_n … O (pred (to_shift + (f_pars … sgn))))::(\fst st)),(\snd st)〉 to_shift n. 192 198 193 199 definition frame_return_call:expr→ frame_store_t→ (option frame_store_t)≝ -
LTS/variable_stack_pass.ma
r3575 r3577 32 32 λl,i.foldr … (λc,instr.SEQ stack_state_params flat_labels (push c) (None ?) instr) i l. 33 33 34 let rec get_expr_bound (e : expr) on e : ℕ ≝ 35 match e with 36 [ Var v ⇒ S v 37 | Const n ⇒ O 38 | Plus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2) 39 | Minus e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2) 40 ]. 41 42 let rec get_cond_bound (c : condition) on c : ℕ ≝ 43 match c with 44 [Eq e1 e2 ⇒ max (get_expr_bound e1) (get_expr_bound e2) 45 | Not c ⇒ get_cond_bound c 46 ]. 47 48 let rec trans_var_instr (i : frame_Instructions) on i : (stack_Instructions × ℕ) ≝ 34 let rec trans_var_instr (i : frame_Instructions) on i : stack_Instructions ≝ 49 35 match i with 50 [ EMPTY ⇒ 〈EMPTY …,O〉51 | RETURN exp ⇒ 〈list_combinators_to_instructions (trans_expr exp) (RETURN … it),get_expr_bound exp〉36 [ EMPTY ⇒ EMPTY … 37 | RETURN exp ⇒ list_combinators_to_instructions (trans_expr exp) (RETURN … it) 52 38 | SEQ seq opt_l instr ⇒ 53 let 〈t_instr,c_bound〉≝ trans_var_instr … instr in39 let t_instr ≝ trans_var_instr … instr in 54 40 match seq with 55 41 [ Seq_i seq' ⇒ 56 42 match seq' with 57 [ sAss v e ⇒ 〈list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr), 58 max (get_expr_bound e) c_bound〉 43 [ sAss v e ⇒ list_combinators_to_instructions (trans_expr e) (SEQ … (pop_Ass v) opt_l t_instr) 59 44 ] 60 | PopReg v ⇒ 〈SEQ stack_instr_params ? (popreg v) opt_l t_instr,max (S v) c_bound〉45 | PopReg v ⇒ SEQ stack_instr_params ? (popreg v) opt_l t_instr 61 46 ] 62 47 | COND cond ltrue i_true lfalse i_false instr ⇒ 63 let 〈t_i_true,i_true_bound〉 ≝ trans_var_instr … i_true in 64 let 〈t_i_false,i_false_bound〉 ≝ trans_var_instr … i_false in 65 let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in 66 〈list_combinators_to_instructions (trans_cond cond) (COND … it ltrue t_i_true lfalse t_i_false t_instr), 67 max (get_cond_bound cond) (max i_true_bound (max i_false_bound c_bound))〉 48 let t_i_true ≝ trans_var_instr … i_true in 49 let t_i_false ≝ trans_var_instr … i_false in 50 let t_instr ≝ trans_var_instr … instr in 51 list_combinators_to_instructions (trans_cond cond) (COND … it ltrue t_i_true lfalse t_i_false t_instr) 68 52 | LOOP cond ltrue i_true lfalse instr ⇒ 69 let 〈t_i_true,i_true_bound〉 ≝ trans_var_instr … i_true in 70 let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in 71 〈LOOP stack_state_params flat_labels (trans_cond … cond) ltrue t_i_true lfalse t_instr, 72 max (get_cond_bound cond) (max i_true_bound c_bound)〉 53 let t_i_true ≝ trans_var_instr … i_true in 54 let t_instr ≝ trans_var_instr … instr in 55 LOOP stack_state_params flat_labels (trans_cond … cond) ltrue t_i_true lfalse t_instr 73 56 | CALL f act_p opt_l instr ⇒ 74 let 〈t_instr,c_bound〉 ≝ trans_var_instr … instr in 75 〈list_combinators_to_instructions (trans_expr act_p) (CALL … f it opt_l t_instr), 76 max (get_expr_bound act_p) c_bound〉 57 let t_instr ≝ trans_var_instr … instr in 58 list_combinators_to_instructions (trans_expr act_p) (CALL … f it opt_l t_instr) 77 59 | IO lin io lout instr ⇒ ? 78 60 ]. … … 80 62 qed. 81 63 82 definition trans_var_prog : Program frame_env_params frame_instr_params flat_labels → 83 (Program stack_env_params stack_instr_params flat_labels × ℕ) ≝ 64 definition trans_var_prog : 65 Program frame_env_params frame_instr_params flat_labels → 66 Program stack_env_params stack_instr_params flat_labels ≝ 84 67 λprog. 85 let 〈t_main,m_bound〉≝ trans_var_instr … (main … prog) in86 〈(mk_Program …68 let t_main ≝ trans_var_instr … (main … prog) in 69 (mk_Program … 87 70 (foldr … 88 (λx,tail.(let 〈t_body,bound〉≝ trans_var_instr … (f_body … x) in71 (λx,tail.(let t_body ≝ trans_var_instr … (f_body … x) in 89 72 mk_env_item … 90 (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … x)) boundit) (f_lab … x) t_body) :: tail)73 (mk_signature stack_env_params stack_instr_params (f_name … (f_sig … x)) (f_pars … x) it) (f_lab … x) t_body) :: tail) 91 74 (nil ?) (env … prog)) 92 t_main ),m_bound〉.75 t_main (initial_act … prog)). 93 76 94 77 include "Simulation.ma". … … 103 86 (mk_relations flat_labels (operational_semantics frame_state_params frame_sem_state_params prog) 104 87 (operational_semantics stack_state_params (stack_sem_state_params bound) t_prog) 105 (λs1,s2.store … s1 = store … s2 ∧ code … s2 = (\fst (trans_var_instr (code … s1))) ∧106 cont … s2 = foldr … (λx,tail. 〈(\fst x), (\fst (trans_var_instr (\snd x)))〉 :: tail) (nil ?) (cont … s1))88 (λs1,s2.store … s1 = store … s2 ∧ code … s2 = trans_var_instr (code … s1) ∧ 89 cont … s2 = foldr … (λx,tail. 〈(\fst x),trans_var_instr (\snd x)〉 :: tail) (nil ?) (cont … s1)) 107 90 (λ_.λ_.True)). 108 109 91 110 92 let rec expr_fv (e : expr) on e : list variable ≝ … … 228 210 definition simulation_imp_frame : 229 211 ∀prog : Program frame_state_params frame_state_params frame_state_params. 230 ∀ t_prog,bound.〈t_prog,bound〉 = trans_var_prog prog →231 simulation_conditions … (frame_variable_pass_rel prog t_progbound) ≝232 λprog, t_prog,bound,good_trans.212 ∀bound: ℕ. 213 simulation_conditions … (frame_variable_pass_rel prog (trans_var_prog prog) bound) ≝ 214 λprog,bound. 233 215 mk_simulation_conditions …. 234 216 cases daemon 235 217 qed. 236
Note: See TracChangeset
for help on using the changeset viewer.