From e148fa2ae5686c13d319d960c798cc542066be8c Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Fri, 5 Feb 2016 13:13:18 +0000
Subject: change signed mod behaviour for numbers to match that of vectors

---
 src/lem_interp/interp_lib.lem | 1 +
 src/type_internal.ml          | 4 ++--
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'src')

diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index d494ab12..c16b6c3d 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -686,6 +686,7 @@ let library_functions direction = [
   ("bitwise_rightshift", shift_op_vec ">>");
   ("bitwise_rotate", shift_op_vec "<<<");
   ("modulo", arith_op_no0 (mod));
+  ("mod_signed", arith_op_no0 hardwaer_mod);
   ("mod_vec", arith_op_vec_no0 hardware_mod "mod" Unsigned 1);
   ("mod_vec_range", arith_op_vec_range_no0 hardware_mod "mod" Unsigned 1);
   ("mod_signed_vec", arith_op_vec_no0 hardware_mod "mod" Signed 1);
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 7ef085b9..81a8e681 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -1967,12 +1967,12 @@ let initial_typ_env =
      Overload(
        Base(((mk_typ_params ["a";"b";"c"]),
              (mk_pure_fun (mk_tup [{t=Tvar "a"};{t=Tvar "b"}]) {t=Tvar "c"})),
-            (External (Some "modulo")),[],pure_e,pure_e,nob),
+            (External (Some "mod_signed")),[],pure_e,pure_e,nob),
        true,
        [Base(((mk_nat_params["n";"o";]),
               (mk_pure_fun (mk_tup [mk_atom (mk_nv "n") ; mk_atom (mk_nv "o")])
                            (mk_range n_zero (mk_sub (mk_nv "o") n_one)))),
-             (External (Some "modulo")),
+             (External (Some "mod_signed")),
              [GtEq(Specc(Parse_ast.Int("modulo",None)),Require,(mk_nv "o"),n_one)],pure_e,pure_e,nob);
         Base(((mk_nat_params["n";"m";"o"])@(mk_ord_params["ord"]),
               (mk_pure_fun (mk_tup [mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m");
-- 
cgit v1.2.3