Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh

6 files changed, 47 insertions, 377 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 399fa843f1..bf383a33ac 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -22,18 +22,10 @@
 #include "coq_memory.h" 
 #include "coq_values.h" 
 
-/*spiwack : imports support functions for 64-bit integers */
-#include <caml/config.h>
-#ifdef ARCH_INT64_TYPE
-#include "int64_native.h"
-#else
-#include "int64_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))
-#define UI64_of_uint32(lo)  ((uint64_t)(I64_literal(0,(uint32_t)(lo))))
+#define UI64_of_uint32(lo) ((uint64_t)(lo))
 #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val)))
 /* /spiwack */
 
@@ -341,6 +333,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(ENVACC){
 	print_instr("ENVACC");
+	print_int(*pc);
 	accu = Field(coq_env, *pc++);
         Next;
       }
@@ -371,6 +364,10 @@ value coq_interprete
 	sp[1] = (value)pc;
 	sp[2] = coq_env;
 	sp[3] = Val_long(coq_extra_args);
+	print_instr("call stack=");
+	print_lint(sp[1]);
+	print_lint(sp[2]);
+	print_lint(sp[3]);
 	pc = Code_val(accu);
 	coq_env = accu;
 	coq_extra_args = 0;
@@ -458,6 +455,7 @@ value coq_interprete
 	sp[0] = arg1;
 	sp[1] = arg2;
 	pc = Code_val(accu);
+	print_lint(accu);
 	coq_env = accu;
 	coq_extra_args += 1;
 	goto check_stacks;
@@ -481,11 +479,18 @@ value coq_interprete
 	print_instr("RETURN");
 	print_int(*pc);
 	sp += *pc++;
+	print_instr("stack=");
+	print_lint(sp[0]);
+	print_lint(sp[1]);
+	print_lint(sp[2]);
 	if (coq_extra_args > 0) {
+	  print_instr("extra args > 0");
+	  print_lint(coq_extra_args);
 	  coq_extra_args--;
 	  pc = Code_val(accu);
 	  coq_env = accu;
 	} else {
+	  print_instr("extra args = 0");
 	  pc = (code_t)(sp[0]);
 	  coq_env = sp[1];
 	  coq_extra_args = Long_val(sp[2]);
@@ -585,7 +590,10 @@ value coq_interprete
 	Alloc_small(accu, 1 + nvars, Closure_tag);
 	Code_val(accu) = pc + *pc;
 	pc++;
-	for (i = 0; i < nvars; i++) Field(accu, i + 1) = sp[i];
+	for (i = 0; i < nvars; i++) {
+	  print_lint(sp[i]);
+	  Field(accu, i + 1) = sp[i];
+	}
 	sp += nvars;
 	Next;
       }
@@ -720,6 +728,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(GETGLOBAL){
 	print_instr("GETGLOBAL");
+	print_int(*pc);
 	accu = Field(coq_global_data, *pc);
         pc++;
         Next;
@@ -732,7 +741,7 @@ value coq_interprete
 	tag_t tag = *pc++;
 	mlsize_t i;
 	value block;
-	print_instr("MAKEBLOCK");
+	print_instr("MAKEBLOCK, tag=");
 	Alloc_small(block, wosize, tag);
 	Field(block, 0) = accu;
 	for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
@@ -743,7 +752,8 @@ value coq_interprete
 	
 	tag_t tag = *pc++;
 	value block;
-	print_instr("MAKEBLOCK1");
+	print_instr("MAKEBLOCK1, tag=");
+	print_int(tag);
 	Alloc_small(block, 1, tag);
 	Field(block, 0) = accu;
 	accu = block;
@@ -753,7 +763,8 @@ value coq_interprete
 	
 	tag_t tag = *pc++;
 	value block;
-	print_instr("MAKEBLOCK2");
+	print_instr("MAKEBLOCK2, tag=");
+	print_int(tag);
 	Alloc_small(block, 2, tag);
 	Field(block, 0) = accu;
 	Field(block, 1) = sp[0];
@@ -764,7 +775,8 @@ value coq_interprete
       Instruct(MAKEBLOCK3) {
 	tag_t tag = *pc++;
 	value block;
-	print_instr("MAKEBLOCK3");
+	print_instr("MAKEBLOCK3, tag=");
+	print_int(tag);
 	Alloc_small(block, 3, tag);
 	Field(block, 0) = accu;
 	Field(block, 1) = sp[0];
@@ -776,7 +788,8 @@ value coq_interprete
       Instruct(MAKEBLOCK4) {
 	tag_t tag = *pc++;
 	value block;
-	print_instr("MAKEBLOCK4");
+	print_instr("MAKEBLOCK4, tag=");
+	print_int(tag);
 	Alloc_small(block, 4, tag);
 	Field(block, 0) = accu;
 	Field(block, 1) = sp[0];
@@ -844,7 +857,6 @@ value coq_interprete
       }
 	
       Instruct(SETFIELD1){
-        int i, j, size, size_aux;
 	print_instr("SETFIELD1");
 	caml_modify(&Field(accu, 1),*sp);
        	sp++;
@@ -884,19 +896,17 @@ value coq_interprete
       Instruct(PROJ){
 	print_instr("PROJ");
 	if (Is_accu (accu)) {
+          value block;
 	  /* Skip over the index of projected field */
 	  pc++;
-	  /* Save the argument on the stack */
-	  *--sp = accu;
 	  /* Create atom */
-	  Alloc_small(accu, 2, ATOM_PROJ_TAG);
-	  Field(accu, 0) = Field(coq_global_data, *pc);
-	  Field(accu, 1) = sp[0];
-	  sp[0] = accu;
+	  Alloc_small(block, 2, ATOM_PROJ_TAG);
+	  Field(block, 0) = Field(coq_global_data, *pc);
+	  Field(block, 1) = accu;
 	  /* Create accumulator */
 	  Alloc_small(accu, 2, Accu_tag);
 	  Code_val(accu) = accumulate;
-	  Field(accu,1) = *sp++;
+	  Field(accu, 1) = block;
 	} else {
 	    accu = Field(accu, *pc++);
 	}
@@ -943,6 +953,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(CONSTINT) {
 	print_instr("CONSTINT");
+	print_int(*pc);
 	accu = Val_int(*pc);
 	pc++;
 	Next;
@@ -1110,7 +1121,6 @@ value coq_interprete
 	/* returns the sum plus one with a carry */
 	uint32_t s;
 	s = (uint32_t)accu + (uint32_t)*sp++ + 1;
-	value block;
         if( (uint32_t)s <= (uint32_t)accu ) {
           /* carry */
 	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
@@ -1183,8 +1193,8 @@ value coq_interprete
         print_instr("MULCINT31");
 	uint64_t p;
         /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */
-        p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1));
-	if ( I64_is_zero(p) ) {
+        p = UI64_of_value (accu) * UI64_of_uint32 ((*sp++)^1);
+	if (p == 0) {
 	  accu = (value)1;
 	}
 	else {
@@ -1193,8 +1203,8 @@ value coq_interprete
 	     of the non-constant constructor is then 1 */
 	  Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
 	  /*unsigned shift*/
-	  Field(accu, 0) = (value)(I64_lsr(p,31)|1) ;  /*higher part*/
-	  Field(accu, 1) = (value)(I64_to_int32(p)|1); /*lower part*/
+	  Field(accu, 0) = (value)((p >> 31)|1) ;  /*higher part*/
+	  Field(accu, 1) = (value)((int32_t)p|1); /*lower part*/
 	}
 	Next;
       }
@@ -1206,19 +1216,20 @@ value coq_interprete
                     int62 by the int31 */
         uint64_t bigint;
         bigint = UI64_of_value(accu);
-        bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++));
+        bigint = (bigint << 31) | UI64_of_value(*sp++);
         uint64_t divisor;
         divisor = UI64_of_value(*sp++);
         Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-        if (I64_is_zero (divisor)) {
+        if (divisor == 0) {
           Field(accu, 0) = 1; /* 2*0+1 */
           Field(accu, 1) = 1; /* 2*0+1 */
 	}
 	else {
 	  uint64_t 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));
+	  quo = bigint / divisor;
+	  mod = bigint % divisor;
+          Field(accu, 0) = value_of_uint32((uint32_t)(quo));
+	  Field(accu, 1) = value_of_uint32((uint32_t)(mod));
 	}
 	Next;
       }
@@ -1271,7 +1282,7 @@ value coq_interprete
 
       Instruct (COMPAREINT31) {
 	/* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
-	/* assumes Inudctive _ : _ := Eq | Lt | Gt */
+	/* assumes Inductive _ : _ := Eq | Lt | Gt */
 	print_instr("COMPAREINT31");
 	if ((uint32_t)accu == (uint32_t)*sp) {
 	  accu = 1;  /* 2*0+1 */
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 8d03829ab0..c9bcdc32ff 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -26,7 +26,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size;
 
 
 value coq_global_data;
-int coq_all_transp;
 value coq_atom_tbl;
 
 int drawinstr;
@@ -104,7 +103,6 @@ static int coq_vm_initialized = 0;
 
 value init_coq_vm(value unit) /* ML */
 {
-  int i;
   if (coq_vm_initialized == 1) {
     fprintf(stderr,"already open \n");fflush(stderr);}
   else {
@@ -117,7 +115,6 @@ value init_coq_vm(value unit) /* ML */
     init_coq_global_data(Coq_global_data_Size);
     init_coq_atom_tbl(40);
     /* Initialing the interpreter */
-    coq_all_transp = 0;
     init_coq_interpreter();
     
     /* Some predefined pointer code */
@@ -137,7 +134,6 @@ void realloc_coq_stack(asize_t required_space)
 {
   asize_t size;
   value * new_low, * new_high, * new_sp;
-  value * p;
   size = coq_stack_high - coq_stack_low;
   do {
     size *= 2;
@@ -207,18 +203,6 @@ value realloc_coq_atom_tbl(value size)            /* ML */
   return Val_unit;
 }
 
-
-value coq_set_transp_value(value transp)
-{
-  coq_all_transp = (transp == Val_true);
-  return Val_unit;
-}
-
-value get_coq_transp_value(value unit)
-{
-  return Val_bool(coq_all_transp);
-}
-
 value coq_set_drawinstr(value unit)
 {
   drawinstr = 1;
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 007f61b27c..528babebfc 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -21,7 +21,6 @@
 
 value coq_kind_of_closure(value v) {
   opcode_t * c;
-  int res;
   int is_app = 0;
   c = Code_val(v);
   if (Is_instruction(c, GRAB)) return Val_int(0);
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 1590a2141d..bb0f0eb5e4 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -17,23 +17,17 @@
 #define Default_tag 0
 #define Accu_tag 0
 
-
-
 #define ATOM_ID_TAG 0
-#define ATOM_IDDEF_TAG 1
-#define ATOM_INDUCTIVE_TAG 2
+#define ATOM_INDUCTIVE_TAG 1
+#define ATOM_TYPE_TAG 2
 #define ATOM_PROJ_TAG 3
 #define ATOM_FIX_TAG 4
 #define ATOM_SWITCH_TAG 5
 #define ATOM_COFIX_TAG 6
 #define ATOM_COFIXEVALUATED_TAG 7
 
-
-
 /* 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))
 #endif /* _COQ_VALUES_ */
-
-
diff --git a/kernel/byterun/int64_emul.h b/kernel/byterun/int64_emul.h
deleted file mode 100644
index 86bee72edb..0000000000
--- a/kernel/byterun/int64_emul.h
+++ /dev/null
@@ -1,270 +0,0 @@
-/***********************************************************************/
-/*                                                                     */
-/*                           Objective Caml                            */
-/*                                                                     */
-/*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         */
-/*                                                                     */
-/*  Copyright 2002 Institut National de Recherche en Informatique et   */
-/*  en Automatique.  All rights reserved.  This file is distributed    */
-/*  under the terms of the GNU Library General Public License, with    */
-/*  the special exception on linking described in file ../LICENSE.     */
-/*                                                                     */
-/***********************************************************************/
-
-/* Software emulation of 64-bit integer arithmetic, for C compilers
-   that do not support it.  */
-
-#ifndef CAML_INT64_EMUL_H
-#define CAML_INT64_EMUL_H
-
-#include <math.h>
-
-#ifdef ARCH_BIG_ENDIAN
-#define I64_literal(hi,lo) { hi, lo }
-#else
-#define I64_literal(hi,lo) { lo, hi }
-#endif
-
-/* Unsigned comparison */
-static int I64_ucompare(uint64 x, uint64 y)
-{
-  if (x.h > y.h) return 1;
-  if (x.h < y.h) return -1;
-  if (x.l > y.l) return 1;
-  if (x.l < y.l) return -1;
-  return 0;
-}
-
-#define I64_ult(x, y) (I64_ucompare(x, y) < 0)
-
-/* Signed comparison */
-static int I64_compare(int64 x, int64 y)
-{
-  if ((int32)x.h > (int32)y.h) return 1;
-  if ((int32)x.h < (int32)y.h) return -1;
-  if (x.l > y.l) return 1;
-  if (x.l < y.l) return -1;
-  return 0;
-}
-
-/* Negation */
-static int64 I64_neg(int64 x)
-{
-  int64 res;
-  res.l = -x.l;
-  res.h = ~x.h;
-  if (res.l == 0) res.h++;
-  return res;
-}
-
-/* Addition */
-static int64 I64_add(int64 x, int64 y)
-{
-  int64 res;
-  res.l = x.l + y.l;
-  res.h = x.h + y.h;
-  if (res.l < x.l) res.h++;
-  return res;
-}
-
-/* Subtraction */
-static int64 I64_sub(int64 x, int64 y)
-{
-  int64 res;
-  res.l = x.l - y.l;
-  res.h = x.h - y.h;
-  if (x.l < y.l) res.h--;
-  return res;
-}
-
-/* Multiplication */
-static int64 I64_mul(int64 x, int64 y)
-{
-  int64 res;
-  uint32 prod00 = (x.l & 0xFFFF) * (y.l & 0xFFFF);
-  uint32 prod10 = (x.l >> 16) * (y.l & 0xFFFF);
-  uint32 prod01 = (x.l & 0xFFFF) * (y.l >> 16);
-  uint32 prod11 = (x.l >> 16) * (y.l >> 16);
-  res.l = prod00;
-  res.h = prod11 + (prod01 >> 16) + (prod10 >> 16);
-  prod01 = prod01 << 16; res.l += prod01; if (res.l < prod01) res.h++;
-  prod10 = prod10 << 16; res.l += prod10; if (res.l < prod10) res.h++;
-  res.h += x.l * y.h + x.h * y.l;
-  return res;
-}
-
-#define I64_is_zero(x) (((x).l | (x).h) == 0)
-
-#define I64_is_negative(x) ((int32) (x).h < 0)
-
-/* Bitwise operations */
-static int64 I64_and(int64 x, int64 y)
-{
-  int64 res;
-  res.l = x.l & y.l;
-  res.h = x.h & y.h;
-  return res;
-}
-
-static int64 I64_or(int64 x, int64 y)
-{
-  int64 res;
-  res.l = x.l | y.l;
-  res.h = x.h | y.h;
-  return res;
-}
-
-static int64 I64_xor(int64 x, int64 y)
-{
-  int64 res;
-  res.l = x.l ^ y.l;
-  res.h = x.h ^ y.h;
-  return res;
-}
-
-/* Shifts */
-static int64 I64_lsl(int64 x, int s)
-{
-  int64 res;
-  s = s & 63;
-  if (s == 0) return x;
-  if (s < 32) {
-    res.l = x.l << s;
-    res.h = (x.h << s) | (x.l >> (32 - s));
-  } else {
-    res.l = 0;
-    res.h = x.l << (s - 32);
-  }
-  return res;
-}
-
-static int64 I64_lsr(int64 x, int s)
-{
-  int64 res;
-  s = s & 63;
-  if (s == 0) return x;
-  if (s < 32) {
-    res.l = (x.l >> s) | (x.h << (32 - s));
-    res.h = x.h >> s;
-  } else {
-    res.l = x.h >> (s - 32);
-    res.h = 0;
-  }
-  return res;
-}
-
-static int64 I64_asr(int64 x, int s)
-{
-  int64 res;
-  s = s & 63;
-  if (s == 0) return x;
-  if (s < 32) {
-    res.l = (x.l >> s) | (x.h << (32 - s));
-    res.h = (int32) x.h >> s;
-  } else {
-    res.l = (int32) x.h >> (s - 32);
-    res.h = (int32) x.h >> 31;
-  }
-  return res;
-}
-
-/* Division and modulus */
-
-#define I64_SHL1(x) x.h = (x.h << 1) | (x.l >> 31); x.l <<= 1
-#define I64_SHR1(x) x.l = (x.l >> 1) | (x.h << 31); x.h >>= 1
-
-static void I64_udivmod(uint64 modulus, uint64 divisor,
-                        uint64 * quo, uint64 * mod)
-{
-  int64 quotient, mask;
-  int cmp;
-
-  quotient.h = 0; quotient.l = 0;
-  mask.h = 0; mask.l = 1;
-  while ((int32) divisor.h >= 0) {
-    cmp = I64_ucompare(divisor, modulus);
-    I64_SHL1(divisor);
-    I64_SHL1(mask);
-    if (cmp >= 0) break;
-  }
-  while (mask.l | mask.h) {
-    if (I64_ucompare(modulus, divisor) >= 0) {
-      quotient.h |= mask.h; quotient.l |= mask.l;
-      modulus = I64_sub(modulus, divisor);
-    }
-    I64_SHR1(mask);
-    I64_SHR1(divisor);
-  }
-  *quo = quotient;
-  *mod = modulus;
-}
-
-static int64 I64_div(int64 x, int64 y)
-{
-  int64 q, r;
-  int32 sign;
-
-  sign = x.h ^ y.h;
-  if ((int32) x.h < 0) x = I64_neg(x);
-  if ((int32) y.h < 0) y = I64_neg(y);
-  I64_udivmod(x, y, &q, &r);
-  if (sign < 0) q = I64_neg(q);
-  return q;
-}
-
-static int64 I64_mod(int64 x, int64 y)
-{
-  int64 q, r;
-  int32 sign;
-
-  sign = x.h;
-  if ((int32) x.h < 0) x = I64_neg(x);
-  if ((int32) y.h < 0) y = I64_neg(y);
-  I64_udivmod(x, y, &q, &r);
-  if (sign < 0) r = I64_neg(r);
-  return r;
-}
-
-/* Coercions */
-
-static int64 I64_of_int32(int32 x)
-{
-  int64 res;
-  res.l = x;
-  res.h = x >> 31;
-  return res;
-}
-
-#define I64_to_int32(x) ((int32) (x).l)
-
-/* Note: we assume sizeof(intnat) = 4 here, which is true otherwise
-   autoconfiguration would have selected native 64-bit integers */
-#define I64_of_intnat I64_of_int32
-#define I64_to_intnat I64_to_int32
-
-static double I64_to_double(int64 x)
-{
-  double res;
-  int32 sign = x.h;
-  if (sign < 0) x = I64_neg(x);
-  res = ldexp((double) x.h, 32) + x.l;
-  if (sign < 0) res = -res;
-  return res;
-}
-
-static int64 I64_of_double(double f)
-{
-  int64 res;
-  double frac, integ;
-  int neg;
-
-  neg = (f < 0);
-  f = fabs(f);
-  frac = modf(ldexp(f, -32), &integ);
-  res.h = (uint32) integ;
-  res.l = (uint32) ldexp(frac, 32);
-  if (neg) res = I64_neg(res);
-  return res;
-}
-
-#endif /* CAML_INT64_EMUL_H */
diff --git a/kernel/byterun/int64_native.h b/kernel/byterun/int64_native.h
deleted file mode 100644
index 657d0a07e0..0000000000
--- a/kernel/byterun/int64_native.h
+++ /dev/null
@@ -1,48 +0,0 @@
-/***********************************************************************/
-/*                                                                     */
-/*                           Objective Caml                            */
-/*                                                                     */
-/*            Xavier Leroy, projet Cristal, INRIA Rocquencourt         */
-/*                                                                     */
-/*  Copyright 2002 Institut National de Recherche en Informatique et   */
-/*  en Automatique.  All rights reserved.  This file is distributed    */
-/*  under the terms of the GNU Library General Public License, with    */
-/*  the special exception on linking described in file ../LICENSE.     */
-/*                                                                     */
-/***********************************************************************/
-
-/* Wrapper macros around native 64-bit integer arithmetic,
-   so that it has the same interface as the software emulation
-   provided in int64_emul.h */
-
-#ifndef CAML_INT64_NATIVE_H
-#define CAML_INT64_NATIVE_H
-
-#define I64_literal(hi,lo) ((int64_t)(hi) << 32 | (lo))
-#define I64_compare(x,y) (((x) > (y)) - ((x) < (y)))
-#define I64_ult(x,y) ((uint64_t)(x) < (uint64_t)(y))
-#define I64_neg(x) (-(x))
-#define I64_add(x,y) ((x) + (y))
-#define I64_sub(x,y) ((x) - (y))
-#define I64_mul(x,y) ((x) * (y))
-#define I64_is_zero(x) ((x) == 0)
-#define I64_is_negative(x) ((x) < 0)
-#define I64_div(x,y) ((x) / (y))
-#define I64_mod(x,y) ((x) % (y))
-#define I64_udivmod(x,y,quo,rem) \
-  (*(rem) = (uint64_t)(x) % (uint64_t)(y), \
-   *(quo) = (uint64_t)(x) / (uint64_t)(y))
-#define I64_and(x,y) ((x) & (y))
-#define I64_or(x,y) ((x) | (y))
-#define I64_xor(x,y) ((x) ^ (y))
-#define I64_lsl(x,y) ((x) << (y))
-#define I64_asr(x,y) ((x) >> (y))
-#define I64_lsr(x,y) ((uint64_t)(x) >> (y))
-#define I64_to_intnat(x) ((intnat) (x))
-#define I64_of_intnat(x) ((intnat) (x))
-#define I64_to_int32(x) ((int32_t) (x))
-#define I64_of_int32(x) ((int64_t) (x))
-#define I64_to_double(x) ((double)(x))
-#define I64_of_double(x) ((int64_t)(x))
-
-#endif /* CAML_INT64_NATIVE_H */