Changeset 14 for C-semantics/Integers.ma


Ignore:
Timestamp:
Jul 21, 2010, 3:08:58 PM (9 years ago)
Author:
campbell
Message:

Make Integers.ma respect bounds again, and reenable the rest of Mem.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Integers.ma

    r10 r14  
    8888  integer (type [Z]) plus a proof that it is in the range 0 (included) to
    8989  [modulus] (excluded. *)
    90 
    91 nrecord int: Type ≝ { intval: Z ; intrange: True (*(0 ≤ intval) ∧ intval < modulus*) }.
     90(* XXX: hack to prevent normalization of huge proof term. *)
     91ninductive inrange : Z → Prop ≝
     92| inrg_mod : ∀i:Z. inrange (i \mod modulus)
     93| inrg_pf : ∀i:Z. (0 ≤ i) ∧ i < modulus → inrange i.
     94ninductive int: Type ≝
     95| mk_int: ∀i:Z. inrange i → int.
     96(*
     97nrecord int: Type ≝ { intval: Z ; intrange: (0 ≤ intval) ∧ intval < modulus }.
     98*)
     99ndefinition intval: int → Z ≝ λi.match i with [ mk_int x _ ⇒ x ].
     100ndefinition intrange: ∀i:int. 0 ≤ (intval i) ∧ (intval i) < modulus.
     101#i;ncases i;
     102#x H; ncases H;
     103##[ #x'; napply modZ_lt_mod; //;
     104##| //;
     105##] nqed.
    92106
    93107(* The [unsigned] and [signed] functions return the Coq integer corresponding
     
    104118(* Conversely, [repr] takes a Coq integer and returns the corresponding
    105119  machine integer.  The argument is treated modulo [modulus]. *)
    106 (* TODO: prove *)
    107120(*naxiom repr : Z → int.*)
    108 
    109 (*naxiom repr_ax : ∀x. 0 ≤ x \mod modulus ∧ x \mod modulus < modulus.*)
    110 
     121(*
    111122ndefinition repr : Z → int := λx.
    112   mk_int x I (*x \mod modulus) ?*) (*Z_mod_lt x modulus modulus_pos*).
    113 (*napply repr_ax.
    114 nqed.*)
     123  mk_int (x \mod modulus) (modZ_lt_mod x modulus modulus_pos).
     124*)
     125ndefinition repr : Z → int ≝ λx. mk_int (x \mod modulus) (inrg_mod x).
    115126
    116127ndefinition zero := repr 0.
     
    145156ndefinition neg : int → int ≝ λx. repr (- unsigned x).
    146157
    147 naxiom zero_ext : Z → int → int.
    148 naxiom sign_ext : Z → int → int.
    149 (*
    150 Definition zero_ext (n: Z) (x: int) : int :=
    151   repr (Zmod (unsigned x) (two_p n)).
    152 Definition sign_ext (n: Z) (x: int) : int :=
    153   repr (let p := two_p n in
    154         let y := Zmod (unsigned x) p in
    155         if zlt y (two_p (n-1)) then y else y - p).
    156 *)
     158ndefinition zero_ext : Z → int → int ≝
     159λn,x. repr (modZ (unsigned x) (two_p n)).
     160ndefinition sign_ext : Z → int → int ≝
     161λn,x. repr (let p ≝ two_p n in
     162        let y ≝ modZ (unsigned x) p in
     163        if Zltb y (two_p (n-1)) then y else y - p).
     164
    157165ndefinition add ≝ λx,y: int.
    158166  repr (unsigned x + unsigned y).
     
    254262  (standard behaviour for arithmetic right shift) and
    255263  [shrx] rounds towards zero. *)
    256 naxiom two_p : Z → Z.
     264
    257265ndefinition shr : int → int → int ≝ λx,y.
    258266  repr (signed x / two_p (unsigned y)).
Note: See TracChangeset for help on using the changeset viewer.