Changeset 9 for C-semantics/Integers.ma

Timestamp:

Jun 21, 2010, 4:22:09 PM (11 years ago)

Author:

campbell

Message:

Enough of an executable semantics to execute a not-quite-trivial program,
plus a patch for compcert to convert C to a matita definition.

File:

• C-semantics/Integers.ma (modified) (2 diffs)

C-semantics/Integers.ma

@@ -94 +94 @@
   [modulus] (excluded. *)
 
-nrecord int: Type ≝ { intval: Z; intrange: (0 ≤ intval) ∧ intval < modulus }.
+nrecord int: Type ≝ { intval: Z ; intrange: True (*(0 ≤ intval) ∧ intval < modulus*) }.
 
 (* The [unsigned] and [signed] functions return the Coq integer corresponding
@@ -110 +110 @@
   machine integer.  The argument is treated modulo [modulus]. *)
 (* TODO: prove *)
-naxiom repr_ax : ∀x. 0 ≤ x \mod modulus ∧ x \mod modulus < modulus.
+(*naxiom repr : Z → int.*)
+
+(*naxiom repr_ax : ∀x. 0 ≤ x \mod modulus ∧ x \mod modulus < modulus.*)
 
 ndefinition repr : Z → int := λx.
-  mk_int (x \mod modulus) ? (*Z_mod_lt x modulus modulus_pos*).
-napply repr_ax.
-nqed.
+  mk_int x I (*x \mod modulus) ?*) (*Z_mod_lt x modulus modulus_pos*).
+(*napply repr_ax.
+nqed.*)
 
 ndefinition zero := repr 0.