Changeset 9 for Csemantics/Cexec.ma
 Timestamp:
 Jun 21, 2010, 4:22:09 PM (11 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Cexec.ma
r5 r9 128 128 ## #b i t0; @ true; @; // 129 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 …); //;130 ## #i s; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*) 131 ## #t; @ false; @; //; (*nwhd in ⊢ (??%?); nrewrite > (eq_true …); //;*) 132 132 ## #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //; 133 133 ##] … … 213 213 ## #b i t0; @ true; @; // 214 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 …); //;215 ## #i s; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*) 216 ## #t; @ false; @; //; (*nwhd; nrewrite > (eq_true …); //;*) 217 217 ## #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //; 218 218 ##] … … 220 220 221 221 (* Prove a few minor results to make proof obligations easy. *) 222 223 nlemma 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. 222 226 223 227 nlemma bind_OK: ∀A,B,P,e,f. … … 290 294 match e' with 291 295 [ Econst_int i ⇒ Some ? (OK ? (Vint i)) 296  Econst_float f ⇒ Some ? (OK ? (Vfloat f)) 292 297  Evar _ ⇒ Some ? ( 298 〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;: 299 opt_to_res ? (load_value_of_type ty m loc ofs)) 300  Ederef _ ⇒ Some ? ( 293 301 〈loc, ofs〉 ← exec_lvalue' ge en m e' ty;: 294 302 opt_to_res ? (load_value_of_type ty m loc ofs)) … … 296 304 〈loc, ofs〉 ← exec_lvalue ge en m a;: 297 305 OK ? (Vptr loc ofs)) 306  Esizeof ty' ⇒ Some ? (OK ? (Vint (repr (sizeof ty')))) 298 307  Eunop op a ⇒ Some ? ( 299 308 v1 ← exec_expr ge en m a;: 300 309 opt_to_res ? (sem_unary_operation op v1 (typeof a))) 310  Ebinop op a1 a2 ⇒ Some ? ( 311 v1 ← exec_expr ge en m a1;: 312 v2 ← exec_expr ge en m a2;: 313 opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m)) 301 314  Econdition a1 a2 a3 ⇒ Some ? ( 302 315 v ← exec_expr ge en m a1;: … … 312 325 l ← opt_to_res ? (get ? PTree ? id en);: 313 326 OK ? 〈l, zero〉) 327  Ederef a ⇒ Some ? ( 328 v ← exec_expr ge en m a;: 329 match v with 330 [ Vptr l ofs ⇒ OK ? 〈l,ofs〉 331  _ ⇒ Error ? 332 ]) 314 333  _ ⇒ Some ? (Error ?) 315 334 ] … … 319 338 ##[ napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H; 320 339 napply opt_OK; #v ev; /2/; 340 ## napply sig_bind2_OK; nrewrite > c2; nrewrite > c4; #loc ofs H; 341 napply opt_OK; #v ev; /2/; 321 342 ## napply sig_bind2_OK; #loc ofs H; 322 343 nwhd; napply eval_Eaddrof; //; … … 324 345 napply opt_OK; #v ev; 325 346 napply (eval_Eunop … Hv1 ev); 347 ## napply sig_bind_OK; #v1 ev1 Hv1; 348 napply sig_bind_OK; #v2 ev2 Hv2; 349 napply opt_OK; #v ev; 350 napply (eval_Ebinop … Hv1 Hv2 ev); 326 351 ## napply sig_bind_OK; #vb evb Hvb; 327 352 napply sig_bind_OK; #b; … … 330 355 ## napply (eval_Econdition_false … Hvb ? Hv); napply (bool_of ??? Hb); 331 356 ##] 332 ## napply opt_bind_OK; #l el; napply eval_Evar_local; // 357 ## napply opt_bind_OK; #l el; napply eval_Evar_local; // 358 ## napply sig_bind_OK; #v; ncases v; //; #l ofs ev Hv; nwhd; 359 napply eval_Ederef; // 360 333 361 ##] nqed. 362 363 (* TODO: Can we do this sensibly with a map combinator? *) 364 nlet 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) ≝ 365 match l with 366 [ nil ⇒ Some ? (OK ? (nil val)) 367  cons e1 es ⇒ Some ? ( 368 v ← exec_expr ge e m e1;: 369 vs ← exec_exprlist ge e m es;: 370 OK ? (cons val v vs)) 371 ]. nwhd; //; 372 napply sig_bind_OK; #v ev Hv; 373 napply sig_bind_OK; #vs evs Hvs; 374 nnormalize; /2/; 375 nqed. 334 376 335 377 (* Don't really want to use subset rather than sigma here, but can't be bothered … … 377 419 ]. nwhd; //; @; #H; ndestruct; nqed. 378 420 421 ninductive decide : Type ≝ 422  dy : decide  dn : decide. 423 424 ndefinition dodecide : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P  dn ⇒ ¬P ]).P + ¬P. 425 #P d;ncases d;/2/; nqed. 426 427 ncoercion decide_inject : 428 ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P  dn ⇒ ¬P ]).P + ¬P ≝ dodecide 429 on d:decide to ? + (¬?). 430 431 alias id "Tint" = "cic:/matita/csemantics/Csyntax/type.con(0,2,0)". 432 alias id "Tfloat" = "cic:/matita/csemantics/Csyntax/type.con(0,3,0)". 433 ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2). 434 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. 435 ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2). 436 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. 437 ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2). 438 #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. 439 440 (* Not very happy about this. *) 441 nlet rec type_eq_dec (t1,t2:type) : Sum (t1 = t2) (t1 ≠ t2) ≝ 442 match t1 with 443 [ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy  _ ⇒ dn ] 444  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 ] 445  Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy  _ ⇒ dn ]  _ ⇒ dn ] 446  Tpointer t ⇒ match t2 with [ Tpointer t' ⇒ match type_eq_dec t t' with [ inl _ ⇒ dy  inr _ ⇒ dn ]  _ ⇒ dn ] 447  Tarray t n ⇒ match t2 with [ Tarray t' n' ⇒ 448 match type_eq_dec t t' with [ inl _ ⇒ 449 match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy  inr _ ⇒ dn ]  inr _ ⇒ dn ]  _ ⇒ dn ] 450  Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match typelist_eq_dec tl tl' with [ inl _ ⇒ 451 match type_eq_dec t t' with [ inl _ ⇒ dy  inr _ ⇒ dn ]  inr _ ⇒ dn ]  _ ⇒ dn ] 452  Tstruct i fl ⇒ 453 match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒ 454 match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy  inr _ ⇒ dn ]  inr _ ⇒ dn ]  _ ⇒ dn ] 455  Tunion i fl ⇒ 456 match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒ 457 match fieldlist_eq_dec fl fl' with [ inl _ ⇒ dy  inr _ ⇒ dn ]  inr _ ⇒ dn ]  _ ⇒ dn ] 458  Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy  inr _ ⇒ dn ]  _ ⇒ dn ] 459 ] 460 and typelist_eq_dec (tl1,tl2:typelist) : (tl1 = tl2) + (tl1 ≠ tl2) ≝ 461 match tl1 with 462 [ Tnil ⇒ match tl2 with [ Tnil ⇒ dy  _ ⇒ dn ] 463  Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn  Tcons t2 ts2 ⇒ 464 match type_eq_dec t1 t2 with [ inl _ ⇒ 465 match typelist_eq_dec ts1 ts2 with [ inl _ ⇒ dy  _ ⇒ dn ]  _ ⇒ dn ] ] 466 ] 467 and fieldlist_eq_dec (fl1,fl2:fieldlist) : (fl1 = fl2) + (fl1 ≠ fl2) ≝ 468 match fl1 with 469 [ Fnil ⇒ match fl2 with [ Fnil ⇒ dy  _ ⇒ dn ] 470  Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn  Fcons i2 t2 fs2 ⇒ 471 match ident_eq i1 i2 with [ inl _ ⇒ 472 match type_eq_dec t1 t2 with [ inl _ ⇒ 473 match fieldlist_eq_dec fs1 fs2 with [ inl _ ⇒ dy  _ ⇒ dn ] 474  _ ⇒ dn ]  _ ⇒ dn ] ] 475 ]. 476 (* A poor man's clear, otherwise automation picks up recursive calls without 477 checking that the argument is smaller. *) 478 ngeneralize in type_eq_dec; 479 ngeneralize in typelist_eq_dec; 480 ngeneralize in fieldlist_eq_dec; #avoid1 avoid2 avoid3 avoid4 avoid5 avoid6; 481 ndestruct; //; @; #H; ndestruct; 482 ##[ nelim c8; /2/ 483 ## nelim c6; /2/ 484 ## nelim c4; /2/ 485 ## nelim c4; /2/ 486 ## nelim c8; /2/ 487 ## nelim c6; /2/ 488 ## nelim c8; /2/ 489 ## nelim c6; /2/ 490 ## nelim c8; /2/ 491 ## nelim c6; /2/ 492 ## nelim c8; /2/ 493 ## nelim c6; /2/ 494 ## nelim c4; /2/ 495 ## nelim c8; /2/ 496 ## nelim c6; /2/ 497 ## nelim c12; /2/ 498 ## nelim c10; /2/ 499 ## nelim c8; /2/ 500 ##] nqed. 501 502 ndefinition are_equal : ∀A:Type. (∀x,y:A.(x=y)+(x≠y)) → ∀x,y:A. res (x=y) ≝ 503 λA,dec,x,y. 504 match dec … x y with 505 [ inl p ⇒ OK ? p 506  inr _ ⇒ Error ? 507 ]. 508 509 nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝ 510 match k with 511 [ Kstop ⇒ dy 512  Kcall _ _ _ _ ⇒ dy 513  _ ⇒ dn 514 ]. nwhd; //; @; #H; nelim H; nqed. 515 379 516 nlet rec exec_step (ge:genv) (st:state) on st : res (Σr:trace × state. step ge st (\fst r) (\snd r)) ≝ 380 517 match st with … … 386 523 m' ← opt_to_res ? (store_value_of_type (typeof a1) m loc ofs v2);: 387 524 OK ? 〈E0, State f Sskip k e m'〉) 525  Scall lhs a al ⇒ Some ? ( 526 vf ← exec_expr ge e m a;: 527 vargs ← exec_exprlist ge e m al;: 528 fd ← opt_to_res ? (find_funct Genv ? ge vf);: 529 p ← are_equal ? type_eq_dec (type_of_fundef fd) (typeof a);: 530 k' ← match lhs with 531 [ None ⇒ OK ? (Kcall (None ?) f e k) 532  Some lhs' ⇒ 533 locofs ← exec_lvalue ge e m lhs';: 534 OK ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k) 535 ];: 536 OK ? 〈E0, Callstate fd vargs k' m〉) 537  Ssequence s1 s2 ⇒ Some ? (OK ? 〈E0, State f s1 (Kseq s2 k) e m〉) 538  Sskip ⇒ 539 match k with 540 [ Kseq s k' ⇒ Some ? (OK ? 〈E0, State f s k' e m〉) 541  Kstop ⇒ 542 match fn_return f with 543 [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉) 544  _ ⇒ Some ? (Error ?) 545 ] 546  Kcall _ _ _ _ ⇒ 547 match fn_return f with 548 [ Tvoid ⇒ Some ? (OK ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉) 549  _ ⇒ Some ? (Error ?) 550 ] 551  _ ⇒ Some ? (Error ?) (* TODO more *) 552 ] 388 553  Sreturn a_opt ⇒ 389 554 match a_opt with … … 410 575  _ ⇒ Some ? (Error ?) 411 576 ]. nwhd; //; 412 ##[ napply sig_bind2_OK; #loc ofs Hlval; 577 ##[ nrewrite > c7; napply step_skip_call; //; napply c8; 578 ## nrewrite > c11; napply step_skip_call; //; napply c12; 579 ## napply sig_bind2_OK; #loc ofs Hlval; 413 580 napply sig_bind_OK; #v2 ev2 Hv2; 414 581 napply opt_bind_OK; #m' em'; 415 582 nwhd; napply (step_assign … Hlval Hv2 em'); 583 ## napply sig_bind_OK; #vf evf Hvf; 584 napply sig_bind_OK; #vargs evargs Hvargs; 585 napply opt_bind_OK; #fd efd; 586 napply bind_OK; #ety ety'; 587 ncases c6; nwhd; 588 ##[ napply (step_call_none … Hvf Hvargs efd ety); 589 ## #lhs'; nrewrite > (bind_assoc_r …); 590 napply sig_bind_OK; #locofs; ncases locofs; #loc ofs elocofs Hlocofs; 591 nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety); 592 ##] 416 593 ## napply step_return_0; napply c9; 417 594 ## napply sig_bind_OK; #u eu Hnotvoid; … … 436 613 nwhd; napply (initial_state_intro … eb ef); 437 614 nqed. 615 616 ndefinition is_final_state : ∀st:state. (∃r. final_state st r) + (¬∃r. final_state st r). 617 #st; nelim st; 618 ##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct; 619 ## #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct; 620 ## #v k m; ncases k; 621 ##[ ncases v; 622 ##[ ##2: #i; @1; @ i; //; 623 ## ##1: @2; @; *; #r H; ninversion H; #i m e; ndestruct; 624 ## #f; @2; @; *; #r H; ninversion H; #i m e; ndestruct; 625 ## #b of; @2; @; *; #r H; ninversion H; #i m e; ndestruct; 626 ##] 627 ## #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct; 628 ## ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct; 629 ## ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct; 630 ## #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct; 631 ##] 632 ##] nqed. 633 634 nlet rec exec_steps (n:nat) (ge:genv) (s:state) : 635 res (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝ 636 match is_final_state s with 637 [ inl _ ⇒ Some ? (OK ? 〈E0, s〉) 638  inr _ ⇒ 639 match n with 640 [ O ⇒ Some ? (OK ? 〈E0, s〉) 641  S n' ⇒ Some ? ( 642 〈t,s'〉 ← exec_step ge s;: 643 〈t',s''〉 ← exec_steps n' ge s';: 644 OK ? 〈t ⧺ t',s''〉) 645 ] 646 ]. nwhd; /2/; 647 napply sig_bind2_OK; #t s' H1; 648 napply sig_bind2_OK; #t' s'' IH; 649 nwhd; napply (star_step … IH); //; 650 nqed.
Note: See TracChangeset
for help on using the changeset viewer.