Changeset 3561

Timestamp:

Jun 16, 2015, 2:39:12 PM (6 years ago)

Author:

piccolo

Message:

 

Location:

LTS

Files:

• Language.ma (modified) (2 diffs)
• frame_variable_pass.ma (modified) (3 diffs)
• variable.ma (modified) (5 diffs)

LTS/Language.ma

@@ -87 +87 @@
 ].
 
-
-(*
-lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) → 
-(i1 ≠ i2 → P false) → P (eq_instructions p i1 i2).
-#P #p #i1 elim i1
+lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,l_p,i1,i2.(i1 = i2 → P true) → 
+(i1 ≠ i2 → P false) → P (eq_instructions p l_p i1 i2).
+#P #p #l_p #i1 elim i1
 [* normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ
   lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ')
@@ -105 +103 @@
   [2,4: #ABS @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
         >(\b (refl …)) in ABS; #EQ destruct]
-  #EQseq inversion(eq_instructions ???) normalize nodelta #Heq_i2
-  [2,4: @H2 % #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct
-*)
+  #EQseq cases daemon
+|*: cases daemon
+qed.
 
 record env_params : Type[1] ≝ 

LTS/frame_variable_pass.ma

@@ -16 +16 @@
 include "variable.ma".
 
+definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝ 
+λA,B,f,a,b,x.if x == a then b else f x.
+
+let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝ 
+match e with
+[  Var v ⇒ Var (map v)
+| Const n ⇒ Const n
+| Plus e1 e2 ⇒ Plus (map_exp e1 map) (map_exp e2 map) 
+| Minus e1 e2 ⇒ Minus (map_exp e1 map) (map_exp e2 map)
+].
+
+let rec map_cond (c : condition) (map : variable → variable) on c : condition ≝ 
+match c with
+[Eq e1 e2 ⇒ Eq (map_exp e1 map) (map_exp e2 map)
+| Not c1 ⇒ Not (map_cond c1 map)
+].
+
+let rec trans_imp_instr (i : imp_Instructions) (map : variable → variable) on i : frame_Instructions  ≝ 
+match i with
+[ EMPTY ⇒ EMPTY …
+| RETURN rt ⇒ RETURN … rt
+| SEQ seq opt_l i ⇒ 
+    match seq with
+    [ sNop ⇒ SEQ … sNop opt_l (trans_imp_instr i map)
+    | sAss v e ⇒ SEQ frame_state_params flat_labels (sAss (map v) (map_exp e map)) opt_l (trans_imp_instr i map)
+    ]
+| COND cond ltrue i_true lfalse i_false instr ⇒ 
+    COND frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse (trans_imp_instr i_false map) 
+           (trans_imp_instr instr map)
+| LOOP cond ltrue i_true lfalse instr ⇒ 
+    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)
+| IO lin io lout instr ⇒ ?
+].
+cases io qed.
+
+
 let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝ 
 match l1 with
@@ -22 +61 @@
 ].
 
-definition store_rel : store_t → frame_store_t → Prop ≝ 
-λst1,st2.
-All2 … (λel1,el2.\snd el1 = \snd el2 ∧ All … (λx.let 〈v,val〉 ≝ x in read_frame … (\fst el2) (to_shift + val) O = return val) 
+definition store_rel : (variable → variable) → store_t → frame_store_t → Prop ≝ 
+λmap,st1,st2.
+All2 … (λel1,el2.\snd el1 = \snd el2 ∧ All … (λx.let 〈v,val〉 ≝ x in read_frame … (\fst el2) (to_shift + (map v)) O = return val) 
        (\fst el1)) st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.
-       
+
+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.
+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))
+(trans_imp_instr (main … prog) map).
+
 definition imp_variable_pass_rel ≝  
+λmap : variable → variable.
 λprog : Program imp_state_params imp_state_params imp_state_params.
+let t_prog ≝ trans_imp_prog map prog in
 mk_relations flat_labels (operational_semantics imp_state_params imp_sem_state_params prog)
- (operational_semantics frame_state_params frame_sem_state_params prog) 
-(λs1,s2.store_rel (store … s1) (store … s2) ∧ (code … s1) = (code … s2) ∧ (cont … s1) = (cont … s2))
-(λ_.λ_.False).
+ (operational_semantics frame_state_params frame_sem_state_params t_prog) 
+(λs1,s2.store_rel map (store … s1) (store … s2) ∧ code … s2 = trans_imp_instr (code … s1) map ∧  
+cont … s2 = foldr … (λx,rem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) (cont … s1))
+(λ_.λ_.True).
 
-definition simulation_imp_frame ≝ λprog.mk_simulation_conditions … (imp_variable_pass_rel prog) ???????????.
+definition simulation_imp_frame ≝ 
+λprog : Program imp_state_params imp_state_params imp_state_params.
+λmap : variable → variable.
+λprf : All … (λx.map (f_pars imp_state_params imp_state_params (f_sig … x)) = O) (env … prog).
+mk_simulation_conditions … (imp_variable_pass_rel map prog) ???????????.
+cases daemon (*TODO*)
+qed.
+
+(*
 [ #s1 #s2 ** #H1 #H2 #H3 whd in match (as_initial ???); (*store iniziali in relazione*) cases daemon
 | cases daemon
@@ -52 +111 @@
 |*: cases daemon
 ]
-qed.
+qed.*)
     
     

LTS/variable.ma

@@ -15 +15 @@
 include "imp.ma".
 
-definition to_shift : ℕ ≝ 3.
+definition to_shift : ℕ ≝ 2.
 
 definition activation_frame ≝ DeqSet_List DeqNat.
@@ -54 +54 @@
 definition frame_store_t≝ DeqProd (DeqSet_List (DeqProd activation_frame variable)) (DeqProd DeqNat DeqNat). (*frame_pointer e stack_pointer*)
 
+definition frame_env_params ≝ mk_env_params unit.
+
 definition frame_state_params:state_params≝
-mk_state_params imp_instr_params imp_env_params flat_labels frame_store_t (*DeqEnv*).
+mk_state_params imp_instr_params frame_env_params flat_labels frame_store_t (*DeqEnv*).
 
 definition frame_current_env:store_type frame_state_params→ option ?≝λs.!hd ← option_hd … (\fst s); return \fst hd.
@@ -91 +93 @@
 definition frame_eval_call:(signature frame_state_params imp_state_params)→ act_params_type frame_state_params → frame_store_t → (option frame_store_t)≝
 λsgn,e,st.
-  match sgn with 
-  [ mk_signature fun fpt rt ⇒
     let 〈var,act_exp〉 ≝ e in
     match (\fst st) with
@@ -98 +98 @@
     |cons hd tl⇒ let 〈env,v〉≝ hd in
                  !n ← frame_sem_expr env act_exp;
-                 frame_assign_var 〈(〈(nil ?),var〉::(\fst st)),(\snd st)〉 fpt n
-    ]
+                 frame_assign_var 〈(〈(nil ?),var〉::(\fst st)),(\snd st)〉 O n
   ].
 
@@ -124 +123 @@
 
 
-definition frame_envitem≝ (env_item imp_env_params imp_instr_params flat_labels).
+definition frame_envitem≝ (env_item frame_env_params imp_instr_params flat_labels).