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, 25 insertions, 3 deletions

diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml
index 8d052d6593..d017dafd3c 100644
--- a/kernel/uint63_63.ml
+++ b/kernel/uint63_63.ml
@@ -53,6 +53,10 @@ let l_sl x y =
 let l_sr x y =
   if 0 <= y && y < 63 then x lsr y else 0
 
+    (* arithmetic shift (for sint63) *)
+let a_sr x y =
+  if 0 <= y && y < 63 then x asr y else 0
+
 let l_and x y = x land y
 [@@ocaml.inline always]
 
@@ -84,6 +88,14 @@ let rem (x : int) (y : int) =
 
 let diveucl x y = (div x y, rem x y)
 
+    (* signed division *)
+let divs (x : int) (y : int) =
+  if y = 0 then 0 else x / y
+
+    (* modulo *)
+let rems (x : int) (y : int) =
+  if y = 0 then 0 else x mod y
+
 let addmuldiv p x y =
   l_or (l_sl x p) (l_sr y (uint_size - p))
 
@@ -96,6 +108,15 @@ let le (x : int) (y : int) =
   (x lxor 0x4000000000000000) <= (y lxor 0x4000000000000000)
 [@@ocaml.inline always]
 
+    (* signed comparison *)
+let lts (x : int) (y : int) =
+  x < y
+[@@ocaml.inline always]
+
+let les (x : int) (y : int) =
+  x <= y
+[@@ocaml.inline always]
+
 let to_int_min n m =
   if lt n m then n else m
 [@@ocaml.inline always]
@@ -175,9 +196,10 @@ let equal (x : int) (y : int) = x = y
 let compare (x:int) (y:int) =
   let x = x lxor 0x4000000000000000 in
   let y = y lxor 0x4000000000000000 in
-  if x > y then 1
-  else if y > x then -1
-  else 0
+  Int.compare x y
+
+let compares (x : int) (y : int) =
+  Int.compare x y
 
     (* head tail *)