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 | |
---|
15 | include "Simulation.ma". |
---|
16 | include "variable.ma". |
---|
17 | include alias "arithmetics/nat.ma". |
---|
18 | |
---|
19 | definition 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 | |
---|
22 | let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝ |
---|
23 | match 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 | |
---|
30 | let rec map_cond (c : condition) (map : variable → variable) on c : condition ≝ |
---|
31 | match 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 | |
---|
36 | let rec trans_imp_instr (i : imp_Instructions) (map : variable → variable) on i : frame_Instructions ≝ |
---|
37 | match 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 | ]. |
---|
55 | cases io qed. |
---|
56 | |
---|
57 | |
---|
58 | let rec All2 (A,B : Type[0]) (f : A → B → Prop) (l1 : list A) (l2 : list B) on l1 : Prop ≝ |
---|
59 | match 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 | |
---|
64 | definition 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 | |
---|
69 | definition store_rel : (variable → variable) → store_t → frame_store_t → Prop ≝ |
---|
70 | λmap,st1,st2. |
---|
71 | All2 … (λel1,el2.\snd el1 = \snd el2 ∧ environment_rel map (\fst el1) (\fst el2)) |
---|
72 | st1 (\fst st2) ∧ \snd st2 = 〈O,O〉. |
---|
73 | |
---|
74 | definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels → |
---|
75 | Program frame_env_params imp_instr_params flat_labels ≝ λmap,prog. |
---|
76 | mk_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 | |
---|
83 | definition imp_variable_pass_rel ≝ |
---|
84 | λmap : variable → variable. |
---|
85 | λprog : Program imp_state_params imp_state_params imp_state_params. |
---|
86 | let t_prog ≝ trans_imp_prog map prog in |
---|
87 | mk_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 ∧ |
---|
90 | cont … s2 = foldr … (λx,rem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) (cont … s1)) |
---|
91 | (λ_.λ_.True). |
---|
92 | |
---|
93 | lemma 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) // ] |
---|
118 | qed. |
---|
119 | |
---|
120 | definition 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). |
---|
124 | mk_simulation_conditions … (imp_variable_pass_rel map prog) ???????????. |
---|
125 | cases daemon (*TODO*) |
---|
126 | qed. |
---|
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 | ] |
---|
146 | qed.*) |
---|
147 | |
---|
148 | |
---|