source: C-semantics/CexecIO.ma @ 20

Last change on this file since 20 was 20, checked in by campbell, 10 years ago

Add resumption monad based version of the executable semantics with simple I/O.

File size: 42.7 KB
Line 
1
2include "Csem.ma".
3
4include "extralib.ma".
5
6(* Some experimental definitions for an executable semantics. *)
7
8ndefinition 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
31nlemma 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
81include "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
87ndefinition 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
121nlemma 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  ##]
134nqed.
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
141ndefinition 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
144ndefinition 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
157ndefinition 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
161ndefinition sig_eject : ∀A.∀P: A → Prop. sigma A P → A ≝
162  λA,P,a.match a with [ sig_intro w p ⇒ w].
163
164ncoercion 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 ? ?).
167ncoercion err_eject : ∀A.∀P:A → Prop.∀c:res (sigma A P).res A ≝ err_eject
168  on _c:res (sigma ? ?) to res ?.
169ncoercion sig_eject : ∀A.∀P:A → Prop.∀c:sigma A P.A ≝ sig_eject
170  on _c:sigma ? ? to ?.
171
172ndefinition 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
201ndefinition 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
208nlemma 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  ##]
219nqed.
220
221(* Prove a few minor results to make proof obligations easy. *)
222
223nlemma bind_assoc_r: ∀A,B,C,e,f,g.
224  bind B C (bind A B e f) g = bind A C e (λx.bind B C (f x) g).
225#A B C e f g; ncases e; nnormalize; //; nqed.
226
227nlemma bind_OK: ∀A,B,P,e,f.
228  (∀v. e = OK A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
229  match bind A B e f with [ Error ⇒ True | OK v ⇒ P v ].
230#A B P e f; nelim e; /2/; nqed.
231
232nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigma A P → res B.
233  (∀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'] ) →
234  match bind (sigma A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
235#A B P P' e f; nelim e; //;
236#v0; nelim v0; #v Hv IH; napply IH; //; nqed.
237
238nlemma bind2_OK: ∀A,B,C,P,e,f.
239  (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P v' ]) →
240  match bind2 A B C e f with [ Error ⇒ True | OK v ⇒ P v ].
241#A B C P e f; nelim e; //; #v; ncases v; /2/; nqed.
242
243nlemma sig_bind2_OK: ∀A,B,C. ∀P:A×B → Prop. ∀P':C → Prop. ∀e:res (sigma (A×B) P). ∀f:A → B → res C.
244  (∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P' v'] ) →
245  match bind2 A B C e f with [ Error ⇒ True | OK v' ⇒ P' v' ].
246#A B C P P' e f; nelim e; //;
247#v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed.
248
249nlemma reinject: ∀A. ∀P,P':A → Prop. ∀e:res (sigma A P').
250  (∀v:A. err_eq A P' e v → P' v → P v) →
251  match err_eject A P' e with [ Error ⇒ True | OK v' ⇒ P v' ].
252#A P P' e; ncases e; //;
253#v0; nelim v0; #v Pv' IH; /2/;
254nqed.
255
256nlemma bool_val_distinct: Vtrue ≠ Vfalse.
257@; #H; nwhd in H:(??%%); ndestruct; napply (absurd ? e0 one_not_zero);
258nqed.
259
260nlemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) →
261  if b then is_true v ty else is_false v ty.
262#v ty b; ncases b; #H; ninversion H; #v' ty' H' ev et ev; //;
263napply False_ind; napply (absurd ? ev ?);
264##[ ##2: napply sym_neq ##] napply bool_val_distinct;
265nqed.
266
267ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ].
268nlemma opt_OK: ∀A,P,e.
269  (∀v. e = Some ? v → P v) →
270  match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ].
271#A P e; nelim e; /2/;
272nqed.
273
274nlemma opt_bind_OK: ∀A,B,P,e,f.
275  (∀v. e = Some A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) →
276  match bind A B (opt_to_res A e) f with [ Error ⇒ True | OK v ⇒ P v ].
277#A B P e f; nelim e; nnormalize; /2/; nqed.
278
279nlemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→res C. ∀R:C→Prop.
280  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v | Error ⇒ True]) →
281  match match eject ?? e with [ mk_pair a b ⇒ Q a b ] with [ OK v ⇒ R v | Error ⇒ True ].
282#A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;
283##[ #H; napply (False_ind … H);
284##| #e''; ncases e''; #a b Pab H; nnormalize; /2/;
285##] nqed.
286
287nlet rec is_neutral_cast (ty:type) : res (Σu:unit.neutral_for_cast ty) ≝
288match ty with
289[ Tint sz _ ⇒ match sz with [ I32 ⇒ Some ? (OK ? something) | _ ⇒ Some ? (Error ?) ]
290| Tpointer _ ⇒ Some ? (OK ? something)
291| Tarray _ _ ⇒ Some ? (OK ? something)
292| Tfunction _ _ ⇒ Some ? (OK ? something)
293| _ ⇒ Some ? (Error ?)
294]. nwhd; //; nqed.
295(*
296nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B | OK v ⇒ Error B ] = Error B.
297#A B e; ncases e; //; nqed.
298*)
299
300nlet rec exec_cast (v:val) (ty:type) (ty':type) : res (Σv':val. cast v ty ty' v') ≝
301match v with
302[ Vint i ⇒
303  match ty with
304  [ Tint sz1 si1 ⇒
305    match ty' with
306    [ Tint sz2 si2 ⇒ Some ? (OK ? (Vint (cast_int_int sz2 si2 i)))
307    | Tfloat sz2 ⇒ Some ? (OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i))))
308    (* no change in data repr *)
309    | _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i))
310    ]
311  | _ ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vint i))
312  ]
313| Vfloat f ⇒
314  match ty with
315  [ Tfloat sz ⇒
316    match ty' with
317    [ Tint sz' si' ⇒ Some ? (OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f))))
318    | Tfloat sz' ⇒ Some ? (OK ? (Vfloat (cast_float_float sz' f)))
319    | _ ⇒ Some ? (Error ?)
320    ]
321  | _ ⇒ Some ? (Error ?)
322  ]
323| Vptr b ofs ⇒ Some ? (u ← is_neutral_cast ty;: u' ← is_neutral_cast ty';: OK ? (Vptr b ofs))
324| _ ⇒ Some ? (Error ?)
325]. ndestruct; /2/;
326##[ ##1,2,3: ncases c2; //; napply cast_nn_i; //
327##| ##4,5,6: napply sig_bind_OK; #u;#_;#H; napply cast_nn_i; //;
328##| napply sig_bind_OK; #u;#_;#H; napply sig_bind_OK; #u';#_;#H';
329    napply cast_nn_p; //
330##] nqed.
331
332(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
333   a structurally smaller value, we break out the surrounding Expr constructor
334   and use exec_lvalue'. *)
335
336nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:val. eval_expr ge en m e r) ≝
337match e with
338[ Expr e' ty ⇒
339  match e' with
340  [ Econst_int i ⇒ Some ? (OK ? (Vint i))
341  | Econst_float f ⇒ Some ? (OK ? (Vfloat f))
342  | Evar _ ⇒ Some ? (
343      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
344      opt_to_res ? (load_value_of_type ty m loc ofs))
345  | Ederef _ ⇒ Some ? (
346      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
347      opt_to_res ? (load_value_of_type ty m loc ofs))
348  | Efield _ _ ⇒ Some ? (
349      〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;:
350      opt_to_res ? (load_value_of_type ty m loc ofs))
351  | Eaddrof a ⇒ Some ? (
352      〈loc, ofs〉 ← exec_lvalue ge en m a;:
353      OK ? (Vptr loc ofs))
354  | Esizeof ty' ⇒ Some ? (OK ? (Vint (repr (sizeof ty'))))
355  | Eunop op a ⇒ Some ? (
356      v1 ← exec_expr ge en m a;:
357      opt_to_res ? (sem_unary_operation op v1 (typeof a)))
358  | Ebinop op a1 a2 ⇒ Some ? (
359      v1 ← exec_expr ge en m a1;:
360      v2 ← exec_expr ge en m a2;:
361      opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m))
362  | Econdition a1 a2 a3 ⇒ Some ? (
363      v ← exec_expr ge en m a1;:
364      b ← bool_of_val_3 v (typeof a1);:
365      match b return λ_.res val with [ true ⇒ (exec_expr ge en m a2) | false ⇒ (exec_expr ge en m a3) ])
366(*      if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
367  | Eorbool a1 a2 ⇒ Some ? (
368      v1 ← exec_expr ge en m a1;:
369      b1 ← bool_of_val_3 v1 (typeof a1);:
370      match b1 return λ_.res val with [ true ⇒ OK ? Vtrue | false ⇒
371        v2 ← exec_expr ge en m a2;:
372        b2 ← bool_of_val_3 v2 (typeof a2);:
373        OK ? (of_bool b2) ])
374  | Eandbool a1 a2 ⇒ Some ? (
375      v1 ← exec_expr ge en m a1;:
376      b1 ← bool_of_val_3 v1 (typeof a1);:
377      match b1 return λ_.res val with [ true ⇒
378        v2 ← exec_expr ge en m a2;:
379        b2 ← bool_of_val_3 v2 (typeof a2);:
380        OK ? (of_bool b2)
381      | false ⇒ OK ? Vfalse ])
382  | Ecast ty' a ⇒ Some ? (
383      v ← exec_expr ge en m a;:
384      exec_cast v (typeof a) ty')
385  ]
386]
387and 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)) ≝
388  match e' with
389  [ Evar id ⇒
390      match (get … id en) with
391      [ None ⇒ Some ? (l ← opt_to_res ? (find_symbol ? ? ge id);: OK ? 〈l,zero〉) (* global *)
392      | Some l ⇒ Some ? (OK ? 〈l,zero〉) (* local *)
393      ]
394  | Ederef a ⇒ Some ? (
395      v ← exec_expr ge en m a;:
396      match v with
397      [ Vptr l ofs ⇒ OK ? 〈l,ofs〉
398      | _ ⇒ Error ?
399      ])
400  | Efield a i ⇒
401      match (typeof a) with
402      [ Tstruct id fList ⇒ Some ? (
403          〈l,ofs〉 ← exec_lvalue ge en m a;:
404          delta ← field_offset i fList;:
405          OK ? 〈l,add ofs (repr delta)〉)
406      | Tunion id fList ⇒ Some ? (
407          〈l,ofs〉 ← exec_lvalue ge en m a;:
408          OK ? 〈l,ofs〉)
409      | _ ⇒ Some ? (Error ?)
410      ]
411  | _ ⇒ Some ? (Error ?)
412  ]
413and 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)) ≝
414match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
415nwhd; //;
416##[ napply sig_bind2_OK; nrewrite > c4; #loc ofs H;
417    napply opt_OK;  #v ev; /2/;
418##| napply sig_bind2_OK; nrewrite > c4; #loc ofs H;
419    napply opt_OK;  #v ev; /2/;
420##| napply sig_bind2_OK; #loc ofs H;
421    nwhd; napply eval_Eaddrof; //;
422##| napply sig_bind_OK; #v1 ev1 Hv1;
423    napply opt_OK; #v ev;
424    napply (eval_Eunop … Hv1 ev);
425##| napply sig_bind_OK; #v1 ev1 Hv1;
426    napply sig_bind_OK; #v2 ev2 Hv2;
427    napply opt_OK; #v ev;
428    napply (eval_Ebinop … Hv1 Hv2 ev);
429##| napply sig_bind_OK; #v ev Hv;
430    napply sig_bind_OK; #v' ev' Hv';
431    napply (eval_Ecast … Hv Hv');
432##| napply sig_bind_OK; #vb evb Hvb;
433    napply sig_bind_OK; #b;
434    ncases b; #eb Hb; napply reinject; #v ev Hv;
435    ##[ napply (eval_Econdition_true … Hvb ? Hv);  napply (bool_of ??? Hb);
436    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
437    ##]
438##| napply sig_bind_OK; #v1 ev1 Hv1;
439    napply sig_bind_OK; #b1; ncases b1; #eb1 Hb1;
440    ##[ napply sig_bind_OK; #v2 ev2 Hv2;
441        napply sig_bind_OK; #b2 eb2 Hb2;
442        napply (eval_Eandbool_2 … Hv1 … Hv2);
443        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
444    ##| napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1);
445    ##]
446##| napply sig_bind_OK; #v1 ev1 Hv1;
447    napply sig_bind_OK; #b1; ncases b1; #eb1 Hb1;
448    ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1);
449    ##| napply sig_bind_OK; #v2 ev2 Hv2;
450        napply sig_bind_OK; #b2 eb2 Hb2;
451        napply (eval_Eorbool_2 … Hv1 … Hv2);
452        ##[ napply (bool_of … Hb1); ##| napply Hb2; ##]
453    ##]
454##| napply sig_bind2_OK; nrewrite > c5; #l ofs H;
455    napply opt_OK; #v ev; /2/;
456##| napply opt_bind_OK; #l el; napply eval_Evar_global; /2/;
457##| napply eval_Evar_local; /2/
458##| napply sig_bind_OK; #v; ncases v; //; #l ofs ev Hv; nwhd;
459    napply eval_Ederef; //
460##| napply sig_bind2_OK; #l ofs H;
461    napply bind_OK; #delta Hdelta;
462    napply (eval_Efield_struct … H c5 Hdelta);
463##| napply sig_bind2_OK; #l ofs H;
464    napply (eval_Efield_union … H c5);
465##] nqed.
466
467(* TODO: Can we do this sensibly with a map combinator? *)
468nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (Σvl:list val. eval_exprlist ge e m l vl) ≝
469match l with
470[ nil ⇒ Some ? (OK ? (nil val))
471| cons e1 es ⇒ Some ? (
472  v ← exec_expr ge e m e1;:
473  vs ← exec_exprlist ge e m es;:
474  OK ? (cons val v vs))
475]. nwhd; //;
476napply sig_bind_OK; #v ev Hv;
477napply sig_bind_OK; #vs evs Hvs;
478nnormalize; /2/;
479nqed.
480
481(* Don't really want to use subset rather than sigma here, but can't be bothered
482   with *another* set of coercions. XXX: why do I have to get the recursive
483   call's property manually? *)
484
485nlet 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) } ≝
486match l with
487[ nil ⇒ Some ? 〈en, m〉
488| cons h vars ⇒
489  match h with [ mk_pair id ty ⇒
490    match alloc m 0 (sizeof ty) with [ mk_pair m1 b1 ⇒
491      match exec_alloc_variables (set … id b1 en) m1 vars with
492      [ sig_intro r p ⇒ r ]
493]]]. nwhd; //;
494nelim (exec_alloc_variables (set ident ? block c3 c7 en) c6 c1);
495#H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
496napply (alloc_variables_cons … IH); /2/;
497nqed.
498
499(* TODO: can we establish that length params = length vs in advance? *)
500nlet 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) ≝
501  match params with
502  [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m) | cons _ _ ⇒ Some ? (Error ?) ]
503  | cons idty params' ⇒ match idty with [ mk_pair id ty ⇒
504      match vs with
505      [ nil ⇒ Some ? (Error ?)
506      | cons v1 vl ⇒ Some ? (
507          b ← opt_to_res ? (get … id e);:
508          m1 ← opt_to_res ? (store_value_of_type ty m b zero v1);:
509          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
510      ]
511  ] ].
512nwhd; //;
513napply opt_bind_OK; #b eb;
514napply opt_bind_OK; #m1 em1;
515napply reinject; #m2 em2 Hm2;
516napply (bind_parameters_cons … eb em1 Hm2);
517nqed.
518
519ndefinition is_not_void : ∀t:type. res (Σu:unit. t ≠ Tvoid) ≝
520λt. match t with
521[ Tvoid ⇒ Some ? (Error ?)
522| _ ⇒ Some ? (OK ??)
523]. nwhd; //; @; #H; ndestruct; nqed.
524
525ninductive decide : Type ≝
526| dy : decide | dn : decide.
527
528ndefinition dodecide : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P.
529#P d;ncases d;/2/; nqed.
530
531ncoercion decide_inject :
532  ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P ≝ dodecide
533  on d:decide to ? + (¬?).
534
535ndefinition dodecide2 : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P.
536#P d; ncases d; nnormalize; #p; ##[ napply (OK ? p); ##| napply Error ##] nqed.
537
538ncoercion decide_inject2 :
539  ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P ≝ dodecide2
540  on d:decide to res ?.
541
542alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)".
543alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)".
544ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
545#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
546ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
547#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
548ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
549#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
550
551nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝
552match t1 with
553[ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy | _ ⇒ dn ]
554| Tint sz sg ⇒ match t2 with [ Tint sz' sg' ⇒ match sz_eq_dec sz sz' with [ inl _ ⇒ match sg_eq_dec sg sg' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
555| Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
556| Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
557| Tarray t n ⇒ match t2 with [ Tarray t' n' ⇒
558    match assert_type_eq t t' with [ OK _ ⇒
559      match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
560| Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒
561    match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
562| Tstruct i fl ⇒
563    match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
564      match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
565| Tunion i fl ⇒
566    match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
567      match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] |  _ ⇒ dn ]
568| Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
569]
570and assert_typelist_eq (tl1,tl2:typelist) : res (tl1 = tl2) ≝
571match tl1 with
572[ Tnil ⇒ match tl2 with [ Tnil ⇒ dy | _ ⇒ dn ]
573| Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn | Tcons t2 ts2 ⇒
574    match assert_type_eq t1 t2 with [ OK _ ⇒
575      match assert_typelist_eq ts1 ts2 with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ]
576]
577and assert_fieldlist_eq (fl1,fl2:fieldlist) : res (fl1 = fl2) ≝
578match fl1 with
579[ Fnil ⇒ match fl2 with [ Fnil ⇒ dy | _ ⇒ dn ]
580| Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn | Fcons i2 t2 fs2 ⇒
581    match ident_eq i1 i2 with [ inl _ ⇒
582      match assert_type_eq t1 t2 with [ OK _ ⇒
583        match assert_fieldlist_eq fs1 fs2 with [ OK _ ⇒ dy | _ ⇒ dn ]
584        | _ ⇒ dn ] | _ ⇒ dn ] ]
585].
586(* A poor man's clear, otherwise automation picks up recursive calls without
587   checking that the argument is smaller. *)
588ngeneralize in assert_type_eq;
589ngeneralize in assert_typelist_eq;
590ngeneralize in assert_fieldlist_eq; #avoid1; #_; #avoid2; #_; #avoid3; #_; nwhd; //;
591(* XXX: I have no idea why the first // didn't catch these. *)
592//; //; //; //; //; //; //; //; //;
593nqed.
594
595nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
596match k with
597[ Kstop ⇒ dy
598| Kcall _ _ _ _ ⇒ dy
599| _ ⇒ dn
600]. nwhd; //; @; #H; nelim H; nqed.
601
602nlet rec is_Sskip (s:statement) : (s = Sskip) + (s ≠ Sskip) ≝
603match s with
604[ Sskip ⇒ dy
605| _ ⇒ dn
606].
607##[ //;
608##| ##*: @; #H; ndestruct;
609##] nqed.
610
611(* IO monad *)
612
613ninductive IO (T:Type) : Type ≝
614| Interact : ident → list eventval → (eventval → IO T) → IO T
615| Value : T → IO T
616| Wrong : IO T.
617
618nlet rec bindIO (T,T':Type) (v:IO T) (f:T → IO T') on v : IO T' ≝
619match v with
620[ Interact fn args k ⇒ (Interact ? fn args (λres. bindIO T T' (k res) f))
621| Value v' ⇒ (f v')
622| Wrong ⇒ Wrong T'
623].
624
625nlet rec bindIO2 (T1,T2,T':Type) (v:IO (T1×T2)) (f:T1 → T2 → IO T') on v : IO T' ≝
626match v with
627[ Interact fn args k ⇒ (Interact ? fn args (λres. bindIO2 T1 T2 T' (k res) f))
628| Value v' ⇒ match v' with [ mk_pair v1 v2 ⇒ f v1 v2 ]
629| Wrong ⇒ Wrong T'
630].
631
632ndefinition do_io : ident → list eventval → IO eventval ≝
633λfn,args. Interact eventval fn args (λres. Value eventval res).
634
635ndefinition ret: ∀T. T → (IO T) ≝
636λT,x.(Value T x).
637
638ndefinition err_to_io : ∀T. res T → IO T ≝
639λT,v. match v with [ OK v' ⇒ Value T v' | Error ⇒ Wrong T ].
640(*ncoercion err_to_io : ∀A.∀c:res A.IO A ≝ err_to_io on _c:res ? to IO ?.*)
641ndefinition err_to_io_sig : ∀T.∀P:T → Prop. res (sigma T P) → IO (sigma T P) ≝
642λT,P,v. match v with [ OK v' ⇒ Value (sigma T P) v' | Error ⇒ Wrong (sigma T P) ].
643ncoercion err_to_io_sig : ∀A.∀P:A → Prop.∀c:res (sigma A P).IO (sigma A P) ≝ err_to_io_sig on _c:res ? to IO ?.
644
645
646(* If the original definitions are vague enough, do I need to do this? *)
647notation "! ident v ← e;: e'" right associative with precedence 40 for @{'bindIO ${e} (λ${ident v}.${e'})}.
648notation "! 〈ident v1, ident v2〉 ← e;: e'" right associative with precedence 40 for @{'bindIO2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
649interpretation "IO monad bind" 'bindIO e f = (bindIO ? ? e f).
650interpretation "IO monad pair bind" 'bindIO2 e f = (bindIO2 ??? e f).
651(**)
652nlet rec P_io (A:Type) (P:A → CProp[0]) (v:IO A) on v : CProp[0] ≝
653match v return λ_.CProp[0] with
654[ Wrong ⇒ True
655| Value z ⇒ P z
656| Interact fn args k ⇒ ∀v'.P_io A P (k v')
657].
658
659ndefinition P_to_P_option_io : ∀A:Type[0].∀P:A → CProp[0].option (IO A) → CProp[0] ≝
660  λA,P,a.match a with
661   [ None ⇒ False
662   | Some y ⇒ P_io A P y
663   ].
664
665nlet rec io_inject_0 (A:Type) (P:A → Prop) (a:IO A) (p:P_io A P a) on a : IO (sigma A P) ≝
666(match a return λa'.a=a' → ? with
667 [ Wrong ⇒ λ_. Wrong ?
668 | Value c ⇒ λe2. Value ? (sig_intro A P c ?)
669 | Interact fn args k ⇒ λe2. Interact ? fn args (λv. io_inject_0 A P (k v) ?)
670 ]) (refl ? a).
671 (* XXX: odd, can't do both cases at once. *)
672##[ nrewrite > e2 in p; nwhd in ⊢ (% → ?); //;
673##| nrewrite > e2 in p; nwhd in ⊢ (% → ?); //;
674##] nqed.
675
676ndefinition io_inject : ∀A.∀P:A → Prop.∀a:option (IO A).∀p:P_to_P_option_io A P a.IO (sigma A P) ≝
677  λA.λP:A → Prop.λa:option (IO A).λp:P_to_P_option_io A P a.
678  (match a return λa'.a=a' → IO (sigma A P) with
679   [ None ⇒ λe1.?
680   | Some b ⇒ λe1. io_inject_0 A P b ?
681   ]) (refl ? a).
682##[ nrewrite > e1 in p; nnormalize; *;
683##| nrewrite > e1 in p; nnormalize; //
684##] nqed.
685
686nlet rec io_eject (A:Type) (P: A → Prop) (a:IO (sigma A P)) on a : IO A ≝
687match a with
688[ Wrong ⇒ Wrong ?
689| Value b ⇒ match b with [ sig_intro w p ⇒ Value ? w]
690| Interact fn args k ⇒ Interact ? fn args (λv. io_eject A P (k v))
691].
692
693ncoercion io_inject :
694  ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_io ? P a.IO (sigma A P) ≝ io_inject
695  on a:option (IO ?) to IO (sigma ? ?).
696ncoercion io_eject : ∀A.∀P:A → Prop.∀c:IO (sigma A P).IO A ≝ io_eject
697  on _c:IO (sigma ? ?) to IO ?.
698
699ndefinition opt_to_io : ∀T.option T → IO T ≝
700λT,v. match v with [ None ⇒ Wrong T | Some v' ⇒ Value T v' ].
701ncoercion opt_to_io : ∀T.∀v:option T. IO T ≝ opt_to_io on _v:option ? to IO ?.
702
703nlemma sig_bindIO_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:IO (sigma A P). ∀f:sigma A P → IO B.
704  (∀v:A. ∀p:P v. P_io ? P' (f (sig_intro A P v p))) →
705  P_io ? P' (bindIO (sigma A P) B e f).
706#A B P P' e f; nelim e;
707##[ #fn args k IH; #IH'; nwhd; #res; napply IH; //;
708##| #v0; nelim v0; #v Hv IH; nwhd; napply IH;
709##| //;
710##] nqed.
711
712nlemma sig_bindIO2_OK: ∀A,B,C. ∀P:(A×B) → Prop. ∀P':C → Prop. ∀e:IO (sigma (A×B) P). ∀f: A → B → IO C.
713  (∀vA:A.∀vB:B. ∀p:P 〈vA,vB〉. P_io ? P' (f vA vB)) →
714  P_io ? P' (bindIO2 A B C e f).
715#A B C P P' e f; nelim e;
716##[ #fn args k IH; #IH'; nwhd; #res; napply IH; napply IH';
717##| #v0; nelim v0; #v; nelim v; #vA vB Hv IH; napply IH; //;
718##| //;
719##] nqed.
720
721nlemma opt_bindIO_OK: ∀A,B. ∀P:B → Prop. ∀e:option A. ∀f: A → IO B.
722  (∀v:A. e = Some A v → P_io ? P (f v)) →
723  P_io ? P (bindIO A B e f).
724#A B P e; nelim e; //; #v f H; napply H; //;
725nqed.
726
727nlemma bindIO_OK: ∀A,B. ∀P:B → Prop. ∀e:IO A. ∀f: A → IO B.
728  (∀v:A. P_io ? P (f v)) →
729  P_io ? P (bindIO A B e f).
730#A B P e; nelim e;
731##[ #fn args k IH; #f H; nwhd; #res; napply IH; //;
732##| #v f H; napply H;
733##| //;
734##] nqed.
735(*
736nlemma bind_assoc_r: ∀A,B,C,e,f,g.
737  bindIO B C (bindIO A B e f) g = bindIO A C e (λx.bindIO B C (f x) g).
738#A B C e f g; nelim e;
739##[ #fn args k IH; nwhd in ⊢ (???%);
740nnormalize;
741*)
742
743nlemma extract_subset_pair_io: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→IO C. ∀R:C→Prop.
744  (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → P_io ? R (Q a b)) →
745  P_io ? R (match eject ?? e with [ mk_pair a b ⇒ Q a b ]).
746#A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;
747##[ *;
748##| #e''; ncases e''; #a b Pab H; nnormalize; /2/;
749##] nqed.
750
751ndefinition check_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝
752λev,ty.
753match ty with
754[ Tint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i)) | _ ⇒ Some ? (Error ?) ]
755| Tfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f)) | _ ⇒ Some ? (Error ?) ]
756| _ ⇒ Some ? (Error ?)
757]. nwhd; //; nqed.
758
759ndefinition check_eventval' : ∀v:val. ∀ty:typ. res (Σev:eventval. eventval_match ev ty v) ≝
760λv,ty.
761match ty with
762[ Tint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i)) | _ ⇒ Some ? (Error ?) ]
763| Tfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f)) | _ ⇒ Some ? (Error ?) ]
764| _ ⇒ Some ? (Error ?)
765]. nwhd; //; nqed.
766
767nlet rec check_eventval_list (vs: list val) (tys: list typ) : res (Σevs:list eventval. eventval_list_match evs tys vs) ≝
768match vs with
769[ nil ⇒ match tys with [ nil ⇒ Some ? (OK ? (nil ?)) | _ ⇒ Some ? (Error ?) ]
770| cons v vt ⇒
771  match tys with
772  [ nil ⇒ Some ? (Error ?)
773  | cons ty tyt ⇒ Some ? (
774    ev ← check_eventval' v ty;:
775    evt ← check_eventval_list vt tyt;:
776    OK ? ((sig_eject ?? ev)::evt))
777  ]
778]. nwhd; //;
779napply sig_bind_OK; #ev eev Hev;
780napply sig_bind_OK; #evt eevt Hevt;
781nnormalize; /2/;
782nqed.
783
784(* execution *)
785
786nlet rec exec_step (ge:genv) (st:state) on st : (IO (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝
787match st with
788[ State f s k e m ⇒
789  match s with
790  [ Sassign a1 a2 ⇒ Some ? (
791    ! 〈loc, ofs〉 ← exec_lvalue ge e m a1;:
792    ! v2 ← exec_expr ge e m a2;:
793    ! m' ← store_value_of_type (typeof a1) m loc ofs v2;:
794    ret ? 〈E0, State f Sskip k e m'〉)
795  | Scall lhs a al ⇒ Some ? (
796    ! vf ← exec_expr ge e m a;:
797    ! vargs ← exec_exprlist ge e m al;:
798    ! fd ← find_funct ? ? ge vf;:
799    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (typeof a));:
800(*
801    ! k' ← match lhs with
802         [ None ⇒ ret ? (Kcall (None ?) f e k)
803         | Some lhs' ⇒
804           ! locofs ← exec_lvalue ge e m lhs';:
805           ret ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k)
806         ];:
807    ret ? 〈E0, Callstate fd vargs k' m〉)
808*)
809    match lhs with
810         [ None ⇒ ret ? 〈E0, Callstate fd vargs (Kcall (None ?) f e k) m〉
811         | Some lhs' ⇒
812           ! locofs ← exec_lvalue ge e m lhs';:
813           ret ? 〈E0, Callstate fd vargs (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k) m〉
814         ])
815  | Ssequence s1 s2 ⇒ Some ? (ret ? 〈E0, State f s1 (Kseq s2 k) e m〉)
816  | Sskip ⇒
817      match k with
818      [ Kseq s k' ⇒ Some ? (ret ? 〈E0, State  f s k' e m〉)
819      | Kstop ⇒
820          match fn_return f with
821          [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
822          | _ ⇒ Some ? (Wrong ?)
823          ]
824      | Kcall _ _ _ _ ⇒
825          match fn_return f with
826          [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
827          | _ ⇒ Some ? (Wrong ?)
828          ]
829      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
830      | Kdowhile a s' k' ⇒ Some ? (
831          ! v ← exec_expr ge e m a;:
832          ! b ← bool_of_val_3 v (typeof a);:
833          match b with
834          [ true ⇒ ret ? 〈E0, State f (Sdowhile a s') k' e m〉
835          | false ⇒ ret ? 〈E0, State f Sskip k' e m〉
836          ])
837      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
838      | Kfor3 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉)
839      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
840      | _ ⇒ Some ? (Wrong ?)
841      ]
842  | Scontinue ⇒
843      match k with
844      [ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
845      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
846      | Kdowhile a s' k' ⇒ Some ? (
847          ! v ← exec_expr ge e m a;:
848          ! b ← bool_of_val_3 v (typeof a);:
849          match b with
850          [ true ⇒ ret ? 〈E0, State f (Sdowhile a s') k' e m〉
851          | false ⇒ ret ? 〈E0, State f Sskip k' e m〉
852          ])
853      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
854      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
855      | _ ⇒ Some ? (Wrong ?)
856      ]
857  | Sbreak ⇒
858      match k with
859      [ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Sbreak k' e m〉)
860      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
861      | Kdowhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
862      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
863      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
864      | _ ⇒ Some ? (Wrong ?)
865      ]
866  | Sifthenelse a s1 s2 ⇒ Some ? (
867      ! v ← exec_expr ge e m a;:
868      ! b ← bool_of_val_3 v (typeof a);:
869      ret ? 〈E0, State f (if b then s1 else s2) k e m〉)
870  | Swhile a s' ⇒ Some ? (
871      ! v ← exec_expr ge e m a;:
872      ! b ← bool_of_val_3 v (typeof a);:
873      ret ? 〈E0, if b then State f s' (Kwhile a s' k) e m
874                     else State f Sskip k e m〉)
875  | Sdowhile a s' ⇒ Some ? (ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉)
876  | Sfor a1 a2 a3 s' ⇒
877      match is_Sskip a1 with
878      [ inl _ ⇒ Some ? (
879          ! v ← exec_expr ge e m a2;:
880          ! b ← bool_of_val_3 v (typeof a2);:
881          ret ? 〈E0, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉)
882      | inr _ ⇒ Some ? (ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉)
883      ]
884  | Sreturn a_opt ⇒
885    match a_opt with
886    [ None ⇒ match fn_return f with
887      [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉)
888      | _ ⇒ Some ? (Wrong ?)
889      ]
890    | Some a ⇒ Some ? (
891        ! u ← is_not_void (fn_return f);:
892        ! v ← exec_expr ge e m a;:
893        ret ? 〈E0, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
894    ]
895  | Sswitch a sl ⇒ Some ? (
896      ! v ← exec_expr ge e m a;:
897      match v with [ Vint n ⇒ ret ? 〈E0, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
898                   | _ ⇒ Wrong ? ])
899  | Slabel lbl s' ⇒ Some ? (ret ? 〈E0, State f s' k e m〉)
900  | Sgoto lbl ⇒
901      match find_label lbl (fn_body f) (call_cont k) with
902      [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ Some ? (ret ? 〈E0, State f s' k' e m〉) ]
903      | None ⇒ Some ? (Wrong ?)
904      ]
905  ]
906| Callstate f0 vargs k m ⇒
907  match f0 with
908  [ Internal f ⇒ Some ? (
909    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒
910      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;:
911      ret ? 〈E0, State f (fn_body f) k e m2〉
912    ])
913  | External f argtys retty ⇒ Some ? (
914      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);:
915      ! evres ← do_io f evargs;:
916      ! vres ← check_eventval evres (proj_sig_res (signature_of_type argtys retty));:
917      ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉)
918  ]
919| Returnstate res k m ⇒
920  match k with
921  [ Kcall r f e k' ⇒
922    match r with
923    [ None ⇒
924      match res with
925      [ Vundef ⇒ Some ? (ret ? 〈E0, (State f Sskip k' e m)〉)
926      | _ ⇒ Some ? (Wrong ?)
927      ]
928    | Some r' ⇒
929      match r' with [ mk_pair locofs ty ⇒
930        match locofs with [ mk_pair loc ofs ⇒ Some ? (
931          ! m' ← store_value_of_type ty m loc ofs res;:
932          ret ? 〈E0, (State f Sskip k' e m')〉)
933        ]
934      ]
935    ]
936  | _ ⇒ Some ? (Wrong ?)
937  ]
938]. nwhd; //;
939##[ nrewrite > c7; napply step_skip_call; //; napply c8;
940##| napply step_skip_or_continue_while; @; //;
941##| napply sig_bindIO_OK; #v Hv;
942    napply sig_bindIO_OK; #b; ncases b; #Hb;
943    ##[ napply (step_skip_or_continue_dowhile_true … Hv);
944      ##[ @; // ##| napply (bool_of … Hb); ##]
945    ##| napply (step_skip_or_continue_dowhile_false … Hv);
946      ##[ @; // ##| napply (bool_of … Hb); ##]
947    ##]
948##| napply step_skip_or_continue_for2; @; //;
949##| napply step_skip_break_switch; @; //;
950##| nrewrite > c11; napply step_skip_call; //; napply c12;
951##| napply sig_bindIO2_OK; #loc ofs Hlval;
952    napply sig_bindIO_OK; #v2 Hv2;
953    napply opt_bindIO_OK; #m' em';
954    nwhd; napply (step_assign … Hlval Hv2 em');
955##| napply sig_bindIO_OK; #vf Hvf;
956    napply sig_bindIO_OK; #vargs Hvargs;
957    napply opt_bindIO_OK; #fd efd;
958    napply bindIO_OK; #ety;
959    ncases c6; nwhd;
960    ##[ napply (step_call_none … Hvf Hvargs efd ety);
961    ##| #lhs';
962        napply sig_bindIO_OK; #locofs; ncases locofs; #loc ofs Hlocofs;
963        nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
964    ##]
965##| napply sig_bindIO_OK; #v Hv;
966    napply sig_bindIO_OK; #b; ncases b; #Hb;
967    ##[ napply (step_ifthenelse_true … Hv); napply (bool_of … Hb);
968    ##| napply (step_ifthenelse_false … Hv); napply (bool_of … Hb)
969    ##]
970##| napply sig_bindIO_OK; #v Hv;
971    napply sig_bindIO_OK; #b; ncases b; #Hb;
972    ##[ napply (step_while_true … Hv); napply (bool_of … Hb);
973    ##| napply (step_while_false … Hv); napply (bool_of … Hb);
974    ##]
975##| nrewrite > c11;
976    napply sig_bindIO_OK; #v Hv;
977    napply sig_bindIO_OK; #b; ncases b; #Hb;
978    ##[ napply (step_for_true … Hv); napply (bool_of … Hb);
979    ##| napply (step_for_false … Hv); napply (bool_of … Hb);
980    ##]
981##| napply step_for_start; //;
982##| napply step_skip_break_switch; @2; //;
983##| napply step_skip_or_continue_while; @2; //;
984##| napply sig_bindIO_OK; #v Hv;
985    napply sig_bindIO_OK; #b; ncases b; #Hb;
986    ##[ napply (step_skip_or_continue_dowhile_true … Hv);
987      ##[ @2; // ##| napply (bool_of … Hb); ##]
988    ##| napply (step_skip_or_continue_dowhile_false … Hv);
989      ##[ @2; // ##| napply (bool_of … Hb); ##]
990    ##]
991##| napply step_skip_or_continue_for2; @2; //
992##| napply step_return_0; napply c9;
993##| napply sig_bindIO_OK; #u Hnotvoid;
994    napply sig_bindIO_OK; #v Hv;
995    nwhd; napply (step_return_1 … Hnotvoid Hv);
996##| napply sig_bindIO_OK; #v; ncases v; //; #n Hv;
997    napply step_switch; //;
998##| napply step_goto; nrewrite < c12; napply c9;
999##| napply extract_subset_pair_io; #e m1 ealloc Halloc;
1000    napply sig_bindIO_OK; #m2 Hbind;
1001    nwhd; napply (step_internal_function … Halloc Hbind);
1002##| napply sig_bindIO_OK; #evs Hevs;
1003    napply bindIO_OK; #eres;
1004    napply sig_bindIO_OK; #res Hres;
1005    nwhd; napply step_external_function; @; ##[ napply Hevs; ##| napply Hres; ##] 
1006##| napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; //;
1007##]
1008nqed.
1009
1010nlet rec make_initial_state (p:program) : IO (Σs:state. initial_state p s) ≝
1011  let ge ≝ globalenv Genv ?? p in
1012  let m0 ≝ init_mem Genv ?? p in
1013  Some ? (
1014    ! b ← find_symbol ? ? ge (prog_main ?? p);:
1015    ! f ← find_funct_ptr ? ? ge b;:
1016    ret ? (Callstate f (nil ?) Kstop m0)).
1017nwhd;
1018napply opt_bindIO_OK; #b eb;
1019napply opt_bindIO_OK; #f ef;
1020nwhd; napply (initial_state_intro … eb ef);
1021nqed.
1022
1023ndefinition is_final_state : ∀st:state. (∃r. final_state st r) + (¬∃r. final_state st r).
1024#st; nelim st;
1025##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
1026##| #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
1027##| #v k m; ncases k;
1028  ##[ ncases v;
1029    ##[ ##2: #i; @1; @ i; //;
1030    ##| ##1: @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
1031    ##| #f; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
1032    ##| #b of; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
1033    ##]
1034  ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
1035  ##| ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
1036  ##| ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
1037  ##| #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
1038  ##]
1039##] nqed.
1040
1041nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
1042 IO (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝
1043match is_final_state s with
1044[ inl _ ⇒ Some ? (ret ? 〈E0, s〉)
1045| inr _ ⇒
1046  match n with
1047  [ O ⇒ Some ? (ret ? 〈E0, s〉)
1048  | S n' ⇒ Some ? (
1049      ! 〈t,s'〉 ← exec_step ge s;:
1050      ! 〈t',s''〉 ← exec_steps n' ge s';:
1051      ret ? 〈t ⧺ t',s''〉)
1052  ]
1053]. nwhd; /2/;
1054napply sig_bindIO2_OK; #t s' H1;
1055napply sig_bindIO2_OK; #t' s'' IH;
1056nwhd; napply (star_step … IH); //;
1057nqed.
1058(*
1059nlet rec exec_steps_without_proof (n:nat) (ge:genv) (s:state) :
1060 res (trace×state) ≝
1061match is_final_state s with
1062[ inl _ ⇒ OK ? 〈E0, s〉
1063| inr _ ⇒
1064  match n with
1065  [ O ⇒ OK ? 〈E0, s〉
1066  | S n' ⇒
1067      〈t,s'〉 ← exec_step ge s;:
1068      〈t',s''〉 ← exec_steps_without_proof n' ge s';:
1069      OK ? 〈t ⧺ t',s''〉
1070  ]
1071].
1072*)
Note: See TracBrowser for help on using the repository browser.