Changeset 3568
- Timestamp:
- Jun 17, 2015, 5:00:06 PM (6 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/frame_variable_pass.ma
r3564 r3568 37 37 λi,map. 38 38 match i with 39 [ sNop ⇒ sNop40 | sAss v e ⇒ sAss (map v) (map_exp e map)39 [ sNop ⇒ Seq_i sNop 40 | sAss v e ⇒ Seq_i (sAss (map v) (map_exp e map)) 41 41 ]. 42 42 … … 52 52 LOOP frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse 53 53 (trans_imp_instr instr map) 54 | CALL f act_p opt_l instr ⇒ 55 CALL frame_state_params flat_labels f 〈(\fst act_p),(map_exp (\snd act_p) map)〉 opt_l (trans_imp_instr instr map) 54 | CALL f act_p opt_l instr ⇒ 55 (CALL frame_state_params flat_labels f (map_exp (\snd act_p) map) opt_l 56 (SEQ … (PopReg (\fst act_p)) (None …) (trans_imp_instr instr map))) 56 57 | IO lin io lout instr ⇒ ? 57 58 ]. … … 72 73 definition store_rel : (variable → variable) → store_t → frame_store_t → Prop ≝ 73 74 λmap,st1,st2. 74 All2 … (λel1,el2.\snd el1 = \snd el2 ∧ environment_rel map (\fst el1) (\fst el2))75 All2 ?? (λel1,el2.environment_rel map (\fst el1) el2) 75 76 st1 (\fst st2) ∧ \snd st2 = 〈O,O〉. 76 77 … … 79 80 store_rel m (〈env,var〉::l) st → 80 81 ∃hd,tl,fpsp. 81 st = 〈 〈hd,var〉::tl,fpsp〉 ∧82 st = 〈hd::tl,fpsp〉 ∧ 82 83 store_rel m l 〈tl,fpsp〉 ∧ 83 84 environment_rel m env hd. 84 #m #env #var #l * # env #fpsp * whd in ⊢ (% → ?); cases env[*] normalize nodelta85 * #frame #var' #frames ** #EQ destruct #Rel #ALL #FPSP85 #m #env #var #l * #xx #fpsp * whd in ⊢ (% → ?); cases xx [*] normalize nodelta 86 #frame #frames * #Rel1 #ALL #EQ destruct (skip fpsp) 86 87 %{frame} %{frames} %{fpsp} % // % // % // 87 88 qed. 88 89 89 90 definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels → 90 Program frame_env_params imp_instr_params flat_labels ≝ λmap,prog.91 Program frame_env_params frame_instr_params flat_labels ≝ λmap,prog. 91 92 mk_Program ??? 92 93 (foldr … 93 (λx,tail.(mk_env_item … 94 (mk_signature frame_env_params … (f_name … (f_sig … x)) it (f_ret …(f_sig … x)))95 (f_lab … x) (trans_imp_instr (f_body …x) map)) :: tail) (nil ?) (env … prog))94 (λx,tail.(mk_env_item … 95 (mk_signature frame_env_params … (f_name … (f_sig … x)) it ?(*(f_ret …(f_sig … x))*)) 96 (f_lab … x) (trans_imp_instr (f_body ? imp_instr_params ? x) map)) :: tail) (nil ?) (env … prog)) 96 97 (trans_imp_instr (main … prog) map). 98 @(f_ret … (f_sig … x)) 99 qed. 97 100 98 101 definition trans_imp_cont ≝ … … 185 188 assign_var (〈env,var〉::tl) v val = Some … st2 → 186 189 ∃st2'. 187 frame_assign_var 〈 〈frame,var〉::frames,fpsp〉 (m v) val = Some … st2' ∧190 frame_assign_var 〈frame::frames,fpsp〉 (m v) val = Some … st2' ∧ 188 191 store_rel m st2 st2'. 189 192 #m #env #var #tl #v #val #frame #frames #st2 #fpsp #Rel1 #Rel2
Note: See TracChangeset
for help on using the changeset viewer.