Changeset 4


Ignore:
Timestamp:
Jun 2, 2010, 7:11:14 PM (7 years ago)
Author:
campbell
Message:

Some experimental work on executable Clight semantics.

Location:
C-semantics
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Csyntax.ma

    r3 r4  
    278278  match t return λ_.Z (* XXX appears to infer nat otherwise *) with
    279279  [ 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 ]
    282282  | Tpointer _ ⇒ 4
    283283  | Tarray t' n ⇒ alignof t'
     
    363363  match t return λ_.Z with
    364364  [ 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 ]
    367367  | Tpointer _ ⇒ 4
    368368  | Tarray t' n ⇒ sizeof t' * Zmax 1 n
  • C-semantics/Errors.ma

    r3 r4  
    5858  | Error (*msg*) => Error ? (*msg*)
    5959  ].
     60
     61(* Not sure what level to use *)
     62notation "ident v ← e;: e'" right associative with precedence 40 for @{'bind ${e} (λ${ident v}.${e'})}.
     63interpretation "error monad bind" 'bind e f = (bind ? ? e f).
     64notation "〈ident v1, ident v2〉 ← e;: e'" right associative with precedence 40 for @{'bind2 ${e} (λ${ident v1}.λ${ident v2}.${e'})}.
     65interpretation "error monad pair bind" 'bind2 e f = (bind2 ??? e f).
     66(*interpretation "error monad ret" 'ret e = (ret ? e).
     67notation "'ret' e" non associative with precedence 45 for @{'ret ${e}}.*)
     68
    6069(*
    6170(** The [do] notation, inspired by Haskell's, keeps the code readable. *)
  • C-semantics/Integers.ma

    r3 r4  
    506506  rewrite half_modulus_modulus. generalize half_modulus_pos. omega. 
    507507Qed.
    508 
     508*)
     509naxiom one_not_zero: one ≠ zero.
     510(*
    509511Theorem one_not_zero: one <> zero.
    510512Proof.
     
    520522  generalize wordsize_pos wordsize_max_unsigned; unfold max_unsigned; omega.
    521523Qed.
    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
     527ntheorem 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
     534ntheorem 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
     542ntheorem 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);
     545nqed.
     546
     547ntheorem 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');
     550nqed.
     551(*
    552552(** ** Modulo arithmetic *)
    553553
Note: See TracChangeset for help on using the changeset viewer.