aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_fix_code.c14
-rw-r--r--kernel/byterun/coq_gc.h6
-rw-r--r--kernel/byterun/coq_interp.c1342
-rw-r--r--kernel/byterun/coq_memory.c12
-rw-r--r--kernel/byterun/coq_memory.h4
-rw-r--r--kernel/byterun/coq_values.c4
-rw-r--r--kernel/byterun/dune6
-rw-r--r--kernel/cooking.ml10
-rw-r--r--kernel/entries.ml2
-rw-r--r--kernel/environ.mli6
-rw-r--r--kernel/indTyping.ml77
-rw-r--r--kernel/inferCumulativity.ml24
-rw-r--r--kernel/inferCumulativity.mli4
-rw-r--r--kernel/kernel.mllib2
-rw-r--r--kernel/safe_typing.ml67
-rw-r--r--kernel/safe_typing.mli4
-rw-r--r--kernel/section.ml183
-rw-r--r--kernel/section.mli11
-rw-r--r--kernel/uint63_31.ml43
19 files changed, 868 insertions, 953 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 931b509f48..306643f758 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -12,7 +12,7 @@
for fast computation of bounded (31bits) integers */
#include <stdio.h>
-#include <stdlib.h>
+#include <stdlib.h>
#include <stdint.h>
#include <caml/config.h>
#include <caml/misc.h>
@@ -42,7 +42,7 @@ void init_arity () {
arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]=
arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
- arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]=
+ arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]=
arity[ADDINT63]=arity[SUBINT63]=arity[LTINT63]=arity[LEINT63]=
arity[LTFLOAT]=arity[LEFLOAT]=
arity[ISINT]=arity[AREINT2]=0;
@@ -76,7 +76,7 @@ void init_arity () {
/* instruction with two operands */
arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
arity[PROJ]=2;
- /* instruction with four operands */
+ /* instruction with four operands */
arity[MAKESWITCHBLOCK]=4;
/* instruction with arbitrary operands */
arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0;
@@ -134,7 +134,7 @@ value coq_is_accumulate_code(value code){
#ifdef ARCH_BIG_ENDIAN
#define Reverse_32(dst,src) { \
- char * _p, * _q; \
+ char * _p, * _q; \
char _a, _b; \
_p = (char *) (src); \
_q = (char *) (dst); \
@@ -159,9 +159,9 @@ value coq_tcode_of_code (value code) {
q = coq_stat_alloc(len);
Code_val(res) = q;
len /= sizeof(opcode_t);
- for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) {
+ for (p = (code_t)code; p < (code_t)code + len; /*nothing*/) {
opcode_t instr;
- COPY32(&instr,p);
+ COPY32(&instr,p);
p++;
if (instr < 0 || instr > STOP){
instr = STOP;
@@ -183,7 +183,7 @@ value coq_tcode_of_code (value code) {
for(i=1; i<n; i++) { COPY32(q,p); p++; q++; };
} else {
uint32_t i, ar;
- ar = arity[instr];
+ ar = arity[instr];
for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
}
}
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index f06275862c..38eda4d11f 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -37,8 +37,8 @@ CAMLextern void minor_collection (void);
#define Make_header(wosize, tag, color) \
(((header_t) (((header_t) (wosize) << 10) \
- + (color) \
- + (tag_t) (tag))) \
+ + (color) \
+ + (tag_t) (tag))) \
)
#endif
@@ -53,7 +53,7 @@ CAMLextern void minor_collection (void);
} \
Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black); \
(result) = Val_hp (young_ptr); \
- }while(0)
+ }while(0)
#endif /*_COQ_CAML_GC_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index ca1308696c..606cce0127 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -17,12 +17,14 @@
#include <signal.h>
#include <stdint.h>
#include <caml/memory.h>
+#include <caml/signals.h>
+#include <caml/version.h>
#include <math.h>
#include "coq_gc.h"
#include "coq_instruct.h"
#include "coq_fix_code.h"
-#include "coq_memory.h"
-#include "coq_values.h"
+#include "coq_memory.h"
+#include "coq_values.h"
#include "coq_float64.h"
#ifdef ARCH_SIXTYFOUR
@@ -49,7 +51,7 @@ sp is a local copy of the global variable extern_sp. */
#ifdef THREADED_CODE
-# define Instruct(name) coq_lbl_##name:
+# define Instruct(name) coq_lbl_##name:
# if defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
# define coq_Jumptbl_base ((char *) &&coq_lbl_ACC0)
# else
@@ -59,22 +61,22 @@ sp is a local copy of the global variable extern_sp. */
# ifdef DEBUG
# define Next goto next_instr
# else
-# define Next goto *(void *)(coq_jumptbl_base + *pc++)
+# define Next goto *(void *)(coq_jumptbl_base + *pc++)
# endif
-#else
+#else
# define Instruct(name) case name:
# define Next break
-#endif
+#endif
/* #define _COQ_DEBUG_ */
-#ifdef _COQ_DEBUG_
+#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)
+# else
+# define print_instr(s)
+# define print_int(i)
# define print_lint(i)
#endif
@@ -95,7 +97,7 @@ if (sp - num_args < coq_stack_threshold) { \
Some compilers underestimate the use of the local variables representing
the abstract machine registers, and don't put them in hardware registers,
which slows down the interpreter considerably.
- For GCC, Xavier Leroy have hand-assigned hardware registers for
+ For GCC, Xavier Leroy have hand-assigned hardware registers for
several architectures.
*/
@@ -171,11 +173,11 @@ if (sp - num_args < coq_stack_threshold) { \
#define CheckPrimArgs(cond, apply_lbl) do{ \
if (cond) pc++; \
- else{ \
- *--sp=accu; \
- accu = Field(coq_global_data, *pc++); \
+ else{ \
+ *--sp=accu; \
+ accu = Field(coq_global_data, *pc++); \
goto apply_lbl; \
- } \
+ } \
}while(0)
#define CheckInt1() CheckPrimArgs(Is_uint63(accu), apply1)
@@ -203,11 +205,13 @@ if (sp - num_args < coq_stack_threshold) { \
*sp = swap_accu_sp_tmp__; \
}while(0)
+#if OCAML_VERSION < 41000
/* For signal handling, we hijack some code from the caml runtime */
-extern intnat caml_signals_are_pending;
-extern intnat caml_pending_signals[];
+extern intnat volatile caml_signals_are_pending;
+extern intnat volatile caml_pending_signals[];
extern void caml_process_pending_signals(void);
+#endif
/* The interpreter itself */
@@ -238,7 +242,7 @@ value coq_interprete
static void * coq_jumptable[] = {
# include "coq_jumptbl.h"
};
-#else
+#else
opcode_t curr_instr;
#endif
print_instr("Enter Interpreter");
@@ -269,193 +273,193 @@ value coq_interprete
switch(curr_instr) {
#endif
/* Basic stack operations */
-
+
Instruct(ACC0){
- print_instr("ACC0");
- accu = sp[0]; Next;
+ print_instr("ACC0");
+ accu = sp[0]; Next;
}
Instruct(ACC1){
- print_instr("ACC1");
- accu = sp[1]; Next;
+ print_instr("ACC1");
+ accu = sp[1]; Next;
}
Instruct(ACC2){
- print_instr("ACC2");
- accu = sp[2]; Next;
+ print_instr("ACC2");
+ accu = sp[2]; Next;
}
Instruct(ACC3){
- print_instr("ACC3");
- accu = sp[3]; Next;
+ print_instr("ACC3");
+ accu = sp[3]; Next;
}
Instruct(ACC4){
- print_instr("ACC4");
- accu = sp[4]; Next;
+ print_instr("ACC4");
+ accu = sp[4]; Next;
}
Instruct(ACC5){
- print_instr("ACC5");
- accu = sp[5]; Next;
+ print_instr("ACC5");
+ accu = sp[5]; Next;
}
Instruct(ACC6){
- print_instr("ACC6");
- accu = sp[6]; Next;
+ print_instr("ACC6");
+ accu = sp[6]; Next;
}
Instruct(ACC7){
- print_instr("ACC7");
+ print_instr("ACC7");
accu = sp[7]; Next;
- }
+ }
Instruct(PUSH){
- print_instr("PUSH");
- *--sp = accu; Next;
+ print_instr("PUSH");
+ *--sp = accu; Next;
}
Instruct(PUSHACC0) {
- print_instr("PUSHACC0");
+ print_instr("PUSHACC0");
*--sp = accu; Next;
}
Instruct(PUSHACC1){
- print_instr("PUSHACC1");
+ print_instr("PUSHACC1");
*--sp = accu; accu = sp[1]; Next;
}
Instruct(PUSHACC2){
- print_instr("PUSHACC2");
+ print_instr("PUSHACC2");
*--sp = accu; accu = sp[2]; Next;
}
Instruct(PUSHACC3){
- print_instr("PUSHACC3");
- *--sp = accu; accu = sp[3]; Next;
+ print_instr("PUSHACC3");
+ *--sp = accu; accu = sp[3]; Next;
}
Instruct(PUSHACC4){
- print_instr("PUSHACC4");
- *--sp = accu; accu = sp[4]; Next;
+ print_instr("PUSHACC4");
+ *--sp = accu; accu = sp[4]; Next;
}
Instruct(PUSHACC5){
- print_instr("PUSHACC5");
- *--sp = accu; accu = sp[5]; Next;
+ print_instr("PUSHACC5");
+ *--sp = accu; accu = sp[5]; Next;
}
Instruct(PUSHACC6){
- print_instr("PUSHACC5");
- *--sp = accu; accu = sp[6]; Next;
+ print_instr("PUSHACC5");
+ *--sp = accu; accu = sp[6]; Next;
}
Instruct(PUSHACC7){
- print_instr("PUSHACC7");
- *--sp = accu; accu = sp[7]; Next;
+ print_instr("PUSHACC7");
+ *--sp = accu; accu = sp[7]; Next;
}
Instruct(PUSHACC){
- print_instr("PUSHACC");
- *--sp = accu;
+ print_instr("PUSHACC");
+ *--sp = accu;
}
/* Fallthrough */
-
+
Instruct(ACC){
- print_instr("ACC");
- accu = sp[*pc++];
+ print_instr("ACC");
+ accu = sp[*pc++];
Next;
}
-
+
Instruct(POP){
- print_instr("POP");
- sp += *pc++;
- Next;
+ print_instr("POP");
+ sp += *pc++;
+ Next;
}
/* Access in heap-allocated environment */
-
+
Instruct(ENVACC1){
- print_instr("ENVACC1");
- accu = Field(coq_env, 1); Next;
+ print_instr("ENVACC1");
+ accu = Field(coq_env, 1); Next;
}
Instruct(ENVACC2){
- print_instr("ENVACC2");
- accu = Field(coq_env, 2); Next;
+ print_instr("ENVACC2");
+ accu = Field(coq_env, 2); Next;
}
Instruct(ENVACC3){
- print_instr("ENVACC3");
- accu = Field(coq_env, 3); Next;
+ print_instr("ENVACC3");
+ accu = Field(coq_env, 3); Next;
}
Instruct(ENVACC4){
- print_instr("ENVACC4");
- accu = Field(coq_env, 4); Next;
+ print_instr("ENVACC4");
+ accu = Field(coq_env, 4); Next;
}
Instruct(PUSHENVACC1){
- print_instr("PUSHENVACC1");
- *--sp = accu; accu = Field(coq_env, 1); Next;
+ print_instr("PUSHENVACC1");
+ *--sp = accu; accu = Field(coq_env, 1); Next;
}
Instruct(PUSHENVACC2){
- print_instr("PUSHENVACC2");
- *--sp = accu; accu = Field(coq_env, 2); Next;
+ print_instr("PUSHENVACC2");
+ *--sp = accu; accu = Field(coq_env, 2); Next;
}
Instruct(PUSHENVACC3){
- print_instr("PUSHENVACC3");
- *--sp = accu; accu = Field(coq_env, 3); Next;
+ print_instr("PUSHENVACC3");
+ *--sp = accu; accu = Field(coq_env, 3); Next;
}
Instruct(PUSHENVACC4){
- print_instr("PUSHENVACC4");
- *--sp = accu; accu = Field(coq_env, 4); Next;
+ print_instr("PUSHENVACC4");
+ *--sp = accu; accu = Field(coq_env, 4); Next;
}
Instruct(PUSHENVACC){
- print_instr("PUSHENVACC");
- *--sp = accu;
+ print_instr("PUSHENVACC");
+ *--sp = accu;
}
/* Fallthrough */
Instruct(ENVACC){
- print_instr("ENVACC");
- print_int(*pc);
- accu = Field(coq_env, *pc++);
+ print_instr("ENVACC");
+ print_int(*pc);
+ accu = Field(coq_env, *pc++);
Next;
}
/* Function application */
-
+
Instruct(PUSH_RETADDR) {
- print_instr("PUSH_RETADDR");
- sp -= 3;
- sp[0] = (value) (pc + *pc);
- sp[1] = coq_env;
- sp[2] = Val_long(coq_extra_args);
- coq_extra_args = 0;
- pc++;
- Next;
+ print_instr("PUSH_RETADDR");
+ sp -= 3;
+ sp[0] = (value) (pc + *pc);
+ sp[1] = coq_env;
+ sp[2] = Val_long(coq_extra_args);
+ coq_extra_args = 0;
+ pc++;
+ Next;
}
Instruct(APPLY) {
- print_instr("APPLY");
- coq_extra_args = *pc - 1;
- pc = Code_val(accu);
- coq_env = accu;
- goto check_stack;
+ print_instr("APPLY");
+ coq_extra_args = *pc - 1;
+ pc = Code_val(accu);
+ coq_env = accu;
+ goto check_stack;
}
Instruct(APPLY1) {
value arg1;
apply1:
- print_instr("APPLY1");
+ print_instr("APPLY1");
arg1 = sp[0];
- sp -= 3;
- sp[0] = arg1;
- 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;
- goto check_stack;
+ sp -= 3;
+ sp[0] = arg1;
+ 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;
+ goto check_stack;
}
Instruct(APPLY2) {
value arg1;
value arg2;
apply2:
- print_instr("APPLY2");
+ print_instr("APPLY2");
arg1 = sp[0];
arg2 = sp[1];
- sp -= 3;
- sp[0] = arg1;
- sp[1] = arg2;
- sp[2] = (value)pc;
- sp[3] = coq_env;
- sp[4] = Val_long(coq_extra_args);
- pc = Code_val(accu);
- coq_env = accu;
- coq_extra_args = 1;
- goto check_stack;
+ sp -= 3;
+ sp[0] = arg1;
+ sp[1] = arg2;
+ sp[2] = (value)pc;
+ sp[3] = coq_env;
+ sp[4] = Val_long(coq_extra_args);
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args = 1;
+ goto check_stack;
}
Instruct(APPLY3) {
@@ -463,21 +467,21 @@ value coq_interprete
value arg2;
value arg3;
apply3:
- print_instr("APPLY3");
+ print_instr("APPLY3");
arg1 = sp[0];
arg2 = sp[1];
arg3 = sp[2];
- sp -= 3;
- sp[0] = arg1;
- sp[1] = arg2;
- sp[2] = arg3;
- sp[3] = (value)pc;
- sp[4] = coq_env;
- sp[5] = Val_long(coq_extra_args);
- pc = Code_val(accu);
- coq_env = accu;
- coq_extra_args = 2;
- goto check_stack;
+ sp -= 3;
+ sp[0] = arg1;
+ sp[1] = arg2;
+ sp[2] = arg3;
+ sp[3] = (value)pc;
+ sp[4] = coq_env;
+ sp[5] = Val_long(coq_extra_args);
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args = 2;
+ goto check_stack;
}
Instruct(APPLY4) {
@@ -501,16 +505,32 @@ value coq_interprete
}
/* Stack checks */
-
+
check_stack:
print_instr("check_stack");
CHECK_STACK(0);
/* We also check for signals */
+#if OCAML_VERSION >= 41000
+ {
+ value res = caml_process_pending_actions_exn();
+ if (Is_exception_result(res)) {
+ /* If there is an asynchronous exception, we reset the vm */
+ coq_sp = coq_stack_high;
+ caml_raise(Extract_exception(res));
+ }
+ }
+#else
if (caml_signals_are_pending) {
- /* If there's a Ctrl-C, we reset the vm */
- if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; }
- caml_process_pending_signals();
+ /* If there's a Ctrl-C, we reset the vm */
+ intnat sigint = caml_pending_signals[SIGINT];
+ if (sigint) { coq_sp = coq_stack_high; }
+ caml_process_pending_signals();
+ if (sigint) {
+ caml_failwith("Coq VM: Fatal error: SIGINT signal detected "
+ "but no exception was raised");
+ }
}
+#endif
Next;
Instruct(ENSURESTACKCAPACITY) {
@@ -524,460 +544,460 @@ value coq_interprete
}
Instruct(APPTERM) {
- int nargs = *pc++;
- int slotsize = *pc;
- value * newsp;
- int i;
- print_instr("APPTERM");
- /* Slide the nargs bottom words of the current frame to the top
- of the frame, and discard the remainder of the frame */
- newsp = sp + slotsize - nargs;
- for (i = nargs - 1; i >= 0; i--) newsp[i] = sp[i];
- sp = newsp;
- pc = Code_val(accu);
- coq_env = accu;
- coq_extra_args += nargs - 1;
- goto check_stack;
+ int nargs = *pc++;
+ int slotsize = *pc;
+ value * newsp;
+ int i;
+ print_instr("APPTERM");
+ /* Slide the nargs bottom words of the current frame to the top
+ of the frame, and discard the remainder of the frame */
+ newsp = sp + slotsize - nargs;
+ for (i = nargs - 1; i >= 0; i--) newsp[i] = sp[i];
+ sp = newsp;
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args += nargs - 1;
+ goto check_stack;
}
Instruct(APPTERM1) {
- value arg1 = sp[0];
- print_instr("APPTERM1");
- sp = sp + *pc - 1;
- sp[0] = arg1;
- pc = Code_val(accu);
- coq_env = accu;
- goto check_stack;
+ value arg1 = sp[0];
+ print_instr("APPTERM1");
+ sp = sp + *pc - 1;
+ sp[0] = arg1;
+ pc = Code_val(accu);
+ coq_env = accu;
+ goto check_stack;
}
Instruct(APPTERM2) {
- value arg1 = sp[0];
- value arg2 = sp[1];
- print_instr("APPTERM2");
- sp = sp + *pc - 2;
- sp[0] = arg1;
- sp[1] = arg2;
- pc = Code_val(accu);
- print_lint(accu);
- coq_env = accu;
- coq_extra_args += 1;
- goto check_stack;
+ value arg1 = sp[0];
+ value arg2 = sp[1];
+ print_instr("APPTERM2");
+ sp = sp + *pc - 2;
+ sp[0] = arg1;
+ sp[1] = arg2;
+ pc = Code_val(accu);
+ print_lint(accu);
+ coq_env = accu;
+ coq_extra_args += 1;
+ goto check_stack;
}
Instruct(APPTERM3) {
- value arg1 = sp[0];
- value arg2 = sp[1];
- value arg3 = sp[2];
- print_instr("APPTERM3");
- sp = sp + *pc - 3;
- sp[0] = arg1;
- sp[1] = arg2;
- sp[2] = arg3;
- pc = Code_val(accu);
- coq_env = accu;
- coq_extra_args += 2;
- goto check_stack;
- }
-
+ value arg1 = sp[0];
+ value arg2 = sp[1];
+ value arg3 = sp[2];
+ print_instr("APPTERM3");
+ sp = sp + *pc - 3;
+ sp[0] = arg1;
+ sp[1] = arg2;
+ sp[2] = arg3;
+ pc = Code_val(accu);
+ coq_env = accu;
+ coq_extra_args += 2;
+ goto check_stack;
+ }
+
Instruct(RETURN) {
- 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]);
- sp += 3;
- }
- Next;
- }
-
+ 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]);
+ sp += 3;
+ }
+ Next;
+ }
+
Instruct(RESTART) {
- int num_args = Wosize_val(coq_env) - 2;
- int i;
- print_instr("RESTART");
+ int num_args = Wosize_val(coq_env) - 2;
+ 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);
- coq_extra_args += num_args;
- Next;
+ sp -= num_args;
+ for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2);
+ coq_env = Field(coq_env, 1);
+ coq_extra_args += num_args;
+ Next;
}
-
+
Instruct(GRAB) {
- int required = *pc++;
- print_instr("GRAB");
- /* printf("GRAB %d\n",required); */
- if (coq_extra_args >= required) {
- coq_extra_args -= required;
- } 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];
- Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
- sp += num_args;
- pc = (code_t)(sp[0]);
- coq_env = sp[1];
- coq_extra_args = Long_val(sp[2]);
- sp += 3;
- }
- Next;
- }
-
- Instruct(GRABREC) {
- 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 */
- } else {
- if (coq_extra_args < rec_pos) {
+ int required = *pc++;
+ print_instr("GRAB");
+ /* printf("GRAB %d\n",required); */
+ if (coq_extra_args >= required) {
+ coq_extra_args -= required;
+ } 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];
+ Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
+ sp += num_args;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ }
+ Next;
+ }
+
+ Instruct(GRABREC) {
+ 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 */
+ } 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;
- sp += num_args;
- pc = (code_t)(sp[0]);
- coq_env = sp[1];
- coq_extra_args = Long_val(sp[2]);
- sp += 3;
- } else {
- /* The recursif argument is an accumulator */
- mlsize_t num_args, i;
- /* 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 */
- 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;
- pc = (code_t)(sp[0]);
- coq_env = sp[1];
- coq_extra_args = Long_val(sp[2]);
- sp += 3;
- }
- }
- Next;
- }
-
+ 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;
+ sp += num_args;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ } else {
+ /* The recursif argument is an accumulator */
+ mlsize_t num_args, i;
+ /* 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 */
+ 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;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ }
+ }
+ Next;
+ }
+
Instruct(CLOSURE) {
- int nvars = *pc++;
- int i;
- print_instr("CLOSURE");
- print_int(nvars);
- if (nvars > 0) *--sp = accu;
- Alloc_small(accu, 1 + nvars, Closure_tag);
- Code_val(accu) = pc + *pc;
- pc++;
- for (i = 0; i < nvars; i++) {
- print_lint(sp[i]);
- Field(accu, i + 1) = sp[i];
- }
- sp += nvars;
- Next;
+ int nvars = *pc++;
+ int i;
+ print_instr("CLOSURE");
+ print_int(nvars);
+ if (nvars > 0) *--sp = accu;
+ Alloc_small(accu, 1 + nvars, Closure_tag);
+ Code_val(accu) = pc + *pc;
+ pc++;
+ for (i = 0; i < nvars; i++) {
+ print_lint(sp[i]);
+ Field(accu, i + 1) = sp[i];
+ }
+ sp += nvars;
+ Next;
}
Instruct(CLOSUREREC) {
- int nfuncs = *pc++;
- int nvars = *pc++;
- int start = *pc++;
- int i;
- value * p;
- print_instr("CLOSUREREC");
- if (nvars > 0) *--sp = accu;
- /* construction du vecteur de type */
+ int nfuncs = *pc++;
+ int nvars = *pc++;
+ int start = *pc++;
+ int i;
+ value * p;
+ print_instr("CLOSUREREC");
+ if (nvars > 0) *--sp = accu;
+ /* construction du vecteur de type */
Alloc_small(accu, nfuncs, Abstract_tag);
- for(i = 0; i < nfuncs; i++) {
- Field(accu,i) = (value)(pc+pc[i]);
- }
- 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++;
- }
- p = &Field(accu, 0);
- *p = (value) (pc + pc[0]);
- p++;
- for (i = 1; i < nfuncs; i++) {
- *p = Make_header(i * 2, Infix_tag, Caml_white);
- p++; /* color irrelevant. */
- *p = (value) (pc + pc[i]);
- p++;
- }
- pc += nfuncs;
- accu = accu + 2 * start * sizeof(value);
- Next;
- }
-
- Instruct(CLOSURECOFIX){
- int nfunc = *pc++;
- int nvars = *pc++;
- int start = *pc++;
- int i, j , size;
- value * p;
- print_instr("CLOSURECOFIX");
- if (nvars > 0) *--sp = accu;
- /* construction du vecteur de type */
+ for(i = 0; i < nfuncs; i++) {
+ Field(accu,i) = (value)(pc+pc[i]);
+ }
+ 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++;
+ }
+ p = &Field(accu, 0);
+ *p = (value) (pc + pc[0]);
+ p++;
+ for (i = 1; i < nfuncs; i++) {
+ *p = Make_header(i * 2, Infix_tag, Caml_white);
+ p++; /* color irrelevant. */
+ *p = (value) (pc + pc[i]);
+ p++;
+ }
+ pc += nfuncs;
+ accu = accu + 2 * start * sizeof(value);
+ Next;
+ }
+
+ Instruct(CLOSURECOFIX){
+ int nfunc = *pc++;
+ int nvars = *pc++;
+ int start = *pc++;
+ int i, j , size;
+ value * p;
+ print_instr("CLOSURECOFIX");
+ if (nvars > 0) *--sp = accu;
+ /* construction du vecteur de type */
Alloc_small(accu, nfunc, Abstract_tag);
- for(i = 0; i < nfunc; i++) {
- Field(accu,i) = (value)(pc+pc[i]);
- }
- pc += nfunc;
- *--sp=accu;
+ for(i = 0; i < nfunc; i++) {
+ Field(accu,i) = (value)(pc+pc[i]);
+ }
+ pc += nfunc;
+ *--sp=accu;
/* Creation des blocks accumulate */
for(i=0; i < nfunc; i++) {
- Alloc_small(accu, 2, Accu_tag);
- Code_val(accu) = accumulate;
- Field(accu,1) = Val_int(1);
- *--sp=accu;
- }
- /* creation des fonction cofix */
+ Alloc_small(accu, 2, Accu_tag);
+ Code_val(accu) = accumulate;
+ Field(accu,1) = Val_int(1);
+ *--sp=accu;
+ }
+ /* creation des fonction cofix */
p = sp;
- size = nfunc + nvars + 2;
- for (i=0; i < nfunc; i++) {
-
- 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, size - 1) = p[nfunc];
- for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = p[j];
- *--sp = accu;
+ size = nfunc + nvars + 2;
+ for (i=0; i < nfunc; i++) {
+
+ 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, 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++;
- }
- pc += nfunc;
- accu = p[start];
+ 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++;
+ }
+ pc += nfunc;
+ accu = p[start];
sp = p + nfunc + 1 + nvars;
- print_instr("ici4");
- Next;
+ print_instr("ici4");
+ Next;
}
-
+
Instruct(PUSHOFFSETCLOSURE) {
- print_instr("PUSHOFFSETCLOSURE");
- *--sp = accu;
+ print_instr("PUSHOFFSETCLOSURE");
+ *--sp = accu;
} /* fallthrough */
Instruct(OFFSETCLOSURE) {
- print_instr("OFFSETCLOSURE");
- accu = coq_env + *pc++ * sizeof(value); Next;
+ print_instr("OFFSETCLOSURE");
+ accu = coq_env + *pc++ * sizeof(value); Next;
}
Instruct(PUSHOFFSETCLOSUREM2) {
- print_instr("PUSHOFFSETCLOSUREM2");
- *--sp = accu;
+ print_instr("PUSHOFFSETCLOSUREM2");
+ *--sp = accu;
} /* fallthrough */
Instruct(OFFSETCLOSUREM2) {
- print_instr("OFFSETCLOSUREM2");
- accu = coq_env - 2 * sizeof(value); Next;
+ print_instr("OFFSETCLOSUREM2");
+ accu = coq_env - 2 * sizeof(value); Next;
}
Instruct(PUSHOFFSETCLOSURE0) {
- print_instr("PUSHOFFSETCLOSURE0");
- *--sp = accu;
+ print_instr("PUSHOFFSETCLOSURE0");
+ *--sp = accu;
}/* fallthrough */
Instruct(OFFSETCLOSURE0) {
- print_instr("OFFSETCLOSURE0");
- accu = coq_env; Next;
+ print_instr("OFFSETCLOSURE0");
+ accu = coq_env; Next;
}
Instruct(PUSHOFFSETCLOSURE2){
- print_instr("PUSHOFFSETCLOSURE2");
- *--sp = accu; /* fallthrough */
+ print_instr("PUSHOFFSETCLOSURE2");
+ *--sp = accu; /* fallthrough */
}
Instruct(OFFSETCLOSURE2) {
- print_instr("OFFSETCLOSURE2");
- accu = coq_env + 2 * sizeof(value); Next;
+ print_instr("OFFSETCLOSURE2");
+ accu = coq_env + 2 * sizeof(value); Next;
}
/* Access to global variables */
Instruct(PUSHGETGLOBAL) {
- print_instr("PUSH");
- *--sp = accu;
+ print_instr("PUSH");
+ *--sp = accu;
}
/* Fallthrough */
Instruct(GETGLOBAL){
- print_instr("GETGLOBAL");
- print_int(*pc);
- accu = Field(coq_global_data, *pc);
+ print_instr("GETGLOBAL");
+ print_int(*pc);
+ accu = Field(coq_global_data, *pc);
pc++;
Next;
- }
+ }
/* Allocation of blocks */
Instruct(MAKEBLOCK) {
- mlsize_t wosize = *pc++;
- tag_t tag = *pc++;
- mlsize_t i;
- value block;
- print_instr("MAKEBLOCK, tag=");
- Alloc_small(block, wosize, tag);
- Field(block, 0) = accu;
- for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
- accu = block;
- Next;
+ mlsize_t wosize = *pc++;
+ tag_t tag = *pc++;
+ mlsize_t i;
+ value block;
+ print_instr("MAKEBLOCK, tag=");
+ Alloc_small(block, wosize, tag);
+ Field(block, 0) = accu;
+ for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
+ accu = block;
+ Next;
}
Instruct(MAKEBLOCK1) {
-
- tag_t tag = *pc++;
- value block;
- print_instr("MAKEBLOCK1, tag=");
- print_int(tag);
- Alloc_small(block, 1, tag);
- Field(block, 0) = accu;
- accu = block;
- Next;
+
+ tag_t tag = *pc++;
+ value block;
+ print_instr("MAKEBLOCK1, tag=");
+ print_int(tag);
+ Alloc_small(block, 1, tag);
+ Field(block, 0) = accu;
+ accu = block;
+ Next;
}
Instruct(MAKEBLOCK2) {
-
- tag_t tag = *pc++;
- value block;
- print_instr("MAKEBLOCK2, tag=");
- print_int(tag);
- Alloc_small(block, 2, tag);
- Field(block, 0) = accu;
- Field(block, 1) = sp[0];
- sp += 1;
- accu = block;
- Next;
+
+ tag_t tag = *pc++;
+ value block;
+ print_instr("MAKEBLOCK2, tag=");
+ print_int(tag);
+ Alloc_small(block, 2, tag);
+ Field(block, 0) = accu;
+ Field(block, 1) = sp[0];
+ sp += 1;
+ accu = block;
+ Next;
}
Instruct(MAKEBLOCK3) {
- tag_t tag = *pc++;
- value block;
- print_instr("MAKEBLOCK3, tag=");
- print_int(tag);
- Alloc_small(block, 3, tag);
- Field(block, 0) = accu;
- Field(block, 1) = sp[0];
- Field(block, 2) = sp[1];
- sp += 2;
- accu = block;
- Next;
+ tag_t tag = *pc++;
+ value block;
+ print_instr("MAKEBLOCK3, tag=");
+ print_int(tag);
+ Alloc_small(block, 3, tag);
+ Field(block, 0) = accu;
+ Field(block, 1) = sp[0];
+ Field(block, 2) = sp[1];
+ sp += 2;
+ accu = block;
+ Next;
}
Instruct(MAKEBLOCK4) {
- tag_t tag = *pc++;
- value block;
- print_instr("MAKEBLOCK4, tag=");
- print_int(tag);
- Alloc_small(block, 4, tag);
- Field(block, 0) = accu;
- Field(block, 1) = sp[0];
- Field(block, 2) = sp[1];
- Field(block, 3) = sp[2];
- sp += 3;
- accu = block;
- Next;
- }
-
-
+ tag_t tag = *pc++;
+ value block;
+ print_instr("MAKEBLOCK4, tag=");
+ print_int(tag);
+ Alloc_small(block, 4, tag);
+ Field(block, 0) = accu;
+ Field(block, 1) = sp[0];
+ Field(block, 2) = sp[1];
+ Field(block, 3) = sp[2];
+ sp += 3;
+ accu = block;
+ Next;
+ }
+
+
/* Access to components of blocks */
-
+
Instruct(SWITCH) {
- uint32_t sizes = *pc++;
- print_instr("SWITCH");
- print_int(sizes & 0xFFFFFF);
- if (Is_block(accu)) {
- long index = Tag_val(accu);
- print_instr("block");
- print_lint(index);
- pc += pc[(sizes & 0xFFFFFF) + index];
- } else {
- long index = Long_val(accu);
- print_instr("constant");
- print_lint(index);
- pc += pc[index];
- }
- Next;
+ uint32_t sizes = *pc++;
+ print_instr("SWITCH");
+ print_int(sizes & 0xFFFFFF);
+ if (Is_block(accu)) {
+ long index = Tag_val(accu);
+ print_instr("block");
+ print_lint(index);
+ pc += pc[(sizes & 0xFFFFFF) + index];
+ } else {
+ long index = Long_val(accu);
+ print_instr("constant");
+ print_lint(index);
+ pc += pc[index];
+ }
+ Next;
}
Instruct(PUSHFIELDS){
- int i;
- int size = *pc++;
- print_instr("PUSHFIELDS");
- sp -= size;
- for(i=0;i<size;i++)sp[i] = Field(accu,i);
- Next;
- }
-
+ int i;
+ int size = *pc++;
+ print_instr("PUSHFIELDS");
+ sp -= size;
+ for(i=0;i<size;i++)sp[i] = Field(accu,i);
+ Next;
+ }
+
Instruct(GETFIELD0){
- print_instr("GETFIELD0");
- accu = Field(accu, 0);
- Next;
+ print_instr("GETFIELD0");
+ accu = Field(accu, 0);
+ Next;
}
Instruct(GETFIELD1){
- print_instr("GETFIELD1");
- accu = Field(accu, 1);
- Next;
+ print_instr("GETFIELD1");
+ accu = Field(accu, 1);
+ Next;
}
Instruct(GETFIELD){
- print_instr("GETFIELD");
- accu = Field(accu, *pc);
- pc++;
- Next;
+ print_instr("GETFIELD");
+ accu = Field(accu, *pc);
+ pc++;
+ Next;
}
-
+
Instruct(SETFIELD0){
- print_instr("SETFIELD0");
- caml_modify(&Field(accu, 0),*sp);
- sp++;
- Next;
+ print_instr("SETFIELD0");
+ caml_modify(&Field(accu, 0),*sp);
+ sp++;
+ Next;
}
-
+
Instruct(SETFIELD1){
- print_instr("SETFIELD1");
- caml_modify(&Field(accu, 1),*sp);
- sp++;
- Next;
+ print_instr("SETFIELD1");
+ caml_modify(&Field(accu, 1),*sp);
+ sp++;
+ Next;
}
-
+
Instruct(SETFIELD){
- print_instr("SETFIELD");
- caml_modify(&Field(accu, *pc),*sp);
- sp++; pc++;
- Next;
+ print_instr("SETFIELD");
+ caml_modify(&Field(accu, *pc),*sp);
+ sp++; pc++;
+ Next;
}
Instruct(PROJ){
do_proj:
- print_instr("PROJ");
- if (Is_accu (accu)) {
+ print_instr("PROJ");
+ if (Is_accu (accu)) {
*--sp = accu; // Save matched block on stack
accu = Field(accu, 1); // Save atom to accu register
switch (Tag_val(accu)) {
@@ -1023,135 +1043,135 @@ value coq_interprete
accu = block;
}
}
- } else {
+ } else {
accu = Field(accu, *pc);
pc += 2;
- }
- Next;
+ }
+ Next;
}
/* Integer constants */
Instruct(CONST0){
- print_instr("CONST0");
- accu = Val_int(0); Next;}
+ print_instr("CONST0");
+ accu = Val_int(0); Next;}
Instruct(CONST1){
- print_instr("CONST1");
- accu = Val_int(1); Next;}
+ print_instr("CONST1");
+ accu = Val_int(1); Next;}
Instruct(CONST2){
- print_instr("CONST2");
- accu = Val_int(2); Next;}
+ print_instr("CONST2");
+ accu = Val_int(2); Next;}
Instruct(CONST3){
- print_instr("CONST3");
- accu = Val_int(3); Next;}
-
+ print_instr("CONST3");
+ accu = Val_int(3); Next;}
+
Instruct(PUSHCONST0){
- print_instr("PUSHCONST0");
- *--sp = accu; accu = Val_int(0); Next;
+ print_instr("PUSHCONST0");
+ *--sp = accu; accu = Val_int(0); Next;
}
Instruct(PUSHCONST1){
- print_instr("PUSHCONST1");
- *--sp = accu; accu = Val_int(1); Next;
+ print_instr("PUSHCONST1");
+ *--sp = accu; accu = Val_int(1); Next;
}
Instruct(PUSHCONST2){
- print_instr("PUSHCONST2");
- *--sp = accu; accu = Val_int(2); Next;
+ print_instr("PUSHCONST2");
+ *--sp = accu; accu = Val_int(2); Next;
}
Instruct(PUSHCONST3){
- print_instr("PUSHCONST3");
- *--sp = accu; accu = Val_int(3); Next;
+ print_instr("PUSHCONST3");
+ *--sp = accu; accu = Val_int(3); Next;
}
Instruct(PUSHCONSTINT){
- print_instr("PUSHCONSTINT");
- *--sp = accu;
+ print_instr("PUSHCONSTINT");
+ *--sp = accu;
}
/* Fallthrough */
Instruct(CONSTINT) {
- print_instr("CONSTINT");
- print_int(*pc);
- accu = Val_int(*pc);
- pc++;
- Next;
+ print_instr("CONSTINT");
+ print_int(*pc);
+ accu = Val_int(*pc);
+ pc++;
+ Next;
}
/* Special operations for reduction of open term */
Instruct(ACCUMULATE) {
- mlsize_t i, size;
- print_instr("ACCUMULATE");
- size = Wosize_val(coq_env);
- Alloc_small(accu, size + coq_extra_args + 1, Accu_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++;
- pc = (code_t)(sp[0]);
- coq_env = sp[1];
- coq_extra_args = Long_val(sp[2]);
- sp += 3;
- Next;
- }
+ mlsize_t i, size;
+ print_instr("ACCUMULATE");
+ size = Wosize_val(coq_env);
+ Alloc_small(accu, size + coq_extra_args + 1, Accu_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++;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ Next;
+ }
Instruct(MAKESWITCHBLOCK) {
- print_instr("MAKESWITCHBLOCK");
- *--sp = accu; // Save matched block on stack
- accu = Field(accu,1); // Save atom to accu register
- switch (Tag_val(accu)) {
- case ATOM_COFIX_TAG: // We are forcing a cofix
- {
- mlsize_t i, nargs;
- print_instr("COFIX_TAG");
- sp-=2;
- pc++;
+ print_instr("MAKESWITCHBLOCK");
+ *--sp = accu; // Save matched block on stack
+ accu = Field(accu,1); // Save atom to accu register
+ switch (Tag_val(accu)) {
+ case ATOM_COFIX_TAG: // We are forcing a cofix
+ {
+ mlsize_t i, nargs;
+ print_instr("COFIX_TAG");
+ sp-=2;
+ pc++;
// Push the return address
- sp[0] = (value) (pc + *pc);
- sp[1] = coq_env;
- 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)
+ sp[0] = (value) (pc + *pc);
+ sp[1] = coq_env;
+ 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)
// Push arguments to stack
CHECK_STACK(nargs+1);
- sp -= nargs;
- for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
+ sp -= nargs;
+ for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
*--sp = accu; // Leftmost argument is the pointer to the suspension
- print_lint(nargs);
- coq_extra_args = nargs;
- pc = Code_val(coq_env); // Trigger evaluation
- goto check_stack;
- }
- case ATOM_COFIXEVALUATED_TAG:
- {
- print_instr("COFIX_EVAL_TAG");
- accu = Field(accu,1);
- pc++;
- pc = pc + *pc;
- sp++;
- Next;
- }
- default:
- {
- mlsize_t sz;
- int i, annot;
- code_t typlbl,swlbl;
- print_instr("MAKESWITCHBLOCK");
-
- typlbl = (code_t)pc + *pc;
- pc++;
- swlbl = (code_t)pc + *pc;
- pc++;
- annot = *pc++;
- sz = *pc++;
- *--sp=Field(coq_global_data, annot);
- /* We save the stack */
- if (sz == 0) accu = Atom(0);
- else {
- Alloc_small(accu, sz, Default_tag);
- if (Field(*sp, 2) == Val_true) {
- for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2];
- }else{
- for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5];
- }
- }
- *--sp = accu;
+ print_lint(nargs);
+ coq_extra_args = nargs;
+ pc = Code_val(coq_env); // Trigger evaluation
+ goto check_stack;
+ }
+ case ATOM_COFIXEVALUATED_TAG:
+ {
+ print_instr("COFIX_EVAL_TAG");
+ accu = Field(accu,1);
+ pc++;
+ pc = pc + *pc;
+ sp++;
+ Next;
+ }
+ default:
+ {
+ mlsize_t sz;
+ int i, annot;
+ code_t typlbl,swlbl;
+ print_instr("MAKESWITCHBLOCK");
+
+ typlbl = (code_t)pc + *pc;
+ pc++;
+ swlbl = (code_t)pc + *pc;
+ pc++;
+ annot = *pc++;
+ sz = *pc++;
+ *--sp=Field(coq_global_data, annot);
+ /* We save the stack */
+ if (sz == 0) accu = Atom(0);
+ else {
+ Alloc_small(accu, sz, Default_tag);
+ if (Field(*sp, 2) == Val_true) {
+ for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2];
+ }else{
+ for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5];
+ }
+ }
+ *--sp = accu;
/* Create bytecode wrappers */
Alloc_small(accu, 1, Abstract_tag);
Code_val(accu) = typlbl;
@@ -1168,47 +1188,47 @@ value coq_interprete
Field(accu, 4) = coq_env;
sp += 3;
sp[0] = accu;
- /* 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;
- /* We create the accumulator */
- Alloc_small(accu, 2, Accu_tag);
- Code_val(accu) = accumulate;
- Field(accu,1) = *sp++;
- }
- }
- Next;
- }
-
-
-
+ /* 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;
+ /* We create the accumulator */
+ Alloc_small(accu, 2, Accu_tag);
+ Code_val(accu) = accumulate;
+ Field(accu,1) = *sp++;
+ }
+ }
+ Next;
+ }
+
+
+
Instruct(MAKEACCU) {
- int i;
- print_instr("MAKEACCU");
- Alloc_small(accu, coq_extra_args + 3, Accu_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++;
- pc = (code_t)(sp[0]);
- coq_env = sp[1];
- coq_extra_args = Long_val(sp[2]);
- sp += 3;
- Next;
- }
-
+ int i;
+ print_instr("MAKEACCU");
+ Alloc_small(accu, coq_extra_args + 3, Accu_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++;
+ pc = (code_t)(sp[0]);
+ coq_env = sp[1];
+ coq_extra_args = Long_val(sp[2]);
+ sp += 3;
+ Next;
+ }
+
Instruct(MAKEPROD) {
- print_instr("MAKEPROD");
- *--sp=accu;
- Alloc_small(accu,2,0);
- Field(accu, 0) = sp[0];
- Field(accu, 1) = sp[1];
- sp += 2;
- Next;
+ print_instr("MAKEPROD");
+ *--sp=accu;
+ Alloc_small(accu,2,0);
+ Field(accu, 0) = sp[0];
+ Field(accu, 1) = sp[1];
+ sp += 2;
+ Next;
}
Instruct(BRANCH) {
- /* unconditional branching */
+ /* unconditional branching */
print_instr("BRANCH");
pc += *pc;
/* pc = (code_t)(pc+*pc); */
@@ -1220,7 +1240,7 @@ value coq_interprete
CheckInt2();
}
Instruct(ADDINT63) {
- /* Adds the integer in the accumulator with
+ /* Adds the integer in the accumulator with
the one ontop of the stack (which is poped)*/
print_instr("ADDINT63");
Uint63_add(accu, *sp++);
@@ -1230,27 +1250,27 @@ value coq_interprete
Instruct (CHECKADDCINT63) {
print_instr("CHECKADDCINT63");
CheckInt2();
- /* returns the sum with a carry */
+ /* returns the sum with a carry */
int c;
Uint63_add(accu, *sp);
Uint63_lt(c, accu, *sp);
Swap_accu_sp;
AllocCarry(c);
Field(accu, 0) = *sp++;
- Next;
+ Next;
}
Instruct (CHECKADDCARRYCINT63) {
print_instr("ADDCARRYCINT63");
CheckInt2();
- /* returns the sum plus one with a carry */
+ /* returns the sum plus one with a carry */
int c;
Uint63_addcarry(accu, *sp);
Uint63_leq(c, accu, *sp);
Swap_accu_sp;
AllocCarry(c);
Field(accu, 0) = *sp++;
- Next;
+ Next;
}
Instruct (CHECKSUBINT63) {
@@ -1259,7 +1279,7 @@ value coq_interprete
}
Instruct (SUBINT63) {
print_instr("SUBINT63");
- /* returns the subtraction */
+ /* returns the subtraction */
Uint63_sub(accu, *sp++);
Next;
}
@@ -1267,35 +1287,35 @@ value coq_interprete
Instruct (CHECKSUBCINT63) {
print_instr("SUBCINT63");
CheckInt2();
- /* returns the subtraction with a carry */
+ /* returns the subtraction with a carry */
int c;
Uint63_lt(c, accu, *sp);
Uint63_sub(accu, *sp);
Swap_accu_sp;
AllocCarry(c);
Field(accu, 0) = *sp++;
- Next;
+ Next;
}
Instruct (CHECKSUBCARRYCINT63) {
print_instr("SUBCARRYCINT63");
CheckInt2();
- /* returns the subtraction minus one with a carry */
+ /* returns the subtraction minus one with a carry */
int c;
Uint63_leq(c,accu,*sp);
Uint63_subcarry(accu,*sp);
Swap_accu_sp;
AllocCarry(c);
Field(accu, 0) = *sp++;
- Next;
+ Next;
}
Instruct (CHECKMULINT63) {
print_instr("MULINT63");
CheckInt2();
- /* returns the multiplication */
+ /* returns the multiplication */
Uint63_mul(accu,*sp++);
- Next;
+ Next;
}
Instruct (CHECKMULCINT63) {
@@ -1320,11 +1340,11 @@ value coq_interprete
Uint63_eq0(b, *sp);
if (b) {
accu = *sp++;
- }
- else {
+ }
+ else {
Uint63_div(accu, *sp++);
}
- Next;
+ Next;
}
Instruct(CHECKMODINT63) {
@@ -1334,11 +1354,11 @@ value coq_interprete
Uint63_eq0(b, *sp);
if (b) {
accu = *sp++;
- }
+ }
else {
Uint63_mod(accu,*sp++);
- }
- Next;
+ }
+ Next;
}
Instruct (CHECKDIVEUCLINT63) {
@@ -1366,7 +1386,7 @@ value coq_interprete
Field(accu, 1) = sp[0];
sp += 2;
}
- Next;
+ Next;
}
Instruct (CHECKDIV21INT63) {
@@ -1520,14 +1540,14 @@ value coq_interprete
Instruct (ISINT){
print_instr("ISINT");
accu = (Is_uint63(accu)) ? coq_true : coq_false;
- Next;
+ Next;
}
Instruct (AREINT2){
print_instr("AREINT2");
accu = (Is_uint63(accu) && Is_uint63(sp[0])) ? coq_true : coq_false;
sp++;
- Next;
+ Next;
}
@@ -1734,16 +1754,16 @@ value coq_interprete
/* Debugging and machine control */
Instruct(STOP){
- print_instr("STOP");
- coq_sp = sp;
+ print_instr("STOP");
+ coq_sp = sp;
CAMLreturn(accu);
}
-
-
+
+
#ifndef THREADED_CODE
default:
/*fprintf(stderr, "%d\n", *pc);*/
- failwith("Coq VM: Fatal error: bad opcode");
+ caml_failwith("Coq VM: Fatal error: bad opcode");
}
}
#endif
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index a1c49bee95..91d6773b1f 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -9,7 +9,7 @@
/***********************************************************************/
#include <stdio.h>
-#include <string.h>
+#include <string.h>
#include <caml/alloc.h>
#include <caml/address_class.h>
#include "coq_gc.h"
@@ -31,7 +31,7 @@ int drawinstr;
long coq_saved_sp_offset;
value * coq_sp;
-/* Some predefined pointer code */
+/* Some predefined pointer code */
code_t accumulate;
/* functions over global environment */
@@ -80,7 +80,7 @@ void init_coq_stack()
coq_stack_high = coq_stack_low + Coq_stack_size / sizeof (value);
coq_stack_threshold = coq_stack_low + Coq_stack_threshold / sizeof(value);
coq_max_stack_size = Coq_max_stack_size;
-}
+}
void init_coq_interpreter()
{
@@ -96,14 +96,14 @@ value init_coq_vm(value unit) /* ML */
fprintf(stderr,"already open \n");fflush(stderr);}
else {
drawinstr=0;
-#ifdef THREADED_CODE
+#ifdef THREADED_CODE
init_arity();
#endif /* THREADED_CODE */
/* Allocate the table of global and the stack */
init_coq_stack();
/* Initialing the interpreter */
init_coq_interpreter();
-
+
/* Some predefined pointer code.
* It is typically contained in accumulator blocks whose tag is 0 and thus
* scanned by the GC, so make it look like an OCaml block. */
@@ -117,7 +117,7 @@ value init_coq_vm(value unit) /* ML */
coq_prev_scan_roots_hook = scan_roots_hook;
scan_roots_hook = coq_scan_roots;
coq_vm_initialized = 1;
- }
+ }
return Val_unit;;
}
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index 1ea461c5e5..7f982d0477 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -39,7 +39,7 @@ extern int drawinstr;
/* interp state */
extern value * coq_sp;
-/* Some predefined pointer code */
+/* Some predefined pointer code */
extern code_t accumulate;
/* functions over global environment */
@@ -49,7 +49,7 @@ value coq_static_alloc(value size); /* ML */
value init_coq_vm(value unit); /* ML */
value re_init_coq_vm(value unit); /* ML */
-void realloc_coq_stack(asize_t required_space);
+void realloc_coq_stack(asize_t required_space);
value coq_set_transp_value(value transp); /* ML */
value get_coq_transp_value(value unit); /* ML */
#endif /* _COQ_MEMORY_ */
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index e05f3fb82e..bbe91da628 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -39,8 +39,8 @@ value coq_closure_arity(value clos) {
if (Is_instruction(c,RESTART)) {
c++;
if (Is_instruction(c,GRAB)) return Val_int(3 + c[1] - Wosize_val(clos));
- else {
- if (Wosize_val(clos) != 2) failwith("Coq Values : coq_closure_arity");
+ else {
+ if (Wosize_val(clos) != 2) caml_failwith("Coq Values : coq_closure_arity");
return Val_int(1);
}
}
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index 8d8374a603..2998178be2 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -2,8 +2,10 @@
(name byterun)
(synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
(public_name coq.vm)
- (c_flags (:include %{project_root}/config/dune.c_flags))
- (c_names coq_fix_code coq_memory coq_values coq_interp))
+ (foreign_stubs
+ (language c)
+ (names coq_fix_code coq_memory coq_values coq_interp)
+ (flags (:include %{project_root}/config/dune.c_flags))))
(rule
(targets coq_instruct.h)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 9d7387c7ad..261a3510d6 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -315,10 +315,6 @@ let refresh_polymorphic_type_of_inductive (_,mip) =
let ctx = List.rev mip.mind_arity_ctxt in
mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true
-let dummy_variance = let open Entries in function
- | Monomorphic_entry _ -> assert false
- | Polymorphic_entry (_,uctx) -> Array.make (Univ.UContext.size uctx) Univ.Variance.Irrelevant
-
let cook_inductive { Opaqueproof.modlist; abstract } mib =
let open Entries in
let (section_decls, subst, abs_uctx) = abstract in
@@ -333,10 +329,6 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
let auctx = Univ.AUContext.repr auctx in
subst, Polymorphic_entry (nas, auctx)
in
- let variance = match mib.mind_variance with
- | None -> None
- | Some _ -> Some (dummy_variance ind_univs)
- in
let cache = RefTable.create 13 in
let discharge c = Vars.subst_univs_level_constr subst (expmod_constr cache modlist c) in
let inds =
@@ -363,7 +355,7 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
mind_entry_params = params';
mind_entry_inds = inds';
mind_entry_private = mib.mind_private;
- mind_entry_variance = variance;
+ mind_entry_cumulative = Option.has_some mib.mind_variance;
mind_entry_universes = ind_univs
}
diff --git a/kernel/entries.ml b/kernel/entries.ml
index b50c3ebbc3..8d930b521c 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -50,7 +50,7 @@ type mutual_inductive_entry = {
mind_entry_params : Constr.rel_context;
mind_entry_inds : one_inductive_entry list;
mind_entry_universes : universes_entry;
- mind_entry_variance : Univ.Variance.t array option;
+ mind_entry_cumulative : bool;
(* universe constraints and the constraints for subtyping of
inductive types in the block. *)
mind_entry_private : bool option;
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 257bd43083..bd5a000c2b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -296,7 +296,13 @@ val add_constraints : Univ.Constraint.t -> env -> env
(** Check constraints are satifiable in the environment. *)
val check_constraints : Univ.Constraint.t -> env -> bool
val push_context : ?strict:bool -> Univ.UContext.t -> env -> env
+(* [push_context ?(strict=false) ctx env] pushes the universe context to the environment.
+ @raise UGraph.AlreadyDeclared if one of the universes is already declared.
+*)
val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
+(* [push_context_set ?(strict=false) ctx env] pushes the universe context set
+ to the environment. It does not fail if one of the universes is already declared. *)
+
val push_constraints_to_env : 'a Univ.constrained -> env -> env
val push_subgraph : Univ.ContextSet.t -> env -> env
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index c91cb39fe2..d9ccf81619 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -61,64 +61,6 @@ let mind_check_names mie =
(************************************************************************)
-(************************** Cumulativity checking************************)
-(************************************************************************)
-
-(* Check arities and constructors *)
-let check_subtyping_arity_constructor env subst arcn numparams is_arity =
- let numchecked = ref 0 in
- let basic_check ev tp =
- if !numchecked < numparams then () else Reduction.conv_leq ev tp (subst tp);
- numchecked := !numchecked + 1
- in
- let check_typ typ typ_env =
- match typ with
- | LocalAssum (_, typ') ->
- begin
- try
- basic_check typ_env typ'; Environ.push_rel typ typ_env
- with Reduction.NotConvertible ->
- CErrors.anomaly ~label:"bad inductive subtyping relation"
- Pp.(str "Invalid subtyping relation")
- end
- | _ -> CErrors.anomaly Pp.(str "")
- in
- let typs, codom = Reduction.dest_prod env arcn in
- let last_env = Context.Rel.fold_outside check_typ typs ~init:env in
- if not is_arity then basic_check last_env codom else ()
-
-let check_cumulativity univs variances env_ar params data =
- let uctx = match univs with
- | Monomorphic_entry _ -> raise (InductiveError BadUnivs)
- | Polymorphic_entry (_,uctx) -> uctx
- in
- let instance = UContext.instance uctx in
- if Instance.length instance != Array.length variances then raise (InductiveError BadUnivs);
- let numparams = Context.Rel.nhyps params in
- let new_levels = Array.init (Instance.length instance)
- (fun i -> Level.(make (UGlobal.make DirPath.empty i)))
- in
- let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
- LMap.empty (Instance.to_array instance) new_levels
- in
- let dosubst = Vars.subst_univs_level_constr lmap in
- let instance_other = Instance.of_array new_levels in
- let constraints_other = Univ.subst_univs_level_constraints lmap (UContext.constraints uctx) in
- let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
- let env = Environ.push_context uctx_other env_ar in
- let subtyp_constraints =
- Univ.enforce_leq_variance_instances variances
- instance instance_other
- Constraint.empty
- in
- let env = Environ.add_constraints subtyp_constraints env in
- (* process individual inductive types: *)
- List.iter (fun (arity,lc) ->
- check_subtyping_arity_constructor env dosubst arity numparams true;
- Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc)
- data
-
-(************************************************************************)
(************************** Type checking *******************************)
(************************************************************************)
@@ -351,8 +293,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
let env_univs =
match mie.mind_entry_universes with
| Monomorphic_entry ctx ->
- let env = if has_template_poly then set_universes_lbound env Univ.Level.prop else env in
- push_context_set ctx env
+ if has_template_poly then
+ (* For that particular case, we typecheck the inductive in an environment
+ where the universes introduced by the definition are only [>= Prop] *)
+ let env = set_universes_lbound env Univ.Level.prop in
+ push_context_set ~strict:false ctx env
+ else
+ (* In the regular case, all universes are [> Set] *)
+ push_context_set ~strict:true ctx env
| Polymorphic_entry (_, ctx) -> push_context ctx env
in
@@ -389,11 +337,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
data, Some None
in
- let () = match mie.mind_entry_variance with
- | None -> ()
- | Some variances ->
- check_cumulativity mie.mind_entry_universes variances env_ar params (List.map pi1 data)
- in
+ (* TODO pass only the needed bits *)
+ let variance = InferCumulativity.infer_inductive env mie in
(* Abstract universes *)
let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
@@ -408,4 +353,4 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
Environ.push_rel_context ctx env
in
- env_ar_par, univs, mie.mind_entry_variance, record, params, Array.of_list data
+ env_ar_par, univs, variance, record, params, Array.of_list data
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 550c81ed82..77abe6b410 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -216,19 +216,11 @@ let infer_inductive env mie =
let open Entries in
let params = mie.mind_entry_params in
let entries = mie.mind_entry_inds in
- let variances =
- match mie.mind_entry_variance with
- | None -> None
- | Some _ ->
- let uctx = match mie.mind_entry_universes with
- | Monomorphic_entry _ -> assert false
- | Polymorphic_entry (_,uctx) -> uctx
- in
- try Some (infer_inductive_core env params entries uctx)
- with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant)
- in
- { mie with mind_entry_variance = variances }
-
-let dummy_variance = let open Entries in function
- | Monomorphic_entry _ -> assert false
- | Polymorphic_entry (_,uctx) -> Array.make (UContext.size uctx) Irrelevant
+ if not mie.mind_entry_cumulative then None
+ else
+ let uctx = match mie.mind_entry_universes with
+ | Monomorphic_entry _ -> assert false
+ | Polymorphic_entry (_,uctx) -> uctx
+ in
+ try Some (infer_inductive_core env params entries uctx)
+ with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant)
diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli
index a234e334d1..2bddfe21e2 100644
--- a/kernel/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
@@ -9,6 +9,4 @@
(************************************************************************)
val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
- Entries.mutual_inductive_entry
-
-val dummy_variance : Entries.universes_entry -> Univ.Variance.t array
+ Univ.Variance.t array option
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 2b83c2d868..f1e994b337 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -42,9 +42,9 @@ Type_errors
Modops
Inductive
Typeops
+InferCumulativity
IndTyping
Indtypes
-InferCumulativity
Cooking
Term_typing
Subtyping
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 06f5aae047..ee101400d6 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -122,7 +122,7 @@ type section_data = {
type safe_environment =
{ env : Environ.env;
- sections : section_data Section.t;
+ sections : section_data Section.t option;
modpath : ModPath.t;
modvariant : modvariant;
modresolver : Mod_subst.delta_resolver;
@@ -159,7 +159,7 @@ let empty_environment =
revstruct = [];
modlabels = Label.Set.empty;
objlabels = Label.Set.empty;
- sections = Section.empty;
+ sections = None;
future_cst = [];
univ = Univ.ContextSet.empty;
engagement = None;
@@ -173,7 +173,7 @@ let is_initial senv =
| [], NONE -> ModPath.equal senv.modpath ModPath.initial
| _ -> false
-let sections_are_opened senv = not (Section.is_empty senv.sections)
+let sections_are_opened senv = not (Option.is_empty senv.sections)
let delta_of_senv senv = senv.modresolver,senv.paramresolver
@@ -323,19 +323,21 @@ let env_of_senv = env_of_safe_env
let sections_of_safe_env senv = senv.sections
+let get_section = function
+ | None -> CErrors.user_err Pp.(str "No open section.")
+ | Some s -> s
+
type constraints_addition =
| Now of Univ.ContextSet.t
| Later of Univ.ContextSet.t Future.computation
-let push_context_set poly cst senv =
+let push_context_set ~strict cst senv =
if Univ.ContextSet.is_empty cst then senv
else
- let sections =
- if Section.is_empty senv.sections then senv.sections
- else Section.push_constraints cst senv.sections
+ let sections = Option.map (Section.push_constraints cst) senv.sections
in
{ senv with
- env = Environ.push_context_set ~strict:(not poly) cst senv.env;
+ env = Environ.push_context_set ~strict cst senv.env;
univ = Univ.ContextSet.union cst senv.univ;
sections }
@@ -344,7 +346,7 @@ let add_constraints cst senv =
| Later fc ->
{senv with future_cst = fc :: senv.future_cst}
| Now cst ->
- push_context_set false cst senv
+ push_context_set ~strict:true cst senv
let add_constraints_list cst senv =
List.fold_left (fun acc c -> add_constraints c acc) senv cst
@@ -399,7 +401,7 @@ let check_current_library dir senv = match senv.modvariant with
(** When operating on modules, we're normally outside sections *)
let check_empty_context senv =
- assert (Environ.empty_context senv.env && Section.is_empty senv.sections)
+ assert (Environ.empty_context senv.env && Option.is_empty senv.sections)
(** When adding a parameter to the current module/modtype,
it must have been freshly started *)
@@ -447,22 +449,25 @@ let safe_push_named d env =
Environ.push_named d env
let push_named_def (id,de) senv =
- let sections = Section.push_local senv.sections in
+ let sections = get_section senv.sections in
+ let sections = Section.push_local sections in
let c, r, typ = Term_typing.translate_local_def senv.env id de in
let x = Context.make_annot id r in
let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in
- { senv with sections; env = env'' }
+ { senv with sections=Some sections; env = env'' }
let push_named_assum (x,t) senv =
- let sections = Section.push_local senv.sections in
+ let sections = get_section senv.sections in
+ let sections = Section.push_local sections in
let t, r = Term_typing.translate_local_assum senv.env t in
let x = Context.make_annot x r in
let env'' = safe_push_named (LocalAssum (x,t)) senv.env in
- { senv with sections; env = env'' }
+ { senv with sections=Some sections; env = env'' }
let push_section_context (nas, ctx) senv =
- let sections = Section.push_context (nas, ctx) senv.sections in
- let senv = { senv with sections } in
+ let sections = get_section senv.sections in
+ let sections = Section.push_context (nas, ctx) sections in
+ let senv = { senv with sections=Some sections } in
let ctx = Univ.ContextSet.of_context ctx in
(* We check that the universes are fresh. FIXME: This should be done
implicitly, but we have to work around the API. *)
@@ -542,7 +547,7 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
else
(* Delayed constraints from opaque body are added by [add_constant_aux] *)
let cst = constraints_of_sfb sfb in
- List.fold_left (fun senv cst -> push_context_set false cst senv) senv cst
+ List.fold_left (fun senv cst -> push_context_set ~strict:true cst senv) senv cst
in
let env' = match sfb, gn with
| SFBconst cb, C con -> Environ.add_constant con cb senv.env
@@ -551,15 +556,18 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
| SFBmodule mb, M -> Modops.add_module mb senv.env
| _ -> assert false
in
- let sections = match sfb, gn with
- | SFBconst cb, C con ->
- let poly = Declareops.constant_is_polymorphic cb in
- Section.push_constant ~poly con senv.sections
- | SFBmind mib, I mind ->
- let poly = Declareops.inductive_is_polymorphic mib in
- Section.push_inductive ~poly mind senv.sections
- | _, (M | MT) -> senv.sections
- | _ -> assert false
+ let sections = match senv.sections with
+ | None -> None
+ | Some sections ->
+ match sfb, gn with
+ | SFBconst cb, C con ->
+ let poly = Declareops.constant_is_polymorphic cb in
+ Some (Section.push_constant ~poly con sections)
+ | SFBmind mib, I mind ->
+ let poly = Declareops.inductive_is_polymorphic mib in
+ Some (Section.push_inductive ~poly mind sections)
+ | _, (M | MT) -> Some sections
+ | _ -> assert false
in
{ senv with
env = env';
@@ -952,11 +960,11 @@ let open_section senv =
rev_objlabels = senv.objlabels;
} in
let sections = Section.open_section ~custom senv.sections in
- { senv with sections }
+ { senv with sections=Some sections }
let close_section senv =
let open Section in
- let sections0 = senv.sections in
+ let sections0 = get_section senv.sections in
let env0 = senv.env in
(* First phase: revert the declarations added in the section *)
let sections, entries, cstrs, revert = Section.close_section sections0 in
@@ -990,7 +998,7 @@ let close_section senv =
let env = Environ.set_opaque_tables env (Environ.opaque_tables senv.env) in
let senv = { senv with env; revstruct; sections; univ; objlabels; } in
(* Second phase: replay the discharged section contents *)
- let senv = add_constraints (Now cstrs) senv in
+ let senv = push_context_set ~strict:true cstrs senv in
let modlist = Section.replacement_context env0 sections0 in
let cooking_info seg =
let { abstr_ctx; abstr_subst; abstr_uctx } = seg in
@@ -1007,7 +1015,6 @@ let close_section senv =
| `Inductive (ind, mib) ->
let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
let mie = Cooking.cook_inductive info mib in
- let mie = InferCumulativity.infer_inductive senv.env mie in
let _, senv = add_mind (MutInd.label ind) mie senv in
senv
in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index ae6993b0e2..92bbd264fa 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -35,7 +35,7 @@ val is_initial : safe_environment -> bool
val env_of_safe_env : safe_environment -> Environ.env
-val sections_of_safe_env : safe_environment -> section_data Section.t
+val sections_of_safe_env : safe_environment -> section_data Section.t option
(** The safe_environment state monad *)
@@ -113,7 +113,7 @@ val add_modtype :
(** Adding universe constraints *)
val push_context_set :
- bool -> Univ.ContextSet.t -> safe_transformer0
+ strict:bool -> Univ.ContextSet.t -> safe_transformer0
val add_constraints :
Univ.Constraint.t -> safe_transformer0
diff --git a/kernel/section.ml b/kernel/section.ml
index a1242f0faf..603ef5d006 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -20,7 +20,9 @@ type section_entry =
type 'a entry_map = 'a Cmap.t * 'a Mindmap.t
-type 'a section = {
+type 'a t = {
+ sec_prev : 'a t option;
+ (** Section surrounding the current one *)
sec_context : int;
(** Length of the named context suffix that has been introduced locally *)
sec_mono_universes : ContextSet.t;
@@ -35,19 +37,9 @@ type 'a section = {
sec_custom : 'a;
}
-(** Sections can be nested with the proviso that no monomorphic section can be
- opened inside a polymorphic one. The reverse is allowed. *)
-type 'a t = 'a section list
+let rec depth sec = 1 + match sec.sec_prev with None -> 0 | Some prev -> depth prev
-let empty = []
-
-let is_empty = List.is_empty
-
-let depth = List.length
-
-let has_poly_univs = function
- | [] -> false
- | sec :: _ -> sec.has_poly_univs
+let has_poly_univs sec = sec.has_poly_univs
let find_emap e (cmap, imap) = match e with
| SecDefinition con -> Cmap.find con cmap
@@ -57,80 +49,59 @@ let add_emap e v (cmap, imap) = match e with
| SecDefinition con -> (Cmap.add con v cmap, imap)
| SecInductive ind -> (cmap, Mindmap.add ind v imap)
-let on_last_section f sections = match sections with
-| [] -> CErrors.user_err (Pp.str "No opened section")
-| sec :: rem -> f sec :: rem
-
-let with_last_section f sections = match sections with
-| [] -> f None
-| sec :: _ -> f (Some sec)
-
-let push_local s =
- let on_sec sec = { sec with sec_context = sec.sec_context + 1 } in
- on_last_section on_sec s
-
-let push_context (nas, ctx) s =
- let on_sec sec =
- if UContext.is_empty ctx then sec
- else
- let (snas, sctx) = sec.sec_poly_universes in
- let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in
- { sec with sec_poly_universes; has_poly_univs = true }
- in
- on_last_section on_sec s
-
-let is_polymorphic_univ u s =
- let check sec =
- let (_, uctx) = sec.sec_poly_universes in
- Array.exists (fun u' -> Level.equal u u') (Instance.to_array (UContext.instance uctx))
- in
- List.exists check s
-
-let push_constraints uctx s =
- let on_sec sec =
- if sec.has_poly_univs && Constraint.exists (fun (l,_,r) -> is_polymorphic_univ l s || is_polymorphic_univ r s) (snd uctx)
- then CErrors.user_err Pp.(str "Cannot add monomorphic constraints which refer to section polymorphic universes.");
- let uctx' = sec.sec_mono_universes in
- let sec_mono_universes = (ContextSet.union uctx uctx') in
- { sec with sec_mono_universes }
- in
- on_last_section on_sec s
-
-let open_section ~custom sections =
- let sec = {
+let push_local sec =
+ { sec with sec_context = sec.sec_context + 1 }
+
+let push_context (nas, ctx) sec =
+ if UContext.is_empty ctx then sec
+ else
+ let (snas, sctx) = sec.sec_poly_universes in
+ let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in
+ { sec with sec_poly_universes; has_poly_univs = true }
+
+let rec is_polymorphic_univ u sec =
+ let (_, uctx) = sec.sec_poly_universes in
+ let here = Array.exists (fun u' -> Level.equal u u') (Instance.to_array (UContext.instance uctx)) in
+ here || Option.cata (is_polymorphic_univ u) false sec.sec_prev
+
+let push_constraints uctx sec =
+ if sec.has_poly_univs &&
+ Constraint.exists
+ (fun (l,_,r) -> is_polymorphic_univ l sec || is_polymorphic_univ r sec)
+ (snd uctx)
+ then CErrors.user_err
+ Pp.(str "Cannot add monomorphic constraints which refer to section polymorphic universes.");
+ let uctx' = sec.sec_mono_universes in
+ let sec_mono_universes = (ContextSet.union uctx uctx') in
+ { sec with sec_mono_universes }
+
+let open_section ~custom sec_prev =
+ {
+ sec_prev;
sec_context = 0;
sec_mono_universes = ContextSet.empty;
sec_poly_universes = ([||], UContext.empty);
- has_poly_univs = has_poly_univs sections;
+ has_poly_univs = Option.cata has_poly_univs false sec_prev;
sec_entries = [];
sec_data = (Cmap.empty, Mindmap.empty);
sec_custom = custom;
- } in
- sec :: sections
+ }
-let close_section sections =
- match sections with
- | sec :: sections ->
- sections, sec.sec_entries, sec.sec_mono_universes, sec.sec_custom
- | [] ->
- CErrors.user_err (Pp.str "No opened section.")
+let close_section sec =
+ sec.sec_prev, sec.sec_entries, sec.sec_mono_universes, sec.sec_custom
let make_decl_univs (nas,uctx) = abstract_universes nas uctx
-let push_global ~poly e s =
- if is_empty s then s
- else if has_poly_univs s && not poly
+let push_global ~poly e sec =
+ if has_poly_univs sec && not poly
then CErrors.user_err
Pp.(str "Cannot add a universe monomorphic declaration when \
section polymorphic universes are present.")
else
- let on_sec sec =
- { sec with
- sec_entries = e :: sec.sec_entries;
- sec_data = add_emap e (make_decl_univs sec.sec_poly_universes) sec.sec_data;
- }
- in
- on_last_section on_sec s
+ { sec with
+ sec_entries = e :: sec.sec_entries;
+ sec_data = add_emap e (make_decl_univs sec.sec_poly_universes) sec.sec_data;
+ }
let push_constant ~poly con s = push_global ~poly (SecDefinition con) s
@@ -154,22 +125,16 @@ let extract_hyps sec vars used =
(* Only keep the part that is used by the declaration *)
List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) used) vars
-let section_segment_of_entry vars e hyps sections =
+let section_segment_of_entry vars e hyps sec =
(* [vars] are the named hypotheses, [hyps] the subset that is declared by the
- global *)
- let with_sec s = match s with
- | None ->
- CErrors.user_err (Pp.str "No opened section.")
- | Some sec ->
- let hyps = extract_hyps sec vars hyps in
- let inst, auctx = find_emap e sec.sec_data in
- {
- abstr_ctx = hyps;
- abstr_subst = inst;
- abstr_uctx = auctx;
- }
- in
- with_last_section with_sec sections
+ global *)
+ let hyps = extract_hyps sec vars hyps in
+ let inst, auctx = find_emap e sec.sec_data in
+ {
+ abstr_ctx = hyps;
+ abstr_subst = inst;
+ abstr_uctx = auctx;
+ }
let segment_of_constant env con s =
let body = Environ.lookup_constant con env in
@@ -190,29 +155,19 @@ let extract_worklist info =
let args = instance_from_variable_context info.abstr_ctx in
info.abstr_subst, args
-let replacement_context env s =
- let with_sec sec = match sec with
- | None -> CErrors.user_err (Pp.str "No opened section.")
- | Some sec ->
- let cmap, imap = sec.sec_data in
- let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con s) cmap in
- let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind s) imap in
- (cmap, imap)
- in
- with_last_section with_sec s
-
-let is_in_section env gr s =
- let with_sec sec = match sec with
- | None -> false
- | Some sec ->
- let open GlobRef in
- match gr with
- | VarRef id ->
- let vars = List.firstn sec.sec_context (Environ.named_context env) in
- List.exists (fun decl -> Id.equal id (NamedDecl.get_id decl)) vars
- | ConstRef con ->
- Cmap.mem con (fst sec.sec_data)
- | IndRef (ind, _) | ConstructRef ((ind, _), _) ->
- Mindmap.mem ind (snd sec.sec_data)
- in
- with_last_section with_sec s
+let replacement_context env sec =
+ let cmap, imap = sec.sec_data in
+ let cmap = Cmap.mapi (fun con _ -> extract_worklist @@ segment_of_constant env con sec) cmap in
+ let imap = Mindmap.mapi (fun ind _ -> extract_worklist @@ segment_of_inductive env ind sec) imap in
+ (cmap, imap)
+
+let is_in_section env gr sec =
+ let open GlobRef in
+ match gr with
+ | VarRef id ->
+ let vars = List.firstn sec.sec_context (Environ.named_context env) in
+ List.exists (fun decl -> Id.equal id (NamedDecl.get_id decl)) vars
+ | ConstRef con ->
+ Cmap.mem con (fst sec.sec_data)
+ | IndRef (ind, _) | ConstructRef ((ind, _), _) ->
+ Mindmap.mem ind (snd sec.sec_data)
diff --git a/kernel/section.mli b/kernel/section.mli
index ec863b3b90..fbd3d8254e 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -16,13 +16,8 @@ open Univ
type 'a t
(** Type of sections with additional data ['a] *)
-val empty : 'a t
-
-val is_empty : 'a t -> bool
-(** Checks whether there is no opened section *)
-
val depth : 'a t -> int
-(** Number of nested sections (0 if no sections are open) *)
+(** Number of nested sections. *)
(** {6 Manipulating sections} *)
@@ -30,13 +25,13 @@ type section_entry =
| SecDefinition of Constant.t
| SecInductive of MutInd.t
-val open_section : custom:'a -> 'a t -> 'a t
+val open_section : custom:'a -> 'a t option -> 'a t
(** Open a new section with the provided universe polymorphic status. Sections
can be nested, with the proviso that polymorphic sections cannot appear
inside a monomorphic one. A custom data can be attached to this section,
that will be returned by {!close_section}. *)
-val close_section : 'a t -> 'a t * section_entry list * ContextSet.t * 'a
+val close_section : 'a t -> 'a t option * section_entry list * ContextSet.t * 'a
(** Close the current section and returns the entries defined inside, the set
of global monomorphic constraints added in this section, and the custom data
provided at the opening of the section. *)
diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml
index e38389ca13..445166f6af 100644
--- a/kernel/uint63_31.ml
+++ b/kernel/uint63_31.ml
@@ -15,8 +15,8 @@ let _ = assert (Sys.word_size = 32)
let uint_size = 63
-let maxuint63 = Int64.of_string "0x7FFFFFFFFFFFFFFF"
-let maxuint31 = Int64.of_string "0x7FFFFFFF"
+let maxuint63 = 0x7FFF_FFFF_FFFF_FFFFL
+let maxuint31 = 0x7FFF_FFFFL
let zero = Int64.zero
let one = Int64.one
@@ -118,27 +118,30 @@ let div21 xh xl y =
let div21 xh xl y =
if Int64.compare y xh <= 0 then zero, zero else div21 xh xl y
- (* exact multiplication *)
+(* exact multiplication *)
let mulc x y =
- let lx = ref (Int64.logand x maxuint31) in
- let ly = ref (Int64.logand y maxuint31) in
+ let lx = Int64.logand x maxuint31 in
+ let ly = Int64.logand y maxuint31 in
let hx = Int64.shift_right x 31 in
let hy = Int64.shift_right y 31 in
- let hr = ref (Int64.mul hx hy) in
- let lr = ref (Int64.logor (Int64.mul !lx !ly) (Int64.shift_left !hr 62)) in
- hr := (Int64.shift_right_logical !hr 1);
- lx := Int64.mul !lx hy;
- ly := Int64.mul hx !ly;
- hr := Int64.logor !hr (Int64.add (Int64.shift_right !lx 32) (Int64.shift_right !ly 32));
- lr := Int64.add !lr (Int64.shift_left !lx 31);
- hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
- lr := Int64.add (Int64.shift_left !ly 31) (mask63 !lr);
- hr := Int64.add !hr (Int64.shift_right_logical !lr 63);
- if Int64.logand !lr Int64.min_int <> 0L
- then Int64.(sub !hr one, mask63 !lr)
- else (!hr, !lr)
-
-let equal x y = mask63 x = mask63 y
+ (* compute the median products *)
+ let s = Int64.add (Int64.mul lx hy) (Int64.mul hx ly) in
+ (* s fits on 64 bits, split it into a 33-bit high part and a 31-bit low part *)
+ let lr = Int64.shift_left (Int64.logand s maxuint31) 31 in
+ let hr = Int64.shift_right_logical s 31 in
+ (* add the outer products *)
+ let lr = Int64.add (Int64.mul lx ly) lr in
+ let hr = Int64.add (Int64.mul hx hy) hr in
+ (* hr fits on 64 bits, since the final result fits on 126 bits *)
+ (* now x * y = hr * 2^62 + lr and lr < 2^63 *)
+ let lr = Int64.add lr (Int64.shift_left (Int64.logand hr 1L) 62) in
+ let hr = Int64.shift_right_logical hr 1 in
+ (* now x * y = hr * 2^63 + lr, but lr might be too large *)
+ if Int64.logand lr Int64.min_int <> 0L
+ then Int64.add hr 1L, mask63 lr
+ else hr, lr
+
+let equal (x : t) y = x = y
let compare x y = Int64.compare x y
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 19:52:49 +0000