diff options
| author | Robert Norton | 2017-04-19 11:58:31 +0100 |
|---|---|---|
| committer | Robert Norton | 2017-04-20 11:06:05 +0100 |
| commit | 3ff6d30fe20aec5b690d61f5519d695f19094c52 (patch) | |
| tree | f94810e83505e312809fb312f08f0e7412db875c | |
| parent | a4b66c24311e2f9525936894f0fb7b191fceb9ee (diff) | |
add missing min and max functions, overriding built-in ocaml ones. Also neq_range.
| -rw-r--r-- | src/gen_lib/sail_values.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml index 73f943b5..600faddc 100644 --- a/src/gen_lib/sail_values.ml +++ b/src/gen_lib/sail_values.ml @@ -599,6 +599,8 @@ let add_big = arith_op add_big_int let add_signed_big = arith_op add_big_int let minus_big = arith_op sub_big_int let multiply_big = arith_op mult_big_int +let min_big = arith_op min_big_int +let max_big = arith_op max_big_int (* this implements truncation towards zero like C and unlike ocaml (consider r < 0) *) let quot_big (l, r) = let q = div_big_int (abs_big_int l) (abs_big_int r) in @@ -640,6 +642,8 @@ let multiply = multiply_big let modulo = modulo_big let quot = quot_big let power = power_big +let min = min_big +let max = max_big let arith_op_vec_big op sign size (l,r) = let ord = get_ord l in @@ -1207,6 +1211,7 @@ let eq_bit = bitwise_binop_bit (=) let neq (l,r) = bitwise_not_bit (eq (l,r)) let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec(l,r)) let neq_bit (l,r) = bitwise_not_bit (eq_bit(l,r)) +let neq_range = neq let mask (n,v) = let n' = int_of_big_int n in |