Fix tdiv_int and tmod_int bindings for Lem

Also rename them for uniformity with other backends.

2 files changed, 11 insertions, 7 deletions

diff --git a/src/gen_lib/sail2_operators.lem b/src/gen_lib/sail2_operators.lem
index 547160d3..43a9812e 100644
--- a/src/gen_lib/sail2_operators.lem
+++ b/src/gen_lib/sail2_operators.lem
@@ -163,9 +163,9 @@ let arith_op_bv_no0 op sign size l r =
   Maybe.bind (int_of_bv sign r) (fun r' ->
   if r' = 0 then Nothing else Just (of_int (length l * size) (op l' r'))))
 
-let mod_bv = arith_op_bv_no0 hardware_mod false 1
-let quot_bv = arith_op_bv_no0 hardware_quot false 1
-let quots_bv = arith_op_bv_no0 hardware_quot true 1
+let mod_bv = arith_op_bv_no0 tmod_int false 1
+let quot_bv = arith_op_bv_no0 tdiv_int false 1
+let quots_bv = arith_op_bv_no0 tdiv_int true 1
 
 let mod_mword = Machine_word.modulo
 let quot_mword = Machine_word.unsignedDivide
@@ -174,8 +174,8 @@ let quots_mword = Machine_word.signedDivide
 let arith_op_bv_int_no0 op sign size l r =
   arith_op_bv_no0 op sign size l (of_int (length l) r)
 
-let quot_bv_int = arith_op_bv_int_no0 hardware_quot false 1
-let mod_bv_int = arith_op_bv_int_no0 hardware_mod false 1
+let quot_bv_int = arith_op_bv_int_no0 tdiv_int false 1
+let mod_bv_int = arith_op_bv_int_no0 tmod_int false 1
 
 let mod_mword_int l r = Machine_word.modulo l (wordFromInteger r)
 let quot_mword_int l r = Machine_word.unsignedDivide l (wordFromInteger r)
diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index 5e6537a8..9de28cca 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -104,21 +104,25 @@ let upper n = n
 
 (* Modulus operation corresponding to quot below -- result
    has sign of dividend. *)
-let hardware_mod (a: integer) (b:integer) : integer =
+let tmod_int (a: integer) (b:integer) : integer =
   let m = (abs a) mod (abs b) in
   if a < 0 then ~m else m
 
+let hardware_mod = tmod_int
+
 (* There are different possible answers for integer divide regarding
 rounding behaviour on negative operands. Positive operands always
 round down so derive the one we want (trucation towards zero) from
 that *)
-let hardware_quot (a:integer) (b:integer) : integer =
+let tdiv_int (a:integer) (b:integer) : integer =
   let q = (abs a) / (abs b) in
   if ((a<0) = (b<0)) then
     q  (* same sign -- result positive *)
   else
     ~q (* different sign -- result negative *)
 
+let hardware_quot = tdiv_int
+
 let max_64u = (integerPow 2 64) - 1
 let max_64  = (integerPow 2 63) - 1
 let min_64  = 0 - (integerPow 2 63)