source: src/common/IntValue.ma @ 1077

Last change on this file since 1077 was 1059, checked in by mulligan, 9 years ago

work from today, bit of a mess at the moment

File size: 3.3 KB
Line 
1(* include "arithmetics/Z.ma". *)
2include "arithmetics/exp.ma".
3include "basics/list.ma".
4include "common/AST.ma".
5include "common/Order.ma".
6
7definition bvint ≝ λsize. BitVector (bitsize_of_intsize size).
8
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 TracBrowser for help on using the repository browser.