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, 23 insertions, 0 deletions

diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index b9b75a9d7c..98cf4219a0 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -158,9 +158,12 @@ val sub : t -> t -> t -> t
 val mul : t -> t -> t -> t
 val div : t -> t -> t -> t
 val rem : t -> t -> t -> t
+val divs : t -> t -> t -> t
+val rems : t -> t -> t -> t
 
 val l_sr  : t -> t -> t -> t
 val l_sl  : t -> t -> t -> t
+val a_sr  : t -> t -> t -> t
 val l_and : t -> t -> t -> t
 val l_xor : t -> t -> t -> t
 val l_or  : t -> t -> t -> t
@@ -179,7 +182,10 @@ val addMulDiv : t -> t -> t -> t -> t
 val eq      : t -> t -> t -> t
 val lt      : t -> t -> t -> t
 val le      : t -> t -> t -> t
+val lts     : t -> t -> t -> t
+val les     : t -> t -> t -> t
 val compare : t -> t -> t -> t
+val compares : t -> t -> t -> t
 
 val print : t -> t
 
@@ -205,12 +211,21 @@ val no_check_div : t -> t -> t
 val no_check_rem : t -> t -> t
 [@@ocaml.inline always]
 
+val no_check_divs : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_rems : t -> t -> t
+[@@ocaml.inline always]
+
 val no_check_l_sr  : t -> t -> t
 [@@ocaml.inline always]
 
 val no_check_l_sl  : t -> t -> t
 [@@ocaml.inline always]
 
+val no_check_a_sr  : t -> t -> t
+[@@ocaml.inline always]
+
 val no_check_l_and : t -> t -> t
 [@@ocaml.inline always]
 
@@ -253,8 +268,16 @@ val no_check_lt      : t -> t -> t
 val no_check_le      : t -> t -> t
 [@@ocaml.inline always]
 
+val no_check_lts     : t -> t -> t
+[@@ocaml.inline always]
+
+val no_check_les     : t -> t -> t
+[@@ocaml.inline always]
+
 val no_check_compare : t -> t -> t
 
+val no_check_compares : t -> t -> t
+
 (** Support for machine floating point values *)
 
 val is_float : t -> bool