Ignore:
Timestamp:
Jun 17, 2015, 5:00:06 PM (4 years ago)
Author:
sacerdot
Message:

More progress.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/frame_variable_pass.ma

    r3564 r3568  
    3737 λi,map.
    3838  match i with
    39   [ sNop ⇒ sNop
    40   | 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))
    4141  ].
    4242
     
    5252    LOOP frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse 
    5353           (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)))
    5657| IO lin io lout instr ⇒ ?
    5758].
     
    7273definition store_rel : (variable → variable) → store_t → frame_store_t → Prop ≝
    7374λmap,st1,st2.
    74 All2 … (λel1,el2.\snd el1 = \snd el2 ∧ environment_rel map (\fst el1) (\fst el2))
     75All2 ?? (λel1,el2.environment_rel map (\fst el1) el2)
    7576 st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.
    7677
     
    7980  store_rel m (〈env,var〉::l) st →
    8081   ∃hd,tl,fpsp.
    81     st = 〈〈hd,var〉::tl,fpsp〉 ∧
     82    st = 〈hd::tl,fpsp〉 ∧
    8283     store_rel m l 〈tl,fpsp〉 ∧
    8384      environment_rel m env hd.
    84  #m #env #var #l * #env #fpsp * whd in ⊢ (% → ?); cases env [*] normalize nodelta
    85  * #frame #var' #frames ** #EQ destruct #Rel #ALL #FPSP
     85 #m #env #var #l * #xx #fpsp * whd in ⊢ (% → ?); cases xx [*] normalize nodelta
     86 #frame #frames * #Rel1 #ALL #EQ destruct (skip fpsp)
    8687 %{frame} %{frames} %{fpsp} % // % // % //
    8788qed.
    8889
    8990definition 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.
     91Program frame_env_params frame_instr_params flat_labels ≝ λmap,prog.
    9192mk_Program ???
    9293(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))
    9697(trans_imp_instr (main … prog) map).
     98@(f_ret … (f_sig … x))
     99qed.
    97100
    98101definition trans_imp_cont ≝
     
    185188  assign_var (〈env,var〉::tl) v val = Some … st2 →
    186189   ∃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' ∧
    188191     store_rel m st2 st2'.
    189192 #m #env #var #tl #v #val #frame #frames #st2 #fpsp #Rel1 #Rel2
Note: See TracChangeset for help on using the changeset viewer.