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.

3 files changed, 112 insertions, 3 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) */