Adds support for the virtual machine to perform reduction of universe polymorphic definitions.

- This implementation passes universes in separate arguments and does not
  eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.

2 files changed, 34 insertions, 17 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0553a5ed7..dc571699e 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -341,6 +341,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(ENVACC){
 	print_instr("ENVACC");
+	print_int(*pc);
 	accu = Field(coq_env, *pc++);
         Next;
       }
@@ -371,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;
@@ -458,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;
@@ -481,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]);
@@ -585,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;
       }
@@ -720,6 +736,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(GETGLOBAL){
 	print_instr("GETGLOBAL");
+	print_int(*pc);
 	accu = Field(coq_global_data, *pc);
         pc++;
         Next;
@@ -732,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++;
@@ -743,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;
@@ -753,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];
@@ -764,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];
@@ -776,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];
@@ -940,6 +961,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(CONSTINT) {
 	print_instr("CONSTINT");
+	print_int(*pc);
 	accu = Val_int(*pc);
 	pc++;
 	Next;
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 80100da71..bb0f0eb5e 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_INDUCTIVE_TAG 1
-#define ATOM_PROJ_TAG 2
-#define ATOM_FIX_TAG 3
-#define ATOM_SWITCH_TAG 4
-#define ATOM_COFIX_TAG 5
-#define ATOM_COFIXEVALUATED_TAG 6
-
-
+#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_ */
-
-