Signed primitive integers

Signed primitive integers defined on top of the existing unsigned ones
with two's complement.

The module Sint63 includes the theory of signed primitive integers that
differs from the unsigned case.

Additions to the kernel:
  les (signed <=), lts (signed <), compares (signed compare),
  divs (signed division), rems (signed remainder),
  asr (arithmetic shift right)
(The s suffix is not used when importing the Sint63 module.)

The printing and parsing of primitive ints was updated and the
int63_syntax_plugin was removed (we use Number Notation instead).

A primitive int is parsed / printed as unsigned or signed depending on
the scope. In the default (Set Printing All) case, it is printed in
hexadecimal.

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;