Changeset 14 for Csemantics/Integers.ma
 Timestamp:
 Jul 21, 2010, 3:08:58 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Integers.ma
r10 r14 88 88 integer (type [Z]) plus a proof that it is in the range 0 (included) to 89 89 [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. *) 91 ninductive inrange : Z → Prop ≝ 92  inrg_mod : ∀i:Z. inrange (i \mod modulus) 93  inrg_pf : ∀i:Z. (0 ≤ i) ∧ i < modulus → inrange i. 94 ninductive int: Type ≝ 95  mk_int: ∀i:Z. inrange i → int. 96 (* 97 nrecord int: Type ≝ { intval: Z ; intrange: (0 ≤ intval) ∧ intval < modulus }. 98 *) 99 ndefinition intval: int → Z ≝ λi.match i with [ mk_int x _ ⇒ x ]. 100 ndefinition 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. 92 106 93 107 (* The [unsigned] and [signed] functions return the Coq integer corresponding … … 104 118 (* Conversely, [repr] takes a Coq integer and returns the corresponding 105 119 machine integer. The argument is treated modulo [modulus]. *) 106 (* TODO: prove *)107 120 (*naxiom repr : Z → int.*) 108 109 (*naxiom repr_ax : ∀x. 0 ≤ x \mod modulus ∧ x \mod modulus < modulus.*) 110 121 (* 111 122 ndefinition repr : Z → int := λx. 112 mk_int x I (*x \mod modulus) ?*) (*Z_mod_lt x modulus modulus_pos*).113 (*napply repr_ax. 114 n qed.*)123 mk_int (x \mod modulus) (modZ_lt_mod x modulus modulus_pos). 124 *) 125 ndefinition repr : Z → int ≝ λx. mk_int (x \mod modulus) (inrg_mod x). 115 126 116 127 ndefinition zero := repr 0. … … 145 156 ndefinition neg : int → int ≝ λx. repr ( unsigned x). 146 157 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 (n1)) then y else y  p). 156 *) 158 ndefinition zero_ext : Z → int → int ≝ 159 λn,x. repr (modZ (unsigned x) (two_p n)). 160 ndefinition 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 (n1)) then y else y  p). 164 157 165 ndefinition add ≝ λx,y: int. 158 166 repr (unsigned x + unsigned y). … … 254 262 (standard behaviour for arithmetic right shift) and 255 263 [shrx] rounds towards zero. *) 256 naxiom two_p : Z → Z. 264 257 265 ndefinition shr : int → int → int ≝ λx,y. 258 266 repr (signed x / two_p (unsigned y)).
Note: See TracChangeset
for help on using the changeset viewer.