Changeset 487 for Deliverables/D3.1/Csemantics/Cexec.ma
 Timestamp:
 Feb 9, 2011, 11:49:17 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Cexec.ma
r485 r487 5 5 include "IOMonad.ma". 6 6 7 (* 7 8 include "Plogic/russell_support.ma". 8 9 ndefinition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝9 *) 10 definition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝ 10 11 λA,P,a.match a with [ None ⇒ False  Some y ⇒ match y return λ_.CProp[0] with [ Error ⇒ True  OK z ⇒ P z ]]. 11 12 12 ndefinition err_inject : ∀A.∀P:A → Prop.∀a:option (res A).∀p:P_to_P_option_res A P a.res (sigmaA P) ≝13 definition err_inject : ∀A.∀P:A → Prop.∀a:option (res A).∀p:P_to_P_option_res A P a.res (Sig A P) ≝ 13 14 λA.λP:A → Prop.λa:option (res A).λp:P_to_P_option_res A P a. 14 (match a return λa'.a=a' → res ( sigmaA P) with15 (match a return λa'.a=a' → res (Sig A P) with 15 16 [ None ⇒ λe1.? 16 17  Some b ⇒ λe1.(match b return λb'.b=b' → ? with 17 18 [ Error ⇒ λ_. Error ? 18  OK c ⇒ λe2. OK ? ( sig_introA P c ?)19  OK c ⇒ λe2. OK ? (dp A P c ?) 19 20 ]) (refl ? b) 20 21 ]) (refl ? a). 21 ##[ nrewrite > e1 in p; nnormalize; *;22 ## nrewrite > e1 in p; nrewrite > e2; nnormalize; //23 ##] nqed.24 25 ndefinition err_eject : ∀A.∀P: A → Prop. res (sigmaA P) → res A ≝22 [ >e1 in p; normalize; *; 23  >e1 in p >e2 normalize; // 24 ] qed. 25 26 definition err_eject : ∀A.∀P: A → Prop. res (Sig A P) → res A ≝ 26 27 λA,P,a.match a with [ Error ⇒ Error ?  OK b ⇒ 27 match b with [ sig_introw p ⇒ OK ? w] ].28 29 ndefinition sig_eject : ∀A.∀P: A → Prop. sigmaA P → A ≝30 λA,P,a.match a with [ sig_introw p ⇒ w].31 32 ncoercion err_inject :33 ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_res ? P a.res ( sigmaA P) ≝ err_inject34 on a:option (res ?) to res ( sigma? ?).35 ncoercion err_eject : ∀A.∀P:A → Prop.∀c:res (sigmaA P).res A ≝ err_eject36 on _c:res ( sigma? ?) to res ?.37 ncoercion sig_eject : ∀A.∀P:A → Prop.∀c:sigmaA P.A ≝ sig_eject38 on _c: sigma? ? to ?.39 40 ndefinition P_res: ∀A.∀P:A → Prop.res A → Prop ≝28 match b with [ dp w p ⇒ OK ? w] ]. 29 30 definition sig_eject : ∀A.∀P: A → Prop. Sig A P → A ≝ 31 λA,P,a.match a with [ dp w p ⇒ w]. 32 33 coercion err_inject : 34 ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_res ? P a.res (Sig A P) ≝ err_inject 35 on a:option (res ?) to res (Sig ? ?). 36 coercion err_eject : ∀A.∀P:A → Prop.∀c:res (Sig A P).res A ≝ err_eject 37 on _c:res (Sig ? ?) to res ?. 38 coercion sig_eject : ∀A.∀P:A → Prop.∀c:Sig A P.A ≝ sig_eject 39 on _c:Sig ? ? to ?. 40 41 definition P_res: ∀A.∀P:A → Prop.res A → Prop ≝ 41 42 λA,P,a. match a with [ Error ⇒ True  OK v ⇒ P v ]. 42 43 43 ndefinition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝44 definition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝ 44 45 λv,ty. match v in val with 45 46 [ Vint i ⇒ match ty with … … 62 63 ]. 63 64 64 nlemma bool_of_val_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ exec_bool_of_val v ty = OK ? b.65 #v ty r H; nelim H; #v t H'; nelim H';66 ##[ #i is s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne);//;67 ## #p b i i0 s; @ true; @;//68 ## #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne);//;69 ## #i s; @ false; @;//;70 ## #r r' t; @ false; @;//;71 ## #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …);//;72 ##]73 nqed.65 lemma bool_of_val_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ exec_bool_of_val v ty = OK ? b. 66 #v #ty #r #H elim H; #v #t #H' elim H'; 67 [ #i #is #s #ne %{ true} % //; whd in ⊢ (??%?); >(eq_false … ne) //; 68  #p #b #i #i0 #s %{ true} % // 69  #f #s #ne %{ true} % //; whd in ⊢ (??%?); >(Feq_zero_false … ne) //; 70  #i #s %{ false} % //; 71  #r #r' #t %{ false} % //; 72  #s %{ false} % //; whd in ⊢ (??%?); >(Feq_zero_true …) //; 73 ] 74 qed. 74 75 75 76 (* Prove a few minor results to make proof obligations easy. *) 76 77 77 nlemma bind_OK: ∀A,B,P,e,f.78 lemma bind_OK: ∀A,B,P,e,f. 78 79 (∀v. e = OK A v → match f v with [ Error ⇒ True  OK v' ⇒ P v' ]) → 79 80 match bind A B e f with [ Error ⇒ True  OK v ⇒ P v ]. 80 #A B P e f; nelim e; /2/; nqed.81 82 nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigmaA P → res B.83 (∀v:A. ∀p:P v. match f ( sig_introA P v p) with [ Error ⇒ True  OK v' ⇒ P' v'] ) →84 match bind ( sigmaA P) B e f with [ Error ⇒ True  OK v' ⇒ P' v' ].85 #A B P P' e f; nelim e;86 ##[ #v0; nelim v0; #v Hv IH; napply IH; 87 ## #_; napply I; 88 ##] nqed.89 90 nlemma bind2_OK: ∀A,B,C,P,e,f.81 #A #B #P #e #f elim e; /2/; qed. 82 83 lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B. 84 (∀v:A. ∀p:P v. match f (dp A P v p) with [ Error ⇒ True  OK v' ⇒ P' v'] ) → 85 match bind (Sig A P) B e f with [ Error ⇒ True  OK v' ⇒ P' v' ]. 86 #A #B #P #P' #e #f elim e; 87 [ #v0 elim v0; #v #Hv #IH @IH 88  #_ @I 89 ] qed. 90 91 lemma bind2_OK: ∀A,B,C,P,e,f. 91 92 (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True  OK v' ⇒ P v' ]) → 92 93 match bind2 A B C e f with [ Error ⇒ True  OK v ⇒ P v ]. 93 #A B C P e f; nelim e; //; #v; ncases v; /2/; nqed.94 95 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.94 #A #B #C #P #e #f elim e; //; #v cases v; /2/; qed. 95 96 lemma sig_bind2_OK: ∀A,B,C. ∀P:A×B → Prop. ∀P':C → Prop. ∀e:res (Sig (A×B) P). ∀f:A → B → res C. 96 97 (∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True  OK v' ⇒ P' v'] ) → 97 98 match bind2 A B C e f with [ Error ⇒ True  OK v' ⇒ P' v' ]. 98 #A B C P P' e f; nelim e; //;99 #v0 ; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed.100 101 nlemma opt_bind_OK: ∀A,B,P,e,f.99 #A #B #C #P #P' #e #f elim e; //; 100 #v0 elim v0; #v elim v; #v1 #v2 #Hv #IH @IH //; qed. 101 102 lemma opt_bind_OK: ∀A,B,P,e,f. 102 103 (∀v. e = Some A v → match f v with [ Error ⇒ True  OK v' ⇒ P v' ]) → 103 104 match bind A B (opt_to_res A e) f with [ Error ⇒ True  OK v ⇒ P v ]. 104 #A B P e f; nelim e; nnormalize; /2/; nqed.105 106 nlemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B  P e}. ∀Q:A→B→res C. ∀R:C→Prop.105 #A #B #P #e #f elim e; normalize; /2/; qed. 106 (* 107 lemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B  P e}. ∀Q:A→B→res C. ∀R:C→Prop. 107 108 (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v  Error ⇒ True]) → 108 match match eject ?? e with [ mk_pair a b ⇒ Q a b ] with [ OK v ⇒ R v  Error ⇒ True ].109 #A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;110 ##[ #H; napply (False_ind … H); 111 ## #e''; ncases e''; #a b Pab H; nnormalize; /2/;112 ##] nqed.113 109 match match eject ?? e with [ pair a b ⇒ Q a b ] with [ OK v ⇒ R v  Error ⇒ True ]. 110 #A #B #C #P #e #Q #R cases e; #e' cases e'; normalize; 111 [ #H @(False_ind … H) 112  #e'' cases e''; #a #b #Pab #H normalize; /2/; 113 ] qed. 114 *) 114 115 (* 115 116 nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B  OK v ⇒ Error B ] = Error B. 116 #A B e; ncases e; //; nqed.117 #A #B #e cases e; //; qed. 117 118 *) 118 119 119 ndefinition try_cast_null : ∀m:mem. ∀i:int. ∀ty:type. ∀ty':type. res val ≝120 definition try_cast_null : ∀m:mem. ∀i:int. ∀ty:type. ∀ty':type. res val ≝ 120 121 λm:mem. λi:int. λty:type. λty':type. 121 122 match eq i zero with … … 134 135 ]. 135 136 136 ndefinition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝137 definition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝ 137 138 λm:mem. λv:val. λty:type. λty':type. 138 139 match v with … … 165 166  Vptr p b ofs ⇒ 166 167 do s ← match ty with [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code  _ ⇒ Error ? ]; 167 do u ← match eq_region_dec p s with [ inl _ ⇒ OK ? something inr _ ⇒ Error ? ];168 do u ← match eq_region_dec p s with [ inl _ ⇒ OK ? it  inr _ ⇒ Error ? ]; 168 169 do s' ← match ty' with 169 170 [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code … … 174 175  Vnull r ⇒ 175 176 do s ← match ty with [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code  _ ⇒ Error ? ]; 176 do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? something inr _ ⇒ Error ? ];177 do u ← match eq_region_dec r s with [ inl _ ⇒ OK ? it  inr _ ⇒ Error ? ]; 177 178 do s' ← match ty' with 178 179 [ Tpointer s _ ⇒ OK ? s  Tarray s _ _ ⇒ OK ? s  Tfunction _ _ ⇒ OK ? Code … … 182 183 ]. 183 184 184 ndefinition load_value_of_type' ≝185 λty,m,l. match l with [ mk_pair pl ofs ⇒ match pl with [ mk_pair psp loc ⇒185 definition load_value_of_type' ≝ 186 λty,m,l. match l with [ pair pl ofs ⇒ match pl with [ pair psp loc ⇒ 186 187 load_value_of_type ty m psp loc ofs ] ]. 187 188 … … 190 191 and use exec_lvalue'. *) 191 192 192 nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝193 let rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝ 193 194 match e with 194 195 [ Expr e' ty ⇒ … … 210 211  Eaddrof a ⇒ 211 212 do 〈plo,tr〉 ← exec_lvalue ge en m a; 212 OK ? 〈match plo with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉213 OK ? 〈match plo with [ pair pl ofs ⇒ match pl with [ pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉 213 214  Esizeof ty' ⇒ OK ? 〈Vint (repr (sizeof ty')), E0〉 214 215  Eunop op a ⇒ … … 282 283 match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ]. 283 284 284 nlemma P_res_to_P: ∀A,P,e,v. P_res A P e → e = OK A v → P v.285 #A P e v H1 H2; nrewrite > H2 in H1; nwhd in ⊢ (% → ?); //; nqed.285 lemma P_res_to_P: ∀A,P,e,v. P_res A P e → e = OK A v → P v. 286 #A #P #e #v #H1 #H2 >H2 in H1; whd in ⊢ (% → ?); //; qed. 286 287 287 288 (* We define a special induction principle tailored to the recursive definition 288 289 above. *) 289 290 290 ndefinition is_not_lvalue: expr_descr → Prop ≝291 definition is_not_lvalue: expr_descr → Prop ≝ 291 292 λe. match e with [ Evar _ ⇒ False  Ederef _ ⇒ False  Efield _ _ ⇒ False  _ ⇒ True ]. 292 293 293 ndefinition Plvalue ≝ λP:(expr → Prop).λe,ty.294 definition Plvalue ≝ λP:(expr → Prop).λe,ty. 294 295 match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty)  Ederef _ ⇒ P (Expr e ty)  Efield _ _ ⇒ P (Expr e ty)  _ ⇒ True ]. 295 296 296 297 (* TODO: Can we do this sensibly with a map combinator? *) 297 nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝298 let rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝ 298 299 match l with 299 300 [ nil ⇒ OK ? 〈nil val, E0〉 … … 304 305 ]. 305 306 306 (* Don't really want to use subset rather than sigma here, but can't be bothered 307 with *another* set of coercions. XXX: why do I have to get the recursive 308 call's property manually? *) 309 310 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) } ≝ 307 let rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : env × mem ≝ 311 308 match l with 312 [ nil ⇒ Some ?〈en, m〉309 [ nil ⇒ 〈en, m〉 313 310  cons h vars ⇒ 314 match h with [ mk_pair id ty ⇒ 315 match alloc m 0 (sizeof ty) Any with [ mk_pair m1 b1 ⇒ 316 match exec_alloc_variables (set … id b1 en) m1 vars with 317 [ sig_intro r p ⇒ r ] 318 ]]]. nwhd; 319 ##[ //; 320 ## nelim (exec_alloc_variables (set ident ? ? c3 c7 en) c6 c1); 321 #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH; 322 napply (alloc_variables_cons … IH); /2/; 323 nqed. 311 match h with [ pair id ty ⇒ 312 match alloc m 0 (sizeof ty) Any with [ pair m1 b1 ⇒ 313 exec_alloc_variables (set … id b1 en) m1 vars 314 ]]]. 324 315 325 316 (* TODO: can we establish that length params = length vs in advance? *) 326 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)≝317 let rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res mem ≝ 327 318 match params with 328 [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m)  cons _ _ ⇒ Some ? (Error ?)]329  cons idty params' ⇒ match idty with [ mk_pair id ty ⇒319 [ nil ⇒ match vs with [ nil ⇒ OK ? m  cons _ _ ⇒ Error ? ] 320  cons idty params' ⇒ match idty with [ pair id ty ⇒ 330 321 match vs with 331 [ nil ⇒ Some ? (Error ?)332  cons v1 vl ⇒ Some ? (322 [ nil ⇒ Error ? 323  cons v1 vl ⇒ 333 324 do b ← opt_to_res ? (get … id e); 334 325 do m1 ← opt_to_res ? (store_value_of_type ty m Any b zero v1); 335 e rr_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)326 exec_bind_parameters e m1 params' vl 336 327 ] 337 328 ] ]. 338 nwhd; //; 339 napply opt_bind_OK; #b eb; 340 napply opt_bind_OK; #m1 em1; 341 napply sig_bind_OK; #m2 Hm2; 342 napply (bind_parameters_cons … eb em1 Hm2); 343 nqed. 344 345 alias id "Tint" = "cic:/matita/csemantics/Csyntax/type.con(0,2,0)". 346 alias id "Tfloat" = "cic:/matita/csemantics/Csyntax/type.con(0,3,0)". 347 ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2). 348 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. 349 ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2). 350 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. 351 ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2). 352 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. 353 354 nlet rec type_eq_dec (t1,t2:type) : (t1 = t2) + (t1 ≠ t2) ≝ 329 330 definition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2). 331 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed. 332 definition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2). 333 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed. 334 definition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2). 335 #s1 cases s1; #s2 cases s2; /2/; %2 ; % #H destruct; qed. 336 337 let rec type_eq_dec (t1,t2:type) : (t1 = t2) + (t1 ≠ t2) ≝ 355 338 match t1 return λt'. (t' = t2) + (t' ≠ t2) with 356 339 [ Tvoid ⇒ match t2 return λt'. (Tvoid = t') + (Tvoid ≠ t') with [ Tvoid ⇒ inl ?? (refl ??)  _ ⇒ inr ?? (nmk ? (λH.?)) ] … … 424 407  inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] 425 408  inr e ⇒ inr ?? (nmk ? (λH.match e with [ nmk e' ⇒ e' ? ])) ] ] 426 ]. ndestruct; //; nqed.427 428 ndefinition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝409 ]. destruct; //; qed. 410 411 definition assert_type_eq : ∀t1,t2:type. res (t1 = t2) ≝ 429 412 λt1,t2. match type_eq_dec t1 t2 with [ inl p ⇒ OK ? p  inr _ ⇒ Error ? ]. 430 413 431 nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝414 let rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝ 432 415 match k return λk'.(is_call_cont k') + (¬is_call_cont k') with 433 416 [ Kstop ⇒ ? … … 435 418  _ ⇒ ? 436 419 ]. 437 ##[ ##1,8: @1; //438 ## ##*: @2; /2/439 ##] nqed.440 441 ndefinition is_Sskip : ∀s:statement. (s = Sskip) + (s ≠ Sskip) ≝420 [ 1,8: %1 ; // 421  *: %2 ; /2/ 422 ] qed. 423 424 definition is_Sskip : ∀s:statement. (s = Sskip) + (s ≠ Sskip) ≝ 442 425 λs.match s return λs'.(s' = Sskip) + (s' ≠ Sskip) with 443 426 [ Sskip ⇒ inl ?? (refl ??) 444 427  _ ⇒ inr ?? (nmk ? (λH.?)) 445 ]. ndestruct;446 nqed.428 ]. destruct 429 qed. 447 430 448 431 (* Checking types of values given to / received from an external function call. *) 449 432 450 ndefinition eventval_type : ∀ty:typ. Type≝433 definition eventval_type : ∀ty:typ. Type[0] ≝ 451 434 λty. match ty with [ ASTint ⇒ int  ASTfloat ⇒ float ]. 452 435 453 ndefinition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝436 definition mk_eventval: ∀ty:typ. eventval_type ty → eventval ≝ 454 437 λty:typ. match ty return λty'.eventval_type ty' → eventval with [ ASTint ⇒ λv.EVint v  ASTfloat ⇒ λv.EVfloat v ]. 455 438 456 ndefinition mk_val: ∀ty:typ. eventval_type ty → val ≝439 definition mk_val: ∀ty:typ. eventval_type ty → val ≝ 457 440 λty:typ. match ty return λty'.eventval_type ty' → val with [ ASTint ⇒ λv.Vint v  ASTfloat ⇒ λv.Vfloat v ]. 458 441 459 nlemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty.442 lemma mk_val_correct: ∀ty:typ. ∀v:eventval_type ty. 460 443 eventval_match (mk_eventval ty v) ty (mk_val ty v). 461 #ty ; ncases ty; nnormalize; //; nqed.462 463 ndefinition convert_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v)≝444 #ty cases ty; normalize; //; qed. 445 446 definition convert_eventval : ∀ev:eventval. ∀ty:typ. res val ≝ 464 447 λev,ty. 465 448 match ty with 466 [ ASTint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i))  _ ⇒ Some ? (Error ?)]467  ASTfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f))  _ ⇒ Some ? (Error ?)]468  _ ⇒ Some ? (Error ?)469 ]. nwhd; //; nqed.470 471 ndefinition check_eventval' : ∀v:val. ∀ty:typ. res (Σev:eventval. eventval_match ev ty v)≝449 [ ASTint ⇒ match ev with [ EVint i ⇒ OK ? (Vint i)  _ ⇒ Error ? ] 450  ASTfloat ⇒ match ev with [ EVfloat f ⇒ OK ? (Vfloat f)  _ ⇒ Error ? ] 451  _ ⇒ Error ? 452 ]. 453 454 definition check_eventval' : ∀v:val. ∀ty:typ. res eventval ≝ 472 455 λv,ty. 473 456 match ty with 474 [ ASTint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i))  _ ⇒ Some ? (Error ?)]475  ASTfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f))  _ ⇒ Some ? (Error ?)]457 [ ASTint ⇒ match v with [ Vint i ⇒ OK ? (EVint i)  _ ⇒ Error ? ] 458  ASTfloat ⇒ match v with [ Vfloat f ⇒ OK ? (EVfloat f)  _ ⇒ Error ? ] 476 459  _ ⇒ Some ? (Error ?) 477 ]. nwhd; //; nqed.478 479 nlet rec check_eventval_list (vs: list val) (tys: list typ) : res (Σevs:list eventval. eventval_list_match evs tys vs) ≝460 ]. 461 462 let rec check_eventval_list (vs: list val) (tys: list typ) : res (list eventval) ≝ 480 463 match vs with 481 [ nil ⇒ match tys with [ nil ⇒ Some ? (OK ? (nil ?))  _ ⇒ Some ? (Error ?)]464 [ nil ⇒ match tys with [ nil ⇒ OK ? (nil ?)  _ ⇒ Error ? ] 482 465  cons v vt ⇒ 483 466 match tys with 484 [ nil ⇒ Some ? (Error ?)485  cons ty tyt ⇒ Some ? (467 [ nil ⇒ Error ? 468  cons ty tyt ⇒ 486 469 do ev ← check_eventval' v ty; 487 470 do evt ← check_eventval_list vt tyt; 488 OK ? ((sig_eject ?? ev)::evt)) 489 ] 490 ]. nwhd; //; 491 napply sig_bind_OK; #ev Hev; 492 napply sig_bind_OK; #evt Hevt; 493 nnormalize; /2/; 494 nqed. 471 OK ? (ev::evt) 472 ] 473 ]. 495 474 496 475 (* IO monad *) … … 498 477 (* Interactions are function calls that return a value and do not change 499 478 the rest of the Clight program's state. *) 500 nrecord io_out : Type≝479 record io_out : Type[0] ≝ 501 480 { io_function: ident 502 481 ; io_args: list eventval … … 504 483 }. 505 484 506 ndefinition io_in ≝ λo. eventval_type (io_in_typ o).507 508 ndefinition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝485 definition io_in ≝ λo. eventval_type (io_in_typ o). 486 487 definition do_io : ident → list eventval → ∀t:typ. IO io_out io_in (eventval_type t) ≝ 509 488 λfn,args,t. Interact ??? (mk_io_out fn args t) (λres. Value ??? res). 510 489 511 ndefinition ret: ∀T. T → (IO io_out io_in T) ≝490 definition ret: ∀T. T → (IO io_out io_in T) ≝ 512 491 λT,x.(Value ?? T x). 513 492 514 493 (* execution *) 515 494 516 ndefinition store_value_of_type' ≝495 definition store_value_of_type' ≝ 517 496 λty,m,l,v. 518 match l with [ mk_pair pl ofs ⇒519 match pl with [ mk_pair pcl loc ⇒497 match l with [ pair pl ofs ⇒ 498 match pl with [ pair pcl loc ⇒ 520 499 store_value_of_type ty m pcl loc ofs v ] ]. 521 500 522 nlet rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝501 let rec exec_step (ge:genv) (st:state) on st : (IO io_out io_in (trace × state)) ≝ 523 502 match st with 524 503 [ State f s k e m ⇒ … … 639 618  Sgoto lbl ⇒ 640 619 match find_label lbl (fn_body f) (call_cont k) with 641 [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ]620 [ Some sk' ⇒ match sk' with [ pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ] 642 621  None ⇒ Wrong ??? 643 622 ] … … 647 626 match f0 with 648 627 [ Internal f ⇒ 649 match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒650 ! m2 ← e rr_to_io_sig … (exec_bind_parameters e m1 (fn_params f) vargs);628 match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ pair e m1 ⇒ 629 ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs; 651 630 ret ? 〈E0, State f (fn_body f) k e m2〉 652 631 ] 653 632  External f argtys retty ⇒ 654 ! evargs ← err_to_io_sig … (check_eventval_list vargs (typlist_of_typelist argtys));633 ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys); 655 634 ! evres ← do_io f evargs (proj_sig_res (signature_of_type argtys retty)); 656 635 ret ? 〈Eextcall f evargs (mk_eventval ? evres), Returnstate (mk_val ? evres) k m〉 … … 662 641 [ None ⇒ ret ? 〈E0, (State f Sskip k' e m)〉 663 642  Some r' ⇒ 664 match r' with [ mk_pair l ty ⇒643 match r' with [ pair l ty ⇒ 665 644 666 645 ! m' ← store_value_of_type' ty m l res; … … 672 651 ]. 673 652 674 nlet rec make_initial_state (p:clight_program) : res (genv × state) ≝653 let rec make_initial_state (p:clight_program) : res (genv × state) ≝ 675 654 do ge ← globalenv Genv ?? p; 676 655 do m0 ← init_mem Genv ?? p; 677 656 do 〈sp,b〉 ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p)); 678 do u ← opt_to_res ? (match eq_region_dec sp Code with [ inl _ ⇒ Some ? something inr _ ⇒ None ? ]);657 do u ← opt_to_res ? (match eq_region_dec sp Code with [ inl _ ⇒ Some ? it  inr _ ⇒ None ? ]); 679 658 do f ← opt_to_res ? (find_funct_ptr ? ? ge b); 680 659 OK ? 〈ge,Callstate f (nil ?) Kstop m0〉. 681 660 682 ndefinition is_final_state : ∀st:state. (Σr. final_state st r) + (¬∃r. final_state st r).683 #st ; nelim st;684 ##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;685 ## #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;686 ## #v k m; ncases k;687 ##[ ncases v;688 ##[ ##2: #i; @1; @ i;//;689 ## ##1: @2; @; *; #r H; ninversion H; #i m e; ndestruct;690 ## #f; @2; @; *; #r H; ninversion H; #i m e; ndestruct;691 ## #r; @2; @; *; #r H; ninversion H; #i m e; ndestruct;692 ## #r b of; @2; @; *; #r H; ninversion H; #i m e; ndestruct;693 ##]694 ## #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;695 ## ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct;696 ## ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct;697 ## #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct;698 ##]699 ##] nqed.700 701 nlet rec exec_steps (n:nat) (ge:genv) (s:state) :661 definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r). 662 #st elim st; 663 [ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct; 664  #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct; 665  #v #k #m cases k; 666 [ cases v; 667 [ 2: #i %1 ; %{ i} //; 668  1: %2 ; % *; #r #H inversion H; #i #m #e destruct; 669  #f %2 ; % *; #r #H inversion H; #i #m #e destruct; 670  #r %2 ; % *; #r #H inversion H; #i #m #e destruct; 671  #r #b #of %2 ; % *; #r #H inversion H; #i #m #e destruct; 672 ] 673  #a #b %2 ; % *; #r #H inversion H; #i #m #e destruct; 674  3,4: #a #b #c %2 ; % *; #r #H inversion H; #i #m #e destruct; 675  5,6,8: #a #b #c #d %2 ; % *; #r #H inversion H; #i #m #e destruct; 676  #a %2 ; % *; #r #H inversion H; #i #m #e destruct; 677 ] 678 ] qed. 679 680 let rec exec_steps (n:nat) (ge:genv) (s:state) : 702 681 IO io_out io_in (trace×state) ≝ 703 682 match is_final_state s with … … 724 703 725 704 (* A (possibly nonterminating) execution. *) 726 ncoinductive execution : Type≝705 coinductive execution : Type[0] ≝ 727 706  e_stop : trace → int → mem → execution 728 707  e_step : trace → state → execution → execution … … 730 709  e_interact : ∀o:io_out. (io_in o → execution) → execution. 731 710 732 ndefinition mem_of_state : state → mem ≝711 definition mem_of_state : state → mem ≝ 733 712 λs.match s with [ State f s k e m ⇒ m  Callstate f a k m ⇒ m  Returnstate r k m ⇒ m ]. 734 713 … … 737 716 state. *) 738 717 739 nlet corec exec_inf_aux (ge:genv) (s:IO io_out io_in (trace×state)) : execution ≝718 let corec exec_inf_aux (ge:genv) (s:IO io_out io_in (trace×state)) : execution ≝ 740 719 match s with 741 720 [ Wrong ⇒ e_wrong 742  Value v ⇒ match v with [ mk_pair t s' ⇒721  Value v ⇒ match v with [ pair t s' ⇒ 743 722 match is_final_state s' with 744 723 [ inl r ⇒ e_stop t (sig_eject … r) (mem_of_state s') … … 748 727 749 728 750 ndefinition exec_inf : clight_program → execution ≝729 definition exec_inf : clight_program → execution ≝ 751 730 λp. 752 731 match make_initial_state p with … … 755 734 ]. 756 735 757 nremarkexecution_cases: ∀e.736 lemma execution_cases: ∀e. 758 737 e = match e with [ e_stop tr r m ⇒ e_stop tr r m  e_step tr s e ⇒ e_step tr s e 759 738  e_wrong ⇒ e_wrong  e_interact o k ⇒ e_interact o k ]. 760 #e ; ncases e; //; nqed.761 762 nlemma exec_inf_aux_unfold: ∀ge,s. exec_inf_aux ge s =739 #e cases e; //; qed. 740 741 lemma exec_inf_aux_unfold: ∀ge,s. exec_inf_aux ge s = 763 742 match s with 764 743 [ Wrong ⇒ e_wrong 765  Value v ⇒ match v with [ mk_pair t s' ⇒744  Value v ⇒ match v with [ pair t s' ⇒ 766 745 match is_final_state s' with 767 746 [ inl r ⇒ e_stop t (sig_eject … r) (mem_of_state s') … … 769 748  Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v)) 770 749 ]. 771 #ge s; nrewrite > (execution_cases (exec_inf_aux …)); ncases s;772 ##[ #ok773 ## #x; ncases x; #tr s'; ncases s';774 ##[ #fn st k envm775 ## #fd args kmem776 ## #v k mem; (* for final state check *) ncases k;777 ##[ ncases v; ##[ ##2,3: #v' ## ##4: #r ## ##5: #sp loc off ##]778 ## #s' k' ## ##3,4: #e s' k' ## ##5,6: #e s' s'' k' ## #k' ## #a b c d ##]779 ##]780 ## ##]781 nwhd in ⊢ (??%%); //;782 nqed.783 750 #ge #s >(execution_cases (exec_inf_aux …)) cases s; 751 [ #o #k 752  #x cases x; #tr #s' cases s'; 753 [ #fn #st #k #env #m 754  #fd #args #k #mem 755  #v #k #mem (* for final state check *) cases k; 756 [ cases v; [ 2,3: #v'  4: #r  5: #sp #loc #off ] 757  #s' #k'  3,4: #e #s' #k'  5,6: #e #s' #s'' #k'  #k'  #a #b #c #d ] 758 ] 759  ] 760 whd in ⊢ (??%%); //; 761 qed. 762
Note: See TracChangeset
for help on using the changeset viewer.