Changeset 9 for C-semantics/Integers.ma


Ignore:
Timestamp:
Jun 21, 2010, 4:22:09 PM (10 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:
1 edited

Legend:

Unmodified
Added
Removed
  • C-semantics/Integers.ma

    r4 r9  
    9494  [modulus] (excluded. *)
    9595
    96 nrecord int: Type ≝ { intval: Z; intrange: (0 ≤ intval) ∧ intval < modulus }.
     96nrecord int: Type ≝ { intval: Z ; intrange: True (*(0 ≤ intval) ∧ intval < modulus*) }.
    9797
    9898(* The [unsigned] and [signed] functions return the Coq integer corresponding
     
    110110  machine integer.  The argument is treated modulo [modulus]. *)
    111111(* TODO: prove *)
    112 naxiom repr_ax : ∀x. 0 ≤ x \mod modulus ∧ x \mod modulus < modulus.
     112(*naxiom repr : Z → int.*)
     113
     114(*naxiom repr_ax : ∀x. 0 ≤ x \mod modulus ∧ x \mod modulus < modulus.*)
    113115
    114116ndefinition repr : Z → int := λx.
    115   mk_int (x \mod modulus) ? (*Z_mod_lt x modulus modulus_pos*).
    116 napply repr_ax.
    117 nqed.
     117  mk_int x I (*x \mod modulus) ?*) (*Z_mod_lt x modulus modulus_pos*).
     118(*napply repr_ax.
     119nqed.*)
    118120
    119121ndefinition zero := repr 0.
Note: See TracChangeset for help on using the changeset viewer.