Changeset 2395 for src/common/FrontEndOps.ma
 Timestamp:
 Oct 12, 2012, 3:33:53 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/FrontEndOps.ma
r2177 r2395 19 19 20 20 include "common/Values.ma". 21 include "common/FrontEndMem.ma". 21 22 22 23 inductive constant : typ → Type[0] ≝ … … 404 405  _ ⇒ None ? ]. 405 406 406 definition ev_cmpp ≝ λ c: comparison. λv1,v2: val.407 definition ev_cmpp ≝ λm. λc: comparison. λv1,v2: val. 407 408 match v1 with 408 409 [ Vptr ptr1 ⇒ match v2 with 409 410 [ Vptr ptr2 ⇒ 410 if eq_block (pblock ptr1) (pblock ptr2) 411 then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2))) 412 else ev_cmp_mismatch c 411 if eq_block (pblock ptr1) (pblock ptr2) then 412 if (valid_pointer m ptr1 ∨ end_pointer m ptr1) ∧ 413 (valid_pointer m ptr2 ∨ end_pointer m ptr2) 414 then Some ? (FE_of_bool (cmp_offset c (poff ptr1) (poff ptr2))) 415 else None ? 416 else 417 if valid_pointer m ptr1 ∧ 418 valid_pointer m ptr2 419 then ev_cmp_mismatch c 420 else None ? 413 421  Vnull ⇒ ev_cmp_mismatch c 414 422  _ ⇒ None ? ] … … 437 445  _ ⇒ None ? ]. 438 446 439 definition eval_binop : ∀t1,t2,t'. binary_operation t1 t2 t' → val → val → option val ≝440 λ t1,t2,t',op.447 definition eval_binop : mem → ∀t1,t2,t'. binary_operation t1 t2 t' → val → val → option val ≝ 448 λm,t1,t2,t',op. 441 449 match op with 442 450 [ Oadd _ _ ⇒ ev_add … … 463 471  Osubpi _ ⇒ ev_subpi 464 472  Osubpp sz ⇒ ev_subpp sz 465  Ocmpp _ c ⇒ ev_cmpp c466 ]. 467 468 lemma eval_binop_typ_correct : ∀ t1,t2,t',op,v1,v2,v'.473  Ocmpp _ c ⇒ ev_cmpp m c 474 ]. 475 476 lemma eval_binop_typ_correct : ∀m,t1,t2,t',op,v1,v2,v'. 469 477 val_typ v1 t1 → val_typ v2 t2 → 470 eval_binop t1 t2 t' op v1 v2 = Some ? v' →478 eval_binop m t1 t2 t' op v1 v2 = Some ? v' → 471 479 val_typ v' t'. 472 # t1x #t2x #tx' *480 #m #t1x #t2x #tx' * 473 481 [ 1,2,3,8,9,10: 474 482 #sz #sg #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) #i1 @(elim_val_typ … V2) #i2 … … 501 509 whd in ⊢ (??%? → ?); [ 2: cases (eq_block ??) whd in ⊢ (??%? → ?);  ] #E destruct // 502 510  #sg' #c #v1 #v2 #v' #V1 #V2 @(elim_val_typ … V1) % [ 2: #b1 #o1 ] @(elim_val_typ … V2) % [ 2,4: #b2 #o2 ] 503 whd in ⊢ (??%? → ?); [ cases ( eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct //511 whd in ⊢ (??%? → ?); [ cases (andb ??) cases (andb ??) cases (eq_block ??) cases (cmp_offset ???) ] cases c whd in ⊢ (??%? → ?); #E destruct // 504 512 ] qed. 505 513
Note: See TracChangeset
for help on using the changeset viewer.