summaryrefslogtreecommitdiff
path: root/src/gen_lib/sail_operators.lem
diff options
context:
space:
mode:
authorThomas Bauereiss2017-10-13 16:06:24 +0100
committerThomas Bauereiss2017-10-13 17:23:39 +0100
commitecdbf28f72860cdb44ce9dc0bdd811b64572fd90 (patch)
tree6a5b00428a4273a3dcbfd9fb6276da9401aceadc /src/gen_lib/sail_operators.lem
parent2ced2254c30061598a3e30f19131122213f3c18b (diff)
Add support for real numbers to Lem backend
Requires version of Lem with real number support, currently at https://bitbucket.org/bauereiss/lem/branch/reals
Diffstat (limited to 'src/gen_lib/sail_operators.lem')
-rw-r--r--src/gen_lib/sail_operators.lem12
1 files changed, 1 insertions, 11 deletions
diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index 7b117726..f14ef2e4 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -197,18 +197,8 @@ let extz_bl (start, len, bits) = Vector bits start false
let exts_bl (start, len, bits) = Vector bits start false
-let add (l,r) = integerAdd l r
-let add_signed (l,r) = integerAdd l r
-let sub (l,r) = integerMinus l r
-let mult (l,r) = integerMult l r
-let quotient (l,r) = integerDiv l r
-let modulo (l,r) = hardware_mod l r
let quot = hardware_quot
-let power (l,r) = integerPow l r
-
-let add_int = add
-let sub_int = sub
-let mult_int = mult
+let modulo (l,r) = hardware_mod l r
let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r =
let (l',r') = (to_num sign l, to_num sign r) in