diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/arith.sail | 14 | ||||
| -rw-r--r-- | lib/flow.sail | 12 | ||||
| -rw-r--r-- | lib/sail.c | 18 | ||||
| -rw-r--r-- | lib/sail.h | 3 |
4 files changed, 41 insertions, 6 deletions
diff --git a/lib/arith.sail b/lib/arith.sail index e5d2d6ea..61a1ff76 100644 --- a/lib/arith.sail +++ b/lib/arith.sail @@ -6,7 +6,7 @@ $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) + (int('n), int('m)) -> int('n + 'm) val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int @@ -15,15 +15,21 @@ 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) + (int('n), int('m)) -> int('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} +val sub_nat = { + ocaml: "(fun (x,y) -> let n = sub_int (x,y) in if Big_int.less_equal n Big_int.zero then Big_int.zero else n)", + lem: "integerMinus", + _: "sub_nat" +} : (nat, nat) -> nat + // ***** Negation ***** -val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. atom('n) -> atom(- 'n) +val negate_atom = {ocaml: "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 @@ -32,7 +38,7 @@ 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) + (int('n), int('m)) -> int('n * 'm) val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int diff --git a/lib/flow.sail b/lib/flow.sail index c16763ee..5ee9a74a 100644 --- a/lib/flow.sail +++ b/lib/flow.sail @@ -1,8 +1,18 @@ $ifndef _FLOW $define _FLOW +/* + +This file contains the basic definitions for equality and comparison +that is required for flow typing to work correctly. It should +therefore be included in just about every Sail specification. + +*/ + val eq_unit : (unit, unit) -> bool +val "eq_bit" : (bit, bit) -> bool + function eq_unit(_, _) = true val not_bool = {coq: "negb", _: "not"} : bool -> bool @@ -49,7 +59,7 @@ val gteq_int = {coq: "Z.geb", _:"gteq"} : (int, int) -> bool val lt_int = {coq: "Z.ltb", _:"lt"} : (int, int) -> bool val gt_int = {coq: "Z.gtb", _:"gt"} : (int, int) -> bool -overload operator == = {eq_atom, eq_range, eq_int, eq_bool, eq_unit} +overload operator == = {eq_atom, eq_range, eq_int, eq_bit, eq_bool, eq_unit} overload operator != = {neq_atom, neq_range, neq_int, neq_bool} overload operator | = {or_bool} overload operator & = {and_bool} @@ -301,6 +301,14 @@ void sub_int(sail_int *rop, const sail_int op1, const sail_int op2) mpz_sub(*rop, op1, op2); } +void sub_nat(sail_int *rop, const sail_int op1, const sail_int op2) +{ + mpz_sub(*rop, op1, op2); + if (mpz_cmp_ui(*rop, 0) < 0ul) { + mpz_set_ui(*rop, 0ul); + } +} + inline void mult_int(sail_int *rop, const sail_int op1, const sail_int op2) { @@ -361,7 +369,15 @@ void abs_int(sail_int *rop, const sail_int op) mpz_abs(*rop, op); } -void pow2(sail_int *rop, const sail_int exp) { +inline +void pow_int(sail_int *rop, const sail_int op1, const sail_int op2) +{ + uint64_t n = mpz_get_ui(op2); + mpz_pow_ui(*rop, op1, n); +} + +void pow2(sail_int *rop, const sail_int exp) +{ /* Assume exponent is never more than 2^64... */ uint64_t exp_ui = mpz_get_ui(exp); mpz_t base; @@ -150,6 +150,7 @@ SAIL_INT_FUNCTION(undefined_range, sail_int, const sail_int, const sail_int); */ SAIL_INT_FUNCTION(add_int, sail_int, const sail_int, const sail_int); SAIL_INT_FUNCTION(sub_int, sail_int, const sail_int, const sail_int); +SAIL_INT_FUNCTION(sub_nat, sail_int, const sail_int, const sail_int); SAIL_INT_FUNCTION(mult_int, sail_int, const sail_int, const sail_int); SAIL_INT_FUNCTION(tdiv_int, sail_int, const sail_int, const sail_int); SAIL_INT_FUNCTION(tmod_int, sail_int, const sail_int, const sail_int); @@ -162,6 +163,8 @@ SAIL_INT_FUNCTION(min_int, sail_int, const sail_int, const sail_int); SAIL_INT_FUNCTION(neg_int, sail_int, const sail_int); SAIL_INT_FUNCTION(abs_int, sail_int, const sail_int); +SAIL_INT_FUNCTION(pow_int, sail_int, const sail_int, const sail_int); + SAIL_INT_FUNCTION(pow2, sail_int, const sail_int); /* ***** Sail bitvectors ***** */ |