Merge PR #6914: Primitive integers

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

7 files changed, 589 insertions, 275 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index be2b05da8d..0865487c98 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -36,20 +36,15 @@ void init_arity () {
     arity[PUSHACC6]=arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]=
     arity[ENVACC3]=arity[ENVACC4]=arity[PUSHENVACC1]=arity[PUSHENVACC2]=
     arity[PUSHENVACC3]=arity[PUSHENVACC4]=arity[APPLY1]=arity[APPLY2]=
-    arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]=
+    arity[APPLY3]=arity[APPLY4]=arity[RESTART]=arity[OFFSETCLOSUREM2]=
     arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]=
     arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]=
     arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]=
     arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
     arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
     arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= 
-    arity[ADDINT31]=arity[ADDCINT31]=arity[ADDCARRYCINT31]=
-    arity[SUBINT31]=arity[SUBCINT31]=arity[SUBCARRYCINT31]=
-    arity[MULCINT31]=arity[MULINT31]=arity[COMPAREINT31]=
-    arity[DIV21INT31]=arity[DIVINT31]=arity[ADDMULDIVINT31]=
-    arity[HEAD0INT31]=arity[TAIL0INT31]=
-    arity[COMPINT31]=arity[DECOMPINT31]=
-    arity[ORINT31]=arity[ANDINT31]=arity[XORINT31]=0;
+    arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]=
+    arity[ISINT]=arity[AREINT2]=0;
   /* instruction with one operand */
   arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
     arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=
@@ -58,10 +53,20 @@ void init_arity () {
     arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]=
     arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=
     arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=
-    arity[BRANCH]=arity[ISCONST]=arity[ENSURESTACKCAPACITY]=1;
+    arity[BRANCH]=arity[ENSURESTACKCAPACITY]=
+    arity[CHECKADDINT63]=arity[CHECKADDCINT63]=arity[CHECKADDCARRYCINT63]=
+    arity[CHECKSUBINT63]=arity[CHECKSUBCINT63]=arity[CHECKSUBCARRYCINT63]=
+    arity[CHECKMULINT63]=arity[CHECKMULCINT63]=
+    arity[CHECKDIVINT63]=arity[CHECKMODINT63]=arity[CHECKDIVEUCLINT63]=
+    arity[CHECKDIV21INT63]=
+    arity[CHECKLXORINT63]=arity[CHECKLORINT63]=arity[CHECKLANDINT63]=
+    arity[CHECKLSLINT63]=arity[CHECKLSRINT63]=arity[CHECKADDMULDIVINT63]=
+    arity[CHECKLSLINT63CONST1]=arity[CHECKLSRINT63CONST1]=
+    arity[CHECKEQINT63]=arity[CHECKLTINT63]=arity[CHECKLEINT63]=
+    arity[CHECKCOMPAREINT63]=arity[CHECKHEAD0INT63]=arity[CHECKTAIL0INT63]=1;
   /* instruction with two operands */
   arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
-  arity[ARECONST]=arity[PROJ]=2;
+  arity[PROJ]=2;
   /* instruction with four operands */ 
   arity[MAKESWITCHBLOCK]=4;
   /* instruction with arbitrary operands */
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index 638d6b5ab5..5a233e6178 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -29,6 +29,7 @@ void init_arity();
 value coq_tcode_of_code(value code);
 value coq_makeaccu (value i);
 value coq_pushpop (value i);
+value coq_accucond (value i);
 value coq_is_accumulate_code(value code);
 
 #endif /* _COQ_FIX_CODE_ */
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index d92e85fdf8..c7abedaed6 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -26,7 +26,7 @@ enum instructions {
   ENVACC1, ENVACC2, ENVACC3, ENVACC4, ENVACC,
   PUSHENVACC1, PUSHENVACC2, PUSHENVACC3, PUSHENVACC4, PUSHENVACC,
   PUSH_RETADDR,
-  APPLY, APPLY1, APPLY2, APPLY3,
+  APPLY, APPLY1, APPLY2, APPLY3, APPLY4,
   APPTERM, APPTERM1, APPTERM2, APPTERM3,
   RETURN, RESTART, GRAB, GRABREC, 
   CLOSURE, CLOSUREREC, CLOSURECOFIX,
@@ -46,15 +46,21 @@ enum instructions {
   MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, 
 /* spiwack: */
   BRANCH,
-  ADDINT31, ADDCINT31, ADDCARRYCINT31,
-  SUBINT31, SUBCINT31, SUBCARRYCINT31,
-  MULCINT31, MULINT31, DIV21INT31, DIVINT31,
-  ADDMULDIVINT31, COMPAREINT31, 
-  HEAD0INT31, TAIL0INT31,
-  ISCONST, ARECONST,
-  COMPINT31, DECOMPINT31,
-  ORINT31, ANDINT31, XORINT31,
-/* /spiwack  */
+  CHECKADDINT63, ADDINT63, CHECKADDCINT63, CHECKADDCARRYCINT63,
+  CHECKSUBINT63, SUBINT63, CHECKSUBCINT63, CHECKSUBCARRYCINT63,
+  CHECKMULINT63, CHECKMULCINT63,
+  CHECKDIVINT63, CHECKMODINT63, CHECKDIVEUCLINT63, CHECKDIV21INT63,
+  CHECKLXORINT63, CHECKLORINT63, CHECKLANDINT63,
+  CHECKLSLINT63, CHECKLSRINT63, CHECKADDMULDIVINT63,
+  CHECKLSLINT63CONST1, CHECKLSRINT63CONST1,
+
+  CHECKEQINT63, CHECKLTINT63, LTINT63, CHECKLEINT63, LEINT63,
+  CHECKCOMPAREINT63,
+
+  CHECKHEAD0INT63, CHECKTAIL0INT63,
+
+  ISINT, AREINT2,
+
   STOP
 };
 
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index a944dbb06c..d2c88bffcc 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -23,6 +23,12 @@
 #include "coq_memory.h" 
 #include "coq_values.h" 
 
+#ifdef ARCH_SIXTYFOUR
+#include "coq_uint63_native.h"
+#else
+#include "coq_uint63_emul.h"
+#endif
+
 /* spiwack: I append here a few macros for value/number manipulation */
 #define uint32_of_value(val) (((uint32_t)(val)) >> 1)
 #define value_of_uint32(i)   ((value)((((uint32_t)(i)) << 1) | 1))
@@ -155,6 +161,38 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #endif
 #endif
 
+#define CheckInt1() do{                            \
+    if (Is_uint63(accu)) pc++;			   \
+    else{					   \
+      *--sp=accu;				   \
+      accu = Field(coq_global_data, *pc++);	   \
+      goto apply1;				   \
+    }						   \
+  }while(0)
+
+#define CheckInt2() do{    			   \
+    if (Is_uint63(accu) && Is_uint63(sp[0])) pc++;	   \
+    else{					   \
+      *--sp=accu;				   \
+      accu = Field(coq_global_data, *pc++);	   \
+      goto apply2;				   \
+    }						   \
+  }while(0)
+
+
+
+#define CheckInt3() do{						      \
+    if (Is_uint63(accu) && Is_uint63(sp[0]) && Is_uint63(sp[1]) ) pc++;     \
+    else{							      \
+      *--sp=accu;						      \
+      accu = Field(coq_global_data, *pc++);			      \
+      goto apply3;						      \
+    }								      \
+  }while(0)
+
+#define AllocCarry(cond) Alloc_small(accu, 1, (cond)? coq_tag_C1 : coq_tag_C0)
+#define AllocPair() Alloc_small(accu, 2, coq_tag_pair)
+
 /* For signal handling, we hijack some code from the caml runtime */
 
 extern intnat caml_signals_are_pending;
@@ -372,8 +410,10 @@ value coq_interprete
 	goto check_stack;
       }
       Instruct(APPLY1) {
-	value arg1 = sp[0];
+        value arg1;
+      apply1:
 	print_instr("APPLY1");
+        arg1 = sp[0];
 	sp -= 3;
 	sp[0] = arg1;
 	sp[1] = (value)pc;
@@ -388,10 +428,14 @@ value coq_interprete
 	coq_extra_args = 0;
 	goto check_stack;
       }
+
       Instruct(APPLY2) {
-	value arg1 = sp[0];
-	value arg2 = sp[1];
+        value arg1;
+        value arg2;
+      apply2:
 	print_instr("APPLY2");
+        arg1 = sp[0];
+        arg2 = sp[1];
 	sp -= 3;
 	sp[0] = arg1;
 	sp[1] = arg2;
@@ -403,11 +447,16 @@ value coq_interprete
 	coq_extra_args = 1;
 	goto check_stack;
       }
+
       Instruct(APPLY3) {
-	value arg1 = sp[0];
-	value arg2 = sp[1];
-	value arg3 = sp[2];
+        value arg1;
+        value arg2;
+        value arg3;
+      apply3:
 	print_instr("APPLY3");
+        arg1 = sp[0];
+        arg2 = sp[1];
+        arg3 = sp[2];
 	sp -= 3;
 	sp[0] = arg1;
 	sp[1] = arg2;
@@ -420,7 +469,28 @@ value coq_interprete
 	coq_extra_args = 2;
 	goto check_stack;
       }
-      /* Stack checks */
+
+       Instruct(APPLY4) {
+        value arg1 = sp[0];
+        value arg2 = sp[1];
+        value arg3 = sp[2];
+        value arg4 = sp[3];
+        print_instr("APPLY4");
+        sp -= 3;
+        sp[0] = arg1;
+        sp[1] = arg2;
+        sp[2] = arg3;
+        sp[3] = arg4;
+        sp[4] = (value)pc;
+        sp[5] = coq_env;
+        sp[6] = Val_long(coq_extra_args);
+        pc = Code_val(accu);
+        coq_env = accu;
+        coq_extra_args = 3;
+        goto check_stack;
+      }
+
+     /* Stack checks */
       
     check_stack:
       print_instr("check_stack");
@@ -1127,7 +1197,6 @@ value coq_interprete
 	Next;
       }
 
-      /* spiwack: code for interpreting compiled integers */
       Instruct(BRANCH) {
 	/* unconditional branching */
         print_instr("BRANCH");
@@ -1136,338 +1205,339 @@ value coq_interprete
         Next;
       }
 
-      Instruct(ADDINT31) {
+      Instruct(CHECKADDINT63){
+        print_instr("CHECKADDINT63");
+        CheckInt2();
+      }
+      Instruct(ADDINT63) {
         /* Adds the integer in the accumulator with 
            the one ontop of the stack (which is poped)*/
-        print_instr("ADDINT31");
-        accu = 
-           (value)((uint32_t) accu + (uint32_t) *sp++ - 1); 
-        /* nota,unlike CaML we don't want
-           to have a different behavior depending on the 
-           architecture. Thus we cast the operand to uint32 */
+        print_instr("ADDINT63");
+        accu = uint63_add(accu, *sp++);
         Next;
       }
 
-      Instruct (ADDCINT31) {
-	print_instr("ADDCINT31");
+      Instruct (CHECKADDCINT63) {
+        print_instr("CHECKADDCINT63");
+        CheckInt2();
 	/* returns the sum with a carry */
-	uint32_t s;
-	s = (uint32_t)accu + (uint32_t)*sp++ - 1;
-        if( (uint32_t)s < (uint32_t)accu ) {
-          /* carry */
-	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
-	}
-	else {
-	  /*no carry */
-	  Alloc_small(accu, 1, 1);
-	}
-	Field(accu, 0)=(value)s;
+        value s;
+        s = uint63_add(accu, *sp++);
+        AllocCarry(uint63_lt(s,accu));
+        Field(accu, 0) = s;
 	Next;
       }
 
-      Instruct (ADDCARRYCINT31) {
-	print_instr("ADDCARRYCINT31");
+      Instruct (CHECKADDCARRYCINT63) {
+        print_instr("ADDCARRYCINT63");
+        CheckInt2();
 	/* returns the sum plus one with a carry */
-	uint32_t s;
-	s = (uint32_t)accu + (uint32_t)*sp++ + 1;
-        if( (uint32_t)s <= (uint32_t)accu ) {
-          /* carry */
-	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
-	}
-	else {
-	  /*no carry */
-	  Alloc_small(accu, 1, 1);
-	}
-	Field(accu, 0)=(value)s;
+        value s;
+        s = uint63_addcarry(accu, *sp++);
+        AllocCarry(uint63_leq(s, accu));
+        Field(accu, 0) = s;
 	Next;
       }
 
-      Instruct (SUBINT31) {
-	print_instr("SUBINT31");
+      Instruct (CHECKSUBINT63) {
+        print_instr("CHECKSUBINT63");
+        CheckInt2();
+      }
+      Instruct (SUBINT63) {
+        print_instr("SUBINT63");
 	/* returns the subtraction */
-	accu = 
-	  (value)((uint32_t) accu - (uint32_t) *sp++ + 1); 
+        accu = uint63_sub(accu, *sp++);
         Next;
       }
 
-      Instruct (SUBCINT31) {
-	print_instr("SUBCINT31");
+      Instruct (CHECKSUBCINT63) {
+        print_instr("SUBCINT63");
+        CheckInt2();
 	/* returns the subtraction with a carry */
-	uint32_t b;
-	uint32_t s;
-	b = (uint32_t)*sp++;
-	s = (uint32_t)accu - b + 1;
-        if( (uint32_t)accu < b ) {
-          /* carry */
-	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
-	}
-	else {
-	  /*no carry */
-	  Alloc_small(accu, 1, 1);
-	}
-	Field(accu, 0)=(value)s;
+        value b;
+        value s;
+        b = *sp++;
+        s = uint63_sub(accu,b);
+        AllocCarry(uint63_lt(accu,b));
+        Field(accu, 0) = s;
 	Next;
       }
 
-      Instruct (SUBCARRYCINT31) {
-	print_instr("SUBCARRYCINT31");
+      Instruct (CHECKSUBCARRYCINT63) {
+        print_instr("SUBCARRYCINT63");
+        CheckInt2();
 	/* returns the subtraction minus one with a carry */
-	uint32_t b;
-	uint32_t s;
-	b = (uint32_t)*sp++;
-	s = (value)((uint32_t)accu - b - 1);
-        if( (uint32_t)accu <= b ) {
-          /* carry */
-	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
-	}
-	else {
-	  /*no carry */
-	  Alloc_small(accu, 1, 1);
-	}
-	Field(accu, 0)=(value)s;
+        value b;
+        value s;
+        b = *sp++;
+        s = uint63_subcarry(accu,b);
+        AllocCarry(uint63_leq(accu,b));
+        Field(accu, 0) = s;
 	Next;
       }
 
-      Instruct (MULINT31) {
+      Instruct (CHECKMULINT63) {
+        print_instr("MULINT63");
+        CheckInt2();
 	/* returns the multiplication */
-	print_instr("MULINT31");
-        accu = 
-	  value_of_uint32((uint32_of_value(accu)) * (uint32_of_value(*sp++)));
+        accu = uint63_mul(accu,*sp++);
 	Next;
       }
 
-      Instruct (MULCINT31) {
-        /*returns the multiplication on a double size word
-          (special case for 0) */
-        print_instr("MULCINT31");
-	uint64_t p;
+      Instruct (CHECKMULCINT63) {
+        /*returns the multiplication on a pair */
+        print_instr("MULCINT63");
+        CheckInt2();
         /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */
-        p = UI64_of_value (accu) * UI64_of_uint32 ((*sp++)^1);
-	if (p == 0) {
-	  accu = (value)1;
+        /* TODO: implement
+        p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1));
+        AllocPair(); */
+        /* Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; */ /*higher part*/
+        /* Field(accu, 1) = (value)(I64_to_int32(p)|1); */ /*lower part*/
+        value x = accu;
+        AllocPair();
+        Field(accu, 1) = uint63_mulc(x, *sp++, &Field(accu, 0));
+        Next;
+      }
+
+      Instruct(CHECKDIVINT63) {
+        print_instr("CHEKDIVINT63");
+        CheckInt2();
+        /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag
+                    since it probably only concerns negative number.
+                    needs to be checked at this point */
+        value divisor;
+        divisor = *sp++;
+        if (uint63_eq0(divisor)) {
+          accu = divisor;
 	}
 	else {
-          /* the output type is supposed to have a constant constructor
-	     and a non-constant constructor (in that order), the tag
-	     of the non-constant constructor is then 1 */
-	  Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-	  /*unsigned shift*/
-	  Field(accu, 0) = (value)((p >> 31)|1) ;  /*higher part*/
-	  Field(accu, 1) = (value)((uint32_t)p|1); /*lower part*/
-	}
+          accu = uint63_div(accu, divisor);
+        }
 	Next;
       }
 
-      Instruct (DIV21INT31) {
-	print_instr("DIV21INT31");
-	/* spiwack: takes three int31 (the two first ones represent an
-                    int62) and performs the euclidian division of the
-                    int62 by the int31 */
-        uint64_t bigint;
-        bigint = UI64_of_value(accu);
-        bigint = (bigint << 31) | UI64_of_value(*sp++);
-        uint64_t divisor;
-        divisor = UI64_of_value(*sp++);
-        Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-        if (divisor == 0) {
-          Field(accu, 0) = 1; /* 2*0+1 */
-          Field(accu, 1) = 1; /* 2*0+1 */
+      Instruct(CHECKMODINT63) {
+        print_instr("CHEKMODINT63");
+        CheckInt2();
+        value divisor;
+        divisor = *sp++;
+        if (uint63_eq0(divisor)) {
+          accu = divisor;
 	}
-	else {
-	  uint64_t quo, mod;
-	  quo = bigint / divisor;
-	  mod = bigint % divisor;
-          Field(accu, 0) = value_of_uint32((uint32_t)(quo));
-	  Field(accu, 1) = value_of_uint32((uint32_t)(mod));
+        else {
+          accu = uint63_mod(accu,divisor);
 	}
 	Next;
       }
 
-      Instruct (DIVINT31) {
-	print_instr("DIVINT31");
+      Instruct (CHECKDIVEUCLINT63) {
+        print_instr("DIVEUCLINT63");
+        CheckInt2();
         /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag
                     since it probably only concerns negative number.
                     needs to be checked at this point */
-        uint32_t divisor;
-        divisor = uint32_of_value(*sp++);
-        if (divisor == 0) { 
+        value divisor;
+        divisor = *sp++;
+        if (uint63_eq0(divisor)) {
           Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-	  Field(accu, 0) = 1; /* 2*0+1 */
-          Field(accu, 1) = 1; /* 2*0+1 */
+          Field(accu, 0) = divisor;
+          Field(accu, 1) = divisor;
         }
         else {
-          uint32_t modulus;
-          modulus = uint32_of_value(accu);
+          value modulus;
+          modulus = accu;
           Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-	  Field(accu, 0) = value_of_uint32(modulus/divisor);
-          Field(accu, 1) = value_of_uint32(modulus%divisor);
+          Field(accu, 0) = uint63_div(modulus,divisor);
+          Field(accu, 1) = uint63_mod(modulus,divisor);
         }
 	Next;
       }
 
-      Instruct (ADDMULDIVINT31) {
-        print_instr("ADDMULDIVINT31");
-        /* higher level shift (does shifts and cycles and such) */
-        uint32_t shiftby;
-        shiftby = uint32_of_value(accu);
-        if (shiftby > 31) {
-          if (shiftby < 62) {
-            sp++;
-	    accu = (value)(((((uint32_t)*sp++)^1) << (shiftby - 31)) | 1);
-          }
-          else {
-            sp+=2;
-            accu = (value)(1);
-          }
+      Instruct (CHECKDIV21INT63) {
+        print_instr("DIV21INT63");
+        CheckInt3();
+        /* spiwack: takes three int31 (the two first ones represent an
+                    int62) and performs the euclidian division of the
+                    int62 by the int31 */
+        /* TODO: implement this
+        bigint = UI64_of_value(accu);
+        bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++));
+        uint64 divisor;
+        divisor = UI64_of_value(*sp++);
+        Alloc_small(accu, 2, 1); */ /* ( _ , arity, tag ) */
+        /* if (I64_is_zero (divisor)) {
+           Field(accu, 0) = 1; */ /* 2*0+1 */
+        /* Field(accu, 1) = 1; */ /* 2*0+1 */
+        /* }
+        else {
+          uint64 quo, mod;
+          I64_udivmod(bigint, divisor, &quo, &mod);
+          Field(accu, 0) = value_of_uint32(I64_to_int32(quo));
+          Field(accu, 1) = value_of_uint32(I64_to_int32(mod));
+        } */
+        value bigint; /* TODO: fix */
+        bigint = *sp++; /* TODO: take accu into account */
+        value divisor;
+        divisor = *sp++;
+        if (uint63_eq0(divisor)) {
+          Alloc_small(accu, 2, 1);
+          Field(accu, 0) = divisor;
+          Field(accu, 1) = divisor;
 	}
-        else{
-        /* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */
-	  accu = (value)((((uint32_t)*sp++)^1) << shiftby);
-        /* accu = 2^(shiftby+1)*x --> 2^(shifby+1)*x+2*y/2^(31-shiftby)+1 */
-        accu = (value)((accu | (((uint32_t)(*sp++)) >> (31-shiftby)))|1);
+        else {
+          value quo, mod;
+          mod = uint63_div21(accu, bigint, divisor, &quo);
+          Alloc_small(accu, 2, 1);
+          Field(accu, 0) = quo;
+          Field(accu, 1) = mod;
 	}
         Next;
       }
 
-      Instruct (COMPAREINT31) {
-	/* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
-	/* assumes Inductive _ : _ := Eq | Lt | Gt */
-	print_instr("COMPAREINT31");
-	if ((uint32_t)accu == (uint32_t)*sp) {
-	  accu = 1;  /* 2*0+1 */
-	  sp++;
-	}
-	else{if ((uint32_t)accu < (uint32_t)(*sp++)) {
-	  accu = 3;  /* 2*1+1 */
-	}
-	else{
-	  accu = 5;   /* 2*2+1 */
-	}}
+      Instruct(CHECKLXORINT63) {
+        print_instr("CHECKLXORINT63");
+        CheckInt2();
+        accu = uint63_lxor(accu,*sp++);
         Next;
       }
- 
-      Instruct (HEAD0INT31) {
-	int r = 0;
-        uint32_t x;
-        print_instr("HEAD0INT31");
-	x = (uint32_t) accu;
-        if (!(x & 0xFFFF0000)) { x <<= 16; r += 16; }
-        if (!(x & 0xFF000000)) { x <<= 8;  r += 8; }
-        if (!(x & 0xF0000000)) { x <<= 4;  r += 4; }
-        if (!(x & 0xC0000000)) { x <<= 2;  r += 2; }
-        if (!(x & 0x80000000)) { x <<=1;   r += 1; }
-        if (!(x & 0x80000000)) {           r += 1; }
-        accu = value_of_uint32(r);
+
+      Instruct(CHECKLORINT63) {
+        print_instr("CHECKLORINT63");
+        CheckInt2();
+        accu = uint63_lor(accu,*sp++);
         Next;
       }
-        
-      Instruct (TAIL0INT31) {
-	int r = 0;
-        uint32_t x;
-        print_instr("TAIL0INT31");
-	x = (((uint32_t) accu >> 1) | 0x80000000);
-        if (!(x & 0xFFFF)) { x >>= 16; r += 16; }
-        if (!(x & 0x00FF)) { x >>= 8;  r += 8; }
-        if (!(x & 0x000F)) { x >>= 4;  r += 4; }
-        if (!(x & 0x0003)) { x >>= 2;  r += 2; }
-        if (!(x & 0x0001)) { x >>=1;   r += 1; }
-        if (!(x & 0x0001)) {           r += 1; }
-        accu = value_of_uint32(r);
+
+      Instruct(CHECKLANDINT63) {
+        print_instr("CHECKLANDINT63");
+        CheckInt2();
+        accu = uint63_land(accu,*sp++);
         Next;
       }
 
-      Instruct (ISCONST) {
-        /* Branches if the accu does not contain a constant
-           (i.e., a non-block value) */
-        print_instr("ISCONST");
-        if ((accu & 1) == 0) /* last bit is 0 -> it is a block */
-	  pc +=  *pc;
-        else
-	  pc++;
+      Instruct(CHECKLSLINT63) {
+        print_instr("CHECKLSLINT63");
+        CheckInt2();
+        value p = *sp++;
+        accu = uint63_lsl(accu,p);
         Next;
+      }
 
+      Instruct(CHECKLSRINT63) {
+        print_instr("CHECKLSRINT63");
+        CheckInt2();
+        value p = *sp++;
+        accu = uint63_lsr(accu,p);
+        Next;
       }
 
-      Instruct (ARECONST) {
-        /* Branches if the n first values on the stack are not
-           all constansts */
-        print_instr("ARECONST");
-        int i, n, ok;
-        ok = 1;
-        n = *pc++;
-        for(i=0; i < n; i++) {
-          if ((sp[i] & 1) == 0) {
-	    ok = 0;
-            break;
-          }
+      Instruct(CHECKLSLINT63CONST1) {
+        print_instr("CHECKLSLINT63CONST1");
+        if (Is_uint63(accu)) {
+          pc++;
+          accu = uint63_lsl1(accu);
+          Next;
+        } else {
+          *--sp = uint63_one();
+          *--sp = accu;
+          accu = Field(coq_global_data, *pc++);
+          goto apply2;
         }
-        if(ok) pc++; else pc += *pc;
+      }
+
+      Instruct(CHECKLSRINT63CONST1) {
+        print_instr("CHECKLSRINT63CONST1");
+        if (Is_uint63(accu)) {
+          pc++;
+          accu = uint63_lsr1(accu);
+          Next;
+        } else {
+          *--sp = uint63_one();
+          *--sp = accu;
+          accu = Field(coq_global_data, *pc++);
+          goto apply2;
+        }
+      }
+
+      Instruct (CHECKADDMULDIVINT63) {
+        print_instr("CHECKADDMULDIVINT63");
+        CheckInt3();
+        value x;
+        value y;
+        x = *sp++;
+        y = *sp++;
+        accu = uint63_addmuldiv(accu,x,y);
         Next;
       }
 
-      Instruct (COMPINT31) {
-        /* makes an 31-bit integer out of the accumulator and
-           the 30 first values of the stack 
-           and put it in the accumulator (the accumulator then the 
-           topmost get to be the heavier bits) */
-        print_instr("COMPINT31");
-        int i;
-        /*accu=accu or accu = (value)((unsigned long)1-accu) if bool
-	               is used for the bits */
-        for(i=0; i < 30; i++) {
-	  accu = (value) ((((uint32_t)accu-1) << 1) | *sp++);
-          /* -1 removes the tag bit, << 1 multiplies the value by 2, 
-              | *sp++ pops the last value and add it (no carry involved)
-	      not that it reintroduces a tag bit */
-          /* alternative, if bool is used for the bits :
-	     accu = (value) ((((unsigned long)accu) << 1) & !*sp++); */
+      Instruct (CHECKEQINT63) {
+        print_instr("CHECKEQINT63");
+        CheckInt2();
+        accu = uint63_eq(accu,*sp++) ? coq_true : coq_false;
+        Next;
+      }
+
+     Instruct (CHECKLTINT63) {
+        print_instr("CHECKLTINT63");
+        CheckInt2();
+     }
+     Instruct (LTINT63) {
+       print_instr("LTINT63");
+       accu = uint63_lt(accu,*sp++) ? coq_true : coq_false;
+       Next;
+     }
+
+     Instruct (CHECKLEINT63) {
+       print_instr("CHECKLEINT63");
+       CheckInt2();
+     }
+     Instruct (LEINT63) {
+       print_instr("LEINT63");
+       accu = uint63_leq(accu,*sp++) ? 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 */
+        print_instr("CHECKCOMPAREINT63");
+        CheckInt2();
+        if (uint63_eq(accu,*sp)) {
+          accu = coq_Eq;
+          sp++;
         }
+        else accu = uint63_lt(accu,*sp++) ? coq_Lt : coq_Gt;
         Next;
       }
 
-      Instruct (DECOMPINT31) {
-        /* builds a block out of a 31-bit integer (from the accumulator), 
-           used before cases */
-        int i;
-	value block;
-	print_instr("DECOMPINT31");
-        Alloc_small(block, 31, 1); // Alloc_small(*, size, tag)
-        for(i = 30; i >= 0; i--) {
-          Field(block, i) = (value)(accu & 3); /* two last bits of the accumulator */
-          //Field(block, i) = 3;
-          accu = (value) ((uint32_t)accu >> 1) | 1;  /* last bit must be a one */
-        };
-	accu = block;
+      Instruct (CHECKHEAD0INT63) {
+        print_instr("CHECKHEAD0INT63");
+        CheckInt1();
+        accu = uint63_head0(accu);
         Next;
       }
 
-      Instruct (ORINT31) {
-	/* returns the bitwise or */
-	print_instr("ORINT31");
-        accu =
-	  value_of_uint32((uint32_of_value(accu)) | (uint32_of_value(*sp++)));
-	Next;
+      Instruct (CHECKTAIL0INT63) {
+        print_instr("CHECKTAIL0INT63");
+        CheckInt1();
+        accu = uint63_tail0(accu);
+        Next;
       }
 
-      Instruct (ANDINT31) {
-	/* returns the bitwise and */
-	print_instr("ANDINT31");
-        accu =
-	  value_of_uint32((uint32_of_value(accu)) & (uint32_of_value(*sp++)));
+      Instruct (ISINT){
+        print_instr("ISINT");
+        accu = (Is_uint63(accu)) ? coq_true : coq_false;
 	Next;
       }
 
-      Instruct (XORINT31) {
-	/* returns the bitwise xor */
-	print_instr("XORINT31");
-        accu =
-	  value_of_uint32((uint32_of_value(accu)) ^ (uint32_of_value(*sp++)));
+      Instruct (AREINT2){
+        print_instr("AREINT2");
+        accu = (Is_uint63(accu) && Is_uint63(sp[0])) ? coq_true : coq_false;
+        sp++;
 	Next;
       }
 
-      /*  /spiwack   */
-
-
 
 /* Debugging and machine control */
 
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
new file mode 100644
index 0000000000..5499f124a2
--- /dev/null
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -0,0 +1,97 @@
+# pragma once
+
+# include <caml/callback.h>
+# include <caml/stack.h>
+
+
+#define Is_uint63(v) (Tag_val(v) == Custom_tag)
+
+# define DECLARE_NULLOP(name) \
+value uint63_##name() { \
+  static value* cb = 0; \
+  CAMLparam0(); \
+  if (!cb) cb = caml_named_value("uint63 " #name); \
+  CAMLreturn(*cb); \
+  }
+
+# define DECLARE_UNOP(name) \
+value uint63_##name(value x) { \
+  static value* cb = 0; \
+  CAMLparam1(x); \
+  if (!cb) cb = caml_named_value("uint63 " #name); \
+  CAMLreturn(caml_callback(*cb, x)); \
+  }
+
+# define DECLARE_PREDICATE(name) \
+value uint63_##name(value x) { \
+  static value* cb = 0; \
+  CAMLparam1(x); \
+  if (!cb) cb = caml_named_value("uint63 " #name); \
+  CAMLreturn(Int_val(caml_callback(*cb, x))); \
+  }
+
+# define DECLARE_BINOP(name) \
+value uint63_##name(value x, value y) { \
+  static value* cb = 0; \
+  CAMLparam2(x, y); \
+  if (!cb) cb = caml_named_value("uint63 " #name); \
+  CAMLreturn(caml_callback2(*cb, x, y)); \
+  }
+
+# define DECLARE_RELATION(name) \
+value uint63_##name(value x, value y) { \
+  static value* cb = 0; \
+  CAMLparam2(x, y); \
+  if (!cb) cb = caml_named_value("uint63 " #name); \
+  CAMLreturn(Int_val(caml_callback2(*cb, x, y))); \
+  }
+
+# define DECLARE_TEROP(name) \
+value uint63_##name(value x, value y, value z) { \
+  static value* cb = 0; \
+  CAMLparam3(x, y, z); \
+  if (!cb) cb = caml_named_value("uint63 " #name); \
+  CAMLreturn(caml_callback3(*cb, x, y, z)); \
+  }
+
+
+DECLARE_NULLOP(one)
+DECLARE_BINOP(add)
+DECLARE_BINOP(addcarry)
+DECLARE_TEROP(addmuldiv)
+DECLARE_BINOP(div)
+DECLARE_TEROP(div21_ml)
+DECLARE_RELATION(eq)
+DECLARE_PREDICATE(eq0)
+DECLARE_UNOP(head0)
+DECLARE_BINOP(land)
+DECLARE_RELATION(leq)
+DECLARE_BINOP(lor)
+DECLARE_BINOP(lsl)
+DECLARE_UNOP(lsl1)
+DECLARE_BINOP(lsr)
+DECLARE_UNOP(lsr1)
+DECLARE_RELATION(lt)
+DECLARE_BINOP(lxor)
+DECLARE_BINOP(mod)
+DECLARE_BINOP(mul)
+DECLARE_BINOP(mulc_ml)
+DECLARE_BINOP(sub)
+DECLARE_BINOP(subcarry)
+DECLARE_UNOP(tail0)
+
+value uint63_div21(value x, value y, value z, value* q) {
+  CAMLparam3(x, y, z);
+  CAMLlocal1(qr);
+  qr = uint63_div21_ml(x, y, z);
+  *q = Field(qr, 0);
+  CAMLreturn(Field(qr, 1));
+}
+
+value uint63_mulc(value x, value y, value* h) {
+  CAMLparam2(x, y);
+  CAMLlocal1(hl);
+  hl = uint63_mulc_ml(x, y);
+  *h = Field(hl, 0);
+  CAMLreturn(Field(hl, 1));
+}
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
new file mode 100644
index 0000000000..92f4dc79bc
--- /dev/null
+++ b/kernel/byterun/coq_uint63_native.h
@@ -0,0 +1,125 @@
+#define Is_uint63(v) (Is_long(v))
+
+#define uint63_of_value(val) ((uint64_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_one() ((value) 3) /* 2*1 + 1 */
+
+#define uint63_eq(x,y) ((x) == (y))
+#define uint63_eq0(x) ((x) == (uint64_t)1)
+#define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y))
+#define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y))
+
+#define uint63_add(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) - 1))
+#define uint63_addcarry(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) + 1))
+#define uint63_sub(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) + 1))
+#define uint63_subcarry(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) - 1))
+#define uint63_mul(x,y) (Val_long(uint63_of_value(x) * uint63_of_value(y)))
+#define uint63_div(x,y) (Val_long(uint63_of_value(x) / uint63_of_value(y)))
+#define uint63_mod(x,y) (Val_long(uint63_of_value(x) % uint63_of_value(y)))
+
+#define uint63_lxor(x,y) ((value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1))
+#define uint63_lor(x,y) ((value)((uint64_t)(x) | (uint64_t)(y)))
+#define uint63_land(x,y) ((value)((uint64_t)(x) & (uint64_t)(y)))
+
+/* TODO: is + or | better? OCAML uses + */
+/* TODO: is - or ^ better? */
+#define uint63_lsl(x,y) ((y) < (uint64_t) 127 ? ((value)((((uint64_t)(x)-1) << (uint63_of_value(y))) | 1)) : uint63_zero)
+#define uint63_lsr(x,y) ((y) < (uint64_t) 127 ? ((value)(((uint64_t)(x) >> (uint63_of_value(y))) | 1)) : uint63_zero)
+#define uint63_lsl1(x) ((value)((((uint64_t)(x)-1) << 1) +1))
+#define uint63_lsr1(x) ((value)(((uint64_t)(x) >> 1) |1))
+
+/* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */
+/* (modulo 2^63) for p <= 63 */
+value uint63_addmuldiv(uint64_t p, uint64_t x, uint64_t y) {
+  uint64_t shiftby = uint63_of_value(p);
+  value r = (value)((uint64_t)(x^1) << shiftby);
+  r |= ((uint64_t)y >> (63-shiftby)) | 1;
+  return r;
+}
+
+value uint63_head0(uint64_t x) {
+  int r = 0;
+  if (!(x & 0xFFFFFFFF00000000)) { x <<= 32; r += 32; }
+  if (!(x & 0xFFFF000000000000)) { x <<= 16; r += 16; }
+  if (!(x & 0xFF00000000000000)) { x <<= 8;  r += 8; }
+  if (!(x & 0xF000000000000000)) { x <<= 4;  r += 4; }
+  if (!(x & 0xC000000000000000)) { x <<= 2;  r += 2; }
+  if (!(x & 0x8000000000000000)) { x <<=1;   r += 1; }
+  return Val_int(r);
+}
+
+value uint63_tail0(value x) {
+  int r = 0;
+  x = (uint64_t)x >> 1;
+  if (!(x & 0xFFFFFFFF)) { x >>= 32; r += 32; }
+  if (!(x & 0x0000FFFF)) { x >>= 16; r += 16; }
+  if (!(x & 0x000000FF)) { x >>= 8;  r += 8; }
+  if (!(x & 0x0000000F)) { x >>= 4;  r += 4; }
+  if (!(x & 0x00000003)) { x >>= 2;  r += 2; }
+  if (!(x & 0x00000001)) { x >>=1;   r += 1; }
+  return Val_int(r);
+}
+
+value uint63_mulc(value x, value y, value* h) {
+  x = (uint64_t)x >> 1;
+  y = (uint64_t)y >> 1;
+  uint64_t lx = x & 0xFFFFFFFF;
+  uint64_t ly = y & 0xFFFFFFFF;
+  uint64_t hx = x >> 32;
+  uint64_t hy = y >> 32;
+  uint64_t hr = hx * hy;
+  uint64_t lr = lx * ly;
+  lx *= hy;
+  ly *= hx;
+  hr += (lx >> 32) + (ly >> 32);
+  lx <<= 32;
+  lr += lx;
+  if (lr < lx) { hr++; }
+  ly <<= 32;
+  lr += ly;
+  if (lr < ly) { hr++; }
+  hr = (hr << 1) | (lr >> 63);
+  *h = Val_int(hr);
+  return Val_int(lr);
+}
+
+#define lt128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_lt(xl,yl)))
+#define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl)))
+
+value uint63_div21(value xh, value xl, value y, value* q) {
+  xh = (uint64_t)xh >> 1;
+  xl = ((uint64_t)xl >> 1) | ((uint64_t)xh << 63);
+  xh = (uint64_t)xh >> 1;
+  uint64_t maskh = 0;
+  uint64_t maskl = 1;
+  uint64_t dh = 0;
+  uint64_t dl = (uint64_t)y >> 1;
+  int cmp = 1;
+  while (dh >= 0 && cmp) {
+    cmp = lt128(dh,dl,xh,xl);
+    dh = (dh << 1) | (dl >> 63);
+    dl = dl << 1;
+    maskh = (maskh << 1) | (maskl >> 63);
+    maskl = maskl << 1;
+  }
+  uint64_t remh = xh;
+  uint64_t reml = xl;
+  uint64_t quotient = 0;
+  while (maskh | maskl) {
+    if (le128(dh,dl,remh,reml)) {
+      quotient = quotient | maskl;
+      if (uint63_lt(reml,dl)) {remh = remh - dh - 1;} else {remh = remh - dh;}
+      reml = reml - dl;
+    }
+    maskl = (maskl >> 1) | (maskh << 63);
+    maskh = maskh >> 1;
+    dl = (dl >> 1) | (dh << 63);
+    dh = dh >> 1;
+  }
+  *q = Val_int(quotient);
+  return Val_int(reml);
+}
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index bb0f0eb5e4..0cf6ccf532 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -28,6 +28,16 @@
 
 /* Les blocs accumulate */
 #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
-
 #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
+
+/* */
+#define coq_tag_C1 2
+#define coq_tag_C0 1
+#define coq_tag_pair 1
+#define coq_true Val_int(0)
+#define coq_false Val_int(1)
+#define coq_Eq Val_int(0)
+#define coq_Lt Val_int(1)
+#define coq_Gt Val_int(2)
+
 #endif /* _COQ_VALUES_ */