summaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/byterun/coq_fix_code.c2
-rw-r--r--kernel/byterun/coq_gc.h13
-rw-r--r--kernel/byterun/coq_instruct.h1
-rw-r--r--kernel/byterun/coq_interp.c79
-rw-r--r--kernel/byterun/coq_memory.c16
-rw-r--r--kernel/byterun/coq_values.c1
-rw-r--r--kernel/byterun/coq_values.h19
-rw-r--r--kernel/cbytecodes.ml251
-rw-r--r--kernel/cbytecodes.mli71
-rw-r--r--kernel/cbytegen.ml266
-rw-r--r--kernel/cbytegen.mli10
-rw-r--r--kernel/cemitcodes.ml35
-rw-r--r--kernel/cemitcodes.mli4
-rw-r--r--kernel/constr.ml54
-rw-r--r--kernel/constr.mli20
-rw-r--r--kernel/conv_oracle.ml15
-rw-r--r--kernel/csymtable.ml44
-rw-r--r--kernel/declarations.mli21
-rw-r--r--kernel/declareops.ml18
-rw-r--r--kernel/declareops.mli12
-rw-r--r--kernel/entries.mli25
-rw-r--r--kernel/environ.ml59
-rw-r--r--kernel/environ.mli13
-rw-r--r--kernel/fast_typeops.ml8
-rw-r--r--kernel/indtypes.ml109
-rw-r--r--kernel/indtypes.mli2
-rw-r--r--kernel/inductive.ml105
-rw-r--r--kernel/mod_subst.ml2
-rw-r--r--kernel/mod_subst.mli5
-rw-r--r--kernel/mod_typing.ml119
-rw-r--r--kernel/mod_typing.mli13
-rw-r--r--kernel/modops.ml12
-rw-r--r--kernel/modops.mli3
-rw-r--r--kernel/names.ml36
-rw-r--r--kernel/names.mli4
-rw-r--r--kernel/nativecode.ml32
-rw-r--r--kernel/nativecode.mli26
-rw-r--r--kernel/nativeconv.ml136
-rw-r--r--kernel/nativeconv.mli4
-rw-r--r--kernel/nativelambda.ml38
-rw-r--r--kernel/nativelambda.mli2
-rw-r--r--kernel/nativelib.ml28
-rw-r--r--kernel/nativelibrary.ml4
-rw-r--r--kernel/nativelibrary.mli2
-rw-r--r--kernel/nativevalues.ml2
-rw-r--r--kernel/opaqueproof.ml5
-rw-r--r--kernel/pre_env.ml6
-rw-r--r--kernel/pre_env.mli3
-rw-r--r--kernel/reduction.ml58
-rw-r--r--kernel/reduction.mli27
-rw-r--r--kernel/safe_typing.ml278
-rw-r--r--kernel/safe_typing.mli61
-rw-r--r--kernel/sorts.ml10
-rw-r--r--kernel/subtyping.ml13
-rw-r--r--kernel/term.ml28
-rw-r--r--kernel/term.mli31
-rw-r--r--kernel/term_typing.ml302
-rw-r--r--kernel/term_typing.mli41
-rw-r--r--kernel/typeops.ml26
-rw-r--r--kernel/univ.ml235
-rw-r--r--kernel/univ.mli21
-rw-r--r--kernel/vars.ml4
-rw-r--r--kernel/vars.mli2
-rw-r--r--kernel/vconv.ml191
-rw-r--r--kernel/vconv.mli10
-rw-r--r--kernel/vm.ml305
-rw-r--r--kernel/vm.mli25
67 files changed, 2052 insertions, 1371 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 1be3e651..29e33d34 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -60,7 +60,7 @@ void init_arity () {
arity[BRANCH]=arity[ISCONST]= 1;
/* instruction with two operands */
arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
- arity[ARECONST]=2;
+ arity[ARECONST]=arity[PROJ]=2;
/* instruction with four operands */
arity[MAKESWITCHBLOCK]=4;
/* instruction with arbitrary operands */
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index c7b18b90..f0627586 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -12,6 +12,7 @@
#define _COQ_CAML_GC_
#include <caml/mlvalues.h>
#include <caml/alloc.h>
+#include <caml/memory.h>
typedef void (*scanning_action) (value, value *);
@@ -24,12 +25,22 @@ CAMLextern void minor_collection (void);
#define Caml_white (0 << 8)
#define Caml_black (3 << 8)
+#ifdef HAS_OCP_MEMPROF
+
+/* This code is necessary to make the OCamlPro memory profiling branch of
+ OCaml compile. */
+
+#define Make_header(wosize, tag, color) \
+ caml_make_header(wosize, tag, color)
+
+#else
+
#define Make_header(wosize, tag, color) \
(((header_t) (((header_t) (wosize) << 10) \
+ (color) \
+ (tag_t) (tag))) \
)
-
+#endif
#define Alloc_small(result, wosize, tag) do{ \
young_ptr -= Bhsize_wosize (wosize); \
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 9cbf4077..8c5ab0ec 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -36,6 +36,7 @@ enum instructions {
SWITCH, PUSHFIELDS,
GETFIELD0, GETFIELD1, GETFIELD,
SETFIELD0, SETFIELD1, SETFIELD,
+ PROJ,
CONST0, CONST1, CONST2, CONST3, CONSTINT,
PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
ACCUMULATE,
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0ab9f89f..dc571699 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -77,9 +77,11 @@ sp is a local copy of the global variable extern_sp. */
#ifdef _COQ_DEBUG_
# define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s)
# define print_int(i) /*if (drawinstr)*/ printf("%d\n",i)
+# define print_lint(i) /*if (drawinstr)*/ printf("%ld\n",i)
# else
# define print_instr(s)
# define print_int(i)
+# define print_lint(i)
#endif
/* GC interface */
@@ -339,6 +341,7 @@ value coq_interprete
/* Fallthrough */
Instruct(ENVACC){
print_instr("ENVACC");
+ print_int(*pc);
accu = Field(coq_env, *pc++);
Next;
}
@@ -369,6 +372,10 @@ value coq_interprete
sp[1] = (value)pc;
sp[2] = coq_env;
sp[3] = Val_long(coq_extra_args);
+ print_instr("call stack=");
+ print_lint(sp[1]);
+ print_lint(sp[2]);
+ print_lint(sp[3]);
pc = Code_val(accu);
coq_env = accu;
coq_extra_args = 0;
@@ -456,6 +463,7 @@ value coq_interprete
sp[0] = arg1;
sp[1] = arg2;
pc = Code_val(accu);
+ print_lint(accu);
coq_env = accu;
coq_extra_args += 1;
goto check_stacks;
@@ -479,11 +487,18 @@ value coq_interprete
print_instr("RETURN");
print_int(*pc);
sp += *pc++;
+ print_instr("stack=");
+ print_lint(sp[0]);
+ print_lint(sp[1]);
+ print_lint(sp[2]);
if (coq_extra_args > 0) {
+ print_instr("extra args > 0");
+ print_lint(coq_extra_args);
coq_extra_args--;
pc = Code_val(accu);
coq_env = accu;
} else {
+ print_instr("extra args = 0");
pc = (code_t)(sp[0]);
coq_env = sp[1];
coq_extra_args = Long_val(sp[2]);
@@ -583,7 +598,10 @@ value coq_interprete
Alloc_small(accu, 1 + nvars, Closure_tag);
Code_val(accu) = pc + *pc;
pc++;
- for (i = 0; i < nvars; i++) Field(accu, i + 1) = sp[i];
+ for (i = 0; i < nvars; i++) {
+ print_lint(sp[i]);
+ Field(accu, i + 1) = sp[i];
+ }
sp += nvars;
Next;
}
@@ -718,6 +736,7 @@ value coq_interprete
/* Fallthrough */
Instruct(GETGLOBAL){
print_instr("GETGLOBAL");
+ print_int(*pc);
accu = Field(coq_global_data, *pc);
pc++;
Next;
@@ -730,7 +749,7 @@ value coq_interprete
tag_t tag = *pc++;
mlsize_t i;
value block;
- print_instr("MAKEBLOCK");
+ print_instr("MAKEBLOCK, tag=");
Alloc_small(block, wosize, tag);
Field(block, 0) = accu;
for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
@@ -741,7 +760,8 @@ value coq_interprete
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK1");
+ print_instr("MAKEBLOCK1, tag=");
+ print_int(tag);
Alloc_small(block, 1, tag);
Field(block, 0) = accu;
accu = block;
@@ -751,7 +771,8 @@ value coq_interprete
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK2");
+ print_instr("MAKEBLOCK2, tag=");
+ print_int(tag);
Alloc_small(block, 2, tag);
Field(block, 0) = accu;
Field(block, 1) = sp[0];
@@ -762,7 +783,8 @@ value coq_interprete
Instruct(MAKEBLOCK3) {
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK3");
+ print_instr("MAKEBLOCK3, tag=");
+ print_int(tag);
Alloc_small(block, 3, tag);
Field(block, 0) = accu;
Field(block, 1) = sp[0];
@@ -774,7 +796,8 @@ value coq_interprete
Instruct(MAKEBLOCK4) {
tag_t tag = *pc++;
value block;
- print_instr("MAKEBLOCK4");
+ print_instr("MAKEBLOCK4, tag=");
+ print_int(tag);
Alloc_small(block, 4, tag);
Field(block, 0) = accu;
Field(block, 1) = sp[0];
@@ -795,12 +818,12 @@ value coq_interprete
if (Is_block(accu)) {
long index = Tag_val(accu);
print_instr("block");
- print_int(index);
+ print_lint(index);
pc += pc[(sizes & 0xFFFFFF) + index];
} else {
long index = Long_val(accu);
print_instr("constant");
- print_int(index);
+ print_lint(index);
pc += pc[index];
}
Next;
@@ -842,7 +865,6 @@ value coq_interprete
}
Instruct(SETFIELD1){
- int i, j, size, size_aux;
print_instr("SETFIELD1");
caml_modify(&Field(accu, 1),*sp);
sp++;
@@ -876,8 +898,30 @@ value coq_interprete
caml_modify(&Field(accu, *pc),*sp);
sp++; pc++;
Next;
- }
-
+ }
+
+
+ Instruct(PROJ){
+ print_instr("PROJ");
+ if (Is_accu (accu)) {
+ value block;
+ /* Skip over the index of projected field */
+ pc++;
+ /* Create atom */
+ Alloc_small(block, 2, ATOM_PROJ_TAG);
+ Field(block, 0) = Field(coq_global_data, *pc);
+ Field(block, 1) = accu;
+ /* Create accumulator */
+ Alloc_small(accu, 2, Accu_tag);
+ Code_val(accu) = accumulate;
+ Field(accu, 1) = block;
+ } else {
+ accu = Field(accu, *pc++);
+ }
+ pc++;
+ Next;
+ }
+
/* Integer constants */
Instruct(CONST0){
@@ -917,6 +961,7 @@ value coq_interprete
/* Fallthrough */
Instruct(CONSTINT) {
print_instr("CONSTINT");
+ print_int(*pc);
accu = Val_int(*pc);
pc++;
Next;
@@ -957,7 +1002,7 @@ value coq_interprete
sp -= nargs;
for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
*--sp = accu;
- print_int(nargs);
+ print_lint(nargs);
coq_extra_args = nargs;
pc = Code_val(coq_env);
goto check_stacks;
@@ -1084,7 +1129,6 @@ value coq_interprete
/* returns the sum plus one with a carry */
uint32_t s;
s = (uint32_t)accu + (uint32_t)*sp++ + 1;
- value block;
if( (uint32_t)s <= (uint32_t)accu ) {
/* carry */
Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
@@ -1226,16 +1270,17 @@ value coq_interprete
shiftby = uint32_of_value(accu);
if (shiftby > 31) {
if (shiftby < 62) {
- *sp++;
- accu = (value)((((*sp++)^1) << (shiftby - 31)) | 1);
+ sp++;
+ accu = (value)(((((uint32_t)*sp++)^1) << (shiftby - 31)) | 1);
}
else {
+ sp+=2;
accu = (value)(1);
}
}
else{
/* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */
- accu = (value)(((*sp++)^1) << shiftby);
+ accu = (value)((((uint32_t)*sp++)^1) << shiftby);
/* accu = 2^(shiftby+1)*x --> 2^(shifby+1)*x+2*y/2^(31-shiftby)+1 */
accu = (value)((accu | (((uint32_t)(*sp++)) >> (31-shiftby)))|1);
}
@@ -1244,7 +1289,7 @@ value coq_interprete
Instruct (COMPAREINT31) {
/* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
- /* assumes Inudctive _ : _ := Eq | Lt | Gt */
+ /* assumes Inductive _ : _ := Eq | Lt | Gt */
print_instr("COMPAREINT31");
if ((uint32_t)accu == (uint32_t)*sp) {
accu = 1; /* 2*0+1 */
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 8d03829a..c9bcdc32 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -26,7 +26,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size;
value coq_global_data;
-int coq_all_transp;
value coq_atom_tbl;
int drawinstr;
@@ -104,7 +103,6 @@ static int coq_vm_initialized = 0;
value init_coq_vm(value unit) /* ML */
{
- int i;
if (coq_vm_initialized == 1) {
fprintf(stderr,"already open \n");fflush(stderr);}
else {
@@ -117,7 +115,6 @@ value init_coq_vm(value unit) /* ML */
init_coq_global_data(Coq_global_data_Size);
init_coq_atom_tbl(40);
/* Initialing the interpreter */
- coq_all_transp = 0;
init_coq_interpreter();
/* Some predefined pointer code */
@@ -137,7 +134,6 @@ void realloc_coq_stack(asize_t required_space)
{
asize_t size;
value * new_low, * new_high, * new_sp;
- value * p;
size = coq_stack_high - coq_stack_low;
do {
size *= 2;
@@ -207,18 +203,6 @@ value realloc_coq_atom_tbl(value size) /* ML */
return Val_unit;
}
-
-value coq_set_transp_value(value transp)
-{
- coq_all_transp = (transp == Val_true);
- return Val_unit;
-}
-
-value get_coq_transp_value(value unit)
-{
- return Val_bool(coq_all_transp);
-}
-
value coq_set_drawinstr(value unit)
{
drawinstr = 1;
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 007f61b2..528babeb 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -21,7 +21,6 @@
value coq_kind_of_closure(value v) {
opcode_t * c;
- int res;
int is_app = 0;
c = Code_val(v);
if (Is_instruction(c, GRAB)) return Val_int(0);
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 1bf493e2..bb0f0eb5 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -17,22 +17,17 @@
#define Default_tag 0
#define Accu_tag 0
-
-
#define ATOM_ID_TAG 0
-#define ATOM_IDDEF_TAG 1
-#define ATOM_INDUCTIVE_TAG 2
-#define ATOM_FIX_TAG 3
-#define ATOM_SWITCH_TAG 4
-#define ATOM_COFIX_TAG 5
-#define ATOM_COFIXEVALUATED_TAG 6
-
-
+#define ATOM_INDUCTIVE_TAG 1
+#define ATOM_TYPE_TAG 2
+#define ATOM_PROJ_TAG 3
+#define ATOM_FIX_TAG 4
+#define ATOM_SWITCH_TAG 5
+#define ATOM_COFIX_TAG 6
+#define ATOM_COFIXEVALUATED_TAG 7
/* Les blocs accumulate */
#define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
#define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
#endif /* _COQ_VALUES_ */
-
-
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 700de502..0a24a75d 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -17,23 +17,28 @@ open Term
type tag = int
-let id_tag = 0
-let iddef_tag = 1
-let ind_tag = 2
-let fix_tag = 3
-let switch_tag = 4
-let cofix_tag = 5
-let cofix_evaluated_tag = 6
-(* It could be greate if OCaml export this value,
- So fixme if this occur in a new version of OCaml *)
+let accu_tag = 0
+
+let type_atom_tag = 2
+let max_atom_tag = 2
+let proj_tag = 3
+let fix_app_tag = 4
+let switch_tag = 5
+let cofix_tag = 6
+let cofix_evaluated_tag = 7
+
+(* It would be great if OCaml exported this value,
+ So fixme if this happens in a new version of OCaml *)
let last_variant_tag = 245
type structured_constant =
| Const_sorts of sorts
- | Const_ind of pinductive
+ | Const_ind of inductive
+ | Const_proj of Constant.t
| Const_b0 of tag
| Const_bn of tag * structured_constant array
-
+ | Const_univ_level of Univ.universe_level
+ | Const_type of Univ.universe
type reloc_table = (tag * int) array
@@ -58,29 +63,30 @@ type instruction =
| Kpush
| Kpop of int
| Kpush_retaddr of Label.t
- | Kapply of int (* number of arguments *)
- | Kappterm of int * int (* number of arguments, slot size *)
- | Kreturn of int (* slot size *)
+ | Kapply of int
+ | Kappterm of int * int
+ | Kreturn of int
| Kjump
| Krestart
- | Kgrab of int (* number of arguments *)
- | Kgrabrec of int (* rec arg *)
- | Kclosure of Label.t * int (* label, number of free variables *)
+ | Kgrab of int
+ | Kgrabrec of int
+ | Kclosure of Label.t * int
| Kclosurerec of int * int * Label.t array * Label.t array
- (* nb fv, init, lbl types, lbl bodies *)
| Kclosurecofix of int * int * Label.t array * Label.t array
(* nb fv, init, lbl types, lbl bodies *)
- | Kgetglobal of pconstant
+ | Kgetglobal of constant
| Kconst of structured_constant
- | Kmakeblock of int * tag (* size, tag *)
+ | Kmakeblock of int * tag
| Kmakeprod
| Kmakeswitchblock of Label.t * Label.t * annot_switch * int
- | Kswitch of Label.t array * Label.t array (* consts,blocks *)
+ | Kswitch of Label.t array * Label.t array
| Kpushfields of int
| Kfield of int
| Ksetfield of int
| Kstop
| Ksequence of bytecodes * bytecodes
+ | Kproj of int * Constant.t (* index of the projected argument,
+ name of projection *)
(* spiwack: instructions concerning integers *)
| Kbranch of Label.t (* jump to label *)
| Kaddint31 (* adds the int31 in the accu
@@ -124,7 +130,10 @@ type instruction =
and bytecodes = instruction list
-type fv_elem = FVnamed of Id.t | FVrel of int
+type fv_elem =
+ | FVnamed of Id.t
+ | FVrel of int
+ | FVuniv_var of int
type fv = fv_elem array
@@ -142,105 +151,138 @@ type vm_env = {
type comp_env = {
- nb_stack : int; (* nbre de variables sur la pile *)
- in_stack : int list; (* position dans la pile *)
- nb_rec : int; (* nbre de fonctions mutuellement *)
- (* recursives = nbr *)
+ nb_uni_stack : int ; (* number of universes on the stack, *)
+ (* universes are always at the bottom. *)
+ nb_stack : int; (* number of variables on the stack *)
+ in_stack : int list; (* position in the stack *)
+ nb_rec : int; (* number of mutually recursive functions *)
pos_rec : instruction list; (* instruction d'acces pour les variables *)
(* de point fix ou de cofix *)
offset : int;
- in_env : vm_env ref
+ in_env : vm_env ref (* The free variables of the expression *)
}
+(* --- Pretty print *)
+open Pp
+open Util
+let pp_sort s =
+ match family_of_sort s with
+ | InSet -> str "Set"
+ | InProp -> str "Prop"
+ | InType -> str "Type"
-(* --- Pretty print *)
-open Format
-let rec instruction ppf = function
- | Klabel lbl -> fprintf ppf "L%i:" lbl
- | Kacc n -> fprintf ppf "\tacc %i" n
- | Kenvacc n -> fprintf ppf "\tenvacc %i" n
- | Koffsetclosure n -> fprintf ppf "\toffsetclosure %i" n
- | Kpush -> fprintf ppf "\tpush"
- | Kpop n -> fprintf ppf "\tpop %i" n
- | Kpush_retaddr lbl -> fprintf ppf "\tpush_retaddr L%i" lbl
- | Kapply n -> fprintf ppf "\tapply %i" n
+let rec pp_struct_const = function
+ | Const_sorts s -> pp_sort s
+ | Const_ind (mind, i) -> pr_mind mind ++ str"#" ++ int i
+ | Const_proj p -> Constant.print p
+ | Const_b0 i -> int i
+ | Const_bn (i,t) ->
+ int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)
+ | Const_univ_level l -> Univ.Level.pr l
+ | Const_type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}"
+
+let pp_lbl lbl = str "L" ++ int lbl
+
+let pp_pcon (id,u) =
+ pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}"
+
+let pp_fv_elem = function
+ | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")"
+ | FVrel i -> str "Rel(" ++ int i ++ str ")"
+ | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")"
+
+let rec pp_instr i =
+ match i with
+ | Klabel _ | Ksequence _ -> assert false
+ | Kacc n -> str "acc " ++ int n
+ | Kenvacc n -> str "envacc " ++ int n
+ | Koffsetclosure n -> str "offsetclosure " ++ int n
+ | Kpush -> str "push"
+ | Kpop n -> str "pop " ++ int n
+ | Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl
+ | Kapply n -> str "apply " ++ int n
| Kappterm(n, m) ->
- fprintf ppf "\tappterm %i, %i" n m
- | Kreturn n -> fprintf ppf "\treturn %i" n
- | Kjump -> fprintf ppf "\tjump"
- | Krestart -> fprintf ppf "\trestart"
- | Kgrab n -> fprintf ppf "\tgrab %i" n
- | Kgrabrec n -> fprintf ppf "\tgrabrec %i" n
+ str "appterm " ++ int n ++ str ", " ++ int m
+ | Kreturn n -> str "return " ++ int n
+ | Kjump -> str "jump"
+ | Krestart -> str "restart"
+ | Kgrab n -> str "grab " ++ int n
+ | Kgrabrec n -> str "grabrec " ++ int n
| Kclosure(lbl, n) ->
- fprintf ppf "\tclosure L%i, %i" lbl n
+ str "closure " ++ pp_lbl lbl ++ str ", " ++ int n
| Kclosurerec(fv,init,lblt,lblb) ->
- fprintf ppf "\tclosurerec";
- fprintf ppf "%i , %i, " fv init;
- print_string "types = ";
- Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
- print_string " bodies = ";
- Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
+ h 1 (str "closurerec " ++
+ int fv ++ str ", " ++ int init ++
+ str " types = " ++
+ prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
+ str " bodies = " ++
+ prlist_with_sep spc pp_lbl (Array.to_list lblb))
| Kclosurecofix (fv,init,lblt,lblb) ->
- fprintf ppf "\tclosurecofix";
- fprintf ppf " %i , %i, " fv init;
- print_string "types = ";
- Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
- print_string " bodies = ";
- Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
- | Kgetglobal (id,u) -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
- | Kconst cst ->
- fprintf ppf "\tconst"
+ h 1 (str "closurecofix " ++
+ int fv ++ str ", " ++ int init ++
+ str " types = " ++
+ prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
+ str " bodies = " ++
+ prlist_with_sep spc pp_lbl (Array.to_list lblb))
+ | Kgetglobal idu -> str "getglobal " ++ pr_con idu
+ | Kconst sc ->
+ str "const " ++ pp_struct_const sc
| Kmakeblock(n, m) ->
- fprintf ppf "\tmakeblock %i, %i" n m
- | Kmakeprod -> fprintf ppf "\tmakeprod"
+ str "makeblock " ++ int n ++ str ", " ++ int m
+ | Kmakeprod -> str "makeprod"
| Kmakeswitchblock(lblt,lbls,_,sz) ->
- fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz
+ str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++
+ pp_lbl lbls ++ str ", " ++ int sz
| Kswitch(lblc,lblb) ->
- fprintf ppf "\tswitch";
- Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc;
- Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
- | Kpushfields n -> fprintf ppf "\tpushfields %i" n
- | Ksetfield n -> fprintf ppf "\tsetfield %i" n
- | Kfield n -> fprintf ppf "\tgetfield %i" n
- | Kstop -> fprintf ppf "\tstop"
- | Ksequence (c1,c2) ->
- fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2
-(* spiwack *)
- | Kbranch lbl -> fprintf ppf "\tbranch %i" lbl
- | Kaddint31 -> fprintf ppf "\taddint31"
- | Kaddcint31 -> fprintf ppf "\taddcint31"
- | Kaddcarrycint31 -> fprintf ppf "\taddcarrycint31"
- | Ksubint31 -> fprintf ppf "\tsubint31"
- | Ksubcint31 -> fprintf ppf "\tsubcint31"
- | Ksubcarrycint31 -> fprintf ppf "\tsubcarrycint31"
- | Kmulint31 -> fprintf ppf "\tmulint31"
- | Kmulcint31 -> fprintf ppf "\tmulcint31"
- | Kdiv21int31 -> fprintf ppf "\tdiv21int31"
- | Kdivint31 -> fprintf ppf "\tdivint31"
- | Kcompareint31 -> fprintf ppf "\tcompareint31"
- | Khead0int31 -> fprintf ppf "\thead0int31"
- | Ktail0int31 -> fprintf ppf "\ttail0int31"
- | Kaddmuldivint31 -> fprintf ppf "\taddmuldivint31"
- | Kisconst lbl -> fprintf ppf "\tisconst %i" lbl
- | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl
- | Kcompint31 -> fprintf ppf "\tcompint31"
- | Kdecompint31 -> fprintf ppf "\tdecompint"
- | Klorint31 -> fprintf ppf "\tlorint31"
- | Klandint31 -> fprintf ppf "\tlandint31"
- | Klxorint31 -> fprintf ppf "\tlxorint31"
+ h 1 (str "switch " ++
+ prlist_with_sep spc pp_lbl (Array.to_list lblc) ++
+ str " | " ++
+ prlist_with_sep spc pp_lbl (Array.to_list lblb))
+ | Kpushfields n -> str "pushfields " ++ int n
+ | Kfield n -> str "field " ++ int n
+ | Ksetfield n -> str "set field" ++ int n
-(* /spiwack *)
+ | Kstop -> str "stop"
+
+ | Kbranch lbl -> str "branch " ++ pp_lbl lbl
+ | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p
-and instruction_list ppf = function
- [] -> ()
- | Klabel lbl :: il ->
- fprintf ppf "L%i:%a" lbl instruction_list il
- | instr :: il ->
- fprintf ppf "%a@ %a" instruction instr instruction_list il
+ | Kaddint31 -> str "addint31"
+ | Kaddcint31 -> str "addcint31"
+ | Kaddcarrycint31 -> str "addcarrycint31"
+ | Ksubint31 -> str "subint31"
+ | Ksubcint31 -> str "subcint31"
+ | Ksubcarrycint31 -> str "subcarrycint31"
+ | Kmulint31 -> str "mulint31"
+ | Kmulcint31 -> str "mulcint31"
+ | Kdiv21int31 -> str "div21int31"
+ | Kdivint31 -> str "divint31"
+ | Kcompareint31 -> str "compareint31"
+ | Khead0int31 -> str "head0int31"
+ | Ktail0int31 -> str "tail0int31"
+ | Kaddmuldivint31 -> str "addmuldivint31"
+ | Kisconst lbl -> str "isconst " ++ int lbl
+ | Kareconst(n,lbl) -> str "areconst " ++ int n ++ spc () ++ int lbl
+ | Kcompint31 -> str "compint31"
+ | Kdecompint31 -> str "decompint"
+ | Klorint31 -> str "lorint31"
+ | Klandint31 -> str "landint31"
+ | Klxorint31 -> str "lxorint31"
+and pp_bytecodes c =
+ match c with
+ | [] -> str ""
+ | Klabel lbl :: c ->
+ str "L" ++ int lbl ++ str ":" ++ fnl () ++
+ pp_bytecodes c
+ | Ksequence (l1, l2) :: c ->
+ pp_bytecodes l1 ++ pp_bytecodes l2 ++ pp_bytecodes c
+ | i :: c ->
+ tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c
+
(*spiwack: moved this type in this file because I needed it for
retroknowledge which can't depend from cbytegen *)
type block =
@@ -253,8 +295,3 @@ type block =
(* spiwack: compilation given by a function *)
(* compilation function (see get_vm_constant_dynamic_info in
retroknowledge.mli for more info) , argument array *)
-
-
-
-let draw_instr c =
- fprintf std_formatter "@[<v 0>%a@]" instruction_list c
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index fbb40ffd..03ae6b9c 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -13,20 +13,28 @@ open Term
type tag = int
-val id_tag : tag
-val iddef_tag : tag
-val ind_tag : tag
-val fix_tag : tag
+val accu_tag : tag
+
+val type_atom_tag : tag
+val max_atom_tag : tag
+val proj_tag : tag
+val fix_app_tag : tag
val switch_tag : tag
val cofix_tag : tag
val cofix_evaluated_tag : tag
-val last_variant_tag : tag
+
+val last_variant_tag : tag
type structured_constant =
| Const_sorts of sorts
- | Const_ind of pinductive
+ | Const_ind of inductive
+ | Const_proj of Constant.t
| Const_b0 of tag
| Const_bn of tag * structured_constant array
+ | Const_univ_level of Univ.universe_level
+ | Const_type of Univ.universe
+
+val pp_struct_const : structured_constant -> Pp.std_ppcmds
type reloc_table = (tag * int) array
@@ -43,13 +51,13 @@ module Label :
type instruction =
| Klabel of Label.t
- | Kacc of int
- | Kenvacc of int
- | Koffsetclosure of int
- | Kpush
- | Kpop of int
- | Kpush_retaddr of Label.t
- | Kapply of int (** number of arguments *)
+ | Kacc of int (** accu = sp[n] *)
+ | Kenvacc of int (** accu = coq_env[n] *)
+ | Koffsetclosure of int (** accu = &coq_env[n] *)
+ | Kpush (** sp = accu :: sp *)
+ | Kpop of int (** sp = skipn n sp *)
+ | Kpush_retaddr of Label.t (** sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0 *)
+ | Kapply of int (** number of arguments (arguments on top of stack) *)
| Kappterm of int * int (** number of arguments, slot size *)
| Kreturn of int (** slot size *)
| Kjump
@@ -61,17 +69,21 @@ type instruction =
(** nb fv, init, lbl types, lbl bodies *)
| Kclosurecofix of int * int * Label.t array * Label.t array
(** nb fv, init, lbl types, lbl bodies *)
- | Kgetglobal of pconstant
+ | Kgetglobal of constant
| Kconst of structured_constant
- | Kmakeblock of int * tag (** size, tag *)
+ | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0
+ ** is accu, all others are popped from
+ ** the top of the stack *)
| Kmakeprod
| Kmakeswitchblock of Label.t * Label.t * annot_switch * int
| Kswitch of Label.t array * Label.t array (** consts,blocks *)
| Kpushfields of int
- | Kfield of int
- | Ksetfield of int
+ | Kfield of int (** accu = accu[n] *)
+ | Ksetfield of int (** accu[n] = sp[0] ; sp = pop sp *)
| Kstop
| Ksequence of bytecodes * bytecodes
+ | Kproj of int * Constant.t (** index of the projected argument,
+ name of projection *)
(** spiwack: instructions concerning integers *)
| Kbranch of Label.t (** jump to label, is it needed ? *)
@@ -115,7 +127,10 @@ type instruction =
and bytecodes = instruction list
-type fv_elem = FVnamed of Id.t | FVrel of int
+type fv_elem =
+ FVnamed of Id.t
+| FVrel of int
+| FVuniv_var of int
type fv = fv_elem array
@@ -124,28 +139,28 @@ type fv = fv_elem array
closed terms. *)
exception NotClosed
-(*spiwack: both type have been moved from Cbytegen because I needed then
+(*spiwack: both type have been moved from Cbytegen because I needed them
for the retroknowledge *)
type vm_env = {
- size : int; (** longueur de la liste [n] *)
+ size : int; (** length of the list [n] *)
fv_rev : fv_elem list (** [fvn; ... ;fv1] *)
}
type comp_env = {
- nb_stack : int; (** nbre de variables sur la pile *)
- in_stack : int list; (** position dans la pile *)
- nb_rec : int; (** nbre de fonctions mutuellement *)
- (** recursives = nbr *)
+ nb_uni_stack : int ; (** number of universes on the stack *)
+ nb_stack : int; (** number of variables on the stack *)
+ in_stack : int list; (** position in the stack *)
+ nb_rec : int; (** number of mutually recursive functions *)
+ (** (= nbr) *)
pos_rec : instruction list; (** instruction d'acces pour les variables *)
(** de point fix ou de cofix *)
offset : int;
- in_env : vm_env ref
+ in_env : vm_env ref (** the variables that are accessed *)
}
-val draw_instr : bytecodes -> unit
-
-
+val pp_bytecodes : bytecodes -> Pp.std_ppcmds
+val pp_fv_elem : fv_elem -> Pp.std_ppcmds
(*spiwack: moved this here because I needed it for retroknowledge *)
type block =
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 07fab06a..1f7cc3c7 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -91,18 +91,20 @@ open Pre_env
(* In Cfxe_t accumulators, we need to store [fcofixi] for testing *)
(* conversion of cofixpoints (which is intentional). *)
+type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t
let empty_fv = { size= 0; fv_rev = [] }
let fv r = !(r.in_env)
-let empty_comp_env ()=
- { nb_stack = 0;
+let empty_comp_env ?(univs=0) ()=
+ { nb_uni_stack = univs;
+ nb_stack = 0;
in_stack = [];
nb_rec = 0;
pos_rec = [];
offset = 0;
- in_env = ref empty_fv;
+ in_env = ref empty_fv
}
(*i Creation functions for comp_env *)
@@ -110,8 +112,9 @@ let empty_comp_env ()=
let rec add_param n sz l =
if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l)
-let comp_env_fun arity =
- { nb_stack = arity;
+let comp_env_fun ?(univs=0) arity =
+ { nb_uni_stack = univs ;
+ nb_stack = arity;
in_stack = add_param arity 0 [];
nb_rec = 0;
pos_rec = [];
@@ -120,8 +123,9 @@ let comp_env_fun arity =
}
-let comp_env_fix_type rfv =
- { nb_stack = 0;
+let comp_env_fix_type rfv =
+ { nb_uni_stack = 0;
+ nb_stack = 0;
in_stack = [];
nb_rec = 0;
pos_rec = [];
@@ -134,7 +138,8 @@ let comp_env_fix ndef curr_pos arity rfv =
for i = ndef downto 1 do
prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec
done;
- { nb_stack = arity;
+ { nb_uni_stack = 0;
+ nb_stack = arity;
in_stack = add_param arity 0 [];
nb_rec = ndef;
pos_rec = !prec;
@@ -143,7 +148,8 @@ let comp_env_fix ndef curr_pos arity rfv =
}
let comp_env_cofix_type ndef rfv =
- { nb_stack = 0;
+ { nb_uni_stack = 0;
+ nb_stack = 0;
in_stack = [];
nb_rec = 0;
pos_rec = [];
@@ -156,7 +162,8 @@ let comp_env_cofix ndef arity rfv =
for i = 1 to ndef do
prec := Kenvacc i :: !prec
done;
- { nb_stack = arity;
+ { nb_uni_stack = 0;
+ nb_stack = arity;
in_stack = add_param arity 0 [];
nb_rec = ndef;
pos_rec = !prec;
@@ -168,7 +175,7 @@ let comp_env_cofix ndef arity rfv =
let push_param n sz r =
{ r with
nb_stack = r.nb_stack + n;
- in_stack = add_param n sz r.in_stack }
+ in_stack = add_param n (sz - r.nb_uni_stack) r.in_stack }
(* [push_local sz r] add a new variable on the stack at position [sz] *)
let push_local sz r =
@@ -176,8 +183,6 @@ let push_local sz r =
nb_stack = r.nb_stack + 1;
in_stack = (sz + 1) :: r.in_stack }
-
-
(*i Compilation of variables *)
let find_at f l =
let rec aux n = function
@@ -214,6 +219,22 @@ let pos_rel i r sz =
r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev};
Kenvacc(r.offset + pos)
+let pos_universe_var i r sz =
+ if i < r.nb_uni_stack then
+ Kacc (sz - r.nb_stack - (r.nb_uni_stack - i))
+ else
+ let env = !(r.in_env) in
+ let f = function
+ | FVuniv_var u -> Int.equal i u
+ | _ -> false
+ in
+ try Kenvacc (r.offset + env.size - (find_at f env.fv_rev))
+ with Not_found ->
+ let pos = env.size in
+ let db = FVuniv_var i in
+ r.in_env := { size = pos + 1; fv_rev = db::env.fv_rev } ;
+ Kenvacc(r.offset + pos)
+
(*i Examination of the continuation *)
(* Discard all instructions up to the next label. *)
@@ -459,8 +480,9 @@ let rec str_const c =
end
| _ -> Bconstr c
end
- | Ind ind -> Bstrconst (Const_ind ind)
- | Construct (((kn,j),i),u) ->
+ | Ind (ind,u) when Univ.Instance.is_empty u ->
+ Bstrconst (Const_ind ind)
+ | Construct (((kn,j),i),_) ->
begin
(* spiwack: tries first to apply the run-time compilation
behavior of the constructor, as in 2/ above *)
@@ -513,6 +535,7 @@ let compile_fv_elem reloc fv sz cont =
match fv with
| FVrel i -> pos_rel i reloc sz :: cont
| FVnamed id -> pos_named id reloc :: cont
+ | FVuniv_var i -> pos_universe_var i reloc sz :: cont
let rec compile_fv reloc l sz cont =
match l with
@@ -524,39 +547,71 @@ let rec compile_fv reloc l sz cont =
(* Compiling constants *)
-let rec get_allias env (kn,u as p) =
+let rec get_alias env kn =
let cb = lookup_constant kn env in
let tps = cb.const_body_code in
match tps with
- | None -> p
+ | None -> kn
| Some tps ->
(match Cemitcodes.force tps with
- | BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
- | _ -> p)
-
-(* Compiling expressions *)
+ | BCalias kn' -> get_alias env kn'
+ | _ -> kn)
+(* sz is the size of the local stack *)
let rec compile_constr reloc c sz cont =
match kind_of_term c with
| Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta"
| Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar"
- | Proj (p,c) ->
- (* compile_const reloc p [|c|] sz cont *)
- let kn = Projection.constant p in
- let cb = lookup_constant kn !global_env in
- (* TODO: better representation of projections *)
- let pb = Option.get cb.const_proj in
- let args = Array.make pb.proj_npars mkProp in
- compile_const reloc kn Univ.Instance.empty (Array.append args [|c|]) sz cont
+ | Proj (p,c) ->
+ let kn = Projection.constant p in
+ let cb = lookup_constant kn !global_env in
+ let pb = Option.get cb.const_proj in
+ let n = pb.proj_arg in
+ compile_constr reloc c sz (Kproj (n,kn) :: cont)
| Cast(c,_,_) -> compile_constr reloc c sz cont
| Rel i -> pos_rel i reloc sz :: cont
| Var id -> pos_named id reloc :: cont
| Const (kn,u) -> compile_const reloc kn u [||] sz cont
- | Sort _ | Ind _ | Construct _ ->
+ | Ind (ind,u) ->
+ let bcst = Bstrconst (Const_ind ind) in
+ if Univ.Instance.is_empty u then
+ compile_str_cst reloc bcst sz cont
+ else
+ comp_app compile_str_cst compile_universe reloc
+ bcst
+ (Univ.Instance.to_array u)
+ sz
+ cont
+ | Sort (Prop _) | Construct _ ->
compile_str_cst reloc (str_const c) sz cont
-
+ | Sort (Type u) ->
+ (* We separate global and local universes in [u]. The former will be part
+ of the structured constant, while the later (if any) will be applied as
+ arguments. *)
+ let open Univ in begin
+ let levels = Universe.levels u in
+ let global_levels =
+ LSet.filter (fun x -> Level.var_index x = None) levels
+ in
+ let local_levels =
+ List.map_filter (fun x -> Level.var_index x)
+ (LSet.elements levels)
+ in
+ (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *)
+ let uglob =
+ LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m
+ in
+ if local_levels = [] then
+ compile_str_cst reloc (Bstrconst (Const_sorts (Type uglob))) sz cont
+ else
+ let compile_get_univ reloc idx sz cont =
+ compile_fv_elem reloc (FVuniv_var idx) sz cont
+ in
+ comp_app compile_str_cst compile_get_univ reloc
+ (Bstrconst (Const_type u)) (Array.of_list local_levels) sz cont
+ end
| LetIn(_,xb,_,body) ->
compile_constr reloc xb sz
(Kpush ::
@@ -665,7 +720,9 @@ let rec compile_constr reloc c sz cont =
let lbl_sw = Label.create () in
let sz_b,branch,is_tailcall =
match branch1 with
- | Kreturn k -> assert (Int.equal k sz); sz, branch1, true
+ | Kreturn k ->
+ assert (Int.equal k sz) ;
+ sz, branch1, true
| _ -> sz+3, Kjump, false
in
let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in
@@ -747,8 +804,20 @@ and compile_str_cst reloc sc sz cont =
(* spiwack : compilation of constants with their arguments.
Makes a special treatment with 31-bit integer addition *)
-and compile_const =
- fun reloc-> fun kn u -> fun args -> fun sz -> fun cont ->
+and compile_get_global reloc (kn,u) sz cont =
+ let kn = get_alias !global_env kn in
+ if Univ.Instance.is_empty u then
+ Kgetglobal kn :: cont
+ else
+ comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
+ compile_universe reloc () (Univ.Instance.to_array u) sz cont
+
+and compile_universe reloc uni sz cont =
+ match Univ.Level.var_index uni with
+ | None -> Kconst (Const_univ_level uni) :: cont
+ | Some idx -> pos_universe_var idx reloc sz :: cont
+
+and compile_const reloc kn u args sz cont =
let nargs = Array.length args in
(* spiwack: checks if there is a specific way to compile the constant
if there is not, Not_found is raised, and the function
@@ -758,30 +827,85 @@ and compile_const =
(mkConstU (kn,u)) reloc args sz cont
with Not_found ->
if Int.equal nargs 0 then
- Kgetglobal (get_allias !global_env (kn, u)) :: cont
+ compile_get_global reloc (kn,u) sz cont
else
- comp_app (fun _ _ _ cont ->
- Kgetglobal (get_allias !global_env (kn,u)) :: cont)
- compile_constr reloc () args sz cont
-
-let compile fail_on_error env c =
+ if Univ.Instance.is_empty u then
+ (* normal compilation *)
+ comp_app (fun _ _ sz cont ->
+ compile_get_global reloc (kn,u) sz cont)
+ compile_constr reloc () args sz cont
+ else
+ let compile_arg reloc constr_or_uni sz cont =
+ match constr_or_uni with
+ | ArgConstr cst -> compile_constr reloc cst sz cont
+ | ArgUniv uni -> compile_universe reloc uni sz cont
+ in
+ let u = Univ.Instance.to_array u in
+ let lu = Array.length u in
+ let all =
+ Array.init (lu + Array.length args)
+ (fun i -> if i < lu then ArgUniv u.(i) else ArgConstr args.(i-lu))
+ in
+ comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
+ compile_arg reloc () all sz cont
+
+let is_univ_copy max u =
+ let u = Univ.Instance.to_array u in
+ if Array.length u = max then
+ Array.fold_left_i (fun i acc u ->
+ if acc then
+ match Univ.Level.var_index u with
+ | None -> false
+ | Some l -> l = i
+ else false) true u
+ else
+ false
+
+let dump_bytecodes init code fvs =
+ let open Pp in
+ (str "code =" ++ fnl () ++
+ pp_bytecodes init ++ fnl () ++
+ pp_bytecodes code ++ fnl () ++
+ str "fv = " ++
+ prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++
+ fnl ())
+
+let compile fail_on_error ?universes:(universes=0) env c =
set_global_env env;
init_fun_code ();
Label.reset_label_counter ();
- let reloc = empty_comp_env () in
- try
- let init_code = compile_constr reloc c 0 [Kstop] in
+ let cont = [Kstop] in
+ try
+ let reloc, init_code =
+ if Int.equal universes 0 then
+ let reloc = empty_comp_env () in
+ reloc, compile_constr reloc c 0 cont
+ else
+ (* We are going to generate a lambda, but merge the universe closure
+ * with the function closure if it exists.
+ *)
+ let reloc = empty_comp_env () in
+ let arity , body =
+ match kind_of_term c with
+ | Lambda _ ->
+ let params, body = decompose_lam c in
+ List.length params , body
+ | _ -> 0 , c
+ in
+ let full_arity = arity + universes in
+ let r_fun = comp_env_fun ~univs:universes arity in
+ let lbl_fun = Label.create () in
+ let cont_fun =
+ compile_constr r_fun body full_arity [Kreturn full_arity]
+ in
+ fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)];
+ let fv = fv r_fun in
+ reloc, compile_fv reloc fv.fv_rev 0 (Kclosure(lbl_fun,fv.size) :: cont)
+ in
let fv = List.rev (!(reloc.in_env).fv_rev) in
-(* draw_instr init_code;
- draw_instr !fun_code;
- Format.print_string "fv = ";
- List.iter (fun v ->
- match v with
- | FVnamed id -> Format.print_string ((Id.to_string id)^"; ")
- | FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv; Format
- .print_string "\n";
- Format.print_flush(); *)
- Some (init_code,!fun_code, Array.of_list fv)
+ (if !Flags.dump_bytecode then
+ Pp.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
+ Some (init_code,!fun_code, Array.of_list fv)
with TooLargeInductive tname ->
let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in
(Pp.(fn
@@ -789,28 +913,33 @@ let compile fail_on_error env c =
Id.print tname ++ str str_max_constructors));
None)
-let compile_constant_body fail_on_error env = function
+let compile_constant_body fail_on_error env univs = function
| Undef _ | OpaqueDef _ -> Some BCconstant
| Def sb ->
let body = Mod_subst.force_constr sb in
+ let instance_size =
+ match univs with
+ | None -> 0
+ | Some univ -> Univ.UContext.size univ
+ in
match kind_of_term body with
- | Const (kn',u) ->
+ | Const (kn',u) when is_univ_copy instance_size u ->
(* we use the canonical name of the constant*)
let con= constant_of_kn (canonical_con kn') in
- Some (BCallias (get_allias env (con,u)))
+ Some (BCalias (get_alias env con))
| _ ->
- let res = compile fail_on_error env body in
+ let res = compile fail_on_error ~universes:instance_size env body in
Option.map (fun x -> BCdefined (to_memory x)) res
(* Shortcut of the previous function used during module strengthening *)
-let compile_alias (kn,u) = BCallias (constant_of_kn (canonical_con kn), u)
+let compile_alias kn = BCalias (constant_of_kn (canonical_con kn))
(* spiwack: additional function which allow different part of compilation of the
31-bit integers *)
let make_areconst n else_lbl cont =
- if n <=0 then
+ if n <= 0 then
cont
else
Kareconst (n, else_lbl)::cont
@@ -867,7 +996,7 @@ let op2_compilation op =
Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
op:: Kreturn 0:: Klabel else_lbl::
(* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*)
- (*Kgetglobal (get_allias !global_env kn):: *)
+ (*Kgetglobal (get_alias !global_env kn):: *)
normal::
Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
in
@@ -886,7 +1015,7 @@ let op2_compilation op =
(*Kaddint31::escape::Klabel else_lbl::Kpush::*)
(op::escape::Klabel else_lbl::Kpush::
(* works as comp_app with nargs = 2 and non-tailcall cont*)
- (*Kgetglobal (get_allias !global_env kn):: *)
+ (*Kgetglobal (get_alias !global_env kn):: *)
normal::
Kapply 2::labeled_cont)))
else if nargs=0 then
@@ -900,16 +1029,16 @@ let op2_compilation op =
1/ checks if all the arguments are constants (i.e. non-block values)
2/ if they are, uses the "op" instruction to execute
3/ if at least one is not, branches to the normal behavior:
- Kgetglobal (get_allias !global_env kn) *)
+ Kgetglobal (get_alias !global_env kn) *)
let op_compilation n op =
- let code_construct kn cont =
+ let code_construct reloc kn sz cont =
let f_cont =
let else_lbl = Label.create () in
Kareconst(n, else_lbl):: Kacc 0:: Kpop 1::
op:: Kreturn 0:: Klabel else_lbl::
(* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*)
- Kgetglobal (get_allias !global_env kn)::
- Kappterm(n, n):: [] (* = discard_dead_code [Kreturn 0] *)
+ compile_get_global reloc kn sz (
+ Kappterm(n, n):: []) (* = discard_dead_code [Kreturn 0] *)
in
let lbl = Label.create () in
fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)];
@@ -926,12 +1055,11 @@ let op_compilation n op =
(*Kaddint31::escape::Klabel else_lbl::Kpush::*)
(op::escape::Klabel else_lbl::Kpush::
(* works as comp_app with nargs = n and non-tailcall cont*)
- Kgetglobal (get_allias !global_env kn)::
- Kapply n::labeled_cont)))
+ compile_get_global reloc kn sz (Kapply n::labeled_cont))))
else if Int.equal nargs 0 then
- code_construct kn cont
+ code_construct reloc kn sz cont
else
- comp_app (fun _ _ _ cont -> code_construct kn cont)
+ comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont)
compile_constr reloc () args sz cont
let int31_escape_before_match fc cont =
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 1128f0d0..c0f48641 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -4,17 +4,17 @@ open Term
open Declarations
open Pre_env
-
+(** Should only be used for monomorphic terms *)
val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *)
- env -> constr -> (bytecodes * bytecodes * fv) option
+ ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option
(** init, fun, fv *)
-val compile_constant_body : bool ->
- env -> constant_def -> body_code option
+val compile_constant_body : bool ->
+ env -> constant_universes option -> constant_def -> body_code option
(** Shortcut of the previous function used during module strengthening *)
-val compile_alias : pconstant -> body_code
+val compile_alias : Names.constant -> body_code
(** spiwack: this function contains the information needed to perform
the static compilation of int31 (trying and obtaining
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 2535a64d..ef0c9af4 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -19,7 +19,7 @@ open Mod_subst
type reloc_info =
| Reloc_annot of annot_switch
| Reloc_const of structured_constant
- | Reloc_getglobal of pconstant
+ | Reloc_getglobal of Names.constant
type patch = reloc_info * int
@@ -127,11 +127,11 @@ let slot_for_const c =
enter (Reloc_const c);
out_int 0
-and slot_for_annot a =
+let slot_for_annot a =
enter (Reloc_annot a);
out_int 0
-and slot_for_getglobal p =
+let slot_for_getglobal p =
enter (Reloc_getglobal p);
out_int 0
@@ -190,7 +190,7 @@ let emit_instr = function
Array.iter (out_label_with_orig org) lbl_bodies
| Kgetglobal q ->
out opGETGLOBAL; slot_for_getglobal q
- | Kconst((Const_b0 i)) ->
+ | Kconst (Const_b0 i) ->
if i >= 0 && i <= 3
then out (opCONST0 + i)
else (out opCONSTINT; out_int i)
@@ -225,6 +225,7 @@ let emit_instr = function
if n <= 1 then out (opSETFIELD0+n)
else (out opSETFIELD;out_int n)
| Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
+ | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p)
(* spiwack *)
| Kbranch lbl -> out opBRANCH; out_label lbl
| Kaddint31 -> out opADDINT31
@@ -306,9 +307,10 @@ type to_patch = emitcodes * (patch list) * fv
(* Substitution *)
let rec subst_strcst s sc =
match sc with
- | Const_sorts _ | Const_b0 _ -> sc
+ | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> sc
+ | Const_proj p -> Const_proj (subst_constant s p)
| Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
- | Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u)
+ | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
let subst_patch s (ri,pos) =
match ri with
@@ -317,7 +319,7 @@ let subst_patch s (ri,pos) =
let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in
(Reloc_annot {a with ci = ci},pos)
| Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
- | Reloc_getglobal kn -> (Reloc_getglobal (subst_pcon s kn), pos)
+ | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos)
let subst_to_patch s (code,pl,fv) =
code,List.rev_map (subst_patch s) pl,fv
@@ -326,36 +328,36 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
type body_code =
| BCdefined of to_patch
- | BCallias of pconstant
+ | BCalias of Names.constant
| BCconstant
type to_patch_substituted =
| PBCdefined of to_patch substituted
-| PBCallias of pconstant substituted
+| PBCalias of Names.constant substituted
| PBCconstant
let from_val = function
| BCdefined tp -> PBCdefined (from_val tp)
-| BCallias cu -> PBCallias (from_val cu)
+| BCalias cu -> PBCalias (from_val cu)
| BCconstant -> PBCconstant
let force = function
| PBCdefined tp -> BCdefined (force subst_to_patch tp)
-| PBCallias cu -> BCallias (force subst_pconstant cu)
+| PBCalias cu -> BCalias (force subst_constant cu)
| PBCconstant -> BCconstant
let subst_to_patch_subst s = function
| PBCdefined tp -> PBCdefined (subst_substituted s tp)
-| PBCallias cu -> PBCallias (subst_substituted s cu)
+| PBCalias cu -> PBCalias (subst_substituted s cu)
| PBCconstant -> PBCconstant
let repr_body_code = function
| PBCdefined tp ->
let (s, tp) = repr_substituted tp in
(s, BCdefined tp)
-| PBCallias cu ->
+| PBCalias cu ->
let (s, cu) = repr_substituted cu in
- (s, BCallias cu)
+ (s, BCalias cu)
| PBCconstant -> (None, BCconstant)
let to_memory (init_code, fun_code, fv) =
@@ -371,8 +373,3 @@ let to_memory (init_code, fun_code, fv) =
| Label_undefined patchlist ->
assert (patchlist = []))) !label_table;
(code, reloc, fv)
-
-
-
-
-
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index cec90130..10f3a608 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -4,7 +4,7 @@ open Cbytecodes
type reloc_info =
| Reloc_annot of annot_switch
| Reloc_const of structured_constant
- | Reloc_getglobal of constant Univ.puniverses
+ | Reloc_getglobal of constant
type patch = reloc_info * int
@@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
type body_code =
| BCdefined of to_patch
- | BCallias of constant Univ.puniverses
+ | BCalias of constant
| BCconstant
diff --git a/kernel/constr.ml b/kernel/constr.ml
index e823c01b..e2b1d3fd 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -475,7 +475,7 @@ let map_with_binders g f l c0 = match kind c0 with
optimisation that physically equal arrays are equals (hence the
calls to {!Array.equal_norefl}). *)
-let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
+let compare_head_gen_leq_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
match kind1 t1, kind2 t2 with
| Rel n1, Rel n2 -> Int.equal n1 n2
| Meta m1, Meta m2 -> Int.equal m1 m2
@@ -512,13 +512,19 @@ let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
not taken into account *)
let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
- compare_head_gen_with kind kind eq_universes leq_sorts eq leq t1 t2
+ compare_head_gen_leq_with kind kind eq_universes leq_sorts eq leq t1 t2
-(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
- the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
- instances and [s] to compare sorts; Cast's,
+(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to
+ compare the immediate subterms of [c1] of [c2] if needed, [u] to
+ compare universe instances and [s] to compare sorts; Cast's,
application associativity, binders name and Cases annotations are
- not taken into account *)
+ not taken into account.
+
+ [compare_head_gen_with] is a variant taking kind-of-term functions,
+ to expose subterms of [c1] and [c2], as arguments. *)
+
+let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 =
+ compare_head_gen_leq_with kind1 kind2 eq_universes eq_sorts eq eq t1 t2
let compare_head_gen eq_universes eq_sorts eq t1 t2 =
compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2
@@ -536,14 +542,6 @@ let rec eq_constr m n =
let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
-let rec equal_with kind1 kind2 m n =
- (* note that pointer equality is not sufficient to ensure equality
- up to [eq_evars], because we may evaluates evars of [m] and [n]
- in different evar contexts. *)
- let req_constr m n = equal_with kind1 kind2 m n in
- compare_head_gen_with kind1 kind2
- (fun _ -> Instance.equal) Sorts.equal req_constr req_constr m n
-
let eq_constr_univs univs m n =
if m == n then true
else
@@ -567,7 +565,7 @@ let leq_constr_univs univs m n =
let rec compare_leq m n =
compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
and leq_constr' m n = m == n || compare_leq m n in
- compare_leq m n
+ compare_leq m n
let eq_constr_univs_infer univs m n =
if m == n then true, Constraint.empty
@@ -578,16 +576,16 @@ let eq_constr_univs_infer univs m n =
if Sorts.equal s1 s2 then true
else
let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- if Univ.check_eq univs u1 u2 then true
- else
- (cstrs := Univ.enforce_eq u1 u2 !cstrs;
- true)
+ if Univ.check_eq univs u1 u2 then true
+ else
+ (cstrs := Univ.enforce_eq u1 u2 !cstrs;
+ true)
in
let rec eq_constr' m n =
m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n
in
let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in
- res, !cstrs
+ res, !cstrs
let leq_constr_univs_infer univs m n =
if m == n then true, Constraint.empty
@@ -598,18 +596,18 @@ let leq_constr_univs_infer univs m n =
if Sorts.equal s1 s2 then true
else
let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- if Univ.check_eq univs u1 u2 then true
- else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
- true)
+ if Univ.check_eq univs u1 u2 then true
+ else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
+ true)
in
let leq_sorts s1 s2 =
if Sorts.equal s1 s2 then true
else
let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
- if Univ.check_leq univs u1 u2 then true
- else
- (cstrs := Univ.enforce_leq u1 u2 !cstrs;
- true)
+ if Univ.check_leq univs u1 u2 then true
+ else
+ (cstrs := Univ.enforce_leq u1 u2 !cstrs;
+ true)
in
let rec eq_constr' m n =
m == n || compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -618,7 +616,7 @@ let leq_constr_univs_infer univs m n =
compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
and leq_constr' m n = m == n || compare_leq m n in
let res = compare_leq m n in
- res, !cstrs
+ res, !cstrs
let always_true _ _ = true
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 67d1aded..e6a3e71f 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -203,14 +203,6 @@ val kind : constr -> (constr, types) kind_of_term
and application grouping *)
val equal : constr -> constr -> bool
-(** [equal_with_evars k1 k2 a b] is true when [a] equals [b] modulo
- alpha, casts, application grouping, and using [k1] to expose the
- head of [a] and [k2] to expose the head of [b]. *)
-val equal_with :
- (constr -> (constr,types) kind_of_term) ->
- (constr -> (constr,types) kind_of_term) ->
- constr -> constr -> bool
-
(** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
application grouping and the universe equalities in [u]. *)
val eq_constr_univs : constr Univ.check_function
@@ -293,6 +285,18 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
(constr -> constr -> bool) ->
constr -> constr -> bool
+(** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2]
+ like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2])
+ is used,rather than {!kind}, to expose the immediate subterms of
+ [c1] (resp. [c2]). *)
+val compare_head_gen_with :
+ (constr -> (constr,types) kind_of_term) ->
+ (constr -> (constr,types) kind_of_term) ->
+ (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+ (Sorts.t -> Sorts.t -> bool) ->
+ (constr -> constr -> bool) ->
+ constr -> constr -> bool
+
(** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using
[f] to compare the immediate subterms of [c1] of [c2] for
conversion, [fle] for cumulativity, [u] to compare universe
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 3b01538b..ec2c334b 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -82,12 +82,17 @@ let fold_strategy f { var_opacity; cst_opacity; } accu =
let get_transp_state { var_trstate; cst_trstate } = (var_trstate, cst_trstate)
(* Unfold the first constant only if it is "more transparent" than the
- second one. In case of tie, expand the second one. *)
+ second one. In case of tie, use the recommended default. *)
let oracle_order f o l2r k1 k2 =
match get_strategy o f k1, get_strategy o f k2 with
- | Expand, _ -> true
- | Level n1, Opaque -> true
- | Level n1, Level n2 -> n1 < n2
- | _ -> l2r (* use recommended default *)
+ | Expand, Expand -> l2r
+ | Expand, (Opaque | Level _) -> true
+ | (Opaque | Level _), Expand -> false
+ | Opaque, Opaque -> l2r
+ | Level _, Opaque -> true
+ | Opaque, Level _ -> false
+ | Level n1, Level n2 ->
+ if Int.equal n1 n2 then l2r
+ else n1 < n2
let get_strategy o = get_strategy o (fun x -> x)
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index b29f06c6..28f0fa4f 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -57,22 +57,34 @@ let set_global v =
let rec eq_structured_constant c1 c2 = match c1, c2 with
| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
-| Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2
+| Const_sorts _, _ -> false
+| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
+| Const_ind _, _ -> false
+| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
+| Const_proj _, _ -> false
| Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
+| Const_b0 _, _ -> false
| Const_bn (t1, a1), Const_bn (t2, a2) ->
Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
-| _ -> false
+| Const_bn _, _ -> false
+| Const_univ_level l1 , Const_univ_level l2 -> Univ.eq_levels l1 l2
+| Const_univ_level _ , _ -> false
+| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2
+| Const_type _ , _ -> false
let rec hash_structured_constant c =
let open Hashset.Combine in
match c with
| Const_sorts s -> combinesmall 1 (Sorts.hash s)
- | Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u))
- | Const_b0 t -> combinesmall 3 (Int.hash t)
+ | Const_ind i -> combinesmall 2 (ind_hash i)
+ | Const_proj p -> combinesmall 3 (Constant.hash p)
+ | Const_b0 t -> combinesmall 4 (Int.hash t)
| Const_bn (t, a) ->
let fold h c = combine h (hash_structured_constant c) in
let h = Array.fold_left fold 0 a in
- combinesmall 4 (combine (Int.hash t) h)
+ combinesmall 5 (combine (Int.hash t) h)
+ | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l)
+ | Const_type u -> combinesmall 7 (Univ.Universe.hash u)
module SConstTable = Hashtbl.Make (struct
type t = structured_constant
@@ -118,7 +130,7 @@ exception NotEvaluated
let key rk =
match !rk with
| None -> raise NotEvaluated
- | Some k -> (*Pp.msgnl (str"found at: "++int k);*)
+ | Some k ->
try Ephemeron.get k
with Ephemeron.InvalidKey -> raise NotEvaluated
@@ -142,23 +154,22 @@ let slot_for_annot key =
AnnotTable.add annot_tbl key n;
n
-let rec slot_for_getglobal env (kn,u) =
+let rec slot_for_getglobal env kn =
let (cb,(_,rk)) = lookup_constant_key kn env in
try key rk
with NotEvaluated ->
(* Pp.msgnl(str"not yet evaluated");*)
let pos =
match cb.const_body_code with
- | None -> set_global (val_of_constant (kn,u))
+ | None -> set_global (val_of_constant kn)
| Some code ->
match Cemitcodes.force code with
| BCdefined(code,pl,fv) ->
- if Univ.Instance.is_empty u then
- let v = eval_to_patch env (code,pl,fv) in
- set_global v
- else set_global (val_of_constant (kn,u))
- | BCallias kn' -> slot_for_getglobal env kn'
- | BCconstant -> set_global (val_of_constant (kn,u)) in
+ let v = eval_to_patch env (code,pl,fv) in
+ set_global v
+ | BCalias kn' -> slot_for_getglobal env kn'
+ | BCconstant -> set_global (val_of_constant kn)
+ in
(*Pp.msgnl(str"value stored at: "++int pos);*)
rk := Some (Ephemeron.create pos);
pos
@@ -191,6 +202,8 @@ and slot_for_fv env fv =
fill_fv_cache rv i val_of_rel env_of_rel b
| Some (v, _) -> v
end
+ | FVuniv_var idu ->
+ assert false
and eval_to_patch env (buff,pl,fv) =
(* copy code *before* patching because of nested evaluations:
@@ -208,7 +221,6 @@ and eval_to_patch env (buff,pl,fv) =
List.iter patch pl;
let vm_env = Array.map (slot_for_fv env) fv in
let tc = tcode_of_code buff (length buff) in
-(*Pp.msgnl (str"execute code");*)
eval_tcode tc vm_env
and val_of_constr env c =
@@ -226,5 +238,3 @@ and val_of_constr env c =
let set_transparent_const kn = () (* !?! *)
let set_opaque_const kn = () (* !?! *)
-
-
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 27c1c3f3..dc5c17a7 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -14,7 +14,10 @@ open Context
declarations. This includes global constants/axioms, mutual
inductive definitions, modules and module types *)
-type engagement = ImpredicativeSet
+type set_predicativity = ImpredicativeSet | PredicativeSet
+type type_hierarchy = TypeInType | StratifiedType
+
+type engagement = set_predicativity * type_hierarchy
(** {6 Representation of constants (Definition/Axiom) } *)
@@ -76,12 +79,6 @@ type constant_body = {
const_proj : projection_body option;
const_inline_code : bool }
-type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
-
-type side_effect =
- | SEsubproof of constant * constant_body * seff_env
- | SEscheme of (inductive * constant * constant_body * seff_env) list * string
-
(** {6 Representation of mutual inductive types in the kernel } *)
type recarg =
@@ -142,12 +139,10 @@ type one_inductive_body = {
mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
mind_consnrealargs : int array;
- (** Number of expected proper arguments of the constructors (w/o params)
- (not used in the kernel) *)
+ (** Number of expected proper arguments of the constructors (w/o params) *)
mind_consnrealdecls : int array;
- (** Length of the signature of the constructors (with let, w/o params)
- (not used in the kernel) *)
+ (** Length of the signature of the constructors (with let, w/o params) *)
mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
@@ -245,8 +240,8 @@ and module_body =
mod_type : module_signature; (** expanded type *)
(** algebraic type, kept if it's relevant for extraction *)
mod_type_alg : module_expression option;
- (** set of all constraints in the module *)
- mod_constraints : Univ.constraints;
+ (** set of all universes constraints in the module *)
+ mod_constraints : Univ.ContextSet.t;
(** quotiented set of equivalent constants and inductive names *)
mod_delta : Mod_subst.delta_resolver;
mod_retroknowledge : Retroknowledge.action list }
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index a7051d5c..248504c1 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -304,17 +304,7 @@ let hcons_mind mib =
(** {6 Stm machinery } *)
-let string_of_side_effect = function
- | SEsubproof (c,_,_) -> Names.string_of_con c
- | SEscheme (cl,_) ->
- String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl)
-type side_effects = side_effect list
-let no_seff = ([] : side_effects)
-let iter_side_effects f l = List.iter f (List.rev l)
-let fold_side_effects f a l = List.fold_left f a l
-let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l))
-let union_side_effects l1 l2 = l1 @ l2
-let flatten_side_effects l = List.flatten l
-let side_effects_of_list l = l
-let cons_side_effects x l = x :: l
-let side_effects_is_empty = List.is_empty
+let string_of_side_effect { Entries.eff } = match eff with
+ | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")"
+ | Entries.SEscheme (cl,_) ->
+ "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")"
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index ce65af97..1b870095 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -9,6 +9,7 @@
open Declarations
open Mod_subst
open Univ
+open Entries
(** Operations concerning types in [Declarations] :
[constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -49,17 +50,6 @@ val is_opaque : constant_body -> bool
val string_of_side_effect : side_effect -> string
-type side_effects
-val no_seff : side_effects
-val iter_side_effects : (side_effect -> unit) -> side_effects -> unit
-val fold_side_effects : ('a -> side_effect -> 'a) -> 'a -> side_effects -> 'a
-val uniquize_side_effects : side_effects -> side_effects
-val union_side_effects : side_effects -> side_effects -> side_effects
-val flatten_side_effects : side_effects list -> side_effects
-val side_effects_of_list : side_effect list -> side_effects
-val cons_side_effects : side_effect -> side_effects -> side_effects
-val side_effects_is_empty : side_effects -> bool
-
(** {6 Inductive types} *)
val eq_recarg : recarg -> recarg -> bool
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 303d27d3..e058519e 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -54,11 +54,11 @@ type mutual_inductive_entry = {
mind_entry_private : bool option }
(** {6 Constants (Definition/Axiom) } *)
-type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects
-type const_entry_body = proof_output Future.computation
+type 'a proof_output = constr Univ.in_universe_context_set * 'a
+type 'a const_entry_body = 'a proof_output Future.computation
-type definition_entry = {
- const_entry_body : const_entry_body;
+type 'a definition_entry = {
+ const_entry_body : 'a const_entry_body;
(* List of section variables *)
const_entry_secctx : Context.section_context option;
(* State id on which the completion of type checking is reported *)
@@ -78,8 +78,8 @@ type projection_entry = {
proj_entry_ind : mutual_inductive;
proj_entry_arg : int }
-type constant_entry =
- | DefinitionEntry of definition_entry
+type 'a constant_entry =
+ | DefinitionEntry of 'a definition_entry
| ParameterEntry of parameter_entry
| ProjectionEntry of projection_entry
@@ -96,3 +96,16 @@ type module_entry =
| MType of module_params_entry * module_struct_entry
| MExpr of
module_params_entry * module_struct_entry * module_struct_entry option
+
+type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
+
+type side_eff =
+ | SEsubproof of constant * Declarations.constant_body * seff_env
+ | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string
+
+type side_effect = {
+ from_env : Declarations.structure_body Ephemeron.key;
+ eff : side_eff;
+}
+
+type side_effects = side_effect list
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a79abbb7..429aba4f 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,11 +46,14 @@ let empty_env = empty_env
let engagement env = env.env_stratification.env_engagement
-let type_in_type env = env.env_stratification.env_type_in_type
-
let is_impredicative_set env =
- match engagement env with
- | Some ImpredicativeSet -> true
+ match fst (engagement env) with
+ | ImpredicativeSet -> true
+ | _ -> false
+
+let type_in_type env =
+ match snd (engagement env) with
+ | TypeInType -> true
| _ -> false
let universes env = env.env_stratification.env_universes
@@ -159,7 +162,7 @@ let reset_context = reset_with_named_context empty_named_context_val
let pop_rel_context n env =
let ctxt = env.env_rel_context in
{ env with
- env_rel_context = List.firstn (List.length ctxt - n) ctxt;
+ env_rel_context = List.skipn n ctxt;
env_nb_rel = env.env_nb_rel - n }
let fold_named_context f env ~init =
@@ -178,30 +181,44 @@ let fold_named_context_reverse f ~init env =
(* Universe constraints *)
-let add_constraints c env =
- if Univ.Constraint.is_empty c then
- env
- else
- let s = env.env_stratification in
+let map_universes f env =
+ let s = env.env_stratification in
{ env with env_stratification =
- { s with env_universes = Univ.merge_constraints c s.env_universes } }
+ { s with env_universes = f s.env_universes } }
+
+let add_constraints c env =
+ if Univ.Constraint.is_empty c then env
+ else map_universes (Univ.merge_constraints c) env
let check_constraints c env =
Univ.check_constraints c env.env_stratification.env_universes
-let set_engagement c env = (* Unsafe *)
- { env with env_stratification =
- { env.env_stratification with env_engagement = Some c } }
-
-let set_type_in_type env =
- { env with env_stratification =
- { env.env_stratification with env_type_in_type = true } }
-
let push_constraints_to_env (_,univs) env =
add_constraints univs env
-let push_context ctx env = add_constraints (Univ.UContext.constraints ctx) env
-let push_context_set ctx env = add_constraints (Univ.ContextSet.constraints ctx) env
+let add_universes strict ctx g =
+ let g = Array.fold_left
+ (* Be lenient, module typing reintroduces universes and constraints due to includes *)
+ (fun g v -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g)
+ g (Univ.Instance.to_array (Univ.UContext.instance ctx))
+ in
+ Univ.merge_constraints (Univ.UContext.constraints ctx) g
+
+let push_context ?(strict=false) ctx env =
+ map_universes (add_universes strict ctx) env
+
+let add_universes_set strict ctx g =
+ let g = Univ.LSet.fold
+ (fun v g -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g)
+ (Univ.ContextSet.levels ctx) g
+ in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g
+
+let push_context_set ?(strict=false) ctx env =
+ map_universes (add_universes_set strict ctx) env
+
+let set_engagement c env = (* Unsafe *)
+ { env with env_stratification =
+ { env.env_stratification with env_engagement = c } }
(* Global constants *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ede356e6..dfe6cc85 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -50,10 +50,9 @@ val opaque_tables : env -> Opaqueproof.opaquetab
val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
-val engagement : env -> engagement option
+val engagement : env -> engagement
val is_impredicative_set : env -> bool
-
-val type_in_type : env -> bool
+val type_in_type : env -> bool
(** is the local context empty *)
val empty_context : env -> bool
@@ -209,14 +208,12 @@ val add_constraints : Univ.constraints -> env -> env
(** Check constraints are satifiable in the environment. *)
val check_constraints : Univ.constraints -> env -> bool
-val push_context : Univ.universe_context -> env -> env
-val push_context_set : Univ.universe_context_set -> env -> env
+val push_context : ?strict:bool -> Univ.universe_context -> env -> env
+val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
val push_constraints_to_env : 'a Univ.constrained -> env -> env
val set_engagement : engagement -> env -> env
-val set_type_in_type : env -> env
-
(** {6 Sets of referred section variables }
[global_vars_set env c] returns the list of [id]'s occurring either
directly as [Var id] in [c] or indirectly as a section variable
@@ -253,7 +250,7 @@ type unsafe_type_judgment = {
(** {6 Compilation of global declaration } *)
-val compile_constant_body : env -> constant_def -> Cemitcodes.body_code option
+val compile_constant_body : env -> constant_universes option -> constant_def -> Cemitcodes.body_code option
exception Hyp_not_found
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 86fb1b64..063c9cf1 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -182,14 +182,12 @@ let sort_of_product env domsort rangsort =
| (Prop _, Prop Pos) -> rangsort
(* Product rule (Type,Set,?) *)
| (Type u1, Prop Pos) ->
- begin match engagement env with
- | Some ImpredicativeSet ->
+ if is_impredicative_set env then
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
- | _ ->
+ else
(* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
Type (Universe.sup Universe.type0 u1)
- end
(* Product rule (Prop,Type_i,Type_i) *)
| (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2)
(* Product rule (Prop,Type_i,Type_i) *)
@@ -229,7 +227,7 @@ let judge_of_cast env c ct k expected_type =
default_conv ~l2r:true CUMUL env ct expected_type
| NATIVEcast ->
let sigma = Nativelambda.empty_evars in
- native_conv CUMUL sigma env ct expected_type
+ Nativeconv.native_conv CUMUL sigma env ct expected_type
with NotConvertible ->
error_actual_type env (make_judge c ct) expected_type
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 6b909824..8b03df64 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -173,38 +173,21 @@ let cumulate_arity_large_levels env sign =
sign (Universe.type0m,env))
let is_impredicative env u =
- is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet)
+ is_type0m_univ u || (is_type0_univ u && is_impredicative_set env)
+(* Returns the list [x_1, ..., x_n] of levels contributing to template
+ polymorphism. The elements x_k is None if the k-th parameter (starting
+ from the most recent and ignoring let-definitions) is not contributing
+ or is Some u_k if its level is u_k and is contributing. *)
let param_ccls params =
- let has_some_univ u = function
- | Some v when Univ.Level.equal u v -> true
- | _ -> false
+ let fold acc = function (_, None, p) ->
+ (let c = strip_prod_assum p in
+ match kind_of_term c with
+ | Sort (Type u) -> Univ.Universe.level u
+ | _ -> None) :: acc
+ | _ -> acc
in
- let remove_some_univ u = function
- | Some v when Univ.Level.equal u v -> None
- | x -> x
- in
- let fold l (_, b, p) = match b with
- | None ->
- (* Parameter contributes to polymorphism only if explicit Type *)
- let c = strip_prod_assum p in
- (* Add Type levels to the ordered list of parameters contributing to *)
- (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
- begin match kind_of_term c with
- | Sort (Type u) ->
- (match Univ.Universe.level u with
- | Some u ->
- if List.exists (has_some_univ u) l then
- None :: List.map (remove_some_univ u) l
- else
- Some u :: l
- | None -> None :: l)
- | _ ->
- None :: l
- end
- | _ -> l
- in
- List.fold_left fold [] params
+ List.fold_left fold [] params
(* Type-check an inductive definition. Does not check positivity
conditions. *)
@@ -302,8 +285,7 @@ let typecheck_inductive env mie =
let full_polymorphic () =
let defu = Term.univ_of_sort def_level in
let is_natural =
- type_in_type env || (check_leq (universes env') infu defu &&
- not (is_type0m_univ defu && not is_unit))
+ type_in_type env || (check_leq (universes env') infu defu)
in
let _ =
(** Impredicative sort, always allow *)
@@ -356,7 +338,7 @@ type ill_formed_ind =
| LocalNonPos of int
| LocalNotEnoughArgs of int
| LocalNotConstructor
- | LocalNonPar of int * int
+ | LocalNonPar of int * int * int
exception IllFormedInd of ill_formed_ind
@@ -377,9 +359,9 @@ let explain_ind_err id ntyp env nbpar c nargs err =
| LocalNotConstructor ->
raise (InductiveError
(NotConstructor (env,id,c',mkRel (ntyp+nbpar),nbpar,nargs)))
- | LocalNonPar (n,l) ->
+ | LocalNonPar (n,i,l) ->
raise (InductiveError
- (NonPar (env,c',n,mkRel (nbpar-n+1), mkRel (l+nbpar))))
+ (NonPar (env,c',n,mkRel i, mkRel (l+nbpar))))
let failwith_non_pos n ntypes c =
for k = n to n + ntypes - 1 do
@@ -408,7 +390,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
| _::hyps ->
match kind_of_term (whd_betadeltaiota env lpar.(k)) with
| Rel w when Int.equal w index -> check (k-1) (index+1) hyps
- | _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
+ | _ -> raise (IllFormedInd (LocalNonPar (k+1, index-n+nhyps+1, l)))
in check (nparams-1) (n-nhyps) hyps;
if not (Array.for_all (noccur_between n ntypes) largs') then
failwith_non_pos_vect n ntypes largs'
@@ -663,10 +645,28 @@ exception UndefinableExpansion
build an expansion function.
The term built is expecting to be substituted first by
a substitution of the form [params, x : ind params] *)
-let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
- mind_consnrealdecls mind_consnrealargs ctx =
+let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
+ mind_consnrealdecls mind_consnrealargs paramslet ctx =
let mp, dp, l = repr_mind kn in
- let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in
+ (** We build a substitution smashing the lets in the record parameters so
+ that typechecking projections requires just a substitution and not
+ matching with a parameter context. *)
+ let indty, paramsletsubst =
+ let subst, inst =
+ List.fold_right
+ (fun (na, b, t) (subst, inst) ->
+ match b with
+ | None -> (mkRel 1 :: List.map (lift 1) subst,
+ mkRel 1 :: List.map (lift 1) inst)
+ | Some b -> (substl subst b) :: subst, List.map (lift 1) inst)
+ paramslet ([], [])
+ in
+ let subst = (* For the record parameter: *)
+ mkRel 1 :: List.map (lift 1) subst
+ in
+ let ty = mkApp (mkIndU indu, CArray.rev_of_list inst) in
+ ty, subst
+ in
let ci =
let print_info =
{ ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
@@ -679,34 +679,39 @@ let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
let len = List.length ctx in
let x = Name x in
let compat_body ccl i =
- (* [ccl] is defined in context [params;x:rp] *)
- (* [ccl'] is defined in context [params;x:rp;x:rp] *)
+ (* [ccl] is defined in context [params;x:indty] *)
+ (* [ccl'] is defined in context [params;x:indty;x:indty] *)
let ccl' = liftn 1 2 ccl in
- let p = mkLambda (x, lift 1 rp, ccl') in
+ let p = mkLambda (x, lift 1 indty, ccl') in
let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
- it_mkLambda_or_LetIn (mkLambda (x,rp,body)) params
+ it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
in
- let projections (na, b, t) (i, j, kns, pbs, subst) =
+ let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) =
match b with
- | Some c -> (i, j+1, kns, pbs, substl subst c :: subst)
+ | Some c -> (i, j+1, kns, pbs, substl subst c :: subst,
+ substl letsubst c :: subst)
| None ->
match na with
| Name id ->
let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
+ let projty = substl letsubst (liftn 1 j t) in
let ty = substl subst (liftn 1 j t) in
let term = mkProj (Projection.make kn true, mkRel 1) in
let fterm = mkProj (Projection.make kn false, mkRel 1) in
let compat = compat_body ty (j - 1) in
- let etab = it_mkLambda_or_LetIn (mkLambda (x, rp, term)) params in
- let etat = it_mkProd_or_LetIn (mkProd (x, rp, ty)) params in
+ let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
+ let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
let body = { proj_ind = fst ind; proj_npars = nparamargs;
- proj_arg = i; proj_type = ty; proj_eta = etab, etat;
+ proj_arg = i; proj_type = projty; proj_eta = etab, etat;
proj_body = compat } in
- (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: subst)
+ (i + 1, j + 1, kn :: kns, body :: pbs,
+ fterm :: subst, fterm :: letsubst)
| Anonymous -> raise UndefinableExpansion
in
- let (_, _, kns, pbs, subst) = List.fold_right projections ctx (0, 1, [], [], []) in
+ let (_, _, kns, pbs, subst, letsubst) =
+ List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
+ in
Array.of_list (List.rev kns),
Array.of_list (List.rev pbs)
@@ -792,12 +797,12 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
else Univ.Instance.empty
in
let indsp = ((kn, 0), u) in
- let rctx, _ = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
+ let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
(try
- let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in
+ let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
let kns, projs =
compute_projections indsp pkt.mind_typename rid nparamargs params
- pkt.mind_consnrealdecls pkt.mind_consnrealargs fields
+ pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
in Some (Some (rid, kns, projs))
with UndefinableExpansion -> Some None)
| Some _ -> Some None
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7774e52e..01acdce5 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -43,5 +43,5 @@ val is_indices_matter : unit -> bool
val compute_projections : pinductive -> Id.t -> Id.t ->
int -> Context.rel_context -> int array -> int array ->
- Context.rel_context ->
+ Context.rel_context -> Context.rel_context ->
(constant array * projection_body array)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ca814f49..1f870665 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -73,7 +73,7 @@ let constructor_instantiate mind u mib c =
let s = ind_subst mind mib u in
substl s (subst_instance_constr u c)
-let instantiate_params full t args sign =
+let instantiate_params full t u args sign =
let fail () =
anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
let (rem_args, subs, ty) =
@@ -81,7 +81,8 @@ let instantiate_params full t args sign =
(fun (_,copt,_) (largs,subs,ty) ->
match (copt, largs, kind_of_term ty) with
| (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
- | (Some b,_,LetIn(_,_,_,t)) -> (largs, (substl subs b)::subs, t)
+ | (Some b,_,LetIn(_,_,_,t)) ->
+ (largs, (substl subs (subst_instance_constr u b))::subs, t)
| (_,[],_) -> if full then fail() else ([], subs, ty)
| _ -> fail ())
sign
@@ -92,15 +93,13 @@ let instantiate_params full t args sign =
let full_inductive_instantiate mib u params sign =
let dummy = prop_sort in
- let t = mkArity (sign,dummy) in
- let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
- Vars.subst_instance_context u ar
-
-let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
- let inst_ind = constructor_instantiate mind u mib in
- (fun t ->
- instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
+ let t = mkArity (Vars.subst_instance_context u sign,dummy) in
+ fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
+let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
+ let inst_ind = constructor_instantiate mind u mib t in
+ instantiate_params true inst_ind u params mib.mind_params_ctxt
+
(************************************************************************)
(************************************************************************)
@@ -134,46 +133,60 @@ let sort_as_univ = function
(* Template polymorphism *)
+(* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
+(* in the domain or add [u |-> sup x su] if [u] is already mapped *)
+(* to [x]. *)
let cons_subst u su subst =
- Univ.LMap.add u su subst
+ try
+ Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+ with Not_found -> Univ.LMap.add u su subst
+
+(* remember_subst updates the mapping [u |-> x] by [u |-> sup x u] *)
+(* if it is presents and returns the substitution unchanged if not.*)
+let remember_subst u subst =
+ try
+ let su = Universe.make u in
+ Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+ with Not_found -> subst
(* Bind expected levels of parameters to actual levels *)
(* Propagate the new levels in the signature *)
-let rec make_subst env = function
- | (_,Some _,_ as t)::sign, exp, args ->
- let ctx,subst = make_subst env (sign, exp, args) in
- t::ctx, subst
- | d::sign, None::exp, args ->
- let args = match args with _::args -> args | [] -> [] in
- let ctx,subst = make_subst env (sign, exp, args) in
- d::ctx, subst
- | d::sign, Some u::exp, a::args ->
- (* We recover the level of the argument, but we don't change the *)
- (* level in the corresponding type in the arity; this level in the *)
- (* arity is a global level which, at typing time, will be enforce *)
- (* to be greater than the level of the argument; this is probably *)
- (* a useless extra constraint *)
- let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
- let ctx,subst = make_subst env (sign, exp, args) in
- d::ctx, cons_subst u s subst
- | (na,None,t as d)::sign, Some u::exp, [] ->
- (* No more argument here: we instantiate the type with a fresh level *)
- (* which is first propagated to the corresponding premise in the arity *)
- (* (actualize_decl_level), then to the conclusion of the arity (via *)
- (* the substitution) *)
- let ctx,subst = make_subst env (sign, exp, []) in
- d::ctx, subst
- | sign, [], _ ->
- (* Uniform parameters are exhausted *)
- sign, Univ.LMap.empty
- | [], _, _ ->
- assert false
+let rec make_subst env =
+ let rec make subst = function
+ | (_,Some _,_)::sign, exp, args ->
+ make subst (sign, exp, args)
+ | d::sign, None::exp, args ->
+ let args = match args with _::args -> args | [] -> [] in
+ make subst (sign, exp, args)
+ | d::sign, Some u::exp, a::args ->
+ (* We recover the level of the argument, but we don't change the *)
+ (* level in the corresponding type in the arity; this level in the *)
+ (* arity is a global level which, at typing time, will be enforce *)
+ (* to be greater than the level of the argument; this is probably *)
+ (* a useless extra constraint *)
+ let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
+ make (cons_subst u s subst) (sign, exp, args)
+ | (na,None,t)::sign, Some u::exp, [] ->
+ (* No more argument here: we add the remaining universes to the *)
+ (* substitution (when [u] is distinct from all other universes in the *)
+ (* template, it is identity substitution otherwise (ie. when u is *)
+ (* already in the domain of the substitution) [remember_subst] will *)
+ (* update its image [x] by [sup x u] in order not to forget the *)
+ (* dependency in [u] that remains to be fullfilled. *)
+ make (remember_subst u subst) (sign, exp, [])
+ | sign, [], _ ->
+ (* Uniform parameters are exhausted *)
+ subst
+ | [], _, _ ->
+ assert false
+ in
+ make Univ.LMap.empty
exception SingletonInductiveBecomesProp of Id.t
let instantiate_universes env ctx ar argsorts =
let args = Array.to_list argsorts in
- let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
+ let subst = make_subst env (ctx,ar.template_param_levels,args) in
let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
let ty =
(* Singleton type not containing types are interpretable in Prop *)
@@ -213,8 +226,8 @@ let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) a
let cst = instantiate_inductive_constraints mib u in
(ty, cst)
-let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args =
- type_of_inductive_gen env mip args
+let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args =
+ type_of_inductive_gen ~polyprop env mip args
(* The max of an array of universes *)
@@ -331,13 +344,13 @@ let is_correct_arity env c pj ind specif params =
| Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
let env' = push_rel (na1,None,a1) env in
let ksort = match kind_of_term (whd_betadeltaiota env' a2) with
- | Sort s -> family_of_sort s
- | _ -> raise (LocalArity None) in
+ | Sort s -> family_of_sort s
+ | _ -> raise (LocalArity None) in
let dep_ind = build_dependent_inductive ind specif params in
let _ =
try conv env a1 dep_ind
with NotConvertible -> raise (LocalArity None) in
- check_allowed_sort ksort specif
+ check_allowed_sort ksort specif
| _, (_,Some _,_ as d)::ar' ->
srec (push_rel d env) (lift 1 pt') ar'
| _ ->
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index f7ae30e7..ba14f65d 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -122,7 +122,7 @@ let add_kn_delta_resolver kn kn' =
let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2
-(** Extending a [substitution] *)
+(** Extending a [substitution] without sequential composition *)
let add_mbid mbid mp resolve s = Umap.add_mbi mbid (mp,resolve) s
let add_mp mp1 mp2 resolve s = Umap.add_mp mp1 (mp2,resolve) s
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index fc2b0441..cd9fa792 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -68,8 +68,9 @@ val empty_subst : substitution
val is_empty_subst : substitution -> bool
-(** add_* add [arg2/arg1]\{arg3\} to the substitution with no
- sequential composition *)
+(** add_* add [arg2/arg1]\{arg3\} to the substitution with no sequential
+ composition. Most often this is not what you want. For sequential
+ composition, try [join (map_mbid mp delta) subs] **)
val add_mbid :
MBId.t -> module_path -> delta_resolver -> substitution -> substitution
val add_mp :
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 26dd45f5..bd7ee7b3 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -21,7 +21,7 @@ open Modops
open Mod_subst
type 'alg translation =
- module_signature * 'alg option * delta_resolver * Univ.constraints
+ module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
let rec mp_from_mexpr = function
| MEident mp -> mp
@@ -52,7 +52,7 @@ let rec rebuild_mp mp l =
| []-> mp
| i::r -> rebuild_mp (MPdot(mp,Label.of_id i)) r
-let (+++) = Univ.Constraint.union
+let (+++) = Univ.ContextSet.union
let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let lab,idl = match idl with
@@ -72,33 +72,71 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
(* In the spirit of subtyping.check_constant, we accept
any implementations of parameters and opaques terms,
as long as they have the right type *)
- let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in
- let env' = Environ.add_constraints ccst env' in
- let newus, cst = Univ.UContext.dest ctx in
- let env' = Environ.add_constraints cst env' in
- let c',cst = match cb.const_body with
- | Undef _ | OpaqueDef _ ->
- let j = Typeops.infer env' c in
- let typ = Typeops.type_of_constant_type env' cb.const_type in
- let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
- j.uj_type typ in
- j.uj_val,cst' +++ cst
- | Def cs ->
- let cst' = Reduction.infer_conv env' (Environ.universes env') c
- (Mod_subst.force_constr cs) in
- let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *)
- if cb.const_polymorphic then cst' +++ cst
- else cst' +++ cst
+ let uctx = Declareops.universes_of_constant (opaque_tables env) cb in
+ let uctx = (* Context of the spec *)
+ if cb.const_polymorphic then
+ Univ.instantiate_univ_context uctx
+ else uctx
+ in
+ let c', univs, ctx' =
+ if not cb.const_polymorphic then
+ let env' = Environ.push_context ~strict:true uctx env' in
+ let env' = Environ.push_context ~strict:true ctx env' in
+ let c',cst = match cb.const_body with
+ | Undef _ | OpaqueDef _ ->
+ let j = Typeops.infer env' c in
+ let typ = Typeops.type_of_constant_type env' cb.const_type in
+ let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+ j.uj_type typ in
+ j.uj_val, cst'
+ | Def cs ->
+ let c' = Mod_subst.force_constr cs in
+ c, Reduction.infer_conv env' (Environ.universes env') c c'
+ in c', ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
+ else
+ let cus, ccst = Univ.UContext.dest uctx in
+ let newus, cst = Univ.UContext.dest ctx in
+ let () =
+ if not (Univ.Instance.length cus == Univ.Instance.length newus) then
+ error_incorrect_with_constraint lab
+ in
+ let inst = Univ.Instance.append cus newus in
+ let csti = Univ.enforce_eq_instances cus newus cst in
+ let csta = Univ.Constraint.union csti ccst in
+ let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in
+ let () = if not (Univ.check_constraints cst (Environ.universes env')) then
+ error_incorrect_with_constraint lab
+ in
+ let cst = match cb.const_body with
+ | Undef _ | OpaqueDef _ ->
+ let j = Typeops.infer env' c in
+ let typ = Typeops.type_of_constant_type env' cb.const_type in
+ let typ = Vars.subst_instance_constr cus typ in
+ let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+ j.uj_type typ in
+ cst'
+ | Def cs ->
+ let c' = Vars.subst_instance_constr cus (Mod_subst.force_constr cs) in
+ let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in
+ cst'
in
- c, cst
+ if not (Univ.Constraint.is_empty cst) then
+ error_incorrect_with_constraint lab;
+ let subst, ctx = Univ.abstract_universes true ctx in
+ Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty
in
let def = Def (Mod_subst.from_val c') in
- let ctx' = Univ.UContext.make (newus, cst) in
+(* let ctx' = Univ.UContext.make (newus, cst) in *)
+ let univs =
+ if cb.const_polymorphic then Some cb.const_universes
+ else None
+ in
let cb' =
{ cb with
const_body = def;
- const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def);
- const_universes = ctx' }
+ const_universes = ctx ;
+ const_body_code = Option.map Cemitcodes.from_val
+ (compile_constant_body env' univs def) }
in
before@(lab,SFBconst(cb'))::after, c', ctx'
else
@@ -145,8 +183,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
begin
try
let mtb_old = module_type_of_module old in
- Subtyping.check_subtypes env' mtb_mp1 mtb_old
- +++ old.mod_constraints
+ Univ.ContextSet.add_constraints (Subtyping.check_subtypes env' mtb_mp1 mtb_old) old.mod_constraints
with Failure _ -> error_incorrect_with_constraint lab
end
| Algebraic (NoFunctor (MEident(mp'))) ->
@@ -194,7 +231,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
| Algebraic (NoFunctor (MEident mp0)) ->
let mpnew = rebuild_mp mp0 idl in
check_modpath_equiv env' mpnew mp;
- before@(lab,spec)::after, equiv, Univ.Constraint.empty
+ before@(lab,spec)::after, equiv, Univ.ContextSet.empty
| _ -> error_generative_module_expected lab
end
with
@@ -207,8 +244,8 @@ let check_with env mp (sign,alg,reso,cst) = function
|WithDef(idl,c) ->
let struc = destr_nofunctor sign in
let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
- let alg' = mk_alg_with alg (WithDef (idl,(c',cst'))) in
- (NoFunctor struc'),alg',reso, cst+++(Univ.UContext.constraints cst')
+ let alg' = mk_alg_with alg (WithDef (idl,(c',Univ.ContextSet.to_context cst'))) in
+ (NoFunctor struc'),alg',reso, cst+++cst'
|WithMod(idl,mp1) as wd ->
let struc = destr_nofunctor sign in
let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
@@ -238,7 +275,7 @@ let rec translate_mse env mpo inl = function
let mtb = lookup_modtype mp1 env in
mtb.mod_type, mtb.mod_delta
in
- sign,Some (MEident mp1),reso,Univ.Constraint.empty
+ sign,Some (MEident mp1),reso,Univ.ContextSet.empty
|MEapply (fe,mp1) ->
translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo)
|MEwith(me, with_decl) ->
@@ -256,7 +293,7 @@ and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
let body = subst_signature subst fbody_b in
let alg' = mkalg alg mp1 in
let reso' = subst_codom_delta_resolver subst reso in
- body,alg',reso', cst1 +++ cst2
+ body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
| Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
@@ -301,13 +338,15 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
mk_mod mp impl sign None cst reso
|Some (params_mte,inl) ->
let res_mtb = translate_modtype env mp inl params_mte in
- let auto_mtb = mk_modtype mp sign Univ.Constraint.empty reso in
+ let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in
let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in
let impl = match alg with Some e -> Algebraic e | None -> Struct sign in
{ res_mtb with
mod_mp = mp;
mod_expr = impl;
- mod_constraints = cst +++ cst' }
+ (** cst from module body typing, cst' from subtyping,
+ and constraints from module type. *)
+ mod_constraints = Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
let translate_module env mp inl = function
|MType (params,ty) ->
@@ -318,12 +357,20 @@ let translate_module env mp inl = function
let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
finalize_module env mp t restype
-let rec translate_mse_incl env mp inl = function
+let rec translate_mse_inclmod env mp inl = function
|MEident mp1 ->
let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
let sign = clean_bounded_mod_expr mb.mod_type in
- sign,None,mb.mod_delta,Univ.Constraint.empty
+ sign,None,mb.mod_delta,Univ.ContextSet.empty
|MEapply (fe,arg) ->
- let ftrans = translate_mse_incl env mp inl fe in
+ let ftrans = translate_mse_inclmod env mp inl fe in
translate_apply env inl ftrans arg (fun _ _ -> None)
- |_ -> Modops.error_higher_order_include ()
+ |MEwith _ -> assert false (* No 'with' syntax for modules *)
+
+let translate_mse_incl is_mod env mp inl me =
+ if is_mod then
+ translate_mse_inclmod env mp inl me
+ else
+ let mtb = translate_modtype env mp inl ([],me) in
+ let sign = clean_bounded_mod_expr mtb.mod_type in
+ sign,None,mtb.mod_delta,mtb.mod_constraints
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index b39e8212..bc0e2020 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -30,17 +30,20 @@ val translate_modtype :
*)
type 'alg translation =
- module_signature * 'alg option * delta_resolver * Univ.constraints
+ module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
val translate_mse :
env -> module_path option -> inline -> module_struct_entry ->
module_alg_expr translation
-val translate_mse_incl :
- env -> module_path -> inline -> module_struct_entry ->
- module_alg_expr translation
-
val finalize_module :
env -> module_path -> module_expression translation ->
(module_type_entry * inline) option ->
module_body
+
+(** [translate_mse_incl] translate the mse of a module or
+ module type given to an Include *)
+
+val translate_mse_incl :
+ bool -> env -> module_path -> inline -> module_struct_entry ->
+ module_alg_expr translation
diff --git a/kernel/modops.ml b/kernel/modops.ml
index d52fe611..cbb79633 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -67,7 +67,6 @@ type module_typing_error =
| IncorrectWithConstraint of Label.t
| GenerativeModuleExpected of Label.t
| LabelMissing of Label.t * string
- | HigherOrderInclude
exception ModuleTypingError of module_typing_error
@@ -113,9 +112,6 @@ let error_generative_module_expected l =
let error_no_such_label_sub l l1 =
raise (ModuleTypingError (LabelMissing (l,l1)))
-let error_higher_order_include () =
- raise (ModuleTypingError HigherOrderInclude)
-
(** {6 Operations on functors } *)
let is_functor = function
@@ -331,13 +327,15 @@ let strengthen_const mp_from l cb resolver =
let kn = KerName.make2 mp_from l in
let con = constant_of_delta_kn resolver kn in
let u =
- if cb.const_polymorphic then
- Univ.UContext.instance cb.const_universes
+ if cb.const_polymorphic then
+ let u = Univ.UContext.instance cb.const_universes in
+ let s = Univ.make_instance_subst u in
+ Univ.subst_univs_level_instance s u
else Univ.Instance.empty
in
{ cb with
const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
- const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias (con,u))) }
+ const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
let rec strengthen_mod mp_from mp_to mb =
if mp_in_delta mb.mod_mp mb.mod_delta then mb
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 6fbcd81d..a335ad9b 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -126,7 +126,6 @@ type module_typing_error =
| IncorrectWithConstraint of Label.t
| GenerativeModuleExpected of Label.t
| LabelMissing of Label.t * string
- | HigherOrderInclude
exception ModuleTypingError of module_typing_error
@@ -153,5 +152,3 @@ val error_incorrect_with_constraint : Label.t -> 'a
val error_generative_module_expected : Label.t -> 'a
val error_no_such_label_sub : Label.t->string->'a
-
-val error_higher_order_include : unit -> 'a
diff --git a/kernel/names.ml b/kernel/names.ml
index 480b37e8..ae2b3b63 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -453,6 +453,9 @@ module KNset = KNmap.Set
- when user and canonical parts differ, we cannot be in a section
anymore, hence the dirpath must be empty
- two pairs with the same user part should have the same canonical part
+ in a given environment (though with backtracking, the hash-table can
+ contains pairs with same user part but different canonical part from
+ a previous state of the session)
Note: since most of the time the canonical and user parts are equal,
we handle this case with a particular constructor to spare some memory *)
@@ -504,7 +507,7 @@ module KerPair = struct
let debug_print kp = str (debug_to_string kp)
(** For ordering kernel pairs, both user or canonical parts may make
- sense, according to your needs : user for the environments, canonical
+ sense, according to your needs: user for the environments, canonical
for other uses (ex: non-logical things). *)
module UserOrd = struct
@@ -521,16 +524,9 @@ module KerPair = struct
let hash x = KerName.hash (canonical x)
end
- (** Default comparison is on the canonical part *)
+ (** Default (logical) comparison and hash is on the canonical part *)
let equal = CanOrd.equal
-
- (** Hash-consing : we discriminate only on the user part, since having
- the same user part implies having the same canonical part
- (invariant of the system). *)
-
- let hash = function
- | Same kn -> KerName.hash kn
- | Dual (kn, _) -> KerName.hash kn
+ let hash = CanOrd.hash
module Self_Hashcons =
struct
@@ -539,8 +535,20 @@ module KerPair = struct
let hashcons hkn = function
| Same kn -> Same (hkn kn)
| Dual (knu,knc) -> make (hkn knu) (hkn knc)
- let equal x y = (user x) == (user y)
- let hash = hash
+ let equal x y = (* physical comparison on subterms *)
+ x == y ||
+ match x,y with
+ | Same x, Same y -> x == y
+ | Dual (ux,cx), Dual (uy,cy) -> ux == uy && cx == cy
+ | (Same _ | Dual _), _ -> false
+ (** Hash-consing (despite having the same user part implies having
+ the same canonical part is a logical invariant of the system, it
+ is not necessarily an invariant in memory, so we treat kernel
+ names as they are syntactically for hash-consing) *)
+ let hash = function
+ | Same kn -> KerName.hash kn
+ | Dual (knu, knc) ->
+ Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
end
module HashKP = Hashcons.Make(Self_Hashcons)
@@ -819,6 +827,10 @@ struct
let map f (c, b as x) =
let c' = f c in
if c' == c then x else (c', b)
+
+ let to_string p = Constant.to_string (constant p)
+ let print p = Constant.print (constant p)
+
end
type projection = Projection.t
diff --git a/kernel/names.mli b/kernel/names.mli
index 92ee58f2..7cc44437 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -652,6 +652,10 @@ module Projection : sig
val compare : t -> t -> int
val map : (constant -> constant) -> t -> t
+
+ val to_string : t -> string
+ val print : t -> Pp.std_ppcmds
+
end
type projection = Projection.t
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ada7ae73..98b2d6d2 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -195,7 +195,11 @@ module HashtblSymbol = Hashtbl.Make(HashedTypeSymbol)
let symb_tbl = HashtblSymbol.create 211
-let clear_symb_tbl () = HashtblSymbol.clear symb_tbl
+let clear_symbols () = HashtblSymbol.clear symb_tbl
+
+type symbols = symbol array
+
+let empty_symbols = [||]
let get_value tbl i =
match tbl.(i) with
@@ -250,7 +254,7 @@ let push_symbol x =
let symbols_tbl_name = Ginternal "symbols_tbl"
-let get_symbols_tbl () =
+let get_symbols () =
let tbl = Array.make (HashtblSymbol.length symb_tbl) dummy_symb in
HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl
@@ -477,7 +481,7 @@ and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 =
in
Array.equal eq_branch br1 br2
-(* hash_mllambda gn n env t computes the hash for t ignoring occurences of gn *)
+(* hash_mllambda gn n env t computes the hash for t ignoring occurrences of gn *)
let rec hash_mllambda gn n env t =
match t with
| MLlocal ln -> combinesmall 1 (LNmap.find ln env)
@@ -975,7 +979,7 @@ let compile_prim decl cond paux =
let args = Array.map opt_prim_aux args in
app_prim (Coq_primitive(op,None)) args
(*
- TODO: check if this inling was useful
+ TODO: check if this inlining was useful
begin match op with
| Int31lt ->
if Sys.word_size = 64 then
@@ -2008,16 +2012,20 @@ let rec compile_deps env sigma prefix ~interactive init t =
match kind_of_term t with
| Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
| Const c ->
- let c,u = get_allias env c in
+ let c,u = get_alias env c in
let cb,(nameref,_) = lookup_constant_key c env in
let (_, (_, const_updates)) = init in
if is_code_loaded ~interactive nameref
|| (Cmap_env.mem c const_updates)
then init
else
- let comp_stack, (mind_updates, const_updates) = match cb.const_body with
- | Def t ->
+ let comp_stack, (mind_updates, const_updates) =
+ match cb.const_proj, cb.const_body with
+ | None, Def t ->
compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
+ | Some pb, _ ->
+ let mind = pb.proj_ind in
+ compile_mind_deps env prefix ~interactive init mind
| _ -> init
in
let code, name =
@@ -2054,7 +2062,7 @@ let mk_internal_let s code =
(* ML Code for conversion function *)
let mk_conv_code env sigma prefix t1 t2 =
- clear_symb_tbl ();
+ clear_symbols ();
clear_global_tbl ();
let gl, (mind_updates, const_updates) =
let init = ([], empty_updates) in
@@ -2076,12 +2084,12 @@ let mk_conv_code env sigma prefix t1 t2 =
let setref2 = Glet(Ginternal "_", MLsetref("rt2",g2)) in
let gl = List.rev (setref2 :: setref1 :: t2 :: t1 :: gl) in
let header = Glet(Ginternal "symbols_tbl",
- MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+ MLapp (MLglobal (Ginternal "get_symbols"),
[|MLglobal (Ginternal "()")|])) in
header::gl, (mind_updates, const_updates)
let mk_norm_code env sigma prefix t =
- clear_symb_tbl ();
+ clear_symbols ();
clear_global_tbl ();
let gl, (mind_updates, const_updates) =
let init = ([], empty_updates) in
@@ -2094,14 +2102,14 @@ let mk_norm_code env sigma prefix t =
let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in
let gl = List.rev (setref :: t1 :: gl) in
let header = Glet(Ginternal "symbols_tbl",
- MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+ MLapp (MLglobal (Ginternal "get_symbols"),
[|MLglobal (Ginternal "()")|])) in
header::gl, (mind_updates, const_updates)
let mk_library_header dir =
let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in
[Glet(Ginternal "symbols_tbl",
- MLapp (MLglobal (Ginternal "get_library_symbols_tbl"),
+ MLapp (MLglobal (Ginternal "get_library_native_symbols"),
[|MLglobal (Ginternal libname)|]))]
let update_location (r,v) = r := v
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 893db92d..5d4c9e1e 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -22,29 +22,33 @@ val pp_global : Format.formatter -> global -> unit
val mk_open : string -> global
+(* Precomputed values for a compilation unit *)
type symbol
+type symbols
-val clear_symb_tbl : unit -> unit
+val empty_symbols : symbols
-val get_value : symbol array -> int -> Nativevalues.t
+val clear_symbols : unit -> unit
-val get_sort : symbol array -> int -> sorts
+val get_value : symbols -> int -> Nativevalues.t
-val get_name : symbol array -> int -> name
+val get_sort : symbols -> int -> sorts
-val get_const : symbol array -> int -> constant
+val get_name : symbols -> int -> name
-val get_match : symbol array -> int -> Nativevalues.annot_sw
+val get_const : symbols -> int -> constant
-val get_ind : symbol array -> int -> inductive
+val get_match : symbols -> int -> Nativevalues.annot_sw
-val get_meta : symbol array -> int -> metavariable
+val get_ind : symbols -> int -> inductive
-val get_evar : symbol array -> int -> existential
+val get_meta : symbols -> int -> metavariable
-val get_level : symbol array -> int -> Univ.Level.t
+val get_evar : symbols -> int -> existential
-val get_symbols_tbl : unit -> symbol array
+val get_level : symbols -> int -> Univ.Level.t
+
+val get_symbols : unit -> symbols
type code_location_update
type code_location_updates
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 75a3fc45..0242fd46 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -16,17 +16,21 @@ open Nativecode
(** This module implements the conversion test by compiling to OCaml code *)
-let rec conv_val env pb lvl cu v1 v2 =
- if v1 == v2 then ()
+let rec conv_val env pb lvl v1 v2 cu =
+ if v1 == v2 then cu
else
match kind_of_value v1, kind_of_value v2 with
- | Vaccu k1, Vaccu k2 ->
- conv_accu env pb lvl cu k1 k2
| Vfun f1, Vfun f2 ->
let v = mk_rel_accu lvl in
- conv_val env CONV (lvl+1) cu (f1 v) (f2 v)
+ conv_val env CONV (lvl+1) (f1 v) (f2 v) cu
+ | Vfun f1, _ ->
+ conv_val env CONV lvl v1 (fun x -> v2 x) cu
+ | _, Vfun f2 ->
+ conv_val env CONV lvl (fun x -> v1 x) v2 cu
+ | Vaccu k1, Vaccu k2 ->
+ conv_accu env pb lvl k1 k2 cu
| Vconst i1, Vconst i2 ->
- if not (Int.equal i1 i2) then raise NotConvertible
+ if Int.equal i1 i2 then cu else raise NotConvertible
| Vblock b1, Vblock b2 ->
let n1 = block_size b1 in
let n2 = block_size b2 in
@@ -34,77 +38,81 @@ let rec conv_val env pb lvl cu v1 v2 =
raise NotConvertible;
let rec aux lvl max b1 b2 i cu =
if Int.equal i max then
- conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i)
+ conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu
else
- (conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i);
- aux lvl max b1 b2 (i+1) cu)
+ let cu = conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in
+ aux lvl max b1 b2 (i+1) cu
in
aux lvl (n1-1) b1 b2 0 cu
- | Vfun f1, _ ->
- conv_val env CONV lvl cu v1 (fun x -> v2 x)
- | _, Vfun f2 ->
- conv_val env CONV lvl cu (fun x -> v1 x) v2
- | _, _ -> raise NotConvertible
+ | Vaccu _, _ | Vconst _, _ | Vblock _, _ -> raise NotConvertible
-and conv_accu env pb lvl cu k1 k2 =
+and conv_accu env pb lvl k1 k2 cu =
let n1 = accu_nargs k1 in
let n2 = accu_nargs k2 in
if not (Int.equal n1 n2) then raise NotConvertible;
if Int.equal n1 0 then
conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
else
- (conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu;
- List.iter2 (conv_val env CONV lvl cu) (args_of_accu k1) (args_of_accu k2))
+ let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
+ List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu
and conv_atom env pb lvl a1 a2 cu =
- if a1 == a2 then ()
+ if a1 == a2 then cu
else
match a1, a2 with
+ | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false
| Arel i1, Arel i2 ->
- if not (Int.equal i1 i2) then raise NotConvertible
- | Aind ind1, Aind ind2 ->
- if not (eq_puniverses eq_ind ind1 ind2) then raise NotConvertible
- | Aconstant c1, Aconstant c2 ->
- if not (eq_puniverses eq_constant c1 c2) then raise NotConvertible
+ if Int.equal i1 i2 then cu else raise NotConvertible
+ | Aind (ind1,u1), Aind (ind2,u2) ->
+ if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu
+ else raise NotConvertible
+ | Aconstant (c1,u1), Aconstant (c2,u2) ->
+ if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
+ else raise NotConvertible
| Asort s1, Asort s2 ->
- check_sort_cmp_universes env pb s1 s2 cu
+ sort_cmp_universes env pb s1 s2 cu
| Avar id1, Avar id2 ->
- if not (Id.equal id1 id2) then raise NotConvertible
+ if Id.equal id1 id2 then cu else raise NotConvertible
| Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
- conv_accu env CONV lvl cu ac1 ac2;
+ let cu = conv_accu env CONV lvl ac1 ac2 cu in
let tbl = a1.asw_reloc in
let len = Array.length tbl in
- if Int.equal len 0 then conv_val env CONV lvl cu p1 p2
+ if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu
else begin
- conv_val env CONV lvl cu p1 p2;
- let max = len - 1 in
- let rec aux i =
- let tag,arity = tbl.(i) in
- let ci =
- if Int.equal arity 0 then mk_const tag
- else mk_block tag (mk_rels_accu lvl arity) in
- let bi1 = bs1 ci and bi2 = bs2 ci in
- if Int.equal i max then conv_val env CONV (lvl + arity) cu bi1 bi2
- else (conv_val env CONV (lvl + arity) cu bi1 bi2; aux (i+1)) in
- aux 0
+ let cu = conv_val env CONV lvl p1 p2 cu in
+ let max = len - 1 in
+ let rec aux i cu =
+ let tag,arity = tbl.(i) in
+ let ci =
+ if Int.equal arity 0 then mk_const tag
+ else mk_block tag (mk_rels_accu lvl arity) in
+ let bi1 = bs1 ci and bi2 = bs2 ci in
+ if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu
+ else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in
+ aux 0 cu
end
| Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) ->
if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible;
- if f1 == f2 then ()
+ if f1 == f2 then cu
else conv_fix env lvl t1 f1 t2 f2 cu
| (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)),
(Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) ->
if not (Int.equal s1 s2) then raise NotConvertible;
- if f1 == f2 then ()
+ if f1 == f2 then cu
else
if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
else conv_fix env lvl t1 f1 t2 f2 cu
| Aprod(_,d1,c1), Aprod(_,d2,c2) ->
- conv_val env CONV lvl cu d1 d2;
- let v = mk_rel_accu lvl in
- conv_val env pb (lvl + 1) cu (d1 v) (d2 v)
- | _, _ -> raise NotConvertible
+ let cu = conv_val env CONV lvl d1 d2 cu in
+ let v = mk_rel_accu lvl in
+ conv_val env pb (lvl + 1) (d1 v) (d2 v) cu
+ | Aproj(p1,ac1), Aproj(p2,ac2) ->
+ if not (Constant.equal p1 p2) then raise NotConvertible
+ else conv_accu env CONV lvl ac1 ac2 cu
+ | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _
+ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _
+ | Aproj _, _ -> raise NotConvertible
(* Precondition length t1 = length f1 = length f2 = length t2 *)
and conv_fix env lvl t1 f1 t2 f2 cu =
@@ -112,22 +120,15 @@ and conv_fix env lvl t1 f1 t2 f2 cu =
let max = len - 1 in
let fargs = mk_rels_accu lvl len in
let flvl = lvl + len in
- let rec aux i =
- conv_val env CONV lvl cu t1.(i) t2.(i);
+ let rec aux i cu =
+ let cu = conv_val env CONV lvl t1.(i) t2.(i) cu in
let fi1 = napply f1.(i) fargs in
let fi2 = napply f2.(i) fargs in
- if Int.equal i max then conv_val env CONV flvl cu fi1 fi2
- else (conv_val env CONV flvl cu fi1 fi2; aux (i+1)) in
- aux 0
+ if Int.equal i max then conv_val env CONV flvl fi1 fi2 cu
+ else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in
+ aux 0 cu
-let native_conv pb sigma env t1 t2 =
- if !Flags.no_native_compiler then begin
- let msg = "Native compiler is disabled, "^
- "falling back to VM conversion test." in
- Pp.msg_warning (Pp.str msg);
- vm_conv pb env t1 t2
- end
- else
+let native_conv_gen pb sigma env univs t1 t2 =
let penv = Environ.pre_env env in
let ml_filename, prefix = get_ml_filename () in
let code, upds = mk_conv_code penv sigma prefix t1 t2 in
@@ -141,8 +142,25 @@ let native_conv pb sigma env t1 t2 =
let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
if !Flags.debug then Pp.msg_debug (Pp.str time_info);
(* TODO change 0 when we can have deBruijn *)
- conv_val env pb 0 (Environ.universes env) !rt1 !rt2
+ fst (conv_val env pb 0 !rt1 !rt2 univs)
end
| _ -> anomaly (Pp.str "Compilation failure")
-let _ = set_nat_conv native_conv
+(* Wrapper for [native_conv] above *)
+let native_conv cv_pb sigma env t1 t2 =
+ if Coq_config.no_native_compiler then begin
+ let msg = "Native compiler is disabled, falling back to VM conversion test." in
+ Pp.msg_warning (Pp.str msg);
+ vm_conv cv_pb env t1 t2
+ end
+ else
+ let univs = Environ.universes env in
+ let b =
+ if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2
+ else Constr.eq_constr_univs univs t1 t2
+ in
+ if not b then
+ let univs = (univs, checked_universes) in
+ let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in
+ let t2 = Term.it_mkLambda_or_LetIn t2 (Environ.rel_context env) in
+ let _ = native_conv_gen cv_pb sigma env univs t1 t2 in ()
diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli
index 318a7d83..4dddb9fd 100644
--- a/kernel/nativeconv.mli
+++ b/kernel/nativeconv.mli
@@ -12,3 +12,7 @@ open Nativelambda
(** This module implements the conversion test by compiling to OCaml code *)
val native_conv : conv_pb -> evars -> types conversion_function
+
+(** A conversion function parametrized by a universe comparator. Used outside of
+ the kernel. *)
+val native_conv_gen : conv_pb -> evars -> (types, 'a) generic_conversion_function
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 383f8102..4d033bc9 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -277,7 +277,7 @@ and reduce_lapp substf lids body substa largs =
| [], _::_ -> simplify_app substf body substa (Array.of_list largs)
-(* [occurence kind k lam]:
+(* [occurrence kind k lam]:
If [kind] is [true] return [true] if the variable [k] does not appear in
[lam], return [false] if the variable appear one time and not
under a lambda, a fixpoint, a cofixpoint; else raise Not_found.
@@ -285,7 +285,7 @@ and reduce_lapp substf lids body substa largs =
else raise [Not_found]
*)
-let rec occurence k kind lam =
+let rec occurrence k kind lam =
match lam with
| Lrel (_,n) ->
if Int.equal n k then
@@ -294,35 +294,35 @@ let rec occurence k kind lam =
| Lvar _ | Lconst _ | Lproj _ | Luint _ | Lval _ | Lsort _ | Lind _
| Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> kind
| Lprod(dom, codom) ->
- occurence k (occurence k kind dom) codom
+ occurrence k (occurrence k kind dom) codom
| Llam(ids,body) ->
- let _ = occurence (k+Array.length ids) false body in kind
+ let _ = occurrence (k+Array.length ids) false body in kind
| Llet(_,def,body) ->
- occurence (k+1) (occurence k kind def) body
+ occurrence (k+1) (occurrence k kind def) body
| Lapp(f, args) ->
- occurence_args k (occurence k kind f) args
+ occurrence_args k (occurrence k kind f) args
| Lprim(_,_,_,args) | Lmakeblock(_,_,_,args) ->
- occurence_args k kind args
+ occurrence_args k kind args
| Lcase(_,t,a,br) ->
- let kind = occurence k (occurence k kind t) a in
+ let kind = occurrence k (occurrence k kind t) a in
let r = ref kind in
Array.iter (fun (_,ids,c) ->
- r := occurence (k+Array.length ids) kind c && !r) br;
+ r := occurrence (k+Array.length ids) kind c && !r) br;
!r
| Lif (t, bt, bf) ->
- let kind = occurence k kind t in
- kind && occurence k kind bt && occurence k kind bf
+ let kind = occurrence k kind t in
+ kind && occurrence k kind bt && occurrence k kind bf
| Lfix(_,(ids,ltypes,lbodies))
| Lcofix(_,(ids,ltypes,lbodies)) ->
- let kind = occurence_args k kind ltypes in
- let _ = occurence_args (k+Array.length ids) false lbodies in
+ let kind = occurrence_args k kind ltypes in
+ let _ = occurrence_args (k+Array.length ids) false lbodies in
kind
-and occurence_args k kind args =
- Array.fold_left (occurence k) kind args
+and occurrence_args k kind args =
+ Array.fold_left (occurrence k) kind args
let occur_once lam =
- try let _ = occurence 1 true lam in true
+ try let _ = occurrence 1 true lam in true
with Not_found -> false
(* [remove_let lam] remove let expression in [lam] if the variable is *)
@@ -373,13 +373,13 @@ let makeblock env cn u tag args =
(* Translation of constants *)
-let rec get_allias env (kn, u as p) =
+let rec get_alias env (kn, u as p) =
let tps = (lookup_constant kn env).const_body_code in
match tps with
| None -> p
| Some tps ->
match Cemitcodes.force tps with
- | Cemitcodes.BCallias kn' -> get_allias env kn'
+ | Cemitcodes.BCalias kn' -> get_alias env (kn', u)
| _ -> p
(*i Global environment *)
@@ -651,7 +651,7 @@ let rec lambda_of_constr env sigma c =
and lambda_of_app env sigma f args =
match kind_of_term f with
| Const (kn,u as c) ->
- let kn,u = get_allias !global_env c in
+ let kn,u = get_alias !global_env c in
let cb = lookup_constant kn !global_env in
(try
let prefix = get_const_prefix !global_env kn in
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index ccf2888b..3b6fafbb 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -26,7 +26,7 @@ val mk_lazy : lambda -> lambda
val get_mind_prefix : env -> mutual_inductive -> string
-val get_allias : env -> pconstant -> pconstant
+val get_alias : env -> pconstant -> pconstant
val lambda_of_constr : env -> evars -> Constr.constr -> lambda
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 605c1225..b2142b43 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -94,7 +94,10 @@ let compile_library dir code fn =
let basename = Filename.basename fn in
let dirname = Filename.dirname fn in
let dirname = dirname / output_dir in
- if not (Sys.file_exists dirname) then Unix.mkdir dirname 0o755;
+ let () =
+ try Unix.mkdir dirname 0o755
+ with Unix.Unix_error (Unix.EEXIST, _, _) -> ()
+ in
let fn = dirname / basename in
write_ml_code fn ~header code;
let r = fst (call_compiler fn) in
@@ -102,22 +105,25 @@ let compile_library dir code fn =
r
(* call_linker links dynamically the code for constants in environment or a *)
-(* conversion test. Silently fails if the file does not exist in bytecode *)
-(* mode, since the standard library is not compiled to bytecode with default *)
-(* settings. *)
+(* conversion test. *)
let call_linker ?(fatal=true) prefix f upds =
rt1 := dummy_value ();
rt2 := dummy_value ();
- if Dynlink.is_native || Sys.file_exists f then
+ if not (Sys.file_exists f) then
+ begin
+ let msg = "Cannot find native compiler file " ^ f in
+ if fatal then Errors.error msg
+ else if !Flags.debug then Pp.msg_debug (Pp.str msg)
+ end
+ else
(try
if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
register_native_file prefix
- with | Dynlink.Error e ->
- let msg = "Dynlink error, " ^ Dynlink.error_message e in
- if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg)
- | e when Errors.noncritical e ->
- if fatal then anomaly (Errors.print e)
- else Pp.msg_warning (Errors.print_no_report e));
+ with Dynlink.Error e as exn ->
+ let exn = Errors.push exn in
+ let msg = "Dynlink error, " ^ Dynlink.error_message e in
+ if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
+ else if !Flags.debug then Pp.msg_debug (Pp.str msg));
match upds with Some upds -> update_locations upds | _ -> ()
let link_library ~prefix ~dirname ~basename =
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 0b8662ff..443cd8c2 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -62,12 +62,12 @@ let dump_library mp dp env mod_expr =
let prefix = mod_uid_of_dirpath dp ^ "." in
let t0 = Sys.time () in
clear_global_tbl ();
- clear_symb_tbl ();
+ clear_symbols ();
let mlcode =
List.fold_left (translate_field prefix mp env) [] struc
in
let t1 = Sys.time () in
let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in
let mlcode = add_header_comment (List.rev mlcode) time_info in
- mlcode, get_symbols_tbl ()
+ mlcode, get_symbols ()
| _ -> assert false
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index a66fb715..29368d14 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -14,4 +14,4 @@ open Nativecode
compiler *)
val dump_library : module_path -> dir_path -> env -> module_signature ->
- global list * symbol array
+ global list * symbols
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index e4a77999..40bef4bc 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -10,7 +10,7 @@ open Names
open Errors
open Util
-(** This modules defines the representation of values internally used by
+(** This module defines the representation of values internally used by
the native compiler *)
type t = t -> t
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 9f4361f4..badb15b5 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -43,7 +43,10 @@ let set_indirect_univ_accessor f = (get_univ := f)
let create cu = Direct ([],cu)
let turn_indirect dp o (prfs,odp) = match o with
- | Indirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque")
+ | Indirect (_,_,i) ->
+ if not (Int.Map.mem i prfs)
+ then Errors.anomaly (Pp.str "Indirect in a different table")
+ else Errors.anomaly (Pp.str "Already an indirect opaque")
| Direct (d,cu) ->
let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
let id = Int.Map.cardinal prfs in
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 557ed3d7..5f3f559a 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -46,8 +46,7 @@ type globals = {
type stratification = {
env_universes : universes;
- env_engagement : engagement option;
- env_type_in_type : bool
+ env_engagement : engagement
}
type val_kind =
@@ -95,8 +94,7 @@ let empty_env = {
env_nb_rel = 0;
env_stratification = {
env_universes = initial_universes;
- env_engagement = None;
- env_type_in_type = false};
+ env_engagement = (PredicativeSet,StratifiedType) };
env_conv_oracle = Conv_oracle.empty;
retroknowledge = Retroknowledge.initial_retroknowledge;
indirect_pterms = Opaqueproof.empty_opaquetab }
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 03ac41b4..0ce0bed2 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -33,8 +33,7 @@ type globals = {
type stratification = {
env_universes : universes;
- env_engagement : engagement option;
- env_type_in_type : bool
+ env_engagement : engagement
}
type lazy_val
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b09367dd..892557ac 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -26,8 +26,6 @@ open Environ
open Closure
open Esubst
-let left2right = ref false
-
let rec is_empty_stack = function
[] -> true
| Zupdate _::s -> is_empty_stack s
@@ -175,7 +173,7 @@ let is_cumul = function CUMUL -> true | CONV -> false
type 'a universe_compare =
{ (* Might raise NotConvertible *)
compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
- compare_instances: bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+ compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
}
type 'a universe_state = 'a * 'a universe_compare
@@ -187,8 +185,10 @@ type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.co
let sort_cmp_universes env pb s0 s1 (u, check) =
(check.compare env pb s0 s1 u, check)
-let convert_instances flex u u' (s, check) =
- (check.compare_instances flex u u' s, check)
+(* [flex] should be true for constants, false for inductive types and
+ constructors. *)
+let convert_instances ~flex u u' (s, check) =
+ (check.compare_instances ~flex u u' s, check)
let conv_table_key infos k1 k2 cuniv =
if k1 == k2 then cuniv else
@@ -198,7 +198,7 @@ let conv_table_key infos k1 k2 cuniv =
else
let flex = evaluable_constant cst (info_env infos)
&& RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst)
- in convert_instances flex u u' cuniv
+ in convert_instances ~flex u u' cuniv
| VarKey id, VarKey id' when Id.equal id id' -> cuniv
| RelKey n, RelKey n' when Int.equal n n' -> cuniv
| _ -> raise NotConvertible
@@ -210,9 +210,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
let cu1 = cmp_rec s1 s2 cuniv in
(match (z1,z2) with
| (Zlapp a1,Zlapp a2) ->
- if !left2right then
- Array.fold_left2 (fun cu x y -> f x y cu) cu1 a1 a2
- else Array.fold_right2 f a1 a2 cu1
+ Array.fold_right2 f a1 a2 cu1
| (Zlproj (c1,l1),Zlproj (c2,l2)) ->
if not (eq_constant c1 c2) then
raise NotConvertible
@@ -594,7 +592,7 @@ let check_sort_cmp_universes env pb s0 s1 univs =
let checked_sort_cmp_universes env pb s0 s1 univs =
check_sort_cmp_universes env pb s0 s1 univs; univs
-let check_convert_instances _flex u u' univs =
+let check_convert_instances ~flex u u' univs =
if Univ.Instance.check_eq univs u u' then univs
else raise NotConvertible
@@ -634,10 +632,10 @@ let infer_cmp_universes env pb s0 s1 univs =
| CONV -> infer_eq univs u1 u2)
else univs
-let infer_convert_instances flex u u' (univs,cstrs) =
+let infer_convert_instances ~flex u u' (univs,cstrs) =
(univs, Univ.enforce_eq_instances u u' cstrs)
-let infered_universes : (Univ.universes * Univ.Constraint.t) universe_compare =
+let inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare =
{ compare = infer_cmp_universes;
compare_instances = infer_convert_instances }
@@ -670,7 +668,7 @@ let trans_conv_universes ?(l2r=false) ?(evars=fun _->None) reds =
let trans_conv_leq_universes ?(l2r=false) ?(evars=fun _->None) reds =
trans_fconv_universes reds CUMUL l2r evars
-let fconv = trans_fconv (Id.Pred.full, Cpred.full)
+let fconv = trans_fconv full_transparent_state
let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None)
let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars
@@ -685,7 +683,7 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
v1
v2
-let generic_conv cv_pb l2r evars reds env univs t1 t2 =
+let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
let (s, _) =
clos_fconv reds cv_pb l2r evars env univs t1 t2
in s
@@ -697,7 +695,7 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
in
if b then cstrs
else
- let univs = ((univs, Univ.Constraint.empty), infered_universes) in
+ let univs = ((univs, Univ.Constraint.empty), inferred_universes) in
let ((_,cstrs), _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in
cstrs
@@ -716,39 +714,19 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta
env univs t1 t2 =
infer_conv_universes CUMUL l2r evars ts env univs t1 t2
-(* option for conversion *)
-let nat_conv = ref (fun cv_pb sigma ->
- fconv cv_pb false (sigma.Nativelambda.evars_val))
-let set_nat_conv f = nat_conv := f
-
-let native_conv cv_pb sigma env t1 t2 =
- if eq_constr t1 t2 then ()
- else begin
- let t1 = (it_mkLambda_or_LetIn t1 (rel_context env)) in
- let t2 = (it_mkLambda_or_LetIn t2 (rel_context env)) in
- !nat_conv cv_pb sigma env t1 t2
- end
-
+(* This reference avoids always having to link C code with the kernel *)
let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
let set_vm_conv f = vm_conv := f
let vm_conv cv_pb env t1 t2 =
try
!vm_conv cv_pb env t1 t2
with Not_found | Invalid_argument _ ->
- (* If compilation fails, fall-back to closure conversion *)
- fconv cv_pb false (fun _->None) env t1 t2
-
-
-let default_conv = ref (fun cv_pb ?(l2r=false) -> fconv cv_pb l2r (fun _->None))
-
-let set_default_conv f = default_conv := f
+ (Pp.msg_warning
+ (Pp.str "Bytecode compilation failed, falling back to default conversion");
+ fconv cv_pb false (fun _->None) env t1 t2)
let default_conv cv_pb ?(l2r=false) env t1 t2 =
- try
- !default_conv ~l2r cv_pb env t1 t2
- with Not_found | Invalid_argument _ ->
- (* If compilation fails, fall-back to closure conversion *)
- fconv cv_pb false (fun _->None) env t1 t2
+ fconv cv_pb false (fun _ -> None) env t1 t2
let default_conv_leq = default_conv CUMUL
(*
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 6ced5c49..0df26d62 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -10,8 +10,6 @@ open Term
open Context
open Environ
-val left2right : bool ref
-
(***********************************************************************
s Reduction functions *)
@@ -39,7 +37,7 @@ type conv_pb = CONV | CUMUL
type 'a universe_compare =
{ (* Might raise NotConvertible *)
compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
- compare_instances: bool (* Instance of a flexible constant? *) ->
+ compare_instances: flex:bool ->
Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
}
@@ -49,14 +47,16 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints
-val check_sort_cmp_universes :
- env -> conv_pb -> sorts -> sorts -> Univ.universes -> unit
+val sort_cmp_universes : env -> conv_pb -> sorts -> sorts ->
+ 'a * 'a universe_compare -> 'a * 'a universe_compare
-(* val sort_cmp : *)
-(* conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *)
+(* [flex] should be true for constants, false for inductive types and
+constructors. *)
+val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t ->
+ 'a * 'a universe_compare -> 'a * 'a universe_compare
-(* val conv_sort : sorts conversion_function *)
-(* val conv_sort_leq : sorts conversion_function *)
+val checked_universes : Univ.universes universe_compare
+val inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare
val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function
val trans_conv :
@@ -77,23 +77,20 @@ val conv_leq :
val conv_leq_vecti :
?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function
+(** These conversion functions are used by module subtyping, which needs to infer
+ universe constraints inside the kernel *)
val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) ->
?ts:Names.transparent_state -> constr infer_conversion_function
val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) ->
?ts:Names.transparent_state -> types infer_conversion_function
-val generic_conv : conv_pb -> bool -> (existential->constr option) ->
+val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) ->
Names.transparent_state -> (constr,'a) generic_conversion_function
(** option for conversion *)
val set_vm_conv : (conv_pb -> types conversion_function) -> unit
val vm_conv : conv_pb -> types conversion_function
-val set_nat_conv :
- (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit
-val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function
-
-val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit
val default_conv : conv_pb -> ?l2r:bool -> types conversion_function
val default_conv_leq : ?l2r:bool -> types conversion_function
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d762a246..e0a07dcc 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -81,8 +81,7 @@ open Declarations
These fields could be deduced from [revstruct], but they allow faster
name freshness checks.
- [univ] and [future_cst] : current and future universe constraints
- - [engagement] : are we Set-impredicative?
- - [type_in_type] : does the universe hierarchy collapse?
+ - [engagement] : are we Set-impredicative? does the universe hierarchy collapse?
- [required] : names and digests of Require'd libraries since big-bang.
This field will only grow
- [loads] : list of libraries Require'd inside the current module.
@@ -119,13 +118,13 @@ type safe_environment =
revstruct : structure_body;
modlabels : Label.Set.t;
objlabels : Label.Set.t;
- univ : Univ.constraints;
- future_cst : Univ.constraints Future.computation list;
+ univ : Univ.ContextSet.t;
+ future_cst : Univ.ContextSet.t Future.computation list;
engagement : engagement option;
- type_in_type : bool;
required : vodigest DPMap.t;
loads : (module_path * module_body) list;
- local_retroknowledge : Retroknowledge.action list }
+ local_retroknowledge : Retroknowledge.action list;
+ native_symbols : Nativecode.symbols DPMap.t }
and modvariant =
| NONE
@@ -149,12 +148,12 @@ let empty_environment =
modlabels = Label.Set.empty;
objlabels = Label.Set.empty;
future_cst = [];
- univ = Univ.Constraint.empty;
+ univ = Univ.ContextSet.empty;
engagement = None;
- type_in_type = false;
required = DPMap.empty;
loads = [];
- local_retroknowledge = [] }
+ local_retroknowledge = [];
+ native_symbols = DPMap.empty }
let is_initial senv =
match senv.revstruct, senv.modvariant with
@@ -182,16 +181,20 @@ let set_engagement c senv =
(** Check that the engagement [c] expected by a library matches
the current (initial) one *)
-let check_engagement env c =
- match Environ.engagement env, c with
- | None, Some ImpredicativeSet ->
- Errors.error "Needs option -impredicative-set."
- | _ -> ()
-
-let set_type_in_type senv =
- { senv with
- env = Environ.set_type_in_type senv.env;
- type_in_type = true }
+let check_engagement env (expected_impredicative_set,expected_type_in_type) =
+ let impredicative_set,type_in_type = Environ.engagement env in
+ begin
+ match impredicative_set, expected_impredicative_set with
+ | PredicativeSet, ImpredicativeSet ->
+ Errors.error "Needs option -impredicative-set."
+ | _ -> ()
+ end;
+ begin
+ match type_in_type, expected_type_in_type with
+ | StratifiedType, TypeInType ->
+ Errors.error "Needs option -type-in-type."
+ | _ -> ()
+ end
(** {6 Stm machinery } *)
@@ -204,36 +207,79 @@ let get_opaque_body env cbo =
(Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
-let sideff_of_con env c =
+type private_constant = Entries.side_effect
+type private_constants = private_constant list
+
+type private_constant_role = Term_typing.side_effect_role =
+ | Subproof
+ | Schema of inductive * string
+
+let empty_private_constants = []
+let add_private x xs = x :: xs
+let concat_private xs ys = xs @ ys
+let mk_pure_proof = Term_typing.mk_pure_proof
+let inline_private_constants_in_constr = Term_typing.inline_side_effects
+let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
+let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
+
+let constant_entry_of_private_constant = function
+ | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
+ [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ]
+ | { Entries.eff = Entries.SEscheme (l,_) } ->
+ List.map (fun (_,kn,cb,eff_env) ->
+ kn, Term_typing.constant_entry_of_side_effect cb eff_env) l
+
+let private_con_of_con env c =
let cbo = Environ.lookup_constant c env.env in
- SEsubproof (c, cbo, get_opaque_body env.env cbo)
-let sideff_of_scheme kind env cl =
- SEscheme(
- List.map (fun (i,c) ->
- let cbo = Environ.lookup_constant c env.env in
- i, c, cbo, get_opaque_body env.env cbo) cl,
- kind)
+ { Entries.from_env = Ephemeron.create env.revstruct;
+ Entries.eff = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) }
+
+let private_con_of_scheme ~kind env cl =
+ { Entries.from_env = Ephemeron.create env.revstruct;
+ Entries.eff = Entries.SEscheme(
+ List.map (fun (i,c) ->
+ let cbo = Environ.lookup_constant c env.env in
+ i, c, cbo, get_opaque_body env.env cbo) cl,
+ kind) }
+
+let universes_of_private eff =
+ let open Declarations in
+ List.fold_left (fun acc { Entries.eff } ->
+ match eff with
+ | Entries.SEscheme (l,s) ->
+ List.fold_left (fun acc (_,_,cb,c) ->
+ let acc = match c with
+ | `Nothing -> acc
+ | `Opaque (_, ctx) -> ctx :: acc in
+ if cb.const_polymorphic then acc
+ else (Univ.ContextSet.of_context cb.const_universes) :: acc)
+ acc l
+ | Entries.SEsubproof (c, cb, e) ->
+ if cb.const_polymorphic then acc
+ else Univ.ContextSet.of_context cb.const_universes :: acc)
+ [] eff
let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env
type constraints_addition =
- Now of Univ.constraints | Later of Univ.constraints Future.computation
+ | Now of bool * Univ.ContextSet.t
+ | Later of Univ.ContextSet.t Future.computation
let add_constraints cst senv =
match cst with
| Later fc ->
{senv with future_cst = fc :: senv.future_cst}
- | Now cst ->
+ | Now (poly,cst) ->
{ senv with
- env = Environ.add_constraints cst senv.env;
- univ = Univ.Constraint.union cst senv.univ }
+ env = Environ.push_context_set ~strict:(not poly) cst senv.env;
+ univ = Univ.ContextSet.union cst senv.univ }
let add_constraints_list cst senv =
- List.fold_right add_constraints cst senv
+ List.fold_left (fun acc c -> add_constraints c acc) senv cst
-let push_context_set ctx = add_constraints (Now (Univ.ContextSet.constraints ctx))
-let push_context ctx = add_constraints (Now (Univ.UContext.constraints ctx))
+let push_context_set poly ctx = add_constraints (Now (poly,ctx))
+let push_context poly ctx = add_constraints (Now (poly,Univ.ContextSet.of_context ctx))
let is_curmod_library senv =
match senv.modvariant with LIBRARY -> true | _ -> false
@@ -243,9 +289,11 @@ let join_safe_environment ?(except=Future.UUIDSet.empty) e =
List.fold_left
(fun e fc ->
if Future.UUIDSet.mem (Future.uuid fc) except then e
- else add_constraints (Now (Future.join fc)) e)
+ else add_constraints (Now (false, Future.join fc)) e)
{e with future_cst = []} e.future_cst
+let is_joined_environment e = List.is_empty e.future_cst
+
(** {6 Various checks } *)
let exists_modlabel l senv = Label.Set.mem l senv.modlabels
@@ -331,21 +379,22 @@ let safe_push_named (id,_,_ as d) env =
let push_named_def (id,de) senv =
- let c,typ,univs = Term_typing.translate_local_def senv.env id de in
- let senv' = push_context univs senv in
- let c, senv' = match c with
- | Def c -> Mod_subst.force_constr c, senv'
+ let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in
+ let poly = de.Entries.const_entry_polymorphic in
+ let univs = Univ.ContextSet.of_context univs in
+ let c, univs = match c with
+ | Def c -> Mod_subst.force_constr c, univs
| OpaqueDef o ->
- Opaqueproof.force_proof (Environ.opaque_tables senv'.env) o,
- push_context_set
- (Opaqueproof.force_constraints (Environ.opaque_tables senv'.env) o)
- senv'
+ Opaqueproof.force_proof (Environ.opaque_tables senv.env) o,
+ Univ.ContextSet.union univs
+ (Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o)
| _ -> assert false in
+ let senv' = push_context_set poly univs senv in
let env'' = safe_push_named (id,Some c,typ) senv'.env in
- {senv' with env=env''}
+ univs, {senv' with env=env''}
-let push_named_assum ((id,t),ctx) senv =
- let senv' = push_context_set ctx senv in
+let push_named_assum ((id,t,poly),ctx) senv =
+ let senv' = push_context_set poly ctx senv in
let t = Term_typing.translate_local_assum senv'.env t in
let env'' = safe_push_named (id,None,t) senv'.env in
{senv' with env=env''}
@@ -368,10 +417,10 @@ let labels_of_mib mib =
let globalize_constant_universes env cb =
if cb.const_polymorphic then
- [Now Univ.Constraint.empty]
+ [Now (true, Univ.ContextSet.empty)]
else
- let cstrs = Univ.UContext.constraints cb.const_universes in
- Now cstrs ::
+ let cstrs = Univ.ContextSet.of_context cb.const_universes in
+ Now (false, cstrs) ::
(match cb.const_body with
| (Undef _ | Def _) -> []
| OpaqueDef lc ->
@@ -379,23 +428,21 @@ let globalize_constant_universes env cb =
| None -> []
| Some fc ->
match Future.peek_val fc with
- | None -> [Later (Future.chain
- ~greedy:(not (Future.is_exn fc))
- ~pure:true fc Univ.ContextSet.constraints)]
- | Some c -> [Now (Univ.ContextSet.constraints c)])
+ | None -> [Later fc]
+ | Some c -> [Now (false, c)])
let globalize_mind_universes mb =
if mb.mind_polymorphic then
- [Now Univ.Constraint.empty]
+ [Now (true, Univ.ContextSet.empty)]
else
- [Now (Univ.UContext.constraints mb.mind_universes)]
+ [Now (false, Univ.ContextSet.of_context mb.mind_universes)]
let constraints_of_sfb env sfb =
match sfb with
| SFBconst cb -> globalize_constant_universes env cb
| SFBmind mib -> globalize_mind_universes mib
- | SFBmodtype mtb -> [Now mtb.mod_constraints]
- | SFBmodule mb -> [Now mb.mod_constraints]
+ | SFBmodtype mtb -> [Now (false, mtb.mod_constraints)]
+ | SFBmodule mb -> [Now (false, mb.mod_constraints)]
(** A generic function for adding a new field in a same environment.
It also performs the corresponding [add_constraints]. *)
@@ -437,19 +484,16 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
(** Insertion of constants and parameters in environment *)
type global_declaration =
- | ConstantEntry of Entries.constant_entry
+ | ConstantEntry of bool * private_constants Entries.constant_entry
| GlobalRecipe of Cooking.recipe
-let add_constant dir l decl senv =
- let kn = make_con senv.modpath dir l in
- let cb = match decl with
- | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce
- | GlobalRecipe r ->
- let cb = Term_typing.translate_recipe senv.env kn r in
- if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
- in
+type exported_private_constant =
+ constant * private_constants Entries.constant_entry * private_constant_role
+
+let add_constant_aux no_section senv (kn, cb) =
+ let l = pi3 (Constant.repr3 kn) in
let cb, otab = match cb.const_body with
- | OpaqueDef lc when DirPath.is_empty dir ->
+ | OpaqueDef lc when no_section ->
(* In coqc, opaque constants outside sections will be stored
indirectly in a specific table *)
let od, otab =
@@ -466,7 +510,32 @@ let add_constant dir l decl senv =
(Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv'
| _ -> senv'
in
- kn, senv''
+ senv''
+
+let add_constant dir l decl senv =
+ let kn = make_con senv.modpath dir l in
+ let no_section = DirPath.is_empty dir in
+ let seff_to_export, decl =
+ match decl with
+ | ConstantEntry (true, ce) ->
+ let exports, ce =
+ Term_typing.export_side_effects senv.revstruct senv.env ce in
+ exports, ConstantEntry (false, ce)
+ | _ -> [], decl
+ in
+ let senv =
+ List.fold_left (add_constant_aux no_section) senv
+ (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in
+ let senv =
+ let cb =
+ match decl with
+ | ConstantEntry (export_seff,ce) ->
+ Term_typing.translate_constant senv.revstruct senv.env kn ce
+ | GlobalRecipe r ->
+ let cb = Term_typing.translate_recipe senv.env kn r in
+ if no_section then Declareops.hcons_const_body cb else cb in
+ add_constant_aux no_section senv (kn, cb) in
+ (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv
(** Insertion of inductive types *)
@@ -498,13 +567,13 @@ let add_modtype l params_mte inl senv =
(** full_add_module adds module with universes and constraints *)
let full_add_module mb senv =
- let senv = add_constraints (Now mb.mod_constraints) senv in
+ let senv = add_constraints (Now (false, mb.mod_constraints)) senv in
let dp = ModPath.dp mb.mod_mp in
let linkinfo = Nativecode.link_info_of_dirpath dp in
{ senv with env = Modops.add_linked_module mb linkinfo senv.env }
let full_add_module_type mp mt senv =
- let senv = add_constraints (Now mt.mod_constraints) senv in
+ let senv = add_constraints (Now (false, mt.mod_constraints)) senv in
{ senv with env = Modops.add_module_type mp mt senv.env }
(** Insertion of modules *)
@@ -612,8 +681,8 @@ let propagate_senv newdef newenv newresolver senv oldsenv =
modlabels = Label.Set.add (fst newdef) oldsenv.modlabels;
univ =
List.fold_left (fun acc cst ->
- Univ.Constraint.union acc (Future.force cst))
- (Univ.Constraint.union senv.univ oldsenv.univ)
+ Univ.ContextSet.union acc (Future.force cst))
+ (Univ.ContextSet.union senv.univ oldsenv.univ)
now_cst;
future_cst = later_cst @ oldsenv.future_cst;
(* engagement is propagated to the upper level *)
@@ -621,7 +690,8 @@ let propagate_senv newdef newenv newresolver senv oldsenv =
required = senv.required;
loads = senv.loads@oldsenv.loads;
local_retroknowledge =
- senv.local_retroknowledge@oldsenv.local_retroknowledge }
+ senv.local_retroknowledge@oldsenv.local_retroknowledge;
+ native_symbols = senv.native_symbols}
let end_module l restype senv =
let mp = senv.modpath in
@@ -635,8 +705,8 @@ let end_module l restype senv =
let senv'=
propagate_loads { senv with
env = newenv;
- univ = Univ.Constraint.union senv.univ mb.mod_constraints} in
- let newenv = Environ.add_constraints mb.mod_constraints senv'.env in
+ univ = Univ.ContextSet.union senv.univ mb.mod_constraints} in
+ let newenv = Environ.push_context_set ~strict:true mb.mod_constraints senv'.env in
let newenv = Modops.add_module mb newenv in
let newresolver =
if Modops.is_functor mb.mod_type then oldsenv.modresolver
@@ -661,7 +731,7 @@ let end_modtype l senv =
let () = check_empty_context senv in
let mbids = List.rev_map fst params in
let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
- let newenv = Environ.add_constraints senv.univ newenv in
+ let newenv = Environ.push_context_set ~strict:true senv.univ newenv in
let newenv = set_engagement_opt newenv senv.engagement in
let senv' = propagate_loads {senv with env=newenv} in
let auto_tb = functorize params (NoFunctor (List.rev senv.revstruct)) in
@@ -676,38 +746,32 @@ let end_modtype l senv =
let add_include me is_module inl senv =
let open Mod_typing in
let mp_sup = senv.modpath in
- let sign,cst,resolver =
- if is_module then
- let sign,_,reso,cst = translate_mse_incl senv.env mp_sup inl me in
- sign,cst,reso
- else
- let mtb = translate_modtype senv.env mp_sup inl ([],me) in
- mtb.mod_type,mtb.mod_constraints,mtb.mod_delta
+ let sign,_,resolver,cst =
+ translate_mse_incl is_module senv.env mp_sup inl me
in
- let senv = add_constraints (Now cst) senv in
+ let senv = add_constraints (Now (false, cst)) senv in
(* Include Self support *)
let rec compute_sign sign mb resolver senv =
match sign with
| MoreFunctor(mbid,mtb,str) ->
let cst_sub = Subtyping.check_subtypes senv.env mb mtb in
- let senv = add_constraints (Now cst_sub) senv in
+ let senv =
+ add_constraints
+ (Now (false, Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty))
+ senv in
let mpsup_delta =
Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.mod_delta
in
let subst = Mod_subst.map_mbid mbid mp_sup mpsup_delta in
let resolver = Mod_subst.subst_codom_delta_resolver subst resolver in
compute_sign (Modops.subst_signature subst str) mb resolver senv
- | str -> resolver,str,senv
+ | NoFunctor str -> resolver,str,senv
in
- let resolver,sign,senv =
+ let resolver,str,senv =
let struc = NoFunctor (List.rev senv.revstruct) in
- let mtb = build_mtb mp_sup struc Univ.Constraint.empty senv.modresolver in
+ let mtb = build_mtb mp_sup struc Univ.ContextSet.empty senv.modresolver in
compute_sign sign mtb resolver senv
in
- let str = match sign with
- | NoFunctor struc -> struc
- | MoreFunctor _ -> Modops.error_higher_order_include ()
- in
let senv = update_resolver (Mod_subst.add_delta_resolver resolver) senv
in
let add senv ((l,elem) as field) =
@@ -729,12 +793,15 @@ type compiled_library = {
comp_name : DirPath.t;
comp_mod : module_body;
comp_deps : library_info array;
- comp_enga : engagement option;
- comp_natsymbs : Nativecode.symbol array
+ comp_enga : engagement;
+ comp_natsymbs : Nativecode.symbols
}
type native_library = Nativecode.global list
+let get_library_native_symbols senv dir =
+ DPMap.find dir senv.native_symbols
+
(** FIXME: MS: remove?*)
let current_modpath senv = senv.modpath
let current_dirpath senv = Names.ModPath.dp (current_modpath senv)
@@ -771,17 +838,17 @@ let export ?except senv dir =
mod_retroknowledge = senv.local_retroknowledge
}
in
- let ast, values =
- if !Flags.no_native_compiler then [], [||]
- else
+ let ast, symbols =
+ if !Flags.native_compiler then
Nativelibrary.dump_library mp dir senv.env str
+ else [], Nativecode.empty_symbols
in
let lib = {
comp_name = dir;
comp_mod = mb;
comp_deps = Array.of_list (DPMap.bindings senv.required);
comp_enga = Environ.engagement senv.env;
- comp_natsymbs = values }
+ comp_natsymbs = symbols }
in
mp, lib, ast
@@ -792,9 +859,11 @@ let import lib cst vodigest senv =
check_engagement senv.env lib.comp_enga;
let mp = MPfile lib.comp_name in
let mb = lib.comp_mod in
- let env = Environ.add_constraints mb.mod_constraints senv.env in
- let env = Environ.push_context_set cst env in
- (mp, lib.comp_natsymbs),
+ let env = Environ.push_context_set ~strict:true
+ (Univ.ContextSet.union mb.mod_constraints cst)
+ senv.env
+ in
+ mp,
{ senv with
env =
(let linkinfo =
@@ -803,7 +872,8 @@ let import lib cst vodigest senv =
Modops.add_linked_module mb linkinfo env);
modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
required = DPMap.add lib.comp_name vodigest senv.required;
- loads = (mp,mb)::senv.loads }
+ loads = (mp,mb)::senv.loads;
+ native_symbols = DPMap.add lib.comp_name lib.comp_natsymbs senv.native_symbols }
(** {6 Safe typing } *)
@@ -845,7 +915,9 @@ let register_inline kn senv =
let env = { env with env_globals = new_globals } in
{ senv with env = env_of_pre_env env }
-let add_constraints c = add_constraints (Now c)
+let add_constraints c =
+ add_constraints
+ (Now (false, Univ.ContextSet.add_constraints c Univ.ContextSet.empty))
(* NB: The next old comment probably refers to [propagate_loads] above.
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index abd5cd7a..2214cf8b 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -39,10 +39,30 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
(** {6 Stm machinery } *)
-val sideff_of_con : safe_environment -> constant -> Declarations.side_effect
-val sideff_of_scheme :
- string -> safe_environment -> (inductive * constant) list ->
- Declarations.side_effect
+type private_constant
+type private_constants
+
+type private_constant_role =
+ | Subproof
+ | Schema of inductive * string
+
+val side_effects_of_private_constants :
+ private_constants -> Entries.side_effects
+
+val empty_private_constants : private_constants
+val add_private : private_constant -> private_constants -> private_constants
+val concat_private : private_constants -> private_constants -> private_constants
+
+val private_con_of_con : safe_environment -> constant -> private_constant
+val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant
+
+val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
+val inline_private_constants_in_constr :
+ Environ.env -> Constr.constr -> private_constants -> Constr.constr
+val inline_private_constants_in_definition_entry :
+ Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry
+
+val universes_of_private : private_constants -> Univ.universe_context_set list
val is_curmod_library : safe_environment -> bool
@@ -51,23 +71,35 @@ val is_curmod_library : safe_environment -> bool
val join_safe_environment :
?except:Future.UUIDSet.t -> safe_environment -> safe_environment
+val is_joined_environment : safe_environment -> bool
(** {6 Enriching a safe environment } *)
(** Insertion of local declarations (Local or Variables) *)
val push_named_assum :
- (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0
+ (Id.t * Term.types * bool (* polymorphic *))
+ Univ.in_universe_context_set -> safe_transformer0
+
+(** Returns the full universe context necessary to typecheck the definition
+ (futures are forced) *)
val push_named_def :
- Id.t * Entries.definition_entry -> safe_transformer0
+ Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer
(** Insertion of global axioms or definitions *)
type global_declaration =
- | ConstantEntry of Entries.constant_entry
+ (* bool: export private constants *)
+ | ConstantEntry of bool * private_constants Entries.constant_entry
| GlobalRecipe of Cooking.recipe
+type exported_private_constant =
+ constant * private_constants Entries.constant_entry * private_constant_role
+
+(** returns the main constant plus a list of auxiliary constants (empty
+ unless one requires the side effects to be exported) *)
val add_constant :
- DirPath.t -> Label.t -> global_declaration -> constant safe_transformer
+ DirPath.t -> Label.t -> global_declaration ->
+ (constant * exported_private_constant list) safe_transformer
(** Adding an inductive type *)
@@ -87,10 +119,10 @@ val add_modtype :
(** Adding universe constraints *)
val push_context_set :
- Univ.universe_context_set -> safe_transformer0
+ bool -> Univ.universe_context_set -> safe_transformer0
val push_context :
- Univ.universe_context -> safe_transformer0
+ bool -> Univ.universe_context -> safe_transformer0
val add_constraints :
Univ.constraints -> safe_transformer0
@@ -98,12 +130,9 @@ val add_constraints :
(* (\** Generator of universes *\) *)
(* val next_universe : int safe_transformer *)
-(** Setting the strongly constructive or classical logical engagement *)
+(** Setting the type theory flavor *)
val set_engagement : Declarations.engagement -> safe_transformer0
-(** Collapsing the type hierarchy *)
-val set_type_in_type : safe_transformer0
-
(** {6 Interactive module functions } *)
val start_module : Label.t -> module_path safe_transformer
@@ -136,6 +165,8 @@ type compiled_library
type native_library = Nativecode.global list
+val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols
+
val start_library : DirPath.t -> module_path safe_transformer
val export :
@@ -145,7 +176,7 @@ val export :
(* Constraints are non empty iff the file is a vi2vo *)
val import : compiled_library -> Univ.universe_context_set -> vodigest ->
- (module_path * Nativecode.symbol array) safe_transformer
+ module_path safe_transformer
(** {6 Safe typing judgments } *)
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index ae86d686..e2854abf 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -26,8 +26,8 @@ let univ_of_sort = function
| Prop Null -> Universe.type0m
let sort_of_univ u =
- if is_type0m_univ u then Prop Null
- else if is_type0_univ u then Prop Pos
+ if is_type0m_univ u then prop
+ else if is_type0_univ u then set
else Type u
let compare s1 s2 =
@@ -62,6 +62,8 @@ let is_small = function
let family = function
| Prop Null -> InProp
| Prop Pos -> InSet
+ | Type u when is_type0m_univ u -> InProp
+ | Type u when is_type0_univ u -> InSet
| Type _ -> InType
let family_equal = (==)
@@ -76,7 +78,7 @@ let hash = function
in
combinesmall 1 h
| Type u ->
- let h = Hashtbl.hash u in (** FIXME *)
+ let h = Univ.Universe.hash u in
combinesmall 2 h
module List = struct
@@ -101,7 +103,7 @@ module Hsorts =
| (Type u1, Type u2) -> u1 == u2
|_ -> false
- let hash = Hashtbl.hash (** FIXME *)
+ let hash = hash
end)
let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index db155e6c..58f3bcdf 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -311,15 +311,19 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
try
(* The environment with the expected universes plus equality
of the body instances with the expected instance *)
- let env = Environ.add_constraints cstrs env in
- (* Check that the given definition does not add any constraint over
- the expected ones, so that it can be used in place of the original. *)
+ let ctxi = Univ.Instance.append inst1 inst2 in
+ let ctx = Univ.UContext.make (ctxi, cstrs) in
+ let env = Environ.push_context ctx env in
+ (* Check that the given definition does not add any constraint over
+ the expected ones, so that it can be used in place of
+ the original. *)
if Univ.check_constraints ctx1 (Environ.universes env) then
cstrs, env, inst2
else error (IncompatibleConstraints ctx1)
with Univ.UniverseInconsistency incon ->
error (IncompatibleUniverses incon)
- else cst, env, Univ.Instance.empty
+ else
+ cst, env, Univ.Instance.empty
in
(* Now check types *)
let typ1 = Typeops.type_of_constant_type env' cb1.const_type in
@@ -456,6 +460,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
let check_subtypes env sup super =
let env = add_module_type sup.mod_mp sup env in
+ let env = Environ.push_context_set ~strict:true super.mod_constraints env in
check_modtypes Univ.Constraint.empty env
(strengthen sup sup.mod_mp) super empty_subst
(map_mp super.mod_mp sup.mod_mp sup.mod_delta) false
diff --git a/kernel/term.ml b/kernel/term.ml
index 7bf4c818..33ed25fe 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -566,8 +566,10 @@ let decompose_lam_assum =
in
lamdec_rec empty_rel_context
-(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T
- into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+(* Given a positive integer n, decompose a product or let-in term
+ of the form [forall (x1:T1)..(xi:=ci:Ti)..(xn:Tn), T] into the pair
+ of the quantifying context [(xn,None,Tn);..;(xi,Some
+ ci,Ti);..;(x1,None,T1)] and of the inner type [T]) *)
let decompose_prod_n_assum n =
if n < 0 then
error "decompose_prod_n_assum: integer parameter must be positive";
@@ -581,10 +583,12 @@ let decompose_prod_n_assum n =
in
prodec_rec empty_rel_context n
-(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T
- into the pair ([(xn,Tn);...;(x1,T1)],T)
+(* Given a positive integer n, decompose a lambda or let-in term [fun
+ (x1:T1)..(xi:=ci:Ti)..(xn:Tn) => T] into the pair of the abstracted
+ context [(xn,None,Tn);...;(xi,Some ci,Ti);...;(x1,None,T1)] and of
+ the inner body [T].
Lets in between are not expanded but turn into local definitions,
- but n is the actual number of destructurated lambdas. *)
+ but n is the actual number of destructurated lambdas. *)
let decompose_lam_n_assum n =
if n < 0 then
error "decompose_lam_n_assum: integer parameter must be positive";
@@ -598,6 +602,20 @@ let decompose_lam_n_assum n =
in
lamdec_rec empty_rel_context n
+(* Same, counting let-in *)
+let decompose_lam_n_decls n =
+ if n < 0 then
+ error "decompose_lam_n_decls: integer parameter must be positive";
+ let rec lamdec_rec l n c =
+ if Int.equal n 0 then l,c
+ else match kind_of_term c with
+ | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
+ | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
+ | Cast (c,_,_) -> lamdec_rec l n c
+ | c -> error "decompose_lam_n_decls: not enough abstractions"
+ in
+ lamdec_rec empty_rel_context n
+
(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
* gives n (casts are ignored) *)
let nb_lam =
diff --git a/kernel/term.mli b/kernel/term.mli
index 501aaf74..d6071641 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -281,13 +281,15 @@ val decompose_prod : constr -> (Name.t*constr) list * constr
{% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a lambda. *)
val decompose_lam : constr -> (Name.t*constr) list * constr
-(** Given a positive integer n, transforms a product term
+(** Given a positive integer n, decompose a product term
{% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %}
- into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. *)
+ into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}.
+ Raise a user error if not enough products. *)
val decompose_prod_n : int -> constr -> (Name.t * constr) list * constr
-(** Given a positive integer {% $ %}n{% $ %}, transforms a lambda term
- {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %} *)
+(** Given a positive integer {% $ %}n{% $ %}, decompose a lambda term
+ {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}.
+ Raise a user error if not enough lambdas. *)
val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr
(** Extract the premisses and the conclusion of a term of the form
@@ -297,10 +299,15 @@ val decompose_prod_assum : types -> rel_context * types
(** Idem with lambda's *)
val decompose_lam_assum : constr -> rel_context * constr
-(** Idem but extract the first [n] premisses *)
+(** Idem but extract the first [n] premisses, counting let-ins. *)
val decompose_prod_n_assum : int -> types -> rel_context * types
+
+(** Idem for lambdas, _not_ counting let-ins *)
val decompose_lam_n_assum : int -> constr -> rel_context * constr
+(** Idem, counting let-ins *)
+val decompose_lam_n_decls : int -> constr -> rel_context * constr
+
(** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
gives {% $ %}n{% $ %} (casts are ignored) *)
val nb_lam : constr -> int
@@ -308,12 +315,14 @@ val nb_lam : constr -> int
(** Similar to [nb_lam], but gives the number of products instead *)
val nb_prod : constr -> int
-(** Returns the premisses/parameters of a type/term (let-in included) *)
+(** Return the premisses/parameters of a type/term (let-in included) *)
val prod_assum : types -> rel_context
val lam_assum : constr -> rel_context
-(** Returns the first n-th premisses/parameters of a type/term (let included)*)
+(** Return the first n-th premisses/parameters of a type (let included and counted) *)
val prod_n_assum : int -> types -> rel_context
+
+(** Return the first n-th premisses/parameters of a term (let included but not counted) *)
val lam_n_assum : int -> constr -> rel_context
(** Remove the premisses/parameters of a type/term *)
@@ -328,11 +337,11 @@ val strip_lam_n : int -> constr -> constr
val strip_prod_assum : types -> types
val strip_lam_assum : constr -> constr
-(** flattens application lists *)
+(** Flattens application lists *)
val collapse_appl : constr -> constr
-(** Removes recursively the casts around a term i.e.
+(** Remove recursively the casts around a term i.e.
[strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
val strip_outer_cast : constr -> constr
@@ -352,10 +361,10 @@ type arity = rel_context * sorts
(** Build an "arity" from its canonical form *)
val mkArity : arity -> types
-(** Destructs an "arity" into its canonical form *)
+(** Destruct an "arity" into its canonical form *)
val destArity : types -> arity
-(** Tells if a term has the form of an arity *)
+(** Tell if a term has the form of an arity *)
val isArity : types -> bool
(** {5 Kind of type} *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a316b449..a566028d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -43,10 +43,29 @@ let map_option_typ = function None -> `None | Some x -> `Some x
(* Insertion of constants and parameters in environment. *)
-let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff
+let mk_pure_proof c = (c, Univ.ContextSet.empty), []
-let handle_side_effects env body side_eff =
- let handle_sideff t se =
+let equal_eff e1 e2 =
+ let open Entries in
+ match e1, e2 with
+ | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } ->
+ Names.Constant.equal c1 c2
+ | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } ->
+ CList.for_all2eq
+ (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2)
+ cl1 cl2
+ | _ -> false
+
+let rec uniq_seff = function
+ | [] -> []
+ | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs)
+(* The list of side effects is in reverse order (most recent first).
+ * To keep the "topological" order between effects we have to uniq-ize from
+ * the tail *)
+let uniq_seff l = List.rev (uniq_seff (List.rev l))
+
+let inline_side_effects env body ctx side_eff =
+ let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
let cbl = match se with
| SEsubproof (c,cb,b) -> [c,cb,b]
| SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in
@@ -65,8 +84,8 @@ let handle_side_effects env body side_eff =
let rec sub_body c u b i x = match kind_of_term x with
| Const (c',u') when eq_constant c c' ->
Vars.subst_instance_constr u' b
- | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in
- let fix_body (c,cb,b) t =
+ | _ -> map_constr_with_binders ((+) 1) (sub_body c u b) i x in
+ let fix_body (c,cb,b) (t,ctx) =
match cb.const_body, b with
| Def b, _ ->
let b = Mod_subst.force_constr b in
@@ -74,37 +93,86 @@ let handle_side_effects env body side_eff =
if not poly then
let b_ty = Typeops.type_of_constant_type env cb.const_type in
let t = sub c 1 (Vars.lift 1 t) in
- mkLetIn (cname c, b, b_ty, t)
+ mkLetIn (cname c, b, b_ty, t),
+ Univ.ContextSet.union ctx
+ (Univ.ContextSet.of_context cb.const_universes)
else
let univs = cb.const_universes in
- sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
+ sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
| OpaqueDef _, `Opaque (b,_) ->
let poly = cb.const_polymorphic in
if not poly then
let b_ty = Typeops.type_of_constant_type env cb.const_type in
let t = sub c 1 (Vars.lift 1 t) in
- mkApp (mkLambda (cname c, b_ty, t), [|b|])
+ mkApp (mkLambda (cname c, b_ty, t), [|b|]),
+ Univ.ContextSet.union ctx
+ (Univ.ContextSet.of_context cb.const_universes)
else
let univs = cb.const_universes in
- sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
+ sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
| _ -> assert false
in
- List.fold_right fix_body cbl t
+ let t, ctx = List.fold_right fix_body cbl (t,ctx) in
+ t, ctx, (mb,List.length cbl) :: sl
in
(* CAVEAT: we assure a proper order *)
- Declareops.fold_side_effects handle_sideff body
- (Declareops.uniquize_side_effects side_eff)
+ List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff)
+
+(* Given the list of signatures of side effects, checks if they match.
+ * I.e. if they are ordered descendants of the current revstruct *)
+let check_signatures curmb sl =
+ let is_direct_ancestor (sl, curmb) (mb, how_many) =
+ match curmb with
+ | None -> None, None
+ | Some curmb ->
+ try
+ let mb = Ephemeron.get mb in
+ match sl with
+ | None -> sl, None
+ | Some n ->
+ if List.length mb >= how_many && CList.skipn how_many mb == curmb
+ then Some (n + how_many), Some mb
+ else None, None
+ with Ephemeron.InvalidKey -> None, None in
+ let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in
+ sl
+
+let skip_trusted_seff sl b e =
+ let rec aux sl b e acc =
+ match sl, kind_of_term b with
+ | (None|Some 0), _ -> b, e, acc
+ | Some sl, LetIn (n,c,ty,bo) ->
+ aux (Some (sl-1)) bo
+ (Environ.push_rel (n,Some c,ty) e) (`Let(n,c,ty)::acc)
+ | Some sl, App(hd,arg) ->
+ begin match kind_of_term hd with
+ | Lambda (n,ty,bo) ->
+ aux (Some (sl-1)) bo
+ (Environ.push_rel (n,None,ty) e) (`Cut(n,ty,arg)::acc)
+ | _ -> assert false
+ end
+ | _ -> assert false
+ in
+ aux sl b e []
+
+let rec unzip ctx j =
+ match ctx with
+ | [] -> j
+ | `Let (n,c,ty) :: ctx ->
+ unzip ctx { j with uj_val = mkLetIn (n,c,ty,j.uj_val) }
+ | `Cut (n,ty,arg) :: ctx ->
+ unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) }
let hcons_j j =
{ uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type}
let feedback_completion_typecheck =
Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-
-let infer_declaration env kn dcl =
+
+let infer_declaration ~trust env kn dcl =
match dcl with
| ParameterEntry (ctx,poly,(t,uctx),nl) ->
- let env = push_context uctx env in
+ let env = push_context ~strict:(not poly) uctx env in
let j = infer env t in
let abstract = poly && not (Option.is_empty kn) in
let usubst, univs = Univ.abstract_universes abstract uctx in
@@ -115,34 +183,41 @@ let infer_declaration env kn dcl =
| DefinitionEntry ({ const_entry_type = Some typ;
const_entry_opaque = true;
const_entry_polymorphic = false} as c) ->
- let env = push_context c.const_entry_universes env in
+ let env = push_context ~strict:true c.const_entry_universes env in
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let tyj = infer_type env typ in
let proofterm =
- Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
- let body = handle_side_effects env body side_eff in
- let env' = push_context_set ctx env in
- let j = infer env' body in
+ Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) ->
+ let body, uctx, signatures =
+ inline_side_effects env body uctx side_eff in
+ let valid_signatures = check_signatures trust signatures in
+ let env' = push_context_set uctx env in
+ let j =
+ let body,env',ectx = skip_trusted_seff valid_signatures body env' in
+ let j = infer env' body in
+ unzip ectx j in
let j = hcons_j j in
let subst = Univ.LMap.empty in
let _typ = constrain_type env' j c.const_entry_polymorphic subst
(`SomeWJ (typ,tyj)) in
feedback_completion_typecheck feedback_id;
- j.uj_val, ctx) in
+ j.uj_val, uctx) in
let def = OpaqueDef (Opaqueproof.create proofterm) in
def, RegularArity typ, None, c.const_entry_polymorphic,
c.const_entry_universes,
c.const_entry_inline_code, c.const_entry_secctx
| DefinitionEntry c ->
- let env = push_context c.const_entry_universes env in
let { const_entry_type = typ; const_entry_opaque = opaque } = c in
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let (body, ctx), side_eff = Future.join body in
- assert(Univ.ContextSet.is_empty ctx);
- let body = handle_side_effects env body side_eff in
+ let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
+ let body, ctx, _ = inline_side_effects env body
+ (Univ.ContextSet.union univsctx ctx) side_eff in
+ let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
- let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
+ let usubst, univs =
+ Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in
let j = infer env body in
let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
@@ -176,14 +251,17 @@ let global_vars_set_constant_type env = function
(fun t c -> Id.Set.union (global_vars_set env t) c))
ctx ~init:Id.Set.empty
-let record_aux env s1 s2 =
+let record_aux env s_ty s_bo suggested_expr =
+ let in_ty = keep_hyps env s_ty in
let v =
String.concat " "
- (List.map (fun (id, _,_) -> Id.to_string id)
- (keep_hyps env (Id.Set.union s1 s2))) in
- Aux_file.record_in_aux "context_used" v
+ (CList.map_filter (fun (id, _,_) ->
+ if List.exists (fun (id',_,_) -> Id.equal id id') in_ty then None
+ else Some (Id.to_string id))
+ (keep_hyps env s_bo)) in
+ Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
-let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
+let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
let set_suggest_proof_using f = suggest_proof_using := f
let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
@@ -198,6 +276,10 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
str " " ++ str (String.conjugate_verb_to_be n) ++
str " used but not declared:" ++
fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in
+ let sort evn l =
+ List.filter (fun (id,_,_) ->
+ List.exists (fun (id',_,_) -> Names.Id.equal id id') l)
+ (named_context env) in
(* We try to postpone the computation of used section variables *)
let hyps, def =
let context_ids = List.map pi1 (named_context env) in
@@ -215,19 +297,21 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
(Opaqueproof.force_proof (opaque_tables env) lc) in
(* we force so that cst are added to the env immediately after *)
ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
- !suggest_proof_using kn env vars ids_typ context_ids;
+ let expr =
+ !suggest_proof_using (Constant.to_string kn)
+ env vars ids_typ context_ids in
if !Flags.compilation_mode = Flags.BuildVo then
- record_aux env ids_typ vars;
+ record_aux env ids_typ vars expr;
vars
in
keep_hyps env (Idset.union ids_typ ids_def), def
| None ->
if !Flags.compilation_mode = Flags.BuildVo then
- record_aux env Id.Set.empty Id.Set.empty;
+ record_aux env Id.Set.empty Id.Set.empty "";
[], def (* Empty section context: no need to check *)
| Some declared ->
(* We use the declared set and chain a check of correctness *)
- declared,
+ sort env declared,
match def with
| Undef _ as x -> x (* nothing to check *)
| Def cs as x ->
@@ -243,16 +327,30 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
check declared inferred) lc) in
let tps =
- (* FIXME: incompleteness of the bytecode vm: we compile polymorphic
- constants like opaque definitions. *)
- if poly then Some (Cemitcodes.from_val Cemitcodes.BCconstant)
- else
- let res =
- match proj with
- | None -> compile_constant_body env def
- | Some pb ->
- compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))
- in Option.map Cemitcodes.from_val res
+ let res =
+ let comp_univs = if poly then Some univs else None in
+ match proj with
+ | None -> compile_constant_body env comp_univs def
+ | Some pb ->
+ (* The compilation of primitive projections is a bit tricky, because
+ they refer to themselves (the body of p looks like fun c =>
+ Proj(p,c)). We break the cycle by building an ad-hoc compilation
+ environment. A cleaner solution would be that kernel projections are
+ simply Proj(i,c) with i an int and c a constr, but we would have to
+ get rid of the compatibility layer. *)
+ let cb =
+ { const_hyps = hyps;
+ const_body = def;
+ const_type = typ;
+ const_proj = proj;
+ const_body_code = None;
+ const_polymorphic = poly;
+ const_universes = univs;
+ const_inline_code = inline_code }
+ in
+ let env = add_constant kn cb env in
+ compile_constant_body env comp_univs def
+ in Option.map Cemitcodes.from_val res
in
{ const_hyps = hyps;
const_body = def;
@@ -263,11 +361,95 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
const_universes = univs;
const_inline_code = inline_code }
-
(*s Global and local constant declaration. *)
-let translate_constant env kn ce =
- build_constant_declaration kn env (infer_declaration env (Some kn) ce)
+let translate_constant mb env kn ce =
+ build_constant_declaration kn env
+ (infer_declaration ~trust:mb env (Some kn) ce)
+
+let constant_entry_of_side_effect cb u =
+ let pt =
+ match cb.const_body, u with
+ | OpaqueDef _, `Opaque (b, c) -> b, c
+ | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
+ | _ -> assert false in
+ DefinitionEntry {
+ const_entry_body = Future.from_val (pt, []);
+ const_entry_secctx = None;
+ const_entry_feedback = None;
+ const_entry_type =
+ (match cb.const_type with RegularArity t -> Some t | _ -> None);
+ const_entry_polymorphic = cb.const_polymorphic;
+ const_entry_universes = cb.const_universes;
+ const_entry_opaque = Declareops.is_opaque cb;
+ const_entry_inline_code = cb.const_inline_code }
+;;
+
+let turn_direct (kn,cb,u,r as orig) =
+ match cb.const_body, u with
+ | OpaqueDef _, `Opaque (b,c) ->
+ let pt = Future.from_val (b,c) in
+ kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r
+ | _ -> orig
+;;
+
+type side_effect_role =
+ | Subproof
+ | Schema of inductive * string
+
+type exported_side_effect =
+ constant * constant_body * side_effects constant_entry * side_effect_role
+
+let export_side_effects mb env ce =
+ match ce with
+ | ParameterEntry _ | ProjectionEntry _ -> [], ce
+ | DefinitionEntry c ->
+ let { const_entry_body = body } = c in
+ let _, eff = Future.force body in
+ let ce = DefinitionEntry { c with
+ const_entry_body = Future.chain ~greedy:true ~pure:true body
+ (fun (b_ctx, _) -> b_ctx, []) } in
+ let not_exists (c,_,_,_) =
+ try ignore(Environ.lookup_constant c env); false
+ with Not_found -> true in
+ let aux (acc,sl) { eff = se; from_env = mb } =
+ let cbl = match se with
+ | SEsubproof (c,cb,b) -> [c,cb,b,Subproof]
+ | SEscheme (cl,k) ->
+ List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in
+ let cbl = List.filter not_exists cbl in
+ if cbl = [] then acc, sl
+ else cbl :: acc, (mb,List.length cbl) :: sl in
+ let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in
+ let trusted = check_signatures mb signatures in
+ let push_seff env = function
+ | kn, cb, `Nothing, _ ->
+ Environ.add_constant kn cb env
+ | kn, cb, `Opaque(_, ctx), _ ->
+ let env = Environ.add_constant kn cb env in
+ Environ.push_context_set
+ ~strict:(not cb.const_polymorphic) ctx env in
+ let rec translate_seff sl seff acc env =
+ match sl, seff with
+ | _, [] -> List.rev acc, ce
+ | (None | Some 0), cbs :: rest ->
+ let env, cbs =
+ List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
+ let ce = constant_entry_of_side_effect ocb u in
+ let cb = translate_constant mb env kn ce in
+ (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs))
+ (env,[]) cbs in
+ translate_seff sl rest (cbs @ acc) env
+ | Some sl, cbs :: rest ->
+ 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 (fun (kn,cb,u,r) ->
+ kn, cb, constant_entry_of_side_effect cb u, r) cbs in
+ translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env
+ in
+ translate_seff trusted seff [] env
+;;
let translate_local_assum env t =
let j = infer env t in
@@ -277,18 +459,36 @@ let translate_local_assum env t =
let translate_recipe env kn r =
build_constant_declaration kn env (Cooking.cook_constant env r)
-let translate_local_def env id centry =
+let translate_local_def mb env id centry =
let def,typ,proj,poly,univs,inline_code,ctx =
- infer_declaration env None (DefinitionEntry centry) in
+ infer_declaration ~trust:mb env None (DefinitionEntry centry) in
let typ = type_of_constant_type env typ in
+ if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
+ match def with
+ | Undef _ -> ()
+ | Def _ -> ()
+ | OpaqueDef lc ->
+ let context_ids = List.map pi1 (named_context env) in
+ let ids_typ = global_vars_set env typ in
+ let ids_def = global_vars_set env
+ (Opaqueproof.force_proof (opaque_tables env) lc) in
+ let expr =
+ !suggest_proof_using (Id.to_string id)
+ env ids_def ids_typ context_ids in
+ record_aux env ids_typ ids_def expr
+ end;
def, typ, univs
(* Insertion of inductive types. *)
let translate_mind env kn mie = Indtypes.check_inductive env kn mie
-let handle_entry_side_effects env ce = { ce with
+let inline_entry_side_effects env ce = { ce with
const_entry_body = Future.chain ~greedy:true ~pure:true
ce.const_entry_body (fun ((body, ctx), side_eff) ->
- (handle_side_effects env body side_eff, ctx), Declareops.no_seff);
+ let body, ctx',_ = inline_side_effects env body ctx side_eff in
+ (body, ctx'), []);
}
+
+let inline_side_effects env body side_eff =
+ pi1 (inline_side_effects env body Univ.ContextSet.empty side_eff)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 1b54b1ea..2e6aa161 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,23 +12,46 @@ open Environ
open Declarations
open Entries
-val translate_local_def : env -> Id.t -> definition_entry ->
+val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
constant_def * types * constant_universes
val translate_local_assum : env -> types -> types
-val mk_pure_proof : constr -> proof_output
+val mk_pure_proof : constr -> side_effects proof_output
-val handle_side_effects : env -> constr -> Declareops.side_effects -> constr
+val inline_side_effects : env -> constr -> side_effects -> constr
(** Returns the term where side effects have been turned into let-ins or beta
redexes. *)
-val handle_entry_side_effects : env -> definition_entry -> definition_entry
-(** Same as {!handle_side_effects} but applied to entries. Only modifies the
+val inline_entry_side_effects :
+ env -> side_effects definition_entry -> side_effects definition_entry
+(** Same as {!inline_side_effects} but applied to entries. Only modifies the
{!Entries.const_entry_body} field. It is meant to get a term out of a not
yet type checked proof. *)
-val translate_constant : env -> constant -> constant_entry -> constant_body
+val uniq_seff : side_effects -> side_effects
+
+val translate_constant :
+ structure_body -> env -> constant -> side_effects constant_entry ->
+ constant_body
+
+type side_effect_role =
+ | Subproof
+ | Schema of inductive * string
+
+type exported_side_effect =
+ constant * constant_body * side_effects constant_entry * side_effect_role
+
+(* Given a constant entry containing side effects it exports them (either
+ * by re-checking them or trusting them). Returns the constant bodies to
+ * be pushed in the safe_env by safe typing. The main constant entry
+ * needs to be translated as usual after this step. *)
+val export_side_effects :
+ structure_body -> env -> side_effects constant_entry ->
+ exported_side_effect list * side_effects constant_entry
+
+val constant_entry_of_side_effect :
+ constant_body -> seff_env -> side_effects constant_entry
val translate_mind :
env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -37,11 +60,11 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
(** Internal functions, mentioned here for debug purpose only *)
-val infer_declaration : env -> constant option ->
- constant_entry -> Cooking.result
+val infer_declaration : trust:structure_body -> env -> constant option ->
+ side_effects constant_entry -> Cooking.result
val build_constant_declaration :
constant -> env -> Cooking.result -> constant_body
val set_suggest_proof_using :
- (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit
+ (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 48dbacf1..4f32fdce 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -134,10 +134,16 @@ let extract_context_levels env l =
let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} =
let params, ccl = dest_prod_assum env t in
match kind_of_term ccl with
- | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) ->
- let param_ccls = extract_context_levels env params in
- let s = { template_param_levels = param_ccls; template_level = u} in
- TemplateArity (params,s)
+ | Sort (Type u) ->
+ let ind, l = decompose_app (whd_betadeltaiota env c) in
+ if isInd ind && List.is_empty l then
+ let mis = lookup_mind_specif env (fst (destInd ind)) in
+ let nparams = Inductive.inductive_params mis in
+ let paramsl = CList.lastn nparams params in
+ let param_ccls = extract_context_levels env paramsl in
+ let s = { template_param_levels = param_ccls; template_level = u} in
+ TemplateArity (params,s)
+ else RegularArity t
| _ ->
RegularArity t
@@ -252,14 +258,12 @@ let sort_of_product env domsort rangsort =
| (Prop _, Prop Pos) -> rangsort
(* Product rule (Type,Set,?) *)
| (Type u1, Prop Pos) ->
- begin match engagement env with
- | Some ImpredicativeSet ->
+ if is_impredicative_set env then
(* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
rangsort
- | _ ->
+ else
(* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
Type (Universe.sup Universe.type0 u1)
- end
(* Product rule (Prop,Type_i,Type_i) *)
| (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2)
(* Product rule (Prop,Type_i,Type_i) *)
@@ -296,7 +300,7 @@ let judge_of_cast env cj k tj =
match k with
| VMcast ->
mkCast (cj.uj_val, k, expected_type),
- vm_conv CUMUL env cj.uj_type expected_type
+ Reduction.vm_conv CUMUL env cj.uj_type expected_type
| DEFAULTcast ->
mkCast (cj.uj_val, k, expected_type),
default_conv ~l2r:false CUMUL env cj.uj_type expected_type
@@ -306,7 +310,7 @@ let judge_of_cast env cj k tj =
| NATIVEcast ->
let sigma = Nativelambda.empty_evars in
mkCast (cj.uj_val, k, expected_type),
- native_conv CUMUL sigma env cj.uj_type expected_type
+ Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type
in
{ uj_val = c;
uj_type = expected_type }
@@ -473,7 +477,7 @@ let rec execute env cstr =
let j' = execute env1 c3 in
judge_of_letin env name j1 j2 j'
- | Cast (c,k, t) ->
+ | Cast (c,k,t) ->
let cj = execute env c in
let tj = execute_type env t in
judge_of_cast env cj k tj
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 763c0822..6c231698 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -270,8 +270,10 @@ module Level = struct
let is_small x =
match data x with
| Level _ -> false
- | _ -> true
-
+ | Var _ -> false
+ | Prop -> true
+ | Set -> true
+
let is_prop x =
match data x with
| Prop -> true
@@ -551,6 +553,10 @@ struct
| Cons (l, _, Nil) -> Expr.is_level l
| _ -> false
+ let rec is_levels l = match l with
+ | Cons (l, _, r) -> Expr.is_level l && is_levels r
+ | Nil -> true
+
let level l = match l with
| Cons (l, _, Nil) -> Expr.level l
| _ -> None
@@ -577,7 +583,7 @@ struct
let is_type0m x = equal type0m x
let is_type0 x = equal type0 x
- (* Returns the formal universe that lies juste above the universe variable u.
+ (* Returns the formal universe that lies just above the universe variable u.
Used to type the sort u. *)
let super l =
if is_small l then type1
@@ -655,7 +661,6 @@ type canonical_arc =
lt: Level.t list;
le: Level.t list;
rank : int;
- predicative : bool;
mutable status : status;
(** Guaranteed to be unset out of the [compare_neq] functions. It is used
to do an imperative traversal of the graph, ensuring a O(1) check that
@@ -670,7 +675,7 @@ let arc_is_lt arc = match arc.status with
| Unset | SetLe -> false
| SetLt -> true
-let terminal u = {univ=u; lt=[]; le=[]; rank=0; predicative=false; status = Unset}
+let terminal u = {univ=u; lt=[]; le=[]; rank=0; status = Unset}
module UMap :
sig
@@ -720,35 +725,51 @@ let enter_arc ca g =
(* Every Level.t has a unique canonical arc representative *)
+(** The graph always contains nodes for Prop and Set. *)
+
+let terminal_lt u v =
+ {(terminal u) with lt=[v]}
+
+let empty_universes =
+ let g = enter_arc (terminal Level.set) UMap.empty in
+ let g = enter_arc (terminal_lt Level.prop Level.set) g in
+ g
+
(* repr : universes -> Level.t -> canonical_arc *)
(* canonical representative : we follow the Equiv links *)
-let repr g u =
- let rec repr_rec u =
- let a =
- try UMap.find u g
- with Not_found -> anomaly ~label:"Univ.repr"
- (str"Universe " ++ Level.pr u ++ str" undefined")
- in
- match a with
- | Equiv v -> repr_rec v
- | Canonical arc -> arc
+let rec repr g u =
+ let a =
+ try UMap.find u g
+ with Not_found -> anomaly ~label:"Univ.repr"
+ (str"Universe " ++ Level.pr u ++ str" undefined")
in
- repr_rec u
+ match a with
+ | Equiv v -> repr g v
+ | Canonical arc -> arc
-(* [safe_repr] also search for the canonical representative, but
- if the graph doesn't contain the searched universe, we add it. *)
+let get_prop_arc g = repr g Level.prop
+let get_set_arc g = repr g Level.set
+let is_set_arc u = Level.is_set u.univ
+let is_prop_arc u = Level.is_prop u.univ
-let safe_repr g u =
- let rec safe_repr_rec u =
- match UMap.find u g with
- | Equiv v -> safe_repr_rec v
- | Canonical arc -> arc
- in
- try g, safe_repr_rec u
- with Not_found ->
- let can = terminal u in
- enter_arc can g, can
+exception AlreadyDeclared
+
+let add_universe vlev strict g =
+ try
+ let _arcv = UMap.find vlev g in
+ raise AlreadyDeclared
+ with Not_found ->
+ let v = terminal vlev in
+ let arc =
+ let arc = get_set_arc g in
+ if strict then
+ { arc with lt=vlev::arc.lt}
+ else
+ { arc with le=vlev::arc.le}
+ in
+ let g = enter_arc arc g in
+ enter_arc v g
(* reprleq : canonical_arc -> canonical_arc list *)
(* All canonical arcv such that arcu<=arcv with arcv#arcu *)
@@ -792,7 +813,6 @@ let between g arcu arcv =
in
let good,_,_ = explore ([arcv],[],false) arcu in
good
-
(* We assume compare(u,v) = LE with v canonical (see compare below).
In this case List.hd(between g u v) = repr u
Otherwise, between g u v = []
@@ -903,8 +923,9 @@ let get_explanation strict g arcu arcv =
in
find [] arc.lt
in
+ let start = (* if is_prop_arc arcu then [Le, make arcv.univ] else *) [] in
try
- let (to_revert, c) = cmp [] [] [] [(arcu, [])] in
+ let (to_revert, c) = cmp start [] [] [(arcu, [])] in
(** Reset all the touched arcs. *)
let () = List.iter (fun arc -> arc.status <- Unset) to_revert in
List.rev c
@@ -928,25 +949,8 @@ let fast_compare_neq strict g arcu arcv =
if arc_is_lt arc then
cmp c to_revert lt_todo le_todo
else
- let rec find lt_todo lt le = match le with
- | [] ->
- begin match lt with
- | [] ->
- let () = arc.status <- SetLt in
- cmp c (arc :: to_revert) lt_todo le_todo
- | u :: lt ->
- let arc = repr g u in
- if arc == arcv then
- if strict then (to_revert, FastLT) else (to_revert, FastLE)
- else find (arc :: lt_todo) lt le
- end
- | u :: le ->
- let arc = repr g u in
- if arc == arcv then
- if strict then (to_revert, FastLT) else (to_revert, FastLE)
- else find (arc :: lt_todo) lt le
- in
- find lt_todo arc.lt arc.le
+ let () = arc.status <- SetLt in
+ process_lt c (arc :: to_revert) lt_todo le_todo arc.lt arc.le
| [], arc::le_todo ->
if arc == arcv then
(* No need to continue inspecting universes above arc:
@@ -958,22 +962,39 @@ let fast_compare_neq strict g arcu arcv =
if arc_is_le arc then
cmp c to_revert [] le_todo
else
- let rec find lt_todo lt = match lt with
- | [] ->
- let fold accu u =
- let node = repr g u in
- node :: accu
- in
- let le_new = List.fold_left fold le_todo arc.le in
- let () = arc.status <- SetLe in
- cmp c (arc :: to_revert) lt_todo le_new
- | u :: lt ->
- let arc = repr g u in
- if arc == arcv then
- if strict then (to_revert, FastLT) else (to_revert, FastLE)
- else find (arc :: lt_todo) lt
- in
- find [] arc.lt
+ let () = arc.status <- SetLe in
+ process_le c (arc :: to_revert) [] le_todo arc.lt arc.le
+
+ and process_lt c to_revert lt_todo le_todo lt le = match le with
+ | [] ->
+ begin match lt with
+ | [] -> cmp c to_revert lt_todo le_todo
+ | u :: lt ->
+ let arc = repr g u in
+ if arc == arcv then
+ if strict then (to_revert, FastLT) else (to_revert, FastLE)
+ else process_lt c to_revert (arc :: lt_todo) le_todo lt le
+ end
+ | u :: le ->
+ let arc = repr g u in
+ if arc == arcv then
+ if strict then (to_revert, FastLT) else (to_revert, FastLE)
+ else process_lt c to_revert (arc :: lt_todo) le_todo lt le
+
+ and process_le c to_revert lt_todo le_todo lt le = match lt with
+ | [] ->
+ let fold accu u =
+ let node = repr g u in
+ node :: accu
+ in
+ let le_new = List.fold_left fold le_todo le in
+ cmp c to_revert lt_todo le_new
+ | u :: lt ->
+ let arc = repr g u in
+ if arc == arcv then
+ if strict then (to_revert, FastLT) else (to_revert, FastLE)
+ else process_le c to_revert (arc :: lt_todo) le_todo lt le
+
in
try
let (to_revert, c) = cmp FastNLE [] [] [arcu] in
@@ -1017,24 +1038,18 @@ let is_lt g arcu arcv =
(** First, checks on universe levels *)
let check_equal g u v =
- let g, arcu = safe_repr g u in
- let _, arcv = safe_repr g v in
- arcu == arcv
+ let arcu = repr g u and arcv = repr g v in
+ arcu == arcv
let check_eq_level g u v = u == v || check_equal g u v
-let is_set_arc u = Level.is_set u.univ
-let is_prop_arc u = Level.is_prop u.univ
-let get_prop_arc g = snd (safe_repr g Level.prop)
-
let check_smaller g strict u v =
- let g, arcu = safe_repr g u in
- let g, arcv = safe_repr g v in
+ let arcu = repr g u and arcv = repr g v in
if strict then
is_lt g arcu arcv
else
is_prop_arc arcu
- || (is_set_arc arcu && arcv.predicative)
+ || (is_set_arc arcu && not (is_prop_arc arcv))
|| is_leq g arcu arcv
(** Then, checks on universes *)
@@ -1076,19 +1091,11 @@ let check_leq g u v =
(** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
-(** To speed up tests of Set </<= i *)
-let set_predicative g arcv =
- enter_arc {arcv with predicative = true} g
-
(* setlt : Level.t -> Level.t -> reason -> unit *)
(* forces u > v *)
(* this is normally an update of u in g rather than a creation. *)
let setlt g arcu arcv =
let arcu' = {arcu with lt=arcv.univ::arcu.lt} in
- let g =
- if is_set_arc arcu then set_predicative g arcv
- else g
- in
enter_arc arcu' g, arcu'
(* checks that non-redundant *)
@@ -1102,11 +1109,6 @@ let setlt_if (g,arcu) v =
(* this is normally an update of u in g rather than a creation. *)
let setleq g arcu arcv =
let arcu' = {arcu with le=arcv.univ::arcu.le} in
- let g =
- if is_set_arc arcu' then
- set_predicative g arcv
- else g
- in
enter_arc arcu' g, arcu'
(* checks that non-redundant *)
@@ -1122,7 +1124,8 @@ let merge g arcu arcv =
(* we find the arc with the biggest rank, and we redirect all others to it *)
let arcu, g, v =
let best_ranked (max_rank, old_max_rank, best_arc, rest) arc =
- if Level.is_small arc.univ || arc.rank >= max_rank
+ if Level.is_small arc.univ ||
+ (arc.rank >= max_rank && not (Level.is_small best_arc.univ))
then (arc.rank, max_rank, arc, best_arc::rest)
else (max_rank, old_max_rank, best_arc, arc::rest)
in
@@ -1152,7 +1155,7 @@ let merge g arcu arcv =
(* we assume compare(u,v) = compare(v,u) = NLE *)
(* merge_disc u v forces u ~ v with repr u as canonical repr *)
let merge_disc g arc1 arc2 =
- let arcu, arcv = if arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
+ let arcu, arcv = if Level.is_small arc2.univ || arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
let arcu, g =
if not (Int.equal arc1.rank arc2.rank) then arcu, g
else
@@ -1175,12 +1178,11 @@ exception UniverseInconsistency of univ_inconsistency
let error_inconsistency o u v (p:explanation option) =
raise (UniverseInconsistency (o,make u,make v,p))
-(* enforc_univ_eq : Level.t -> Level.t -> unit *)
-(* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
+(* enforce_univ_eq : Level.t -> Level.t -> unit *)
+(* enforce_univ_eq u v will force u=v if possible, will fail otherwise *)
let enforce_univ_eq u v g =
- let g,arcu = safe_repr g u in
- let g,arcv = safe_repr g v in
+ let arcu = repr g u and arcv = repr g v in
match fast_compare g arcu arcv with
| FastEQ -> g
| FastLT ->
@@ -1199,8 +1201,7 @@ let enforce_univ_eq u v g =
(* enforce_univ_leq : Level.t -> Level.t -> unit *)
(* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
let enforce_univ_leq u v g =
- let g,arcu = safe_repr g u in
- let g,arcv = safe_repr g v in
+ let arcu = repr g u and arcv = repr g v in
if is_leq g arcu arcv then g
else
match fast_compare g arcv arcu with
@@ -1213,8 +1214,7 @@ let enforce_univ_leq u v g =
(* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
let enforce_univ_lt u v g =
- let g,arcu = safe_repr g u in
- let g,arcv = safe_repr g v in
+ let arcu = repr g u and arcv = repr g v in
match fast_compare g arcu arcv with
| FastLT -> g
| FastLE -> fst (setlt g arcu arcv)
@@ -1227,18 +1227,10 @@ let enforce_univ_lt u v g =
let p = get_explanation false g arcv arcu in
error_inconsistency Lt u v p
-let empty_universes = UMap.empty
-
(* Prop = Set is forbidden here. *)
-let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty
+let initial_universes = empty_universes
let is_initial_universes g = UMap.equal (==) g initial_universes
-
-let add_universe vlev g =
- let v = terminal vlev in
- let proparc = get_prop_arc g in
- enter_arc {proparc with le=vlev::proparc.le}
- (enter_arc v g)
(* Constraints and sets of constraints. *)
@@ -1372,10 +1364,12 @@ let check_univ_leq u v =
let enforce_leq u v c =
let open Universe.Huniv in
+ let rec aux acc v =
match v with
- | Cons (v, _, Nil) ->
- fold (fun u -> constraint_add_leq u v) u c
- | _ -> anomaly (Pp.str"A universe bound can only be a variable")
+ | Cons (v, _, l) ->
+ aux (fold (fun u -> constraint_add_leq u v) u c) l
+ | Nil -> acc
+ in aux c v
let enforce_leq u v c =
if check_univ_leq u v then c
@@ -1446,7 +1440,6 @@ let normalize_universes g =
lt = LSet.elements lt;
le = LSet.elements le;
rank = rank;
- predicative = false;
status = Unset;
}
in
@@ -1589,9 +1582,9 @@ let sort_universes orig =
let sorted = LMap.fold fold compact UMap.empty in
(** Add all [Type.n] nodes *)
let fold i accu u =
- if 0 < i then
- let pred = types.(i - 1) in
- let arc = {univ = u; lt = [pred]; le = []; rank = 0; predicative = false; status = Unset; } in
+ if i < max then
+ let pred = types.(i + 1) in
+ let arc = {univ = u; lt = [pred]; le = []; rank = 0; status = Unset; } in
UMap.add u (Canonical arc) accu
else accu
in
@@ -1761,7 +1754,7 @@ let eq_puniverses f (x, u) (y, u') =
f x y && Instance.equal u u'
(** A context of universe levels with universe constraints,
- representiong local universe variables and constraints *)
+ representing local universe variables and constraints *)
module UContext =
struct
@@ -1775,7 +1768,7 @@ struct
let pr prl (univs, cst as ctx) =
if is_empty ctx then mt() else
- Instance.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst)
+ h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
let hcons (univs, cst) =
(Instance.hcons univs, hcons_constraints cst)
@@ -1785,8 +1778,11 @@ struct
let union (univs, cst) (univs', cst') =
Instance.append univs univs', Constraint.union cst cst'
-
+
let dest x = x
+
+ let size (x,_) = Instance.length x
+
end
type universe_context = UContext.t
@@ -1804,6 +1800,9 @@ struct
let empty = (LSet.empty, Constraint.empty)
let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst
+ let equal (univs, cst as x) (univs', cst' as y) =
+ x == y || (LSet.equal univs univs' && Constraint.equal cst cst')
+
let of_set s = (s, Constraint.empty)
let singleton l = of_set (LSet.singleton l)
let of_instance i = of_set (Instance.levels i)
@@ -1843,7 +1842,7 @@ struct
let pr prl (univs, cst as ctx) =
if is_empty ctx then mt() else
- LSet.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst)
+ h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
let constraints (univs, cst) = cst
let levels (univs, cst) = univs
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7aaf2ffe..c926c57b 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -20,7 +20,11 @@ sig
val is_small : t -> bool
(** Is the universe set or prop? *)
-
+
+ val is_prop : t -> bool
+ val is_set : t -> bool
+ (** Is it specifically Prop or Set *)
+
val compare : t -> t -> int
(** Comparison function *)
@@ -87,6 +91,9 @@ sig
val is_level : t -> bool
(** Test if the universe is a level or an algebraic universe. *)
+ val is_levels : t -> bool
+ (** Test if the universe is a lub of levels or contains +n's. *)
+
val level : t -> Level.t option
(** Try to get a level out of a universe, returns [None] if it
is an algebraic universe. *)
@@ -159,8 +166,12 @@ val is_initial_universes : universes -> bool
val sort_universes : universes -> universes
-(** Adds a universe to the graph, ensuring it is >= Prop. *)
-val add_universe : universe_level -> universes -> universes
+(** Adds a universe to the graph, ensuring it is >= or > Set.
+ @raises AlreadyDeclared if the level is already declared in the graph. *)
+
+exception AlreadyDeclared
+
+val add_universe : universe_level -> bool -> universes -> universes
(** {6 Constraints. } *)
@@ -332,6 +343,9 @@ sig
(** Keeps the order of the instances *)
val union : t -> t -> t
+ (* the number of universes in the context *)
+ val size : t -> int
+
end
type universe_context = UContext.t
@@ -349,6 +363,7 @@ sig
val of_instance : Instance.t -> t
val of_set : universe_set -> t
+ val equal : t -> t -> bool
val union : t -> t -> t
val append : t -> t -> t
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 88c1e103..a800e253 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -337,5 +337,5 @@ let subst_instance_context s ctx =
if Univ.Instance.is_empty s then ctx
else map_rel_context (fun x -> subst_instance_constr s x) ctx
-type id_key = pconstant tableKey
-let eq_id_key x y = Names.eq_table_key (Univ.eq_puniverses Constant.equal) x y
+type id_key = constant tableKey
+let eq_id_key x y = Names.eq_table_key Constant.equal x y
diff --git a/kernel/vars.mli b/kernel/vars.mli
index fdd4603b..c0fbeeb6 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -88,5 +88,5 @@ val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_
val subst_instance_constr : universe_instance -> constr -> constr
val subst_instance_context : universe_instance -> rel_context -> rel_context
-type id_key = pconstant tableKey
+type id_key = constant tableKey
val eq_id_key : id_key -> id_key -> bool
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 1c31cc04..4610dbcb 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -18,8 +18,8 @@ let compare_zipper z1 z2 =
match z1, z2 with
| Zapp args1, Zapp args2 -> Int.equal (nargs args1) (nargs args2)
| Zfix(f1,args1), Zfix(f2,args2) -> Int.equal (nargs args1) (nargs args2)
- | Zswitch _, Zswitch _ -> true
- | _ , _ -> false
+ | Zswitch _, Zswitch _ | Zproj _, Zproj _ -> true
+ | Zapp _ , _ | Zfix _, _ | Zswitch _, _ | Zproj _, _ -> false
let rec compare_stack stk1 stk2 =
match stk1, stk2 with
@@ -40,15 +40,20 @@ let conv_vect fconv vect1 vect2 cu =
!rcu
else raise NotConvertible
-let infos = ref (create_clos_infos betaiotazeta Environ.empty_env)
-
let rec conv_val env pb k v1 v2 cu =
if v1 == v2 then cu
else conv_whd env pb k (whd_val v1) (whd_val v2) cu
and conv_whd env pb k whd1 whd2 cu =
+(* Pp.(msg_debug (str "conv_whd(" ++ pr_whd whd1 ++ str ", " ++ pr_whd whd2 ++ str ")")) ; *)
match whd1, whd2 with
- | Vsort s1, Vsort s2 -> check_sort_cmp_universes env pb s1 s2 cu; cu
+ | Vsort s1, Vsort s2 -> sort_cmp_universes env pb s1 s2 cu
+ | Vuniv_level _ , _
+ | _ , Vuniv_level _ ->
+ (** Both of these are invalid since universes are handled via
+ ** special cases in the code.
+ **)
+ assert false
| Vprod p1, Vprod p2 ->
let cu = conv_val env CONV k (dom p1) (dom p2) cu in
conv_fun env pb k (codom p1) (codom p2) cu
@@ -76,50 +81,53 @@ and conv_whd env pb k whd1 whd2 cu =
| Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) ->
conv_atom env pb k a1 stk1 a2 stk2 cu
| Vfun _, _ | _, Vfun _ ->
- conv_val env CONV (k+1) (eta_whd k whd1) (eta_whd k whd2) cu
- | _, Vatom_stk(Aiddef(_,v),stk) ->
- conv_whd env pb k whd1 (force_whd v stk) cu
- | Vatom_stk(Aiddef(_,v),stk), _ ->
- conv_whd env pb k (force_whd v stk) whd2 cu
- | _, _ -> raise NotConvertible
+ conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu
+
+ | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _
+ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
+
and conv_atom env pb k a1 stk1 a2 stk2 cu =
+(* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *)
match a1, a2 with
- | Aind ind1, Aind ind2 ->
- if eq_puniverses eq_ind ind1 ind2 && compare_stack stk1 stk2
+ | Aind ((mi,i) as ind1) , Aind ind2 ->
+ if eq_ind ind1 ind2 && compare_stack stk1 stk2
then
- conv_stack env k stk1 stk2 cu
+ if Environ.polymorphic_ind ind1 env
+ then
+ let mib = Environ.lookup_mind mi env in
+ let ulen = Univ.UContext.size mib.Declarations.mind_universes in
+ match stk1 , stk2 with
+ | [], [] -> assert (Int.equal ulen 0); cu
+ | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
+ assert (ulen <= nargs args1);
+ assert (ulen <= nargs args2);
+ let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in
+ let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in
+ let u1 = Univ.Instance.of_array u1 in
+ let u2 = Univ.Instance.of_array u2 in
+ let cu = convert_instances ~flex:false u1 u2 cu in
+ conv_arguments env ~from:ulen k args1 args2
+ (conv_stack env k stk1' stk2' cu)
+ | _, _ -> assert false (* Should not happen if problem is well typed *)
+ else
+ conv_stack env k stk1 stk2 cu
else raise NotConvertible
| Aid ik1, Aid ik2 ->
if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
conv_stack env k stk1 stk2 cu
else raise NotConvertible
- | Aiddef(ik1,v1), Aiddef(ik2,v2) ->
- begin
- try
- if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
- conv_stack env k stk1 stk2 cu
- else raise NotConvertible
- with NotConvertible ->
- if oracle_order Univ.out_punivs (oracle_of_infos !infos)
- false ik1 ik2 then
- conv_whd env pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
- else conv_whd env pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
- end
- | Aiddef(ik1,v1), _ ->
- conv_whd env pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
- | _, Aiddef(ik2,v2) ->
- conv_whd env pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
- | _, _ -> raise NotConvertible
+ | Atype _ , _ | _, Atype _ -> assert false
+ | Aind _, _ | Aid _, _ -> raise NotConvertible
-and conv_stack env k stk1 stk2 cu =
+and conv_stack env ?from:(from=0) k stk1 stk2 cu =
match stk1, stk2 with
| [], [] -> cu
| Zapp args1 :: stk1, Zapp args2 :: stk2 ->
- conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu)
+ conv_stack env k stk1 stk2 (conv_arguments env ~from:from k args1 args2 cu)
| Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 ->
conv_stack env k stk1 stk2
- (conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu))
+ (conv_arguments env ~from:from k args1 args2 (conv_fix env k f1 f2 cu))
| Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
if check_switch sw1 sw2 then
let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
@@ -131,7 +139,11 @@ and conv_stack env k stk1 stk2 cu =
done;
conv_stack env k stk1 stk2 !rcu
else raise NotConvertible
- | _, _ -> raise NotConvertible
+ | Zproj p1 :: stk1, Zproj p2 :: stk2 ->
+ if Constant.equal p1 p2 then conv_stack env k stk1 stk2 cu
+ else raise NotConvertible
+ | [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _
+ | Zproj _ :: _, _ -> raise NotConvertible
and conv_fun env pb k f1 f2 cu =
if f1 == f2 then cu
@@ -159,98 +171,37 @@ and conv_cofix env k cf1 cf2 cu =
conv_vect (conv_val env CONV (k + Array.length tcf1)) bcf1 bcf2 cu
else raise NotConvertible
-and conv_arguments env k args1 args2 cu =
+and conv_arguments env ?from:(from=0) k args1 args2 cu =
if args1 == args2 then cu
else
let n = nargs args1 in
if Int.equal n (nargs args2) then
let rcu = ref cu in
- for i = 0 to n - 1 do
+ for i = from to n - 1 do
rcu := conv_val env CONV k (arg args1 i) (arg args2 i) !rcu
done;
!rcu
else raise NotConvertible
-let rec eq_puniverses f (x,l1) (y,l2) cu =
- if f x y then conv_universes l1 l2 cu
- else raise NotConvertible
-
-and conv_universes l1 l2 cu =
- if Univ.Instance.equal l1 l2 then cu else raise NotConvertible
-
-let rec conv_eq env pb t1 t2 cu =
- if t1 == t2 then cu
- else
- match kind_of_term t1, kind_of_term t2 with
- | Rel n1, Rel n2 ->
- if Int.equal n1 n2 then cu else raise NotConvertible
- | Meta m1, Meta m2 ->
- if Int.equal m1 m2 then cu else raise NotConvertible
- | Var id1, Var id2 ->
- if Id.equal id1 id2 then cu else raise NotConvertible
- | Sort s1, Sort s2 -> check_sort_cmp_universes env pb s1 s2 cu; cu
- | Cast (c1,_,_), _ -> conv_eq env pb c1 t2 cu
- | _, Cast (c2,_,_) -> conv_eq env pb t1 c2 cu
- | Prod (_,t1,c1), Prod (_,t2,c2) ->
- conv_eq env pb c1 c2 (conv_eq env CONV t1 t2 cu)
- | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq env CONV c1 c2 cu
- | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
- conv_eq env pb c1 c2 (conv_eq env CONV b1 b2 cu)
- | App (c1,l1), App (c2,l2) ->
- conv_eq_vect env l1 l2 (conv_eq env CONV c1 c2 cu)
- | Evar (e1,l1), Evar (e2,l2) ->
- if Evar.equal e1 e2 then conv_eq_vect env l1 l2 cu
- else raise NotConvertible
- | Const c1, Const c2 -> eq_puniverses eq_constant c1 c2 cu
- | Proj (p1,c1), Proj (p2,c2) ->
- if eq_constant (Projection.constant p1) (Projection.constant p2) then
- conv_eq env pb c1 c2 cu
- else raise NotConvertible
- | Ind c1, Ind c2 ->
- eq_puniverses eq_ind c1 c2 cu
- | Construct c1, Construct c2 ->
- eq_puniverses eq_constructor c1 c2 cu
- | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
- let pcu = conv_eq env CONV p1 p2 cu in
- let ccu = conv_eq env CONV c1 c2 pcu in
- conv_eq_vect env bl1 bl2 ccu
- | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
- if Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 then conv_eq_vect env tl1 tl2 (conv_eq_vect env bl1 bl2 cu)
- else raise NotConvertible
- | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
- if Int.equal ln1 ln2 then conv_eq_vect env tl1 tl2 (conv_eq_vect env bl1 bl2 cu)
- else raise NotConvertible
- | _ -> raise NotConvertible
-
-and conv_eq_vect env vt1 vt2 cu =
- let len = Array.length vt1 in
- if Int.equal len (Array.length vt2) then
- let rcu = ref cu in
- for i = 0 to len-1 do
- rcu := conv_eq env CONV vt1.(i) vt2.(i) !rcu
- done; !rcu
- else raise NotConvertible
-
-let vconv pb env t1 t2 =
- infos := create_clos_infos betaiotazeta env;
- let _cu =
- try conv_eq env pb t1 t2 (universes env)
- with NotConvertible ->
- let v1 = val_of_constr env t1 in
- let v2 = val_of_constr env t2 in
- let cu = conv_val env pb (nb_rel env) v1 v2 (universes env) in
- cu
- in ()
-
-let _ = Reduction.set_vm_conv vconv
-
-let use_vm = ref false
-
-let set_use_vm b =
- use_vm := b;
- if b then Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> vconv cv_pb)
- else Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> Reduction.conv_cmp cv_pb)
-
-let use_vm _ = !use_vm
-
-
+let vm_conv_gen cv_pb env univs t1 t2 =
+ try
+ let v1 = val_of_constr env t1 in
+ let v2 = val_of_constr env t2 in
+ fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
+ with Not_found | Invalid_argument _ ->
+ (Pp.msg_warning
+ (Pp.str "Bytecode compilation failed, falling back to default conversion");
+ Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
+ full_transparent_state env univs t1 t2)
+
+let vm_conv cv_pb env t1 t2 =
+ let univs = Environ.universes env in
+ let b =
+ if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2
+ else Constr.eq_constr_univs univs t1 t2
+ in
+ if not b then
+ let univs = (univs, checked_universes) in
+ let _ = vm_conv_gen cv_pb env univs t1 t2 in ()
+
+let _ = Reduction.set_vm_conv vm_conv
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 096d31ac..49e5d23e 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -12,9 +12,11 @@ open Reduction
(**********************************************************************
s conversion functions *)
-val use_vm : unit -> bool
-val set_use_vm : bool -> unit
-val vconv : conv_pb -> types conversion_function
+val vm_conv : conv_pb -> types conversion_function
-val val_of_constr : env -> constr -> values
+(** A conversion function parametrized by a universe comparator. Used outside of
+ the kernel. *)
+val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function
+(** Precompute a VM value from a constr *)
+val val_of_constr : env -> constr -> values
diff --git a/kernel/vm.ml b/kernel/vm.ml
index d4bf461b..64ddc437 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -19,8 +19,6 @@ external set_drawinstr : unit -> unit = "coq_set_drawinstr"
external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
external offset : Obj.t -> int = "coq_offset"
-let accu_tag = 0
-
(*******************************************)
(* Initalization of the abstract machine ***)
(*******************************************)
@@ -29,9 +27,6 @@ external init_vm : unit -> unit = "init_coq_vm"
let _ = init_vm ()
-external transp_values : unit -> bool = "get_coq_transp_value"
-external set_transp_values : bool -> unit = "coq_set_transp_value"
-
(*******************************************)
(* Machine code *** ************************)
(*******************************************)
@@ -126,11 +121,12 @@ type vswitch = {
(* *)
(* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ] *)
(* - representation of [accu] : tag_[....] *)
-(* -- tag <= 2 : encoding atom type (sorts, free vars, etc.) *)
-(* -- 3_[accu|fix_app] : a fixpoint blocked by an accu *)
-(* -- 4_[accu|vswitch] : a match blocked by an accu *)
-(* -- 5_[fcofix] : a cofix function *)
-(* -- 6_[fcofix|val] : a cofix function, val represent the value *)
+(* -- tag <= 3 : encoding atom type (sorts, free vars, etc.) *)
+(* -- 10_[accu|proj name] : a projection blocked by an accu *)
+(* -- 11_[accu|fix_app] : a fixpoint blocked by an accu *)
+(* -- 12_[accu|vswitch] : a match blocked by an accu *)
+(* -- 13_[fcofix] : a cofix function *)
+(* -- 14_[fcofix|val] : a cofix function, val represent the value *)
(* of the function applied to arg1 ... argn *)
(* The [arguments] type, which is abstracted as an array, represents : *)
(* tag[ _ | _ |v1|... | vn] *)
@@ -140,8 +136,8 @@ type vswitch = {
type atom =
| Aid of Vars.id_key
- | Aiddef of Vars.id_key * values
- | Aind of pinductive
+ | Aind of inductive
+ | Atype of Univ.universe
(* Zippers *)
@@ -149,6 +145,7 @@ type zipper =
| Zapp of arguments
| Zfix of vfix*arguments (* Possibly empty *)
| Zswitch of vswitch
+ | Zproj of Constant.t (* name of the projection *)
type stack = zipper list
@@ -163,28 +160,112 @@ type whd =
| Vconstr_const of int
| Vconstr_block of vblock
| Vatom_stk of atom * stack
+ | Vuniv_level of Univ.universe_level
+
+(************************************************)
+(* Abstract machine *****************************)
+(************************************************)
+
+(* gestion de la pile *)
+external push_ra : tcode -> unit = "coq_push_ra"
+external push_val : values -> unit = "coq_push_val"
+external push_arguments : arguments -> unit = "coq_push_arguments"
+external push_vstack : vstack -> unit = "coq_push_vstack"
+
+
+(* interpreteur *)
+external interprete : tcode -> values -> vm_env -> int -> values =
+ "coq_interprete_ml"
+
+
+
+(* Functions over arguments *)
+let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
+let arg args i =
+ if 0 <= i && i < (nargs args) then
+ val_of_obj (Obj.field (Obj.repr args) (i+2))
+ else invalid_arg
+ ("Vm.arg size = "^(string_of_int (nargs args))^
+ " acces "^(string_of_int i))
+
+(* Apply a value to arguments contained in [vargs] *)
+let apply_arguments vf vargs =
+ let n = nargs vargs in
+ if Int.equal n 0 then vf
+ else
+ begin
+ push_ra stop;
+ push_arguments vargs;
+ interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
+ end
+
+(* Apply value [vf] to an array of argument values [varray] *)
+let apply_varray vf varray =
+ let n = Array.length varray in
+ if Int.equal n 0 then vf
+ else
+ begin
+ push_ra stop;
+ push_vstack varray;
+ interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
+ end
(*************************************************)
(* Destructors ***********************************)
(*************************************************)
+let uni_lvl_val (v : values) : Univ.universe_level =
+ let whd = Obj.magic v in
+ match whd with
+ | Vuniv_level lvl -> lvl
+ | _ ->
+ let pr =
+ let open Pp in
+ match whd with
+ | Vsort _ -> str "Vsort"
+ | Vprod _ -> str "Vprod"
+ | Vfun _ -> str "Vfun"
+ | Vfix _ -> str "Vfix"
+ | Vcofix _ -> str "Vcofix"
+ | Vconstr_const i -> str "Vconstr_const"
+ | Vconstr_block b -> str "Vconstr_block"
+ | Vatom_stk (a,stk) -> str "Vatom_stk"
+ | _ -> assert false
+ in
+ Errors.anomaly
+ Pp.( strbrk "Parsing virtual machine value expected universe level, got "
+ ++ pr)
+
let rec whd_accu a stk =
let stk =
if Int.equal (Obj.size a) 2 then stk
else Zapp (Obj.obj a) :: stk in
let at = Obj.field a 1 in
match Obj.tag at with
- | i when i <= 2 ->
+ | i when Int.equal i type_atom_tag ->
+ begin match stk with
+ | [Zapp args] ->
+ let u = ref (Obj.obj (Obj.field at 0)) in
+ for i = 0 to nargs args - 1 do
+ u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i)))
+ done;
+ Vsort (Type !u)
+ | _ -> assert false
+ end
+ | i when i <= max_atom_tag ->
Vatom_stk(Obj.magic at, stk)
- | 3 (* fix_app tag *) ->
+ | i when Int.equal i proj_tag ->
+ let zproj = Zproj (Obj.obj (Obj.field at 0)) in
+ whd_accu (Obj.field at 1) (zproj :: stk)
+ | i when Int.equal i fix_app_tag ->
let fa = Obj.field at 1 in
let zfix =
Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
whd_accu (Obj.field at 0) (zfix :: stk)
- | 4 (* switch tag *) ->
+ | i when Int.equal i switch_tag ->
let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
whd_accu (Obj.field at 0) (zswitch :: stk)
- | 5 (* cofix_tag *) ->
+ | i when Int.equal i cofix_tag ->
let vcfx = Obj.obj (Obj.field at 0) in
let to_up = Obj.obj a in
begin match stk with
@@ -192,7 +273,7 @@ let rec whd_accu a stk =
| [Zapp args] -> Vcofix(vcfx, to_up, Some args)
| _ -> assert false
end
- | 6 (* cofix_evaluated_tag *) ->
+ | i when Int.equal i cofix_evaluated_tag ->
let vcofix = Obj.obj (Obj.field at 0) in
let res = Obj.obj a in
begin match stk with
@@ -200,7 +281,9 @@ let rec whd_accu a stk =
| [Zapp args] -> Vcofix(vcofix, res, Some args)
| _ -> assert false
end
- | _ -> assert false
+ | tg ->
+ Errors.anomaly
+ Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg)
external kind_of_closure : Obj.t -> int = "coq_kind_of_closure"
@@ -213,65 +296,19 @@ let whd_val : values -> whd =
if tag = accu_tag then
(
if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *)
- else
+ else
if is_accumulate (fun_code o) then whd_accu o []
- else (Vprod(Obj.obj o)))
+ else Vprod(Obj.obj o))
else
if tag = Obj.closure_tag || tag = Obj.infix_tag then
- ( match kind_of_closure o with
+ (match kind_of_closure o with
| 0 -> Vfun(Obj.obj o)
| 1 -> Vfix(Obj.obj o, None)
| 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
| 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
| _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work"))
- else
- Vconstr_block(Obj.obj o)
-
-(************************************************)
-(* Abstrct machine ******************************)
-(************************************************)
-
-(* gestion de la pile *)
-external push_ra : tcode -> unit = "coq_push_ra"
-external push_val : values -> unit = "coq_push_val"
-external push_arguments : arguments -> unit = "coq_push_arguments"
-external push_vstack : vstack -> unit = "coq_push_vstack"
-
-
-(* interpreteur *)
-external interprete : tcode -> values -> vm_env -> int -> values =
- "coq_interprete_ml"
-
-
-
-(* Functions over arguments *)
-let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
-let arg args i =
- if 0 <= i && i < (nargs args) then
- val_of_obj (Obj.field (Obj.repr args) (i+2))
- else invalid_arg
- ("Vm.arg size = "^(string_of_int (nargs args))^
- " acces "^(string_of_int i))
-
-let apply_arguments vf vargs =
- let n = nargs vargs in
- if Int.equal n 0 then vf
- else
- begin
- push_ra stop;
- push_arguments vargs;
- interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
- end
-
-let apply_vstack vf vstk =
- let n = Array.length vstk in
- if Int.equal n 0 then vf
- else
- begin
- push_ra stop;
- push_vstack vstk;
- interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
- end
+ else
+ Vconstr_block(Obj.obj o)
(**********************************************)
(* Constructors *******************************)
@@ -289,6 +326,7 @@ let rec obj_of_str_const str =
match str with
| Const_sorts s -> Obj.repr (Vsort s)
| Const_ind ind -> obj_of_atom (Aind ind)
+ | Const_proj p -> Obj.repr p
| Const_b0 tag -> Obj.repr tag
| Const_bn(tag, args) ->
let len = Array.length args in
@@ -297,6 +335,8 @@ let rec obj_of_str_const str =
Obj.set_field res i (obj_of_str_const args.(i))
done;
res
+ | Const_univ_level l -> Obj.repr (Vuniv_level l)
+ | Const_type u -> obj_of_atom (Atype u)
let val_of_obj o = ((Obj.obj o) : values)
@@ -304,13 +344,22 @@ let val_of_str_const str = val_of_obj (obj_of_str_const str)
let val_of_atom a = val_of_obj (obj_of_atom a)
+let atom_of_proj kn v =
+ let r = Obj.new_block proj_tag 2 in
+ Obj.set_field r 0 (Obj.repr kn);
+ Obj.set_field r 1 (Obj.repr v);
+ ((Obj.obj r) : atom)
+
+let val_of_proj kn v =
+ val_of_atom (atom_of_proj kn v)
+
module IdKeyHash =
struct
- type t = pconstant tableKey
- let equal = Names.eq_table_key (Univ.eq_puniverses Constant.equal)
+ type t = constant tableKey
+ let equal = Names.eq_table_key Constant.equal
open Hashset.Combine
let hash = function
- | ConstKey (c,u) -> combinesmall 1 (Constant.hash c)
+ | ConstKey c -> combinesmall 1 (Constant.hash c)
| VarKey id -> combinesmall 2 (Id.hash id)
| RelKey i -> combinesmall 3 (Int.hash i)
end
@@ -354,14 +403,14 @@ external closure_arity : vfun -> int = "coq_closure_arity"
let body_of_vfun k vf =
let vargs = mkrel_vstack k 1 in
- apply_vstack (Obj.magic vf) vargs
+ apply_varray (Obj.magic vf) vargs
let decompose_vfun2 k vf1 vf2 =
let arity = min (closure_arity vf1) (closure_arity vf2) in
assert (0 < arity && arity < Sys.max_array_length);
let vargs = mkrel_vstack k arity in
- let v1 = apply_vstack (Obj.magic vf1) vargs in
- let v2 = apply_vstack (Obj.magic vf2) vargs in
+ let v1 = apply_varray (Obj.magic vf1) vargs in
+ let v2 = apply_varray (Obj.magic vf2) vargs in
arity, v1, v2
(* Functions over fixpoint *)
@@ -491,7 +540,7 @@ let reduce_cofix k vcf =
let self = Obj.new_block accu_tag 2 in
Obj.set_field self 0 (Obj.repr accumulate);
Obj.set_field self 1 (Obj.repr atom);
- apply_vstack (Obj.obj e) [|Obj.obj self|] in
+ apply_varray (Obj.obj e) [|Obj.obj self|] in
(Array.init ndef cofix_body, ftyp)
@@ -544,62 +593,13 @@ let branch_of_switch k sw =
in
Array.map eval_branch sw.sw_annot.rtbl
-
-
-(* Evaluation *)
-
-let rec whd_stack v stk =
- match stk with
- | [] -> whd_val v
- | Zapp args :: stkt -> whd_stack (apply_arguments v args) stkt
- | Zfix (f,args) :: stkt ->
- let o = Obj.repr v in
- if Obj.is_block o && Obj.tag o = accu_tag then
- whd_accu (Obj.repr v) stk
- else
- let v', stkt =
- match stkt with
- | Zapp args' :: stkt ->
- push_ra stop;
- push_arguments args';
- push_val v;
- push_arguments args;
- let v' =
- interprete (fun_code f) (Obj.magic f) (Obj.magic f)
- (nargs args+ nargs args') in
- v', stkt
- | _ ->
- push_ra stop;
- push_val v;
- push_arguments args;
- let v' =
- interprete (fun_code f) (Obj.magic f) (Obj.magic f)
- (nargs args) in
- v', stkt
- in
- whd_stack v' stkt
- | Zswitch sw :: stkt ->
- let o = Obj.repr v in
- if Obj.is_block o && Obj.tag o = accu_tag then
- if Obj.tag (Obj.field o 1) < cofix_tag then whd_accu (Obj.repr v) stk
- else
- let to_up =
- match whd_accu (Obj.repr v) [] with
- | Vcofix (_, to_up, _) -> to_up
- | _ -> assert false in
- whd_stack (apply_switch sw to_up) stkt
- else whd_stack (apply_switch sw v) stkt
-
-let rec force_whd v stk =
- match whd_stack v stk with
- | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk
- | res -> res
-
-
-let rec eta_stack a stk v =
+(* Apply the term represented by a under stack stk to argument v *)
+(* t = a stk --> t v *)
+let rec apply_stack a stk v =
match stk with
- | [] -> apply_vstack a [|v|]
- | Zapp args :: stk -> eta_stack (apply_arguments a args) stk v
+ | [] -> apply_varray a [|v|]
+ | Zapp args :: stk -> apply_stack (apply_arguments a args) stk v
+ | Zproj kn :: stk -> apply_stack (val_of_proj kn a) stk v
| Zfix(f,args) :: stk ->
let a,stk =
match stk with
@@ -620,11 +620,11 @@ let rec eta_stack a stk v =
interprete (fun_code f) (Obj.magic f) (Obj.magic f)
(nargs args) in
a, stk in
- eta_stack a stk v
+ apply_stack a stk v
| Zswitch sw :: stk ->
- eta_stack (apply_switch sw a) stk v
+ apply_stack (apply_switch sw a) stk v
-let eta_whd k whd =
+let apply_whd k whd =
let v = val_of_rel k in
match whd with
| Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false
@@ -643,8 +643,35 @@ let eta_whd k whd =
push_val v;
interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0
| Vatom_stk(a,stk) ->
- eta_stack (val_of_atom a) stk v
-
-
-
-
+ apply_stack (val_of_atom a) stk v
+ | Vuniv_level lvl -> assert false
+
+let rec pr_atom a =
+ Pp.(match a with
+ | Aid c -> str "Aid(" ++ (match c with
+ | ConstKey c -> Names.pr_con c
+ | RelKey i -> str "#" ++ int i
+ | _ -> str "...") ++ str ")"
+ | Aind (mi,i) -> str "Aind(" ++ Names.pr_mind mi ++ str "#" ++ int i ++ str ")"
+ | Atype _ -> str "Atype(")
+and pr_whd w =
+ Pp.(match w with
+ | Vsort _ -> str "Vsort"
+ | Vprod _ -> str "Vprod"
+ | Vfun _ -> str "Vfun"
+ | Vfix _ -> str "Vfix"
+ | Vcofix _ -> str "Vcofix"
+ | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")"
+ | Vconstr_block b -> str "Vconstr_block"
+ | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")"
+ | Vuniv_level _ -> assert false)
+and pr_stack stk =
+ Pp.(match stk with
+ | [] -> str "[]"
+ | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk)
+and pr_zipper z =
+ Pp.(match z with
+ | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")"
+ | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")"
+ | Zswitch s -> str "Zswitch(...)"
+ | Zproj c -> str "Zproj(" ++ Names.pr_con c ++ str ")")
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 51903568..43a42eb9 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -2,13 +2,10 @@ open Names
open Term
open Cbytecodes
-(** Efficient Virtual Machine *)
+(** Debug printing *)
val set_drawinstr : unit -> unit
-val transp_values : unit -> bool
-val set_transp_values : bool -> unit
-
(** Machine code *)
type tcode
@@ -25,8 +22,8 @@ type arguments
type atom =
| Aid of Vars.id_key
- | Aiddef of Vars.id_key * values
- | Aind of pinductive
+ | Aind of inductive
+ | Atype of Univ.universe
(** Zippers *)
@@ -34,6 +31,7 @@ type zipper =
| Zapp of arguments
| Zfix of vfix * arguments (** might be empty *)
| Zswitch of vswitch
+ | Zproj of Constant.t (* name of the projection *)
type stack = zipper list
@@ -48,19 +46,24 @@ type whd =
| Vconstr_const of int
| Vconstr_block of vblock
| Vatom_stk of atom * stack
+ | Vuniv_level of Univ.universe_level
+
+val pr_atom : atom -> Pp.std_ppcmds
+val pr_whd : whd -> Pp.std_ppcmds
(** Constructors *)
val val_of_str_const : structured_constant -> values
val val_of_rel : int -> values
val val_of_named : Id.t -> values
-val val_of_constant : pconstant -> values
+val val_of_constant : constant -> values
external val_of_annot_switch : annot_switch -> values = "%identity"
(** Destructors *)
val whd_val : values -> whd
+val uni_lvl_val : values -> Univ.universe_level
(** Arguments *)
@@ -105,10 +108,6 @@ val case_info : vswitch -> case_info
val type_of_switch : vswitch -> values
val branch_of_switch : int -> vswitch -> (int * values) array
-(** Evaluation *)
-
-val whd_stack : values -> stack -> whd
-val force_whd : values -> stack -> whd
-
-val eta_whd : int -> whd -> values
+(** Apply a value *)
+val apply_whd : int -> whd -> values