diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-16 15:26:07 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-16 15:26:50 +0200 |
commit | 568aa9dff652d420e66cda7914d4bc265bb276e7 (patch) | |
tree | c493eaaa87636e304f5788136a5fd1c255816821 /kernel | |
parent | bce318b6d991587773ef2fb18c83de8d24bc4a5f (diff) | |
parent | 2d4701b4d1bdb0fb4f64dec9ffbd9ad90506ba26 (diff) |
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/declarations.mli | 16 | ||||
-rw-r--r-- | kernel/declareops.ml | 7 | ||||
-rw-r--r-- | kernel/entries.mli | 5 | ||||
-rw-r--r-- | kernel/fast_typeops.ml | 69 | ||||
-rw-r--r-- | kernel/fast_typeops.mli | 7 | ||||
-rw-r--r-- | kernel/indtypes.ml | 48 | ||||
-rw-r--r-- | kernel/inductive.ml | 54 | ||||
-rw-r--r-- | kernel/inductive.mli | 7 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 20 | ||||
-rw-r--r-- | kernel/safe_typing.mli | 4 | ||||
-rw-r--r-- | kernel/term_typing.ml | 45 | ||||
-rw-r--r-- | kernel/term_typing.mli | 12 | ||||
-rw-r--r-- | kernel/typeops.ml | 4 |
13 files changed, 176 insertions, 122 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 1b77d5b7c..8b42a90e4 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -66,6 +66,15 @@ type constant_def = type constant_universes = Univ.universe_context +(** The [typing_flags] are instructions to the type-checker which + modify its behaviour. The typing flags used in the type-checking + of a constant are tracked in their {!constant_body} so that they + can be displayed to the user. *) +type typing_flags = { + check_guarded : bool; (** If [false] then fixed points and co-fixed + points are assumed to be total. *) +} + (* some contraints are in constant_constraints, some other may be in * the OpaueDef *) type constant_body = { @@ -76,7 +85,11 @@ type constant_body = { const_polymorphic : bool; (** Is it polymorphic or not *) const_universes : constant_universes; const_proj : projection_body option; - const_inline_code : bool } + const_inline_code : bool; + const_typing_flags : typing_flags; (** The typing options which + were used for + type-checking. *) +} (** {6 Representation of mutual inductive types in the kernel } *) @@ -178,6 +191,7 @@ type mutual_inductive_body = { mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *) + mind_checked_positive : bool; (** [false] when the mutual-inductive was assumed to be well-founded, bypassing the positivity checker. *) } (** {6 Module declarations } *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index a09a8b786..78e2f386e 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -131,7 +131,8 @@ let subst_const_body sub cb = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; - const_inline_code = cb.const_inline_code } + const_inline_code = cb.const_inline_code; + const_typing_flags = cb.const_typing_flags } (** {7 Hash-consing of constants } *) @@ -254,7 +255,9 @@ let subst_mind_body sub mib = mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_polymorphic = mib.mind_polymorphic; mind_universes = mib.mind_universes; - mind_private = mib.mind_private } + mind_private = mib.mind_private; + mind_checked_positive = mib.mind_checked_positive; + } let inductive_instance mib = if mib.mind_polymorphic then diff --git a/kernel/entries.mli b/kernel/entries.mli index d07ca2103..8b29e3abd 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -51,7 +51,10 @@ type mutual_inductive_entry = { mind_entry_inds : one_inductive_entry list; mind_entry_polymorphic : bool; mind_entry_universes : Univ.universe_context; - mind_entry_private : bool option } + mind_entry_private : bool option; + mind_entry_check_positivity : bool; + (** [false] if positivity is to be assumed. *) +} (** {6 Constants (Definition/Axiom) } *) type 'a proof_output = constr Univ.in_universe_context_set * 'a diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 7f4ba8ecb..35c162cf3 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -327,7 +327,7 @@ let type_fixpoint env lna lar vdef vdeft = (* 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 rec execute ~flags env cstr = let open Context.Rel.Declaration in match kind_of_term cstr with (* Atomic terms *) @@ -347,12 +347,12 @@ let rec execute env cstr = judge_of_constant env c | Proj (p, c) -> - let ct = execute env c in + let ct = execute ~flags env c in judge_of_projection env p c ct (* Lambda calculus operators *) | App (f,args) -> - let argst = execute_array env args in + let argst = execute_array ~flags env args in let ft = match kind_of_term f with | Ind ind when Environ.template_polymorphic_pind ind env -> @@ -365,7 +365,7 @@ let rec execute env cstr = judge_of_constant_knowing_parameters env cst args | _ -> (* Full or no sort-polymorphism *) - execute env f + execute ~flags env f in judge_of_apply env f ft args argst @@ -373,25 +373,25 @@ let rec execute env cstr = | 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 + let c2t = execute ~flags env1 c2 in judge_of_abstraction env name c1 c2t | Prod (name,c1,c2) -> - let vars = execute_is_type env c1 in + let vars = execute_is_type ~flags env c1 in let env1 = push_rel (LocalAssum (name,c1)) env in - let vars' = execute_is_type env1 c2 in + let vars' = execute_is_type ~flags env1 c2 in judge_of_product env name vars vars' | LetIn (name,c1,c2,c3) -> - let c1t = execute env c1 in + let c1t = execute ~flags 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 + let c3t = execute ~flags env1 c3 in subst1 c1 c3t | Cast (c,k,t) -> - let ct = execute env c in + let ct = execute ~flags env c in let _ts = execute_type env t in let _ = judge_of_cast env c ct k t in t @@ -404,20 +404,20 @@ let rec execute env cstr = 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 + let ct = execute ~flags env c in + let pt = execute ~flags env p in + let lft = execute_array ~flags 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_ty,recdef') = execute_recdef ~flags env recdef i in let fix = (vni,recdef') in - check_fix env fix; fix_ty + check_fix env ~flags fix; fix_ty | CoFix (i,recdef) -> - let (fix_ty,recdef') = execute_recdef env recdef i in + let (fix_ty,recdef') = execute_recdef ~flags env recdef i in let cofix = (i,recdef') in - check_cofix env cofix; fix_ty + check_cofix env ~flags cofix; fix_ty (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -426,38 +426,41 @@ let rec execute env cstr = | Evar _ -> anomaly (Pp.str "the kernel does not support existential variables") -and execute_is_type env constr = - let t = execute env constr in +and execute_is_type ~flags env constr = + let t = execute ~flags env constr in check_type env constr t -and execute_type env constr = - let t = execute env constr in +and execute_type ~flags env constr = + let t = execute ~flags env constr in type_judgment env constr t -and execute_recdef env (names,lar,vdef) i = - let lart = execute_array env lar in +and execute_recdef ~flags env (names,lar,vdef) i = + let lart = execute_array ~flags 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 vdeft = execute_array ~flags 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) +and execute_array ~flags env = Array.map (execute ~flags env) (* Derived functions *) -let infer env constr = - let t = execute env constr in +let infer ~flags env constr = + let t = execute ~flags 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 infer - else infer + Profile.profile3 infer_key (fun a b c -> infer ~flags:a b c) + else (fun a b c -> infer ~flags:a b c) -let infer_type env constr = - execute_type env constr +(* Restores the labels of [infer] lost to profiling. *) +let infer ~flags env t = infer flags env t -let infer_v env cv = - let jv = execute_array env cv in +let infer_type ~flags env constr = + execute_type ~flags env constr + +let infer_v ~flags env cv = + let jv = execute_array ~flags env cv in make_judgev cv jv diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli index 05d52b2d3..45a603038 100644 --- a/kernel/fast_typeops.mli +++ b/kernel/fast_typeops.mli @@ -8,6 +8,7 @@ open Term open Environ +open Declarations (** {6 Typing functions (not yet tagged as safe) } @@ -18,6 +19,6 @@ open Environ *) -val infer : env -> constr -> unsafe_judgment -val infer_v : env -> constr array -> unsafe_judgment array -val infer_type : env -> types -> unsafe_type_judgment +val infer : flags:typing_flags -> env -> constr -> unsafe_judgment +val infer_v : flags:typing_flags -> env -> constr array -> unsafe_judgment array +val infer_type : flags:typing_flags -> env -> types -> unsafe_type_judgment diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index edb758f07..b74788d21 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -483,8 +483,12 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else for use by the guard condition (terms at these positions are considered sub-terms) as well as the number of of non-uniform arguments (used to generate induction schemes, so a priori less - relevant to the kernel). *) -let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as ind) nnonrecargs lcnames indlc = + relevant to the kernel). + + If [chkpos] is [false] then positivity is assumed, and + [check_positivity_one] computes the subterms occurrences in a + best-effort fashion. *) +let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as ind) nnonrecargs lcnames indlc = let nparamsctxt = Context.Rel.length paramsctxt in let nmr = Context.Rel.nhyps paramsctxt in (** Positivity of one argument [c] of a constructor (i.e. the @@ -501,9 +505,12 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as i recursive call. Occurrences in the right-hand side of the product must be strictly positive.*) (match weaker_noccur_between env n ntypes b with - None -> failwith_non_pos_list n ntypes [b] + | None when chkpos -> + failwith_non_pos_list n ntypes [b] + | None -> + check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d | Some b -> - check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) + check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) | Rel k -> (try let (ra,rarg) = List.nth ra_env (k-1) in let largs = List.map (whd_betadeltaiota env) largs in @@ -515,7 +522,8 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as i (** The case where one of the inductives of the mutually inductive block occurs as an argument of another is not known to be safe. So Coq rejects it. *) - if not (List.for_all (noccur_between n ntypes) largs) + if chkpos && + not (List.for_all (noccur_between n ntypes) largs) then failwith_non_pos_list n ntypes largs else (nmr1,rarg) with Failure _ | Invalid_argument _ -> (nmr,mk_norec)) @@ -530,8 +538,9 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as i (** If an inductive of the mutually inductive block appears in any other way, then the positivy check gives up. *) - if noccur_between n ntypes x && - List.for_all (noccur_between n ntypes) largs + if not chkpos || + (noccur_between n ntypes x && + List.for_all (noccur_between n ntypes) largs) then (nmr,mk_norec) else failwith_non_pos_list n ntypes (x::largs) @@ -553,7 +562,7 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as i (** Inductives of the inductive block being defined are only allowed to appear nested in the parameters of another inductive type. Not in the proper indices. *) - if not (List.for_all (noccur_between n ntypes) auxnonrecargs) then + if chkpos && not (List.for_all (noccur_between n ntypes) auxnonrecargs) then failwith_non_pos_list n ntypes auxnonrecargs; (* Nested mutual inductive types are not supported *) let auxntyp = mib.mind_ntypes in @@ -613,7 +622,8 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as i | _ -> raise (IllFormedInd (LocalNotConstructor(paramsctxt,nnonrecargs))) end else - if not (List.for_all (noccur_between n ntypes) largs) + if chkpos && + not (List.for_all (noccur_between n ntypes) largs) then failwith_non_pos_list n ntypes largs in (nmr, List.rev lrec) @@ -633,9 +643,13 @@ let check_positivity_one recursive (env,_,ntypes,_ as ienv) paramsctxt (_,i as i and nmr' = array_min nmr irecargs_nmr in (nmr', mk_paths (Mrec ind) irecargs) -(** [check_positivity kn env_ar paramsctxt inds] checks that the mutually - inductive block [inds] is strictly positive. *) -let check_positivity kn env_ar_par paramsctxt finite inds = +(** [check_positivity ~chkpos kn env_ar paramsctxt inds] checks that the mutually + inductive block [inds] is strictly positive. + + If [chkpos] is [false] then positivity is assumed, and + [check_positivity_one] computes the subterms occurrences in a + best-effort fashion. *) +let check_positivity ~chkpos kn env_ar_par paramsctxt finite inds = let ntypes = Array.length inds in let recursive = finite != Decl_kinds.BiFinite in let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in @@ -647,7 +661,7 @@ let check_positivity kn env_ar_par paramsctxt finite inds = List.init nparamsctxt (fun _ -> (Norec,mk_norec)) @ ra_env_ar in let ienv = (env_ar_par, 1+nparamsctxt, ntypes, ra_env_ar_par) in let nnonrecargs = Context.Rel.nhyps sign - nmr in - check_positivity_one recursive ienv paramsctxt (kn,i) nnonrecargs lcnames lc + check_positivity_one ~chkpos recursive ienv paramsctxt (kn,i) nnonrecargs lcnames lc in let irecargs_nmr = Array.mapi check_one inds in let irecargs = Array.map snd irecargs_nmr @@ -802,7 +816,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params Array.of_list (List.rev kns), Array.of_list (List.rev pbs) -let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs = +let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs is_checked = let ntypes = Array.length inds in (* Compute the set of used section variables *) let hyps = used_section_variables env inds in @@ -908,6 +922,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm mind_polymorphic = p; mind_universes = ctx; mind_private = prv; + mind_checked_positive = is_checked; } (************************************************************************) @@ -916,10 +931,11 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm let check_inductive env kn mie = (* First type-check the inductive definition *) let (env_ar, env_ar_par, paramsctxt, inds) = typecheck_inductive env mie in + let chkpos = mie.mind_entry_check_positivity in (* Then check positivity conditions *) - let (nmr,recargs) = check_positivity kn env_ar_par paramsctxt mie.mind_entry_finite inds in + let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in (* Build the inductive packets *) build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private mie.mind_entry_universes env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite - inds nmr recargs + inds nmr recargs chkpos diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 499cbf0df..24bdaa5c4 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1067,21 +1067,24 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (Array.map fst rv, Array.map snd rv) -let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) = - let (minds, rdef) = inductive_of_mutfix env fix in - let get_tree (kn,i) = - let mib = Environ.lookup_mind kn env in - mib.mind_packets.(i).mind_recargs - in - let trees = Array.map (fun (mind,_) -> get_tree mind) minds in - for i = 0 to Array.length bodies - 1 do - let (fenv,body) = rdef.(i) in - let renv = make_renv fenv nvect.(i) trees.(i) in - try check_one_fix renv nvect trees body - with FixGuardError (fixenv,err) -> - error_ill_formed_rec_body fixenv err names i - (push_rec_types recdef env) (judgment_of_fixpoint recdef) - done +let check_fix env ~flags ((nvect,_),(names,_,bodies as recdef) as fix) = + if flags.check_guarded then + let (minds, rdef) = inductive_of_mutfix env fix in + let get_tree (kn,i) = + let mib = Environ.lookup_mind kn env in + mib.mind_packets.(i).mind_recargs + in + let trees = Array.map (fun (mind,_) -> get_tree mind) minds in + for i = 0 to Array.length bodies - 1 do + let (fenv,body) = rdef.(i) in + let renv = make_renv fenv nvect.(i) trees.(i) in + try check_one_fix renv nvect trees body + with FixGuardError (fixenv,err) -> + error_ill_formed_rec_body fixenv err names i + (push_rec_types recdef env) (judgment_of_fixpoint recdef) + done + else + () (* let cfkey = Profile.declare_profile "check_fix";; @@ -1192,12 +1195,15 @@ let check_one_cofix env nbfix def deftype = (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env (bodynum,(names,types,bodies as recdef)) = - let nbfix = Array.length bodies in - for i = 0 to nbfix-1 do - let fixenv = push_rec_types recdef env in - try check_one_cofix fixenv nbfix bodies.(i) types.(i) - with CoFixGuardError (errenv,err) -> - error_ill_formed_rec_body errenv err names i - fixenv (judgment_of_fixpoint recdef) - done +let check_cofix env ~flags (bodynum,(names,types,bodies as recdef)) = + if flags.check_guarded then + let nbfix = Array.length bodies in + for i = 0 to nbfix-1 do + let fixenv = push_rec_types recdef env in + try check_one_cofix fixenv nbfix bodies.(i) types.(i) + with CoFixGuardError (errenv,err) -> + error_ill_formed_rec_body errenv err names i + fixenv (judgment_of_fixpoint recdef) + done + else + () diff --git a/kernel/inductive.mli b/kernel/inductive.mli index c0d18bc6e..25a557472 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -94,8 +94,11 @@ val inductive_sort_family : one_inductive_body -> sorts_family val check_case_info : env -> pinductive -> case_info -> unit (** {6 Guard conditions for fix and cofix-points. } *) -val check_fix : env -> fixpoint -> unit -val check_cofix : env -> cofixpoint -> unit + +(** When [chk] is false, the guard condition is not actually + checked. *) +val check_fix : env -> flags:typing_flags -> fixpoint -> unit +val check_cofix : env -> flags:typing_flags -> cofixpoint -> unit (** {6 Support for sort-polymorphic inductive types } *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index ce05190b6..72d6ee518 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -373,8 +373,8 @@ let safe_push_named d env = Environ.push_named d env -let push_named_def (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in +let push_named_def ~flags (id,de) senv = + let c,typ,univs = Term_typing.translate_local_def ~flags senv.revstruct senv.env id de in let poly = de.Entries.const_entry_polymorphic in let univs = Univ.ContextSet.of_context univs in let c, univs = match c with @@ -388,9 +388,9 @@ let push_named_def (id,de) senv = let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in univs, {senv' with env=env''} -let push_named_assum ((id,t,poly),ctx) senv = +let push_named_assum ~flags ((id,t,poly),ctx) senv = let senv' = push_context_set poly ctx senv in - let t = Term_typing.translate_local_assum senv'.env t in + let t = Term_typing.translate_local_assum ~flags senv'.env t in let env'' = safe_push_named (LocalAssum (id,t)) senv'.env in {senv' with env=env''} @@ -479,7 +479,7 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) type global_declaration = - | ConstantEntry of bool * private_constants Entries.constant_entry + | ConstantEntry of bool * private_constants Entries.constant_entry * Declarations.typing_flags | GlobalRecipe of Cooking.recipe type exported_private_constant = @@ -512,10 +512,10 @@ let add_constant dir l decl senv = let no_section = DirPath.is_empty dir in let seff_to_export, decl = match decl with - | ConstantEntry (true, ce) -> + | ConstantEntry (true, ce, flags) -> let exports, ce = - Term_typing.export_side_effects senv.revstruct senv.env ce in - exports, ConstantEntry (false, ce) + Term_typing.export_side_effects ~flags senv.revstruct senv.env ce in + exports, ConstantEntry (false, ce, flags) | _ -> [], decl in let senv = @@ -524,8 +524,8 @@ let add_constant dir l decl senv = let senv = let cb = match decl with - | ConstantEntry (export_seff,ce) -> - Term_typing.translate_constant senv.revstruct senv.env kn ce + | ConstantEntry (export_seff,ce,flags) -> + Term_typing.translate_constant ~flags senv.revstruct senv.env kn ce | GlobalRecipe r -> let cb = Term_typing.translate_recipe senv.env kn r in if no_section then Declareops.hcons_const_body cb else cb in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 71dac321f..b614a368c 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -77,19 +77,21 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) val push_named_assum : + flags:Declarations.typing_flags -> (Id.t * Term.types * bool (* polymorphic *)) Univ.in_universe_context_set -> safe_transformer0 (** Returns the full universe context necessary to typecheck the definition (futures are forced) *) val push_named_def : + flags:Declarations.typing_flags -> Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer (** Insertion of global axioms or definitions *) type global_declaration = (* bool: export private constants *) - | ConstantEntry of bool * private_constants Entries.constant_entry + | ConstantEntry of bool * private_constants Entries.constant_entry * Declarations.typing_flags | GlobalRecipe of Cooking.recipe type exported_private_constant = diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 6bfd2457a..8d74dc390 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -22,18 +22,18 @@ open Entries open Typeops open Fast_typeops -let constrain_type env j poly subst = function +let constrain_type ~flags env j poly subst = function | `None -> if not poly then (* Old-style polymorphism *) make_polymorphic_if_constant_for_ind env j else RegularArity (Vars.subst_univs_level_constr subst j.uj_type) | `Some t -> - let tj = infer_type env t in + let tj = infer_type ~flags env t in let _ = judge_of_cast env j DEFAULTcast tj in assert (eq_constr t tj.utj_val); RegularArity (Vars.subst_univs_level_constr subst t) | `SomeWJ (t, tj) -> - let tj = infer_type env t in + let tj = infer_type ~flags env t in let _ = judge_of_cast env j DEFAULTcast tj in assert (eq_constr t tj.utj_val); RegularArity (Vars.subst_univs_level_constr subst t) @@ -171,11 +171,11 @@ let feedback_completion_typecheck = Option.iter (fun state_id -> feedback ~id:(State state_id) Feedback.Complete) -let infer_declaration ~trust env kn dcl = +let infer_declaration ~flags ~trust env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context ~strict:(not poly) uctx env in - let j = infer env t in + let j = infer ~flags env t in let abstract = poly && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract uctx in let c = Typeops.assumption_of_judgment env j in @@ -196,7 +196,7 @@ let infer_declaration ~trust env kn dcl = let env' = push_context_set uctx env in let j = let body,env',ectx = skip_trusted_seff valid_signatures body env' in - let j = infer env' body in + let j = infer ~flags env' body in unzip ectx j in let j = hcons_j j in let subst = Univ.LMap.empty in @@ -220,8 +220,8 @@ let infer_declaration ~trust env kn dcl = let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in - let j = infer env body in - let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in + let j = infer ~flags env body in + let typ = constrain_type ~flags env j c.const_entry_polymorphic usubst (map_option_typ typ) in let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in let def = if opaque then OpaqueDef (Opaqueproof.create (Future.from_val (def, Univ.ContextSet.empty))) @@ -268,7 +268,7 @@ let record_aux env s_ty s_bo suggested_expr = 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 build_constant_declaration ~flags 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 @@ -352,7 +352,9 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_body_code = None; const_polymorphic = poly; const_universes = univs; - const_inline_code = inline_code } + const_inline_code = inline_code; + const_typing_flags = flags; + } in let env = add_constant kn cb env in compile_constant_body env comp_univs def @@ -365,13 +367,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_body_code = tps; const_polymorphic = poly; const_universes = univs; - const_inline_code = inline_code } + const_inline_code = inline_code; + const_typing_flags = flags } (*s Global and local constant declaration. *) -let translate_constant mb env kn ce = - build_constant_declaration kn env - (infer_declaration ~trust:mb env (Some kn) ce) +let translate_constant ~flags mb env kn ce = + build_constant_declaration ~flags kn env + (infer_declaration ~flags ~trust:mb env (Some kn) ce) let constant_entry_of_side_effect cb u = let pt = @@ -406,7 +409,7 @@ type side_effect_role = type exported_side_effect = constant * constant_body * side_effects constant_entry * side_effect_role -let export_side_effects mb env ce = +let export_side_effects ~flags mb env ce = match ce with | ParameterEntry _ | ProjectionEntry _ -> [], ce | DefinitionEntry c -> @@ -447,7 +450,7 @@ let export_side_effects mb env ce = let env, cbs = List.fold_left (fun (env,cbs) (kn, ocb, u, r) -> let ce = constant_entry_of_side_effect ocb u in - let cb = translate_constant mb env kn ce in + let cb = translate_constant ~flags mb env kn ce in (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) (env,[]) cbs in translate_seff sl rest (cbs @ acc) env @@ -462,17 +465,17 @@ let export_side_effects mb env ce = translate_seff trusted seff [] env ;; -let translate_local_assum env t = - let j = infer env t in +let translate_local_assum ~flags env t = + let j = infer ~flags env t in let t = Typeops.assumption_of_judgment env j in t let translate_recipe env kn r = - build_constant_declaration kn env (Cooking.cook_constant env r) + build_constant_declaration ~flags:{check_guarded=true} kn env (Cooking.cook_constant env r) -let translate_local_def mb env id centry = +let translate_local_def ~flags mb env id centry = let def,typ,proj,poly,univs,inline_code,ctx = - infer_declaration ~trust:mb env None (DefinitionEntry centry) in + infer_declaration ~flags ~trust:mb env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin match def with diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index fcd95576c..b635f2d31 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -12,10 +12,10 @@ open Environ open Declarations open Entries -val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry -> +val translate_local_def : flags:typing_flags -> structure_body -> env -> Id.t -> side_effects definition_entry -> constant_def * types * constant_universes -val translate_local_assum : env -> types -> types +val translate_local_assum : flags:typing_flags -> env -> types -> types val mk_pure_proof : constr -> side_effects proof_output @@ -32,7 +32,7 @@ val inline_entry_side_effects : val uniq_seff : side_effects -> side_effects val translate_constant : - structure_body -> env -> constant -> side_effects constant_entry -> + flags:typing_flags -> structure_body -> env -> constant -> side_effects constant_entry -> constant_body type side_effect_role = @@ -47,7 +47,7 @@ type exported_side_effect = * be pushed in the safe_env by safe typing. The main constant entry * needs to be translated as usual after this step. *) val export_side_effects : - structure_body -> env -> side_effects constant_entry -> + flags:typing_flags -> structure_body -> env -> side_effects constant_entry -> exported_side_effect list * side_effects constant_entry val constant_entry_of_side_effect : @@ -60,11 +60,11 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : trust:structure_body -> env -> constant option -> +val infer_declaration : flags:typing_flags -> trust:structure_body -> env -> constant option -> side_effects constant_entry -> Cooking.result val build_constant_declaration : - constant -> env -> Cooking.result -> constant_body + flags:typing_flags -> constant -> env -> Cooking.result -> constant_body val set_suggest_proof_using : (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 0ea68e2bc..a94a049df 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -500,13 +500,13 @@ let rec execute env cstr = | 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; + check_fix ~flags:{check_guarded=true} env fix; make_judge (mkFix 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; + check_cofix ~flags:{check_guarded=true} env cofix; (make_judge (mkCoFix cofix) fix_ty) (* Partial proofs: unsupported by the kernel *) |