From f4acbce30be2aecdfc491478a24c5eb551824f24 Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Fri, 22 Mar 2019 16:50:48 +0000
Subject: 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.

---
 aarch64/prelude.sail | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

(limited to 'aarch64')

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
 
-- 
cgit v1.2.3