diff options
Diffstat (limited to 'kernel')
46 files changed, 912 insertions, 1179 deletions
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c index 29e33d349b..d5feafbf91 100644 --- a/kernel/byterun/coq_fix_code.c +++ b/kernel/byterun/coq_fix_code.c @@ -57,7 +57,7 @@ void init_arity () { arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]= arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]= arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]= - arity[BRANCH]=arity[ISCONST]= 1; + arity[BRANCH]=arity[ISCONST]=arity[ENSURESTACKCAPACITY]=1; /* instruction with two operands */ arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]= arity[ARECONST]=arity[PROJ]=2; @@ -79,7 +79,7 @@ void * coq_stat_alloc (asize_t sz) value coq_makeaccu (value i) { code_t q; - code_t res = coq_stat_alloc(8); + code_t res = coq_stat_alloc(2 * sizeof(opcode_t)); q = res; *q++ = VALINSTR(MAKEACCU); *q = (opcode_t)Int_val(i); @@ -91,13 +91,13 @@ value coq_pushpop (value i) { int n; n = Int_val(i); if (n == 0) { - res = coq_stat_alloc(4); + res = coq_stat_alloc(sizeof(opcode_t)); *res = VALINSTR(STOP); return (value)res; } else { code_t q; - res = coq_stat_alloc(12); + res = coq_stat_alloc(3 * sizeof(opcode_t)); q = res; *q++ = VALINSTR(POP); *q++ = (opcode_t)n; diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h index 8c5ab0ecbd..d92e85fdf8 100644 --- a/kernel/byterun/coq_instruct.h +++ b/kernel/byterun/coq_instruct.h @@ -14,6 +14,8 @@ /* Nota: this list of instructions is parsed to produce derived files */ /* coq_jumptbl.h and copcodes.ml. Instructions should be uppercase */ /* and alone on lines starting by two spaces. */ +/* If adding an instruction, DON'T FORGET TO UPDATE coq_fix_code.c */ +/* with the arity of the instruction and maybe coq_tcode_of_code. */ enum instructions { ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC, @@ -37,6 +39,7 @@ enum instructions { GETFIELD0, GETFIELD1, GETFIELD, SETFIELD0, SETFIELD1, SETFIELD, PROJ, + ENSURESTACKCAPACITY, 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 df5fdce755..af89712d5e 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -23,9 +23,9 @@ #include "coq_values.h" /* spiwack: I append here a few macros for value/number manipulation */ -#define uint32_of_value(val) (((uint32_t)val >> 1)) -#define value_of_uint32(i) ((value)(((uint32_t)(i) << 1) | 1)) -#define UI64_of_uint32(lo) ((uint64_t)(lo)) +#define uint32_of_value(val) (((uint32_t)(val)) >> 1) +#define value_of_uint32(i) ((value)((((uint32_t)(i)) << 1) | 1)) +#define UI64_of_uint32(lo) ((uint64_t)((uint32_t)(lo))) #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val))) /* /spiwack */ @@ -76,6 +76,14 @@ sp is a local copy of the global variable extern_sp. */ # define print_lint(i) #endif +#define CHECK_STACK(num_args) { \ +if (sp - num_args < coq_stack_threshold) { \ + coq_sp = sp; \ + realloc_coq_stack(num_args + Coq_stack_threshold / sizeof(value)); \ + sp = coq_sp; \ + } \ +} + /* GC interface */ #define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; } #define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; } @@ -198,6 +206,9 @@ value coq_interprete sp = coq_sp; pc = coq_pc; accu = coq_accu; + + CHECK_STACK(0); + #ifdef THREADED_CODE goto *(void *)(coq_jumptbl_base + *pc++); /* Jump to the first instruction */ #else @@ -354,7 +365,7 @@ value coq_interprete coq_extra_args = *pc - 1; pc = Code_val(accu); coq_env = accu; - goto check_stacks; + goto check_stack; } Instruct(APPLY1) { value arg1 = sp[0]; @@ -371,7 +382,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args = 0; - goto check_stacks; + goto check_stack; } Instruct(APPLY2) { value arg1 = sp[0]; @@ -386,7 +397,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args = 1; - goto check_stacks; + goto check_stack; } Instruct(APPLY3) { value arg1 = sp[0]; @@ -403,17 +414,13 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args = 2; - goto check_stacks; + goto check_stack; } /* Stack checks */ - check_stacks: - print_instr("check_stacks"); - if (sp < coq_stack_threshold) { - coq_sp = sp; - realloc_coq_stack(Coq_stack_threshold); - sp = coq_sp; - } + check_stack: + print_instr("check_stack"); + CHECK_STACK(0); /* We also check for signals */ if (caml_signals_are_pending) { /* If there's a Ctrl-C, we reset the vm */ @@ -422,6 +429,16 @@ value coq_interprete } Next; + Instruct(ENSURESTACKCAPACITY) { + print_instr("ENSURESTACKCAPACITY"); + int size = *pc++; + /* CHECK_STACK may trigger here a useless allocation because of the + threshold, but check_stack: often does it anyway, so we prefer to + factorize the code. */ + CHECK_STACK(size); + Next; + } + Instruct(APPTERM) { int nargs = *pc++; int slotsize = *pc; @@ -436,7 +453,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args += nargs - 1; - goto check_stacks; + goto check_stack; } Instruct(APPTERM1) { value arg1 = sp[0]; @@ -445,7 +462,7 @@ value coq_interprete sp[0] = arg1; pc = Code_val(accu); coq_env = accu; - goto check_stacks; + goto check_stack; } Instruct(APPTERM2) { value arg1 = sp[0]; @@ -458,7 +475,7 @@ value coq_interprete print_lint(accu); coq_env = accu; coq_extra_args += 1; - goto check_stacks; + goto check_stack; } Instruct(APPTERM3) { value arg1 = sp[0]; @@ -472,7 +489,7 @@ value coq_interprete pc = Code_val(accu); coq_env = accu; coq_extra_args += 2; - goto check_stacks; + goto check_stack; } Instruct(RETURN) { @@ -503,6 +520,7 @@ value coq_interprete int num_args = Wosize_val(coq_env) - 2; int i; print_instr("RESTART"); + CHECK_STACK(num_args); sp -= num_args; for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2); coq_env = Field(coq_env, 1); @@ -539,6 +557,7 @@ value coq_interprete pc++;/* On saute le Restart */ } else { if (coq_extra_args < rec_pos) { + /* Partial application */ mlsize_t num_args, i; num_args = 1 + coq_extra_args; /* arg1 + extra args */ Alloc_small(accu, num_args + 2, Closure_tag); @@ -553,10 +572,10 @@ value coq_interprete } else { /* The recursif argument is an accumulator */ mlsize_t num_args, i; - /* Construction of partially applied PF */ + /* Construction of fixpoint applied to its [rec_pos-1] first arguments */ Alloc_small(accu, rec_pos + 2, Closure_tag); - Field(accu, 1) = coq_env; - for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; + Field(accu, 1) = coq_env; // We store the fixpoint in the first field + for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i]; // Storing args Code_val(accu) = pc; sp += rec_pos; *--sp = accu; @@ -862,29 +881,7 @@ value coq_interprete sp++; Next; } - - /* *sp = accu; - * Netoyage des cofix * - size = Wosize_val(accu); - for (i = 2; i < size; i++) { - accu = Field(*sp, i); - if (IS_EVALUATED_COFIX(accu)) { - size_aux = Wosize_val(accu); - *--sp = accu; - Alloc_small(accu, size_aux, Accu_tag); - for(j = 0; j < size_aux; j++) Field(accu, j) = Field(*sp, j); - *sp = accu; - Alloc_small(accu, 1, ATOM_COFIX_TAG); - Field(accu, 0) = Field(Field(*sp, 1), 0); - caml_modify(&Field(*sp, 1), accu); - accu = *sp; sp++; - caml_modify(&Field(*sp, i), accu); - } - } - sp++; - Next; - } */ - + Instruct(SETFIELD){ print_instr("SETFIELD"); caml_modify(&Field(accu, *pc),*sp); @@ -894,25 +891,58 @@ value coq_interprete Instruct(PROJ){ + do_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; - accu = block; - /* Create accumulator */ - Alloc_small(block, 2, Accu_tag); - Code_val(block) = accumulate; - Field(block, 1) = accu; - accu = block; + *--sp = accu; // Save matched block on stack + accu = Field(accu, 1); // Save atom to accu register + switch (Tag_val(accu)) { + case ATOM_COFIX_TAG: // We are forcing a cofix + { + mlsize_t i, nargs; + sp -= 2; + // Push the current instruction as the return address + sp[0] = (value)(pc - 1); + sp[1] = coq_env; + coq_env = Field(accu, 0); // Pointer to suspension + accu = sp[2]; // Save accumulator to accu register + sp[2] = Val_long(coq_extra_args); // Push number of args for return + nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom) + // Push arguments to stack + CHECK_STACK(nargs + 1); + sp -= nargs; + for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 2); + *--sp = accu; // Last argument is the pointer to the suspension + coq_extra_args = nargs; + pc = Code_val(coq_env); // Trigger evaluation + goto check_stack; + } + case ATOM_COFIXEVALUATED_TAG: + { + accu = Field(accu, 1); + ++sp; + goto do_proj; + } + default: + { + value block; + /* Skip over the index of projected field */ + ++pc; + /* Create atom */ + Alloc_small(accu, 2, ATOM_PROJ_TAG); + Field(accu, 0) = Field(coq_global_data, *pc++); + Field(accu, 1) = *sp++; + /* Create accumulator */ + Alloc_small(block, 2, Accu_tag); + Code_val(block) = accumulate; + Field(block, 1) = accu; + accu = block; + } + } } else { - accu = Field(accu, *pc++); + accu = Field(accu, *pc); + pc += 2; } - pc++; Next; } @@ -978,28 +1008,31 @@ value coq_interprete } Instruct(MAKESWITCHBLOCK) { print_instr("MAKESWITCHBLOCK"); - *--sp = accu; - accu = Field(accu,1); + *--sp = accu; // Save matched block on stack + accu = Field(accu,1); // Save atom to accu register switch (Tag_val(accu)) { - case ATOM_COFIX_TAG: + case ATOM_COFIX_TAG: // We are forcing a cofix { mlsize_t i, nargs; print_instr("COFIX_TAG"); sp-=2; pc++; + // Push the return address sp[0] = (value) (pc + *pc); sp[1] = coq_env; - coq_env = Field(accu,0); - accu = sp[2]; - sp[2] = Val_long(coq_extra_args); - nargs = Wosize_val(accu) - 2; + coq_env = Field(accu,0); // Pointer to suspension + accu = sp[2]; // Save accumulator to accu register + sp[2] = Val_long(coq_extra_args); // Push number of args for return + nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom) + // Push arguments to stack + CHECK_STACK(nargs+1); sp -= nargs; - for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); - *--sp = accu; + for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2); + *--sp = accu; // Last argument is the pointer to the suspension print_lint(nargs); coq_extra_args = nargs; - pc = Code_val(coq_env); - goto check_stacks; + pc = Code_val(coq_env); // Trigger evaluation + goto check_stack; } case ATOM_COFIXEVALUATED_TAG: { @@ -1024,7 +1057,7 @@ value coq_interprete annot = *pc++; sz = *pc++; *--sp=Field(coq_global_data, annot); - /* On sauve la pile */ + /* We save the stack */ if (sz == 0) accu = Atom(0); else { Alloc_small(accu, sz, Default_tag); @@ -1035,17 +1068,17 @@ value coq_interprete } } *--sp = accu; - /* On cree le zipper switch */ + /* We create the switch zipper */ Alloc_small(accu, 5, Default_tag); Field(accu, 0) = (value)typlbl; Field(accu, 1) = (value)swlbl; Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; Field(accu, 4) = coq_env; sp++;sp[0] = accu; - /* On cree l'atome */ + /* We create the atom */ Alloc_small(accu, 2, ATOM_SWITCH_TAG); Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0]; sp++;sp[0] = accu; - /* On cree l'accumulateur */ + /* We create the accumulator */ Alloc_small(accu, 2, Accu_tag); Code_val(accu) = accumulate; Field(accu,1) = *sp++; @@ -1206,7 +1239,7 @@ value coq_interprete Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */ /*unsigned shift*/ Field(accu, 0) = (value)((p >> 31)|1) ; /*higher part*/ - Field(accu, 1) = (value)((int32_t)p|1); /*lower part*/ + Field(accu, 1) = (value)((uint32_t)p|1); /*lower part*/ } Next; } @@ -1457,26 +1490,32 @@ value coq_push_val(value v) { value coq_push_arguments(value args) { int nargs,i; + value * sp = coq_sp; nargs = Wosize_val(args) - 2; + CHECK_STACK(nargs); coq_sp -= nargs; print_instr("push_args");print_int(nargs); for(i = 0; i < nargs; i++) coq_sp[i] = Field(args, i+2); return Val_unit; } -value coq_push_vstack(value stk) { +value coq_push_vstack(value stk, value max_stack_size) { int len,i; + value * sp = coq_sp; len = Wosize_val(stk); + CHECK_STACK(len); coq_sp -= len; print_instr("push_vstack");print_int(len); for(i = 0; i < len; i++) coq_sp[i] = Field(stk,i); + sp = coq_sp; + CHECK_STACK(uint32_of_value(max_stack_size)); return Val_unit; } value coq_interprete_ml(value tcode, value a, value e, value ea) { print_instr("coq_interprete"); return coq_interprete((code_t)tcode, a, e, Long_val(ea)); - print_instr("end coq_interprete"); + print_instr("end coq_interprete"); } value coq_eval_tcode (value tcode, value e) { diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index c9bcdc32ff..45cfae509d 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -130,6 +130,7 @@ value init_coq_vm(value unit) /* ML */ return Val_unit;; } +/* [required_space] is a size in words */ void realloc_coq_stack(asize_t required_space) { asize_t size; diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index d475f097ce..fe9ec5794c 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -270,11 +270,9 @@ let info_env info = info.i_cache.i_env open Context.Named.Declaration -let rec assoc_defined id = function -| [] -> raise Not_found -| LocalAssum _ :: ctxt -> assoc_defined id ctxt -| LocalDef (id', c, _) :: ctxt -> - if Id.equal id id' then c else assoc_defined id ctxt +let assoc_defined id env = match Environ.lookup_named id env with +| LocalDef (_, c, _) -> c +| _ -> raise Not_found let ref_value_cache ({i_cache = cache} as infos) ref = try @@ -291,7 +289,7 @@ let ref_value_cache ({i_cache = cache} as infos) ref = | None -> raise Not_found | Some t -> lift n t end - | VarKey id -> assoc_defined id (named_context cache.i_env) + | VarKey id -> assoc_defined id cache.i_env | ConstKey cst -> constant_value_in cache.i_env cst in let v = cache.i_repr infos body in diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 8d4de523a1..94ca4c72dd 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -43,7 +43,7 @@ type structured_constant = type reloc_table = (tag * int) array type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool} + {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} module Label = struct @@ -87,6 +87,7 @@ type instruction = | Ksequence of bytecodes * bytecodes | Kproj of int * Constant.t (* index of the projected argument, name of projection *) + | Kensurestackcapacity of int (* spiwack: instructions concerning integers *) | Kbranch of Label.t (* jump to label *) | Kaddint31 (* adds the int31 in the accu @@ -264,6 +265,8 @@ let rec pp_instr i = | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p + | Kensurestackcapacity size -> str "growstack " ++ int size + | Kaddint31 -> str "addint31" | Kaddcint31 -> str "addcint31" | Kaddcarrycint31 -> str "addcarrycint31" @@ -296,7 +299,7 @@ and 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 + 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 *) diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 5f1f09d00c..b8de7619cf 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -39,7 +39,7 @@ val pp_struct_const : structured_constant -> Pp.std_ppcmds type reloc_table = (tag * int) array type annot_switch = - {ci : case_info; rtbl : reloc_table; tailcall : bool} + {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} module Label : sig @@ -84,6 +84,7 @@ type instruction = | Ksequence of bytecodes * bytecodes | Kproj of int * Constant.t (** index of the projected argument, name of projection *) + | Kensurestackcapacity of int (** spiwack: instructions concerning integers *) | Kbranch of Label.t (** jump to label, is it needed ? *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 008955d804..57b397e6f8 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -91,6 +91,11 @@ open Pre_env (* In Cfxe_t accumulators, we need to store [fcofixi] for testing *) (* conversion of cofixpoints (which is intentional). *) +module Config = struct + let stack_threshold = 256 (* see byterun/coq_memory.h *) + let stack_safety_margin = 15 +end + type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t let empty_fv = { size= 0; fv_rev = []; fv_fwd = FvMap.empty } @@ -112,6 +117,26 @@ let empty_comp_env ?(univs=0) ()= in_env = ref empty_fv } +(* Maximal stack size reached during the current function body. Used to + reallocate the stack if we lack space. *) +let max_stack_size = ref 0 + +let set_max_stack_size stack_size = + if stack_size > !max_stack_size then + max_stack_size := stack_size + +let ensure_stack_capacity f x = + let old = !max_stack_size in + max_stack_size := 0; + let code = f x in + let used_safe = + !max_stack_size + Config.stack_safety_margin + in + max_stack_size := old; + if used_safe > Config.stack_threshold then + Kensurestackcapacity used_safe :: code + else code + (*i Creation functions for comp_env *) let rec add_param n sz l = @@ -370,14 +395,28 @@ let const_bn tag args = else Const_bn(last_variant_tag, Array.append [|Const_b0 (tag - last_variant_tag) |] args) - -let code_makeblock arity tag cont = +(* +If [tag] hits the OCaml limitation for non constant constructors, we switch to +another representation for the remaining constructors: +[last_variant_tag|tag - last_variant_tag|args] + +We subtract last_variant_tag for efficiency of match interpretation. + *) + +let nest_block tag arity cont = + Kconst (Const_b0 (tag - last_variant_tag)) :: + Kmakeblock(arity+1, last_variant_tag) :: cont + +let code_makeblock ~stack_size ~arity ~tag cont = if tag < last_variant_tag then Kmakeblock(arity, tag) :: cont - else - Kpush :: Kconst (Const_b0 (tag - last_variant_tag)) :: - Kmakeblock(arity+1, last_variant_tag) :: cont + else begin + set_max_stack_size (stack_size + 1); + Kpush :: nest_block tag arity cont + end +(* [code_construct] compiles an abstracted constructor dropping parameters and + updates [fun_code] *) (* Inv : nparam + arity > 0 *) let code_construct tag nparams arity cont = let f_cont = @@ -386,11 +425,11 @@ let code_construct tag nparams arity cont = [Kconst (Const_b0 tag); Kreturn 0] else if tag < last_variant_tag then [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0] - else - [Kconst (Const_b0 (tag - last_variant_tag)); - Kmakeblock(arity+1, last_variant_tag); Kreturn 0]) + else + nest_block tag arity [Kreturn 0]) in let lbl = Label.create() in + (* No need to grow the stack here, as the function does not push stuff. *) fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)]; Kclosure(lbl,0) :: cont @@ -506,6 +545,7 @@ let comp_args comp_expr reloc args sz cont = done; !c +(* Precondition: args not empty *) let comp_app comp_fun comp_arg reloc f args sz cont = let nargs = Array.length args in match is_tailcall cont with @@ -535,11 +575,12 @@ let compile_fv_elem reloc fv sz cont = let rec compile_fv reloc l sz cont = match l with | [] -> cont - | [fvn] -> compile_fv_elem reloc fvn sz cont + | [fvn] -> set_max_stack_size (sz + 1); compile_fv_elem reloc fvn sz cont | fvn :: tl -> compile_fv_elem reloc fvn sz (Kpush :: compile_fv reloc tl (sz + 1) cont) + (* Compiling constants *) let rec get_alias env kn = @@ -554,6 +595,7 @@ let rec get_alias env kn = (* sz is the size of the local stack *) let rec compile_constr reloc c sz cont = + set_max_stack_size sz; match kind_of_term c with | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta" | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar" @@ -602,6 +644,7 @@ let rec compile_constr reloc c sz cont = compile_str_cst reloc (Bstrconst (Const_sorts (Type uglob))) sz cont else let compile_get_univ reloc idx sz cont = + set_max_stack_size sz; compile_fv_elem reloc (FVuniv_var idx) sz cont in comp_app compile_str_cst compile_get_univ reloc @@ -621,7 +664,8 @@ let rec compile_constr reloc c sz cont = let r_fun = comp_env_fun arity in let lbl_fun = Label.create() in let cont_fun = - compile_constr r_fun body arity [Kreturn arity] in + ensure_stack_capacity (compile_constr r_fun body arity) [Kreturn arity] + in fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)]; let fv = fv r_fun in compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont) @@ -641,9 +685,10 @@ let rec compile_constr reloc c sz cont = (* Compilation des types *) let env_type = comp_env_fix_type rfv in for i = 0 to ndef - 1 do - let lbl,fcode = - label_code - (compile_constr env_type type_bodies.(i) 0 [Kstop]) in + let fcode = + ensure_stack_capacity (compile_constr env_type type_bodies.(i) 0) [Kstop] + in + let lbl,fcode = label_code fcode in lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; @@ -653,7 +698,8 @@ let rec compile_constr reloc c sz cont = let arity = List.length params in let env_body = comp_env_fix ndef i arity rfv in let cont1 = - compile_constr env_body body arity [Kreturn arity] in + ensure_stack_capacity (compile_constr env_body body arity) [Kreturn arity] + in let lbl = Label.create () in lbl_bodies.(i) <- lbl; let fcode = add_grabrec rec_args.(i) arity lbl cont1 in @@ -671,9 +717,10 @@ let rec compile_constr reloc c sz cont = let rfv = ref empty_fv in let env_type = comp_env_cofix_type ndef rfv in for i = 0 to ndef - 1 do - let lbl,fcode = - label_code - (compile_constr env_type type_bodies.(i) 0 [Kstop]) in + let fcode = + ensure_stack_capacity (compile_constr env_type type_bodies.(i) 0) [Kstop] + in + let lbl,fcode = label_code fcode in lbl_types.(i) <- lbl; fun_code := [Ksequence(fcode,!fun_code)] done; @@ -683,14 +730,17 @@ let rec compile_constr reloc c sz cont = let arity = List.length params in let env_body = comp_env_cofix ndef arity rfv in let lbl = Label.create () in - let cont1 = - compile_constr env_body body (arity+1) (cont_cofix arity) in - let cont2 = - add_grab (arity+1) lbl cont1 in + let comp arity = + (* 4 stack slots are needed to update the cofix when forced *) + set_max_stack_size (arity + 4); + compile_constr env_body body (arity+1) (cont_cofix arity) + in + let cont = ensure_stack_capacity comp arity in lbl_bodies.(i) <- lbl; - fun_code := [Ksequence(cont2,!fun_code)]; + fun_code := [Ksequence(add_grab (arity+1) lbl cont,!fun_code)]; done; let fv = !rfv in + set_max_stack_size (sz + fv.size + ndef + 2); compile_fv reloc fv.fv_rev sz (Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont) @@ -708,9 +758,11 @@ let rec compile_constr reloc c sz cont = let lbl_eblocks = Array.make neblock Label.no in let branch1,cont = make_branch cont in (* Compiling return type *) - let lbl_typ,fcode = - label_code (compile_constr reloc t sz [Kpop sz; Kstop]) - in fun_code := [Ksequence(fcode,!fun_code)]; + let fcode = + ensure_stack_capacity (compile_constr reloc t sz) [Kpop sz; Kstop] + in + let lbl_typ,fcode = label_code fcode in + fun_code := [Ksequence(fcode,!fun_code)]; (* Compiling branches *) let lbl_sw = Label.create () in let sz_b,branch,is_tailcall = @@ -720,14 +772,9 @@ let rec compile_constr reloc c sz cont = sz, branch1, true | _ -> sz+3, Kjump, false in - let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in - (* Compiling branch for accumulators *) - let lbl_accu, code_accu = - label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch::cont) - in - lbl_blocks.(0) <- lbl_accu; - let c = ref code_accu in - (* perform the extra match if needed (to many block constructors) *) + + let c = ref cont in + (* Perform the extra match if needed (too many block constructors) *) if neblock <> 0 then begin let lbl_b, code_b = label_code ( @@ -757,14 +804,34 @@ let rec compile_constr reloc c sz cont = compile_constr reloc branchs.(i) (sz_b+arity) (Kappterm(arity,sz_appterm) :: !c) in let code_b = - if tag < last_variant_tag then Kpushfields arity :: code_b - else Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b in + if tag < last_variant_tag then begin + set_max_stack_size (sz_b + arity); + Kpushfields arity :: code_b + end + else begin + set_max_stack_size (sz_b + arity + 1); + Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b + end + in let lbl_b,code_b = label_code code_b in if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b else lbl_eblocks.(tag - last_variant_tag) <- lbl_b; c := code_b done; - c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c; + + let annot = + {ci = ci; rtbl = tbl; tailcall = is_tailcall; + max_stack_size = !max_stack_size - sz} + in + + (* Compiling branch for accumulators *) + let lbl_accu, code_accu = + set_max_stack_size (sz+3); + label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch :: !c) + in + lbl_blocks.(0) <- lbl_accu; + + c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: code_accu; let code_sw = match branch1 with (* spiwack : branch1 can't be a lbl anymore it's a Branch instead @@ -781,12 +848,14 @@ let rec compile_constr reloc c sz cont = code_sw) and compile_str_cst reloc sc sz cont = + set_max_stack_size sz; match sc with | Bconstr c -> compile_constr reloc c sz cont | Bstrconst sc -> Kconst sc :: cont | Bmakeblock(tag,args) -> - let nargs = Array.length args in - comp_args compile_str_cst reloc args sz (code_makeblock nargs tag cont) + let arity = Array.length args in + let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in + comp_args compile_str_cst reloc args sz cont | Bconstruct_app(tag,nparams,arity,args) -> if Int.equal (Array.length args) 0 then code_construct tag nparams arity cont @@ -800,6 +869,7 @@ 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_get_global reloc (kn,u) sz cont = + set_max_stack_size sz; let kn = get_alias !global_env kn in if Univ.Instance.is_empty u then Kgetglobal kn :: cont @@ -808,11 +878,13 @@ and compile_get_global reloc (kn,u) sz cont = compile_universe reloc () (Univ.Instance.to_array u) sz cont and compile_universe reloc uni sz cont = + set_max_stack_size sz; 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 = + set_max_stack_size sz; 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 @@ -874,7 +946,7 @@ let compile fail_on_error ?universes:(universes=0) env c = let reloc, init_code = if Int.equal universes 0 then let reloc = empty_comp_env () in - reloc, compile_constr reloc c 0 cont + reloc, ensure_stack_capacity (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. @@ -891,18 +963,23 @@ let compile fail_on_error ?universes:(universes=0) env c = 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] + ensure_stack_capacity (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) + let init_code = + ensure_stack_capacity (compile_fv reloc fv.fv_rev 0) + (Kclosure(lbl_fun,fv.size) :: cont) + in + reloc, init_code in let fv = List.rev (!(reloc.in_env).fv_rev) in (if !Flags.dump_bytecode then Feedback.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 CErrors.errorlabstrm "compile" else + let fn = if fail_on_error then CErrors.user_err ?loc:None ~hdr:"compile" else (fun x -> Feedback.msg_warning x) in (Pp.(fn (str "Cannot compile code for virtual machine as it uses inductive " ++ diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index d779a81ff6..ad7a41a347 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -234,6 +234,7 @@ let emit_instr = function 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) + | Kensurestackcapacity size -> out opENSURESTACKCAPACITY; out_int size (* spiwack *) | Kbranch lbl -> out opBRANCH; out_label lbl | Kaddint31 -> out opADDINT31 diff --git a/kernel/constr.mli b/kernel/constr.mli index 42d298e3b9..7095dbe6f9 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -189,8 +189,12 @@ type ('constr, 'types) pcofixpoint = int * ('constr, 'types) prec_declaration type ('constr, 'types) kind_of_term = - | Rel of int - | Var of Id.t + | Rel of int (** Gallina-variable introduced by [forall], [fun], [let-in], [fix], or [cofix]. *) + + | Var of Id.t (** Gallina-variable that was introduced by Vernacular-command that extends + the local context of the currently open section + (i.e. [Variable] or [Let]). *) + | Meta of metavariable | Evar of 'constr pexistential | Sort of Sorts.t @@ -199,12 +203,16 @@ type ('constr, 'types) kind_of_term = | Lambda of Name.t * 'types * 'constr (** Concrete syntax ["fun A:B => C"] is represented as [Lambda (A,B,C)]. *) | LetIn of Name.t * 'constr * 'types * 'constr (** Concrete syntax ["let A:B := C in D"] is represented as [LetIn (A,B,C,D)]. *) | App of 'constr * 'constr array (** Concrete syntax ["(F P1 P2 ... Pn)"] is represented as [App (F, [|P1; P2; ...; Pn|])]. + The {!mkApp} constructor also enforces the following invariant: - [F] itself is not {!App} - and [[|P1;..;Pn|]] is not empty. *) - | Const of constant puniverses - | Ind of inductive puniverses - | Construct of constructor puniverses + + | Const of constant puniverses (** Gallina-variable that was introduced by Vernacular-command that extends the global environment + (i.e. [Parameter], or [Axiom], or [Definition], or [Theorem] etc.) *) + + | Ind of inductive puniverses (** A name of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) + | Construct of constructor puniverses (** A constructor of an inductive type defined by [Variant], [Inductive] or [Record] Vernacular-commands. *) | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint diff --git a/kernel/context.ml b/kernel/context.ml index 4e53b73a28..ae0388003d 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -138,7 +138,7 @@ struct | LocalDef (_,v,ty) -> f v; f ty (** Reduce all terms in a given declaration to a single value. *) - let fold f decl acc = + let fold_constr f decl acc = match decl with | LocalAssum (n,ty) -> f ty acc | LocalDef (n,v,ty) -> f ty (f v acc) @@ -147,9 +147,6 @@ struct | LocalAssum (na, ty) -> na, None, ty | LocalDef (na, v, ty) -> na, Some v, ty - let of_tuple = function - | n, None, ty -> LocalAssum (n,ty) - | n, Some v, ty -> LocalDef (n,v,ty) end (** Rel-context is represented as a list of declarations. @@ -336,7 +333,7 @@ struct | LocalDef (_, v, ty) -> f v; f ty (** Reduce all terms in a given declaration to a single value. *) - let fold f decl a = + let fold_constr f decl a = match decl with | LocalAssum (_, ty) -> f ty a | LocalDef (_, v, ty) -> a |> f v |> f ty @@ -348,6 +345,18 @@ struct let of_tuple = function | id, None, ty -> LocalAssum (id, ty) | id, Some v, ty -> LocalDef (id, v, ty) + + let of_rel_decl f = function + | Rel.Declaration.LocalAssum (na,t) -> + LocalAssum (f na, t) + | Rel.Declaration.LocalDef (na,v,t) -> + LocalDef (f na, v, t) + + let to_rel_decl = function + | LocalAssum (id,t) -> + Rel.Declaration.LocalAssum (Name id, t) + | LocalDef (id,v,t) -> + Rel.Declaration.LocalDef (Name id,v,t) end (** Named-context is represented as a list of declarations. @@ -401,23 +410,39 @@ struct | _ -> None in List.map_filter filter - end +end -module NamedList = +module Compacted = struct module Declaration = struct - type t = Id.t list * Constr.t option * Constr.t - - let map_constr f (ids, copt, ty as decl) = - let copt' = Option.map f copt in - let ty' = f ty in - if copt == copt' && ty == ty' then decl else (ids, copt', ty') + type t = + | LocalAssum of Id.t list * Constr.t + | LocalDef of Id.t list * Constr.t * Constr.t + + let map_constr f = function + | LocalAssum (ids, ty) as decl -> + let ty' = f ty in + if ty == ty' then decl else LocalAssum (ids, ty') + | LocalDef (ids, c, ty) as decl -> + let ty' = f ty in + let c' = f c in + if c == c' && ty == ty' then decl else LocalDef (ids,c',ty') + + let of_named_decl = function + | Named.Declaration.LocalAssum (id,t) -> + LocalAssum ([id],t) + | Named.Declaration.LocalDef (id,v,t) -> + LocalDef ([id],v,t) + + let to_named_context = function + | LocalAssum (ids, t) -> + List.map (fun id -> Named.Declaration.LocalAssum (id,t)) ids + | LocalDef (ids, v, t) -> + List.map (fun id -> Named.Declaration.LocalDef (id,v,t)) ids end type t = Declaration.t list let fold f l ~init = List.fold_right f l init end - -type section_context = Named.t diff --git a/kernel/context.mli b/kernel/context.mli index b5f3904d22..955e214cb9 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -79,10 +79,9 @@ sig val iter_constr : (Constr.t -> unit) -> t -> unit (** Reduce all terms in a given declaration to a single value. *) - val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + val fold_constr : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a val to_tuple : t -> Name.t * Constr.t option * Constr.t - val of_tuple : Name.t * Constr.t option * Constr.t -> t end (** Rel-context is represented as a list of declarations. @@ -193,10 +192,18 @@ sig val iter_constr : (Constr.t -> unit) -> t -> unit (** Reduce all terms in a given declaration to a single value. *) - val fold : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a + val fold_constr : (Constr.t -> 'a -> 'a) -> t -> 'a -> 'a val to_tuple : t -> Id.t * Constr.t option * Constr.t val of_tuple : Id.t * Constr.t option * Constr.t -> t + + (** Convert [Rel.Declaration.t] value to the corresponding [Named.Declaration.t] value. + The function provided as the first parameter determines how to translate "names" to "ids". *) + val of_rel_decl : (Name.t -> Id.t) -> Rel.Declaration.t -> t + + (** Convert [Named.Declaration.t] value to the corresponding [Rel.Declaration.t] value. *) + (* TODO: Move this function to [Rel.Declaration] module and rename it to [of_named]. *) + val to_rel_decl : t -> Rel.Declaration.t end (** Rel-context is represented as a list of declarations. @@ -244,17 +251,20 @@ sig val to_instance : t -> Constr.t list end -module NamedList : +module Compacted : sig module Declaration : sig - type t = Id.t list * Constr.t option * Constr.t + type t = + | LocalAssum of Id.t list * Constr.t + | LocalDef of Id.t list * Constr.t * Constr.t + val map_constr : (Constr.t -> Constr.t) -> t -> t + val of_named_decl : Named.Declaration.t -> t + val to_named_context : t -> Named.t end type t = Declaration.t list val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a end - -type section_context = Named.t diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 1345991503..f5059cd750 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -21,6 +21,8 @@ open Declarations open Environ open Univ +module NamedDecl = Context.Named.Declaration + (*s Cooking the constants. *) let pop_dirpath p = match DirPath.repr p with @@ -152,7 +154,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * bool * constant_universes * inline - * Context.section_context option + * Context.Named.t option let on_body ml hy f = function | Undef _ as x -> x @@ -202,8 +204,7 @@ let cook_constant env { from = cb; info } = in let const_hyps = Context.Named.fold_outside (fun decl hyps -> - let open Context.Named.Declaration in - List.filter (fun decl' -> not (Id.equal (get_id decl) (get_id decl'))) + List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl'))) hyps) hyps ~init:cb.const_hyps in let typ = match cb.const_type with diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 327e697d23..eb40730969 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -19,7 +19,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * bool * constant_universes * inline - * Context.section_context option + * Context.Named.t option val cook_constant : env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index e195618b6b..40595f944c 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -22,6 +22,8 @@ open Declarations open Pre_env open Cbytegen +module NamedDecl = Context.Named.Declaration +module RelDecl = Context.Rel.Declaration external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code" external eval_tcode : tcode -> values array -> values = "coq_eval_tcode" @@ -189,18 +191,14 @@ and slot_for_fv env fv = let nv = Pre_env.lookup_named_val id env in begin match force_lazy_val nv with | None -> - let open Context.Named in - let open Declaration in - env.env_named_context |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun + env |> Pre_env.lookup_named id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun | Some (v, _) -> v end | FVrel i -> let rv = Pre_env.lookup_rel_val i env in begin match force_lazy_val rv with | None -> - let open Context.Rel in - let open Declaration in - env.env_rel_context |> lookup i |> get_value |> fill_fv_cache rv i val_of_rel env_of_rel + env.env_rel_context |> Context.Rel.lookup i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end | FVuniv_var idu -> diff --git a/kernel/declarations.mli b/kernel/declarations.mli index f89773fcc5..7821ea20ff 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -58,10 +58,11 @@ type projection_body = { proj_body : constr; (* For compatibility with VMs only, the match version *) } +(* Global declarations (i.e. constants) can be either: *) type constant_def = - | Undef of inline - | Def of constr Mod_subst.substituted - | OpaqueDef of Opaqueproof.opaque + | Undef of inline (** a global assumption *) + | Def of constr Mod_subst.substituted (** or a transparent global definition *) + | OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *) type constant_universes = Univ.universe_context @@ -78,7 +79,7 @@ type typing_flags = { (* some contraints are in constant_constraints, some other may be in * the OpaueDef *) type constant_body = { - const_hyps : Context.section_context; (** New: younger hyp at top *) + const_hyps : Context.Named.t; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted option; @@ -177,7 +178,7 @@ type mutual_inductive_body = { mind_ntypes : int; (** Number of types in the block *) - mind_hyps : Context.section_context; (** Section hypotheses on which the block depends *) + mind_hyps : Context.Named.t; (** Section hypotheses on which the block depends *) mind_nparams : int; (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 211e5e062a..0a822d6fad 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -9,7 +9,8 @@ open Declarations open Mod_subst open Util -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (** Operations concernings types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) @@ -94,7 +95,7 @@ let is_opaque cb = match cb.const_body with (** {7 Constant substitutions } *) let subst_rel_declaration sub = - map_constr (subst_mps sub) + RelDecl.map_constr (subst_mps sub) let subst_rel_context sub = List.smartmap (subst_rel_declaration sub) @@ -146,7 +147,7 @@ let subst_const_body sub cb = themselves. But would it really bring substantial gains ? *) let hcons_rel_decl = - map_type Term.hcons_types % map_value Term.hcons_constr % map_name Names.Name.hcons + RelDecl.map_name Names.Name.hcons %> RelDecl.map_value Term.hcons_constr %> RelDecl.map_type Term.hcons_types let hcons_rel_context l = List.smartmap hcons_rel_decl l diff --git a/kernel/entries.mli b/kernel/entries.mli index df2c4653f7..77081947ec 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -61,7 +61,7 @@ type 'a const_entry_body = 'a proof_output Future.computation type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) - const_entry_secctx : Context.section_context option; + const_entry_secctx : Context.Named.t option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; @@ -73,7 +73,7 @@ type 'a definition_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Context.section_context option * bool * types Univ.in_universe_context * inline + Context.Named.t option * bool * types Univ.in_universe_context * inline type projection_entry = { proj_entry_ind : mutual_inductive; @@ -98,7 +98,12 @@ type module_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 seff_env = + [ `Nothing + (* The proof term and its universes. + Same as the constant_body's but not in an ephemeron *) + | `Opaque of Constr.t * Univ.universe_context_set ] type side_eff = | SEsubproof of constant * Declarations.constant_body * seff_env diff --git a/kernel/environ.ml b/kernel/environ.ml index 7351a87d44..4a543f1957 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -56,14 +56,14 @@ let type_in_type env = not (typing_flags env).check_universes let deactivated_guard env = not (typing_flags env).check_guarded let universes env = env.env_stratification.env_universes -let named_context env = env.env_named_context -let named_context_val env = env.env_named_context,env.env_named_vals +let named_context env = env.env_named_context.env_named_ctx +let named_context_val env = env.env_named_context let rel_context env = env.env_rel_context let opaque_tables env = env.indirect_pterms let set_opaque_tables env indirect_pterms = { env with indirect_pterms } let empty_context env = - match env.env_rel_context, env.env_named_context with + match env.env_rel_context, env.env_named_context.env_named_ctx with | [], [] -> true | _ -> false @@ -99,14 +99,12 @@ let fold_rel_context f env ~init = (* Named context *) -let named_context_of_val = fst -let named_vals_of_val = snd +let named_context_of_val c = c.env_named_ctx (* [map_named_val f ctxt] apply [f] to the body and the type of each declarations. *** /!\ *** [f t] should be convertible with t *) -let map_named_val f = - on_fst (Context.Named.map f) +let map_named_val = map_named_val let empty_named_context = Context.Named.empty @@ -118,8 +116,8 @@ let val_of_named_context ctxt = List.fold_right push_named_context_val ctxt empty_named_context_val -let lookup_named id env = Context.Named.lookup id env.env_named_context -let lookup_named_val id (ctxt,_) = Context.Named.lookup id ctxt +let lookup_named = lookup_named +let lookup_named_val id ctxt = fst (Id.Map.find id ctxt.env_named_map) let eq_named_context_val c1 c2 = c1 == c2 || Context.Named.equal (named_context_of_val c1) (named_context_of_val c2) @@ -139,10 +137,9 @@ let evaluable_named id env = | Some _ -> true | _ -> false -let reset_with_named_context (ctxt,ctxtv) env = +let reset_with_named_context ctxt env = { env with env_named_context = ctxt; - env_named_vals = ctxtv; env_rel_context = Context.Rel.empty; env_rel_val = []; env_nb_rel = 0 } @@ -157,11 +154,11 @@ let pop_rel_context n env = let fold_named_context f env ~init = let rec fold_right env = - match env.env_named_context with - | [] -> init - | d::ctxt -> + match match_named_context_val env.env_named_context with + | None -> init + | Some (d, v, rem) -> let env = - reset_with_named_context (ctxt,List.tl env.env_named_vals) env in + reset_with_named_context rem env in f env d (fold_right env) in fold_right env @@ -416,7 +413,7 @@ let global_vars_set env constr = Id.Set.union (vars_of_global env c) acc | _ -> acc in - fold_constr filtrec acc c + Term.fold_constr filtrec acc c in filtrec Id.Set.empty constr @@ -493,66 +490,35 @@ let compile_constant_body = Cbytegen.compile_constant_body false exception Hyp_not_found -let apply_to_hyp (ctxt,vals) id f = - let rec aux rtail ctxt vals = - match ctxt, vals with - | d::ctxt, v::vals -> - if Id.equal (get_id d) id then - (f ctxt d rtail)::ctxt, v::vals - else - let ctxt',vals' = aux (d::rtail) ctxt vals in - d::ctxt', v::vals' - | [],[] -> raise Hyp_not_found - | _, _ -> assert false - in aux [] ctxt vals - -let apply_to_hyp_and_dependent_on (ctxt,vals) id f g = - let rec aux ctxt vals = - match ctxt,vals with - | d::ctxt, v::vals -> +let apply_to_hyp ctxt id f = + let rec aux rtail ctxt = + match match_named_context_val ctxt with + | Some (d, v, ctxt) -> if Id.equal (get_id d) id then - let sign = ctxt,vals in - push_named_context_val (f d sign) sign + push_named_context_val_val (f ctxt.env_named_ctx d rtail) v ctxt else - let (ctxt,vals as sign) = aux ctxt vals in - push_named_context_val (g d sign) sign - | [],[] -> raise Hyp_not_found - | _,_ -> assert false - in aux ctxt vals - -let insert_after_hyp (ctxt,vals) id d check = - let rec aux ctxt vals = - match ctxt, vals with - | decl::ctxt', v::vals' -> - if Id.equal (get_id decl) id then begin - check ctxt; - push_named_context_val d (ctxt,vals) - end else - let ctxt,vals = aux ctxt vals in - d::ctxt, v::vals - | [],[] -> raise Hyp_not_found - | _, _ -> assert false - in aux ctxt vals - + let ctxt' = aux (d::rtail) ctxt in + push_named_context_val_val d v ctxt' + | None -> raise Hyp_not_found + in aux [] ctxt (* To be used in Logic.clear_hyps *) -let remove_hyps ids check_context check_value (ctxt, vals) = - let rec remove_hyps ctxt vals = match ctxt, vals with - | [], [] -> ([], []), false - | d :: rctxt, (nid, v) :: rvals -> - let (ans, seen) = remove_hyps rctxt rvals in +let remove_hyps ids check_context check_value ctxt = + let rec remove_hyps ctxt = match match_named_context_val ctxt with + | None -> empty_named_context_val, false + | Some (d, v, rctxt) -> + let (ans, seen) = remove_hyps rctxt in if Id.Set.mem (get_id d) ids then (ans, true) - else if not seen then (ctxt, vals), false + else if not seen then ctxt, false else - let (rctxt', rvals') = ans in + let rctxt' = ans in let d' = check_context d in let v' = check_value v in - if d == d' && v == v' && rctxt == rctxt' && rvals == rvals' then - (ctxt, vals), true - else (d' :: rctxt', (nid, v') :: rvals'), true - | _ -> assert false + if d == d' && v == v' && rctxt == rctxt' then + ctxt, true + else push_named_context_val_val d' v' rctxt', true in - fst (remove_hyps ctxt vals) + fst (remove_hyps ctxt) (*spiwack: the following functions assemble the pieces of the retroknowledge note that the "consistent" register function is available in the module diff --git a/kernel/environ.mli b/kernel/environ.mli index b5e5764354..ea570cb4a8 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -78,7 +78,6 @@ val fold_rel_context : (** {5 Context of variables (section variables and goal assumptions) } *) val named_context_of_val : named_context_val -> Context.Named.t -val named_vals_of_val : named_context_val -> Pre_env.named_vals val val_of_named_context : Context.Named.t -> named_context_val val empty_named_context_val : named_context_val @@ -232,7 +231,7 @@ val vars_of_global : env -> constr -> Id.Set.t val really_needed : env -> Id.Set.t -> Id.Set.t (** like [really_needed] but computes a well ordered named context *) -val keep_hyps : env -> Id.Set.t -> Context.section_context +val keep_hyps : env -> Id.Set.t -> Context.Named.t (** {5 Unsafe judgments. } We introduce here the pre-type of judgments, which is @@ -265,18 +264,6 @@ val apply_to_hyp : named_context_val -> variable -> (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) -> named_context_val -(** [apply_to_hyp_and_dependent_on sign id f g] split [sign] into - [tail::(id,_,_)::head] and - return [(g tail)::(f (id,_,_))::head]. *) -val apply_to_hyp_and_dependent_on : named_context_val -> variable -> - (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) -> - (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) -> - named_context_val - -val insert_after_hyp : named_context_val -> variable -> - Context.Named.Declaration.t -> - (Context.Named.t -> unit) -> named_context_val - val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml deleted file mode 100644 index bd91c689d2..0000000000 --- a/kernel/fast_typeops.ml +++ /dev/null @@ -1,463 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open CErrors -open Util -open Names -open Univ -open Term -open Vars -open Declarations -open Environ -open Reduction -open Inductive -open Type_errors - -let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y - -let conv_leq_vecti env v1 v2 = - Array.fold_left2_i - (fun i _ t1 t2 -> - try conv_leq false env t1 t2 - with NotConvertible -> raise (NotConvertibleVect i)) - () - v1 - v2 - -let check_constraints cst env = - if Environ.check_constraints cst env then () - else error_unsatisfied_constraints env cst - -(* This should be a type (a priori without intention to be an assumption) *) -let type_judgment env c t = - match kind_of_term(whd_all env t) with - | Sort s -> {utj_val = c; utj_type = s } - | _ -> error_not_type env (make_judge c t) - -let check_type env c t = - match kind_of_term(whd_all env t) with - | Sort s -> s - | _ -> error_not_type env (make_judge c t) - -(* This should be a type intended to be assumed. The error message is *) -(* not as useful as for [type_judgment]. *) -let assumption_of_judgment env t ty = - try let _ = check_type env t ty in t - with TypeError _ -> - error_assumption env (make_judge t ty) - -(************************************************) -(* Incremental typing rules: builds a typing judgment given the *) -(* judgments for the subterms. *) - -(*s Type of sorts *) - -(* Prop and Set *) - -let judge_of_prop = mkSort type1_sort - -let judge_of_prop_contents _ = judge_of_prop - -(* Type of Type(i). *) - -let judge_of_type u = - let uu = Universe.super u in - mkType uu - -(*s Type of a de Bruijn index. *) - -let judge_of_relative env n = - try - let open Context.Rel.Declaration in - env |> lookup_rel n |> get_type |> lift n - with Not_found -> - error_unbound_rel env n - -(* Type of variables *) -let judge_of_variable env id = - try named_type id env - with Not_found -> - error_unbound_var env id - -(* Management of context of variables. *) - -(* Checks if a context of variables can be instantiated by the - variables of the current env *) -(* TODO: check order? *) -let check_hyps_inclusion env f c sign = - Context.Named.fold_outside - (fun decl () -> - let open Context.Named.Declaration in - let id = get_id decl in - let ty1 = get_type decl in - try - let ty2 = named_type id env in - if not (eq_constr ty2 ty1) then raise Exit - with Not_found | Exit -> - error_reference_variables env id (f c)) - sign - ~init:() - -(* Instantiation of terms on real arguments. *) - -(* Make a type polymorphic if an arity *) - -(* Type of constants *) - - -let type_of_constant_knowing_parameters_arity env t paramtyps = - match t with - | RegularArity t -> t - | TemplateArity (sign,ar) -> - let ctx = List.rev sign in - let ctx,s = instantiate_universes env ctx ar paramtyps in - mkArity (List.rev ctx,s) - -let type_of_constant_knowing_parameters env cst paramtyps = - let ty, cu = constant_type env cst in - type_of_constant_knowing_parameters_arity env ty paramtyps, cu - -let judge_of_constant_knowing_parameters env (kn,u as cst) args = - let cb = lookup_constant kn env in - let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in - let ty, cu = type_of_constant_knowing_parameters env cst args in - let () = check_constraints cu env in - ty - -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] - -(* Type of a lambda-abstraction. *) - -(* [judge_of_abstraction env name var j] implements the rule - - env, name:typ |- j.uj_val:j.uj_type env, |- (name:typ)j.uj_type : s - ----------------------------------------------------------------------- - env |- [name:typ]j.uj_val : (name:typ)j.uj_type - - Since all products are defined in the Calculus of Inductive Constructions - and no upper constraint exists on the sort $s$, we don't need to compute $s$ -*) - -let judge_of_abstraction env name var ty = - mkProd (name, var, ty) - -(* Type of an application. *) - -let make_judgev c t = - Array.map2 make_judge c t - -let judge_of_apply env func funt argsv argstv = - let len = Array.length argsv in - let rec apply_rec i typ = - if Int.equal i len then typ - else - (match kind_of_term (whd_all env typ) with - | Prod (_,c1,c2) -> - let arg = argsv.(i) and argt = argstv.(i) in - (try - let () = conv_leq false env argt c1 in - apply_rec (i+1) (subst1 arg c2) - with NotConvertible -> - error_cant_apply_bad_type env - (i+1,c1,argt) - (make_judge func funt) - (make_judgev argsv argstv)) - - | _ -> - error_cant_apply_not_functional env - (make_judge func funt) - (make_judgev argsv argstv)) - in apply_rec 0 funt - -(* Type of product *) - -let sort_of_product env domsort rangsort = - match (domsort, rangsort) with - (* Product rule (s,Prop,Prop) *) - | (_, Prop Null) -> rangsort - (* Product rule (Prop/Set,Set,Set) *) - | (Prop _, Prop Pos) -> rangsort - (* Product rule (Type,Set,?) *) - | (Type u1, Prop Pos) -> - 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) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Pos, Type u2) -> Type (Universe.sup Universe.type0 u2) - (* Product rule (Prop,Type_i,Type_i) *) - | (Prop Null, Type _) -> rangsort - (* Product rule (Type_i,Type_i,Type_i) *) - | (Type u1, Type u2) -> Type (Universe.sup u1 u2) - -(* [judge_of_product env name (typ1,s1) (typ2,s2)] implements the rule - - env |- typ1:s1 env, name:typ1 |- typ2 : s2 - ------------------------------------------------------------------------- - s' >= (s1,s2), env |- (name:typ)j.uj_val : s' - - where j.uj_type is convertible to a sort s2 -*) -let judge_of_product env name s1 s2 = - let s = sort_of_product env s1 s2 in - mkSort s - -(* Type of a type cast *) - -(* [judge_of_cast env (c,typ1) (typ2,s)] implements the rule - - env |- c:typ1 env |- typ2:s env |- typ1 <= typ2 - --------------------------------------------------------------------- - env |- c:typ2 -*) - -let judge_of_cast env c ct k expected_type = - try - match k with - | VMcast -> - vm_conv CUMUL env ct expected_type - | DEFAULTcast -> - default_conv ~l2r:false CUMUL env ct expected_type - | REVERTcast -> - default_conv ~l2r:true CUMUL env ct expected_type - | NATIVEcast -> - let sigma = Nativelambda.empty_evars in - Nativeconv.native_conv CUMUL sigma env ct expected_type - with NotConvertible -> - error_actual_type env (make_judge c ct) expected_type - -(* Inductive types. *) - -(* The type is parametric over the uniform parameters whose conclusion - is in Type; to enforce the internal constraints between the - parameters and the instances of Type occurring in the type of the - constructors, we use the level variables _statically_ assigned to - the conclusions of the parameters as mediators: e.g. if a parameter - has conclusion Type(alpha), static constraints of the form alpha<=v - exist between alpha and the Type's occurring in the constructor - types; when the parameters is finally instantiated by a term of - conclusion Type(u), then the constraints u<=alpha is computed in - the App case of execute; from this constraints, the expected - dynamic constraints of the form u<=v are enforced *) - -let judge_of_inductive_knowing_parameters env (ind,u as indu) args = - let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters - env (spec,u) args - in - check_constraints cst env; - t - -let judge_of_inductive env (ind,u as indu) = - let (mib,mip) = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in - check_constraints cst env; - t - -(* Constructors. *) - -let judge_of_constructor env (c,u as cu) = - let _ = - let ((kn,_),_) = c in - let mib = lookup_mind kn env in - check_hyps_inclusion env mkConstructU cu mib.mind_hyps in - let specif = lookup_mind_specif env (inductive_of_constructor c) in - let t,cst = constrained_type_of_constructor cu specif in - let () = check_constraints cst env in - t - -(* Case. *) - -let check_branch_types env (ind,u) c ct lft explft = - try conv_leq_vecti env lft explft - with - NotConvertibleVect i -> - error_ill_formed_branch env c ((ind,i+1),u) lft.(i) explft.(i) - | Invalid_argument _ -> - error_number_branches env (make_judge c ct) (Array.length explft) - -let judge_of_case env ci p pt c ct lf lft = - let (pind, _ as indspec) = - try find_rectype env ct - with Not_found -> error_case_not_inductive env (make_judge c ct) in - let _ = check_case_info env pind ci in - let (bty,rslty) = - type_case_branches env indspec (make_judge p pt) c in - let () = check_branch_types env pind c ct lft bty in - rslty - -let judge_of_projection env p c ct = - let pb = lookup_projection p env in - let (ind,u), args = - try find_rectype env ct - with Not_found -> error_case_not_inductive env (make_judge c ct) - in - assert(eq_mind pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - substl (c :: List.rev args) ty - - -(* Fixpoints. *) - -(* Checks the type of a general (co)fixpoint, i.e. without checking *) -(* the specific guard condition. *) - -let type_fixpoint env lna lar vdef vdeft = - let lt = Array.length vdeft in - assert (Int.equal (Array.length lar) lt); - try - conv_leq_vecti env vdeft (Array.map (fun ty -> lift lt ty) lar) - with NotConvertibleVect i -> - error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar - -(************************************************************************) -(************************************************************************) - -(* The typing machine. *) - (* ATTENTION : faudra faire le typage du contexte des Const, - Ind et Constructsi un jour cela devient des constructions - arbitraires et non plus des variables *) -let rec execute env cstr = - let open Context.Rel.Declaration in - match kind_of_term cstr with - (* Atomic terms *) - | Sort (Prop c) -> - judge_of_prop_contents c - - | Sort (Type u) -> - judge_of_type u - - | Rel n -> - judge_of_relative env n - - | Var id -> - judge_of_variable env id - - | Const c -> - judge_of_constant env c - - | Proj (p, c) -> - let ct = execute env c in - judge_of_projection env p c ct - - (* Lambda calculus operators *) - | App (f,args) -> - let argst = execute_array env args in - let ft = - match kind_of_term f with - | Ind ind when Environ.template_polymorphic_pind ind env -> - (* Template sort-polymorphism of inductive types *) - let args = Array.map (fun t -> lazy t) argst in - judge_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_pconstant cst env -> - (* Template sort-polymorphism of constants *) - let args = Array.map (fun t -> lazy t) argst in - judge_of_constant_knowing_parameters env cst args - | _ -> - (* Full or no sort-polymorphism *) - execute env f - in - - judge_of_apply env f ft args argst - - | Lambda (name,c1,c2) -> - let _ = execute_is_type env c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let c2t = execute env1 c2 in - judge_of_abstraction env name c1 c2t - - | Prod (name,c1,c2) -> - let vars = execute_is_type env c1 in - let env1 = push_rel (LocalAssum (name,c1)) env in - let vars' = execute_is_type env1 c2 in - judge_of_product env name vars vars' - - | LetIn (name,c1,c2,c3) -> - let c1t = execute env c1 in - let _c2s = execute_is_type env c2 in - let _ = judge_of_cast env c1 c1t DEFAULTcast c2 in - let env1 = push_rel (LocalDef (name,c1,c2)) env in - let c3t = execute env1 c3 in - subst1 c1 c3t - - | Cast (c,k,t) -> - let ct = execute env c in - let _ts = execute_type env t in - let _ = judge_of_cast env c ct k t in - t - - (* Inductive types *) - | Ind ind -> - judge_of_inductive env ind - - | Construct c -> - judge_of_constructor env c - - | Case (ci,p,c,lf) -> - let ct = execute env c in - let pt = execute env p in - let lft = execute_array env lf in - judge_of_case env ci p pt c ct lf lft - - | Fix ((vn,i as vni),recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in - let fix = (vni,recdef') in - check_fix env fix; fix_ty - - | CoFix (i,recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in - let cofix = (i,recdef') in - check_cofix env cofix; fix_ty - - (* Partial proofs: unsupported by the kernel *) - | Meta _ -> - anomaly (Pp.str "the kernel does not support metavariables") - - | Evar _ -> - anomaly (Pp.str "the kernel does not support existential variables") - -and execute_is_type env constr = - let t = execute env constr in - check_type env constr t - -and execute_type env constr = - let t = execute env constr in - type_judgment env constr t - -and execute_recdef env (names,lar,vdef) i = - let lart = execute_array env lar in - let lara = Array.map2 (assumption_of_judgment env) lar lart in - let env1 = push_rec_types (names,lara,vdef) env in - let vdeft = execute_array env1 vdef in - let () = type_fixpoint env1 names lara vdef vdeft in - (lara.(i),(names,lara,vdef)) - -and execute_array env = Array.map (execute env) - -(* Derived functions *) -let infer env constr = - let t = execute env constr in - make_judge constr t - -let infer = - if Flags.profile then - let infer_key = Profile.declare_profile "Fast_infer" in - Profile.profile2 infer_key (fun b c -> infer b c) - else (fun b c -> infer b c) - -let infer_type env constr = - execute_type env constr - -let infer_v env cv = - let jv = execute_array env cv in - make_judgev cv jv diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli deleted file mode 100644 index 41cff607e7..0000000000 --- a/kernel/fast_typeops.mli +++ /dev/null @@ -1,24 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Term -open Environ -open Declarations - -(** {6 Typing functions (not yet tagged as safe) } - - They return unsafe judgments that are "in context" of a set of - (local) universe variables (the ones that appear in the term) - and associated constraints. In case of polymorphic definitions, - these variables and constraints will be generalized. - *) - - -val infer : env -> constr -> unsafe_judgment -val infer_v : env -> constr array -> unsafe_judgment array -val infer_type : env -> types -> unsafe_type_judgment diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 15f213ce9c..4c540a6d73 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -32,7 +32,6 @@ Type_errors Modops Inductive Typeops -Fast_typeops Indtypes Cooking Term_typing diff --git a/kernel/make-opcodes b/kernel/make-opcodes index c8f573c682..e1371b3d0c 100644 --- a/kernel/make-opcodes +++ b/kernel/make-opcodes @@ -1,2 +1,3 @@ $1=="enum" {n=0; next; } - {for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}} + {printf("(* THIS FILE IS GENERATED. DON'T EDIT. *)\n\n"); + for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}} diff --git a/kernel/names.ml b/kernel/names.ml index 9267a64d61..1f138581cc 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -34,9 +34,15 @@ struct let hash = String.hash + let warn_invalid_identifier = + CWarnings.create ~name:"invalid-identifier" ~category:"parsing" + ~default:CWarnings.Disabled + (fun s -> str s) + let check_soft ?(warn = true) x = let iter (fatal, x) = - if fatal then CErrors.error x else if warn then Feedback.msg_warning (str x) + if fatal then CErrors.error x else + if warn then warn_invalid_identifier x in Option.iter iter (Unicode.ident_refutation x) @@ -82,11 +88,14 @@ struct type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + let mk_name id = + Name id + let is_anonymous = function | Anonymous -> true | Name _ -> false - let is_name = not % is_anonymous + let is_name = is_anonymous %> not let compare n1 n2 = match n1, n2 with | Anonymous, Anonymous -> 0 @@ -595,7 +604,13 @@ end module Constant = KerPair module Cmap = HMap.Make(Constant.CanOrd) +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "cannonical form" of the constant. *) + module Cmap_env = HMap.Make(Constant.UserOrd) +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "user form" of the constant. *) + module Cpred = Predicate.Make(Constant.CanOrd) module Cset = Cmap.Set module Cset_env = Cmap_env.Set diff --git a/kernel/names.mli b/kernel/names.mli index feaedc775c..6b0a80625b 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -82,6 +82,9 @@ sig type t = Anonymous (** anonymous identifier *) | Name of Id.t (** non-anonymous identifier *) + val mk_name : Id.t -> t + (** constructor *) + val is_anonymous : t -> bool (** Return [true] iff a given name is [Anonymous]. *) @@ -368,8 +371,14 @@ end module Cpred : Predicate.S with type elt = Constant.t module Cset : CSig.SetS with type elt = Constant.t module Cset_env : CSig.SetS with type elt = Constant.t + module Cmap : Map.ExtS with type key = Constant.t and module Set := Cset +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "cannonical form" of the constant. *) + module Cmap_env : Map.ExtS with type key = Constant.t and module Set := Cset_env +(** A map whose keys are constants (values of the {!Constant.t} type). + Keys are ordered wrt. "user form" of the constant. *) (** {6 Inductive names} *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 87302dcf5a..33bd7d8ddc 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -22,8 +22,12 @@ to OCaml code. *) (** Local names **) +(* The first component is there for debugging purposes only *) type lname = { lname : name; luid : int } +let eq_lname ln1 ln2 = + Int.equal ln1.luid ln2.luid + let dummy_lname = { lname = Anonymous; luid = -1 } module LNord = @@ -82,6 +86,9 @@ let eq_gname gn1 gn2 = | Gnamed id1, Gnamed id2 -> Id.equal id1 id2 | _ -> false +let dummy_gname = + Grel 0 + open Hashset.Combine let gname_hash gn = match gn with @@ -404,9 +411,13 @@ let opush_lnames n env lns = let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 = match t1, t2 with | MLlocal ln1, MLlocal ln2 -> + (try Int.equal (LNmap.find ln1 env1) (LNmap.find ln2 env2) + with Not_found -> + eq_lname ln1 ln2) | MLglobal gn1', MLglobal gn2' -> eq_gname gn1' gn2' || (eq_gname gn1 gn1' && eq_gname gn2 gn2') + || (eq_gname gn1 gn2' && eq_gname gn2 gn1') | MLprimitive prim1, MLprimitive prim2 -> eq_primitive prim1 prim2 | MLlam (lns1, ml1), MLlam (lns2, ml2) -> Int.equal (Array.length lns1) (Array.length lns2) && @@ -719,6 +730,11 @@ let push_global_norm gn params body = let push_global_case gn params annot a accu bs = push_global gn (Gletcase (gn, params, annot, a, accu, bs)) +(* Compares [t1] and [t2] up to alpha-equivalence. [t1] and [t2] may contain + free variables. *) +let eq_mllambda t1 t2 = + eq_mllambda dummy_gname dummy_gname 0 LNmap.empty LNmap.empty t1 t2 + (*s Compilation environment *) type env = @@ -897,9 +913,7 @@ let rec insert cargs body rl = let params = rm_params fv params in rl:= Rcons(ref [(c,params)], fv, body, ref Rnil) | Rcons(l,fv,body',rl) -> - (** ppedrot: It seems we only want to factorize common branches. It should - not matter to do so with a subapproximation by (==). *) - if body == body' then + if eq_mllambda body body' then let (c,params) = cargs in let params = rm_params fv params in l := (c,params)::!l @@ -1446,12 +1460,14 @@ let optimize gdef l = end | MLif(t,b1,b2) -> + (* This optimization is critical: it applies to all fixpoints that start + by matching on their recursive argument *) let t = optimize s t in let b1 = optimize s b1 in let b2 = optimize s b2 in begin match t, b2 with | MLapp(MLprimitive Is_accu,[| l1 |]), MLmatch(annot, l2, _, bs) - when l1 == l2 -> MLmatch(annot, l1, b1, bs) (** approximation *) + when eq_mllambda l1 l2 -> MLmatch(annot, l1, b1, bs) | _, _ -> MLif(t, b1, b2) end | MLmatch(annot,a,accu,bs) -> @@ -1832,10 +1848,9 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml = auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named))) and compile_rel env sigma univ auxdefs n = - let open Context.Rel in - let n = length env.env_rel_context - n in - let open Declaration in - match lookup n env.env_rel_context with + let n = Context.Rel.length env.env_rel_context - n in + let open Context.Rel.Declaration in + match Context.Rel.lookup n env.env_rel_context with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in @@ -1845,7 +1860,7 @@ and compile_rel env sigma univ auxdefs n = and compile_named env sigma univ auxdefs id = let open Context.Named.Declaration in - match Context.Named.lookup id env.env_named_context with + match lookup_named id env with | LocalDef (_,t,_) -> let code = lambda_of_constr env sigma t in let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 91b40be7e9..366f9a0a6d 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -14,6 +14,8 @@ open Pre_env open Nativevalues open Nativeinstr +module RelDecl = Context.Rel.Declaration + (** This file defines the lambda code generation phase of the native compiler *) exception NotClosed @@ -727,8 +729,7 @@ let optimize lam = let lambda_of_constr env sigma c = set_global_env env; let env = Renv.make () in - let open Context.Rel.Declaration in - let ids = List.rev_map get_name !global_env.env_rel_context in + let ids = List.rev_map RelDecl.get_name !global_env.env_rel_context in Renv.push_rels env (Array.of_list ids); let lam = lambda_of_constr env sigma c in (* if Flags.vm_draw_opt () then begin diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 1c58c7445c..6bd82170e6 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -35,7 +35,7 @@ let ( / ) = Filename.concat (* We have to delay evaluation of include_dirs because coqlib cannot be guessed until flags have been properly initialized *) let include_dirs () = - [Filename.temp_dir_name; coqlib () / "kernel"; coqlib () / "library"] + [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"] (* Pointer to the function linking an ML object into coq's toplevel *) let load_obj = ref (fun x -> () : string -> unit) diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 5afefeebde..d14a254d32 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -17,7 +17,8 @@ open Util open Names open Term open Declarations -open Context.Named.Declaration + +module NamedDecl = Context.Named.Declaration (* The type of environments. *) @@ -61,12 +62,14 @@ let force_lazy_val vk = match !vk with let dummy_lazy_val () = ref VKnone let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) -type named_vals = (Id.t * lazy_val) list +type named_context_val = { + env_named_ctx : Context.Named.t; + env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; +} type env = { env_globals : globals; - env_named_context : Context.Named.t; - env_named_vals : named_vals; + env_named_context : named_context_val; env_rel_context : Context.Rel.t; env_rel_val : lazy_val list; env_nb_rel : int; @@ -77,9 +80,10 @@ type env = { indirect_pterms : Opaqueproof.opaquetab; } -type named_context_val = Context.Named.t * named_vals - -let empty_named_context_val = [],[] +let empty_named_context_val = { + env_named_ctx = []; + env_named_map = Id.Map.empty; +} let empty_env = { env_globals = { @@ -87,8 +91,7 @@ let empty_env = { env_inductives = Mindmap_env.empty; env_modules = MPmap.empty; env_modtypes = MPmap.empty}; - env_named_context = Context.Named.empty; - env_named_vals = []; + env_named_context = empty_named_context_val; env_rel_context = Context.Rel.empty; env_rel_val = []; env_nb_rel = 0; @@ -125,17 +128,43 @@ let env_of_rel n env = (* Named context *) -let push_named_context_val d (ctxt,vals) = - let rval = ref VKnone in - Context.Named.add d ctxt, (get_id d,rval)::vals +let push_named_context_val_val d rval ctxt = +(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *) + { + env_named_ctx = Context.Named.add d ctxt.env_named_ctx; + env_named_map = Id.Map.add (NamedDecl.get_id d) (d, rval) ctxt.env_named_map; + } + +let push_named_context_val d ctxt = + push_named_context_val_val d (ref VKnone) ctxt + +let match_named_context_val c = match c.env_named_ctx with +| [] -> None +| decl :: ctx -> + let (_, v) = Id.Map.find (NamedDecl.get_id decl) c.env_named_map in + let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in + let cval = { env_named_ctx = ctx; env_named_map = map } in + Some (decl, v, cval) + +let map_named_val f ctxt = + let open Context.Named.Declaration in + let fold accu d = + let d' = map_constr f d in + let accu = + if d == d' then accu + else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu + in + (accu, d') + in + let map, ctx = List.fold_map fold ctxt.env_named_map ctxt.env_named_ctx in + if map == ctxt.env_named_map then ctxt + else { env_named_ctx = ctx; env_named_map = map } let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); assert (env.env_rel_context = []); *) - let rval = ref VKnone in { env_globals = env.env_globals; - env_named_context = Context.Named.add d env.env_named_context; - env_named_vals = (get_id d, rval) :: env.env_named_vals; + env_named_context = push_named_context_val d env.env_named_context; env_rel_context = env.env_rel_context; env_rel_val = env.env_rel_val; env_nb_rel = env.env_nb_rel; @@ -146,8 +175,11 @@ let push_named d env = indirect_pterms = env.indirect_pterms; } +let lookup_named id env = + fst (Id.Map.find id env.env_named_context.env_named_map) + let lookup_named_val id env = - snd(List.find (fun (id',_) -> Id.equal id id') env.env_named_vals) + snd(Id.Map.find id env.env_named_context.env_named_map) (* Warning all the names should be different *) let env_of_named id env = env diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index e551d22c81..866790367d 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -40,12 +40,14 @@ val force_lazy_val : lazy_val -> (values * Id.Set.t) option val dummy_lazy_val : unit -> lazy_val val build_lazy_val : lazy_val -> (values * Id.Set.t) -> unit -type named_vals = (Id.t * lazy_val) list +type named_context_val = private { + env_named_ctx : Context.Named.t; + env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; +} type env = { env_globals : globals; - env_named_context : Context.Named.t; - env_named_vals : named_vals; + env_named_context : named_context_val; env_rel_context : Context.Rel.t; env_rel_val : lazy_val list; env_nb_rel : int; @@ -56,8 +58,6 @@ type env = { indirect_pterms : Opaqueproof.opaquetab; } -type named_context_val = Context.Named.t * named_vals - val empty_named_context_val : named_context_val val empty_env : env @@ -73,7 +73,15 @@ val env_of_rel : int -> env -> env val push_named_context_val : Context.Named.Declaration.t -> named_context_val -> named_context_val +val push_named_context_val_val : + Context.Named.Declaration.t -> lazy_val -> named_context_val -> named_context_val +val match_named_context_val : + named_context_val -> (Context.Named.Declaration.t * lazy_val * named_context_val) option +val map_named_val : + (constr -> constr) -> named_context_val -> named_context_val + val push_named : Context.Named.Declaration.t -> env -> env +val lookup_named : Id.t -> env -> Context.Named.Declaration.t val lookup_named_val : Id.t -> env -> lazy_val val env_of_named : Id.t -> env -> env diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 6c664f7918..1ae89347ad 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -316,7 +316,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (try let cuniv = conv_table_key infos fl1 fl2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv - with NotConvertible -> + with NotConvertible | Univ.UniverseInconsistency _ -> (* else the oracle tells which constant is to be expanded *) let oracle = CClosure.oracle_of_infos infos in let (app1,app2) = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 9812c45f7b..8a2b2469d6 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -36,7 +36,7 @@ type 'a extended_conversion_function = type conv_pb = CONV | CUMUL type 'a universe_compare = - { (* Might raise NotConvertible *) + { (* Might raise NotConvertible or UnivInconsistency *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; @@ -56,9 +56,12 @@ constructors. *) val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare +(** These two never raise UnivInconsistency, inferred_universes + just gathers the constraints. *) val checked_universes : UGraph.t universe_compare val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare +(** These two functions can only raise NotConvertible *) val conv : constr extended_conversion_function val conv_leq : types extended_conversion_function @@ -70,6 +73,9 @@ val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> types infer_conversion_function +(** Depending on the universe state functions, this might raise + [UniverseInconsistency] in addition to [NotConvertible] (for better error + messages). *) val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 09f7bd75cd..e4b3fcbf1a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -62,6 +62,8 @@ open Names open Declarations open Context.Named.Declaration +module NamedDecl = Context.Named.Declaration + (** {6 Safe environments } Fields of [safe_environment] : @@ -213,8 +215,8 @@ type private_constant_role = Term_typing.side_effect_role = | Schema of inductive * string let empty_private_constants = [] -let add_private x xs = x :: xs -let concat_private xs ys = xs @ ys +let add_private x xs = if List.mem_f Term_typing.equal_eff x xs then xs else x :: xs +let concat_private xs ys = List.fold_right add_private 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 @@ -361,7 +363,7 @@ let check_required current_libs needed = cost too much. *) let safe_push_named d env = - let id = get_id d in + let id = NamedDecl.get_id d in let _ = try let _ = Environ.lookup_named id env in @@ -794,7 +796,10 @@ type compiled_library = { type native_library = Nativecode.global list let get_library_native_symbols senv dir = - DPMap.find dir senv.native_symbols + try DPMap.find dir senv.native_symbols + with Not_found -> CErrors.user_err ~hdr:"get_library_native_symbols" + Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++ + (str "This use case is not supported, but disabling the native compiler may help.")) (** FIXME: MS: remove?*) let current_modpath senv = senv.modpath @@ -816,7 +821,7 @@ let export ?except senv dir = try join_safe_environment ?except senv with e -> let e = CErrors.push e in - CErrors.errorlabstrm "export" (CErrors.iprint e) + CErrors.user_err ~hdr:"export" (CErrors.iprint e) in assert(senv.future_cst = []); let () = check_current_library dir senv in @@ -852,7 +857,7 @@ let import lib cst vodigest senv = check_required senv.required lib.comp_deps; check_engagement senv.env lib.comp_enga; if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then - CErrors.errorlabstrm "Safe_typing.import" + CErrors.user_err ~hdr:"Safe_typing.import" (Pp.strbrk "Cannot load a library with the same name as the current one."); let mp = MPfile lib.comp_name in let mb = lib.comp_mod in diff --git a/kernel/term.ml b/kernel/term.ml index 15f187e5c4..62c161be4c 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -328,38 +328,9 @@ let destCoFix c = match kind_of_term c with let isCoFix c = match kind_of_term c with CoFix _ -> true | _ -> false (******************************************************************) -(* Cast management *) -(******************************************************************) - -let rec strip_outer_cast c = match kind_of_term c with - | Cast (c,_,_) -> strip_outer_cast c - | _ -> c - -(* Fonction spéciale qui laisse les cast clés sous les Fix ou les Case *) - -let under_outer_cast f c = match kind_of_term c with - | Cast (b,k,t) -> mkCast (f b, k, f t) - | _ -> f c - -let rec under_casts f c = match kind_of_term c with - | Cast (c,k,t) -> mkCast (under_casts f c, k, t) - | _ -> f c - -(******************************************************************) (* Flattening and unflattening of embedded applications and casts *) (******************************************************************) -(* flattens application lists throwing casts in-between *) -let collapse_appl c = match kind_of_term c with - | App (f,cl) -> - let rec collapse_rec f cl2 = - match kind_of_term (strip_outer_cast f) with - | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | _ -> mkApp (f,cl2) - in - collapse_rec f cl - | _ -> c - let decompose_app c = match kind_of_term c with | App (f,cl) -> (f, Array.to_list cl) @@ -465,7 +436,7 @@ let rec to_lambda n prod = match kind_of_term prod with | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd) | Cast (c,_,_) -> to_lambda n c - | _ -> errorlabstrm "to_lambda" (mt ()) + | _ -> user_err ~hdr:"to_lambda" (mt ()) let rec to_prod n lam = if Int.equal n 0 then @@ -474,7 +445,7 @@ let rec to_prod n lam = match kind_of_term lam with | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd) | Cast (c,_,_) -> to_prod n c - | _ -> errorlabstrm "to_prod" (mt ()) + | _ -> user_err ~hdr:"to_prod" (mt ()) let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) diff --git a/kernel/term.mli b/kernel/term.mli index 60a3c77154..a8d9dfbfff 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -349,20 +349,6 @@ val strip_lam_n : int -> constr -> constr val strip_prod_assum : types -> types val strip_lam_assum : constr -> constr -(** Flattens application lists *) -val collapse_appl : constr -> constr - - -(** 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 - -(** Apply a function letting Casted types in place *) -val under_casts : (constr -> constr) -> constr -> constr - -(** Apply a function under components of Cast if any *) -val under_outer_cast : (constr -> constr) -> constr -> constr - (** {5 ... } *) (** An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort. Such a term can canonically be seen as the pair of a context of types diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 749b5dbafa..3a0d1a2a5e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -20,7 +20,9 @@ open Declarations open Environ open Entries open Typeops -open Fast_typeops + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration let constrain_type env j poly subst = function | `None -> @@ -249,18 +251,17 @@ let global_vars_set_constant_type env = function | RegularArity t -> global_vars_set env t | TemplateArity (ctx,_) -> Context.Rel.fold_outside - (Context.Rel.Declaration.fold + (RelDecl.fold_constr (fun t c -> Id.Set.union (global_vars_set env t) c)) ctx ~init:Id.Set.empty let record_aux env s_ty s_bo suggested_expr = - let open Context.Named.Declaration in let in_ty = keep_hyps env s_ty in let v = String.concat " " (CList.map_filter (fun decl -> - let id = get_id decl in - if List.exists (Id.equal id % get_id) in_ty then None + let id = NamedDecl.get_id decl in + if List.exists (NamedDecl.get_id %> Id.equal 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) @@ -269,26 +270,25 @@ 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) = - let open Context.Named.Declaration in let check declared inferred = - let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in + let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in if not (Id.Set.subset inferred_set declared_set) then let l = Id.Set.elements (Idset.diff inferred_set declared_set) in let n = List.length l in - errorlabstrm "" (Pp.(str "The following section " ++ + user_err (Pp.(str "The following section " ++ str (String.plural n "variable") ++ 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 decl -> - let id = get_id decl in - List.exists (Names.Id.equal id % get_id) l) + let id = NamedDecl.get_id decl in + List.exists (NamedDecl.get_id %> Names.Id.equal id) l) (named_context env) in (* We try to postpone the computation of used section variables *) let hyps, def = - let context_ids = List.map get_id (named_context env) in + let context_ids = List.map NamedDecl.get_id (named_context env) in match ctx with | None when not (List.is_empty context_ids) -> (* No declared section vars, and non-empty section context: @@ -482,8 +482,7 @@ let translate_local_def mb env id centry = | Undef _ -> () | Def _ -> () | OpaqueDef lc -> - let open Context.Named.Declaration in - let context_ids = List.map get_id (named_context env) in + let context_ids = List.map NamedDecl.get_id (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 diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index fcd95576c0..89b5fc40e3 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -30,6 +30,7 @@ val inline_entry_side_effects : yet type checked proof. *) val uniq_seff : side_effects -> side_effects +val equal_eff : side_effect -> side_effect -> bool val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 0059111c09..7d9a2aac09 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -14,11 +14,12 @@ open Term open Vars open Declarations open Environ -open Entries open Reduction open Inductive open Type_errors -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y @@ -35,61 +36,46 @@ let check_constraints cst env = if Environ.check_constraints cst env then () else error_unsatisfied_constraints env cst -(* This should be a type (a priori without intension to be an assumption) *) -let type_judgment env j = - match kind_of_term(whd_all env j.uj_type) with - | Sort s -> {utj_val = j.uj_val; utj_type = s } - | _ -> error_not_type env j +(* This should be a type (a priori without intention to be an assumption) *) +let check_type env c t = + match kind_of_term(whd_all env t) with + | Sort s -> s + | _ -> error_not_type env (make_judge c t) -(* This should be a type intended to be assumed. The error message is *) -(* not as useful as for [type_judgment]. *) -let assumption_of_judgment env j = - try (type_judgment env j).utj_val +(* This should be a type intended to be assumed. The error message is + not as useful as for [type_judgment]. *) +let check_assumption env t ty = + try let _ = check_type env t ty in t with TypeError _ -> - error_assumption env j + error_assumption env (make_judge t ty) (************************************************) -(* Incremental typing rules: builds a typing judgement given the *) -(* judgements for the subterms. *) +(* Incremental typing rules: builds a typing judgment given the *) +(* judgments for the subterms. *) (*s Type of sorts *) (* Prop and Set *) -let judge_of_prop = - { uj_val = mkProp; - uj_type = mkSort type1_sort } - -let judge_of_set = - { uj_val = mkSet; - uj_type = mkSort type1_sort } - -let judge_of_prop_contents = function - | Null -> judge_of_prop - | Pos -> judge_of_set +let type1 = mkSort type1_sort (* Type of Type(i). *) -let judge_of_type u = +let type_of_type u = let uu = Universe.super u in - { uj_val = mkType u; - uj_type = mkType uu } + mkType uu (*s Type of a de Bruijn index. *) -let judge_of_relative env n = +let type_of_relative env n = try - let typ = get_type (lookup_rel n env) in - { uj_val = mkRel n; - uj_type = lift n typ } + env |> lookup_rel n |> RelDecl.get_type |> lift n with Not_found -> error_unbound_rel env n (* Type of variables *) -let judge_of_variable env id = - try - let ty = named_type id env in - make_judge (mkVar id) ty +let type_of_variable env id = + try named_type id env with Not_found -> error_unbound_var env id @@ -98,11 +84,11 @@ let judge_of_variable env id = (* Checks if a context of variables can be instantiated by the variables of the current env. Order does not have to be checked assuming that all names are distinct *) -let check_hyps_inclusion env c sign = +let check_hyps_inclusion env f c sign = Context.Named.fold_outside (fun d1 () -> let open Context.Named.Declaration in - let id = get_id d1 in + let id = NamedDecl.get_id d1 in try let d2 = lookup_named id env in conv env (get_type d2) (get_type d1); @@ -114,7 +100,7 @@ let check_hyps_inclusion env c sign = | LocalDef _, LocalAssum _ -> raise NotConvertible | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1); with Not_found | NotConvertible | Option.Heterogeneous -> - error_reference_variables env id c) + error_reference_variables env id (f c)) sign ~init:() @@ -122,35 +108,9 @@ let check_hyps_inclusion env c sign = (* Make a type polymorphic if an arity *) -let extract_level env p = - let _,c = dest_prod_assum env p in - match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None - -let extract_context_levels env l = - let fold l = function - | LocalAssum (_,p) -> extract_level env p :: l - | LocalDef _ -> l - in - List.fold_left fold [] 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) -> - let ind, l = decompose_app (whd_all 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 - (* Type of constants *) + let type_of_constant_type_knowing_parameters env t paramtyps = match t with | RegularArity t -> t @@ -159,49 +119,28 @@ let type_of_constant_type_knowing_parameters env t paramtyps = let ctx,s = instantiate_universes env ctx ar paramtyps in mkArity (List.rev ctx,s) -let type_of_constant_knowing_parameters env cst paramtyps = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in +let type_of_constant_knowing_parameters env (kn,u as cst) args = + let cb = lookup_constant kn env in + let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty, cu = constant_type env cst in - type_of_constant_type_knowing_parameters env ty paramtyps, cu + let ty = type_of_constant_type_knowing_parameters env ty args in + let () = check_constraints cu env in + ty -let type_of_constant_knowing_parameters_in env cst paramtyps = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in +let type_of_constant_knowing_parameters_in env (kn,u as cst) args = + let cb = lookup_constant kn env in + let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ty paramtyps - -let type_of_constant_type env t = - type_of_constant_type_knowing_parameters env t [||] + type_of_constant_type_knowing_parameters env ty args let type_of_constant env cst = type_of_constant_knowing_parameters env cst [||] let type_of_constant_in env cst = - let cb = lookup_constant (fst cst) env in - let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in - let ar = constant_type_in env cst in - type_of_constant_type_knowing_parameters env ar [||] - -let judge_of_constant_knowing_parameters env (kn,u as cst) args = - let c = mkConstU cst in - let ty, cu = type_of_constant_knowing_parameters env cst args in - let () = check_constraints cu env in - make_judge c ty - -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] - -let type_of_projection env (p,u) = - let cst = Projection.constant p in - let cb = lookup_constant cst env in - match cb.const_proj with - | Some pb -> - if cb.const_polymorphic then - Vars.subst_instance_constr u pb.proj_type - else pb.proj_type - | None -> raise (Invalid_argument "type_of_projection: not a projection") + type_of_constant_knowing_parameters_in env cst [||] +let type_of_constant_type env t = + type_of_constant_type_knowing_parameters env t [||] (* Type of a lambda-abstraction. *) @@ -215,40 +154,36 @@ let type_of_projection env (p,u) = and no upper constraint exists on the sort $s$, we don't need to compute $s$ *) -let judge_of_abstraction env name var j = - { uj_val = mkLambda (name, var.utj_val, j.uj_val); - uj_type = mkProd (name, var.utj_val, j.uj_type) } - -(* Type of let-in. *) - -let judge_of_letin env name defj typj j = - { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ; - uj_type = subst1 defj.uj_val j.uj_type } +let type_of_abstraction env name var ty = + mkProd (name, var, ty) (* Type of an application. *) -let judge_of_apply env funj argjv = - let rec apply_rec n typ = function - | [] -> - { uj_val = mkApp (j_val funj, Array.map j_val argjv); - uj_type = typ } - | hj::restjl -> - (match kind_of_term (whd_all env typ) with - | Prod (_,c1,c2) -> - (try - let () = conv_leq false env hj.uj_type c1 in - apply_rec (n+1) (subst1 hj.uj_val c2) restjl - with NotConvertible -> - error_cant_apply_bad_type env - (n,c1, hj.uj_type) - funj argjv) - - | _ -> - error_cant_apply_not_functional env funj argjv) - in - apply_rec 1 - funj.uj_type - (Array.to_list argjv) +let make_judgev c t = + Array.map2 make_judge c t + +let type_of_apply env func funt argsv argstv = + let len = Array.length argsv in + let rec apply_rec i typ = + if Int.equal i len then typ + else + (match kind_of_term (whd_all env typ) with + | Prod (_,c1,c2) -> + let arg = argsv.(i) and argt = argstv.(i) in + (try + let () = conv_leq false env argt c1 in + apply_rec (i+1) (subst1 arg c2) + with NotConvertible -> + error_cant_apply_bad_type env + (i+1,c1,argt) + (make_judge func funt) + (make_judgev argsv argstv)) + + | _ -> + error_cant_apply_not_functional env + (make_judge func funt) + (make_judgev argsv argstv)) + in apply_rec 0 funt (* Type of product *) @@ -281,10 +216,9 @@ let sort_of_product env domsort rangsort = where j.uj_type is convertible to a sort s2 *) -let judge_of_product env name t1 t2 = - let s = sort_of_product env t1.utj_type t2.utj_type in - { uj_val = mkProd (name, t1.utj_val, t2.utj_val); - uj_type = mkSort s } +let type_of_product env name s1 s2 = + let s = sort_of_product env s1 s2 in + mkSort s (* Type of a type cast *) @@ -295,29 +229,20 @@ let judge_of_product env name t1 t2 = env |- c:typ2 *) -let judge_of_cast env cj k tj = - let expected_type = tj.utj_val in +let check_cast env c ct k expected_type = try - let c, cst = - match k with - | VMcast -> - mkCast (cj.uj_val, k, 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 - | REVERTcast -> - cj.uj_val, - default_conv ~l2r:true CUMUL env cj.uj_type expected_type - | NATIVEcast -> - let sigma = Nativelambda.empty_evars in - mkCast (cj.uj_val, k, expected_type), - Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type - in - { uj_val = c; - uj_type = expected_type } + match k with + | VMcast -> + vm_conv CUMUL env ct expected_type + | DEFAULTcast -> + default_conv ~l2r:false CUMUL env ct expected_type + | REVERTcast -> + default_conv ~l2r:true CUMUL env ct expected_type + | NATIVEcast -> + let sigma = Nativelambda.empty_evars in + Nativeconv.native_conv CUMUL sigma env ct expected_type with NotConvertible -> - error_actual_type env cj expected_type + error_actual_type env (make_judge c ct) expected_type (* Inductive types. *) @@ -333,83 +258,78 @@ let judge_of_cast env cj k tj = the App case of execute; from this constraints, the expected dynamic constraints of the form u<=v are enforced *) -let judge_of_inductive_knowing_parameters env (ind,u as indu) args = - let c = mkIndU indu in +let type_of_inductive_knowing_parameters env (ind,u as indu) args = let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env c mib.mind_hyps; + check_hyps_inclusion env mkIndU indu mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters env (spec,u) args in - check_constraints cst env; - make_judge c t + check_constraints cst env; + t -let judge_of_inductive env (ind,u as indu) = - let c = mkIndU indu in - let (mib,mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env c mib.mind_hyps; - let t,cst = Inductive.constrained_type_of_inductive env (spec,u) in - check_constraints cst env; - (make_judge c t) +let type_of_inductive env (ind,u as indu) = + let (mib,mip) = lookup_mind_specif env ind in + check_hyps_inclusion env mkIndU indu mib.mind_hyps; + let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in + check_constraints cst env; + t (* Constructors. *) -let judge_of_constructor env (c,u as cu) = - let constr = mkConstructU cu in - let _ = +let type_of_constructor env (c,u as cu) = + let () = let ((kn,_),_) = c in let mib = lookup_mind kn env in - check_hyps_inclusion env constr mib.mind_hyps in + check_hyps_inclusion env mkConstructU cu mib.mind_hyps + in let specif = lookup_mind_specif env (inductive_of_constructor c) in let t,cst = constrained_type_of_constructor cu specif in let () = check_constraints cst env in - (make_judge constr t) + t (* Case. *) -let check_branch_types env (ind,u) cj (lfj,explft) = - try conv_leq_vecti env (Array.map j_type lfj) explft +let check_branch_types env (ind,u) c ct lft explft = + try conv_leq_vecti env lft explft with NotConvertibleVect i -> - error_ill_formed_branch env cj.uj_val ((ind,i+1),u) lfj.(i).uj_type explft.(i) + error_ill_formed_branch env c ((ind,i+1),u) lft.(i) explft.(i) | Invalid_argument _ -> - error_number_branches env cj (Array.length explft) + error_number_branches env (make_judge c ct) (Array.length explft) -let judge_of_case env ci pj cj lfj = +let type_of_case env ci p pt c ct lf lft = let (pind, _ as indspec) = - try find_rectype env cj.uj_type - with Not_found -> error_case_not_inductive env cj in + try find_rectype env ct + with Not_found -> error_case_not_inductive env (make_judge c ct) in let () = check_case_info env pind ci in let (bty,rslty) = - type_case_branches env indspec pj cj.uj_val in - let () = check_branch_types env pind cj (lfj,bty) in - ({ uj_val = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, - Array.map j_val lfj); - uj_type = rslty }) + type_case_branches env indspec (make_judge p pt) c in + let () = check_branch_types env pind c ct lft bty in + rslty -let judge_of_projection env p cj = +let type_of_projection env p c ct = let pb = lookup_projection p env in let (ind,u), args = - try find_rectype env cj.uj_type - with Not_found -> error_case_not_inductive env cj + try find_rectype env ct + with Not_found -> error_case_not_inductive env (make_judge c ct) in - assert(eq_mind pb.proj_ind (fst ind)); - let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in - let ty = substl (cj.uj_val :: List.rev args) ty in - {uj_val = mkProj (p,cj.uj_val); - uj_type = ty} + assert(eq_mind pb.proj_ind (fst ind)); + let ty = Vars.subst_instance_constr u pb.Declarations.proj_type in + substl (c :: List.rev args) ty + (* Fixpoints. *) (* Checks the type of a general (co)fixpoint, i.e. without checking *) (* the specific guard condition. *) -let type_fixpoint env lna lar vdefj = - let lt = Array.length vdefj in +let check_fixpoint env lna lar vdef vdeft = + let lt = Array.length vdeft in assert (Int.equal (Array.length lar) lt); try - conv_leq_vecti env (Array.map j_type vdefj) (Array.map (fun ty -> lift lt ty) lar) + conv_leq_vecti env vdeft (Array.map (fun ty -> lift lt ty) lar) with NotConvertibleVect i -> - error_ill_typed_rec_body env i lna vdefj lar + error_ill_typed_rec_body env i lna (make_judgev vdef vdeft) lar (************************************************************************) (************************************************************************) @@ -419,95 +339,96 @@ let type_fixpoint env lna lar vdefj = Ind et Constructsi un jour cela devient des constructions arbitraires et non plus des variables *) let rec execute env cstr = + let open Context.Rel.Declaration in match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> - judge_of_prop_contents c + type1 | Sort (Type u) -> - judge_of_type u + type_of_type u | Rel n -> - judge_of_relative env n + type_of_relative env n | Var id -> - judge_of_variable env id + type_of_variable env id | Const c -> - judge_of_constant env c + type_of_constant env c | Proj (p, c) -> - let cj = execute env c in - judge_of_projection env p cj + let ct = execute env c in + type_of_projection env p c ct (* Lambda calculus operators *) | App (f,args) -> - let jl = execute_array env args in - let j = + let argst = execute_array env args in + let ft = match kind_of_term f with - | Ind ind when Environ.template_polymorphic_pind ind env -> - (* Sort-polymorphism of inductive types *) - let args = Array.map (fun j -> lazy j.uj_type) jl in - judge_of_inductive_knowing_parameters env ind args - | Const cst when Environ.template_polymorphic_pconstant cst env -> - (* Sort-polymorphism of constant *) - let args = Array.map (fun j -> lazy j.uj_type) jl in - judge_of_constant_knowing_parameters env cst args - | _ -> - (* No sort-polymorphism *) - execute env f + | Ind ind when Environ.template_polymorphic_pind ind env -> + (* Template sort-polymorphism of inductive types *) + let args = Array.map (fun t -> lazy t) argst in + type_of_inductive_knowing_parameters env ind args + | Const cst when Environ.template_polymorphic_pconstant cst env -> + (* Template sort-polymorphism of constants *) + let args = Array.map (fun t -> lazy t) argst in + type_of_constant_knowing_parameters env cst args + | _ -> + (* Full or no sort-polymorphism *) + execute env f in - judge_of_apply env j jl + + type_of_apply env f ft args argst | Lambda (name,c1,c2) -> - let varj = execute_type env c1 in - let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in - let j' = execute env1 c2 in - judge_of_abstraction env name varj j' + let _ = execute_is_type env c1 in + let env1 = push_rel (LocalAssum (name,c1)) env in + let c2t = execute env1 c2 in + type_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> - let varj = execute_type env c1 in - let env1 = push_rel (LocalAssum (name,varj.utj_val)) env in - let varj' = execute_type env1 c2 in - judge_of_product env name varj varj' + let vars = execute_is_type env c1 in + let env1 = push_rel (LocalAssum (name,c1)) env in + let vars' = execute_is_type env1 c2 in + type_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> - let j1 = execute env c1 in - let j2 = execute_type env c2 in - let _ = judge_of_cast env j1 DEFAULTcast j2 in - let env1 = push_rel (LocalDef (name,j1.uj_val,j2.utj_val)) env in - let j' = execute env1 c3 in - judge_of_letin env name j1 j2 j' + let c1t = execute env c1 in + let _c2s = execute_is_type env c2 in + let () = check_cast env c1 c1t DEFAULTcast c2 in + let env1 = push_rel (LocalDef (name,c1,c2)) env in + let c3t = execute env1 c3 in + subst1 c1 c3t | Cast (c,k,t) -> - let cj = execute env c in - let tj = execute_type env t in - judge_of_cast env cj k tj + let ct = execute env c in + let _ts = (check_type env t (execute env t)) in + let () = check_cast env c ct k t in + t (* Inductive types *) | Ind ind -> - judge_of_inductive env ind + type_of_inductive env ind | Construct c -> - judge_of_constructor env c + type_of_constructor env c | Case (ci,p,c,lf) -> - let cj = execute env c in - let pj = execute env p in - let lfj = execute_array env lf in - judge_of_case env ci pj cj lfj + let ct = execute env c in + let pt = execute env p in + let lft = execute_array env lf in + type_of_case env ci p pt c ct lf lft | Fix ((vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let fix = (vni,recdef') in - check_fix env fix; - make_judge (mkFix fix) fix_ty + check_fix env fix; fix_ty | CoFix (i,recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let cofix = (i,recdef') in - check_cofix env cofix; - (make_judge (mkCoFix cofix) fix_ty) + check_cofix env cofix; fix_ty (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -516,53 +437,158 @@ let rec execute env cstr = | Evar _ -> anomaly (Pp.str "the kernel does not support existential variables") -and execute_type env constr = - let j = execute env constr in - type_judgment env j +and execute_is_type env constr = + let t = execute env constr in + check_type env constr t and execute_recdef env (names,lar,vdef) i = - let larj = execute_array env lar in - let lara = Array.map (assumption_of_judgment env) larj in + let lart = execute_array env lar in + let lara = Array.map2 (check_assumption env) lar lart in let env1 = push_rec_types (names,lara,vdef) env in - let vdefj = execute_array env1 vdef in - let vdefv = Array.map j_val vdefj in - let () = type_fixpoint env1 names lara vdefj in - (lara.(i),(names,lara,vdefv)) + let vdeft = execute_array env1 vdef in + let () = check_fixpoint env1 names lara vdef vdeft in + (lara.(i),(names,lara,vdef)) and execute_array env = Array.map (execute env) (* Derived functions *) let infer env constr = - let j = execute env constr in - assert (eq_constr j.uj_val constr); - j + let t = execute env constr in + make_judge constr t + +let infer = + if Flags.profile then + let infer_key = Profile.declare_profile "Fast_infer" in + Profile.profile2 infer_key (fun b c -> infer b c) + else (fun b c -> infer b c) + +let assumption_of_judgment env {uj_val=c; uj_type=t} = + check_assumption env c t -(* let infer_key = Profile.declare_profile "infer" *) -(* let infer = Profile.profile2 infer_key infer *) +let type_judgment env {uj_val=c; uj_type=t} = + let s = check_type env c t in + {utj_val = c; utj_type = s } let infer_type env constr = - let j = execute_type env constr in - j + let t = execute env constr in + let s = check_type env constr t in + {utj_val = constr; utj_type = s} let infer_v env cv = let jv = execute_array env cv in - jv + make_judgev cv jv (* Typing of several terms. *) let infer_local_decl env id = function - | LocalDefEntry c -> - let j = infer env c in - LocalDef (Name id, j.uj_val, j.uj_type) - | LocalAssumEntry c -> - let j = infer env c in - LocalAssum (Name id, assumption_of_judgment env j) + | Entries.LocalDefEntry c -> + let t = execute env c in + RelDecl.LocalDef (Name id, c, t) + | Entries.LocalAssumEntry c -> + let t = execute env c in + RelDecl.LocalAssum (Name id, check_assumption env c t) let infer_local_decls env decls = let rec inferec env = function | (id, d) :: l -> let (env, l) = inferec env l in let d = infer_local_decl env id d in - (push_rel d env, Context.Rel.add d l) - | [] -> (env, Context.Rel.empty) in + (push_rel d env, Context.Rel.add d l) + | [] -> (env, Context.Rel.empty) + in inferec env decls + +let judge_of_prop = make_judge mkProp type1 +let judge_of_set = make_judge mkSet type1 +let judge_of_type u = make_judge (mkType u) (type_of_type u) + +let judge_of_prop_contents = function + | Null -> judge_of_prop + | Pos -> judge_of_set + +let judge_of_relative env k = make_judge (mkRel k) (type_of_relative env k) + +let judge_of_variable env x = make_judge (mkVar x) (type_of_variable env x) + +let judge_of_constant env cst = make_judge (mkConstU cst) (type_of_constant env cst) +let judge_of_constant_knowing_parameters env cst args = + make_judge (mkConstU cst) (type_of_constant_knowing_parameters env cst args) + +let judge_of_projection env p cj = + make_judge (mkProj (p,cj.uj_val)) (type_of_projection env p cj.uj_val cj.uj_type) + +let dest_judgev v = + Array.map j_val v, Array.map j_type v + +let judge_of_apply env funj argjv = + let args, argtys = dest_judgev argjv in + make_judge (mkApp (funj.uj_val, args)) (type_of_apply env funj.uj_val funj.uj_type args argtys) + +let judge_of_abstraction env x varj bodyj = + make_judge (mkLambda (x, varj.utj_val, bodyj.uj_val)) + (type_of_abstraction env x varj.utj_val bodyj.uj_type) + +let judge_of_product env x varj outj = + make_judge (mkProd (x, varj.utj_val, outj.utj_val)) + (mkSort (sort_of_product env varj.utj_type outj.utj_type)) + +let judge_of_letin env name defj typj j = + make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) + (subst1 defj.uj_val j.uj_type) + +let judge_of_cast env cj k tj = + let () = check_cast env cj.uj_val cj.uj_type k tj.utj_val in + let c = match k with | REVERTcast -> cj.uj_val | _ -> mkCast (cj.uj_val, k, tj.utj_val) in + make_judge c tj.utj_val + +let judge_of_inductive env indu = + make_judge (mkIndU indu) (type_of_inductive env indu) + +let judge_of_constructor env cu = + make_judge (mkConstructU cu) (type_of_constructor env cu) + +let judge_of_case env ci pj cj lfj = + let lf, lft = dest_judgev lfj in + make_judge (mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val, lft)) + (type_of_case env ci pj.uj_val pj.uj_type cj.uj_val cj.uj_type lf lft) + +let type_of_projection_constant env (p,u) = + let cst = Projection.constant p in + let cb = lookup_constant cst env in + match cb.const_proj with + | Some pb -> + if cb.const_polymorphic then + Vars.subst_instance_constr u pb.proj_type + else pb.proj_type + | None -> raise (Invalid_argument "type_of_projection: not a projection") + +(* Instantiation of terms on real arguments. *) + +(* Make a type polymorphic if an arity *) + +let extract_level env p = + let _,c = dest_prod_assum env p in + match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None + +let extract_context_levels env l = + let fold l = function + | RelDecl.LocalAssum (_,p) -> extract_level env p :: l + | RelDecl.LocalDef _ -> l + in + List.fold_left fold [] 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) -> + let ind, l = decompose_app (whd_all 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 diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 2112284ea6..007acae604 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -15,7 +15,7 @@ open Declarations (** {6 Typing functions (not yet tagged as safe) } - They return unsafe judgments that are "in context" of a set of + They return unsafe judgments that are "in context" of a set of (local) universe variables (the ones that appear in the term) and associated constraints. In case of polymorphic definitions, these variables and constraints will be generalized. @@ -91,9 +91,6 @@ val judge_of_cast : val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment -(* val judge_of_inductive_knowing_parameters : *) -(* env -> inductive -> unsafe_judgment array -> unsafe_judgment *) - val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment (** {6 Type of Cases. } *) @@ -101,24 +98,15 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -(** Typecheck general fixpoint (not checking guard conditions) *) -val type_fixpoint : env -> Name.t array -> types array - -> unsafe_judgment array -> unit - -val type_of_constant : env -> pconstant -> types constrained - val type_of_constant_type : env -> constant_type -> types -val type_of_projection : env -> Names.projection puniverses -> types +val type_of_projection_constant : env -> Names.projection puniverses -> types val type_of_constant_in : env -> pconstant -> types val type_of_constant_type_knowing_parameters : env -> constant_type -> types Lazy.t array -> types -val type_of_constant_knowing_parameters : - env -> pconstant -> types Lazy.t array -> types constrained - val type_of_constant_knowing_parameters_in : env -> pconstant -> types Lazy.t array -> types @@ -127,4 +115,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> constant_type (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> constr -> Context.section_context -> unit +val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index e2712615be..4884d0deb1 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -638,19 +638,6 @@ let check_smaller g strict u v = type 'a check_function = universes -> 'a -> 'a -> bool -let check_equal_expr g x y = - x == y || (let (u, n) = x and (v, m) = y in - Int.equal n m && check_equal g u v) - -let check_eq_univs g l1 l2 = - let f x1 x2 = check_equal_expr g x1 x2 in - let exists x1 l = Universe.exists (fun x2 -> f x1 x2) l in - Universe.for_all (fun x1 -> exists x1 l2) l1 - && Universe.for_all (fun x2 -> exists x2 l1) l2 - -let check_eq g u v = - Universe.equal u v || check_eq_univs g u v - let check_smaller_expr g (u,n) (v,m) = let diff = n - m in match diff with @@ -669,7 +656,13 @@ let real_check_leq g u v = let check_leq g u v = Universe.equal u v || is_type0m_univ u || - check_eq_univs g u v || real_check_leq g u v + real_check_leq g u v + +let check_eq_univs g l1 l2 = + real_check_leq g l1 l2 && real_check_leq g l2 l1 + +let check_eq g u v = + Universe.equal u v || check_eq_univs g u v (* enforce_univ_eq g u v will force u=v if possible, will fail otherwise *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 9224ec48d7..09f884ecd0 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -468,15 +468,32 @@ struct else if Level.is_prop u then hcons (Level.set,n+k) else hcons (u,n+k) - + + type super_result = + SuperSame of bool + (* The level expressions are in cumulativity relation. boolean + indicates if left is smaller than right? *) + | SuperDiff of int + (* The level expressions are unrelated, the comparison result + is canonical *) + + (** [super u v] compares two level expressions, + returning [SuperSame] if they refer to the same level at potentially different + increments or [SuperDiff] if they are different. The booleans indicate if the + left expression is "smaller" than the right one in both cases. *) let super (u,n as x) (v,n' as y) = let cmp = Level.compare u v in - if Int.equal cmp 0 then - if n < n' then Inl true - else Inl false - else if is_prop x then Inl true - else if is_prop y then Inl false - else Inr cmp + if Int.equal cmp 0 then SuperSame (n < n') + else + match x, y with + | (l,0), (l',0) -> + let open RawLevel in + (match Level.data l, Level.data l' with + | Prop, Prop -> SuperSame false + | Prop, _ -> SuperSame true + | _, Prop -> SuperSame false + | _, _ -> SuperDiff cmp) + | _, _ -> SuperDiff cmp let to_string (v, n) = if Int.equal n 0 then Level.to_string v @@ -598,24 +615,26 @@ struct | Nil, _ -> l2 | _, Nil -> l1 | Cons (h1, _, t1), Cons (h2, _, t2) -> - (match Expr.super h1 h2 with - | Inl true (* h1 < h2 *) -> merge_univs t1 l2 - | Inl false -> merge_univs l1 t2 - | Inr c -> - if c <= 0 (* h1 < h2 is name order *) - then cons h1 (merge_univs t1 l2) - else cons h2 (merge_univs l1 t2)) + let open Expr in + (match super h1 h2 with + | SuperSame true (* h1 < h2 *) -> merge_univs t1 l2 + | SuperSame false -> merge_univs l1 t2 + | SuperDiff c -> + if c <= 0 (* h1 < h2 is name order *) + then cons h1 (merge_univs t1 l2) + else cons h2 (merge_univs l1 t2)) let sort u = let rec aux a l = match l with | Cons (b, _, l') -> - (match Expr.super a b with - | Inl false -> aux a l' - | Inl true -> l - | Inr c -> - if c <= 0 then cons a l - else cons b (aux a l')) + let open Expr in + (match super a b with + | SuperSame false -> aux a l' + | SuperSame true -> l + | SuperDiff c -> + if c <= 0 then cons a l + else cons b (aux a l')) | Nil -> cons a l in fold (fun a acc -> aux a acc) u nil diff --git a/kernel/vars.ml b/kernel/vars.ml index 2ca749d505..4affb5f9fb 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -8,7 +8,8 @@ open Names open Esubst -open Context.Rel.Declaration + +module RelDecl = Context.Rel.Declaration (*********************) (* Occurring *) @@ -160,14 +161,15 @@ let substnl laml n c = substn_many (make_subst laml) n c let substl laml c = substn_many (make_subst laml) 0 c let subst1 lam c = substn_many [|make_substituend lam|] 0 c -let substnl_decl laml k r = map_constr (fun c -> substnl laml k c) r -let substl_decl laml r = map_constr (fun c -> substnl laml 0 c) r -let subst1_decl lam r = map_constr (fun c -> subst1 lam c) r +let substnl_decl laml k r = RelDecl.map_constr (fun c -> substnl laml k c) r +let substl_decl laml r = RelDecl.map_constr (fun c -> substnl laml 0 c) r +let subst1_decl lam r = RelDecl.map_constr (fun c -> subst1 lam c) r (* Build a substitution from an instance, inserting missing let-ins *) let subst_of_rel_context_instance sign l = let rec aux subst sign l = + let open RelDecl in match sign, l with | LocalAssum _ :: sign', a::args' -> aux (a::subst) sign' args' | LocalDef (_,c,_)::sign', args' -> @@ -179,6 +181,15 @@ let subst_of_rel_context_instance sign l = let adjust_subst_to_rel_context sign l = List.rev (subst_of_rel_context_instance sign l) +let adjust_rel_to_rel_context sign n = + let rec aux sign = + let open RelDecl in + match sign with + | LocalAssum _ :: sign' -> let (n',p) = aux sign' in (n'+1,p) + | LocalDef (_,c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p) + | [] -> (0,n) + in snd (aux sign) + (* (thin_val sigma) removes identity substitutions from sigma *) let rec thin_val = function diff --git a/kernel/vars.mli b/kernel/vars.mli index 574d50eccb..f7535e6d8f 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -73,6 +73,10 @@ val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl (** For compatibility: returns the substitution reversed *) val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list +(** Take an index in an instance of a context and returns its index wrt to + the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *) +val adjust_rel_to_rel_context : Context.Rel.t -> int -> int + (** [substnl [a₁;...;an] k c] substitutes in parallel [a₁],...,[an] for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates accordingly indexes in [an],...,[a1] and [c]. In terms of typing, if diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 894f5296a8..74d956bef0 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -77,6 +77,7 @@ 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 _ -> + (* on the fly eta expansion *) conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ diff --git a/kernel/vm.ml b/kernel/vm.ml index eb992ef892..53483a2220 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -170,7 +170,7 @@ type whd = 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" +external push_vstack : vstack -> int -> unit = "coq_push_vstack" (* interpreteur *) @@ -206,7 +206,9 @@ let apply_varray vf varray = else begin push_ra stop; - push_vstack varray; + (* The fun code of [vf] will make sure we have enough stack, so we put 0 + here. *) + push_vstack varray 0; interprete (fun_code vf) vf (Obj.magic vf) (n - 1) end @@ -560,7 +562,9 @@ let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl let case_info sw = sw.sw_annot.ci let type_of_switch sw = - push_vstack sw.sw_stk; + (* The fun code of types will make sure we have enough stack, so we put 0 + here. *) + push_vstack sw.sw_stk 0; interprete sw.sw_type_code crazy_val sw.sw_env 0 let branch_arg k (tag,arity) = @@ -580,9 +584,10 @@ let branch_arg k (tag,arity) = let apply_switch sw arg = let tc = sw.sw_annot.tailcall in if tc then - (push_ra stop;push_vstack sw.sw_stk) + (push_ra stop;push_vstack sw.sw_stk sw.sw_annot.max_stack_size) else - (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk))); + (push_vstack sw.sw_stk sw.sw_annot.max_stack_size; + push_ra (popstop_code (Array.length sw.sw_stk))); interprete sw.sw_code arg sw.sw_env 0 let branch_of_switch k sw = |