Merge PR #13559: Signed primitive integers

Reviewed-by: SkySkimmer
Reviewed-by: silene
Reviewed-by: jfehrle
Ack-by: gares
Ack-by: Zimmi48
Ack-by: proux01

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) */