Imported Upstream version 8.5~beta3+dfsg

7 files changed, 83 insertions, 48 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 1be3e651..29e33d34 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -60,7 +60,7 @@ void init_arity () {
     arity[BRANCH]=arity[ISCONST]= 1;
   /* instruction with two operands */
   arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
-  arity[ARECONST]=2;
+  arity[ARECONST]=arity[PROJ]=2;
   /* instruction with four operands */ 
   arity[MAKESWITCHBLOCK]=4;
   /* instruction with arbitrary operands */
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index c7b18b90..f0627586 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -12,6 +12,7 @@
 #define _COQ_CAML_GC_
 #include <caml/mlvalues.h>
 #include <caml/alloc.h>
+#include <caml/memory.h>
 
 typedef void (*scanning_action) (value, value *);
 
@@ -24,12 +25,22 @@ CAMLextern void minor_collection (void);
 #define Caml_white (0 << 8)
 #define Caml_black (3 << 8)
 
+#ifdef HAS_OCP_MEMPROF
+
+/*  This code is necessary to make the OCamlPro memory profiling branch of
+    OCaml compile. */
+
+#define Make_header(wosize, tag, color)                                 \
+  caml_make_header(wosize, tag, color)
+
+#else
+
 #define Make_header(wosize, tag, color)                                 \
   (((header_t) (((header_t) (wosize) << 10)                             \
 		+ (color)                                               \
 		+ (tag_t) (tag)))   					\
    )
-
+#endif
 
 #define Alloc_small(result, wosize, tag) do{                            \
   young_ptr -= Bhsize_wosize (wosize);                                  \
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 9cbf4077..8c5ab0ec 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -36,6 +36,7 @@ enum instructions {
   SWITCH, PUSHFIELDS, 
   GETFIELD0, GETFIELD1, GETFIELD, 
   SETFIELD0, SETFIELD1, SETFIELD,
+  PROJ,
   CONST0, CONST1, CONST2, CONST3, CONSTINT,
   PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
   ACCUMULATE,
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0ab9f89f..dc571699 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -77,9 +77,11 @@ sp is a local copy of the global variable extern_sp. */
 #ifdef _COQ_DEBUG_ 
 #   define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s)
 #   define print_int(i)   /*if (drawinstr)*/ printf("%d\n",i)
+#   define print_lint(i)  /*if (drawinstr)*/ printf("%ld\n",i)
 # else 
 #   define print_instr(s) 
 #   define print_int(i) 
+#   define print_lint(i)
 #endif
 
 /* GC interface */
@@ -339,6 +341,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(ENVACC){
 	print_instr("ENVACC");
+	print_int(*pc);
 	accu = Field(coq_env, *pc++);
         Next;
       }
@@ -369,6 +372,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;
@@ -456,6 +463,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;
@@ -479,11 +487,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]);
@@ -583,7 +598,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;
       }
@@ -718,6 +736,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(GETGLOBAL){
 	print_instr("GETGLOBAL");
+	print_int(*pc);
 	accu = Field(coq_global_data, *pc);
         pc++;
         Next;
@@ -730,7 +749,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++;
@@ -741,7 +760,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;
@@ -751,7 +771,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];
@@ -762,7 +783,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];
@@ -774,7 +796,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];
@@ -795,12 +818,12 @@ value coq_interprete
 	if (Is_block(accu)) {
 	  long index = Tag_val(accu);
 	  print_instr("block");
-	  print_int(index);
+	  print_lint(index);
 	  pc += pc[(sizes & 0xFFFFFF) + index];
 	} else {
 	  long index = Long_val(accu);
 	  print_instr("constant");
-	  print_int(index);
+	  print_lint(index);
 	  pc += pc[index];
 	}
 	  Next;
@@ -842,7 +865,6 @@ value coq_interprete
       }
 	
       Instruct(SETFIELD1){
-        int i, j, size, size_aux;
 	print_instr("SETFIELD1");
 	caml_modify(&Field(accu, 1),*sp);
        	sp++;
@@ -876,8 +898,30 @@ value coq_interprete
 	caml_modify(&Field(accu, *pc),*sp);
 	sp++; pc++;
 	Next;
-      }	
-   
+      }
+
+
+      Instruct(PROJ){
+	print_instr("PROJ");
+	if (Is_accu (accu)) {
+          value block;
+	  /* Skip over the index of projected field */
+	  pc++;
+	  /* Create atom */
+	  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) = block;
+	} else {
+	    accu = Field(accu, *pc++);
+	}
+	pc++;
+	Next;
+      }
+
 /* Integer constants */
 
       Instruct(CONST0){
@@ -917,6 +961,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(CONSTINT) {
 	print_instr("CONSTINT");
+	print_int(*pc);
 	accu = Val_int(*pc);
 	pc++;
 	Next;
@@ -957,7 +1002,7 @@ value coq_interprete
 	    sp -= nargs;
 	    for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
 	    *--sp = accu;
-	    print_int(nargs);
+	    print_lint(nargs);
 	    coq_extra_args = nargs;
 	    pc = Code_val(coq_env);
 	    goto check_stacks;
@@ -1084,7 +1129,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 ) */
@@ -1226,16 +1270,17 @@ value coq_interprete
         shiftby = uint32_of_value(accu);
         if (shiftby > 31) {
           if (shiftby < 62) {
-            *sp++;
-	    accu = (value)((((*sp++)^1) << (shiftby - 31)) | 1);
+            sp++;
+	    accu = (value)(((((uint32_t)*sp++)^1) << (shiftby - 31)) | 1);
           }
           else {
+            sp+=2;
             accu = (value)(1);
           }
 	}
         else{
         /* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */
-        accu = (value)(((*sp++)^1) << shiftby);
+	  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);
 	}
@@ -1244,7 +1289,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 8d03829a..c9bcdc32 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 007f61b2..528babeb 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 1bf493e2..bb0f0eb5 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -17,22 +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_FIX_TAG 3
-#define ATOM_SWITCH_TAG 4
-#define ATOM_COFIX_TAG 5
-#define ATOM_COFIXEVALUATED_TAG 6
-
-
+#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_ */
-
-