Ignore:
Timestamp:
Jul 6, 2011, 6:09:39 PM (8 years ago)
Author:
mulligan
Message:

work from today, bit of a mess at the moment

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IntValue.ma

    r1057 r1059  
    22include "arithmetics/exp.ma".
    33include "basics/list.ma".
     4include "common/AST.ma".
    45include "common/Order.ma".
    56
    6 definition big_int_size ≝ nat.
    7 axiom big_int: big_int_size → Type[0].
    8 axiom big_int_int_repr: Type[0].
     7definition bvint ≝ λsize. BitVector (bitsize_of_intsize size).
    98
    10 axiom compare: ∀size: big_int_size. big_int size → big_int size → order.
    11 axiom zero: ∀size: big_int_size. big_int size.
    12 axiom one: ∀size: big_int_size. big_int size.
    13 axiom to_signed_int_repr: ∀size: big_int_size. big_int size → big_int_int_repr.
    14 axiom to_unsigned_int_repr: ∀size: big_int_size. big_int size → big_int_int_repr.
    15 axiom succ: ∀size: big_int_size. big_int size → big_int size.
    16 axiom pred: ∀size: big_int_size. big_int size → big_int size.
    17 axiom add: ∀size: big_int_size. big_int size → big_int size → big_int size.
    18 axiom add_of: ∀size: big_int_size. big_int size → big_int size → bool.
    19 axiom sub: ∀size: big_int_size. big_int size → big_int size → big_int size.
    20 axiom sub_uf: ∀size: big_int_size. big_int size → big_int size → bool.
    21 axiom mul: ∀size: big_int_size. big_int size → big_int size → big_int size.
    22 axiom div: ∀size: big_int_size. big_int size → big_int size → big_int size.
    23 axiom divu: ∀size: big_int_size. big_int size → big_int size → big_int size.
    24 axiom modulo: ∀size: big_int_size. big_int size → big_int size → big_int size.
    25 axiom modulou: ∀size: big_int_size. big_int size → big_int size → big_int size.
    26 axiom eq: ∀size: big_int_size. big_int size → big_int size → bool.
    27 axiom neq: ∀size: big_int_size. big_int size → big_int size → bool.
    28 axiom lt: ∀size: big_int_size. big_int size → big_int size → bool.
    29 axiom ltu: ∀size: big_int_size. big_int size → big_int size → bool.
    30 axiom le: ∀size: big_int_size. big_int size → big_int size → bool.
    31 axiom leu: ∀size: big_int_size. big_int size → big_int size → bool.
    32 axiom gt: ∀size: big_int_size. big_int size → big_int size → bool.
    33 axiom gtu: ∀size: big_int_size. big_int size → big_int size → bool.
    34 axiom ge: ∀size: big_int_size. big_int size → big_int size → bool.
    35 axiom geu: ∀size: big_int_size. big_int size → big_int size → bool.
    36 axiom neg: ∀size: big_int_size. big_int size → big_int size.
    37 axiom lognot: ∀size: big_int_size. big_int size → big_int size.
    38 axiom logand: ∀size: big_int_size. big_int size → big_int size → big_int size.
    39 axiom logor: ∀size: big_int_size. big_int size → big_int size → big_int size.
    40 axiom logxor: ∀size: big_int_size. big_int size → big_int size → big_int size.
    41 axiom shl: ∀size: big_int_size. big_int size → big_int size → big_int size.
    42 axiom shr: ∀size: big_int_size. big_int size → big_int size → big_int size.
    43 axiom shrl: ∀size: big_int_size. big_int size → big_int size → big_int size.
    44 axiom max: ∀size: big_int_size. big_int size → big_int size → big_int size.
    45 axiom maxu: ∀size: big_int_size. big_int size → big_int size → big_int size.
    46 axiom min: ∀size: big_int_size. big_int size → big_int size → big_int size.
    47 axiom minu: ∀size: big_int_size. big_int size → big_int size → big_int size.
    48 axiom cast: ∀size: big_int_size. big_int_int_repr → big_int size.
    49 axiom of_int: ∀size: big_int_size. nat → big_int size. (*dpm: replace when Z is added to stdlib *)
    50 axiom to_int: ∀size: big_int_size. big_int size → nat. (*dpm: """" *)
    51 axiom zero_ext: ∀size: big_int_size. nat → big_int size → big_int size. (* nat here correct *)
    52 axiom sign_ext: ∀size: big_int_size. nat → big_int size → big_int size. (* nat here correct *)
    53 axiom break: ∀size: big_int_size. big_int size → nat → list (big_int size).
    54 axiom merge: ∀size: big_int_size. list (big_int size) → big_int size.
     9definition bitsize_of_intsize: intsize → nat ≝
     10  λsize.
     11    S (match size with [ I8 ⇒ 7 | I16 ⇒ 15 | I32 ⇒ 31]).
     12
     13definition of_int ≝
     14  λsize.
     15  λn.
     16    bitvector_of_nat (bitsize_of_intsize size) n.
     17
     18axiom compare: ∀size: intsize. bvint size → bvint size → order.
     19axiom zero: ∀size: intsize. bvint size.
     20axiom one: ∀size: intsize. bvint size.
     21axiom to_signed_int_repr: ∀size: intsize. bvint size → bvint_int_repr.
     22axiom to_unsigned_int_repr: ∀size: intsize. bvint size → bvint_int_repr.
     23axiom succ: ∀size: intsize. bvint size → bvint size.
     24axiom pred: ∀size: intsize. bvint size → bvint size.
     25axiom add: ∀size: intsize. bvint size → bvint size → bvint size.
     26axiom add_of: ∀size: intsize. bvint size → bvint size → bool.
     27axiom sub: ∀size: intsize. bvint size → bvint size → bvint size.
     28axiom sub_uf: ∀size: intsize. bvint size → bvint size → bool.
     29axiom mul: ∀size: intsize. bvint size → bvint size → bvint size.
     30axiom div: ∀size: intsize. bvint size → bvint size → bvint size.
     31axiom divu: ∀size: intsize. bvint size → bvint size → bvint size.
     32axiom modulo: ∀size: intsize. bvint size → bvint size → bvint size.
     33axiom modulou: ∀size: intsize. bvint size → bvint size → bvint size.
     34axiom eq: ∀size: intsize. bvint size → bvint size → bool.
     35axiom neq: ∀size: intsize. bvint size → bvint size → bool.
     36axiom lt: ∀size: intsize. bvint size → bvint size → bool.
     37axiom ltu: ∀size: intsize. bvint size → bvint size → bool.
     38axiom le: ∀size: intsize. bvint size → bvint size → bool.
     39axiom leu: ∀size: intsize. bvint size → bvint size → bool.
     40axiom gt: ∀size: intsize. bvint size → bvint size → bool.
     41axiom gtu: ∀size: intsize. bvint size → bvint size → bool.
     42axiom ge: ∀size: intsize. bvint size → bvint size → bool.
     43axiom geu: ∀size: intsize. bvint size → bvint size → bool.
     44axiom neg: ∀size: intsize. bvint size → bvint size.
     45axiom lognot: ∀size: intsize. bvint size → bvint size.
     46axiom logand: ∀size: intsize. bvint size → bvint size → bvint size.
     47axiom logor: ∀size: intsize. bvint size → bvint size → bvint size.
     48axiom logxor: ∀size: intsize. bvint size → bvint size → bvint size.
     49axiom shl: ∀size: intsize. bvint size → bvint size → bvint size.
     50axiom shr: ∀size: intsize. bvint size → bvint size → bvint size.
     51axiom shrl: ∀size: intsize. bvint size → bvint size → bvint size.
     52axiom max: ∀size: intsize. bvint size → bvint size → bvint size.
     53axiom maxu: ∀size: intsize. bvint size → bvint size → bvint size.
     54axiom min: ∀size: intsize. bvint size → bvint size → bvint size.
     55axiom minu: ∀size: intsize. bvint size → bvint size → bvint size.
     56axiom cast: ∀size: intsize. bvint_int_repr → bvint size.
     57axiom to_int: ∀size: intsize. bvint size → nat. (*dpm: """" *)
     58axiom zero_ext: ∀size: intsize. nat → bvint size → bvint size. (* nat here correct *)
     59axiom sign_ext: ∀size: intsize. nat → bvint size → bvint size. (* nat here correct *)
     60axiom break: ∀size: intsize. bvint size → nat → list (bvint size).
     61axiom merge: ∀size: intsize. list (bvint size) → bvint size.
Note: See TracChangeset for help on using the changeset viewer.