Merge PR #13559: Signed primitive integers

Reviewed-by: SkySkimmer
Reviewed-by: silene
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: proux01

1 files changed, 50 insertions, 0 deletions

diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index bd6241ae67..c986cb473d 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -333,6 +333,22 @@ let rem accu x y =
   if is_int x && is_int y then no_check_rem x y
   else accu x y
 
+let no_check_divs x y =
+  mk_uint (Uint63.divs (to_uint x) (to_uint y))
+[@@ocaml.inline always]
+
+let divs accu x y =
+  if is_int x && is_int y then no_check_divs x y
+  else accu x y
+
+let no_check_rems x y =
+  mk_uint (Uint63.rems (to_uint x) (to_uint y))
+[@@ocaml.inline always]
+
+let rems accu x y =
+  if is_int x && is_int y then no_check_rems x y
+  else accu x y
+
 let no_check_l_sr x y =
   mk_uint (Uint63.l_sr (to_uint x) (to_uint y))
 [@@ocaml.inline always]
@@ -349,6 +365,14 @@ let l_sl accu x y =
   if is_int x && is_int y then no_check_l_sl x y
   else accu x y
 
+let no_check_a_sr x y =
+  mk_uint (Uint63.a_sr (to_uint x) (to_uint y))
+[@@ocaml.inline always]
+
+let a_sr accu x y =
+  if is_int x && is_int y then no_check_a_sr x y
+  else accu x y
+
 let no_check_l_and x y =
   mk_uint (Uint63.l_and (to_uint x) (to_uint y))
 [@@ocaml.inline always]
@@ -502,6 +526,22 @@ let le accu x y =
   if is_int x && is_int y then no_check_le x y
   else accu x y
 
+let no_check_lts x y =
+  mk_bool (Uint63.lts (to_uint x) (to_uint y))
+[@@ocaml.inline always]
+
+let lts accu x y =
+  if is_int x && is_int y then no_check_lts x y
+  else accu x y
+
+let no_check_les x y =
+  mk_bool (Uint63.les (to_uint x) (to_uint y))
+[@@ocaml.inline always]
+
+let les accu x y =
+  if is_int x && is_int y then no_check_les x y
+  else accu x y
+
 let no_check_compare x y =
   match Uint63.compare (to_uint x) (to_uint y) with
   | x when x < 0 -> (Obj.magic CmpLt:t)
@@ -512,6 +552,16 @@ let compare accu x y =
   if is_int x && is_int y then no_check_compare x y
   else accu x y
 
+let no_check_compares x y =
+  match Uint63.compares (to_uint x) (to_uint y) with
+  | x when x < 0 -> (Obj.magic CmpLt:t)
+  | 0 -> (Obj.magic CmpEq:t)
+  | _ -> (Obj.magic CmpGt:t)
+
+let compares accu x y =
+  if is_int x && is_int y then no_check_compares x y
+  else accu x y
+
 let print x =
   Printf.fprintf stderr "%s" (Uint63.to_string (to_uint x));
   flush stderr;