Changeset 3568

Timestamp:

Jun 17, 2015, 5:00:06 PM (6 years ago)

Author:

sacerdot

Message:

More progress.

File:

• LTS/frame_variable_pass.ma (modified) (5 diffs)

LTS/frame_variable_pass.ma

@@ -37 +37 @@
  λi,map.
   match i with
-  [ sNop ⇒ sNop
-  | sAss v e ⇒ sAss (map v) (map_exp e map)
+  [ sNop ⇒ Seq_i sNop
+  | sAss v e ⇒ Seq_i (sAss (map v) (map_exp e map))
   ].
 
@@ -52 +52 @@
     LOOP frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse  
            (trans_imp_instr instr map)
-| CALL f act_p opt_l instr ⇒ 
-      CALL frame_state_params flat_labels f 〈(\fst act_p),(map_exp (\snd act_p) map)〉 opt_l (trans_imp_instr instr map)
+| CALL f act_p opt_l instr ⇒
+    (CALL frame_state_params flat_labels f (map_exp (\snd act_p) map) opt_l
+      (SEQ … (PopReg (\fst act_p)) (None …) (trans_imp_instr instr map)))
 | IO lin io lout instr ⇒ ?
 ].
@@ -72 +73 @@
 definition store_rel : (variable → variable) → store_t → frame_store_t → Prop ≝ 
 λmap,st1,st2.
-All2 … (λel1,el2.\snd el1 = \snd el2 ∧ environment_rel map (\fst el1) (\fst el2))
+All2 ?? (λel1,el2.environment_rel map (\fst el1) el2)
  st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.
 
@@ -79 +80 @@
   store_rel m (〈env,var〉::l) st →
    ∃hd,tl,fpsp.
-    st = 〈〈hd,var〉::tl,fpsp〉 ∧
+    st = 〈hd::tl,fpsp〉 ∧
      store_rel m l 〈tl,fpsp〉 ∧
       environment_rel m env hd.
- #m #env #var #l * #env #fpsp * whd in ⊢ (% → ?); cases env [*] normalize nodelta
- * #frame #var' #frames ** #EQ destruct #Rel #ALL #FPSP
+ #m #env #var #l * #xx #fpsp * whd in ⊢ (% → ?); cases xx [*] normalize nodelta
+ #frame #frames * #Rel1 #ALL #EQ destruct (skip fpsp)
  %{frame} %{frames} %{fpsp} % // % // % //
 qed.
 
 definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels → 
-Program frame_env_params imp_instr_params flat_labels ≝ λmap,prog.
+Program frame_env_params frame_instr_params flat_labels ≝ λmap,prog.
 mk_Program ??? 
 (foldr … 
-   (λx,tail.(mk_env_item … 
-               (mk_signature frame_env_params … (f_name … (f_sig … x)) it (f_ret …(f_sig … x))) 
-               (f_lab … x) (trans_imp_instr (f_body … x) map)) :: tail) (nil ?) (env … prog))
+   (λx,tail.(mk_env_item …
+               (mk_signature frame_env_params … (f_name … (f_sig … x)) it ?(*(f_ret …(f_sig … x))*))
+               (f_lab … x) (trans_imp_instr (f_body ? imp_instr_params ? x) map)) :: tail) (nil ?) (env … prog))
 (trans_imp_instr (main … prog) map).
+@(f_ret … (f_sig … x))
+qed.
 
 definition trans_imp_cont ≝
@@ -185 +188 @@
   assign_var (〈env,var〉::tl) v val = Some … st2 →
    ∃st2'.
-    frame_assign_var 〈〈frame,var〉::frames,fpsp〉 (m v) val = Some … st2' ∧
+    frame_assign_var 〈frame::frames,fpsp〉 (m v) val = Some … st2' ∧
      store_rel m st2 st2'.
  #m #env #var #tl #v #val #frame #frames #st2 #fpsp #Rel1 #Rel2