aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_fix_code.c12
-rw-r--r--kernel/byterun/coq_interp.c245
-rw-r--r--kernel/byterun/coq_memory.c2
-rw-r--r--kernel/byterun/coq_values.c16
-rw-r--r--kernel/byterun/coq_values.h4
-rw-r--r--kernel/cClosure.mli2
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/declareops.ml2
-rw-r--r--kernel/dune2
-rw-r--r--kernel/environ.ml22
-rw-r--r--kernel/environ.mli7
-rw-r--r--kernel/genOpcodeFiles.ml16
-rw-r--r--kernel/indTyping.ml2
-rw-r--r--kernel/kernel.mllib12
-rw-r--r--kernel/mod_typing.ml4
-rw-r--r--kernel/modops.ml2
-rw-r--r--kernel/nativelambda.ml4
-rw-r--r--kernel/reduction.ml51
-rw-r--r--kernel/safe_typing.ml14
-rw-r--r--kernel/term_typing.ml8
-rw-r--r--kernel/uGraph.ml36
-rw-r--r--kernel/uGraph.mli12
-rw-r--r--kernel/univ.ml42
-rw-r--r--kernel/vconv.ml2
-rw-r--r--kernel/vm.ml4
-rw-r--r--kernel/vmbytecodes.ml (renamed from kernel/cbytecodes.ml)6
-rw-r--r--kernel/vmbytecodes.mli (renamed from kernel/cbytecodes.mli)0
-rw-r--r--kernel/vmbytegen.ml (renamed from kernel/cbytegen.ml)100
-rw-r--r--kernel/vmbytegen.mli (renamed from kernel/cbytegen.mli)4
-rw-r--r--kernel/vmemitcodes.ml (renamed from kernel/cemitcodes.ml)22
-rw-r--r--kernel/vmemitcodes.mli (renamed from kernel/cemitcodes.mli)2
-rw-r--r--kernel/vmlambda.ml (renamed from kernel/clambda.ml)6
-rw-r--r--kernel/vmlambda.mli (renamed from kernel/clambda.mli)0
-rw-r--r--kernel/vmsymtable.ml (renamed from kernel/csymtable.ml)22
-rw-r--r--kernel/vmsymtable.mli (renamed from kernel/csymtable.mli)0
-rw-r--r--kernel/vmvalues.ml118
-rw-r--r--kernel/vmvalues.mli3
37 files changed, 436 insertions, 372 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 814cdfe1d8..9118410549 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -33,12 +33,12 @@ void init_arity () {
arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]=
arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]=
arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]=
- 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[APPLY4]=arity[RESTART]=arity[OFFSETCLOSUREM2]=
- arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]=
- arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]=
+ arity[PUSHACC6]=arity[PUSHACC7]=
+ arity[ENVACC0]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]=
+ arity[PUSHENVACC0]=arity[PUSHENVACC1]=arity[PUSHENVACC2]=arity[PUSHENVACC3]=
+ arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[APPLY4]=arity[RESTART]=
+ arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE1]=
+ arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE1]=
arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]=
arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 15cc451ea8..1b6da7dd6f 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -193,6 +193,8 @@ if (sp - num_args < coq_stack_threshold) { \
#endif
#endif
+#define Is_accu(v) (Is_block(v) && Tag_val(v) == Closure_tag && Code_val(v) == accumulate)
+
#define CheckPrimArgs(cond, apply_lbl) do{ \
if (cond) pc++; \
else{ \
@@ -383,37 +385,49 @@ value coq_interprete
}
/* Access in heap-allocated environment */
+ Instruct(ENVACC0){
+ print_instr("ENVACC0");
+ accu = Field(coq_env, 2);
+ Next;
+ }
Instruct(ENVACC1){
print_instr("ENVACC1");
- accu = Field(coq_env, 1); Next;
+ accu = Field(coq_env, 3);
+ Next;
}
Instruct(ENVACC2){
print_instr("ENVACC2");
- accu = Field(coq_env, 2); Next;
+ accu = Field(coq_env, 4);
+ Next;
}
Instruct(ENVACC3){
print_instr("ENVACC3");
- accu = Field(coq_env, 3); Next;
+ accu = Field(coq_env, 5);
+ Next;
}
- Instruct(ENVACC4){
- print_instr("ENVACC4");
- accu = Field(coq_env, 4); Next;
+ Instruct(PUSHENVACC0){
+ print_instr("PUSHENVACC0");
+ *--sp = accu;
+ accu = Field(coq_env, 2);
+ Next;
}
Instruct(PUSHENVACC1){
print_instr("PUSHENVACC1");
- *--sp = accu; accu = Field(coq_env, 1); Next;
+ *--sp = accu;
+ accu = Field(coq_env, 3);
+ Next;
}
Instruct(PUSHENVACC2){
print_instr("PUSHENVACC2");
- *--sp = accu; accu = Field(coq_env, 2); Next;
+ *--sp = accu;
+ accu = Field(coq_env, 4);
+ Next;
}
Instruct(PUSHENVACC3){
print_instr("PUSHENVACC3");
- *--sp = accu; accu = Field(coq_env, 3); Next;
- }
- Instruct(PUSHENVACC4){
- print_instr("PUSHENVACC4");
- *--sp = accu; accu = Field(coq_env, 4); Next;
+ *--sp = accu;
+ accu = Field(coq_env, 5);
+ Next;
}
Instruct(PUSHENVACC){
print_instr("PUSHENVACC");
@@ -423,7 +437,7 @@ value coq_interprete
Instruct(ENVACC){
print_instr("ENVACC");
print_int(*pc);
- accu = Field(coq_env, *pc++);
+ accu = Field(coq_env, 2 + *pc++);
Next;
}
/* Function application */
@@ -598,7 +612,6 @@ 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_stack;
@@ -643,13 +656,13 @@ value coq_interprete
}
Instruct(RESTART) {
- int num_args = Wosize_val(coq_env) - 2;
+ int num_args = Wosize_val(coq_env) - 3;
int i;
print_instr("RESTART");
CHECK_STACK(num_args);
sp -= num_args;
- for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2);
- coq_env = Field(coq_env, 1);
+ for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 3);
+ coq_env = Field(coq_env, 2);
coq_extra_args += num_args;
Next;
}
@@ -663,9 +676,10 @@ value coq_interprete
} else {
mlsize_t num_args, i;
num_args = 1 + coq_extra_args; /* arg1 + extra args */
- Alloc_small(accu, num_args + 2, Closure_tag);
- Field(accu, 1) = coq_env;
- for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+ Alloc_small(accu, num_args + 3, Closure_tag);
+ Field(accu, 1) = Val_int(2);
+ Field(accu, 2) = coq_env;
+ for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i];
Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
sp += num_args;
pc = (code_t)(sp[0]);
@@ -680,16 +694,18 @@ value coq_interprete
int rec_pos = *pc++; /* commence a zero */
print_instr("GRABREC");
if (rec_pos <= coq_extra_args && !Is_accu(sp[rec_pos])) {
- pc++;/* On saute le Restart */
+ pc++; /* Skip the next RESTART, then point coq_env at the free variables. */
+ coq_env = coq_env + (Int_val(Field(coq_env, 1)) - 2) * sizeof(value);
} else {
if (coq_extra_args < rec_pos) {
/* Partial application */
mlsize_t num_args, i;
num_args = 1 + coq_extra_args; /* arg1 + extra args */
- Alloc_small(accu, num_args + 2, Closure_tag);
- Field(accu, 1) = coq_env;
- for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
- Code_val(accu) = pc - 3;
+ Alloc_small(accu, num_args + 3, Closure_tag);
+ Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
+ Field(accu, 1) = Val_int(2);
+ Field(accu, 2) = coq_env;
+ for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i];
sp += num_args;
pc = (code_t)(sp[0]);
coq_env = sp[1];
@@ -698,25 +714,26 @@ value coq_interprete
} else {
/* The recursif argument is an accumulator */
mlsize_t num_args, i;
+ value block;
/* Construction of fixpoint applied to its [rec_pos-1] first arguments */
- Alloc_small(accu, rec_pos + 2, Closure_tag);
- Field(accu, 1) = coq_env; // We store the fixpoint in the first field
- for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; // Storing args
- Code_val(accu) = pc;
- sp += rec_pos;
- *--sp = accu;
- /* Construction of the atom */
- Alloc_small(accu, 2, ATOM_FIX_TAG);
- Field(accu,1) = sp[0];
- Field(accu,0) = sp[1];
- sp++; sp[0] = accu;
- /* Construction of the accumulator */
+ Alloc_small(accu, rec_pos + 3, Closure_tag);
+ Code_val(accu) = pc; /* Point to the next RESTART instr. */
+ Field(accu, 1) = Val_int(2);
+ Field(accu, 2) = coq_env; // We store the fixpoint in the first field
+ for (i = 0; i < rec_pos; i++) Field(accu, i + 3) = *sp++; // Storing args
+ /* Construction of the atom */
+ Alloc_small(block, 2, ATOM_FIX_TAG);
+ Field(block, 0) = *sp++;
+ Field(block, 1) = accu;
+ accu = block;
+ /* Construction of the accumulator */
num_args = coq_extra_args - rec_pos;
- Alloc_small(accu, 2+num_args, Accu_tag);
- Code_val(accu) = accumulate;
- Field(accu,1) = sp[0]; sp++;
- for (i = 0; i < num_args;i++)Field(accu, i + 2) = sp[i];
- sp += num_args;
+ Alloc_small(block, 3 + num_args, Closure_tag);
+ Code_val(block) = accumulate;
+ Field(block, 1) = Val_int(2);
+ Field(block, 2) = accu;
+ for (i = 0; i < num_args; i++) Field(block, i + 3) = *sp++;
+ accu = block;
pc = (code_t)(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
@@ -732,12 +749,13 @@ value coq_interprete
print_instr("CLOSURE");
print_int(nvars);
if (nvars > 0) *--sp = accu;
- Alloc_small(accu, 1 + nvars, Closure_tag);
+ Alloc_small(accu, 2 + nvars, Closure_tag);
+ Field(accu, 1) = Val_int(2);
Code_val(accu) = pc + *pc;
pc++;
for (i = 0; i < nvars; i++) {
print_lint(sp[i]);
- Field(accu, i + 1) = sp[i];
+ Field(accu, i + 2) = sp[i];
}
sp += nvars;
Next;
@@ -758,24 +776,19 @@ value coq_interprete
}
pc += nfuncs;
*--sp=accu;
- Alloc_small(accu, nfuncs * 2 + nvars, Closure_tag);
- Field(accu, nfuncs * 2 + nvars - 1) = *sp++;
- /* On remplie la partie pour les variables libres */
- p = &Field(accu, nfuncs * 2 - 1);
- for (i = 0; i < nvars; i++) {
- *p++ = *sp++;
- }
+ Alloc_small(accu, nfuncs * 3 + nvars, Closure_tag);
+ Field(accu, nfuncs * 3 + nvars - 1) = *sp++;
p = &Field(accu, 0);
- *p = (value) (pc + pc[0]);
- p++;
+ *p++ = (value) (pc + pc[0]);
+ *p++ = Val_int(nfuncs * 3 - 1);
for (i = 1; i < nfuncs; i++) {
- *p = Make_header(i * 2, Infix_tag, Caml_white);
- p++; /* color irrelevant. */
- *p = (value) (pc + pc[i]);
- p++;
+ *p++ = Make_header(i * 3, Infix_tag, Caml_white); /* color irrelevant. */
+ *p++ = (value) (pc + pc[i]);
+ *p++ = Val_int((nfuncs - i) * 3 - 1);
}
+ for (i = 0; i < nvars; i++) *p++ = *sp++;
pc += nfuncs;
- accu = accu + 2 * start * sizeof(value);
+ accu = accu + start * 3 * sizeof(value);
Next;
}
@@ -797,31 +810,28 @@ value coq_interprete
/* Creation des blocks accumulate */
for(i=0; i < nfunc; i++) {
- Alloc_small(accu, 2, Accu_tag);
+ Alloc_small(accu, 3, Closure_tag);
Code_val(accu) = accumulate;
- Field(accu,1) = Val_int(1);
+ Field(accu, 1) = Val_int(2);
+ Field(accu, 2) = Val_int(1);
*--sp=accu;
}
/* creation des fonction cofix */
p = sp;
- size = nfunc + nvars + 2;
+ size = nfunc + nvars + 3;
for (i=0; i < nfunc; i++) {
-
+ value block;
Alloc_small(accu, size, Closure_tag);
Code_val(accu) = pc+pc[i];
- for (j = 0; j < nfunc; j++) Field(accu, j+1) = p[j];
+ Field(accu, 1) = Val_int(2);
+ for (j = 0; j < nfunc; ++j) Field(accu, j + 2) = p[j];
Field(accu, size - 1) = p[nfunc];
- for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = p[j];
- *--sp = accu;
- /* creation du block contenant le cofix */
-
- Alloc_small(accu,1, ATOM_COFIX_TAG);
- Field(accu, 0) = sp[0];
- *sp = accu;
- /* mise a jour du block accumulate */
- caml_modify(&Field(p[i], 1),*sp);
- sp++;
+ for (j = nfunc + 1; j <= nfunc + nvars; ++j) Field(accu, j + 1) = p[j];
+ Alloc_small(block, 1, ATOM_COFIX_TAG);
+ Field(block, 0) = accu;
+ /* update the accumulate block */
+ caml_modify(&Field(p[i], 2), block);
}
pc += nfunc;
accu = p[start];
@@ -837,15 +847,8 @@ value coq_interprete
} /* fallthrough */
Instruct(OFFSETCLOSURE) {
print_instr("OFFSETCLOSURE");
- accu = coq_env + *pc++ * sizeof(value); Next;
- }
- Instruct(PUSHOFFSETCLOSUREM2) {
- print_instr("PUSHOFFSETCLOSUREM2");
- *--sp = accu;
- } /* fallthrough */
- Instruct(OFFSETCLOSUREM2) {
- print_instr("OFFSETCLOSUREM2");
- accu = coq_env - 2 * sizeof(value); Next;
+ accu = coq_env - *pc++ * 3 * sizeof(value);
+ Next;
}
Instruct(PUSHOFFSETCLOSURE0) {
print_instr("PUSHOFFSETCLOSURE0");
@@ -853,15 +856,17 @@ value coq_interprete
}/* fallthrough */
Instruct(OFFSETCLOSURE0) {
print_instr("OFFSETCLOSURE0");
- accu = coq_env; Next;
+ accu = coq_env;
+ Next;
}
- Instruct(PUSHOFFSETCLOSURE2){
- print_instr("PUSHOFFSETCLOSURE2");
+ Instruct(PUSHOFFSETCLOSURE1){
+ print_instr("PUSHOFFSETCLOSURE1");
*--sp = accu; /* fallthrough */
}
- Instruct(OFFSETCLOSURE2) {
- print_instr("OFFSETCLOSURE2");
- accu = coq_env + 2 * sizeof(value); Next;
+ Instruct(OFFSETCLOSURE1) {
+ print_instr("OFFSETCLOSURE1");
+ accu = coq_env - 3 * sizeof(value);
+ Next;
}
/* Access to global variables */
@@ -954,6 +959,7 @@ value coq_interprete
print_int(sizes & 0xFFFFFF);
if (Is_block(accu)) {
long index = Tag_val(accu);
+ if (index == Closure_tag) index = 0;
print_instr("block");
print_lint(index);
pc += pc[(sizes & 0xFFFFFF) + index];
@@ -1021,7 +1027,7 @@ value coq_interprete
print_instr("PROJ");
if (Is_accu (accu)) {
*--sp = accu; // Save matched block on stack
- accu = Field(accu, 1); // Save atom to accu register
+ accu = Field(accu, 2); // Save atom to accu register
switch (Tag_val(accu)) {
case ATOM_COFIX_TAG: // We are forcing a cofix
{
@@ -1033,11 +1039,11 @@ value coq_interprete
coq_env = Field(accu, 0); // Pointer to suspension
accu = sp[2]; // Save accumulator to accu register
sp[2] = Val_long(coq_extra_args); // Push number of args for return
- nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom)
+ nargs = Wosize_val(accu) - 3; // Number of args = size of accumulator - 2 (accumulator closure) - 1 (atom)
// Push arguments to stack
CHECK_STACK(nargs + 1);
sp -= nargs;
- for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 2);
+ for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 3);
*--sp = accu; // Last argument is the pointer to the suspension
coq_extra_args = nargs;
pc = Code_val(coq_env); // Trigger evaluation
@@ -1059,9 +1065,10 @@ value coq_interprete
Field(accu, 0) = Field(coq_global_data, *pc++);
Field(accu, 1) = *sp++;
/* Create accumulator */
- Alloc_small(block, 2, Accu_tag);
+ Alloc_small(block, 3, Closure_tag);
Code_val(block) = accumulate;
- Field(block, 1) = accu;
+ Field(block, 1) = Val_int(2);
+ Field(block, 2) = accu;
accu = block;
}
}
@@ -1122,7 +1129,7 @@ value coq_interprete
mlsize_t i, size;
print_instr("ACCUMULATE");
size = Wosize_val(coq_env);
- Alloc_small(accu, size + coq_extra_args + 1, Accu_tag);
+ Alloc_small(accu, size + coq_extra_args + 1, Closure_tag);
for(i = 0; i < size; i++) Field(accu, i) = Field(coq_env, i);
for(i = size; i <= coq_extra_args + size; i++)
Field(accu, i) = *sp++;
@@ -1135,7 +1142,7 @@ value coq_interprete
Instruct(MAKESWITCHBLOCK) {
print_instr("MAKESWITCHBLOCK");
*--sp = accu; // Save matched block on stack
- accu = Field(accu,1); // Save atom to accu register
+ accu = Field(accu, 2); // Save atom to accu register
switch (Tag_val(accu)) {
case ATOM_COFIX_TAG: // We are forcing a cofix
{
@@ -1149,11 +1156,11 @@ value coq_interprete
coq_env = Field(accu,0); // Pointer to suspension
accu = sp[2]; // Save accumulator to accu register
sp[2] = Val_long(coq_extra_args); // Push number of args for return
- nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom)
+ nargs = Wosize_val(accu) - 3; // Number of args = size of accumulator - 2 (accumulator closure) - 1 (atom)
// Push arguments to stack
CHECK_STACK(nargs+1);
sp -= nargs;
- for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
+ for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 3);
*--sp = accu; // Leftmost argument is the pointer to the suspension
print_lint(nargs);
coq_extra_args = nargs;
@@ -1174,6 +1181,7 @@ value coq_interprete
mlsize_t sz;
int i, annot;
code_t typlbl,swlbl;
+ value block;
print_instr("MAKESWITCHBLOCK");
typlbl = (code_t)pc + *pc;
@@ -1200,24 +1208,26 @@ value coq_interprete
*--sp = accu;
Alloc_small(accu, 1, Abstract_tag);
Code_val(accu) = swlbl;
- *--sp = accu;
/* We create the switch zipper */
- Alloc_small(accu, 5, Default_tag);
- Field(accu, 0) = sp[1];
- Field(accu, 1) = sp[0];
- Field(accu, 2) = sp[3];
- Field(accu, 3) = sp[2];
- Field(accu, 4) = coq_env;
+ Alloc_small(block, 5, Default_tag);
+ Field(block, 0) = sp[0];
+ Field(block, 1) = accu;
+ Field(block, 2) = sp[2];
+ Field(block, 3) = sp[1];
+ Field(block, 4) = coq_env;
sp += 3;
- sp[0] = accu;
+ accu = block;
/* We create the atom */
- Alloc_small(accu, 2, ATOM_SWITCH_TAG);
- Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0];
- sp++;sp[0] = accu;
+ Alloc_small(block, 2, ATOM_SWITCH_TAG);
+ Field(block, 0) = *sp++;
+ Field(block, 1) = accu;
+ accu = block;
/* We create the accumulator */
- Alloc_small(accu, 2, Accu_tag);
- Code_val(accu) = accumulate;
- Field(accu,1) = *sp++;
+ Alloc_small(block, 3, Closure_tag);
+ Code_val(block) = accumulate;
+ Field(block, 1) = Val_int(2);
+ Field(block, 2) = accu;
+ accu = block;
}
}
Next;
@@ -1228,10 +1238,11 @@ value coq_interprete
Instruct(MAKEACCU) {
int i;
print_instr("MAKEACCU");
- Alloc_small(accu, coq_extra_args + 3, Accu_tag);
+ Alloc_small(accu, coq_extra_args + 4, Closure_tag);
Code_val(accu) = accumulate;
- Field(accu,1) = Field(coq_atom_tbl, *pc);
- for(i = 2; i < coq_extra_args + 3; i++) Field(accu, i) = *sp++;
+ Field(accu, 1) = Val_int(2);
+ Field(accu, 2) = Field(coq_atom_tbl, *pc);
+ for (i = 2; i < coq_extra_args + 3; i++) Field(accu, i + 1) = *sp++;
pc = (code_t)(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
@@ -1875,11 +1886,11 @@ value coq_push_val(value v) {
value coq_push_arguments(value args) {
int nargs,i;
value * sp = coq_sp;
- nargs = Wosize_val(args) - 2;
+ nargs = Wosize_val(args) - 3;
CHECK_STACK(nargs);
coq_sp -= nargs;
print_instr("push_args");print_int(nargs);
- for(i = 0; i < nargs; i++) coq_sp[i] = Field(args, i+2);
+ for (i = 0; i < nargs; i++) coq_sp[i] = Field(args, i + 3);
return Val_unit;
}
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 6233675c66..ae5251c252 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -108,7 +108,7 @@ value init_coq_vm(value unit) /* ML */
init_coq_interpreter();
/* Some predefined pointer code.
- * It is typically contained in accumulator blocks whose tag is 0 and thus
+ * It is typically contained in accumulator blocks and thus might be
* scanned by the GC, so make it look like an OCaml block. */
value accu_block = (value) coq_stat_alloc(2 * sizeof(value));
Hd_hp (accu_block) = Make_header (1, Abstract_tag, Caml_black); \
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index bbe91da628..adfd4e8954 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -38,9 +38,9 @@ value coq_closure_arity(value clos) {
opcode_t * c = Code_val(clos);
if (Is_instruction(c,RESTART)) {
c++;
- if (Is_instruction(c,GRAB)) return Val_int(3 + c[1] - Wosize_val(clos));
+ if (Is_instruction(c,GRAB)) return Val_int(4 + c[1] - Wosize_val(clos));
else {
- if (Wosize_val(clos) != 2) caml_failwith("Coq Values : coq_closure_arity");
+ if (Wosize_val(clos) != 3) caml_failwith("Coq Values : coq_closure_arity");
return Val_int(1);
}
}
@@ -50,13 +50,17 @@ value coq_closure_arity(value clos) {
/* Fonction sur les fix */
-value coq_offset(value v) {
+value coq_current_fix(value v) {
if (Tag_val(v) == Closure_tag) return Val_int(0);
- else return Val_long(-Wsize_bsize(Infix_offset_val(v)));
+ else return Val_long(Wsize_bsize(Infix_offset_val(v)) / 3);
}
-value coq_offset_closure(value v, value offset){
- return (value)&Field(v, Int_val(offset));
+value coq_shift_fix(value v, value offset) {
+ return v + Int_val(offset) * 3 * sizeof(value);
+}
+
+value coq_last_fix(value v) {
+ return v + (Int_val(Field(v, 1)) - 2) * sizeof(value);
}
value coq_set_bytecode_field(value v, value i, value code) {
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index a19f9b56c1..f07018711b 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -17,7 +17,6 @@
#include <float.h>
#define Default_tag 0
-#define Accu_tag 0
#define ATOM_ID_TAG 0
#define ATOM_INDUCTIVE_TAG 1
@@ -28,9 +27,6 @@
#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))
#define Is_double(v) (Tag_val(v) == Double_tag)
#define Is_tailrec_switch(v) (Field(v,1) == Val_true)
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index ada0fc9780..3e8916673d 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -159,7 +159,7 @@ val inject : constr -> fconstr
(** mk_atom: prevents a term from being evaluated *)
val mk_atom : constr -> fconstr
-(** mk_red: makes a reducible term (used in newring) *)
+(** mk_red: makes a reducible term (used in ring) *)
val mk_red : fterm -> fconstr
val fterm_of : fconstr -> fterm
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 7609c1a64d..9c32cd8e0e 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -107,7 +107,7 @@ type 'opaque constant_body = {
const_body : (Constr.t Mod_subst.substituted, 'opaque) constant_def;
const_type : types;
const_relevance : Sorts.relevance;
- const_body_code : Cemitcodes.to_patch_substituted option;
+ const_body_code : Vmemitcodes.to_patch_substituted option;
const_universes : universes;
const_inline_code : bool;
const_typing_flags : typing_flags; (** The typing options which
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 326bf0d6ad..b9f434f179 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -116,7 +116,7 @@ let subst_const_body sub cb =
const_body = body';
const_type = type';
const_body_code =
- Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
+ Option.map (Vmemitcodes.subst_to_patch_subst sub) cb.const_body_code;
const_universes = cb.const_universes;
const_relevance = cb.const_relevance;
const_inline_code = cb.const_inline_code;
diff --git a/kernel/dune b/kernel/dune
index 5f7502ef6b..ce6fdc03df 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -11,7 +11,7 @@
(modules genOpcodeFiles))
(rule
- (targets copcodes.ml)
+ (targets vmopcodes.ml)
(action (with-stdout-to %{targets} (run ./genOpcodeFiles.exe copml))))
(rule
diff --git a/kernel/environ.ml b/kernel/environ.ml
index e75ccbb252..dec9e1deb8 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -87,6 +87,7 @@ let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key)
type named_context_val = {
env_named_ctx : Constr.named_context;
env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t;
+ env_named_var : Constr.t list;
}
type rel_context_val = {
@@ -109,6 +110,7 @@ type env = {
let empty_named_context_val = {
env_named_ctx = [];
env_named_map = Id.Map.empty;
+ env_named_var = [];
}
let empty_rel_context_val = {
@@ -183,6 +185,7 @@ let push_named_context_val_val d rval ctxt =
{
env_named_ctx = Context.Named.add d ctxt.env_named_ctx;
env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map;
+ env_named_var = mkVar (NamedDecl.get_id d) :: ctxt.env_named_var;
}
let push_named_context_val d ctxt =
@@ -193,7 +196,7 @@ let match_named_context_val c = match c.env_named_ctx with
| decl :: ctx ->
let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in
let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in
- let cval = { env_named_ctx = ctx; env_named_map = map } in
+ let cval = { env_named_ctx = ctx; env_named_map = map; env_named_var = List.tl c.env_named_var } in
Some (decl, v, cval)
let map_named_val f ctxt =
@@ -208,7 +211,7 @@ let map_named_val f ctxt =
in
let map, ctx = List.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in
if map == ctxt.env_named_map then ctxt
- else { env_named_ctx = ctx; env_named_map = map }
+ else { env_named_ctx = ctx; env_named_map = map; env_named_var = ctxt.env_named_var }
let push_named d env =
{env with env_named_context = push_named_context_val d env.env_named_context}
@@ -271,6 +274,11 @@ let is_impredicative_sort env = function
let is_impredicative_univ env u = is_impredicative_sort env (Sorts.sort_of_univ u)
+let is_impredicative_family env = function
+ | Sorts.InSProp | Sorts.InProp -> true
+ | Sorts.InSet -> is_impredicative_set env
+ | Sorts.InType -> false
+
let type_in_type env = not (typing_flags env).check_universes
let deactivated_guard env = not (typing_flags env).check_guarded
@@ -464,14 +472,22 @@ let same_flags {
[@warning "+9"]
let set_cumulative_sprop b = map_universes (UGraph.set_cumulative_sprop b)
+let set_type_in_type b = map_universes (UGraph.set_type_in_type b)
let set_typing_flags c env =
if same_flags env.env_typing_flags c then env
- else set_cumulative_sprop c.cumulative_sprop { env with env_typing_flags = c }
+ else
+ let env = { env with env_typing_flags = c } in
+ let env = set_cumulative_sprop c.cumulative_sprop env in
+ let env = set_type_in_type (not c.check_universes) env in
+ env
let set_cumulative_sprop b env =
set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env
+let set_type_in_type b env =
+ set_typing_flags {env.env_typing_flags with check_universes=not b} env
+
let set_allow_sprop b env =
{ env with env_stratification =
{ env.env_stratification with env_sprop_allowed = b } }
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 5cb56a2a29..f443ba38e1 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -69,6 +69,11 @@ type stratification = {
type named_context_val = private {
env_named_ctx : Constr.named_context;
env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t;
+ (** Identifier-indexed version of [env_named_ctx] *)
+ env_named_var : Constr.t list;
+ (** List of identifiers in [env_named_ctx], in the same order, including
+ let-ins. This is not used in the kernel, but is critical to preserve
+ sharing of evar instances in the proof engine. *)
}
type rel_context_val = private {
@@ -117,6 +122,7 @@ val indices_matter : env -> bool
val is_impredicative_sort : env -> Sorts.t -> bool
val is_impredicative_univ : env -> Univ.Universe.t -> bool
+val is_impredicative_family : env -> Sorts.family -> bool
(** is the local context empty *)
val empty_context : env -> bool
@@ -315,6 +321,7 @@ val push_subgraph : Univ.ContextSet.t -> env -> env
val set_engagement : engagement -> env -> env
val set_typing_flags : typing_flags -> env -> env
val set_cumulative_sprop : bool -> env -> env
+val set_type_in_type : bool -> env -> env
val set_allow_sprop : bool -> env -> env
val sprop_allowed : env -> bool
diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml
index 67a672c349..f052e03cde 100644
--- a/kernel/genOpcodeFiles.ml
+++ b/kernel/genOpcodeFiles.ml
@@ -11,7 +11,7 @@
(** List of opcodes.
It is used to generate the [coq_instruct.h], [coq_jumptbl.h] and
- [copcodes.ml] files.
+ [vmopcodes.ml] files.
If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c
with the arity of the instruction and maybe coq_tcode_of_code.
@@ -38,15 +38,15 @@ let opcodes =
"PUSHACC7";
"PUSHACC";
"POP";
+ "ENVACC0";
"ENVACC1";
"ENVACC2";
"ENVACC3";
- "ENVACC4";
"ENVACC";
+ "PUSHENVACC0";
"PUSHENVACC1";
"PUSHENVACC2";
"PUSHENVACC3";
- "PUSHENVACC4";
"PUSHENVACC";
"PUSH_RETADDR";
"APPLY";
@@ -65,13 +65,11 @@ let opcodes =
"CLOSURE";
"CLOSUREREC";
"CLOSURECOFIX";
- "OFFSETCLOSUREM2";
"OFFSETCLOSURE0";
- "OFFSETCLOSURE2";
+ "OFFSETCLOSURE1";
"OFFSETCLOSURE";
- "PUSHOFFSETCLOSUREM2";
"PUSHOFFSETCLOSURE0";
- "PUSHOFFSETCLOSURE2";
+ "PUSHOFFSETCLOSURE1";
"PUSHOFFSETCLOSURE";
"GETGLOBAL";
"PUSHGETGLOBAL";
@@ -196,7 +194,7 @@ let pp_coq_instruct_h fmt =
let pp_coq_jumptbl_h fmt =
pp_with_commas fmt (fun fmt -> Format.fprintf fmt "&&coq_lbl_%s")
-let pp_copcodes_ml fmt =
+let pp_vmopcodes_ml fmt =
pp_header true fmt;
Array.iteri (fun n s ->
Format.fprintf fmt "let op%s = %d@.@." s n
@@ -210,7 +208,7 @@ let main () =
match Sys.argv.(1) with
| "enum" -> pp_coq_instruct_h Format.std_formatter
| "jump" -> pp_coq_jumptbl_h Format.std_formatter
- | "copml" -> pp_copcodes_ml Format.std_formatter
+ | "copml" -> pp_vmopcodes_ml Format.std_formatter
| _ -> usage ()
| exception Invalid_argument _ -> usage ()
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 179353d3f0..b2520b780f 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -77,7 +77,7 @@ let check_univ_leq ?(is_real_arg=false) env u info =
else info
in
(* Inductive types provide explicit lifting from SProp to other universes, so allow SProp <= any. *)
- if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
+ if Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ }
else if is_impredicative_univ env ind_univ
&& Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 41388d9f17..d4d7150222 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -15,9 +15,9 @@ Term
CPrimitives
Mod_subst
Vmvalues
-Cbytecodes
-Copcodes
-Cemitcodes
+Vmbytecodes
+Vmopcodes
+Vmemitcodes
Opaqueproof
Declarations
Entries
@@ -30,12 +30,12 @@ Primred
CClosure
Relevanceops
Reduction
-Clambda
+Vmlambda
Nativelambda
-Cbytegen
+Vmbytegen
Nativecode
Nativelib
-Csymtable
+Vmsymtable
Vm
Vconv
Nativeconv
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 44b010204b..5873d1f502 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -124,8 +124,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
{ cb with
const_body = def;
const_universes = univs ;
- const_body_code = Option.map Cemitcodes.from_val
- (Cbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) }
+ const_body_code = Option.map Vmemitcodes.from_val
+ (Vmbytegen.compile_constant_body ~fail_on_error:false env' cb.const_universes def) }
in
before@(lab,SFBconst(cb'))::after, c', ctx'
else
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 77ef38dfd5..883ad79be5 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -328,7 +328,7 @@ let strengthen_const mp_from l cb resolver =
let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in
{ cb with
const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
- const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
+ const_body_code = Some (Vmemitcodes.from_val (Vmbytegen.compile_alias con)) }
let rec strengthen_mod mp_from mp_to mb =
if mp_in_delta mb.mod_mp mb.mod_delta then mb
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index b00b96018f..99090f0147 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -395,8 +395,8 @@ let rec get_alias env (kn, u as p) =
match tps with
| None -> p
| Some tps ->
- match Cemitcodes.force tps with
- | Cemitcodes.BCalias kn' -> get_alias env (kn', u)
+ match Vmemitcodes.force tps with
+ | Vmemitcodes.BCalias kn' -> get_alias env (kn', u)
| _ -> p
let prim env kn p args =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 0754e9d4cc..7c6b869b4a 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -234,6 +234,8 @@ let sort_cmp_universes env pb s0 s1 (u, check) =
let convert_instances ~flex u u' (s, check) =
(check.compare_instances ~flex u u' s, check)
+exception MustExpand
+
let get_cumulativity_constraints cv_pb variance u u' =
match cv_pb with
| CONV ->
@@ -251,7 +253,8 @@ let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2
| Some variances ->
let num_param_arity = inductive_cumulativity_arguments (mind,ind) in
if not (Int.equal num_param_arity nargs) then
- cmp_instances u1 u2 s
+ (* shortcut, not sure if worth doing, could use perf data *)
+ if Univ.Instance.equal u1 u2 then s else raise MustExpand
else
cmp_cumul cv_pb variances u1 u2 s
@@ -269,7 +272,7 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u
| Some _ ->
let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in
if not (Int.equal num_cnstr_args nargs) then
- cmp_instances u1 u2 s
+ if Univ.Instance.equal u1 u2 then s else raise MustExpand
else
(** By invariant, both constructors have a common supertype,
so they are convertible _at that type_. *)
@@ -336,6 +339,28 @@ let is_irrelevant infos lft c =
let env = info_env infos.cnv_inf in
try Relevanceops.relevance_of_fterm env (info_relevances infos.cnv_inf) lft c == Sorts.Irrelevant with _ -> false
+let identity_of_ctx (ctx:Constr.rel_context) =
+ Context.Rel.to_extended_vect mkRel 0 ctx
+
+(* ind -> fun args => ind args *)
+let eta_expand_ind env (ind,u as pind) =
+ let mib = Environ.lookup_mind (fst ind) env in
+ let mip = mib.mind_packets.(snd ind) in
+ let ctx = Vars.subst_instance_context u mip.mind_arity_ctxt in
+ let args = identity_of_ctx ctx in
+ let c = mkApp (mkIndU pind, args) in
+ let c = Term.it_mkLambda_or_LetIn c ctx in
+ inject c
+
+let eta_expand_constructor env ((ind,ctor),u as pctor) =
+ let mib = Environ.lookup_mind (fst ind) env in
+ let mip = mib.mind_packets.(snd ind) in
+ let ctx = Vars.subst_instance_context u (fst mip.mind_nf_lc.(ctor-1)) in
+ let args = identity_of_ctx ctx in
+ let c = mkApp (mkConstructU pctor, args) in
+ let c = Term.it_mkLambda_or_LetIn c ctx in
+ inject c
+
(* Conversion between [lft1]term1 and [lft2]term2 *)
let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
try eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
@@ -545,7 +570,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
end
(* Inductive types: MutInd MutConstruct Fix Cofix *)
- | (FInd (ind1,u1), FInd (ind2,u2)) ->
+ | (FInd (ind1,u1 as pind1), FInd (ind2,u2 as pind2)) ->
if eq_ind ind1 ind2 then
if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
let cuniv = convert_instances ~flex:false u1 u2 cuniv in
@@ -556,11 +581,16 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
if not (Int.equal nargs (CClosure.stack_args_size v2))
then raise NotConvertible
else
- let cuniv = convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv in
- convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ match convert_inductives cv_pb (mind, snd ind1) nargs u1 u2 cuniv with
+ | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ | exception MustExpand ->
+ let env = info_env infos.cnv_inf in
+ let hd1 = eta_expand_ind env pind1 in
+ let hd2 = eta_expand_ind env pind2 in
+ eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
else raise NotConvertible
- | (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
+ | (FConstruct ((ind1,j1),u1 as pctor1), FConstruct ((ind2,j2),u2 as pctor2)) ->
if Int.equal j1 j2 && eq_ind ind1 ind2 then
if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
let cuniv = convert_instances ~flex:false u1 u2 cuniv in
@@ -571,8 +601,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
if not (Int.equal nargs (CClosure.stack_args_size v2))
then raise NotConvertible
else
- let cuniv = convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv in
- convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ match convert_constructors (mind, snd ind1, j1) nargs u1 u2 cuniv with
+ | cuniv -> convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ | exception MustExpand ->
+ let env = info_env infos.cnv_inf in
+ let hd1 = eta_expand_constructor env pctor1 in
+ let hd2 = eta_expand_constructor env pctor2 in
+ eqappr cv_pb l2r infos (lft1,(hd1,v1)) (lft2,(hd2,v2)) cuniv
else raise NotConvertible
(* Eta expansion of records *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8b85072d6d..da77a2882e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -936,12 +936,14 @@ let add_private_constant l decl senv : (Constant.t * private_constants) * safe_e
| DefinitionEff ce ->
Term_typing.translate_constant senv.env kn (Entries.DefinitionEntry ce)
in
- let senv, dcb = match cb.const_body with
- | Def _ as const_body -> senv, { cb with const_body }
- | OpaqueDef c ->
- let local = empty_private cb.const_universes in
- let senv, o = push_opaque_proof (Future.from_val (c, local)) senv in
- senv, { cb with const_body = OpaqueDef o }
+ let dcb = match cb.const_body with
+ | Def _ as const_body -> { cb with const_body }
+ | OpaqueDef _ ->
+ (* We drop the body, to save the definition of an opaque and thus its
+ hashconsing. It does not matter since this only happens inside a proof,
+ and depending of the opaque status of the latter, this proof term will be
+ either inlined or reexported. *)
+ { cb with const_body = Undef None }
| Undef _ | Primitive _ -> assert false
in
let senv = add_constant_aux senv (kn, dcb) in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 48567aa564..24aa4ed771 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -283,8 +283,8 @@ let build_constant_declaration env result =
let univs = result.cook_universes in
let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
let tps =
- let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs def in
- Option.map Cemitcodes.from_val res
+ let res = Vmbytegen.compile_constant_body ~fail_on_error:false env univs def in
+ Option.map Vmemitcodes.from_val res
in
{ const_hyps = hyps;
const_body = def;
@@ -343,8 +343,8 @@ let translate_recipe env _kn r =
let open Cooking in
let result = Cooking.cook_constant r in
let univs = result.cook_universes in
- let res = Cbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in
- let tps = Option.map Cemitcodes.from_val res in
+ let res = Vmbytegen.compile_constant_body ~fail_on_error:false env univs result.cook_body in
+ let tps = Option.map Vmemitcodes.from_val res in
let hyps = Option.get result.cook_context in
(* Trust the set of section hypotheses generated by Cooking *)
let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 927db9e9e6..096e458ec4 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -29,7 +29,12 @@ module G = AcyclicGraph.Make(struct
code (eg add_universe with a constraint vs G.add with no
constraint) *)
-type t = { graph: G.t; sprop_cumulative : bool }
+type t = {
+ graph: G.t;
+ sprop_cumulative : bool;
+ type_in_type : bool;
+}
+
type 'a check_function = t -> 'a -> 'a -> bool
let g_map f g =
@@ -39,6 +44,10 @@ let g_map f g =
let set_cumulative_sprop b g = {g with sprop_cumulative=b}
+let set_type_in_type b g = {g with type_in_type=b}
+
+let type_in_type g = g.type_in_type
+
let check_smaller_expr g (u,n) (v,m) =
let diff = n - m in
match diff with
@@ -55,28 +64,33 @@ let real_check_leq g u v =
Universe.for_all (fun ul -> exists_bigger g ul v) u
let check_leq g u v =
+ type_in_type g ||
Universe.equal u v || (g.sprop_cumulative && Universe.is_sprop u) ||
(not (Universe.is_sprop u) && not (Universe.is_sprop v) &&
(is_type0m_univ u ||
real_check_leq g u v))
let check_eq g u v =
+ type_in_type g ||
Universe.equal u v ||
(not (Universe.is_sprop u || Universe.is_sprop v) &&
(real_check_leq g u v && real_check_leq g v u))
let check_eq_level g u v =
u == v ||
+ type_in_type g ||
(not (Level.is_sprop u || Level.is_sprop v) && G.check_eq g.graph u v)
-let empty_universes = {graph=G.empty; sprop_cumulative=false}
+let empty_universes = {graph=G.empty; sprop_cumulative=false; type_in_type=false}
let initial_universes =
let big_rank = 1000000 in
let g = G.empty in
let g = G.add ~rank:big_rank Level.prop g in
let g = G.add ~rank:big_rank Level.set g in
- {graph=G.enforce_lt Level.prop Level.set g; sprop_cumulative=false}
+ {empty_universes with graph=G.enforce_lt Level.prop Level.set g}
+
+let initial_universes_with g = {g with graph=initial_universes.graph}
let enforce_constraint (u,d,v) g =
match d with
@@ -91,6 +105,10 @@ let enforce_constraint (u,d,v as cst) g =
| true, Le, false when g.sprop_cumulative -> g
| _ -> raise (UniverseInconsistency (d,Universe.make u, Universe.make v, None))
+let enforce_constraint cst g =
+ if not (type_in_type g) then enforce_constraint cst g
+ else try enforce_constraint cst g with UniverseInconsistency _ -> g
+
let merge_constraints csts g = Constraint.fold enforce_constraint csts g
let check_constraint g (u,d,v) =
@@ -103,8 +121,8 @@ let check_constraint g (u,d,v as cst) =
match Level.is_sprop u, d, Level.is_sprop v with
| false, _, false -> check_constraint g.graph cst
| true, (Eq|Le), true -> true
- | true, Le, false -> g.sprop_cumulative
- | _ -> false
+ | true, Le, false -> g.sprop_cumulative || type_in_type g
+ | _ -> type_in_type g
let check_constraints csts g = Constraint.for_all (check_constraint g) csts
@@ -142,6 +160,14 @@ let enforce_leq_alg u v g =
| Inl x -> x
| Inr e -> raise e
+let enforce_leq_alg u v g =
+ match Universe.is_sprop u, Universe.is_sprop v with
+ | true, true -> Constraint.empty, g
+ | false, false -> enforce_leq_alg u v g
+ | left, _ ->
+ if left && g.sprop_cumulative then Constraint.empty, g
+ else raise (UniverseInconsistency (Le, u, v, None))
+
(* sanity check wrapper *)
let enforce_leq_alg u v g =
let _,g as cg = enforce_leq_alg u v g in
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index c9fbd7f694..87b3634e28 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -16,6 +16,15 @@ type t
val set_cumulative_sprop : bool -> t -> t
(** Makes the system incomplete. *)
+val set_type_in_type : bool -> t -> t
+
+(** When [type_in_type], functions adding constraints do not fail and
+ may instead ignore inconsistent constraints.
+
+ Checking functions such as [check_leq] always return [true].
+*)
+val type_in_type : t -> bool
+
type 'a check_function = t -> 'a -> 'a -> bool
val check_leq : Universe.t check_function
@@ -25,6 +34,9 @@ val check_eq_level : Level.t check_function
(** The initial graph of universes: Prop < Set *)
val initial_universes : t
+(** Initial universes, but keeping options such as type in type from the argument. *)
+val initial_universes_with : t -> t
+
(** Check equality of instances w.r.t. a universe graph *)
val check_eq_instances : Instance.t check_function
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 6d8aa02dff..a2fd14025e 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -205,12 +205,6 @@ module Level = struct
let pr u = str (to_string u)
- let apart u v =
- match data u, data v with
- | SProp, _ | _, SProp
- | Prop, Set | Set, Prop -> true
- | _ -> false
-
let vars = Array.init 20 (fun i -> make (Var i))
let var n =
@@ -250,7 +244,7 @@ module LMap = struct
ext empty
let pr f m =
- h 0 (prlist_with_sep fnl (fun (u, v) ->
+ h (prlist_with_sep fnl (fun (u, v) ->
Level.pr u ++ f v) (bindings m))
end
@@ -568,16 +562,6 @@ let constraint_type_ord c1 c2 = match c1, c2 with
| Eq, Eq -> 0
| Eq, _ -> 1
-(* Universe inconsistency: error raised when trying to enforce a relation
- that would create a cycle in the graph of universes. *)
-
-type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option
-
-exception UniverseInconsistency of univ_inconsistency
-
-let error_inconsistency o u v p =
- raise (UniverseInconsistency (o,Universe.make u,Universe.make v,p))
-
(* Constraints and sets of constraints. *)
type univ_constraint = Level.t * constraint_type * Level.t
@@ -660,8 +644,6 @@ type 'a constraint_function = 'a -> 'a -> constraints -> constraints
let enforce_eq_level u v c =
(* We discard trivial constraints like u=u *)
if Level.equal u v then c
- else if Level.apart u v then
- error_inconsistency Eq u v None
else Constraint.add (u,Eq,v) c
let enforce_eq u v c =
@@ -684,9 +666,9 @@ let constraint_add_leq v u c =
let j = m - n in
if j = -1 (* n = m+1, v+1 <= u <-> v < u *) then
Constraint.add (x,Lt,y) c
- else if j <= -1 (* n = m+k, v+k <= u <-> v+(k-1) < u *) then
- if Level.equal x y then (* u+(k+1) <= u *)
- raise (UniverseInconsistency (Le, Universe.tip v, Universe.tip u, None))
+ else if j <= -1 (* n = m+k, v+k <= u and k>0 *) then
+ if Level.equal x y then (* u+k <= u with k>0 *)
+ Constraint.add (x,Lt,x) c
else anomaly (Pp.str"Unable to handle arbitrary u+k <= v constraints.")
else if j = 0 then
Constraint.add (x,Le,y) c
@@ -703,8 +685,8 @@ let check_univ_leq u v =
let enforce_leq u v c =
match Universe.is_sprop u, Universe.is_sprop v with
| true, true -> c
- | true, false | false, true ->
- raise (UniverseInconsistency (Le, u, v, None))
+ | true, false -> Constraint.add (Level.sprop,Le,Level.prop) c
+ | false, true -> Constraint.add (Level.prop,Le,Level.sprop) c
| false, false ->
List.fold_left (fun c v -> (List.fold_left (fun c u -> constraint_add_leq u v c) c u)) c v
@@ -961,7 +943,7 @@ struct
let pr prl ?variance (univs, cst as ctx) =
if is_empty ctx then mt() else
- h 0 (Instance.pr prl ?variance univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
+ h (Instance.pr prl ?variance univs ++ str " |= ") ++ h (v 0 (Constraint.pr prl cst))
let hcons (univs, cst) =
(Instance.hcons univs, hcons_constraints cst)
@@ -1076,7 +1058,7 @@ struct
let pr prl (univs, cst as ctx) =
if is_empty ctx then mt() else
- h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
+ h (LSet.pr prl univs ++ str " |= ") ++ h (v 0 (Constraint.pr prl cst))
let constraints (_univs, cst) = cst
let levels (univs, _cst) = univs
@@ -1232,6 +1214,14 @@ let hcons_universe_context_set (v, c) =
let hcons_univ x = Universe.hcons x
+(* Universe inconsistency: error raised when trying to enforce a relation
+ that would create a cycle in the graph of universes. *)
+
+type univ_inconsistency = constraint_type * universe * universe * explanation Lazy.t option
+
+(* Do not use in this file as we may be type-in-type *)
+exception UniverseInconsistency of univ_inconsistency
+
let explain_universe_inconsistency prl (o,u,v,p : univ_inconsistency) =
let pr_uni = Universe.pr_with prl in
let pr_rel = function
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index f78f0d4d1e..cc2c2c0b4b 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -4,7 +4,7 @@ open Environ
open Reduction
open Vm
open Vmvalues
-open Csymtable
+open Vmsymtable
(* Test la structure des piles *)
diff --git a/kernel/vm.ml b/kernel/vm.ml
index d8c66bebd2..3adb2f2113 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -44,7 +44,7 @@ external coq_interprete : tcode -> values -> atom array -> vm_global -> vm_env -
"coq_interprete_byte" "coq_interprete_ml"
let interprete code v env k =
- coq_interprete code v (get_atom_rel ()) (Csymtable.get_global_data ()) env k
+ coq_interprete code v (get_atom_rel ()) (Vmsymtable.get_global_data ()) env k
(* Functions over arguments *)
@@ -95,7 +95,7 @@ let reduce_fix k vf =
(* computing types *)
let fc_typ = fix_types fb in
let ndef = Array.length fc_typ in
- let et = offset_closure_fix fb (2*(ndef - 1)) in
+ let et = fix_env fb in
let ftyp =
Array.map
(fun c -> interprete c crazy_val et 0) fc_typ in
diff --git a/kernel/cbytecodes.ml b/kernel/vmbytecodes.ml
index 74405a0105..c156a21c86 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/vmbytecodes.ml
@@ -106,14 +106,14 @@ let rec pp_instr i =
| Kclosure(lbl, n) ->
str "closure " ++ pp_lbl lbl ++ str ", " ++ int n
| Kclosurerec(fv,init,lblt,lblb) ->
- h 1 (str "closurerec " ++
+ hv 1 (str "closurerec " ++
int fv ++ str ", " ++ int init ++
str " types = " ++
prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
str " bodies = " ++
prlist_with_sep spc pp_lbl (Array.to_list lblb))
| Kclosurecofix (fv,init,lblt,lblb) ->
- h 1 (str "closurecofix " ++
+ hv 1 (str "closurecofix " ++
int fv ++ str ", " ++ int init ++
str " types = " ++
prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
@@ -129,7 +129,7 @@ let rec pp_instr i =
str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++
pp_lbl lbls ++ str ", " ++ int sz
| Kswitch(lblc,lblb) ->
- h 1 (str "switch " ++
+ hv 1 (str "switch " ++
prlist_with_sep spc pp_lbl (Array.to_list lblc) ++
str " | " ++
prlist_with_sep spc pp_lbl (Array.to_list lblb))
diff --git a/kernel/cbytecodes.mli b/kernel/vmbytecodes.mli
index b703058fb7..b703058fb7 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/vmbytecodes.mli
diff --git a/kernel/cbytegen.ml b/kernel/vmbytegen.ml
index bacc308e1f..375b1aface 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -15,9 +15,9 @@
open Util
open Names
open Vmvalues
-open Cbytecodes
-open Cemitcodes
-open Clambda
+open Vmbytecodes
+open Vmemitcodes
+open Vmlambda
open Constr
open Declarations
open Environ
@@ -28,10 +28,10 @@ open Environ
(* The virtual machine doesn't distinguish closures and their environment *)
(* Representation of function environments : *)
-(* [clos_t | code | fv1 | fv2 | ... | fvn ] *)
+(* [clos_t | code | envofs=2 | fv1 | fv2 | ... | fvn ] *)
(* ^ *)
-(* The offset for accessing free variables is 1 (we must skip the code *)
-(* pointer). *)
+(* The offset for accessing free variables is 2 (we must skip the code *)
+(* pointer and the environment offset). *)
(* While compiling, free variables are stored in [in_env] in order *)
(* opposite to machine representation, so we can add new free variables *)
(* easily (i.e. without changing the position of previous variables) *)
@@ -42,9 +42,9 @@ open Environ
(* In the function body [arg1] is represented by de Bruijn [n], and *)
(* [argn] by de Bruijn [1] *)
-(* Representation of environments of mutual fixpoints : *)
-(* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *)
-(* ^<----------offset---------> *)
+(* Representation of environments of mutual fixpoints : *)
+(* [clos_t|C1|envofs1| ... |infix_t|Ci|envofsi| ... |infix_t|Cnbr|envofsnbr=2| fv1 | fv2 | .... | fvn | type] *)
+(* ^ *)
(* type = [Ct1 | .... | Ctn] *)
(* Ci is the code pointer of the i-th body *)
(* At runtime, a fixpoint environment (which is the same as the fixpoint *)
@@ -52,45 +52,45 @@ open Environ
(* In each fixpoint body, de Bruijn [nbr] represents the first fixpoint *)
(* and de Bruijn [1] the last one. *)
(* Access to these variables is performed by the [Koffsetclosure n] *)
-(* instruction that shifts the environment pointer of [n] fields. *)
+(* instruction that shifts the environment pointer by [n] closuress. *)
(* This allows representing mutual fixpoints in just one block. *)
(* [Ct1 | ... | Ctn] is an array holding code pointers of the fixpoint *)
(* types. They are used in conversion tests (which requires that *)
(* fixpoint types must be convertible). Their environment is the one of *)
(* the last fixpoint : *)
-(* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *)
-(* ^ *)
+(* [clos_t|C1| ... |infix_t|Ci| ... |infix_t|Cnbr|envofsnbr=2| fv1 | fv2 | .... | fvn | type] *)
+(* ^ *)
(* Representation of mutual cofix : *)
(* a1 = [A_t | accumulate | [Cfx_t | fcofix1 ] ] *)
(* ... *)
(* anbr = [A_t | accumulate | [Cfx_t | fcofixnbr ] ] *)
(* *)
-(* fcofix1 = [clos_t | code1 | a1 |...| anbr | fv1 |...| fvn | type] *)
+(* fcofix1 = [clos_t | code1 | envofs=2 | a1 |...| anbr | fv1 |...| fvn | type] *)
(* ^ *)
(* ... *)
-(* fcofixnbr = [clos_t | codenbr | a1 |...| anbr | fv1 |...| fvn | type] *)
+(* fcofixnbr = [clos_t | codenbr | envofs=2 | a1 |...| anbr | fv1 |...| fvn | type] *)
(* ^ *)
(* The [ai] blocks are functions that accumulate their arguments: *)
(* ai arg1 argp ---> *)
-(* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *)
+(* ai' = [A_t | accumulate | envofs | [Cfx_t | fcofixi] | arg1 | ... | argp ] *)
(* If such a block is matched against, we have to force evaluation, *)
(* function [fcofixi] is then applied to [ai'] [arg1] ... [argp] *)
(* (note that [ai'] is a pointer to the closure, passed as argument) *)
(* Once evaluation is completed [ai'] is updated with the result: *)
(* ai' <-- *)
-(* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *)
+(* [A_t | accumulate | envofs | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *)
(* This representation is nice because the application of the cofix is *)
(* evaluated only once (it simulates a lazy evaluation) *)
(* Moreover, when cofix don't have arguments, it is possible to create *)
(* a cycle, e.g.: *)
(* cofix one := cons 1 one *)
-(* a1 = [A_t | accumulate | [Cfx_t|fcofix1] ] *)
-(* fcofix1 = [clos_t | code | a1] *)
+(* a1 = [A_t | accumulate | envofs | [Cfx_t|fcofix1] ] *)
+(* fcofix1 = [clos_t | code | envofs | a1] *)
(* The result of evaluating [a1] is [cons_t | 1 | a1]. *)
(* When [a1] is updated : *)
-(* a1 = [A_t | accumulate | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ] *)
+(* a1 = [A_t | accumulate | envofs | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ] *)
(* The cycle is created ... *)
(* *)
(* In Cfxe_t accumulators, we need to store [fcofixi] for testing *)
@@ -116,7 +116,7 @@ end
module FvMap = Map.Make(Fv_elem)
-(*spiwack: both type have been moved from Cbytegen because I needed then
+(*spiwack: both type have been moved from Vmbytegen because I needed then
for the retroknowledge *)
type vm_env = {
size : int; (* longueur de la liste [n] *)
@@ -131,9 +131,7 @@ type comp_env = {
(* universes are always at the bottom. *)
nb_stack : int; (* number of variables on the stack *)
in_stack : int Range.t; (* position in the stack *)
- nb_rec : int; (* number of mutually recursive functions *)
- pos_rec : instruction list; (* instruction d'acces pour les variables *)
- (* de point fix ou de cofix *)
+ pos_rec : instruction array; (* instruction to access mutually-defined functions *)
offset : int;
in_env : vm_env ref (* The free variables of the expression *)
}
@@ -159,8 +157,7 @@ let empty_comp_env ()=
nb_uni_stack = 0;
nb_stack = 0;
in_stack = Range.empty;
- nb_rec = 0;
- pos_rec = [];
+ pos_rec = [||];
offset = 0;
in_env = ref empty_fv
}
@@ -195,9 +192,8 @@ let comp_env_fun ?(univs=0) arity =
nb_uni_stack = univs ;
nb_stack = arity;
in_stack = add_param arity 0 Range.empty;
- nb_rec = 0;
- pos_rec = [];
- offset = 1;
+ pos_rec = [||];
+ offset = 0;
in_env = ref empty_fv
}
@@ -207,24 +203,18 @@ let comp_env_fix_type rfv =
nb_uni_stack = 0;
nb_stack = 0;
in_stack = Range.empty;
- nb_rec = 0;
- pos_rec = [];
- offset = 1;
+ pos_rec = [||];
+ offset = 0;
in_env = rfv
}
-let comp_env_fix ndef curr_pos arity rfv =
- let prec = ref [] in
- for i = ndef downto 1 do
- prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec
- done;
+let comp_env_fix ndef arity rfv =
{ arity;
nb_uni_stack = 0;
nb_stack = arity;
in_stack = add_param arity 0 Range.empty;
- nb_rec = ndef;
- pos_rec = !prec;
- offset = 2 * (ndef - curr_pos - 1)+1;
+ pos_rec = Array.init ndef (fun i -> Koffsetclosure i);
+ offset = 0;
in_env = rfv
}
@@ -233,24 +223,18 @@ let comp_env_cofix_type ndef rfv =
nb_uni_stack = 0;
nb_stack = 0;
in_stack = Range.empty;
- nb_rec = 0;
- pos_rec = [];
- offset = 1+ndef;
+ pos_rec = [||];
+ offset = ndef;
in_env = rfv
}
let comp_env_cofix ndef arity rfv =
- let prec = ref [] in
- for i = 1 to ndef do
- prec := Kenvacc i :: !prec
- done;
{ arity;
nb_uni_stack = 0;
nb_stack = arity;
in_stack = add_param arity 0 Range.empty;
- nb_rec = ndef;
- pos_rec = !prec;
- offset = ndef+1;
+ pos_rec = Array.init ndef (fun i -> Kenvacc (ndef - 1 - i));
+ offset = ndef;
in_env = rfv
}
@@ -283,11 +267,11 @@ let pos_rel i r sz =
Kacc(sz - (Range.get r.in_stack (i-1)))
else
let i = i - r.nb_stack in
- if i <= r.nb_rec then
- try List.nth r.pos_rec (i-1)
- with (Failure _|Invalid_argument _) -> assert false
+ let nb_rec = Array.length r.pos_rec in
+ if i <= nb_rec then
+ r.pos_rec.(i - 1)
else
- let i = i - r.nb_rec in
+ let i = i - nb_rec in
let db = FVrel(i) in
let env = !(r.in_env) in
try Kenvacc(r.offset + find_at db env)
@@ -410,16 +394,16 @@ let add_grabrec rec_arg arity lbl cont =
let cont_cofix arity =
(* accu = res *)
(* stk = ai::args::ra::... *)
- (* ai = [At|accumulate|[Cfx_t|fcofix]|args] *)
+ (* ai = [At|accumulate|envofs|[Cfx_t|fcofix]|args] *)
[ Kpush;
Kpush; (* stk = res::res::ai::args::ra::... *)
Kacc 2;
- Kfield 1;
+ Kfield 2;
Kfield 0;
Kmakeblock(2, cofix_evaluated_tag);
Kpush; (* stk = [Cfxe_t|fcofix|res]::res::ai::args::ra::...*)
Kacc 2;
- Ksetfield 1; (* ai = [At|accumulate|[Cfxe_t|fcofix|res]|args] *)
+ Ksetfield 2; (* ai = [At|accumulate|envofs|[Cfxe_t|fcofix|res]|args] *)
(* stk = res::ai::args::ra::... *)
Kacc 0; (* accu = res *)
Kreturn (arity+2) ]
@@ -512,7 +496,7 @@ let rec get_alias env kn =
match tps with
| None -> kn
| Some tps ->
- (match Cemitcodes.force tps with
+ (match Vmemitcodes.force tps with
| BCalias kn' -> get_alias env kn'
| _ -> kn)
@@ -627,7 +611,7 @@ let rec compile_lam env cenv lam sz cont =
for i = 0 to ndef - 1 do
let params,body = decompose_Llam bodies.(i) in
let arity = Array.length params in
- let env_body = comp_env_fix ndef i arity rfv in
+ let env_body = comp_env_fix ndef arity rfv in
let cont1 =
ensure_stack_capacity (compile_lam env env_body body arity) [Kreturn arity]
in
diff --git a/kernel/cbytegen.mli b/kernel/vmbytegen.mli
index d5ea2509ef..aef7ac3d6b 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/vmbytegen.mli
@@ -8,8 +8,8 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Cbytecodes
-open Cemitcodes
+open Vmbytecodes
+open Vmemitcodes
open Constr
open Declarations
open Environ
diff --git a/kernel/cemitcodes.ml b/kernel/vmemitcodes.ml
index ed475dca7e..f913cb906c 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -14,8 +14,8 @@
open Names
open Vmvalues
-open Cbytecodes
-open Copcodes
+open Vmbytecodes
+open Vmopcodes
open Mod_subst
open CPrimitives
@@ -270,12 +270,12 @@ let emit_instr env = function
| Kacc n ->
if n < 8 then out env(opACC0 + n) else (out env opACC; out_int env n)
| Kenvacc n ->
- if n >= 1 && n <= 4
- then out env(opENVACC1 + n - 1)
+ if n >= 0 && n <= 3
+ then out env(opENVACC0 + n)
else (out env opENVACC; out_int env n)
| Koffsetclosure ofs ->
- if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
- then out env (opOFFSETCLOSURE0 + ofs / 2)
+ if Int.equal ofs 0 || Int.equal ofs 1
+ then out env (opOFFSETCLOSURE0 + ofs)
else (out env opOFFSETCLOSURE; out_int env ofs)
| Kpush ->
out env opPUSH
@@ -350,7 +350,7 @@ let emit_instr env = function
| Ksetfield n ->
if n <= 1 then out env (opSETFIELD0+n)
else (out env opSETFIELD;out_int env n)
- | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
+ | Ksequence _ -> invalid_arg "Vmemitcodes.emit_instr"
| Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p
| Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
| Kbranch lbl -> out env opBRANCH; out_label env lbl
@@ -385,13 +385,13 @@ let rec emit env insns remaining = match insns with
if n < 8 then out env(opPUSHACC0 + n) else (out env opPUSHACC; out_int env n);
emit env c remaining
| Kpush :: Kenvacc n :: c ->
- if n >= 1 && n <= 4
- then out env(opPUSHENVACC1 + n - 1)
+ if n >= 0 && n <= 3
+ then out env(opPUSHENVACC0 + n)
else (out env opPUSHENVACC; out_int env n);
emit env c remaining
| Kpush :: Koffsetclosure ofs :: c ->
- if Int.equal ofs (-2) || Int.equal ofs 0 || Int.equal ofs 2
- then out env(opPUSHOFFSETCLOSURE0 + ofs / 2)
+ if Int.equal ofs 0 || Int.equal ofs 1
+ then out env(opPUSHOFFSETCLOSURE0 + ofs)
else (out env opPUSHOFFSETCLOSURE; out_int env ofs);
emit env c remaining
| Kpush :: Kgetglobal id :: c ->
diff --git a/kernel/cemitcodes.mli b/kernel/vmemitcodes.mli
index c4262f3380..5c0e103143 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/vmemitcodes.mli
@@ -9,7 +9,7 @@
(************************************************************************)
open Names
open Vmvalues
-open Cbytecodes
+open Vmbytecodes
type reloc_info =
| Reloc_annot of annot_switch
diff --git a/kernel/clambda.ml b/kernel/vmlambda.ml
index 6690a379ce..332a331a7a 100644
--- a/kernel/clambda.ml
+++ b/kernel/vmlambda.ml
@@ -559,8 +559,8 @@ let rec get_alias env kn =
match tps with
| None -> kn
| Some tps ->
- (match Cemitcodes.force tps with
- | Cemitcodes.BCalias kn' -> get_alias env kn'
+ (match Vmemitcodes.force tps with
+ | Vmemitcodes.BCalias kn' -> get_alias env kn'
| _ -> kn)
(* Compilation of primitive *)
@@ -681,7 +681,7 @@ open Renv
let rec lambda_of_constr env c =
match Constr.kind c with
- | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta")
+ | Meta _ -> raise (Invalid_argument "Vmbytegen.lambda_of_constr: Meta")
| Evar (evk, args) ->
let args = Array.map_of_list (fun c -> lambda_of_constr env c) args in
Levar (evk, args)
diff --git a/kernel/clambda.mli b/kernel/vmlambda.mli
index bd11c2667f..bd11c2667f 100644
--- a/kernel/clambda.mli
+++ b/kernel/vmlambda.mli
diff --git a/kernel/csymtable.ml b/kernel/vmsymtable.ml
index 185fb9f5a4..4ad830a298 100644
--- a/kernel/csymtable.ml
+++ b/kernel/vmsymtable.ml
@@ -17,11 +17,11 @@
open Util
open Names
open Vmvalues
-open Cemitcodes
-open Cbytecodes
+open Vmemitcodes
+open Vmbytecodes
open Declarations
open Environ
-open Cbytegen
+open Vmbytegen
module NamedDecl = Context.Named.Declaration
module RelDecl = Context.Rel.Declaration
@@ -155,7 +155,7 @@ let rec slot_for_getglobal env kn =
match cb.const_body_code with
| None -> set_global (val_of_constant kn)
| Some code ->
- match Cemitcodes.force code with
+ match Vmemitcodes.force code with
| BCdefined(code,pl,fv) ->
let v = eval_to_patch env (code,pl,fv) in
set_global v
@@ -206,15 +206,11 @@ and eval_to_patch env (buff,pl,fv) =
in
let tc = patch buff pl slots in
let vm_env =
- (* Beware, this may look like a call to [Array.map], but it's not.
- Calling [Array.map f] when the first argument returned by [f]
- is a float would lead to [vm_env] being an unboxed Double_array
- (Tag_val = Double_array_tag) whereas eval_tcode expects a
- regular array (Tag_val = 0).
- See test-suite/primitive/float/coq_env_double_array.v
- for an actual instance. *)
- let a = Array.make (Array.length fv) crazy_val in
- Array.iteri (fun i v -> a.(i) <- slot_for_fv env v) fv; a in
+ (* Environment should look like a closure, so free variables start at slot 2. *)
+ let a = Array.make (Array.length fv + 2) crazy_val in
+ a.(1) <- Obj.magic 2;
+ Array.iteri (fun i v -> a.(i + 2) <- slot_for_fv env v) fv;
+ a in
eval_tcode tc (get_atom_rel ()) (vm_global global_data.glob_val) vm_env
and val_of_constr env c =
diff --git a/kernel/csymtable.mli b/kernel/vmsymtable.mli
index e480bfcec1..e480bfcec1 100644
--- a/kernel/csymtable.mli
+++ b/kernel/vmsymtable.mli
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index de604176cb..0678f37a0b 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -34,8 +34,6 @@ let crazy_val = (val_of_obj (Obj.repr 0))
type tag = int
-let accu_tag = 0
-
let type_atom_tag = 2
let max_atom_tag = 2
let proj_tag = 3
@@ -166,7 +164,6 @@ let cofix_upd_val v = (Obj.magic v : values)
type vm_env
type vm_global
let fun_env v = (Obj.magic v : vm_env)
-let fix_env v = (Obj.magic v : vm_env)
let cofix_env v = (Obj.magic v : vm_env)
let cofix_upd_env v = (Obj.magic v : vm_env)
type vstack = values array
@@ -207,13 +204,13 @@ type vswitch = {
(* dom : values, codom : vfun *)
(* *)
(* + Functions have two representations : *)
-(* - unapplied fun : vf = Ct_[ C | fv1 | ... | fvn] *)
+(* - unapplied fun : vf = Ct_[ C | envofs=2 | fv1 | ... | fvn] *)
(* C:tcode, fvi : values *)
(* Remark : a function and its environment is the same value. *)
-(* - partially applied fun : Ct_[Restart:C| vf | arg1 | ... argn] *)
+(* - partially applied fun : Ct_[ Restart::C | envofs=2 | vf | arg1 | ... | argn] *)
(* *)
(* + Fixpoints : *)
-(* - Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn] *)
+(* - Ct_[C1|envofs1=3*n-1 | Infix_t|C2|envofs2 | ... | Infix_t|Cn|envofsn=2 | fv1|...|fvn] *)
(* One single block to represent all of the fixpoints, each fixpoint *)
(* is the pointer to the field holding the pointer to its code, and *)
(* the infix tag is used to know where the block starts. *)
@@ -226,13 +223,12 @@ type vswitch = {
(* + Cofixpoints : see cbytegen.ml *)
(* *)
(* + vblock's encode (non constant) constructors as in Ocaml, but *)
-(* starting from 0 up. tag 0 ( = accu_tag) is reserved for *)
-(* accumulators. *)
+(* starting from 0 up. *)
(* *)
(* + vm_env is the type of the machine environments (i.e. a function or *)
(* a fixpoint) *)
(* *)
-(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *)
+(* + Accumulators : At_[accumulate | envofs=2 | accu | arg1 | ... | argn ] *)
(* - representation of [accu] : tag_[....] *)
(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *)
(* -- 10_[accu|proj name] : a projection blocked by an accu *)
@@ -291,10 +287,10 @@ type whd =
| Vuniv_level of Univ.Level.t
(* Functions over arguments *)
-let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
+let nargs : arguments -> int = fun args -> Obj.size (Obj.repr args) - 3
let arg args i =
if 0 <= i && i < (nargs args) then
- val_of_obj (Obj.field (Obj.repr args) (i+2))
+ val_of_obj (Obj.field (Obj.repr args) (i + 3))
else invalid_arg
("Vm.arg size = "^(string_of_int (nargs args))^
" acces "^(string_of_int i))
@@ -329,9 +325,9 @@ let uni_lvl_val (v : values) : Univ.Level.t =
let rec whd_accu a stk =
let stk =
- if Int.equal (Obj.size a) 2 then stk
+ if Int.equal (Obj.size a) 3 then stk
else Zapp (Obj.obj a) :: stk in
- let at = Obj.field a 1 in
+ let at = Obj.field a 2 in
match Obj.tag at with
| i when Int.equal i type_atom_tag ->
begin match stk with
@@ -356,7 +352,7 @@ let rec whd_accu a stk =
| i when Int.equal i fix_app_tag ->
let fa = Obj.field at 1 in
let zfix =
- Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
+ Zfix (Obj.obj (Obj.field fa 2), Obj.obj fa) in
whd_accu (Obj.field at 0) (zfix :: stk)
| i when Int.equal i switch_tag ->
let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
@@ -392,29 +388,28 @@ external accumulate : unit -> tcode = "accumulate_code"
external set_bytecode_field : Obj.t -> int -> tcode -> unit = "coq_set_bytecode_field"
let accumulate = accumulate ()
-let whd_val : values -> whd =
- fun v ->
- let o = Obj.repr v in
- if Obj.is_int o then Vconstr_const (Obj.obj o)
+let whd_val (v: values) =
+ let o = Obj.repr v in
+ if Obj.is_int o then Vconstr_const (Obj.obj o)
+ else
+ let tag = Obj.tag o in
+ if Int.equal tag 0 then
+ if Int.equal (Obj.size o) 1 then
+ Varray (Obj.obj o)
+ else Vprod (Obj.obj o)
+ else if Int.equal tag Obj.closure_tag && is_accumulate (fun_code o) then
+ whd_accu o []
+ else if Int.equal tag Obj.closure_tag || Int.equal tag Obj.infix_tag then
+ (match kind_of_closure o with
+ | 0 -> Vfun(Obj.obj o)
+ | 1 -> Vfix(Obj.obj o, None)
+ | 2 -> Vfix(Obj.obj (Obj.field o 2), Some (Obj.obj o))
+ | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
+ | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work."))
+ else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v)
+ else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v)
else
- let tag = Obj.tag o in
- if tag = accu_tag then
- if Int.equal (Obj.size o) 1 then
- Varray(Obj.obj o)
- else if is_accumulate (fun_code o) then whd_accu o []
- else Vprod(Obj.obj o)
- else
- if tag = Obj.closure_tag || tag = Obj.infix_tag then
- (match kind_of_closure o with
- | 0 -> Vfun(Obj.obj o)
- | 1 -> Vfix(Obj.obj o, None)
- | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
- | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
- | _ -> CErrors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work."))
- else if Int.equal tag Obj.custom_tag then Vint64 (Obj.magic v)
- else if Int.equal tag Obj.double_tag then Vfloat64 (Obj.magic v)
- else
- Vconstr_block(Obj.obj o)
+ Vconstr_block (Obj.obj o)
(**********************************************)
(* Constructors *******************************)
@@ -422,9 +417,10 @@ let whd_val : values -> whd =
let obj_of_atom : atom -> Obj.t =
fun a ->
- let res = Obj.new_block accu_tag 2 in
+ let res = Obj.new_block Obj.closure_tag 3 in
set_bytecode_field res 0 accumulate;
- Obj.set_field res 1 (Obj.repr a);
+ Obj.set_field res 1 (Obj.repr 2);
+ Obj.set_field res 2 (Obj.repr a);
res
(* obj_of_str_const : structured_constant -> Obj.t *)
@@ -516,29 +512,23 @@ external closure_arity : vfun -> int = "coq_closure_arity"
(* Functions over fixpoint *)
-external offset : Obj.t -> int = "coq_offset"
-external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
-external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure"
+external current_fix : vfix -> int = "coq_current_fix"
+external shift_fix : vfix -> int -> vfix = "coq_shift_fix"
+external last_fix : vfix -> vfix = "coq_last_fix"
external tcode_array : tcode_array -> tcode array = "coq_tcode_array"
-let first o = (offset_closure o (offset o))
-let first_fix (v:vfix) = (Obj.magic (first (Obj.repr v)) : vfix)
+let first_fix o = shift_fix o (- current_fix o)
+let fix_env v = (Obj.magic (last_fix v) : vm_env)
let last o = (Obj.field o (Obj.size o - 1))
let fix_types (v:vfix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array)
let cofix_types (v:vcofix) = tcode_array (Obj.magic (last (Obj.repr v)) : tcode_array)
-let current_fix vf = - (offset (Obj.repr vf) / 2)
-
-let unsafe_fb_code fb i =
- let off = (2 * i) * (Sys.word_size / 8) in
- Obj.obj (Obj.add_offset (Obj.repr fb) (Int32.of_int off))
-
-let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1
+let unsafe_rec_arg fb i = int_tcode (Obj.magic (shift_fix fb i)) 1
let rec_args vf =
- let fb = first (Obj.repr vf) in
- let size = Obj.size (last fb) in
+ let fb = first_fix vf in
+ let size = Obj.size (last (Obj.repr fb)) in
Array.init size (unsafe_rec_arg fb)
exception FALSE
@@ -547,10 +537,10 @@ let check_fix f1 f2 =
let i1, i2 = current_fix f1, current_fix f2 in
(* Checking starting point *)
if i1 = i2 then
- let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in
- let n = Obj.size (last fb1) in
+ let fb1,fb2 = first_fix f1, first_fix f2 in
+ let n = Obj.size (last (Obj.repr fb1)) in
(* Checking number of definitions *)
- if n = Obj.size (last fb2) then
+ if n = Obj.size (last (Obj.repr fb2)) then
(* Checking recursive arguments *)
try
for i = 0 to n - 1 do
@@ -593,21 +583,23 @@ let relaccu_code i =
let mk_fix_body k ndef fb =
let e = Obj.dup (Obj.repr fb) in
+ let env = Obj.repr (fix_env (Obj.obj e)) in
for i = 0 to ndef - 1 do
- set_bytecode_field e (2 * i) (relaccu_code (k + i))
+ set_bytecode_field e (3 * i) (relaccu_code (k + i))
done;
let fix_body i =
- let c = offset_tcode (unsafe_fb_code fb i) 2 in
- let res = Obj.new_block Obj.closure_tag 2 in
+ let c = offset_tcode (Obj.magic (shift_fix fb i)) 2 in
+ let res = Obj.new_block Obj.closure_tag 3 in
set_bytecode_field res 0 c;
- Obj.set_field res 1 (offset_closure e (2*i));
+ Obj.set_field res 1 (Obj.repr 2);
+ Obj.set_field res 2 env;
((Obj.obj res) : vfun) in
Array.init ndef fix_body
(* Functions over vcofix *)
let get_fcofix vcf i =
- match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with
+ match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+2))) with
| Vcofix(vcfi, _, _) -> vcfi
| _ -> assert false
@@ -628,7 +620,7 @@ let check_cofix vcf1 vcf2 =
let mk_cofix_body apply_varray k ndef vcf =
let e = Obj.dup (Obj.repr vcf) in
for i = 0 to ndef - 1 do
- Obj.set_field e (i+1) (Obj.repr (val_of_rel (k+i)))
+ Obj.set_field e (i+2) (Obj.repr (val_of_rel (k+i)))
done;
let cofix_body i =
@@ -636,9 +628,7 @@ let mk_cofix_body apply_varray k ndef vcf =
let c = Obj.field (Obj.repr vcfi) 0 in
Obj.set_field e 0 c;
let atom = Obj.new_block cofix_tag 1 in
- let self = Obj.new_block accu_tag 2 in
- set_bytecode_field self 0 accumulate;
- Obj.set_field self 1 (Obj.repr atom);
+ let self = obj_of_atom (Obj.obj atom) in
apply_varray (Obj.obj e) [|Obj.obj self|] in
Array.init ndef cofix_body
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index f6efd49cfc..6632dc46b2 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -27,8 +27,6 @@ type to_update
type tag = int
-val accu_tag : tag
-
val type_atom_tag : tag
val max_atom_tag : tag
val proj_tag : tag
@@ -181,7 +179,6 @@ val rec_args : vfix -> int array
val first_fix : vfix -> vfix
val fix_types : vfix -> tcode array
val cofix_types : vcofix -> tcode array
-external offset_closure_fix : vfix -> int -> vm_env = "coq_offset_closure"
val mk_fix_body : int -> int -> vfix -> vfun array
(** CoFix *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 07:22:22 +0000