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.

1 files changed, 3 insertions, 9 deletions

diff --git a/aarch64/prelude.sail b/aarch64/prelude.sail
index f4f7dc75..431ad1f7 100755
--- a/aarch64/prelude.sail
+++ b/aarch64/prelude.sail
@@ -284,17 +284,11 @@ val abs_real = {coq: "Rabs", _: "abs_real"} : real -> real
 
 overload abs = {abs_atom, abs_real}
 
-val quotient_nat = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int"} : (nat, nat) -> nat
-
 val quotient_real = {ocaml: "quotient_real", lem: "realDiv", c: "div_real", coq: "Rdiv"} : (real, real) -> real
 
-val quotient = {ocaml: "quotient", lem: "integerDiv", c: "tdiv_int", coq: "Z.quot"} : (int, int) -> int
-
-overload operator / = {quotient_nat, quotient, quotient_real}
-
-val modulus = {ocaml: "modulus", lem: "hardware_mod", c: "tmod_int", coq: "Z.rem"} : (int, int) -> int
-
-overload operator % = {modulus}
+overload operator / = {ediv_int, quotient_real}
+overload div = {ediv_int}
+overload operator % = {emod_int}
 
 val Real = {ocaml: "to_real", lem: "realFromInteger", c: "to_real", coq: "IZR"} : int -> real