source: LTS/frame_variable_pass.ma @ 3564

Last change on this file since 3564 was 3564, checked in by sacerdot, 4 years ago

...

File size: 9.7 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "Simulation.ma".
16include "variable.ma".
17include alias "arithmetics/nat.ma".
18
19definition update_fun : ∀A : DeqSet.∀B : Type[0].(A → B) → A → B → A → B ≝
20λA,B,f,a,b,x.if x == a then b else f x.
21
22let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝
23match e with
24[ Var v ⇒ Var (map v)
25| Const n ⇒ Const n
26| Plus e1 e2 ⇒ Plus (map_exp e1 map) (map_exp e2 map)
27| Minus e1 e2 ⇒ Minus (map_exp e1 map) (map_exp e2 map)
28].
29
30let rec map_cond (c : condition) (map : variable → variable) on c : condition ≝
31match c with
32[Eq e1 e2 ⇒ Eq (map_exp e1 map) (map_exp e2 map)
33| Not c1 ⇒ Not (map_cond c1 map)
34].
35
36definition map_seq ≝
37 λi,map.
38  match i with
39  [ sNop ⇒ sNop
40  | sAss v e ⇒ sAss (map v) (map_exp e map)
41  ].
42
43let rec trans_imp_instr (i : imp_Instructions) (map : variable → variable) on i : frame_Instructions  ≝
44match i with
45[ EMPTY ⇒ EMPTY …
46| RETURN rt ⇒ RETURN … rt
47| SEQ seq opt_l i ⇒ SEQ … (map_seq seq map) opt_l (trans_imp_instr i map)
48| COND cond ltrue i_true lfalse i_false instr ⇒
49    COND frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse (trans_imp_instr i_false map)
50           (trans_imp_instr instr map)
51| LOOP cond ltrue i_true lfalse instr ⇒
52    LOOP frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse 
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)
56| IO lin io lout instr ⇒ ?
57].
58cases io qed.
59
60
61let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝
62match l1 with
63[ nil ⇒ match l2 with [nil ⇒ True | cons _ _ ⇒ False]
64| cons x xs ⇒ match l2 with [nil ⇒ False | cons y ys ⇒ f x y ∧ All2 … f xs ys]
65].
66
67definition environment_rel : (variable → variable) → environment → activation_frame → Prop ≝
68λmap,st1,st2.
69 All … (λx.let 〈v,val〉 ≝ x in read_frame … st2 (to_shift + (map v)) O = return val)
70  st1.
71
72definition store_rel : (variable → variable) → store_t → frame_store_t → Prop ≝
73λmap,st1,st2.
74All2 … (λel1,el2.\snd el1 = \snd el2 ∧ environment_rel map (\fst el1) (\fst el2))
75 st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.
76
77lemma store_rel_inv:
78 ∀m,env,var,l,st.
79  store_rel m (〈env,var〉::l) st →
80   ∃hd,tl,fpsp.
81    st = 〈〈hd,var〉::tl,fpsp〉 ∧
82     store_rel m l 〈tl,fpsp〉 ∧
83      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
86 %{frame} %{frames} %{fpsp} % // % // % //
87qed.
88
89definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels →
90Program frame_env_params imp_instr_params flat_labels ≝ λmap,prog.
91mk_Program ???
92(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))
96(trans_imp_instr (main … prog) map).
97
98definition trans_imp_cont ≝
99 λmap,cont.
100  foldr … (λx:(ActionLabel flat_labels)×?.λrem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) cont.
101
102definition imp_variable_pass_rel ≝ 
103λmap : variable → variable.
104λprog : Program imp_state_params imp_state_params imp_state_params.
105let t_prog ≝ trans_imp_prog map prog in
106mk_relations flat_labels (operational_semantics imp_state_params imp_sem_state_params prog)
107 (operational_semantics frame_state_params frame_sem_state_params t_prog)
108(λs1,s2.store_rel map (store … s1) (store … s2) ∧ code … s2 = trans_imp_instr (code … s1) map ∧ 
109cont … s2 = trans_imp_cont map (cont … s1))
110(λ_.λ_.True).
111
112lemma map_exp_ok:
113 ∀m: variable → variable.
114  ∀e: expr.
115  let e' ≝ map_exp e m in
116   ∀env: environment.
117    ∀env': activation_frame.
118     environment_rel m env env' →
119      ∀val.
120       sem_expr env e = Some … val →
121        frame_sem_expr env' e' = Some … val.
122 #m #e elim e
123 [ #v #env elim env
124   [ #env' #_ #val #abs normalize in abs; destruct
125   | * #var #val #tl #IH #env' * #RF #Htl #val'
126     whd in ⊢ (??%? → ?); inversion (?==?) #Hv_var normalize nodelta
127     [ #Hval_val' destruct >(\P Hv_var) assumption
128     | #Hread_tl @IH // assumption ]]
129 | normalize //
130 |*: #e1 #e2 #IH1 #IH2 #env #env' #Rel #v
131   change with (m_bind ?????) in match (sem_expr ??);
132   #H cases (bind_inversion ????? H) -H #v1 * #He1
133   #H cases (bind_inversion ????? H) -H #v2 * #He2
134   #H normalize in H; destruct
135   change with (m_bind ?????) in ⊢ (??%?);
136   >(IH1 … He1) // >(IH2 … He2) // ]
137qed.
138
139lemma map_cond_ok:
140 ∀m: variable → variable.
141  ∀e: condition.
142  let e' ≝ map_cond e m in
143   ∀env: environment.
144    ∀env': activation_frame.
145     environment_rel m env env' →
146      ∀val.
147       sem_condition env e = Some … val →
148        frame_sem_condition env' e' = Some … val.
149 #m #e elim e
150 [ #e1 #e2 #env #env' #Rel #v
151   change with (m_bind ?????) in ⊢ (??%? → ?);
152   #H cases (bind_inversion ????? H) -H #v1 * #He1
153   #H cases (bind_inversion ????? H) -H #v2 * #He2
154   #H normalize in H; destruct
155   change with (m_bind ?????) in ⊢ (??%?);
156   >(map_exp_ok … He1) // >(map_exp_ok … He2) //
157 | #c #IH #env #env' #Rel #v
158   change with (m_bind ?????) in ⊢ (??%? → ?);
159   #H cases (bind_inversion ????? H) -H #v' * #Hv'
160   #H normalize in H; destruct
161   change with (m_bind ?????) in ⊢ (??%?);
162   >(IH … Hv') // ]
163qed.
164
165lemma map_assign_ok:
166 ∀m,env,frame,v,val.
167  environment_rel m env frame →
168   environment_rel m (assign env v val) (assign_frame frame (m v) 0 val).
169 #m #env #frame #v #val #Rel whd in match assign_frame; normalize nodelta
170 elim env in Rel;
171 [ * % // whd in ⊢ (??%?); cases daemon (* NTH-UPDATE *)
172 | * #v' #val' #frames #IH * #Hread #Hall change with (environment_rel ???) in Hall;
173   whd in match (assign ???);
174   inversion (v==v') normalize nodelta
175   [2: #Ineq % [ cases daemon (* NTH-UPDATE *) | @IH // ]
176   | #EQ % [ cases daemon (* NTH-UPDATE *)
177   |change with (environment_rel ???) cases daemon (* NOT IMPLIED BY Hall BECAUSE
178    OF DUPLICATES :-( *)]]]
179qed.
180
181lemma map_assign_var_ok:
182 ∀m,env,var,tl,v,val,frame,frames,st2,fpsp.
183 store_rel m tl 〈frames,fpsp〉 →
184 environment_rel m env frame →
185  assign_var (〈env,var〉::tl) v val = Some … st2 →
186   ∃st2'.
187    frame_assign_var 〈〈frame,var〉::frames,fpsp〉 (m v) val = Some … st2' ∧
188     store_rel m st2 st2'.
189 #m #env #var #tl #v #val #frame #frames #st2 #fpsp #Rel1 #Rel2
190 whd in ⊢ (??%? → ?); #EQ destruct
191 whd in match frame_assign_var; normalize nodelta % [2: % [%] | skip]
192 cases Rel1 -Rel1 #Rel3 #Rel4 destruct % // whd /6/
193qed.
194
195lemma map_seq_ok:
196 ∀m: variable → variable.
197  ∀e:seq_i.
198  let e' ≝ map_seq e m in
199   ∀st1.
200    ∀st1'.
201     store_rel m st1 st1' →
202      ∀st2.
203       imp_eval_seq e st1 = Some … st2 →
204        ∃st2'.
205         frame_eval_seq e' st1' = Some … st2' ∧
206          store_rel m st2 st2'.
207 #m * [2: #v #expr] #st1 * #st1' * #fp #sp #Rel #st2
208 whd in match imp_eval_seq; normalize nodelta
209 [2: #EQ destruct /3/
210 | cases st1 in Rel; normalize nodelta [ #_ #abs destruct ]
211   * #env #var #tl #Rel
212   cases (store_rel_inv … Rel) -Rel #frame * #frames * #fpsp ** #EQ destruct
213   #Rel1 #Rel2 normalize nodelta #H cases (bind_inversion ????? H) -H #val *
214   #Hval #H whd in match (frame_eval_seq ??); >(map_exp_ok … Rel2 … Hval)
215   normalize nodelta cases (map_assign_var_ok … Rel1 Rel2 … H) #st2' *
216   #H1 #H2 %{st2'} % // assumption ]
217qed.
218
219definition simulation_imp_frame ≝
220λprog : Program imp_state_params imp_state_params imp_state_params.
221λmap : variable → variable.
222λprf : All … (λx.map (f_pars imp_state_params imp_state_params (f_sig … x)) = O) (env … prog).
223mk_simulation_conditions … (imp_variable_pass_rel map prog) ???????????.
224[ #s1 #s2 ** #H1 #H2 #H3 whd in match (as_initial ???); (*store iniziali in relazione*) cases daemon
225| cases daemon
226| cases daemon
227| #s1 #s2 #s1' #H inversion H
228  [ #s11 #s22 * #act #instr #cont #EQcode_s11 #EQcont_s11 #EQ #EQ1 destruct #EQstore #Hio1 #Hio2
229    #act_no_ret #EQ1 #EQ2 #EQ3 destruct #_ ** #Hstore #EQcode #EQcont #_ #_
230    %{(mk_state … (trans_imp_instr (code … s22) map)
231      (trans_imp_cont map (cont … s22)) (store … s2) (io_info … s22))}
232    %{(t_ind … (t_base …))}
233    [2: @(cost_act … (None ?))
234    | @hide_prf whd applyS(empty)
235      [9: >EQcode >EQcode_s11 %
236      |2: normalize % *
237      |3: %
238      |4: cases daemon (*da mettere a posto io *)
239    |5: % |6: % |7: % |8: >EQcont >EQcont_s11 % |*:]
240    | % [ % // % // ] %1 %2 [cases daemon] %1 cases daemon
241    ]
242  |*: cases daemon 
243  ]
244|*: cases daemon
245]
246qed.
Note: See TracBrowser for help on using the repository browser.