Changeset 4
 Timestamp:
 Jun 2, 2010, 7:11:14 PM (9 years ago)
 Location:
 Csemantics
 Files:

 1 added
 3 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Csyntax.ma
r3 r4 278 278 match t return λ_.Z (* XXX appears to infer nat otherwise *) with 279 279 [ Tvoid ⇒ 1 280  Tint sz _ ⇒ match sz with [ I8 ⇒ 1  I16 ⇒ 2  I32 ⇒ 4 ]281  Tfloat sz ⇒ match sz with [ F32 ⇒ 4  F64 ⇒ 8 ]280  Tint sz _ ⇒ match sz return λ_.Z with [ I8 ⇒ 1  I16 ⇒ 2  I32 ⇒ 4 ] 281  Tfloat sz ⇒ match sz return λ_.Z with [ F32 ⇒ 4  F64 ⇒ 8 ] 282 282  Tpointer _ ⇒ 4 283 283  Tarray t' n ⇒ alignof t' … … 363 363 match t return λ_.Z with 364 364 [ Tvoid ⇒ 1 365  Tint i _ ⇒ match i with [ I8 ⇒ 1  I16 ⇒ 2  I32 ⇒ 4 ]366  Tfloat f ⇒ match f with [ F32 ⇒ 4  F64 ⇒ 8 ]365  Tint i _ ⇒ match i return λ_.Z with [ I8 ⇒ 1  I16 ⇒ 2  I32 ⇒ 4 ] 366  Tfloat f ⇒ match f return λ_.Z with [ F32 ⇒ 4  F64 ⇒ 8 ] 367 367  Tpointer _ ⇒ 4 368 368  Tarray t' n ⇒ sizeof t' * Zmax 1 n 
Csemantics/Errors.ma
r3 r4 58 58  Error (*msg*) => Error ? (*msg*) 59 59 ]. 60 61 (* Not sure what level to use *) 62 notation "ident v ← e;: e'" right associative with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}. 63 interpretation "error monad bind" 'bind e f = (bind ? ? e f). 64 notation "〈ident v1, ident v2〉 ← e;: e'" right associative with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}. 65 interpretation "error monad pair bind" 'bind2 e f = (bind2 ??? e f). 66 (*interpretation "error monad ret" 'ret e = (ret ? e). 67 notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*) 68 60 69 (* 61 70 (** The [do] notation, inspired by Haskell's, keeps the code readable. *) 
Csemantics/Integers.ma
r3 r4 506 506 rewrite half_modulus_modulus. generalize half_modulus_pos. omega. 507 507 Qed. 508 508 *) 509 naxiom one_not_zero: one ≠ zero. 510 (* 509 511 Theorem one_not_zero: one <> zero. 510 512 Proof. … … 520 522 generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega. 521 523 Qed. 522 523 (** ** Properties of equality *) 524 525 Theorem eq_sym: 526 forall x y, eq x y = eq y x. 527 Proof. 528 intros; unfold eq. case (zeq (unsigned x) (unsigned y)); intro. 529 rewrite e. rewrite zeq_true. auto. 530 rewrite zeq_false. auto. auto. 531 Qed. 532 533 Theorem eq_spec: forall (x y: int), if eq x y then x = y else x <> y. 534 Proof. 535 intros; unfold eq. case (eq_dec x y); intro. 536 subst y. rewrite zeq_true. auto. 537 rewrite zeq_false. auto. 538 destruct x; destruct y. 539 simpl. red; intro. elim n. apply mkint_eq. auto. 540 Qed. 541 542 Theorem eq_true: forall x, eq x x = true. 543 Proof. 544 intros. generalize (eq_spec x x); case (eq x x); intros; congruence. 545 Qed. 546 547 Theorem eq_false: forall x y, x <> y > eq x y = false. 548 Proof. 549 intros. generalize (eq_spec x y); case (eq x y); intros; congruence. 550 Qed. 551 524 *) 525 (* * ** Properties of equality *) 526 527 ntheorem eq_sym: 528 ∀x,y. eq x y = eq y x. 529 #x y; nwhd in ⊢ (??%%); napply eqZb_elim; #H; 530 ##[ nrewrite > H; nrewrite > (eqZb_z_z …); // 531 ## nrewrite > (eqZb_false … (sym_neq … H)); // 532 ##] nqed. 533 534 ntheorem eq_spec: ∀x,y: int. if eq x y then x = y else (x ≠ y). 535 #x y; nwhd in ⊢ (??%??); nelim (eq_dec x y); #H; 536 ##[ nrewrite > H; nrewrite > (eqZb_z_z …); //; 537 ## nrewrite > (eqZb_false …); //; 538 nelim x in H ⊢ %; nelim y; 539 #x' Px y' Py H; nnormalize; napply (not_to_not … H); napply mk_int_eq; 540 ##] nqed. 541 542 ntheorem eq_true: ∀x. eq x x = true. 543 #x; nlapply (eq_spec x x); nelim (eq x x); //; 544 #H; nnormalize in H; napply False_ind; napply (absurd ? (refl ??) H); 545 nqed. 546 547 ntheorem eq_false: ∀x,y. x ≠ y → eq x y = false. 548 #x y; nlapply (eq_spec x y); nelim (eq x y); //; 549 #H H'; napply False_ind; napply (absurd ? H H'); 550 nqed. 551 (* 552 552 (** ** Modulo arithmetic *) 553 553
Note: See TracChangeset
for help on using the changeset viewer.