From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- kernel/byterun/coq_fix_code.c | 2 +- kernel/byterun/coq_gc.h | 13 +- kernel/byterun/coq_instruct.h | 1 + kernel/byterun/coq_interp.c | 79 ++++++++--- kernel/byterun/coq_memory.c | 16 --- kernel/byterun/coq_values.c | 1 - kernel/byterun/coq_values.h | 19 +-- kernel/cbytecodes.ml | 251 +++++++++++++++++++--------------- kernel/cbytecodes.mli | 71 ++++++---- kernel/cbytegen.ml | 266 ++++++++++++++++++++++++++---------- kernel/cbytegen.mli | 10 +- kernel/cemitcodes.ml | 35 +++-- kernel/cemitcodes.mli | 4 +- kernel/constr.ml | 54 ++++---- kernel/constr.mli | 20 +-- kernel/conv_oracle.ml | 15 ++- kernel/csymtable.ml | 44 +++--- kernel/declarations.mli | 21 ++- kernel/declareops.ml | 18 +-- kernel/declareops.mli | 12 +- kernel/entries.mli | 25 +++- kernel/environ.ml | 59 +++++--- kernel/environ.mli | 13 +- kernel/fast_typeops.ml | 8 +- kernel/indtypes.ml | 109 ++++++++------- kernel/indtypes.mli | 2 +- kernel/inductive.ml | 105 ++++++++------- kernel/mod_subst.ml | 2 +- kernel/mod_subst.mli | 5 +- kernel/mod_typing.ml | 119 +++++++++++----- kernel/mod_typing.mli | 13 +- kernel/modops.ml | 12 +- kernel/modops.mli | 3 - kernel/names.ml | 36 +++-- kernel/names.mli | 4 + kernel/nativecode.ml | 32 +++-- kernel/nativecode.mli | 26 ++-- kernel/nativeconv.ml | 136 +++++++++++-------- kernel/nativeconv.mli | 4 + kernel/nativelambda.ml | 38 +++--- kernel/nativelambda.mli | 2 +- kernel/nativelib.ml | 28 ++-- kernel/nativelibrary.ml | 4 +- kernel/nativelibrary.mli | 2 +- kernel/nativevalues.ml | 2 +- kernel/opaqueproof.ml | 5 +- kernel/pre_env.ml | 6 +- kernel/pre_env.mli | 3 +- kernel/reduction.ml | 58 +++----- kernel/reduction.mli | 27 ++-- kernel/safe_typing.ml | 278 ++++++++++++++++++++++++-------------- kernel/safe_typing.mli | 61 ++++++--- kernel/sorts.ml | 10 +- kernel/subtyping.ml | 13 +- kernel/term.ml | 28 +++- kernel/term.mli | 31 +++-- kernel/term_typing.ml | 302 ++++++++++++++++++++++++++++++++++------- kernel/term_typing.mli | 41 ++++-- kernel/typeops.ml | 26 ++-- kernel/univ.ml | 235 ++++++++++++++++---------------- kernel/univ.mli | 21 ++- kernel/vars.ml | 4 +- kernel/vars.mli | 2 +- kernel/vconv.ml | 191 ++++++++++---------------- kernel/vconv.mli | 10 +- kernel/vm.ml | 305 +++++++++++++++++++++++------------------- kernel/vm.mli | 25 ++-- 67 files changed, 2052 insertions(+), 1371 deletions(-) (limited to 'kernel') 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 #include +#include 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 "@[%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 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 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 -- cgit v1.2.3