aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_interp.c234
-rw-r--r--kernel/byterun/coq_memory.h2
-rw-r--r--kernel/byterun/coq_uint63_emul.h137
-rw-r--r--kernel/byterun/coq_uint63_native.h104
-rw-r--r--kernel/entries.ml14
-rw-r--r--kernel/indtypes.ml17
-rw-r--r--kernel/indtypes.mli19
-rw-r--r--kernel/modops.ml6
-rw-r--r--kernel/names.ml3
-rw-r--r--kernel/names.mli3
-rw-r--r--kernel/nativecode.ml291
-rw-r--r--kernel/nativeconv.ml23
-rw-r--r--kernel/nativelambda.ml180
-rw-r--r--kernel/nativelambda.mli14
-rw-r--r--kernel/nativelib.ml25
-rw-r--r--kernel/nativelib.mli11
-rw-r--r--kernel/opaqueproof.ml29
-rw-r--r--kernel/opaqueproof.mli4
-rw-r--r--kernel/safe_typing.ml119
-rw-r--r--kernel/safe_typing.mli12
-rw-r--r--kernel/typeops.ml22
-rw-r--r--kernel/typeops.mli8
-rw-r--r--kernel/uint63.mli4
-rw-r--r--kernel/uint63_amd64.ml26
-rw-r--r--kernel/uint63_x86.ml25
-rw-r--r--kernel/univ.ml17
-rw-r--r--kernel/univ.mli4
27 files changed, 711 insertions, 642 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index d2c88bffcc..4b45608ae5 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -29,13 +29,6 @@
#include "coq_uint63_emul.h"
#endif
-/* spiwack: I append here a few macros for value/number manipulation */
-#define uint32_of_value(val) (((uint32_t)(val)) >> 1)
-#define value_of_uint32(i) ((value)((((uint32_t)(i)) << 1) | 1))
-#define UI64_of_uint32(lo) ((uint64_t)((uint32_t)(lo)))
-#define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val)))
-/* /spiwack */
-
/* Registers for the abstract machine:
@@ -104,7 +97,8 @@ if (sp - num_args < coq_stack_threshold) { \
several architectures.
*/
-#if defined(__GNUC__) && !defined(DEBUG)
+#if defined(__GNUC__) && !defined(DEBUG) && !defined(__INTEL_COMPILER) \
+ && !defined(__llvm__)
#ifdef __mips__
#define PC_REG asm("$16")
#define SP_REG asm("$17")
@@ -133,7 +127,7 @@ if (sp - num_args < coq_stack_threshold) { \
#define SP_REG asm("%edi")
#define ACCU_REG
#endif
-#if defined(PPC) || defined(_POWER) || defined(_IBMR2)
+#if defined(__ppc__) || defined(__ppc64__)
#define PC_REG asm("26")
#define SP_REG asm("27")
#define ACCU_REG asm("28")
@@ -148,8 +142,9 @@ if (sp - num_args < coq_stack_threshold) { \
#define SP_REG asm("a4")
#define ACCU_REG asm("d7")
#endif
-#if defined(__arm__) && !defined(__thumb2__)
-#define PC_REG asm("r9")
+/* OCaml PR#4953: these specific registers not available in Thumb mode */
+#if defined(__arm__) && !defined(__thumb__)
+#define PC_REG asm("r6")
#define SP_REG asm("r8")
#define ACCU_REG asm("r7")
#endif
@@ -159,6 +154,17 @@ if (sp - num_args < coq_stack_threshold) { \
#define ACCU_REG asm("38")
#define JUMPTBL_BASE_REG asm("39")
#endif
+#ifdef __x86_64__
+#define PC_REG asm("%r15")
+#define SP_REG asm("%r14")
+#define ACCU_REG asm("%r13")
+#endif
+#ifdef __aarch64__
+#define PC_REG asm("%x19")
+#define SP_REG asm("%x20")
+#define ACCU_REG asm("%x21")
+#define JUMPTBL_BASE_REG asm("%x22")
+#endif
#endif
#define CheckInt1() do{ \
@@ -193,6 +199,12 @@ if (sp - num_args < coq_stack_threshold) { \
#define AllocCarry(cond) Alloc_small(accu, 1, (cond)? coq_tag_C1 : coq_tag_C0)
#define AllocPair() Alloc_small(accu, 2, coq_tag_pair)
+#define Swap_accu_sp do{ \
+ value swap_accu_sp_tmp__ = accu; \
+ accu = *sp; \
+ *sp = swap_accu_sp_tmp__; \
+ }while(0)
+
/* For signal handling, we hijack some code from the caml runtime */
extern intnat caml_signals_are_pending;
@@ -1213,7 +1225,7 @@ value coq_interprete
/* Adds the integer in the accumulator with
the one ontop of the stack (which is poped)*/
print_instr("ADDINT63");
- accu = uint63_add(accu, *sp++);
+ Uint63_add(accu, *sp++);
Next;
}
@@ -1221,10 +1233,12 @@ value coq_interprete
print_instr("CHECKADDCINT63");
CheckInt2();
/* returns the sum with a carry */
- value s;
- s = uint63_add(accu, *sp++);
- AllocCarry(uint63_lt(s,accu));
- Field(accu, 0) = s;
+ int c;
+ Uint63_add(accu, *sp);
+ Uint63_lt(c, accu, *sp);
+ Swap_accu_sp;
+ AllocCarry(c);
+ Field(accu, 0) = *sp++;
Next;
}
@@ -1232,10 +1246,12 @@ value coq_interprete
print_instr("ADDCARRYCINT63");
CheckInt2();
/* returns the sum plus one with a carry */
- value s;
- s = uint63_addcarry(accu, *sp++);
- AllocCarry(uint63_leq(s, accu));
- Field(accu, 0) = s;
+ int c;
+ Uint63_addcarry(accu, *sp);
+ Uint63_leq(c, accu, *sp);
+ Swap_accu_sp;
+ AllocCarry(c);
+ Field(accu, 0) = *sp++;
Next;
}
@@ -1246,7 +1262,7 @@ value coq_interprete
Instruct (SUBINT63) {
print_instr("SUBINT63");
/* returns the subtraction */
- accu = uint63_sub(accu, *sp++);
+ Uint63_sub(accu, *sp++);
Next;
}
@@ -1254,12 +1270,12 @@ value coq_interprete
print_instr("SUBCINT63");
CheckInt2();
/* returns the subtraction with a carry */
- value b;
- value s;
- b = *sp++;
- s = uint63_sub(accu,b);
- AllocCarry(uint63_lt(accu,b));
- Field(accu, 0) = s;
+ int c;
+ Uint63_lt(c, accu, *sp);
+ Uint63_sub(accu, *sp);
+ Swap_accu_sp;
+ AllocCarry(c);
+ Field(accu, 0) = *sp++;
Next;
}
@@ -1267,12 +1283,12 @@ value coq_interprete
print_instr("SUBCARRYCINT63");
CheckInt2();
/* returns the subtraction minus one with a carry */
- value b;
- value s;
- b = *sp++;
- s = uint63_subcarry(accu,b);
- AllocCarry(uint63_leq(accu,b));
- Field(accu, 0) = s;
+ int c;
+ Uint63_leq(c,accu,*sp);
+ Uint63_subcarry(accu,*sp);
+ Swap_accu_sp;
+ AllocCarry(c);
+ Field(accu, 0) = *sp++;
Next;
}
@@ -1280,7 +1296,7 @@ value coq_interprete
print_instr("MULINT63");
CheckInt2();
/* returns the multiplication */
- accu = uint63_mul(accu,*sp++);
+ Uint63_mul(accu,*sp++);
Next;
}
@@ -1288,15 +1304,11 @@ value coq_interprete
/*returns the multiplication on a pair */
print_instr("MULCINT63");
CheckInt2();
- /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */
- /* TODO: implement
- p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1));
- AllocPair(); */
- /* Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; */ /*higher part*/
- /* Field(accu, 1) = (value)(I64_to_int32(p)|1); */ /*lower part*/
- value x = accu;
+ Uint63_mulc(accu, *sp, sp);
+ *--sp = accu;
AllocPair();
- Field(accu, 1) = uint63_mulc(x, *sp++, &Field(accu, 0));
+ Field(accu, 1) = *sp++;
+ Field(accu, 0) = *sp++;
Next;
}
@@ -1306,13 +1318,13 @@ value coq_interprete
/* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag
since it probably only concerns negative number.
needs to be checked at this point */
- value divisor;
- divisor = *sp++;
- if (uint63_eq0(divisor)) {
- accu = divisor;
+ int b;
+ Uint63_eq0(b, *sp);
+ if (b) {
+ accu = *sp++;
}
else {
- accu = uint63_div(accu, divisor);
+ Uint63_div(accu, *sp++);
}
Next;
}
@@ -1320,13 +1332,13 @@ value coq_interprete
Instruct(CHECKMODINT63) {
print_instr("CHEKMODINT63");
CheckInt2();
- value divisor;
- divisor = *sp++;
- if (uint63_eq0(divisor)) {
- accu = divisor;
+ int b;
+ Uint63_eq0(b, *sp);
+ if (b) {
+ accu = *sp++;
}
else {
- accu = uint63_mod(accu,divisor);
+ Uint63_mod(accu,*sp++);
}
Next;
}
@@ -1337,19 +1349,24 @@ value coq_interprete
/* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag
since it probably only concerns negative number.
needs to be checked at this point */
- value divisor;
- divisor = *sp++;
- if (uint63_eq0(divisor)) {
- Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
- Field(accu, 0) = divisor;
- Field(accu, 1) = divisor;
+ int b;
+ Uint63_eq0(b, *sp);
+ if (b) {
+ AllocPair();
+ Field(accu, 0) = *sp;
+ Field(accu, 1) = *sp++;
}
else {
- value modulus;
- modulus = accu;
- Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
- Field(accu, 0) = uint63_div(modulus,divisor);
- Field(accu, 1) = uint63_mod(modulus,divisor);
+ *--sp = accu;
+ Uint63_div(sp[0],sp[1]);
+ Swap_accu_sp;
+ Uint63_mod(accu,sp[1]);
+ sp[1] = sp[0];
+ Swap_accu_sp;
+ AllocPair();
+ Field(accu, 0) = sp[1];
+ Field(accu, 1) = sp[0];
+ sp += 2;
}
Next;
}
@@ -1357,78 +1374,47 @@ value coq_interprete
Instruct (CHECKDIV21INT63) {
print_instr("DIV21INT63");
CheckInt3();
- /* spiwack: takes three int31 (the two first ones represent an
- int62) and performs the euclidian division of the
- int62 by the int31 */
- /* TODO: implement this
- bigint = UI64_of_value(accu);
- bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++));
- uint64 divisor;
- divisor = UI64_of_value(*sp++);
- Alloc_small(accu, 2, 1); */ /* ( _ , arity, tag ) */
- /* if (I64_is_zero (divisor)) {
- Field(accu, 0) = 1; */ /* 2*0+1 */
- /* Field(accu, 1) = 1; */ /* 2*0+1 */
- /* }
- else {
- uint64 quo, mod;
- I64_udivmod(bigint, divisor, &quo, &mod);
- Field(accu, 0) = value_of_uint32(I64_to_int32(quo));
- Field(accu, 1) = value_of_uint32(I64_to_int32(mod));
- } */
- value bigint; /* TODO: fix */
- bigint = *sp++; /* TODO: take accu into account */
- value divisor;
- divisor = *sp++;
- if (uint63_eq0(divisor)) {
- Alloc_small(accu, 2, 1);
- Field(accu, 0) = divisor;
- Field(accu, 1) = divisor;
- }
- else {
- value quo, mod;
- mod = uint63_div21(accu, bigint, divisor, &quo);
- Alloc_small(accu, 2, 1);
- Field(accu, 0) = quo;
- Field(accu, 1) = mod;
- }
+ Uint63_div21(accu, sp[0], sp[1], &(sp[1]));
+ Swap_accu_sp;
+ AllocPair();
+ Field(accu, 0) = sp[1];
+ Field(accu, 1) = sp[0];
+ sp += 2;
Next;
}
Instruct(CHECKLXORINT63) {
print_instr("CHECKLXORINT63");
CheckInt2();
- accu = uint63_lxor(accu,*sp++);
+ Uint63_lxor(accu,*sp++);
Next;
}
Instruct(CHECKLORINT63) {
print_instr("CHECKLORINT63");
CheckInt2();
- accu = uint63_lor(accu,*sp++);
+ Uint63_lor(accu,*sp++);
Next;
}
Instruct(CHECKLANDINT63) {
print_instr("CHECKLANDINT63");
CheckInt2();
- accu = uint63_land(accu,*sp++);
+ Uint63_land(accu,*sp++);
Next;
}
Instruct(CHECKLSLINT63) {
print_instr("CHECKLSLINT63");
CheckInt2();
- value p = *sp++;
- accu = uint63_lsl(accu,p);
+ Uint63_lsl(accu,*sp++);
Next;
}
Instruct(CHECKLSRINT63) {
print_instr("CHECKLSRINT63");
CheckInt2();
- value p = *sp++;
- accu = uint63_lsr(accu,p);
+ Uint63_lsr(accu,*sp++);
Next;
}
@@ -1436,7 +1422,7 @@ value coq_interprete
print_instr("CHECKLSLINT63CONST1");
if (Is_uint63(accu)) {
pc++;
- accu = uint63_lsl1(accu);
+ Uint63_lsl1(accu);
Next;
} else {
*--sp = uint63_one();
@@ -1450,7 +1436,7 @@ value coq_interprete
print_instr("CHECKLSRINT63CONST1");
if (Is_uint63(accu)) {
pc++;
- accu = uint63_lsr1(accu);
+ Uint63_lsr1(accu);
Next;
} else {
*--sp = uint63_one();
@@ -1463,18 +1449,17 @@ value coq_interprete
Instruct (CHECKADDMULDIVINT63) {
print_instr("CHECKADDMULDIVINT63");
CheckInt3();
- value x;
- value y;
- x = *sp++;
- y = *sp++;
- accu = uint63_addmuldiv(accu,x,y);
+ Uint63_addmuldiv(accu,sp[0],sp[1]);
+ sp += 2;
Next;
}
Instruct (CHECKEQINT63) {
print_instr("CHECKEQINT63");
CheckInt2();
- accu = uint63_eq(accu,*sp++) ? coq_true : coq_false;
+ int b;
+ Uint63_eq(b, accu, *sp++);
+ accu = b ? coq_true : coq_false;
Next;
}
@@ -1484,7 +1469,9 @@ value coq_interprete
}
Instruct (LTINT63) {
print_instr("LTINT63");
- accu = uint63_lt(accu,*sp++) ? coq_true : coq_false;
+ int b;
+ Uint63_lt(b,accu,*sp++);
+ accu = b ? coq_true : coq_false;
Next;
}
@@ -1494,7 +1481,9 @@ value coq_interprete
}
Instruct (LEINT63) {
print_instr("LEINT63");
- accu = uint63_leq(accu,*sp++) ? coq_true : coq_false;
+ int b;
+ Uint63_leq(b,accu,*sp++);
+ accu = b ? coq_true : coq_false;
Next;
}
@@ -1503,25 +1492,30 @@ value coq_interprete
/* assumes Inductive _ : _ := Eq | Lt | Gt */
print_instr("CHECKCOMPAREINT63");
CheckInt2();
- if (uint63_eq(accu,*sp)) {
+ int b;
+ Uint63_eq(b, accu, *sp);
+ if (b) {
accu = coq_Eq;
sp++;
}
- else accu = uint63_lt(accu,*sp++) ? coq_Lt : coq_Gt;
+ else {
+ Uint63_lt(b, accu, *sp++);
+ accu = b ? coq_Lt : coq_Gt;
+ }
Next;
}
Instruct (CHECKHEAD0INT63) {
print_instr("CHECKHEAD0INT63");
CheckInt1();
- accu = uint63_head0(accu);
+ Uint63_head0(accu);
Next;
}
Instruct (CHECKTAIL0INT63) {
print_instr("CHECKTAIL0INT63");
CheckInt1();
- accu = uint63_tail0(accu);
+ Uint63_tail0(accu);
Next;
}
@@ -1593,7 +1587,7 @@ value coq_push_vstack(value stk, value max_stack_size) {
print_instr("push_vstack");print_int(len);
for(i = 0; i < len; i++) coq_sp[i] = Field(stk,i);
sp = coq_sp;
- CHECK_STACK(uint32_of_value(max_stack_size));
+ CHECK_STACK(uint_of_value(max_stack_size));
return Val_unit;
}
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index 9375b15de2..1ea461c5e5 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -19,7 +19,7 @@
#define Coq_stack_size (4096 * sizeof(value))
-#define Coq_stack_threshold (256 * sizeof(value))
+#define Coq_stack_threshold (256 * sizeof(value)) /* see kernel/cbytegen.ml */
#define Coq_max_stack_size (256 * 1024)
#define TRANSP 0
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index 5499f124a2..528cc6fc1f 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -6,6 +6,8 @@
#define Is_uint63(v) (Tag_val(v) == Custom_tag)
+#define uint_of_value(val) (((uint32_t)(val)) >> 1)
+
# define DECLARE_NULLOP(name) \
value uint63_##name() { \
static value* cb = 0; \
@@ -15,83 +17,142 @@ value uint63_##name() { \
}
# define DECLARE_UNOP(name) \
-value uint63_##name(value x) { \
+value uint63_##name##_ml(value x) { \
static value* cb = 0; \
CAMLparam1(x); \
if (!cb) cb = caml_named_value("uint63 " #name); \
CAMLreturn(caml_callback(*cb, x)); \
}
-# define DECLARE_PREDICATE(name) \
-value uint63_##name(value x) { \
- static value* cb = 0; \
- CAMLparam1(x); \
- if (!cb) cb = caml_named_value("uint63 " #name); \
- CAMLreturn(Int_val(caml_callback(*cb, x))); \
- }
+# define CALL_UNOP_NOASSIGN(name, x) \
+ value uint63_return_value__; \
+ value uint63_arg_x__ = (x); \
+ Setup_for_gc; \
+ uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__); \
+ Restore_after_gc
+
+# define CALL_UNOP(name, x) do{ \
+ CALL_UNOP_NOASSIGN(name, x); \
+ accu = uint63_return_value__; \
+ }while(0)
+
+# define CALL_PREDICATE(r, name, x) do{ \
+ CALL_UNOP_NOASSIGN(name, x); \
+ (r) = Int_val(uint63_return_value__); \
+ }while(0)
# define DECLARE_BINOP(name) \
-value uint63_##name(value x, value y) { \
+value uint63_##name##_ml(value x, value y) { \
static value* cb = 0; \
CAMLparam2(x, y); \
if (!cb) cb = caml_named_value("uint63 " #name); \
CAMLreturn(caml_callback2(*cb, x, y)); \
}
-# define DECLARE_RELATION(name) \
-value uint63_##name(value x, value y) { \
- static value* cb = 0; \
- CAMLparam2(x, y); \
- if (!cb) cb = caml_named_value("uint63 " #name); \
- CAMLreturn(Int_val(caml_callback2(*cb, x, y))); \
- }
+# define CALL_BINOP_NOASSIGN(name, x, y) \
+ value uint63_return_value__; \
+ value uint63_arg_x__ = (x); \
+ value uint63_arg_y__ = (y); \
+ Setup_for_gc; \
+ uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__, uint63_arg_y__); \
+ Restore_after_gc
+
+# define CALL_BINOP(name, x, y) do{ \
+ CALL_BINOP_NOASSIGN(name, x, y); \
+ accu = uint63_return_value__; \
+ }while(0)
+
+# define CALL_RELATION(r, name, x, y) do{ \
+ CALL_BINOP_NOASSIGN(name, x, y); \
+ (r) = Int_val(uint63_return_value__); \
+ }while(0)
# define DECLARE_TEROP(name) \
-value uint63_##name(value x, value y, value z) { \
+value uint63_##name##_ml(value x, value y, value z) { \
static value* cb = 0; \
CAMLparam3(x, y, z); \
if (!cb) cb = caml_named_value("uint63 " #name); \
CAMLreturn(caml_callback3(*cb, x, y, z)); \
}
+# define CALL_TEROP(name, x, y, z) do{ \
+ value uint63_return_value__; \
+ value uint63_arg_x__ = (x); \
+ value uint63_arg_y__ = (y); \
+ value uint63_arg_z__ = (z); \
+ Setup_for_gc; \
+ uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__, uint63_arg_y__, uint63_arg_z__); \
+ Restore_after_gc; \
+ accu = uint63_return_value__; \
+ }while(0)
DECLARE_NULLOP(one)
DECLARE_BINOP(add)
+#define Uint63_add(x, y) CALL_BINOP(add, x, y)
DECLARE_BINOP(addcarry)
+#define Uint63_addcarry(x, y) CALL_BINOP(addcarry, x, y)
DECLARE_TEROP(addmuldiv)
+#define Uint63_addmuldiv(x, y, z) CALL_TEROP(addmuldiv, x, y, z)
DECLARE_BINOP(div)
-DECLARE_TEROP(div21_ml)
-DECLARE_RELATION(eq)
-DECLARE_PREDICATE(eq0)
+#define Uint63_div(x, y) CALL_BINOP(div, x, y)
+DECLARE_BINOP(eq)
+#define Uint63_eq(r, x, y) CALL_RELATION(r, eq, x, y)
+DECLARE_UNOP(eq0)
+#define Uint63_eq0(r, x) CALL_PREDICATE(r, eq0, x)
DECLARE_UNOP(head0)
+#define Uint63_head0(x) CALL_UNOP(head0, x)
DECLARE_BINOP(land)
-DECLARE_RELATION(leq)
+#define Uint63_land(x, y) CALL_BINOP(land, x, y)
+DECLARE_BINOP(leq)
+#define Uint63_leq(r, x, y) CALL_RELATION(r, leq, x, y)
DECLARE_BINOP(lor)
+#define Uint63_lor(x, y) CALL_BINOP(lor, x, y)
DECLARE_BINOP(lsl)
+#define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y)
DECLARE_UNOP(lsl1)
+#define Uint63_lsl1(x) CALL_UNOP(lsl1, x)
DECLARE_BINOP(lsr)
+#define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y)
DECLARE_UNOP(lsr1)
-DECLARE_RELATION(lt)
+#define Uint63_lsr1(x) CALL_UNOP(lsr1, x)
+DECLARE_BINOP(lt)
+#define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y)
DECLARE_BINOP(lxor)
+#define Uint63_lxor(x, y) CALL_BINOP(lxor, x, y)
DECLARE_BINOP(mod)
+#define Uint63_mod(x, y) CALL_BINOP(mod, x, y)
DECLARE_BINOP(mul)
-DECLARE_BINOP(mulc_ml)
+#define Uint63_mul(x, y) CALL_BINOP(mul, x, y)
DECLARE_BINOP(sub)
+#define Uint63_sub(x, y) CALL_BINOP(sub, x, y)
DECLARE_BINOP(subcarry)
+#define Uint63_subcarry(x, y) CALL_BINOP(subcarry, x, y)
DECLARE_UNOP(tail0)
+#define Uint63_tail0(x) CALL_UNOP(tail0, x)
+
+DECLARE_TEROP(div21_ml)
+# define Uint63_div21(x, y, z, q) do{ \
+ value uint63_return_value__; \
+ value uint63_arg_x__ = (x); \
+ value uint63_arg_y__ = (y); \
+ value uint63_arg_z__ = (z); \
+ Setup_for_gc; \
+ uint63_return_value__ = \
+ uint63_div21_ml_ml(uint63_arg_x__, uint63_arg_y__, uint63_arg_z__); \
+ Restore_after_gc; \
+ *q = Field(uint63_return_value__, 0); \
+ accu = Field(uint63_return_value__, 1); \
+ }while(0)
-value uint63_div21(value x, value y, value z, value* q) {
- CAMLparam3(x, y, z);
- CAMLlocal1(qr);
- qr = uint63_div21_ml(x, y, z);
- *q = Field(qr, 0);
- CAMLreturn(Field(qr, 1));
-}
-
-value uint63_mulc(value x, value y, value* h) {
- CAMLparam2(x, y);
- CAMLlocal1(hl);
- hl = uint63_mulc_ml(x, y);
- *h = Field(hl, 0);
- CAMLreturn(Field(hl, 1));
-}
+DECLARE_BINOP(mulc_ml)
+# define Uint63_mulc(x, y, h) do{ \
+ value uint63_return_value__; \
+ value uint63_arg_x__ = (x); \
+ value uint63_arg_y__ = (y); \
+ Setup_for_gc; \
+ uint63_return_value__ = \
+ uint63_mulc_ml_ml(uint63_arg_x__, uint63_arg_y__); \
+ Restore_after_gc; \
+ *(h) = Field(uint63_return_value__, 0); \
+ accu = Field(uint63_return_value__, 1); \
+ }while(0)
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 92f4dc79bc..1fdafc9d8f 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -1,5 +1,6 @@
#define Is_uint63(v) (Is_long(v))
+#define uint_of_value(val) (((uint64_t)(val)) >> 1)
#define uint63_of_value(val) ((uint64_t)(val) >> 1)
/* 2^63 * y + x as a value */
@@ -9,28 +10,43 @@
#define uint63_one() ((value) 3) /* 2*1 + 1 */
#define uint63_eq(x,y) ((x) == (y))
-#define uint63_eq0(x) ((x) == (uint64_t)1)
+#define Uint63_eq(r,x,y) ((r) = uint63_eq(x,y))
+#define Uint63_eq0(r,x) ((r) = ((x) == (uint64_t)1))
#define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y))
+#define Uint63_lt(r,x,y) ((r) = uint63_lt(x,y))
#define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y))
+#define Uint63_leq(r,x,y) ((r) = uint63_leq(x,y))
-#define uint63_add(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) - 1))
-#define uint63_addcarry(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) + 1))
-#define uint63_sub(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) + 1))
-#define uint63_subcarry(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) - 1))
-#define uint63_mul(x,y) (Val_long(uint63_of_value(x) * uint63_of_value(y)))
-#define uint63_div(x,y) (Val_long(uint63_of_value(x) / uint63_of_value(y)))
-#define uint63_mod(x,y) (Val_long(uint63_of_value(x) % uint63_of_value(y)))
+#define Uint63_add(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) - 1))
+#define Uint63_addcarry(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) + 1))
+#define Uint63_sub(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) + 1))
+#define Uint63_subcarry(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) - 1))
+#define Uint63_mul(x,y) (accu = Val_long(uint63_of_value(x) * uint63_of_value(y)))
+#define Uint63_div(x,y) (accu = Val_long(uint63_of_value(x) / uint63_of_value(y)))
+#define Uint63_mod(x,y) (accu = Val_long(uint63_of_value(x) % uint63_of_value(y)))
-#define uint63_lxor(x,y) ((value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1))
-#define uint63_lor(x,y) ((value)((uint64_t)(x) | (uint64_t)(y)))
-#define uint63_land(x,y) ((value)((uint64_t)(x) & (uint64_t)(y)))
+#define Uint63_lxor(x,y) (accu = (value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1))
+#define Uint63_lor(x,y) (accu = (value)((uint64_t)(x) | (uint64_t)(y)))
+#define Uint63_land(x,y) (accu = (value)((uint64_t)(x) & (uint64_t)(y)))
/* TODO: is + or | better? OCAML uses + */
/* TODO: is - or ^ better? */
-#define uint63_lsl(x,y) ((y) < (uint64_t) 127 ? ((value)((((uint64_t)(x)-1) << (uint63_of_value(y))) | 1)) : uint63_zero)
-#define uint63_lsr(x,y) ((y) < (uint64_t) 127 ? ((value)(((uint64_t)(x) >> (uint63_of_value(y))) | 1)) : uint63_zero)
-#define uint63_lsl1(x) ((value)((((uint64_t)(x)-1) << 1) +1))
-#define uint63_lsr1(x) ((value)(((uint64_t)(x) >> 1) |1))
+#define Uint63_lsl(x,y) do{ \
+ value uint63_lsl_y__ = (y); \
+ if (uint63_lsl_y__ < (uint64_t) 127) \
+ accu = (value)((((uint64_t)(x)-1) << uint63_of_value(uint63_lsl_y__)) | 1); \
+ else \
+ accu = uint63_zero; \
+ }while(0)
+#define Uint63_lsr(x,y) do{ \
+ value uint63_lsl_y__ = (y); \
+ if (uint63_lsl_y__ < (uint64_t) 127) \
+ accu = (value)(((uint64_t)(x) >> uint63_of_value(uint63_lsl_y__)) | 1); \
+ else \
+ accu = uint63_zero; \
+ }while(0)
+#define Uint63_lsl1(x) (accu = (value)((((uint64_t)(x)-1) << 1) +1))
+#define Uint63_lsr1(x) (accu = (value)(((uint64_t)(x) >> 1) |1))
/* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */
/* (modulo 2^63) for p <= 63 */
@@ -40,6 +56,7 @@ value uint63_addmuldiv(uint64_t p, uint64_t x, uint64_t y) {
r |= ((uint64_t)y >> (63-shiftby)) | 1;
return r;
}
+#define Uint63_addmuldiv(p, x, y) (accu = uint63_addmuldiv(p, x, y))
value uint63_head0(uint64_t x) {
int r = 0;
@@ -51,6 +68,7 @@ value uint63_head0(uint64_t x) {
if (!(x & 0x8000000000000000)) { x <<=1; r += 1; }
return Val_int(r);
}
+#define Uint63_head0(x) (accu = uint63_head0(x))
value uint63_tail0(value x) {
int r = 0;
@@ -63,6 +81,7 @@ value uint63_tail0(value x) {
if (!(x & 0x00000001)) { x >>=1; r += 1; }
return Val_int(r);
}
+#define Uint63_tail0(x) (accu = uint63_tail0(x))
value uint63_mulc(value x, value y, value* h) {
x = (uint64_t)x >> 1;
@@ -86,40 +105,61 @@ value uint63_mulc(value x, value y, value* h) {
*h = Val_int(hr);
return Val_int(lr);
}
+#define Uint63_mulc(x, y, h) (accu = uint63_mulc(x, y, h))
#define lt128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_lt(xl,yl)))
#define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl)))
-value uint63_div21(value xh, value xl, value y, value* q) {
- xh = (uint64_t)xh >> 1;
- xl = ((uint64_t)xl >> 1) | ((uint64_t)xh << 63);
- xh = (uint64_t)xh >> 1;
+#define maxuint63 ((uint64_t)0x7FFFFFFFFFFFFFFF)
+/* precondition: y <> 0 */
+/* outputs r and sets ql to q % 2^63 s.t. x = q * y + r, r < y */
+static value uint63_div21_aux(value xh, value xl, value y, value* ql) {
+ xh = uint63_of_value(xh);
+ xl = uint63_of_value(xl);
+ y = uint63_of_value(y);
uint64_t maskh = 0;
uint64_t maskl = 1;
uint64_t dh = 0;
- uint64_t dl = (uint64_t)y >> 1;
+ uint64_t dl = y;
int cmp = 1;
- while (dh >= 0 && cmp) {
+ /* int n = 0 */
+ /* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0, d < 2^(2*63) */
+ while (!(dh >> (63 - 1)) && cmp) {
+ dh = (dh << 1) | (dl >> (63 - 1));
+ dl = (dl << 1) & maxuint63;
+ maskh = (maskh << 1) | (maskl >> (63 - 1));
+ maskl = (maskl << 1) & maxuint63;
+ /* ++n */
cmp = lt128(dh,dl,xh,xl);
- dh = (dh << 1) | (dl >> 63);
- dl = dl << 1;
- maskh = (maskh << 1) | (maskl >> 63);
- maskl = maskl << 1;
}
uint64_t remh = xh;
uint64_t reml = xl;
- uint64_t quotient = 0;
+ /* uint64_t quotienth = 0; */
+ uint64_t quotientl = 0;
+ /* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r,
+ mask = floor(2^n), d = mask * y, n >= -1 */
while (maskh | maskl) {
- if (le128(dh,dl,remh,reml)) {
- quotient = quotient | maskl;
- if (uint63_lt(reml,dl)) {remh = remh - dh - 1;} else {remh = remh - dh;}
+ if (le128(dh,dl,remh,reml)) { /* if rem >= d, add one bit and subtract d */
+ /* quotienth = quotienth | maskh */
+ quotientl = quotientl | maskl;
+ remh = (uint63_lt(reml,dl)) ? (remh - dh - 1) : (remh - dh);
reml = reml - dl;
}
- maskl = (maskl >> 1) | (maskh << 63);
+ maskl = (maskl >> 1) | ((maskh << (63 - 1)) & maxuint63);
maskh = maskh >> 1;
- dl = (dl >> 1) | (dh << 63);
+ dl = (dl >> 1) | ((dh << (63 - 1)) & maxuint63);
dh = dh >> 1;
+ /* decr n */
}
- *q = Val_int(quotient);
+ *ql = Val_int(quotientl);
return Val_int(reml);
}
+value uint63_div21(value xh, value xl, value y, value* ql) {
+ if (uint63_of_value(y) == 0) {
+ *ql = Val_int(0);
+ return Val_int(0);
+ } else {
+ return uint63_div21_aux(xh, xl, y, ql);
+ }
+}
+#define Uint63_div21(xh, xl, y, q) (accu = uint63_div21(xh, xl, y, q))
diff --git a/kernel/entries.ml b/kernel/entries.ml
index a3d32267a7..adb3f6bd29 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -108,21 +108,7 @@ type module_entry =
| MExpr of
module_params_entry * module_struct_entry * module_struct_entry option
-
-type seff_env =
- [ `Nothing
- (* The proof term and its universes.
- Same as the constant_body's but not in an ephemeron *)
- | `Opaque of Constr.t * Univ.ContextSet.t ]
-
(** Not used by the kernel. *)
type side_effect_role =
| Subproof
| Schema of inductive * string
-
-type side_eff = {
- seff_constant : Constant.t;
- seff_body : Declarations.constant_body;
- seff_env : seff_env;
- seff_role : side_effect_role;
-}
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 009eb3da38..bb3b0a538e 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -49,20 +49,6 @@ let weaker_noccur_between env x nvars t =
(************************************************************************)
(* Various well-formedness check for inductive declarations *)
-(* Errors related to inductive constructions *)
-type inductive_error = Type_errors.inductive_error =
- | NonPos of env * constr * constr
- | NotEnoughArgs of env * constr * constr
- | NotConstructor of env * Id.t * constr * constr * int * int
- | NonPar of env * constr * int * constr * constr
- | SameNamesTypes of Id.t
- | SameNamesConstructors of Id.t
- | SameNamesOverlap of Id.t list
- | NotAnArity of env * constr
- | BadEntry
- | LargeNonPropInductiveNotInType
- | BadUnivs
-
exception InductiveError = Type_errors.InductiveError
(************************************************************************)
@@ -84,6 +70,7 @@ exception IllFormedInd of ill_formed_ind
let mind_extract_params = decompose_prod_n_assum
let explain_ind_err id ntyp env nparamsctxt c err =
+ let open Type_errors in
let (_lparams,c') = mind_extract_params nparamsctxt c in
match err with
| LocalNonPos kt ->
@@ -329,7 +316,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (
| Prod (na,b,d) ->
let () = assert (List.is_empty largs) in
if not recursive && not (noccur_between n ntypes b) then
- raise (InductiveError BadEntry);
+ raise (InductiveError Type_errors.BadEntry);
let nmr',recarg = check_pos ienv nmr b in
let ienv' = ienv_push_var ienv (na,b,mk_norec) in
check_constr_rec ienv' nmr' (recarg::lrec) d
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7810c1723e..1b8e4208ff 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -9,28 +9,9 @@
(************************************************************************)
open Names
-open Constr
open Declarations
open Environ
open Entries
(** Check an inductive. *)
val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
-
-(** Deprecated *)
-type inductive_error =
- | NonPos of env * constr * constr
- | NotEnoughArgs of env * constr * constr
- | NotConstructor of env * Id.t * constr * constr * int * int
- | NonPar of env * constr * int * constr * constr
- | SameNamesTypes of Id.t
- | SameNamesConstructors of Id.t
- | SameNamesOverlap of Id.t list
- | NotAnArity of env * constr
- | BadEntry
- | LargeNonPropInductiveNotInType
- | BadUnivs
-[@@ocaml.deprecated "Use [Type_errors.inductive_error]"]
-
-exception InductiveError of Type_errors.inductive_error
-[@@ocaml.deprecated "Use [Type_errors.InductiveError]"]
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 4f992d3972..4fdd7ab334 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -608,11 +608,7 @@ let clean_bounded_mod_expr sign =
(** {6 Stm machinery } *)
let join_constant_body except otab cb =
match cb.const_body with
- | OpaqueDef o ->
- (match Opaqueproof.uuid_opaque otab o with
- | Some uuid when not(Future.UUIDSet.mem uuid except) ->
- Opaqueproof.join_opaque otab o
- | _ -> ())
+ | OpaqueDef o -> Opaqueproof.join_opaque ~except otab o
| _ -> ()
let join_structure except otab s =
diff --git a/kernel/names.ml b/kernel/names.ml
index 9f27212967..047a1d6525 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -376,9 +376,6 @@ module KerName = struct
{ modpath; knlabel; refhash = -1; }
let repr kn = (kn.modpath, kn.knlabel)
- let make2 = make
- [@@ocaml.deprecated "Please use [KerName.make]"]
-
let modpath kn = kn.modpath
let label kn = kn.knlabel
diff --git a/kernel/names.mli b/kernel/names.mli
index 61df3bad0e..2238e932b0 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -278,9 +278,6 @@ sig
val make : ModPath.t -> Label.t -> t
val repr : t -> ModPath.t * Label.t
- val make2 : ModPath.t -> Label.t -> t
- [@@ocaml.deprecated "Please use [KerName.make]"]
-
(** Projections *)
val modpath : t -> ModPath.t
val label : t -> Label.t
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 2dab14e732..3f791dfc22 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -51,7 +51,6 @@ let fresh_lname n =
(** Global names **)
type gname =
| Gind of string * inductive (* prefix, inductive name *)
- | Gconstruct of string * constructor (* prefix, constructor name *)
| Gconstant of string * Constant.t (* prefix, constant name *)
| Gproj of string * inductive * int (* prefix, inductive, index (start from 0) *)
| Gcase of Label.t option * int
@@ -67,8 +66,6 @@ let eq_gname gn1 gn2 =
match gn1, gn2 with
| Gind (s1, ind1), Gind (s2, ind2) ->
String.equal s1 s2 && eq_ind ind1 ind2
- | Gconstruct (s1, c1), Gconstruct (s2, c2) ->
- String.equal s1 s2 && eq_constructor c1 c2
| Gconstant (s1, c1), Gconstant (s2, c2) ->
String.equal s1 s2 && Constant.equal c1 c2
| Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) ->
@@ -88,7 +85,7 @@ let eq_gname gn1 gn2 =
| Ginternal s1, Ginternal s2 -> String.equal s1 s2
| Grel i1, Grel i2 -> Int.equal i1 i2
| Gnamed id1, Gnamed id2 -> Id.equal id1 id2
- | (Gind _| Gconstruct _ | Gconstant _ | Gproj _ | Gcase _ | Gpred _
+ | (Gind _| Gconstant _ | Gproj _ | Gcase _ | Gpred _
| Gfixtype _ | Gnorm _ | Gnormtbl _ | Ginternal _ | Grel _ | Gnamed _), _ ->
false
@@ -100,19 +97,17 @@ open Hashset.Combine
let gname_hash gn = match gn with
| Gind (s, ind) ->
combinesmall 1 (combine (String.hash s) (ind_hash ind))
-| Gconstruct (s, c) ->
- combinesmall 2 (combine (String.hash s) (constructor_hash c))
| Gconstant (s, c) ->
- combinesmall 3 (combine (String.hash s) (Constant.hash c))
-| Gcase (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gpred (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gfixtype (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gnorm (l, i) -> combinesmall 7 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gnormtbl (l, i) -> combinesmall 8 (combine (Option.hash Label.hash l) (Int.hash i))
-| Ginternal s -> combinesmall 9 (String.hash s)
-| Grel i -> combinesmall 10 (Int.hash i)
-| Gnamed id -> combinesmall 11 (Id.hash id)
-| Gproj (s, p, i) -> combinesmall 12 (combine (String.hash s) (combine (ind_hash p) i))
+ combinesmall 2 (combine (String.hash s) (Constant.hash c))
+| Gcase (l, i) -> combinesmall 3 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gpred (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gfixtype (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gnorm (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gnormtbl (l, i) -> combinesmall 7 (combine (Option.hash Label.hash l) (Int.hash i))
+| Ginternal s -> combinesmall 8 (String.hash s)
+| Grel i -> combinesmall 9 (Int.hash i)
+| Gnamed id -> combinesmall 10 (Id.hash id)
+| Gproj (s, p, i) -> combinesmall 11 (combine (String.hash s) (combine (ind_hash p) i))
let case_ctr = ref (-1)
@@ -382,8 +377,8 @@ type mllambda =
| MLif of mllambda * mllambda * mllambda
| MLmatch of annot_sw * mllambda * mllambda * mllam_branches
(* argument, prefix, accu branch, branches *)
- | MLconstruct of string * constructor * mllambda array
- (* prefix, constructor name, arguments *)
+ | MLconstruct of string * inductive * int * mllambda array
+ (* prefix, inductive name, tag, arguments *)
| MLint of int
| MLuint of Uint63.t
| MLsetref of string * mllambda
@@ -391,7 +386,11 @@ type mllambda =
| MLarray of mllambda array
| MLisaccu of string * inductive * mllambda
-and mllam_branches = ((constructor * lname option array) list * mllambda) array
+and 'a mllam_pattern =
+ | ConstPattern of int
+ | NonConstPattern of tag * 'a array
+
+and mllam_branches = (lname option mllam_pattern list * mllambda) array
let push_lnames n env lns =
snd (Array.fold_left (fun (i,r) x -> (i+1, LNmap.add x i r)) (n,env) lns)
@@ -444,9 +443,10 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
eq_mllambda gn1 gn2 n env1 env2 c1 c2 &&
eq_mllambda gn1 gn2 n env1 env2 accu1 accu2 &&
eq_mllam_branches gn1 gn2 n env1 env2 br1 br2
- | MLconstruct (pf1, cs1, args1), MLconstruct (pf2, cs2, args2) ->
+ | MLconstruct (pf1, ind1, tag1, args1), MLconstruct (pf2, ind2, tag2, args2) ->
String.equal pf1 pf2 &&
- eq_constructor cs1 cs2 &&
+ eq_ind ind1 ind2 &&
+ Int.equal tag1 tag2 &&
Array.equal (eq_mllambda gn1 gn2 n env1 env2) args1 args2
| MLint i1, MLint i2 ->
Int.equal i1 i2
@@ -479,15 +479,22 @@ and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 =
(* we require here that patterns have the same order, which may be too strong *)
and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 =
- let eq_cargs (cs1, args1) (cs2, args2) body1 body2 =
+ let eq_cargs args1 args2 body1 body2 =
Int.equal (Array.length args1) (Array.length args2) &&
- eq_constructor cs1 cs2 &&
let env1 = opush_lnames n env1 args1 in
let env2 = opush_lnames n env2 args2 in
eq_mllambda gn1 gn2 (n + Array.length args1) env1 env2 body1 body2
in
- let eq_branch (ptl1,body1) (ptl2,body2) =
- List.equal (fun pt1 pt2 -> eq_cargs pt1 pt2 body1 body2) ptl1 ptl2
+ let eq_pattern pat1 pat2 body1 body2 =
+ match pat1, pat2 with
+ | ConstPattern tag1, ConstPattern tag2 ->
+ Int.equal tag1 tag2 && eq_mllambda gn1 gn2 n env1 env2 body1 body2
+ | NonConstPattern (tag1,args1), NonConstPattern (tag2,args2) ->
+ Int.equal tag1 tag2 && eq_cargs args1 args2 body1 body2
+ | (ConstPattern _ | NonConstPattern _), _ -> false
+ in
+ let eq_branch (patl1,body1) (patl2,body2) =
+ List.equal (fun pt1 pt2 -> eq_pattern pt1 pt2 body1 body2) patl1 patl2
in
Array.equal eq_branch br1 br2
@@ -523,10 +530,11 @@ let rec hash_mllambda gn n env t =
let hc = hash_mllambda gn n env c in
let haccu = hash_mllambda gn n env accu in
combinesmall 9 (hash_mllam_branches gn n env (combine3 hannot hc haccu) br)
- | MLconstruct (pf, cs, args) ->
+ | MLconstruct (pf, ind, tag, args) ->
let hpf = String.hash pf in
- let hcs = constructor_hash cs in
- combinesmall 10 (hash_mllambda_array gn n env (combine hpf hcs) args)
+ let hcs = ind_hash ind in
+ let htag = Int.hash tag in
+ combinesmall 10 (hash_mllambda_array gn n env (combine3 hpf hcs htag) args)
| MLint i ->
combinesmall 11 i
| MLuint i ->
@@ -556,15 +564,18 @@ and hash_mllambda_array gn n env init arr =
Array.fold_left (fun acc t -> combine (hash_mllambda gn n env t) acc) init arr
and hash_mllam_branches gn n env init br =
- let hash_cargs (cs, args) body =
+ let hash_cargs args body =
let nargs = Array.length args in
- let hcs = constructor_hash cs in
let env = opush_lnames n env args in
let hbody = hash_mllambda gn (n + nargs) env body in
- combine3 nargs hcs hbody
+ combine nargs hbody
+ in
+ let hash_pattern pat body = match pat with
+ | ConstPattern i -> combinesmall 1 (Int.hash i)
+ | NonConstPattern (tag,args) -> combinesmall 2 (combine (Int.hash tag) (hash_cargs args body))
in
let hash_branch acc (ptl,body) =
- List.fold_left (fun acc t -> combine (hash_cargs t body) acc) acc ptl
+ List.fold_left (fun acc t -> combine (hash_pattern t body) acc) acc ptl
in
Array.fold_left hash_branch init br
@@ -594,17 +605,20 @@ let fv_lam l =
| MLmatch(_,a,p,bs) ->
let fv = aux a bind (aux p bind fv) in
let fv_bs (cargs, body) fv =
- let bind =
- List.fold_right (fun (_,args) bind ->
- Array.fold_right
- (fun o bind -> match o with
- | Some l -> LNset.add l bind
- | _ -> bind) args bind)
- cargs bind in
- aux body bind fv in
+ let bind =
+ List.fold_right (fun pat bind ->
+ match pat with
+ | ConstPattern _ -> bind
+ | NonConstPattern(_,args) ->
+ Array.fold_right
+ (fun o bind -> match o with
+ | Some l -> LNset.add l bind
+ | _ -> bind) args bind)
+ cargs bind in
+ aux body bind fv in
Array.fold_right fv_bs bs fv
- (* argument, accu branch, branches *)
- | MLconstruct (_,_,p) ->
+ (* argument, accu branch, branches *)
+ | MLconstruct (_,_,_,p) ->
Array.fold_right (fun a fv -> aux a bind fv) p fv
| MLsetref(_,l) -> aux l bind fv
| MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv)
@@ -652,8 +666,8 @@ type global =
| Gletcase of
gname * lname array * annot_sw * mllambda * mllambda * mllam_branches
| Gopen of string
- | Gtype of inductive * int array
- (* ind name, arities of constructors *)
+ | Gtype of inductive * (tag * int) array
+ (* ind name, tag and arities of constructors *)
| Gcomment of string
(* Alpha-equivalence on globals *)
@@ -678,7 +692,8 @@ let eq_global g1 g2 =
eq_mllambda gn1 gn2 (Array.length lns1) env1 env2 t1 t2
| Gopen s1, Gopen s2 -> String.equal s1 s2
| Gtype (ind1, arr1), Gtype (ind2, arr2) ->
- eq_ind ind1 ind2 && Array.equal Int.equal arr1 arr2
+ eq_ind ind1 ind2 &&
+ Array.equal (fun (tag1,ar1) (tag2,ar2) -> Int.equal tag1 tag2 && Int.equal ar1 ar2) arr1 arr2
| Gcomment s1, Gcomment s2 -> String.equal s1 s2
| _, _ -> false
@@ -705,7 +720,10 @@ let hash_global g =
combinesmall 4 (combine nlns (hash_mllambda gn nlns env t))
| Gopen s -> combinesmall 5 (String.hash s)
| Gtype (ind, arr) ->
- combinesmall 6 (combine (ind_hash ind) (Array.fold_left combine 0 arr))
+ let hash_aux acc (tag,ar) =
+ combine3 acc (Int.hash tag) (Int.hash ar)
+ in
+ combinesmall 6 (combine (ind_hash ind) (Array.fold_left hash_aux 0 arr))
| Gcomment s -> combinesmall 7 (String.hash s)
let global_stack = ref ([] : global list)
@@ -912,26 +930,33 @@ let get_proj_code i =
[|MLglobal symbols_tbl_name; MLint i|])
type rlist =
- | Rnil
- | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist'
+ | Rnil
+ | Rcons of lname option mllam_pattern list ref * LNset.t * mllambda * rlist'
and rlist' = rlist ref
-let rm_params fv params =
- Array.map (fun l -> if LNset.mem l fv then Some l else None) params
+let rm_params fv params =
+ Array.map (fun l -> if LNset.mem l fv then Some l else None) params
-let rec insert cargs body rl =
+let rec insert pat body rl =
match !rl with
| Rnil ->
let fv = fv_lam body in
- let (c,params) = cargs in
- let params = rm_params fv params in
- rl:= Rcons(ref [(c,params)], fv, body, ref Rnil)
+ begin match pat with
+ | ConstPattern _ as p ->
+ rl:= Rcons(ref [p], fv, body, ref Rnil)
+ | NonConstPattern (tag,args) ->
+ let args = rm_params fv args in
+ rl:= Rcons(ref [NonConstPattern (tag,args)], fv, body, ref Rnil)
+ end
| Rcons(l,fv,body',rl) ->
- if eq_mllambda body body' then
- let (c,params) = cargs in
- let params = rm_params fv params in
- l := (c,params)::!l
- else insert cargs body rl
+ if eq_mllambda body body' then
+ match pat with
+ | ConstPattern _ as p ->
+ l := p::!l
+ | NonConstPattern (tag,args) ->
+ let args = rm_params fv args in
+ l := NonConstPattern (tag,args)::!l
+ else insert pat body rl
let rec to_list rl =
match !rl with
@@ -940,7 +965,7 @@ let rec to_list rl =
let merge_branches t =
let newt = ref Rnil in
- Array.iter (fun (c,args,body) -> insert (c,args) body newt) t;
+ Array.iter (fun (pat,body) -> insert pat body newt) t;
Array.of_list (to_list newt)
let app_prim p args = MLapp(MLprimitive p, args)
@@ -1097,14 +1122,19 @@ let ml_of_instance instance u =
let a_uid = fresh_lname Anonymous in
let la_uid = MLlocal a_uid in
(* compilation of branches *)
- let ml_br (c,params, body) =
- let lnames, env_c = push_rels env_c params in
- (c, lnames, ml_of_lam env_c l body)
+ let nbconst = Array.length bs.constant_branches in
+ let nbtotal = nbconst + Array.length bs.nonconstant_branches in
+ let br = Array.init nbtotal (fun i -> if i < Array.length bs.constant_branches then
+ (ConstPattern i, ml_of_lam env_c l bs.constant_branches.(i))
+ else
+ let (params, body) = bs.nonconstant_branches.(i-nbconst) in
+ let lnames, env_c = push_rels env_c params in
+ (NonConstPattern (i-nbconst+1,lnames), ml_of_lam env_c l body)
+ )
in
- let bs = Array.map ml_br bs in
let cn = fresh_gcase l in
(* Compilation of accu branch *)
- let pred = MLapp(MLglobal pn, fv_args env_c pfvn pfvr) in
+ let pred = MLapp(MLglobal pn, fv_args env_c pfvn pfvr) in
let (fvn, fvr) = !(env_c.env_named), !(env_c.env_urel) in
let cn_fv = mkMLapp (MLglobal cn) (fv_args env_c fvn fvr) in
(* remark : the call to fv_args does not add free variables in env_c *)
@@ -1117,7 +1147,7 @@ let ml_of_instance instance u =
(* let body = MLlam([|a_uid|], MLmatch(annot, la_uid, accu, bs)) in
let case = generalize_fv env_c body in *)
let cn = push_global_case cn (Array.append (fv_params env_c) [|a_uid|])
- annot la_uid accu (merge_branches bs)
+ annot la_uid accu (merge_branches br)
in
(* Final result *)
let arg = ml_of_lam env l a in
@@ -1277,12 +1307,11 @@ let ml_of_instance instance u =
(lname, paramsi, body) in
MLletrec(Array.mapi mkrec lf, lf_args.(start)) *)
- | Lmakeblock (prefix,(cn,_u),_,args) ->
+ | Lint tag -> MLapp(MLprimitive Mk_int, [|MLint tag|])
+
+ | Lmakeblock (prefix,cn,tag,args) ->
let args = Array.map (ml_of_lam env l) args in
- MLconstruct(prefix,cn,args)
- | Lconstruct (prefix, (cn,u)) ->
- let uargs = ml_of_instance env.env_univ u in
- mkMLapp (MLglobal (Gconstruct (prefix, cn))) uargs
+ MLconstruct(prefix,cn,tag,args)
| Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|])
| Lval v ->
let i = push_symbol (SymbValue v) in get_value_code i
@@ -1345,7 +1374,7 @@ let subst s l =
| MLmatch(annot,a,accu,bs) ->
let auxb (cargs,body) = (cargs,aux body) in
MLmatch(annot,a,aux accu, Array.map auxb bs)
- | MLconstruct(prefix,c,args) -> MLconstruct(prefix,c,Array.map aux args)
+ | MLconstruct(prefix,c,tag,args) -> MLconstruct(prefix,c,tag,Array.map aux args)
| MLsetref(s,l1) -> MLsetref(s,aux l1)
| MLsequence(l1,l2) -> MLsequence(aux l1, aux l2)
| MLarray arr -> MLarray (Array.map aux arr)
@@ -1454,8 +1483,8 @@ let optimize gdef l =
| MLmatch(annot,a,accu,bs) ->
let opt_b (cargs,body) = (cargs,optimize s body) in
MLmatch(annot, optimize s a, subst s accu, Array.map opt_b bs)
- | MLconstruct(prefix,c,args) ->
- MLconstruct(prefix,c,Array.map (optimize s) args)
+ | MLconstruct(prefix,c,tag,args) ->
+ MLconstruct(prefix,c,tag,Array.map (optimize s) args)
| MLsetref(r,l) -> MLsetref(r, optimize s l)
| MLsequence(l1,l2) -> MLsequence(optimize s l1, optimize s l2)
| MLarray arr -> MLarray (Array.map (optimize s) arr)
@@ -1528,13 +1557,12 @@ let string_of_kn kn =
let string_of_con c = string_of_kn (Constant.user c)
let string_of_mind mind = string_of_kn (MutInd.user mind)
+let string_of_ind (mind,i) = string_of_kn (MutInd.user mind) ^ "_" ^ string_of_int i
let string_of_gname g =
match g with
| Gind (prefix, (mind, i)) ->
Format.sprintf "%sindaccu_%s_%i" prefix (string_of_mind mind) i
- | Gconstruct (prefix, ((mind, i), j)) ->
- Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1)
| Gconstant (prefix, c) ->
Format.sprintf "%sconst_%s" prefix (string_of_con c)
| Gproj (prefix, (mind, n), i) ->
@@ -1567,10 +1595,13 @@ let pp_ldecls fmt ids =
Format.fprintf fmt " (%a : Nativevalues.t)" pp_lname ids.(i)
done
-let string_of_construct prefix ((mind,i),j) =
- let id = Format.sprintf "Construct_%s_%i_%i" (string_of_mind mind) i (j-1) in
- prefix ^ id
-
+let string_of_construct prefix ~constant ind tag =
+ let base = if constant then "Int" else "Construct" in
+ Format.sprintf "%s%s_%s_%i" prefix base (string_of_ind ind) tag
+
+let string_of_accu_construct prefix ind =
+ Format.sprintf "%sAccu_%s" prefix (string_of_ind ind)
+
let pp_int fmt i =
if i < 0 then Format.fprintf fmt "(%i)" i else Format.fprintf fmt "%i" i
@@ -1596,16 +1627,16 @@ let pp_mllam fmt l =
Format.fprintf fmt "@[(if %a then@\n %a@\nelse@\n %a)@]"
pp_mllam t pp_mllam l1 pp_mllam l2
| MLmatch (annot, c, accu_br, br) ->
- let mind,i = annot.asw_ind in
+ let ind = annot.asw_ind in
let prefix = annot.asw_prefix in
- let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in
- Format.fprintf fmt
- "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n %a@\n%aend@]"
- pp_mllam c accu pp_mllam accu_br (pp_branches prefix) br
-
- | MLconstruct(prefix,c,args) ->
+ let accu = string_of_accu_construct prefix ind in
+ Format.fprintf fmt
+ "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n %a@\n%aend@]"
+ pp_mllam c accu pp_mllam accu_br (pp_branches prefix ind) br
+
+ | MLconstruct(prefix,ind,tag,args) ->
Format.fprintf fmt "@[(Obj.magic (%s%a) : Nativevalues.t)@]"
- (string_of_construct prefix c) pp_cargs args
+ (string_of_construct prefix ~constant:false ind tag) pp_cargs args
| MLint i -> pp_int fmt i
| MLuint i -> Format.fprintf fmt "(%s)" (Uint63.compile i)
| MLsetref (s, body) ->
@@ -1622,8 +1653,8 @@ let pp_mllam fmt l =
pp_mllam fmt arr.(len-1)
end;
Format.fprintf fmt "|]@]"
- | MLisaccu (prefix, (mind, i), c) ->
- let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in
+ | MLisaccu (prefix, ind, c) ->
+ let accu = string_of_accu_construct prefix ind in
Format.fprintf fmt
"@[begin match Obj.magic (%a) with@\n| %s _ ->@\n true@\n| _ ->@\n false@\nend@]"
pp_mllam c accu
@@ -1646,7 +1677,7 @@ let pp_mllam fmt l =
| MLprimitive (Mk_prod | Mk_sort) (* FIXME: why this special case? *)
| MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ ->
Format.fprintf fmt "(%a)" pp_mllam l
- | MLconstruct(_,_,args) when Array.length args > 0 ->
+ | MLconstruct(_,_,_,args) when Array.length args > 0 ->
Format.fprintf fmt "(%a)" pp_mllam l
| _ -> pp_mllam fmt l
@@ -1685,19 +1716,23 @@ let pp_mllam fmt l =
done in
Format.fprintf fmt "(%a)" aux params
- and pp_branches prefix fmt bs =
+ and pp_branches prefix ind fmt bs =
let pp_branch (cargs,body) =
- let pp_c fmt (cn,args) =
- Format.fprintf fmt "| %s%a "
- (string_of_construct prefix cn) pp_cparams args in
- let rec pp_cargs fmt cargs =
- match cargs with
- | [] -> ()
- | cargs::cargs' ->
- Format.fprintf fmt "%a%a" pp_c cargs pp_cargs cargs' in
- Format.fprintf fmt "%a ->@\n %a@\n"
- pp_cargs cargs pp_mllam body
+ let pp_pat fmt = function
+ | ConstPattern i ->
+ Format.fprintf fmt "| %s "
+ (string_of_construct prefix ~constant:true ind i)
+ | NonConstPattern (tag,args) ->
+ Format.fprintf fmt "| %s%a "
+ (string_of_construct prefix ~constant:false ind tag) pp_cparams args in
+ let rec pp_pats fmt pats =
+ match pats with
+ | [] -> ()
+ | pat::pats ->
+ Format.fprintf fmt "%a%a" pp_pat pat pp_pats pats
in
+ Format.fprintf fmt "%a ->@\n %a@\n" pp_pats cargs pp_mllam body
+ in
Array.iter pp_branch bs
and pp_primitive fmt = function
@@ -1771,19 +1806,24 @@ let pp_global fmt g =
pp_mllam c
| Gopen s ->
Format.fprintf fmt "@[open %s@]@." s
- | Gtype ((mind, i), lar) ->
- let l = string_of_mind mind in
- let rec aux s ar =
- if Int.equal ar 0 then s else aux (s^" * Nativevalues.t") (ar-1) in
- let pp_const_sig i fmt j ar =
- let sig_str = if ar > 0 then aux "of Nativevalues.t" (ar-1) else "" in
- Format.fprintf fmt " | Construct_%s_%i_%i %s@\n" l i j sig_str
- in
- let pp_const_sigs i fmt lar =
- Format.fprintf fmt " | Accu_%s_%i of Nativevalues.t@\n" l i;
- Array.iteri (pp_const_sig i fmt) lar
- in
- Format.fprintf fmt "@[type ind_%s_%i =@\n%a@]@\n@." l i (pp_const_sigs i) lar
+ | Gtype (ind, lar) ->
+ let rec aux s arity =
+ if Int.equal arity 0 then s else aux (s^" * Nativevalues.t") (arity-1) in
+ let pp_const_sig fmt (tag,arity) =
+ if arity > 0 then
+ let sig_str = aux "of Nativevalues.t" (arity-1) in
+ let cstr = string_of_construct "" ~constant:false ind tag in
+ Format.fprintf fmt " | %s %s@\n" cstr sig_str
+ else
+ let sig_str = if arity > 0 then aux "of Nativevalues.t" (arity-1) else "" in
+ let cstr = string_of_construct "" ~constant:true ind tag in
+ Format.fprintf fmt " | %s %s@\n" cstr sig_str
+ in
+ let pp_const_sigs fmt lar =
+ Format.fprintf fmt " | %s of Nativevalues.t@\n" (string_of_accu_construct "" ind);
+ Array.iter (pp_const_sig fmt) lar
+ in
+ Format.fprintf fmt "@[type ind_%s =@\n%a@]@\n@." (string_of_ind ind) pp_const_sigs lar
| Gtblfixtype (g, params, t) ->
Format.fprintf fmt "@[let %a %a =@\n %a@]@\n@." pp_gname g
pp_ldecls params pp_array t
@@ -1920,7 +1960,7 @@ let compile_mind mb mind stack =
(** Generate data for every block *)
let f i stack ob =
let ind = (mind, i) in
- let gtype = Gtype(ind, Array.map snd ob.mind_reloc_tbl) in
+ let gtype = Gtype(ind, ob.mind_reloc_tbl) in
let j = push_symbol (SymbInd ind) in
let name = Gind ("", ind) in
let accu =
@@ -1932,16 +1972,6 @@ let compile_mind mb mind stack =
Glet(name, MLapp (MLprimitive Mk_ind, args))
in
let nparams = mb.mind_nparams in
- let params =
- Array.init nparams (fun i -> {lname = param_name; luid = i}) in
- let add_construct j acc (_,arity) =
- let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in
- let c = ind, (j+1) in
- Glet(Gconstruct ("", c),
- mkMLlam (Array.append params args)
- (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc
- in
- let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in
let add_proj proj_arg acc _pb =
let tbl = ob.mind_reloc_tbl in
(* Building info *)
@@ -1953,15 +1983,16 @@ let compile_mind mb mind stack =
asw_reloc = tbl; asw_finite = true } in
let c_uid = fresh_lname Anonymous in
let cf_uid = fresh_lname Anonymous in
- let _, arity = tbl.(0) in
+ let tag, arity = tbl.(0) in
+ assert (arity > 0);
let ci_uid = fresh_lname Anonymous in
let cargs = Array.init arity
(fun i -> if Int.equal i proj_arg then Some ci_uid else None)
in
- let i = push_symbol (SymbProj (ind, j)) in
+ let i = push_symbol (SymbProj (ind, proj_arg)) in
let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in
let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in
- let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
+ let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[NonConstPattern (tag,cargs)],MLlocal ci_uid|]) in
let code = MLlet(cf_uid, mkForceCofix "" ind (MLlocal c_uid), code) in
let gn = Gproj ("", ind, proj_arg) in
Glet (gn, mkMLlam [|c_uid|] code) :: acc
@@ -1972,7 +2003,7 @@ let compile_mind mb mind stack =
let _, _, _, pbs = info.(i) in
Array.fold_left_i add_proj [] pbs
in
- projs @ constructors @ gtype :: accu :: stack
+ projs @ gtype :: accu :: stack
in
Array.fold_left_i f stack mb.mind_packets
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index baa290367f..d153f84e9c 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open CErrors
open Names
open Nativelib
open Reduction
@@ -152,19 +151,15 @@ let native_conv_gen pb sigma env univs t1 t2 =
else
let ml_filename, prefix = get_ml_filename () in
let code, upds = mk_conv_code env sigma prefix t1 t2 in
- match compile ml_filename code ~profile:false with
- | (true, fn) ->
- begin
- if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
- let t0 = Sys.time () in
- call_linker ~fatal:true prefix fn (Some upds);
- let t1 = Sys.time () in
- let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
- if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
- (* TODO change 0 when we can have de Bruijn *)
- fst (conv_val env pb 0 !rt1 !rt2 univs)
- end
- | _ -> anomaly (Pp.str "Compilation failure.")
+ let fn = compile ml_filename code ~profile:false in
+ if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
+ let t0 = Sys.time () in
+ call_linker ~fatal:true prefix fn (Some upds);
+ let t1 = Sys.time () in
+ let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
+ if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
+ (* TODO change 0 when we can have de Bruijn *)
+ fst (conv_val env pb 0 !rt1 !rt2 univs)
(* Wrapper for [native_conv] above *)
let native_conv cv_pb sigma env t1 t2 =
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index ec3a7b893d..62afd9df68 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -39,11 +39,10 @@ type lambda =
| Lif of lambda * lambda * lambda
| Lfix of (int array * (string * inductive) array * int) * fix_decl
| Lcofix of int * fix_decl
- | Lmakeblock of prefix * pconstructor * int * lambda array
- (* prefix, constructor Name.t, constructor tag, arguments *)
- (* A fully applied constructor *)
- | Lconstruct of prefix * pconstructor (* prefix, constructor Name.t *)
- (* A partially applied constructor *)
+ | Lint of int (* a constant constructor *)
+ | Lmakeblock of prefix * inductive * int * lambda array
+ (* prefix, inductive name, constructor tag, arguments *)
+ (* A fully applied non-constant constructor *)
| Luint of Uint63.t
| Lval of Nativevalues.t
| Lsort of Sorts.t
@@ -51,7 +50,10 @@ type lambda =
| Llazy
| Lforce
-and lam_branches = (constructor * Name.t Context.binder_annot array * lambda) array
+and lam_branches =
+ { constant_branches : lambda array;
+ nonconstant_branches : (Name.t Context.binder_annot array * lambda) array;
+ }
and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array
@@ -121,7 +123,7 @@ let get_const_prefix env c =
let map_lam_with_binders g f n lam =
match lam with
| Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Luint _
- | Lconstruct _ | Llazy | Lforce | Lmeta _ -> lam
+ | Llazy | Lforce | Lmeta _ | Lint _ -> lam
| Lprod(dom,codom) ->
let dom' = f n dom in
let codom' = f n codom in
@@ -143,17 +145,26 @@ let map_lam_with_binders g f n lam =
| Lprim(prefix,kn,op,args) ->
let args' = Array.Smart.map (f n) args in
if args == args' then lam else Lprim(prefix,kn,op,args')
- | Lcase(annot,t,a,br) ->
- let t' = f n t in
- let a' = f n a in
- let on_b b =
- let (cn,ids,body) = b in
- let body' =
- if Array.is_empty ids then f n body
- else f (g (Array.length ids) n) body in
- if body == body' then b else (cn,ids,body') in
- let br' = Array.Smart.map on_b br in
- if t == t' && a == a' && br == br' then lam else Lcase(annot,t',a',br')
+ | Lcase(annot,t,a,branches) ->
+ let const = branches.constant_branches in
+ let nonconst = branches.nonconstant_branches in
+ let t' = f n t in
+ let a' = f n a in
+ let const' = Array.Smart.map (f n) const in
+ let on_b b =
+ let (ids,body) = b in
+ let body' = f (g (Array.length ids) n) body in
+ if body == body' then b else (ids,body') in
+ let nonconst' = Array.Smart.map on_b nonconst in
+ let branches' =
+ if const == const' && nonconst == nonconst' then
+ branches
+ else
+ { constant_branches = const';
+ nonconstant_branches = nonconst' }
+ in
+ if t == t' && a == a' && branches == branches' then lam else
+ Lcase(annot,t',a',branches')
| Lif(t,bt,bf) ->
let t' = f n t in
let bt' = f n bt in
@@ -222,7 +233,7 @@ let lam_subst_args subst args =
let can_subst lam =
match lam with
| Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Llam _
- | Lconstruct _ | Lmeta _ | Levar _ -> true
+ | Lmeta _ | Levar _ -> true
| _ -> false
let can_merge_if bt bf =
@@ -320,16 +331,13 @@ and reduce_lapp substf lids body substa largs =
let is_value lc =
match lc with
- | Lval _ -> true
- | Lmakeblock(_,_,_,args) when Array.is_empty args -> true
- | Luint _ -> true
+ | Lval _ | Lint _ | Luint _ -> true
| _ -> false
let get_value lc =
match lc with
| Lval v -> v
- | Lmakeblock(_,_,tag,args) when Array.is_empty args ->
- Nativevalues.mk_int tag
+ | Lint tag -> Nativevalues.mk_int tag
| Luint i -> Nativevalues.mk_uint i
| _ -> raise Not_found
@@ -337,14 +345,30 @@ let make_args start _end =
Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i))
(* Translation of constructors *)
+let expand_constructor prefix ind tag nparams arity =
+ let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *)
+ let ids = Array.make (nparams + arity) anon in
+ if Int.equal arity 0 then mkLlam ids (Lint tag)
+ else
+ let args = make_args arity 1 in
+ Llam(ids, Lmakeblock (prefix, ind, tag, args))
-let makeblock env cn u tag args =
- if Array.for_all is_value args && Array.length args > 0 then
+(* [nparams] is the number of parameters still expected *)
+let makeblock env ind tag nparams arity args =
+ let nargs = Array.length args in
+ if nparams > 0 || nargs < arity then
+ let prefix = get_mind_prefix env (fst ind) in
+ mkLapp (expand_constructor prefix ind tag nparams arity) args
+ else
+ (* The constructor is fully applied *)
+ if Int.equal arity 0 then Lint tag
+ else
+ if Array.for_all is_value args then
let args = Array.map get_value args in
Lval (Nativevalues.mk_block tag args)
else
- let prefix = get_mind_prefix env (fst (fst cn)) in
- Lmakeblock(prefix, (cn,u), tag, args)
+ let prefix = get_mind_prefix env (fst ind) in
+ Lmakeblock(prefix, ind, tag, args)
(* Translation of constants *)
@@ -420,8 +444,6 @@ let empty_evars =
{ evars_val = (fun _ -> None);
evars_metas = (fun _ -> assert false) }
-let empty_ids = [||]
-
(** Extract the inductive type over which a fixpoint is decreasing *)
let rec get_fix_struct env i t = match kind (Reduction.whd_all env t) with
| Prod (na, dom, t) ->
@@ -492,43 +514,51 @@ let rec lambda_of_constr cache env sigma c =
let prefix = get_mind_prefix env (fst ind) in
mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|]
- | Case(ci,t,a,branches) ->
- let (mind,i as ind) = ci.ci_ind in
- let mib = lookup_mind mind env in
- let oib = mib.mind_packets.(i) in
- let tbl = oib.mind_reloc_tbl in
- (* Building info *)
- let prefix = get_mind_prefix env mind in
- let annot_sw =
- { asw_ind = ind;
- asw_ci = ci;
- asw_reloc = tbl;
- asw_finite = mib.mind_finite <> CoFinite;
- asw_prefix = prefix}
- in
- (* translation of the argument *)
- let la = lambda_of_constr cache env sigma a in
- (* translation of the type *)
- let lt = lambda_of_constr cache env sigma t in
- (* translation of branches *)
- let mk_branch i b =
- let cn = (ind,i+1) in
- let _, arity = tbl.(i) in
- let b = lambda_of_constr cache env sigma b in
- if Int.equal arity 0 then (cn, empty_ids, b)
- else
- match b with
- | Llam(ids, body) when Int.equal (Array.length ids) arity -> (cn, ids, body)
+ | Case(ci,t,a,branches) ->
+ let (mind,i as ind) = ci.ci_ind in
+ let mib = lookup_mind mind env in
+ let oib = mib.mind_packets.(i) in
+ let tbl = oib.mind_reloc_tbl in
+ (* Building info *)
+ let prefix = get_mind_prefix env mind in
+ let annot_sw =
+ { asw_ind = ind;
+ asw_ci = ci;
+ asw_reloc = tbl;
+ asw_finite = mib.mind_finite <> CoFinite;
+ asw_prefix = prefix}
+ in
+ (* translation of the argument *)
+ let la = lambda_of_constr cache env sigma a in
+ (* translation of the type *)
+ let lt = lambda_of_constr cache env sigma t in
+ (* translation of branches *)
+ let dummy = Lrel(Anonymous,0) in
+ let consts = Array.make oib.mind_nb_constant dummy in
+ let blocks = Array.make oib.mind_nb_args ([||],dummy) in
+ let rtbl = oib.mind_reloc_tbl in
+ for i = 0 to Array.length rtbl - 1 do
+ let tag, arity = rtbl.(i) in
+ let b = lambda_of_constr cache env sigma branches.(i) in
+ if arity = 0 then consts.(tag) <- b
+ else
+ let b =
+ match b with
+ | Llam(ids, body) when Array.length ids = arity -> (ids, body)
| _ ->
- (** TODO relevance *)
- let anon = Context.make_annot Anonymous Sorts.Relevant in
- let ids = Array.make arity anon in
- let args = make_args arity 1 in
- let ll = lam_lift arity b in
- (cn, ids, mkLapp ll args) in
- let bs = Array.mapi mk_branch branches in
- Lcase(annot_sw, lt, la, bs)
-
+ let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *)
+ let ids = Array.make arity anon in
+ let args = make_args arity 1 in
+ let ll = lam_lift arity b in
+ (ids, mkLapp ll args)
+ in blocks.(tag-1) <- b
+ done;
+ let branches =
+ { constant_branches = consts;
+ nonconstant_branches = blocks }
+ in
+ Lcase(annot_sw, lt, la, branches)
+
| Fix((pos, i), (names,type_bodies,rec_bodies)) ->
let ltypes = lambda_of_args cache env sigma 0 type_bodies in
let map i t =
@@ -572,17 +602,13 @@ and lambda_of_app cache env sigma f args =
let prefix = get_const_prefix env kn in
mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args cache env sigma 0 args)
end
- | Construct (c,u) ->
- let tag, nparams, arity = Cache.get_construct_info cache env c in
- let expected = nparams + arity in
- let nargs = Array.length args in
- let prefix = get_mind_prefix env (fst (fst c)) in
- if Int.equal nargs expected then
- let args = lambda_of_args cache env sigma nparams args in
- makeblock env c u tag args
- else
- let args = lambda_of_args cache env sigma 0 args in
- mkLapp (Lconstruct (prefix, (c,u))) args
+ | Construct ((ind,_ as c),_) ->
+ let tag, nparams, arity = Cache.get_construct_info cache env c in
+ let nargs = Array.length args in
+ if nparams < nargs then (* got all parameters *)
+ let args = lambda_of_args cache env sigma nparams args in
+ makeblock env ind tag 0 arity args
+ else makeblock env ind tag (nparams - nargs) arity empty_args
| _ ->
let f = lambda_of_constr cache env sigma f in
let args = lambda_of_args cache env sigma 0 args in
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index b0de257a27..446df1a1ea 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -33,11 +33,10 @@ type lambda =
| Lif of lambda * lambda * lambda
| Lfix of (int array * (string * inductive) array * int) * fix_decl
| Lcofix of int * fix_decl
- | Lmakeblock of prefix * pconstructor * int * lambda array
- (* prefix, constructor Name.t, constructor tag, arguments *)
- (* A fully applied constructor *)
- | Lconstruct of prefix * pconstructor (* prefix, constructor Name.t *)
- (* A partially applied constructor *)
+ | Lint of int (* a constant constructor *)
+ | Lmakeblock of prefix * inductive * int * lambda array
+ (* prefix, inductive name, constructor tag, arguments *)
+ (* A fully applied non-constant constructor *)
| Luint of Uint63.t
| Lval of Nativevalues.t
| Lsort of Sorts.t
@@ -45,7 +44,10 @@ type lambda =
| Llazy
| Lforce
-and lam_branches = (constructor * Name.t Context.binder_annot array * lambda) array
+and lam_branches =
+ { constant_branches : lambda array;
+ nonconstant_branches : (Name.t Context.binder_annot array * lambda) array;
+ }
and fix_decl = Name.t Context.binder_annot array * lambda array * lambda array
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 833e4082f0..43c9676f05 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -56,14 +56,15 @@ let write_ml_code fn ?(header=[]) code =
List.iter (pp_global fmt) (header@code);
close_out ch_out
-let warn_native_compiler_failed =
- let print = function
+let error_native_compiler_failed e =
+ let msg = match e with
+ | Inl (Unix.WEXITED 127) -> Pp.(strbrk "The OCaml compiler was not found. Make sure it is installed, together with findlib.")
| Inl (Unix.WEXITED n) -> Pp.(strbrk "Native compiler exited with status" ++ str" " ++ int n)
| Inl (Unix.WSIGNALED n) -> Pp.(strbrk "Native compiler killed by signal" ++ str" " ++ int n)
| Inl (Unix.WSTOPPED n) -> Pp.(strbrk "Native compiler stopped by signal" ++ str" " ++ int n)
| Inr e -> Pp.(strbrk "Native compiler failed with error: " ++ strbrk (Unix.error_message e))
in
- CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print
+ CErrors.user_err msg
let call_compiler ?profile:(profile=false) ml_filename =
let load_path = !get_load_paths () in
@@ -100,15 +101,12 @@ let call_compiler ?profile:(profile=false) ml_filename =
if !Flags.debug then Feedback.msg_debug (Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args)));
try
let res = CUnix.sys_command (Envars.ocamlfind ()) args in
- let res = match res with
- | Unix.WEXITED 0 -> true
- | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
- warn_native_compiler_failed (Inl res); false
- in
- res, link_filename
+ match res with
+ | Unix.WEXITED 0 -> link_filename
+ | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
+ error_native_compiler_failed (Inl res)
with Unix.Unix_error (e,_,_) ->
- warn_native_compiler_failed (Inr e);
- false, link_filename
+ error_native_compiler_failed (Inr e)
let compile fn code ~profile:profile =
write_ml_code fn code;
@@ -128,9 +126,8 @@ let compile_library dir code fn =
in
let fn = dirname / basename in
write_ml_code fn ~header code;
- let r = fst (call_compiler fn) in
- if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn;
- r
+ let _ = call_compiler fn in
+ if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn
(* call_linker links dynamically the code for constants in environment or a *)
(* conversion test. *)
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index 25adcf224b..e113350368 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -21,9 +21,14 @@ val load_obj : (string -> unit) ref
val get_ml_filename : unit -> string * string
-val compile : string -> global list -> profile:bool -> bool * string
-
-val compile_library : Names.DirPath.t -> global list -> string -> bool
+(** [compile file code ~profile] will compile native [code] to [file],
+ and return the name of the object file; this name depends on
+ whether are in byte mode or not; file is expected to be .ml file *)
+val compile : string -> global list -> profile:bool -> string
+
+(** [compile_library lib code file] is similar to [compile file code]
+ but will perform some extra tweaks to handle [code] as a Coq lib. *)
+val compile_library : Names.DirPath.t -> global list -> string -> unit
val call_linker :
?fatal:bool -> string -> string -> code_location_updates option -> unit
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 303cb06c55..57059300b8 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -87,19 +87,18 @@ let discharge_direct_opaque ~cook_constr ci = function
| Direct (d,cu) ->
Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
-let join_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) -> ignore(Future.join cu)
+let join except cu = match except with
+| None -> ignore (Future.join cu)
+| Some except ->
+ if Future.UUIDSet.mem (Future.uuid cu) except then ()
+ else ignore (Future.join cu)
+
+let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
+ | Direct (_,cu) -> join except cu
| Indirect (_,dp,i) ->
if DirPath.equal dp odp then
let fp = snd (Int.Map.find i prfs) in
- ignore(Future.join fp)
-
-let uuid_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) -> Some (Future.uuid cu)
- | Indirect (_,dp,i) ->
- if DirPath.equal dp odp
- then Some (Future.uuid (snd (Int.Map.find i prfs)))
- else None
+ join except fp
let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
| Direct (_,cu) ->
@@ -128,16 +127,6 @@ let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
then Some(Future.chain (snd (Int.Map.find i prfs)) snd)
else !get_univ dp i
-let get_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) -> Future.chain cu fst
- | Indirect (l,dp,i) ->
- let pt =
- if DirPath.equal dp odp
- then Future.chain (snd (Int.Map.find i prfs)) fst
- else !get_opaque dp i in
- Future.chain pt (fun c ->
- force_constr (List.fold_right subst_substituted l (from_val c)))
-
module FMap = Future.UUIDMap
let a_constr = Future.from_val (mkRel 1)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 5ea6da649b..d47c0bbb3c 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -39,7 +39,6 @@ val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
indirect opaque accessor configured below. *)
val force_proof : opaquetab -> opaque -> constr
val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t
-val get_proof : opaquetab -> opaque -> constr Future.computation
val get_constraints :
opaquetab -> opaque -> Univ.ContextSet.t Future.computation option
@@ -60,8 +59,7 @@ type cooking_info = {
val discharge_direct_opaque :
cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque
-val uuid_opaque : opaquetab -> opaque -> Future.UUID.t option
-val join_opaque : opaquetab -> opaque -> unit
+val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
val dump : opaquetab ->
Constr.t Future.computation array *
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 673f025c75..75375812c0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -228,6 +228,12 @@ let check_engagement env expected_impredicative_set =
(** {6 Stm machinery } *)
+type seff_env =
+ [ `Nothing
+ (* The proof term and its universes.
+ Same as the constant_body's but not in an ephemeron *)
+ | `Opaque of Constr.t * Univ.ContextSet.t ]
+
let get_opaque_body env cbo =
match cbo.const_body with
| Undef _ -> assert false
@@ -240,7 +246,10 @@ let get_opaque_body env cbo =
type side_effect = {
from_env : Declarations.structure_body CEphemeron.key;
- eff : Entries.side_eff list;
+ seff_constant : Constant.t;
+ seff_body : Declarations.constant_body;
+ seff_env : seff_env;
+ seff_role : Entries.side_effect_role;
}
module SideEffects :
@@ -254,11 +263,9 @@ end =
struct
module SeffOrd = struct
-open Entries
type t = side_effect
let compare e1 e2 =
- let cmp e1 e2 = Constant.CanOrd.compare e1.seff_constant e2.seff_constant in
- List.compare cmp e1.eff e2.eff
+ Constant.CanOrd.compare e1.seff_constant e2.seff_constant
end
module SeffSet = Set.Make(SeffOrd)
@@ -279,37 +286,37 @@ end
type private_constants = SideEffects.t
let side_effects_of_private_constants l =
- let ans = List.rev (SideEffects.repr l) in
- List.map_append (fun { eff; _ } -> eff) ans
+ List.rev (SideEffects.repr l)
+
+let push_private_constants env eff =
+ let eff = side_effects_of_private_constants eff in
+ let add_if_undefined env eff =
+ try ignore(Environ.lookup_constant eff.seff_constant env); env
+ with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
+ in
+ List.fold_left add_if_undefined env eff
let empty_private_constants = SideEffects.empty
-let add_private mb eff effs =
- let from_env = CEphemeron.create mb in
- SideEffects.add { eff; from_env } effs
let concat_private = SideEffects.concat
-let make_eff env cst r =
- let open Entries in
+let private_constant env role cst =
+ (** The constant must be the last entry of the safe environment *)
+ let () = match env.revstruct with
+ | (lbl, SFBconst _) :: _ -> assert (Label.equal lbl (Constant.label cst))
+ | _ -> assert false
+ in
+ let from_env = CEphemeron.create env.revstruct in
let cbo = Environ.lookup_constant cst env.env in
- {
+ let eff = {
+ from_env = from_env;
seff_constant = cst;
seff_body = cbo;
seff_env = get_opaque_body env.env cbo;
- seff_role = r;
- }
-
-let private_con_of_con env c =
- let open Entries in
- let eff = [make_eff env c Subproof] in
- add_private env.revstruct eff empty_private_constants
-
-let private_con_of_scheme ~kind env cl =
- let open Entries in
- let eff = List.map (fun (i, c) -> make_eff env c (Schema (i, kind))) cl in
- add_private env.revstruct eff empty_private_constants
+ seff_role = role;
+ } in
+ SideEffects.add eff empty_private_constants
let universes_of_private eff =
- let open Entries in
let fold acc eff =
let acc = match eff.seff_env with
| `Nothing -> acc
@@ -588,22 +595,17 @@ let add_constant_aux ~in_section senv (kn, cb) =
let mk_pure_proof c = (c, Univ.ContextSet.empty), SideEffects.empty
let inline_side_effects env body side_eff =
- let open Entries in
let open Constr in
(** First step: remove the constants that are still in the environment *)
- let filter { eff = se; from_env = mb } =
- let map e = (e.seff_constant, e.seff_body, e.seff_env) in
- let cbl = List.map map se in
- let not_exists (c,_,_) =
- try ignore(Environ.lookup_constant c env); false
- with Not_found -> true in
- let cbl = List.filter not_exists cbl in
- (cbl, mb)
+ let filter e =
+ let cb = (e.seff_constant, e.seff_body, e.seff_env) in
+ try ignore (Environ.lookup_constant e.seff_constant env); None
+ with Not_found -> Some (cb, e.from_env)
in
(* CAVEAT: we assure that most recent effects come first *)
- let side_eff = List.map filter (SideEffects.repr side_eff) in
- let sigs = List.rev_map (fun (cbl, mb) -> mb, List.length cbl) side_eff in
- let side_eff = List.fold_left (fun accu (cbl, _) -> cbl @ accu) [] side_eff in
+ let side_eff = List.map_filter filter (SideEffects.repr side_eff) in
+ let sigs = List.rev_map (fun (_, mb) -> mb) side_eff in
+ let side_eff = List.fold_left (fun accu (cb, _) -> cb :: accu) [] side_eff in
let side_eff = List.rev side_eff in
(** Most recent side-effects first in side_eff *)
if List.is_empty side_eff then (body, Univ.ContextSet.empty, sigs)
@@ -675,24 +677,22 @@ let inline_private_constants_in_definition_entry env ce =
let inline_private_constants_in_constr env body side_eff =
pi1 (inline_side_effects env body side_eff)
-let rec is_nth_suffix n l suf =
- if Int.equal n 0 then l == suf
- else match l with
- | [] -> false
- | _ :: l -> is_nth_suffix (pred n) l suf
+let is_suffix l suf = match l with
+| [] -> false
+| _ :: l -> l == suf
(* Given the list of signatures of side effects, checks if they match.
* I.e. if they are ordered descendants of the current revstruct.
Returns the number of effects that can be trusted. *)
let check_signatures curmb sl =
- let is_direct_ancestor accu (mb, how_many) =
+ let is_direct_ancestor accu mb =
match accu with
| None -> None
| Some (n, curmb) ->
try
let mb = CEphemeron.get mb in
- if is_nth_suffix how_many mb curmb
- then Some (n + how_many, mb)
+ if is_suffix mb curmb
+ then Some (n + 1, mb)
else None
with CEphemeron.InvalidKey -> None in
let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in
@@ -725,7 +725,6 @@ let constant_entry_of_side_effect cb u =
const_entry_inline_code = cb.const_inline_code }
let turn_direct orig =
- let open Entries in
let cb = orig.seff_body in
if Declareops.is_opaque cb then
let p = match orig.seff_env with
@@ -738,7 +737,6 @@ let turn_direct orig =
else orig
let export_eff eff =
- let open Entries in
(eff.seff_constant, eff.seff_body, eff.seff_role)
let export_side_effects mb env c =
@@ -751,10 +749,9 @@ let export_side_effects mb env c =
let not_exists e =
try ignore(Environ.lookup_constant e.seff_constant env); false
with Not_found -> true in
- let aux (acc,sl) { eff = se; from_env = mb } =
- let cbl = List.filter not_exists se in
- if List.is_empty cbl then acc, sl
- else cbl :: acc, (mb,List.length cbl) :: sl in
+ let aux (acc,sl) e =
+ if not (not_exists e) then acc, sl
+ else e :: acc, e.from_env :: sl in
let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in
let trusted = check_signatures mb signatures in
let push_seff env eff =
@@ -772,10 +769,9 @@ let export_side_effects mb env c =
let rec translate_seff sl seff acc env =
match seff with
| [] -> List.rev acc, ce
- | cbs :: rest ->
+ | eff :: rest ->
if Int.equal sl 0 then
- let env, cbs =
- List.fold_left (fun (env,cbs) eff ->
+ let env, cb =
let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in
let ce = constant_entry_of_side_effect ocb u in
let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in
@@ -783,15 +779,14 @@ let export_side_effects mb env c =
seff_body = cb;
seff_env = `Nothing;
} in
- (push_seff env eff, export_eff eff :: cbs))
- (env,[]) cbs in
- translate_seff 0 rest (cbs @ acc) env
+ (push_seff env eff, export_eff eff)
+ in
+ translate_seff 0 rest (cb :: acc) env
else
- let cbs_len = List.length cbs in
- let cbs = List.map turn_direct cbs in
- let env = List.fold_left push_seff env cbs in
- let ecbs = List.map export_eff cbs in
- translate_seff (sl - cbs_len) rest (ecbs @ acc) env
+ let cb = turn_direct eff in
+ let env = push_seff env cb in
+ let ecb = export_eff cb in
+ translate_seff (sl - 1) rest (ecb :: acc) env
in
translate_seff trusted seff [] env
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 46c97c1fb8..d6c7022cf5 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -43,18 +43,13 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
type private_constants
-val side_effects_of_private_constants :
- private_constants -> Entries.side_eff list
-(** Return the list of individual side-effects in the order of their
- creation. *)
-
val empty_private_constants : private_constants
val concat_private : private_constants -> private_constants -> private_constants
(** [concat_private e1 e2] adds the constants of [e1] to [e2], i.e. constants in
[e1] must be more recent than those of [e2]. *)
-val private_con_of_con : safe_environment -> Constant.t -> private_constants
-val private_con_of_scheme : kind:string -> safe_environment -> (inductive * Constant.t) list -> private_constants
+val private_constant : safe_environment -> Entries.side_effect_role -> Constant.t -> private_constants
+(** Constant must be the last definition of the safe_environment. *)
val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
val inline_private_constants_in_constr :
@@ -62,6 +57,9 @@ val inline_private_constants_in_constr :
val inline_private_constants_in_definition_entry :
Environ.env -> private_constants Entries.definition_entry -> unit Entries.definition_entry
+val push_private_constants : Environ.env -> private_constants -> Environ.env
+(** Push the constants in the environment if not already there. *)
+
val universes_of_private : private_constants -> Univ.ContextSet.t list
val is_curmod_library : safe_environment -> bool
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 12ffbf4357..af710e7822 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -462,28 +462,6 @@ let type_of_global_in_context env r =
let inst = Univ.make_abstract_instance univs in
Inductive.type_of_constructor (cstr,inst) specif, univs
-(* Build a fresh instance for a given context, its associated substitution and
- the instantiated constraints. *)
-
-let constr_of_global_in_context env r =
- let open GlobRef in
- match r with
- | VarRef id -> mkVar id, Univ.AUContext.empty
- | ConstRef c ->
- let cb = lookup_constant c env in
- let univs = Declareops.constant_polymorphic_context cb in
- mkConstU (c, Univ.make_abstract_instance univs), univs
- | IndRef ind ->
- let (mib,_) = Inductive.lookup_mind_specif env ind in
- let univs = Declareops.inductive_polymorphic_context mib in
- mkIndU (ind, Univ.make_abstract_instance univs), univs
- | ConstructRef cstr ->
- let (mib,_) =
- Inductive.lookup_mind_specif env (inductive_of_constructor cstr)
- in
- let univs = Declareops.inductive_polymorphic_context mib in
- mkConstructU (cstr, Univ.make_abstract_instance univs), univs
-
(************************************************************************)
(************************************************************************)
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index cc1885f42d..c8f3e506e6 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -107,14 +107,6 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
usage. For non-universe-polymorphic constants, it does not
matter. *)
-(** {6 Building a term from a global reference *)
-
-(** Map a global reference to a term in its local universe
- context. The term should not be used without pushing it's universe
- context in the environmnent of usage. For non-universe-polymorphic
- constants, it does not matter. *)
-val constr_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t
-
(** {6 Miscellaneous. } *)
(** Check that hyps are included in env and fails with error otherwise *)
diff --git a/kernel/uint63.mli b/kernel/uint63.mli
index b5f40ca804..f25f24512d 100644
--- a/kernel/uint63.mli
+++ b/kernel/uint63.mli
@@ -40,6 +40,10 @@ val rem : t -> t -> t
(* Specific arithmetic operations *)
val mulc : t -> t -> t * t
val addmuldiv : t -> t -> t -> t
+
+(** [div21 xh xl y] returns [q % 2^63, r]
+ s.t. [xh * 2^63 + xl = q * y + r] and [r < y].
+ When [y] is [0], returns [0, 0]. *)
val div21 : t -> t -> t -> t * t
(* comparison *)
diff --git a/kernel/uint63_amd64.ml b/kernel/uint63_amd64.ml
index 010b594de8..2d4d685775 100644
--- a/kernel/uint63_amd64.ml
+++ b/kernel/uint63_amd64.ml
@@ -102,26 +102,35 @@ let le128 xh xl yh yl =
lt xh yh || (xh = yh && le xl yl)
(* division of two numbers by one *)
+(* precondition: y <> 0 *)
+(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *)
let div21 xh xl y =
let maskh = ref 0 in
let maskl = ref 1 in
let dh = ref 0 in
let dl = ref y in
let cmp = ref true in
- while !dh >= 0 && !cmp do
- cmp := lt128 !dh !dl xh xl;
+ (* n = ref 0 *)
+ (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *)
+ while !dh >= 0 && !cmp do (* dh >= 0 tests that dh highest bit is zero *)
(* We don't use addmuldiv below to avoid checks on 1 *)
dh := (!dh lsl 1) lor (!dl lsr (uint_size - 1));
dl := !dl lsl 1;
maskh := (!maskh lsl 1) lor (!maskl lsr (uint_size - 1));
- maskl := !maskl lsl 1
- done; (* mask = 2^N, d = 2^N * d, d >= x *)
+ maskl := !maskl lsl 1;
+ (* incr n *)
+ cmp := lt128 !dh !dl xh xl;
+ done; (* mask = 2^n, d = 2^n * y, 2 * d > x *)
let remh = ref xh in
let reml = ref xl in
- let quotient = ref 0 in
+ (* quotienth = ref 0 *)
+ let quotientl = ref 0 in
+ (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r,
+ mask = floor(2^n), d = mask * y, n >= -1 *)
while !maskh lor !maskl <> 0 do
if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *)
- quotient := !quotient lor !maskl;
+ (* quotienth := !quotienth lor !maskh *)
+ quotientl := !quotientl lor !maskl;
remh := if lt !reml !dl then !remh - !dh - 1 else !remh - !dh;
reml := !reml - !dl;
end;
@@ -129,8 +138,11 @@ let div21 xh xl y =
maskh := !maskh lsr 1;
dl := (!dl lsr 1) lor (!dh lsl (uint_size - 1));
dh := !dh lsr 1;
+ (* decr n *)
done;
- !quotient, !reml
+ !quotientl, !reml
+
+let div21 xh xl y = if y = 0 then 0, 0 else div21 xh xl y
(* exact multiplication *)
(* TODO: check that none of these additions could be a logical or *)
diff --git a/kernel/uint63_x86.ml b/kernel/uint63_x86.ml
index 461184c432..fa45c90241 100644
--- a/kernel/uint63_x86.ml
+++ b/kernel/uint63_x86.ml
@@ -94,26 +94,35 @@ let le128 xh xl yh yl =
lt xh yh || (xh = yh && le xl yl)
(* division of two numbers by one *)
+(* precondition: y <> 0 *)
+(* outputs: q % 2^63, r s.t. x = q * y + r, r < y *)
let div21 xh xl y =
let maskh = ref zero in
let maskl = ref one in
let dh = ref zero in
let dl = ref y in
let cmp = ref true in
- while le zero !dh && !cmp do
- cmp := lt128 !dh !dl xh xl;
+ (* n = ref 0 *)
+ (* loop invariant: mask = 2^n, d = mask * y, (2 * d <= x -> cmp), n >= 0 *)
+ while Int64.equal (l_sr !dh (of_int (uint_size - 1))) zero && !cmp do
(* We don't use addmuldiv below to avoid checks on 1 *)
dh := l_or (l_sl !dh one) (l_sr !dl (of_int (uint_size - 1)));
dl := l_sl !dl one;
maskh := l_or (l_sl !maskh one) (l_sr !maskl (of_int (uint_size - 1)));
- maskl := l_sl !maskl one
- done; (* mask = 2^N, d = 2^N * d, d >= x *)
+ maskl := l_sl !maskl one;
+ (* incr n *)
+ cmp := lt128 !dh !dl xh xl;
+ done; (* mask = 2^n, d = 2^n * d, 2 * d > x *)
let remh = ref xh in
let reml = ref xl in
- let quotient = ref zero in
+ (* quotienth = ref 0 *)
+ let quotientl = ref zero in
+ (* loop invariant: x = quotient * y + rem, y * 2^(n+1) > r,
+ mask = floor(2^n), d = mask * y, n >= -1 *)
while not (Int64.equal (l_or !maskh !maskl) zero) do
if le128 !dh !dl !remh !reml then begin (* if rem >= d, add one bit and subtract d *)
- quotient := l_or !quotient !maskl;
+ (* quotienth := !quotienth lor !maskh *)
+ quotientl := l_or !quotientl !maskl;
remh := if lt !reml !dl then sub (sub !remh !dh) one else sub !remh !dh;
reml := sub !reml !dl
end;
@@ -121,9 +130,11 @@ let div21 xh xl y =
maskh := l_sr !maskh one;
dl := l_or (l_sr !dl one) (l_sl !dh (of_int (uint_size - 1)));
dh := l_sr !dh one
+ (* decr n *)
done;
- !quotient, !reml
+ !quotientl, !reml
+let div21 xh xl y = if Int64.equal y zero then zero, zero else div21 xh xl y
(* exact multiplication *)
let mulc x y =
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8263c68bf5..b1bbc25fe6 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -231,18 +231,15 @@ module LMap = struct
module M = HMap.Make (Level)
include M
- let union l r =
- merge (fun _k l r ->
- match l, r with
- | Some _, _ -> l
- | _, _ -> r) l r
+ let lunion l r =
+ union (fun _k l _r -> Some l) l r
- let subst_union l r =
- merge (fun _k l r ->
+ let subst_union l r =
+ union (fun _k l r ->
match l, r with
- | Some (Some _), _ -> l
- | Some None, None -> l
- | _, _ -> r) l r
+ | Some _, _ -> Some l
+ | None, None -> Some l
+ | _, _ -> Some r) l r
let diff ext orig =
fold (fun u v acc ->
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 5543c35741..db178c4bb0 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -223,8 +223,8 @@ module LMap :
sig
include CMap.ExtS with type key = Level.t and module Set := LSet
- val union : 'a t -> 'a t -> 'a t
- (** [union x y] favors the bindings in the first map. *)
+ val lunion : 'a t -> 'a t -> 'a t
+ (** [lunion x y] favors the bindings in the first map. *)
val diff : 'a t -> 'a t -> 'a t
(** [diff x y] removes bindings from x that appear in y (whatever the value). *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 03:31:13 +0000