1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
|
$ifndef _ARITH
$define _ARITH
$include <flow.sail>
// ***** Addition *****
val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm.
(atom('n), atom('m)) -> atom('n + 'm)
val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int
overload operator + = {add_atom, add_int}
// ***** Subtraction *****
val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm.
(atom('n), atom('m)) -> atom('n - 'm)
val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int
overload operator - = {sub_atom, sub_int}
// ***** Negation *****
val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. atom('n) -> atom(- 'n)
val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : int -> int
overload negate = {negate_atom, negate_int}
// ***** Multiplication *****
val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm.
(atom('n), atom('m)) -> atom('n * 'm)
val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int
overload operator * = {mult_atom, mult_int}
val "print_int" : (string, int) -> unit
val "prerr_int" : (string, int) -> unit
// ***** Integer shifts *****
val shl_int = "shl_int" : (int, int) -> int
val shr_int = "shr_int" : (int, int) -> int
// ***** div and mod *****
val div_int = {
smt: "div",
ocaml: "quotient",
lem: "integerDiv",
c: "div_int",
coq: "Z.quot"
} : (int, int) -> int
overload operator / = {div_int}
val mod_int = {
smt: "mod",
ocaml: "modulus",
lem: "integerMod",
c: "mod_int",
coq: "Z.rem"
} : (int, int) -> int
overload operator % = {mod_int}
val abs_int = {
smt : "abs",
ocaml: "abs_int",
lem: "abs_int",
coq: "Z.abs"
} : (int, int) -> int
$endif
|
