source: LTS/frame_variable_pass.ma @ 3563

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

bind_inversion on Opt moved to utils + some progress

File size: 6.4 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
36let rec trans_imp_instr (i : imp_Instructions) (map : variable → variable) on i : frame_Instructions  ≝
37match i with
38[ EMPTY ⇒ EMPTY …
39| RETURN rt ⇒ RETURN … rt
40| SEQ seq opt_l i ⇒
41    match seq with
42    [ sNop ⇒ SEQ … sNop opt_l (trans_imp_instr i map)
43    | sAss v e ⇒ SEQ frame_state_params flat_labels (sAss (map v) (map_exp e map)) opt_l (trans_imp_instr i map)
44    ]
45| COND cond ltrue i_true lfalse i_false instr ⇒
46    COND frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse (trans_imp_instr i_false map)
47           (trans_imp_instr instr map)
48| LOOP cond ltrue i_true lfalse instr ⇒
49    LOOP frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse 
50           (trans_imp_instr instr map)
51| CALL f act_p opt_l instr ⇒
52      CALL frame_state_params flat_labels f 〈(\fst act_p),(map_exp (\snd act_p) map)〉 opt_l (trans_imp_instr instr map)
53| IO lin io lout instr ⇒ ?
54].
55cases io qed.
56
57
58let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝
59match l1 with
60[ nil ⇒ match l2 with [nil ⇒ True | cons _ _ ⇒ False]
61| cons x xs ⇒ match l2 with [nil ⇒ False | cons y ys ⇒ f x y ∧ All2 … f xs ys]
62].
63
64definition environment_rel : (variable → variable) → environment → activation_frame → Prop ≝
65λmap,st1,st2.
66 All … (λx.let 〈v,val〉 ≝ x in read_frame … st2 (to_shift + (map v)) O = return val)
67  st1.
68
69definition store_rel : (variable → variable) → store_t → frame_store_t → Prop ≝
70λmap,st1,st2.
71All2 … (λel1,el2.\snd el1 = \snd el2 ∧ environment_rel map (\fst el1) (\fst el2))
72 st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.
73
74definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels →
75Program frame_env_params imp_instr_params flat_labels ≝ λmap,prog.
76mk_Program ???
77(foldr …
78   (λx,tail.(mk_env_item …
79               (mk_signature frame_env_params … (f_name … (f_sig … x)) it (f_ret …(f_sig … x)))
80               (f_lab … x) (trans_imp_instr (f_body … x) map)) :: tail) (nil ?) (env … prog))
81(trans_imp_instr (main … prog) map).
82
83definition imp_variable_pass_rel ≝ 
84λmap : variable → variable.
85λprog : Program imp_state_params imp_state_params imp_state_params.
86let t_prog ≝ trans_imp_prog map prog in
87mk_relations flat_labels (operational_semantics imp_state_params imp_sem_state_params prog)
88 (operational_semantics frame_state_params frame_sem_state_params t_prog)
89(λs1,s2.store_rel map (store … s1) (store … s2) ∧ code … s2 = trans_imp_instr (code … s1) map ∧ 
90cont … s2 = foldr … (λx,rem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) (cont … s1))
91(λ_.λ_.True).
92
93lemma eval_cond_ok:
94 ∀m: variable → variable.
95  ∀e: expr.
96  let e' ≝ map_exp e m in
97   ∀env: environment.
98    ∀env': activation_frame.
99     environment_rel m env env' →
100      ∀val.
101       sem_expr env e = Some … val →
102        frame_sem_expr env' e' = Some … val.
103 #m #e elim e
104 [ #v #env elim env
105   [ #env' #_ #val #abs normalize in abs; destruct
106   | * #var #val #tl #IH #env' * #RF #Htl #val'
107     whd in ⊢ (??%? → ?); inversion (?==?) #Hv_var normalize nodelta
108     [ #Hval_val' destruct >(\P Hv_var) assumption
109     | #Hread_tl @IH // assumption ]]
110 | normalize //
111 |*: #e1 #e2 #IH1 #IH2 #env #env' #Rel #v
112   change with (!x ← ?; ? = return ?) in match (sem_expr ?? = Some ??);
113   #H cases (bind_inversion ????? H) -H #v1 * #He1
114   #H cases (bind_inversion ????? H) -H #v2 * #He2
115   #H normalize in H; destruct
116   change with (m_bind ?????) in ⊢ (??%?);
117   >(IH1 … He1) // >(IH2 … He2) // ]
118qed.
119
120definition simulation_imp_frame ≝
121λprog : Program imp_state_params imp_state_params imp_state_params.
122λmap : variable → variable.
123λprf : All … (λx.map (f_pars imp_state_params imp_state_params (f_sig … x)) = O) (env … prog).
124mk_simulation_conditions … (imp_variable_pass_rel map prog) ???????????.
125cases daemon (*TODO*)
126qed.
127
128(*
129[ #s1 #s2 ** #H1 #H2 #H3 whd in match (as_initial ???); (*store iniziali in relazione*) cases daemon
130| cases daemon
131| cases daemon
132| #s1 #s2 #s1' #H inversion H
133  [ #s11 #s22 * #act #instr #cont #EQcode_s11 #EQcont_s11 #EQ #EQ1 destruct #EQstore #Hio1 #Hio2
134    #act_no_ret #EQ1 #EQ2 #EQ3 destruct #_ ** #Hstore #EQcode #EQcont #_ #_
135    %{(mk_state … (code … s22) (cont … s22) (store … s2) (io_info … s22))}
136    %{(t_ind … (t_base …))}
137    [2: @(cost_act … (None ?))
138    | @hide_prf whd applyS(empty) [9: <EQcode assumption |2: normalize % * |3: % |4: cases daemon (*da mettere a posto io *)
139    |5: % |6: % |7: % |8: <EQcont assumption |*:]
140    | % [ % // % // ] %1 %2 [cases daemon] %1 cases daemon
141    ]
142  |*: cases daemon 
143  ]
144|*: cases daemon
145]
146qed.*)
147   
148   
Note: See TracBrowser for help on using the repository browser.