Add flooring division in prelude

Defined in terms of tdiv so we don't have to add it to backends that
don't already have it

1 files changed, 27 insertions, 2 deletions

diff --git a/lib/arith.sail b/lib/arith.sail
index 6b064433..58f25bbc 100644
--- a/lib/arith.sail
+++ b/lib/arith.sail
@@ -88,13 +88,38 @@ val tdiv_int = {
 } : (int, int) -> int
 
 /*! Remainder for truncating division (has sign of dividend) */
-val tmod_int = {
+val _tmod_int = {
   ocaml: "tmod_int",
   interpreter: "tmod_int",
   lem: "tmod_int",
   c: "tmod_int",
   coq: "Z.rem"
-} : (int, int) -> nat
+} : (int, int) -> int
+
+/*! If we know the second argument is positive, we know the result is positive */
+val _tmod_int_positive = {
+  ocaml: "tmod_int",
+  interpreter: "tmod_int",
+  lem: "tmod_int",
+  c: "tmod_int",
+  coq: "Z.rem"
+} : forall 'n, 'n >= 1. (int, int('n)) -> nat
+
+overload tmod_int = {_tmod_int_positive, _tmod_int}
+
+function fdiv_int(n: int, m: int) -> int = {
+  if n < 0 & m > 0 then {
+    tdiv_int(n + 1, m) - 1
+  } else if n > 0 & m < 0 then {
+    tdiv_int(n - 1, m) - 1
+  } else {
+    tdiv_int(n, m)
+  }
+}
+
+function fmod_int(n: int, m: int) -> int = {
+  n - (m * fdiv_int(n, m))
+}
 
 val abs_int_plain = {
   smt : "abs",