Tidy up of div and mod operators (C implementation was previously inconsistent with ocaml etc.). Rename div and mod builtins to ediv_int/emod_int and tdiv_int/tmod_int and add corresponding implementations. Add a test with negative operands. This will break existing models but will mean users have to think about which versions they want and won't accidentally use the wrong one.

7 files changed, 19 insertions, 7 deletions

diff --git a/test/typecheck/pass/Replicate.sail b/test/typecheck/pass/Replicate.sail
index 03954a9f..291b7e16 100644
--- a/test/typecheck/pass/Replicate.sail
+++ b/test/typecheck/pass/Replicate.sail
@@ -3,6 +3,9 @@ default Order dec
 $include <smt.sail>
 $include <prelude.sail>
 
+overload operator / = {ediv_int}
+overload operator % = {emod_int}
+
 val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
diff --git a/test/typecheck/pass/Replicate/v1.expect b/test/typecheck/pass/Replicate/v1.expect
index 92c6d7cd..c40aa5ec 100644
--- a/test/typecheck/pass/Replicate/v1.expect
+++ b/test/typecheck/pass/Replicate/v1.expect
@@ -1,8 +1,8 @@
 Type error:
-[Replicate/v1.sail]:11:4-30
-11 |    replicate_bits(x, 'N / 'M)
+[Replicate/v1.sail]:14:4-30
+14 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, div(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from vector(('M * div('N, 'M)), dec, bit) to vector('N, dec, bit) on replicate_bits(x, ediv_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/Replicate/v1.sail b/test/typecheck/pass/Replicate/v1.sail
index 69f2bb6f..55627db5 100644
--- a/test/typecheck/pass/Replicate/v1.sail
+++ b/test/typecheck/pass/Replicate/v1.sail
@@ -3,6 +3,9 @@ default Order dec
 $include <smt.sail>
 $include <prelude.sail>
 
+overload operator / = {ediv_int}
+overload operator % = {emod_int}
+
 val Replicate : forall ('M : Int) ('N : Int), 'M >= 0.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
diff --git a/test/typecheck/pass/Replicate/v2.expect b/test/typecheck/pass/Replicate/v2.expect
index 6afdac30..c2c15c12 100644
--- a/test/typecheck/pass/Replicate/v2.expect
+++ b/test/typecheck/pass/Replicate/v2.expect
@@ -1,8 +1,8 @@
 Type error:
-[Replicate/v2.sail]:10:4-30
-10 |    replicate_bits(x, 'N / 'M)
+[Replicate/v2.sail]:13:4-30
+13 |    replicate_bits(x, 'N / 'M)
    |    ^------------------------^
-   | Tried performing type coercion from {('ex118# : Int), true. vector(('M * 'ex118#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, div_int(__id(N), bitvector_length(x)))
+   | Tried performing type coercion from {('ex118# : Int), true. vector(('M * 'ex118#), dec, bit)} to vector('N, dec, bit) on replicate_bits(x, tdiv_int(__id(N), bitvector_length(x)))
    | Coercion failed because:
    | Mismatched argument types in subtype check
    | 
diff --git a/test/typecheck/pass/Replicate/v2.sail b/test/typecheck/pass/Replicate/v2.sail
index e54b0af4..436ef24b 100644
--- a/test/typecheck/pass/Replicate/v2.sail
+++ b/test/typecheck/pass/Replicate/v2.sail
@@ -2,6 +2,9 @@ default Order dec
 
 $include <prelude.sail>
 
+overload operator / = {tdiv_int}
+overload operator % = {tmod_int}
+
 val Replicate : forall ('M : Int) ('N : Int), 'M >= 1.
   (implicit('N), bits('M)) -> bits('N) effect {escape}
 
diff --git a/test/typecheck/pass/guards.sail b/test/typecheck/pass/guards.sail
index 4aac2bed..594130a8 100644
--- a/test/typecheck/pass/guards.sail
+++ b/test/typecheck/pass/guards.sail
@@ -1,8 +1,9 @@
 default Order dec
 
 $include <prelude.sail>
+$include <smt.sail>
 
-overload operator / = {quotient}
+overload operator / = {ediv_int}
 
 union T = {C1 : int, C2 : int}
 
diff --git a/test/typecheck/pass/recursion.sail b/test/typecheck/pass/recursion.sail
index 5ca85f53..cd3ca46c 100644
--- a/test/typecheck/pass/recursion.sail
+++ b/test/typecheck/pass/recursion.sail
@@ -2,6 +2,8 @@ default Order dec
 
 $include <prelude.sail>
 
+overload operator / = {tdiv_int}
+
 val log2 : int -> int
 
 function log2(n) =