diff options
Diffstat (limited to 'lib/arith.sail')
| -rw-r--r-- | lib/arith.sail | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index 20231de1..a1eef9f0 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -5,19 +5,19 @@ $include <flow.sail> // ***** Addition ***** -val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm. +val add_atom = {ocaml: "add_int", interpreter: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm. (int('n), int('m)) -> int('n + 'm) -val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int +val add_int = {ocaml: "add_int", interpreter: "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. +val sub_atom = {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm. (int('n), int('m)) -> int('n - 'm) -val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int +val sub_int = {ocaml: "sub_int", interpreter: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int overload operator - = {sub_atom, sub_int} @@ -29,18 +29,18 @@ val sub_nat = { // ***** Negation ***** -val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. int('n) -> int(- 'n) +val negate_atom = {ocaml: "negate", interpreter: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. int('n) -> int(- 'n) -val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : int -> int +val negate_int = {ocaml: "negate", interpreter: "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. +val mult_atom = {ocaml: "mult", interpreter: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm. (int('n), int('m)) -> int('n * 'm) -val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int +val mult_int = {ocaml: "mult", interpreter: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int overload operator * = {mult_atom, mult_int} @@ -81,6 +81,7 @@ overload shr_int = {_shr32, _shr_int} val div_int = { smt: "div", ocaml: "quotient", + interpreter: "quotient", lem: "integerDiv", c: "tdiv_int", coq: "Z.quot" @@ -91,6 +92,7 @@ overload operator / = {div_int} val mod_int = { smt: "mod", ocaml: "modulus", + interpreter: "modulus", lem: "integerMod", c: "tmod_int", coq: "Z.rem" @@ -101,6 +103,7 @@ overload operator % = {mod_int} val abs_int = { smt : "abs", ocaml: "abs_int", + interpreter: "abs_int", lem: "abs_int", c: "abs_int", coq: "Z.abs" |