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.

13 files changed, 334 insertions, 9 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 95a334561f..704eb1ef98 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -1426,6 +1426,41 @@ value coq_interprete
         Next;
       }
 
+      Instruct(CHECKDIVSINT63) {
+        print_instr("CHEKDIVSINT63");
+        CheckInt2();
+        int b;
+        Uint63_eq0(b, *sp);
+        if (b) {
+          accu = *sp++;
+        }
+        else {
+          Uint63_eqm1(b, *sp);
+          if (b) {
+            Uint63_neg(accu);
+            sp++;
+          }
+          else {
+            Uint63_divs(accu, *sp++);
+          }
+        }
+        Next;
+      }
+
+      Instruct(CHECKMODSINT63) {
+        print_instr("CHEKMODSINT63");
+        CheckInt2();
+        int b;
+        Uint63_eq0(b, *sp);
+        if (b) {
+          accu = *sp++;
+        }
+        else {
+          Uint63_mods(accu,*sp++);
+        }
+        Next;
+      }
+
       Instruct (CHECKDIV21INT63) {
         print_instr("DIV21INT63");
         CheckInt3();
@@ -1473,6 +1508,13 @@ value coq_interprete
         Next;
       }
 
+      Instruct(CHECKASRINT63) {
+        print_instr("CHECKASRINT63");
+        CheckInt2();
+        Uint63_asr(accu,*sp++);
+        Next;
+      }
+
       Instruct (CHECKADDMULDIVINT63) {
         print_instr("CHECKADDMULDIVINT63");
         CheckInt3();
@@ -1508,6 +1550,24 @@ value coq_interprete
        Next;
      }
 
+     Instruct (CHECKLTSINT63) {
+       print_instr("CHECKLTSINT63");
+       CheckInt2();
+       int b;
+       Uint63_lts(b,accu,*sp++);
+       accu = b ? coq_true : coq_false;
+       Next;
+     }
+
+     Instruct (CHECKLESINT63) {
+       print_instr("CHECKLESINT63");
+       CheckInt2();
+       int b;
+       Uint63_les(b,accu,*sp++);
+       accu = b ? coq_true : coq_false;
+       Next;
+     }
+
      Instruct (CHECKCOMPAREINT63) {
         /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
         /* assumes Inductive _ : _ := Eq | Lt | Gt */
@@ -1526,6 +1586,24 @@ value coq_interprete
         Next;
       }
 
+     Instruct (CHECKCOMPARESINT63) {
+       /* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
+       /* assumes Inductive _ : _ := Eq | Lt | Gt */
+       print_instr("CHECKCOMPARESINT63");
+       CheckInt2();
+       int b;
+       Uint63_eq(b, accu, *sp);
+       if (b) {
+         accu = coq_Eq;
+         sp++;
+       }
+       else {
+         Uint63_lts(b, accu, *sp++);
+         accu = b ? coq_Lt : coq_Gt;
+       }
+       Next;
+     }
+
       Instruct (CHECKHEAD0INT63) {
         print_instr("CHECKHEAD0INT63");
         CheckInt1();
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index dd9b9e55be..693716ee90 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -96,7 +96,10 @@ value uint63_##name##_ml(value x, value y, value z) { \
     accu = uint63_return_value__; \
   }while(0)
 
+DECLARE_NULLOP(zero)
 DECLARE_NULLOP(one)
+DECLARE_UNOP(neg)
+#define Uint63_neg(x) CALL_UNOP(neg, x)
 DECLARE_BINOP(add)
 #define Uint63_add(x, y) CALL_BINOP(add, x, y)
 DECLARE_BINOP(addcarry)
@@ -105,28 +108,40 @@ DECLARE_TEROP(addmuldiv)
 #define Uint63_addmuldiv(x, y, z) CALL_TEROP(addmuldiv, x, y, z)
 DECLARE_BINOP(div)
 #define Uint63_div(x, y) CALL_BINOP(div, x, y)
+DECLARE_BINOP(divs)
+#define Uint63_divs(x, y) CALL_BINOP(divs, x, y)
 DECLARE_BINOP(eq)
 #define Uint63_eq(r, x, y) CALL_RELATION(r, eq, x, y)
 DECLARE_UNOP(eq0)
 #define Uint63_eq0(r, x) CALL_PREDICATE(r, eq0, x)
+DECLARE_UNOP(eqm1)
+#define Uint63_eqm1(r, x) CALL_PREDICATE(r, eqm1, x)
 DECLARE_UNOP(head0)
 #define Uint63_head0(x) CALL_UNOP(head0, x)
 DECLARE_BINOP(land)
 #define Uint63_land(x, y) CALL_BINOP(land, x, y)
 DECLARE_BINOP(leq)
 #define Uint63_leq(r, x, y) CALL_RELATION(r, leq, x, y)
+DECLARE_BINOP(les)
+#define Uint63_les(r, x, y) CALL_RELATION(r, les, x, y)
 DECLARE_BINOP(lor)
 #define Uint63_lor(x, y) CALL_BINOP(lor, x, y)
 DECLARE_BINOP(lsl)
 #define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y)
 DECLARE_BINOP(lsr)
 #define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y)
+DECLARE_BINOP(asr)
+#define Uint63_asr(x, y) CALL_BINOP(asr, x, y)
 DECLARE_BINOP(lt)
 #define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y)
+DECLARE_BINOP(lts)
+#define Uint63_lts(r, x, y) CALL_RELATION(r, lts, x, y)
 DECLARE_BINOP(lxor)
 #define Uint63_lxor(x, y) CALL_BINOP(lxor, x, y)
 DECLARE_BINOP(mod)
 #define Uint63_mod(x, y) CALL_BINOP(mod, x, y)
+DECLARE_BINOP(mods)
+#define Uint63_mods(x, y) CALL_BINOP(mods, x, y)
 DECLARE_BINOP(mul)
 #define Uint63_mul(x, y) CALL_BINOP(mul, x, y)
 DECLARE_BINOP(sub)
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 731ae8f46e..da9ae7f147 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -12,21 +12,28 @@
 
 #define uint_of_value(val) (((uint64_t)(val)) >> 1)
 #define uint63_of_value(val) ((uint64_t)(val) >> 1)
+#define int63_of_value(val) ((int64_t)(val) >> 1)
 
 /* 2^63 * y + x as a value */
 //#define Val_intint(x,y) ((value)(((uint64_t)(x)) << 1 + ((uint64_t)(y) << 64)))
 
-#define uint63_zero ((value) 1) /* 2*0 + 1 */
+#define uint63_zero() ((value) 1) /* 2*0 + 1 */
 #define uint63_one() ((value) 3) /* 2*1 + 1 */
 
 #define uint63_eq(x,y) ((x) == (y))
 #define Uint63_eq(r,x,y) ((r) = uint63_eq(x,y))
 #define Uint63_eq0(r,x) ((r) = ((x) == (uint64_t)1))
+#define Uint63_eqm1(r,x) ((r) = ((x) == (uint64_t)(int64_t)(-1)))
 #define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y))
 #define Uint63_lt(r,x,y) ((r) = uint63_lt(x,y))
 #define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y))
 #define Uint63_leq(r,x,y) ((r) = uint63_leq(x,y))
+#define uint63_lts(x,y) ((int64_t) (x) < (int64_t) (y))
+#define Uint63_lts(r,x,y) ((r) = uint63_lts(x,y))
+#define uint63_les(x,y) ((int64_t) (x) <= (int64_t) (y))
+#define Uint63_les(r,x,y) ((r) = uint63_les(x,y))
 
+#define Uint63_neg(x) (accu = (value)(2 - (uint64_t) x))
 #define Uint63_add(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) - 1))
 #define Uint63_addcarry(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) + 1))
 #define Uint63_sub(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) + 1))
@@ -34,6 +41,8 @@
 #define Uint63_mul(x,y) (accu = Val_long(uint63_of_value(x) * uint63_of_value(y)))
 #define Uint63_div(x,y) (accu = Val_long(uint63_of_value(x) / uint63_of_value(y)))
 #define Uint63_mod(x,y) (accu = Val_long(uint63_of_value(x) % uint63_of_value(y)))
+#define Uint63_divs(x,y) (accu = Val_long(int63_of_value(x) / int63_of_value(y)))
+#define Uint63_mods(x,y) (accu = Val_long(int63_of_value(x) % int63_of_value(y)))
 
 #define Uint63_lxor(x,y) (accu = (value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1))
 #define Uint63_lor(x,y) (accu = (value)((uint64_t)(x) | (uint64_t)(y)))
@@ -46,14 +55,21 @@
   if (uint63_lsl_y__ < (uint64_t) 127) \
     accu = (value)((((uint64_t)(x)-1) << uint63_of_value(uint63_lsl_y__)) | 1); \
   else \
-    accu = uint63_zero; \
+    accu = uint63_zero(); \
   }while(0)
 #define Uint63_lsr(x,y) do{ \
   value uint63_lsl_y__ = (y); \
   if (uint63_lsl_y__ < (uint64_t) 127) \
     accu = (value)(((uint64_t)(x) >> uint63_of_value(uint63_lsl_y__)) | 1); \
   else \
-    accu = uint63_zero; \
+    accu = uint63_zero(); \
+  }while(0)
+#define Uint63_asr(x,y) do{ \
+    value uint63_asr_y__ = (y); \
+    if (uint63_asr_y__ < (uint64_t) 127) \
+      accu = (value)(((int64_t)(x) >> uint63_of_value(uint63_asr_y__)) | 1); \
+    else \
+      accu = uint63_zero(); \
   }while(0)
 
 /* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 5cd91b4e74..6ef0e9fa15 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -8,6 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+(* Note: don't forget to update v_primitive in checker/values.ml if the *)
+(* number of primitives is changed. *)
+
 open Univ
 
 type t =
@@ -18,8 +21,11 @@ type t =
   | Int63mul
   | Int63div
   | Int63mod
+  | Int63divs
+  | Int63mods
   | Int63lsr
   | Int63lsl
+  | Int63asr
   | Int63land
   | Int63lor
   | Int63lxor
@@ -34,7 +40,10 @@ type t =
   | Int63eq
   | Int63lt
   | Int63le
+  | Int63lts
+  | Int63les
   | Int63compare
+  | Int63compares
   | Float64opp
   | Float64abs
   | Float64eq
@@ -68,8 +77,11 @@ let parse = function
   | "int63_mul" -> Int63mul
   | "int63_div" -> Int63div
   | "int63_mod" -> Int63mod
+  | "int63_divs" -> Int63divs
+  | "int63_mods" -> Int63mods
   | "int63_lsr" -> Int63lsr
   | "int63_lsl" -> Int63lsl
+  | "int63_asr" -> Int63asr
   | "int63_land" -> Int63land
   | "int63_lor" -> Int63lor
   | "int63_lxor" -> Int63lxor
@@ -84,7 +96,10 @@ let parse = function
   | "int63_eq" -> Int63eq
   | "int63_lt" -> Int63lt
   | "int63_le" -> Int63le
+  | "int63_lts" -> Int63lts
+  | "int63_les" -> Int63les
   | "int63_compare" -> Int63compare
+  | "int63_compares" -> Int63compares
   | "float64_opp" -> Float64opp
   | "float64_abs" -> Float64abs
   | "float64_eq" -> Float64eq
@@ -163,6 +178,12 @@ let hash = function
   | Arrayset -> 46
   | Arraycopy -> 47
   | Arraylength -> 48
+  | Int63lts -> 49
+  | Int63les -> 50
+  | Int63divs -> 51
+  | Int63mods -> 52
+  | Int63asr -> 53
+  | Int63compares -> 54
 
 (* Should match names in nativevalues.ml *)
 let to_string = function
@@ -173,8 +194,11 @@ let to_string = function
   | Int63mul -> "mul"
   | Int63div -> "div"
   | Int63mod -> "rem"
+  | Int63divs -> "divs"
+  | Int63mods -> "rems"
   | Int63lsr -> "l_sr"
   | Int63lsl -> "l_sl"
+  | Int63asr -> "a_sr"
   | Int63land -> "l_and"
   | Int63lor -> "l_or"
   | Int63lxor -> "l_xor"
@@ -189,7 +213,10 @@ let to_string = function
   | Int63eq -> "eq"
   | Int63lt -> "lt"
   | Int63le -> "le"
+  | Int63lts -> "lts"
+  | Int63les -> "les"
   | Int63compare -> "compare"
+  | Int63compares -> "compares"
   | Float64opp -> "fopp"
   | Float64abs -> "fabs"
   | Float64eq -> "feq"
@@ -271,14 +298,15 @@ let types =
   | Int63head0 | Int63tail0 -> [int_ty; int_ty]
   | Int63add | Int63sub | Int63mul
   | Int63div | Int63mod
-  | Int63lsr | Int63lsl
+  | Int63divs | Int63mods
+  | Int63lsr | Int63lsl | Int63asr
   | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty]
   | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC ->
      [int_ty; int_ty; PITT_ind (PIT_carry, int_ty)]
   | Int63mulc | Int63diveucl ->
      [int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))]
-  | Int63eq | Int63lt | Int63le -> [int_ty; int_ty; PITT_ind (PIT_bool, ())]
-  | Int63compare -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())]
+  | Int63eq | Int63lt | Int63le | Int63lts | Int63les -> [int_ty; int_ty; PITT_ind (PIT_bool, ())]
+  | Int63compare | Int63compares -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())]
   | Int63div21 ->
      [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))]
   | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty]
@@ -314,8 +342,11 @@ let params = function
   | Int63mul
   | Int63div
   | Int63mod
+  | Int63divs
+  | Int63mods
   | Int63lsr
   | Int63lsl
+  | Int63asr
   | Int63land
   | Int63lor
   | Int63lxor
@@ -330,7 +361,10 @@ let params = function
   | Int63eq
   | Int63lt
   | Int63le
+  | Int63lts
+  | Int63les
   | Int63compare
+  | Int63compares
   | Float64opp
   | Float64abs
   | Float64eq
@@ -367,8 +401,11 @@ let univs = function
   | Int63mul
   | Int63div
   | Int63mod
+  | Int63divs
+  | Int63mods
   | Int63lsr
   | Int63lsl
+  | Int63asr
   | Int63land
   | Int63lor
   | Int63lxor
@@ -383,7 +420,10 @@ let univs = function
   | Int63eq
   | Int63lt
   | Int63le
+  | Int63lts
+  | Int63les
   | Int63compare
+  | Int63compares
   | Float64opp
   | Float64abs
   | Float64eq
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index 0db643faf4..de90179726 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -16,8 +16,11 @@ type t =
   | Int63mul
   | Int63div
   | Int63mod
+  | Int63divs
+  | Int63mods
   | Int63lsr
   | Int63lsl
+  | Int63asr
   | Int63land
   | Int63lor
   | Int63lxor
@@ -32,7 +35,10 @@ type t =
   | Int63eq
   | Int63lt
   | Int63le
+  | Int63lts
+  | Int63les
   | Int63compare
+  | Int63compares
   | Float64opp
   | Float64abs
   | Float64eq
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index bda65956be..20220dd9d2 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -110,6 +110,8 @@ let opcodes =
     "CHECKMULCINT63", 1;
     "CHECKDIVINT63", 1;
     "CHECKMODINT63", 1;
+    "CHECKDIVSINT63", 1;
+    "CHECKMODSINT63", 1;
     "CHECKDIVEUCLINT63", 1;
     "CHECKDIV21INT63", 1;
     "CHECKLXORINT63", 1;
@@ -117,11 +119,15 @@ let opcodes =
     "CHECKLANDINT63", 1;
     "CHECKLSLINT63", 1;
     "CHECKLSRINT63", 1;
+    "CHECKASRINT63", 1;
     "CHECKADDMULDIVINT63", 1;
     "CHECKEQINT63", 1;
     "CHECKLTINT63", 1;
     "CHECKLEINT63", 1;
+    "CHECKLTSINT63", 1;
+    "CHECKLESINT63", 1;
     "CHECKCOMPAREINT63", 1;
+    "CHECKCOMPARESINT63", 1;
     "CHECKHEAD0INT63", 1;
     "CHECKTAIL0INT63", 1;
     "CHECKOPPFLOAT", 1;
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;
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
diff --git a/kernel/primred.ml b/kernel/primred.ml
index f0b4d6d362..23b7e13ab8 100644
--- a/kernel/primred.ml
+++ b/kernel/primred.ml
@@ -223,10 +223,16 @@ struct
       let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.div i1 i2)
     | Int63mod ->
       let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.rem i1 i2)
+    | Int63divs ->
+      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.divs i1 i2)
+    | Int63mods ->
+      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.rems i1 i2)
     | Int63lsr ->
       let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sr i1 i2)
     | Int63lsl ->
       let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_sl i1 i2)
+    | Int63asr ->
+      let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.a_sr i1 i2)
     | Int63land ->
       let i1, i2 = get_int2 evd args in E.mkInt env (Uint63.l_and i1 i2)
     | Int63lor ->
@@ -276,6 +282,12 @@ struct
     | Int63le ->
       let i1, i2 = get_int2 evd args in
       E.mkBool env (Uint63.le i1 i2)
+    | Int63lts ->
+      let i1, i2 = get_int2 evd args in
+      E.mkBool env (Uint63.lts i1 i2)
+    | Int63les ->
+      let i1, i2 = get_int2 evd args in
+      E.mkBool env (Uint63.les i1 i2)
     | Int63compare ->
       let i1, i2 = get_int2 evd args in
       begin match Uint63.compare i1 i2 with
@@ -283,6 +295,13 @@ struct
         | 0 -> E.mkEq env
         | _ -> E.mkGt env
       end
+    | Int63compares ->
+      let i1, i2 = get_int2 evd args in
+      begin match Uint63.compares i1 i2 with
+        | x when x < 0 ->  E.mkLt env
+        | 0 -> E.mkEq env
+        | _ -> E.mkGt env
+      end
     | Float64opp ->
       let f = get_float1 evd args in E.mkFloat env (Float64.opp f)
     | Float64abs ->
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index 6b2519918a..ff8d1eefb7 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -48,6 +48,7 @@ val l_xor   : t -> t -> t
 val l_or    : t -> t -> t
 
       (* Arithmetic operations *)
+val a_sr    : t -> t -> t
 val add     : t -> t -> t
 val sub     : t -> t -> t
 val mul     : t -> t -> t
@@ -56,6 +57,10 @@ val rem     : t -> t -> t
 
 val diveucl : t -> t -> t * t
 
+      (* Signed arithmetic opeartions *)
+val divs     : t -> t -> t
+val rems     : t -> t -> t
+
       (* Specific arithmetic operations *)
 val mulc    : t -> t -> t * t
 val addmuldiv : t -> t -> t -> t
@@ -71,6 +76,11 @@ val equal      : t -> t -> bool
 val le      : t -> t -> bool
 val compare : t -> t -> int
 
+      (* signed comparision *)
+val lts      : t -> t -> bool
+val les      : t -> t -> bool
+val compares : t -> t -> int
+
       (* head and tail *)
 val head0   : t -> t
 val tail0   : t -> t
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index 4f2cbc4262..9c8401105e 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -52,6 +52,15 @@ let lt x y =
 let le x y =
   Int64.compare x y <= 0
 
+    (* signed comparison *)
+(* We shift the arguments by 1 to the left so that the top-most bit is interpreted as a sign *)
+(* The zero at the end doesn't change the order (it is stable by multiplication by 2) *)
+let lts x y =
+  Int64.(compare (shift_left x 1) (shift_left y 1)) < 0
+
+let les x y =
+  Int64.(compare (shift_left x 1) (shift_left y 1)) <= 0
+
     (* logical shift *)
 let l_sl x y =
   if le 0L y && lt y 63L then mask63 (Int64.shift_left x (Int64.to_int y)) else 0L
@@ -59,6 +68,12 @@ let l_sl x y =
 let l_sr x y =
   if le 0L y && lt y 63L then Int64.shift_right x (Int64.to_int y) else 0L
 
+    (* arithmetic shift (for sint63) *)
+let a_sr x y =
+  if les 0L y && lts y 63L then
+    mask63 (Int64.shift_right (Int64.shift_left x 1) ((Int64.to_int y) + 1))
+  else 0L
+
 let l_and x y = Int64.logand x y
 let l_or x y = Int64.logor x y
 let l_xor x y = Int64.logxor x y
@@ -86,6 +101,15 @@ let rem x y =
 
 let diveucl x y = (div x y, rem x y)
 
+    (* signed division *)
+let divs x y =
+  if y = 0L then 0L else mask63 Int64.(div (shift_left x 1) (shift_left y 1))
+
+    (* signed modulo *)
+let rems x y =
+  if y = 0L then 0L else
+    Int64.shift_right_logical (Int64.(rem (shift_left x 1) (shift_left y 1))) 1
+
 let addmuldiv p x y =
   l_or (l_sl x p) (l_sr y Int64.(sub (of_int uint_size) p))
 
@@ -139,6 +163,8 @@ let equal (x : t) y = x = y
 
 let compare x y = Int64.compare x y
 
+let compares x y = Int64.(compare (shift_left x 1) (shift_left y 1))
+
 (* Number of leading zeroes *)
 let head0 x =
   let r = ref 0 in
@@ -198,22 +224,30 @@ let () =
   Callback.register "uint63 addcarry" addcarry;
   Callback.register "uint63 addmuldiv" addmuldiv;
   Callback.register "uint63 div" div;
+  Callback.register "uint63 divs" divs;
   Callback.register "uint63 div21_ml" div21;
   Callback.register "uint63 eq" equal;
   Callback.register "uint63 eq0" (equal Int64.zero);
+  Callback.register "uint63 eqm1" (equal (sub zero one));
   Callback.register "uint63 head0" head0;
   Callback.register "uint63 land" l_and;
   Callback.register "uint63 leq" le;
+  Callback.register "uint63 les" les;
   Callback.register "uint63 lor" l_or;
   Callback.register "uint63 lsl" l_sl;
   Callback.register "uint63 lsr" l_sr;
+  Callback.register "uint63 asr" a_sr;
   Callback.register "uint63 lt" lt;
+  Callback.register "uint63 lts" lts;
   Callback.register "uint63 lxor" l_xor;
   Callback.register "uint63 mod" rem;
+  Callback.register "uint63 mods" rems;
   Callback.register "uint63 mul" mul;
   Callback.register "uint63 mulc_ml" mulc;
+  Callback.register "uint63 zero" zero;
   Callback.register "uint63 one" one;
   Callback.register "uint63 sub" sub;
+  Callback.register "uint63 neg" (sub zero);
   Callback.register "uint63 subcarry" subcarry;
   Callback.register "uint63 tail0" tail0;
   Callback.register "uint63 of_float" of_float;
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 *)
 
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index d3af8bf09b..caa263432e 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -226,8 +226,11 @@ let check_prim_op = function
   | Int63mul       -> opCHECKMULINT63
   | Int63div       -> opCHECKDIVINT63
   | Int63mod       -> opCHECKMODINT63
+  | Int63divs      -> opCHECKDIVSINT63
+  | Int63mods      -> opCHECKMODSINT63
   | Int63lsr       -> opCHECKLSRINT63
   | Int63lsl       -> opCHECKLSLINT63
+  | Int63asr       -> opCHECKASRINT63
   | Int63land      -> opCHECKLANDINT63
   | Int63lor       -> opCHECKLORINT63
   | Int63lxor      -> opCHECKLXORINT63
@@ -242,7 +245,10 @@ let check_prim_op = function
   | Int63eq        -> opCHECKEQINT63
   | Int63lt        -> opCHECKLTINT63
   | Int63le        -> opCHECKLEINT63
+  | Int63lts       -> opCHECKLTSINT63
+  | Int63les       -> opCHECKLESINT63
   | Int63compare   -> opCHECKCOMPAREINT63
+  | Int63compares  -> opCHECKCOMPARESINT63
   | Float64opp     -> opCHECKOPPFLOAT
   | Float64abs     -> opCHECKABSFLOAT
   | Float64eq      -> opCHECKEQFLOAT