another mod and quot definition

1 files changed, 13 insertions, 15 deletions

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 3589c84f..4966a2b0 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -7,21 +7,19 @@ open import List
 open import Word
 open import Bool
 
-val quomod : integer -> integer -> (integer * integer)
-declare ocaml    target_rep function quomod = `Big_int.quomod_big_int`
-
-let hardware_mod a b = 
- let (q,r) = quomod a b in
- if q < 0 then r-b 
- else 
-   if a > b && a < 0
-   then a else r
-
-let hardware_quot a b = 
- let (q,r) = quomod a b in
- if q < 0 then q+1 
- else if a > b && a < 0
- then 0 else q
+let hardware_mod (a: integer) (b:integer) : integer = 
+ if a < 0 && b < 0
+ then (abs a) mod (abs b)
+ else if (a < 0 && b >= 0) || (a >= 0 && b < 0) 
+ then (a mod b) - b
+ else a mod b
+
+let hardware_quot (a:integer) (b:integer) : integer = 
+  if a < 0 && b < 0
+  then (abs a) / (abs b)
+  else if (a < 0 && b >= 0) || (a >= 0 && b < 0)
+  then (a/b) + 1
+  else a/b
 
 let ignore_sail x = V_lit (L_aux L_unit Unknown) ;;