1 | |
---|
2 | include "Csem.ma". |
---|
3 | |
---|
4 | include "extralib.ma". |
---|
5 | |
---|
6 | (* Some experimental definitions for an executable semantics. *) |
---|
7 | |
---|
8 | ndefinition bool_of_val_1 : val → type → res val ≝ |
---|
9 | λv,ty. match v with |
---|
10 | [ Vint i ⇒ match ty with |
---|
11 | [ Tint _ _ ⇒ OK ? (of_bool (¬eq i zero)) |
---|
12 | | Tpointer _ ⇒ OK ? (of_bool (¬eq i zero)) |
---|
13 | | _ ⇒ Error ? |
---|
14 | ] |
---|
15 | | Vfloat f ⇒ match ty with |
---|
16 | [ Tfloat _ ⇒ OK ? (of_bool (¬Fcmp Ceq f Fzero)) |
---|
17 | | _ ⇒ Error ? |
---|
18 | ] |
---|
19 | | Vptr _ _ ⇒ match ty with |
---|
20 | [ Tint _ _ ⇒ OK ? Vtrue |
---|
21 | | Tpointer _ ⇒ OK ? Vtrue |
---|
22 | | _ ⇒ Error ? |
---|
23 | ] |
---|
24 | | _ ⇒ Error ? |
---|
25 | ]. |
---|
26 | |
---|
27 | (* There's a lot more repetition than I'd like here, in large part because |
---|
28 | there's no way to introduce different numbers of hypotheses when doing the |
---|
29 | case distinctions. *) |
---|
30 | |
---|
31 | nlemma bool_of_val_1_ok : ∀v,ty,r. bool_of_val_1 v ty = OK ? r ↔ bool_of_val v ty r. |
---|
32 | #v ty r; @; |
---|
33 | ##[ |
---|
34 | nelim v; ##[ #H; nnormalize in H; ndestruct; ##| ##2,3: #x; ##| ##4: #x y; ##] |
---|
35 | ncases ty; |
---|
36 | ##[ ##1,10,19: #H; nnormalize in H; ndestruct; |
---|
37 | ##| #i s; nwhd in ⊢ (??%? → ?); nelim (eq_dec x zero); #H; |
---|
38 | ##[ nrewrite > H; nrewrite > (eq_true …); #H'; |
---|
39 | ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##] |
---|
40 | #H''; nrewrite > H''; /2/; |
---|
41 | ##| nrewrite > (eq_false …); //; #H'; |
---|
42 | ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##] |
---|
43 | #H''; nrewrite > H''; /3/; |
---|
44 | ##] |
---|
45 | ##|##3,9,13,18,21,27: #x H; nnormalize in H; ndestruct; |
---|
46 | ##| #t; nwhd in ⊢ (??%? → ?); nelim (eq_dec x zero); #H; |
---|
47 | ##[ nrewrite > H; nrewrite > (eq_true …); #H'; |
---|
48 | ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##] |
---|
49 | #H''; nrewrite > H''; /2/; |
---|
50 | ##| nrewrite > (eq_false …); //; #H'; |
---|
51 | ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##] |
---|
52 | #H''; nrewrite > H''; /3/; |
---|
53 | ##] |
---|
54 | ##| ##5,6,7,8,11,14,15,16,17,23,24,25,26: #a b H; nnormalize in H; ndestruct; |
---|
55 | ##| #f; nwhd in ⊢ (??%? → ?); nelim (eq_dec x Fzero); #H; |
---|
56 | ##[ nrewrite > H; nrewrite > (Feq_zero_true …); #H'; |
---|
57 | ncut (r = Vfalse); ##[ nwhd in H':(??(??%)?); ndestruct;//;##] |
---|
58 | #H''; nrewrite > H''; /2/; |
---|
59 | ##| nrewrite > (Feq_zero_false …); //; #H'; |
---|
60 | ncut (r = Vtrue); ##[ nwhd in H':(??(??%)?); ndestruct;//;##] |
---|
61 | #H''; nrewrite > H''; /3/; |
---|
62 | ##] |
---|
63 | ##| #i s H; nwhd in H:(??%?); |
---|
64 | ncut (r = Vtrue); ##[ nwhd in H:(??(??%)?); ndestruct;//;##] |
---|
65 | #H'; nrewrite > H'; /2/; |
---|
66 | ##| #t H; nwhd in H:(??%?); |
---|
67 | ncut (r = Vtrue); ##[ nwhd in H:(??(??%)?); ndestruct;//;##] |
---|
68 | #H'; nrewrite > H'; /2/; |
---|
69 | ##] |
---|
70 | ##| #H; nelim H; #v t H'; nelim H'; |
---|
71 | ##[ #i is s ne; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //; |
---|
72 | ##| ##2,4: // |
---|
73 | ##| #i t ne; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //; |
---|
74 | ##| #f s ne; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //; |
---|
75 | ##| #i s; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //; |
---|
76 | ##| #t; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //; |
---|
77 | ##| #s; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //; |
---|
78 | ##] |
---|
79 | ##] nqed. |
---|
80 | |
---|
81 | include "Plogic/russell_support.ma". |
---|
82 | |
---|
83 | (* Nicer - we still have to deal with all of the cases, but only need to |
---|
84 | introduce the result value, so there's a single case for getting rid of |
---|
85 | all the Error goals. *) |
---|
86 | |
---|
87 | ndefinition bool_of_val_2 : ∀v:val. ∀ty:type. { r : res bool | ∀r'. r = OK ? r' → bool_of_val v ty (of_bool r') } ≝ |
---|
88 | λv,ty. match v in val with |
---|
89 | [ Vint i ⇒ match ty with |
---|
90 | [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero)) |
---|
91 | | Tpointer _ ⇒ Some ? (OK ? (¬eq i zero)) |
---|
92 | | _ ⇒ Some ? (Error ?) |
---|
93 | ] |
---|
94 | | Vfloat f ⇒ match ty with |
---|
95 | [ Tfloat _ ⇒ Some ? (OK ? (¬Fcmp Ceq f Fzero)) |
---|
96 | | _ ⇒ Some ? (Error ?) |
---|
97 | ] |
---|
98 | | Vptr _ _ ⇒ match ty with |
---|
99 | [ Tint _ _ ⇒ Some ? (OK ? true) |
---|
100 | | Tpointer _ ⇒ Some ? (OK ? true) |
---|
101 | | _ ⇒ Some ? (Error ?) |
---|
102 | ] |
---|
103 | | _ ⇒ Some ? (Error ?) |
---|
104 | ]. nwhd; |
---|
105 | ##[ ##3,5: #r; nlapply (eq_spec c0 zero); nelim (eq c0 zero); |
---|
106 | ##[ ##1,3: #e H; nrewrite > (?:of_bool r=Vfalse); ##[ ##2,4: ndestruct; // ##] nrewrite > e; /3/; |
---|
107 | ##| ##2,4: #ne H; nrewrite > (?:of_bool r=Vtrue); ##[ ##2,4: ndestruct; // ##] /3/; |
---|
108 | ##] |
---|
109 | ##| ##13: #r; nelim (eq_dec c0 Fzero); |
---|
110 | ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); #H; nrewrite > (?:of_bool r=Vfalse); ##[ ##2: ndestruct; // ##] /2/; |
---|
111 | ##| #ne; nrewrite > (Feq_zero_false …); //; #H; |
---|
112 | nrewrite > (?:of_bool r=Vtrue); ##[ ##2: ndestruct; // ##] /3/; |
---|
113 | ##] |
---|
114 | ##| ##21,23: #r H; nrewrite > (?:of_bool r = Vtrue); ##[ ##2,4: ndestruct; // ##] /2/ |
---|
115 | ##| ##*: #a b; ndestruct; |
---|
116 | ##] nqed. |
---|
117 | |
---|
118 | (* Same as before, except we have to write eject in because the type for the |
---|
119 | equality is left implied, so the coercion isn't used. *) |
---|
120 | |
---|
121 | nlemma bool_of_val_2_complete : ∀v,ty,r. |
---|
122 | bool_of_val v ty r → |
---|
123 | ∃b. r = of_bool b ∧ eject ?? (bool_of_val_2 v ty) = OK ? b. |
---|
124 | #v ty r H; nelim H; #v t H'; nelim H'; |
---|
125 | ##[ #i is s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //; |
---|
126 | ##| #b i i0 s; @ true; @; // |
---|
127 | ##| #i t ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //; |
---|
128 | ##| #b i t0; @ true; @; // |
---|
129 | ##| #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //; |
---|
130 | ##| #i s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //; |
---|
131 | ##| #t; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_true …); //; |
---|
132 | ##| #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //; |
---|
133 | ##] |
---|
134 | nqed. |
---|
135 | |
---|
136 | |
---|
137 | (* Nicer again (after the extra definitions). Just use sigma type rather than |
---|
138 | the subset, but take into account the error monad. The error cases all |
---|
139 | become trivial and we don't have to muck around to get the result. *) |
---|
140 | |
---|
141 | ndefinition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝ |
---|
142 | λA,P,a.match a with [ None ⇒ False | Some y ⇒ match y return λ_.CProp[0] with [ Error ⇒ True | OK z ⇒ P z ]]. |
---|
143 | |
---|
144 | ndefinition err_inject : ∀A.∀P:A → Prop.∀a:option (res A).∀p:P_to_P_option_res A P a.res (sigma A P) ≝ |
---|
145 | λA.λP:A → Prop.λa:option (res A).λp:P_to_P_option_res A P a. |
---|
146 | (match a return λa'.a=a' → res (sigma A P) with |
---|
147 | [ None ⇒ λe1.? |
---|
148 | | Some b ⇒ λe1.(match b return λb'.b=b' → ? with |
---|
149 | [ Error ⇒ λ_. Error ? |
---|
150 | | OK c ⇒ λe2. OK ? (sig_intro A P c ?) |
---|
151 | ]) (refl ? b) |
---|
152 | ]) (refl ? a). |
---|
153 | ##[ nrewrite > e1 in p; nnormalize; *; |
---|
154 | ##| nrewrite > e1 in p; nrewrite > e2; nnormalize; // |
---|
155 | ##] nqed. |
---|
156 | |
---|
157 | ndefinition err_eject : ∀A.∀P: A → Prop. res (sigma A P) → res A ≝ |
---|
158 | λA,P,a.match a with [ Error ⇒ Error ? | OK b ⇒ |
---|
159 | match b with [ sig_intro w p ⇒ OK ? w] ]. |
---|
160 | |
---|
161 | ndefinition sig_eject : ∀A.∀P: A → Prop. sigma A P → A ≝ |
---|
162 | λA,P,a.match a with [ sig_intro w p ⇒ w]. |
---|
163 | |
---|
164 | ncoercion err_inject : |
---|
165 | ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_res ? P a.res (sigma A P) ≝ err_inject |
---|
166 | on a:option (res ?) to res (sigma ? ?). |
---|
167 | ncoercion err_eject : ∀A.∀P:A → Prop.∀c:res (sigma A P).res A ≝ err_eject |
---|
168 | on _c:res (sigma ? ?) to res ?. |
---|
169 | ncoercion sig_eject : ∀A.∀P:A → Prop.∀c:sigma A P.A ≝ sig_eject |
---|
170 | on _c:sigma ? ? to ?. |
---|
171 | |
---|
172 | ndefinition bool_of_val_3 : ∀v:val. ∀ty:type. res (Σr:bool. bool_of_val v ty (of_bool r)) ≝ |
---|
173 | λv,ty. match v in val with |
---|
174 | [ Vint i ⇒ match ty with |
---|
175 | [ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero)) |
---|
176 | | Tpointer _ ⇒ Some ? (OK ? (¬eq i zero)) |
---|
177 | | _ ⇒ Some ? (Error ?) |
---|
178 | ] |
---|
179 | | Vfloat f ⇒ match ty with |
---|
180 | [ Tfloat _ ⇒ Some ? (OK ? (¬Fcmp Ceq f Fzero)) |
---|
181 | | _ ⇒ Some ? (Error ?) |
---|
182 | ] |
---|
183 | | Vptr _ _ ⇒ match ty with |
---|
184 | [ Tint _ _ ⇒ Some ? (OK ? true) |
---|
185 | | Tpointer _ ⇒ Some ? (OK ? true) |
---|
186 | | _ ⇒ Some ? (Error ?) |
---|
187 | ] |
---|
188 | | _ ⇒ Some ? (Error ?) |
---|
189 | ]. nwhd; //; |
---|
190 | ##[ ##1,2: nlapply (eq_spec c0 zero); nelim (eq c0 zero); |
---|
191 | ##[ ##1,3: #e; nrewrite > e; napply bool_of_val_false; //; |
---|
192 | ##| ##2,4: #ne; napply bool_of_val_true; /2/; |
---|
193 | ##] |
---|
194 | ##| nelim (eq_dec c0 Fzero); |
---|
195 | ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); napply bool_of_val_false; //; |
---|
196 | ##| #ne; nrewrite > (Feq_zero_false …); //; napply bool_of_val_true; /2/; |
---|
197 | ##] |
---|
198 | ##| ##4,5: napply bool_of_val_true; // |
---|
199 | ##] nqed. |
---|
200 | |
---|
201 | ndefinition err_eq ≝ λA,P. λx:res (sigma A P). λy:A. |
---|
202 | match x with [ Error ⇒ False | OK x' ⇒ |
---|
203 | match x' with [ sig_intro x'' _ ⇒ x'' = y ]]. |
---|
204 | (* TODO: can I write a coercion for the above? *) |
---|
205 | |
---|
206 | (* Same as before, except we have to use a slightly different "equality". *) |
---|
207 | |
---|
208 | nlemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ err_eq ?? (bool_of_val_3 v ty) b. |
---|
209 | #v ty r H; nelim H; #v t H'; nelim H'; |
---|
210 | ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //; |
---|
211 | ##| #b i i0 s; @ true; @; // |
---|
212 | ##| #i t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //; |
---|
213 | ##| #b i t0; @ true; @; // |
---|
214 | ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //; |
---|
215 | ##| #i s; @ false; @; //; nwhd; nrewrite > (eq_true …); //; |
---|
216 | ##| #t; @ false; @; //; nwhd; nrewrite > (eq_true …); //; |
---|
217 | ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //; |
---|
218 | ##] |
---|
219 | nqed. |
---|
220 | |
---|
221 | (* Prove a few minor results to make proof obligations easy. *) |
---|
222 | |
---|
223 | nlemma bind_OK: ∀A,B,P,e,f. |
---|
224 | (∀v. e = OK A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) → |
---|
225 | match bind A B e f with [ Error ⇒ True | OK v ⇒ P v ]. |
---|
226 | #A B P e f; nelim e; /2/; nqed. |
---|
227 | |
---|
228 | nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigma A P → res B. |
---|
229 | (∀v:A. err_eq A P e v → ∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) → |
---|
230 | match bind (sigma A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ]. |
---|
231 | #A B P P' e f; nelim e; //; |
---|
232 | #v0; nelim v0; #v Hv IH; napply IH; //; nqed. |
---|
233 | |
---|
234 | nlemma bind2_OK: ∀A,B,C,P,e,f. |
---|
235 | (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P v' ]) → |
---|
236 | match bind2 A B C e f with [ Error ⇒ True | OK v ⇒ P v ]. |
---|
237 | #A B C P e f; nelim e; //; #v; ncases v; /2/; nqed. |
---|
238 | |
---|
239 | nlemma sig_bind2_OK: ∀A,B,C. ∀P:A×B → Prop. ∀P':C → Prop. ∀e:res (sigma (A×B) P). ∀f:A → B → res C. |
---|
240 | (∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P' v'] ) → |
---|
241 | match bind2 A B C e f with [ Error ⇒ True | OK v' ⇒ P' v' ]. |
---|
242 | #A B C P P' e f; nelim e; //; |
---|
243 | #v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed. |
---|
244 | |
---|
245 | nlemma reinject: ∀A. ∀P,P':A → Prop. ∀e:res (sigma A P'). |
---|
246 | (∀v:A. err_eq A P' e v → P' v → P v) → |
---|
247 | match err_eject A P' e with [ Error ⇒ True | OK v' ⇒ P v' ]. |
---|
248 | #A P P' e; ncases e; //; |
---|
249 | #v0; nelim v0; #v Pv' IH; /2/; |
---|
250 | nqed. |
---|
251 | |
---|
252 | nlemma bool_val_distinct: Vtrue ≠ Vfalse. |
---|
253 | @; #H; nwhd in H:(??%%); ndestruct; napply (absurd ? e0 one_not_zero); |
---|
254 | nqed. |
---|
255 | |
---|
256 | nlemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) → |
---|
257 | if b then is_true v ty else is_false v ty. |
---|
258 | #v ty b; ncases b; #H; ninversion H; #v' ty' H' ev et ev; //; |
---|
259 | napply False_ind; napply (absurd ? ev ?); |
---|
260 | ##[ ##2: napply sym_neq ##] napply bool_val_distinct; |
---|
261 | nqed. |
---|
262 | |
---|
263 | ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ]. |
---|
264 | nlemma opt_OK: ∀A,P,e. |
---|
265 | (∀v. e = Some ? v → P v) → |
---|
266 | match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ]. |
---|
267 | #A P e; nelim e; /2/; |
---|
268 | nqed. |
---|
269 | |
---|
270 | nlemma opt_bind_OK: ∀A,B,P,e,f. |
---|
271 | (∀v. e = Some A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) → |
---|
272 | match bind A B (opt_to_res A e) f with [ Error ⇒ True | OK v ⇒ P v ]. |
---|
273 | #A B P e f; nelim e; nnormalize; /2/; nqed. |
---|
274 | |
---|
275 | nlemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→res C. ∀R:C→Prop. |
---|
276 | (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v | Error ⇒ True]) → |
---|
277 | match match eject ?? e with [ mk_pair a b ⇒ Q a b ] with [ OK v ⇒ R v | Error ⇒ True ]. |
---|
278 | #A B C P e Q R; ncases e; #e'; ncases e'; nnormalize; |
---|
279 | ##[ #H; napply (False_ind … H); |
---|
280 | ##| #e''; ncases e''; #a b Pab H; nnormalize; /2/; |
---|
281 | ##] nqed. |
---|
282 | |
---|
283 | (* To make the evaluation of bare lvalue expressions invoke exec_lvalue with |
---|
284 | a structurally smaller value, we break out the surrounding Expr constructor |
---|
285 | and use exec_lvalue'. *) |
---|
286 | |
---|
287 | nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:val. eval_expr ge en m e r) ≝ |
---|
288 | match e with |
---|
289 | [ Expr e' ty ⇒ |
---|
290 | match e' with |
---|
291 | [ Econst_int i ⇒ Some ? (OK ? (Vint i)) |
---|
292 | | Evar _ ⇒ Some ? ( |
---|
293 | 〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;: |
---|
294 | opt_to_res ? (load_value_of_type ty m loc ofs)) |
---|
295 | | Eaddrof a ⇒ Some ? ( |
---|
296 | 〈loc, ofs〉 ← exec_lvalue ge en m a;: |
---|
297 | OK ? (Vptr loc ofs)) |
---|
298 | | Eunop op a ⇒ Some ? ( |
---|
299 | v1 ← exec_expr ge en m a;: |
---|
300 | opt_to_res ? (sem_unary_operation op v1 (typeof a))) |
---|
301 | | Econdition a1 a2 a3 ⇒ Some ? ( |
---|
302 | v ← exec_expr ge en m a1;: |
---|
303 | b ← bool_of_val_3 v (typeof a1);: |
---|
304 | match b return λ_.res val with [ true ⇒ (exec_expr ge en m a2) | false ⇒ (exec_expr ge en m a3) ]) |
---|
305 | (* if b then exec_expr ge en m a2 else exec_expr ge en m a3)*) |
---|
306 | | _ ⇒ Some ? (Error ?) |
---|
307 | ] |
---|
308 | ] |
---|
309 | and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:block × int. eval_lvalue ge en m (Expr e' ty) (\fst r) (\snd r)) ≝ |
---|
310 | match e' with |
---|
311 | [ Evar id ⇒ Some ? ( |
---|
312 | l ← opt_to_res ? (get ? PTree ? id en);: |
---|
313 | OK ? 〈l, zero〉) |
---|
314 | | _ ⇒ Some ? (Error ?) |
---|
315 | ] |
---|
316 | and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:block × int. eval_lvalue ge en m e (\fst r) (\snd r)) ≝ |
---|
317 | match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ]. |
---|
318 | nwhd; //; |
---|
319 | ##[ napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H; |
---|
320 | napply opt_OK; #v ev; /2/; |
---|
321 | ##| napply sig_bind2_OK; #loc ofs H; |
---|
322 | nwhd; napply eval_Eaddrof; //; |
---|
323 | ##| napply sig_bind_OK; #v1 ev1 Hv1; |
---|
324 | napply opt_OK; #v ev; |
---|
325 | napply (eval_Eunop … Hv1 ev); |
---|
326 | ##| napply sig_bind_OK; #vb evb Hvb; |
---|
327 | napply sig_bind_OK; #b; |
---|
328 | ncases b; #eb Hb; napply reinject; #v ev Hv; |
---|
329 | ##[ napply (eval_Econdition_true … Hvb ? Hv); napply (bool_of ??? Hb); |
---|
330 | ##| napply (eval_Econdition_false … Hvb ? Hv); napply (bool_of ??? Hb); |
---|
331 | ##] |
---|
332 | ##| napply opt_bind_OK; #l el; napply eval_Evar_local; // |
---|
333 | ##] nqed. |
---|
334 | |
---|
335 | (* Don't really want to use subset rather than sigma here, but can't be bothered |
---|
336 | with *another* set of coercions. XXX: why do I have to get the recursive |
---|
337 | call's property manually? *) |
---|
338 | |
---|
339 | nlet rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : { r:env × mem | alloc_variables en m l (\fst r) (\snd r) } ≝ |
---|
340 | match l with |
---|
341 | [ nil ⇒ Some ? 〈en, m〉 |
---|
342 | | cons h vars ⇒ |
---|
343 | match h with [ mk_pair id ty ⇒ |
---|
344 | match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒ |
---|
345 | match exec_alloc_variables (set ? PTree ? id b1 en) m1 vars with |
---|
346 | [ sig_intro r p ⇒ r ] |
---|
347 | ]]]. nwhd; //; |
---|
348 | nelim (exec_alloc_variables (set ident PTree block c3 c7 en) c6 c1); |
---|
349 | #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH; |
---|
350 | napply (alloc_variables_cons … IH); /2/; |
---|
351 | nqed. |
---|
352 | |
---|
353 | (* TODO: can we establish that length params = length vs in advance? *) |
---|
354 | nlet rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res (Σm2:mem. bind_parameters e m params vs m2) ≝ |
---|
355 | match params with |
---|
356 | [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m) | cons _ _ ⇒ Some ? (Error ?) ] |
---|
357 | | cons idty params' ⇒ match idty with [ mk_pair id ty ⇒ |
---|
358 | match vs with |
---|
359 | [ nil ⇒ Some ? (Error ?) |
---|
360 | | cons v1 vl ⇒ Some ? ( |
---|
361 | b ← opt_to_res ? (get ? PTree ? id e);: |
---|
362 | m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);: |
---|
363 | err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *) |
---|
364 | ] |
---|
365 | ] ]. |
---|
366 | nwhd; //; |
---|
367 | napply opt_bind_OK; #b eb; |
---|
368 | napply opt_bind_OK; #m1 em1; |
---|
369 | napply reinject; #m2 em2 Hm2; |
---|
370 | napply (bind_parameters_cons … eb em1 Hm2); |
---|
371 | nqed. |
---|
372 | |
---|
373 | ndefinition is_not_void : ∀t:type. res (Σu:unit. t ≠ Tvoid) ≝ |
---|
374 | λt. match t with |
---|
375 | [ Tvoid ⇒ Some ? (Error ?) |
---|
376 | | _ ⇒ Some ? (OK ??) |
---|
377 | ]. nwhd; //; @; #H; ndestruct; nqed. |
---|
378 | |
---|
379 | nlet rec exec_step (ge:genv) (st:state) on st : res (Σr:trace × state. step ge st (\fst r) (\snd r)) ≝ |
---|
380 | match st with |
---|
381 | [ State f s k e m ⇒ |
---|
382 | match s with |
---|
383 | [ Sassign a1 a2 ⇒ Some ? ( |
---|
384 | 〈loc, ofs〉 ← exec_lvalue ge e m a1;: |
---|
385 | v2 ← exec_expr ge e m a2;: |
---|
386 | m' ← opt_to_res ? (store_value_of_type (typeof a1) m loc ofs v2);: |
---|
387 | OK ? 〈E0, State f Sskip k e m'〉) |
---|
388 | | Sreturn a_opt ⇒ |
---|
389 | match a_opt with |
---|
390 | [ None ⇒ match fn_return f with |
---|
391 | [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉) |
---|
392 | | _ ⇒ Some ? (Error ?) |
---|
393 | ] |
---|
394 | | Some a ⇒ Some ? ( |
---|
395 | u ← is_not_void (fn_return f);: |
---|
396 | v ← exec_expr ge e m a;: |
---|
397 | OK ? 〈E0, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉) |
---|
398 | ] |
---|
399 | | _ ⇒ Some ? (Error ?) |
---|
400 | ] |
---|
401 | | Callstate f0 vargs k m ⇒ |
---|
402 | match f0 with |
---|
403 | [ Internal f ⇒ Some ? ( |
---|
404 | match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒ |
---|
405 | m2 ← exec_bind_parameters e m1 (fn_params f) vargs;: |
---|
406 | OK ? 〈E0, State f (fn_body f) k e m2〉 |
---|
407 | ]) |
---|
408 | | _ ⇒ Some ? (Error ?) |
---|
409 | ] |
---|
410 | | _ ⇒ Some ? (Error ?) |
---|
411 | ]. nwhd; //; |
---|
412 | ##[ napply sig_bind2_OK; #loc ofs Hlval; |
---|
413 | napply sig_bind_OK; #v2 ev2 Hv2; |
---|
414 | napply opt_bind_OK; #m' em'; |
---|
415 | nwhd; napply (step_assign … Hlval Hv2 em'); |
---|
416 | ##| napply step_return_0; napply c9; |
---|
417 | ##| napply sig_bind_OK; #u eu Hnotvoid; |
---|
418 | napply sig_bind_OK; #v ev Hv; |
---|
419 | nwhd; napply (step_return_1 … Hnotvoid Hv); |
---|
420 | ##| napply extract_subset_pair; #e m1 ealloc Halloc; |
---|
421 | napply sig_bind_OK; #m2 em1 Hbind; |
---|
422 | nwhd; napply (step_internal_function … Halloc Hbind); |
---|
423 | ##] |
---|
424 | nqed. |
---|
425 | |
---|
426 | nlet rec make_initial_state (p:program) : res (Σs:state. initial_state p s) ≝ |
---|
427 | let ge ≝ globalenv Genv ?? p in |
---|
428 | let m0 ≝ init_mem Genv ?? p in |
---|
429 | Some ? ( |
---|
430 | b ← opt_to_res ? (find_symbol Genv ? ge (prog_main ?? p));: |
---|
431 | f ← opt_to_res ? (find_funct_ptr Genv ? ge b);: |
---|
432 | OK ? (Callstate f (nil ?) Kstop m0)). |
---|
433 | nwhd; |
---|
434 | napply opt_bind_OK; #b eb; |
---|
435 | napply opt_bind_OK; #f ef; |
---|
436 | nwhd; napply (initial_state_intro … eb ef); |
---|
437 | nqed. |
---|