diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/declarations.mli | 13 | ||||
| -rw-r--r-- | kernel/declareops.ml | 2 | ||||
| -rw-r--r-- | kernel/fast_typeops.ml | 68 | ||||
| -rw-r--r-- | kernel/fast_typeops.mli | 7 | ||||
| -rw-r--r-- | kernel/inductive.ml | 8 | ||||
| -rw-r--r-- | kernel/inductive.mli | 4 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 14 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 6 | ||||
| -rw-r--r-- | kernel/term_typing.ml | 34 | ||||
| -rw-r--r-- | kernel/term_typing.mli | 10 | ||||
| -rw-r--r-- | kernel/typeops.ml | 4 |
11 files changed, 91 insertions, 79 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 591a7d404c..0c085df39e 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -64,6 +64,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 = { @@ -75,7 +84,9 @@ type constant_body = { const_universes : constant_universes; const_proj : projection_body option; const_inline_code : bool; - const_checked_guarded : bool; (** [false] is the (co)fixpoint in the constant were assumed to be well-founded. *) + const_typing_flags : typing_flags; (** The typing options which + were used for + type-checking. *) } type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ] diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 068bc498a0..98d2877373 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -133,7 +133,7 @@ let subst_const_body sub cb = const_polymorphic = cb.const_polymorphic; const_universes = cb.const_universes; const_inline_code = cb.const_inline_code; - const_checked_guarded = cb.const_checked_guarded } + const_typing_flags = cb.const_typing_flags } (** {7 Hash-consing of constants } *) diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index 8c14f5e045..32583f531b 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -326,7 +326,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 ~chkguard env cstr = +let rec execute ~flags env cstr = match kind_of_term cstr with (* Atomic terms *) | Sort (Prop c) -> @@ -345,12 +345,12 @@ let rec execute ~chkguard env cstr = judge_of_constant env c | Proj (p, c) -> - let ct = execute ~chkguard 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 ~chkguard 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 -> @@ -363,7 +363,7 @@ let rec execute ~chkguard env cstr = judge_of_constant_knowing_parameters env cst args | _ -> (* Full or no sort-polymorphism *) - execute ~chkguard env f + execute ~flags env f in judge_of_apply env f ft args argst @@ -371,25 +371,25 @@ let rec execute ~chkguard env cstr = | Lambda (name,c1,c2) -> let _ = execute_is_type env c1 in let env1 = push_rel (name,None,c1) env in - let c2t = execute ~chkguard 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 ~chkguard env c1 in + let vars = execute_is_type ~flags env c1 in let env1 = push_rel (name,None,c1) env in - let vars' = execute_is_type ~chkguard 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 ~chkguard 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 (name,Some c1,c2) env in - let c3t = execute ~chkguard env1 c3 in + let c3t = execute ~flags env1 c3 in subst1 c1 c3t | Cast (c,k,t) -> - let ct = execute ~chkguard 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 @@ -402,20 +402,20 @@ let rec execute ~chkguard env cstr = judge_of_constructor env c | Case (ci,p,c,lf) -> - let ct = execute ~chkguard env c in - let pt = execute ~chkguard env p in - let lft = execute_array ~chkguard 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 ~chkguard env recdef i in + let (fix_ty,recdef') = execute_recdef ~flags env recdef i in let fix = (vni,recdef') in - check_fix env ~chk:chkguard fix; fix_ty + check_fix env ~flags fix; fix_ty | CoFix (i,recdef) -> - let (fix_ty,recdef') = execute_recdef ~chkguard env recdef i in + let (fix_ty,recdef') = execute_recdef ~flags env recdef i in let cofix = (i,recdef') in - check_cofix env ~chk:chkguard cofix; fix_ty + check_cofix env ~flags cofix; fix_ty (* Partial proofs: unsupported by the kernel *) | Meta _ -> @@ -424,41 +424,41 @@ let rec execute ~chkguard env cstr = | Evar _ -> anomaly (Pp.str "the kernel does not support existential variables") -and execute_is_type ~chkguard env constr = - let t = execute ~chkguard 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 ~chkguard env constr = - let t = execute ~chkguard env constr in +and execute_type ~flags env constr = + let t = execute ~flags env constr in type_judgment env constr t -and execute_recdef ~chkguard env (names,lar,vdef) i = - let lart = execute_array ~chkguard 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 ~chkguard 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 ~chkguard env = Array.map (execute ~chkguard env) +and execute_array ~flags env = Array.map (execute ~flags env) (* Derived functions *) -let infer ~chkguard env constr = - let t = execute ~chkguard 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.profile3 infer_key (fun a b c -> infer ~chkguard:a b c) - else (fun a b c -> infer ~chkguard:a b c) + Profile.profile3 infer_key (fun a b c -> infer ~flags:a b c) + else (fun a b c -> infer ~flags:a b c) (* Restores the labels of [infer] lost to profiling. *) -let infer ~chkguard env t = infer chkguard env t +let infer ~flags env t = infer flags env t -let infer_type ~chkguard env constr = - execute_type ~chkguard env constr +let infer_type ~flags env constr = + execute_type ~flags env constr -let infer_v ~chkguard env cv = - let jv = execute_array ~chkguard env cv in +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 98dbefad13..1c0146baea 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 : chkguard:bool -> env -> constr -> unsafe_judgment -val infer_v : chkguard:bool -> env -> constr array -> unsafe_judgment array -val infer_type : chkguard:bool -> 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/inductive.ml b/kernel/inductive.ml index 532287c304..fdca5ce26b 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1065,8 +1065,8 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (Array.map fst rv, Array.map snd rv) -let check_fix env ~chk ((nvect,_),(names,_,bodies as recdef) as fix) = - if chk then +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 @@ -1193,8 +1193,8 @@ 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 ~chk (bodynum,(names,types,bodies as recdef)) = - if chk then +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 diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 36f32b30c6..54036d86aa 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -98,8 +98,8 @@ val check_case_info : env -> pinductive -> case_info -> unit (** When [chk] is false, the guard condition is not actually checked. *) -val check_fix : env -> chk:bool -> fixpoint -> unit -val check_cofix : env -> chk:bool -> cofixpoint -> unit +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 18d8978174..2cea50d9ec 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -332,8 +332,8 @@ let safe_push_named (id,_,_ as d) env = Environ.push_named d env -let push_named_def ~chkguard (id,de) senv = - let c,typ,univs = Term_typing.translate_local_def ~chkguard senv.env id de in +let push_named_def ~flags (id,de) senv = + let c,typ,univs = Term_typing.translate_local_def ~flags senv.env id de in let senv' = push_context univs senv in let c, senv' = match c with | Def c -> Mod_subst.force_constr c, senv' @@ -346,9 +346,9 @@ let push_named_def ~chkguard (id,de) senv = let env'' = safe_push_named (id,Some c,typ) senv'.env in {senv' with env=env''} -let push_named_assum ~chkguard ((id,t),ctx) senv = +let push_named_assum ~flags ((id,t),ctx) senv = let senv' = push_context_set ctx senv in - let t = Term_typing.translate_local_assum ~chkguard senv'.env t in + let t = Term_typing.translate_local_assum ~flags senv'.env t in let env'' = safe_push_named (id,None,t) senv'.env in {senv' with env=env''} @@ -439,14 +439,14 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver } (** Insertion of constants and parameters in environment *) type global_declaration = - | ConstantEntry of Entries.constant_entry * bool (* check guard *) + | ConstantEntry of Entries.constant_entry * Declarations.typing_flags | GlobalRecipe of Cooking.recipe let add_constant dir l decl senv = let kn = make_con senv.modpath dir l in let cb = match decl with - | ConstantEntry (ce,chkguard) -> - Term_typing.translate_constant ~chkguard senv.env kn ce + | ConstantEntry (ce,flags) -> + Term_typing.translate_constant ~flags senv.env kn ce | GlobalRecipe r -> let cb = Term_typing.translate_recipe senv.env kn r in if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 80b9bb495a..c5e43e42ac 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -57,16 +57,16 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) val push_named_assum : - chkguard:bool -> + flags:Declarations.typing_flags -> (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0 val push_named_def : - chkguard:bool -> + flags:Declarations.typing_flags -> Id.t * Entries.definition_entry -> safe_transformer0 (** Insertion of global axioms or definitions *) type global_declaration = - | ConstantEntry of Entries.constant_entry * bool (* chkguard *) + | ConstantEntry of Entries.constant_entry * Declarations.typing_flags | GlobalRecipe of Cooking.recipe val add_constant : diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 8a105ac971..64597469a8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -23,18 +23,18 @@ open Entries open Typeops open Fast_typeops -let constrain_type ~chkguard 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 ~chkguard 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 ~chkguard 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) @@ -101,11 +101,11 @@ let hcons_j j = let feedback_completion_typecheck = Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete) -let infer_declaration ~chkguard env kn dcl = +let infer_declaration ~flags env kn dcl = match dcl with | ParameterEntry (ctx,poly,(t,uctx),nl) -> let env = push_context uctx env in - let j = infer ~chkguard 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 @@ -122,7 +122,7 @@ let infer_declaration ~chkguard env kn dcl = Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) -> let body = handle_side_effects env body side_eff in let env' = push_context_set ctx env in - let j = infer ~chkguard env' body in + let j = infer ~flags env' body in let j = hcons_j j in let subst = Univ.LMap.empty in let _typ = constrain_type env' j c.const_entry_polymorphic subst @@ -143,8 +143,8 @@ let infer_declaration ~chkguard env kn dcl = let body = handle_side_effects env body side_eff in let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in - let j = infer ~chkguard env body in - let typ = constrain_type ~chkguard 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))) @@ -186,7 +186,7 @@ let record_aux env s1 s2 = let suggest_proof_using = ref (fun _ _ _ _ _ -> ()) let set_suggest_proof_using f = suggest_proof_using := f -let build_constant_declaration ~chkguard 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 check declared inferred = let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in @@ -262,25 +262,25 @@ let build_constant_declaration ~chkguard kn env (def,typ,proj,poly,univs,inline_ const_polymorphic = poly; const_universes = univs; const_inline_code = inline_code; - const_checked_guarded = chkguard } + const_typing_flags = flags } (*s Global and local constant declaration. *) -let translate_constant ~chkguard env kn ce = - build_constant_declaration ~chkguard kn env (infer_declaration ~chkguard env (Some kn) ce) +let translate_constant ~flags env kn ce = + build_constant_declaration ~flags kn env (infer_declaration ~flags env (Some kn) ce) -let translate_local_assum ~chkguard env t = - let j = infer ~chkguard 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 ~chkguard:true 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 ~chkguard env id centry = +let translate_local_def ~flags env id centry = let def,typ,proj,poly,univs,inline_code,ctx = - infer_declaration ~chkguard env None (DefinitionEntry centry) in + infer_declaration ~flags env None (DefinitionEntry centry) in let typ = type_of_constant_type env typ in def, typ, univs diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index ba4d96a5f0..f167603a79 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 : chkguard:bool -> env -> Id.t -> definition_entry -> +val translate_local_def : flags:typing_flags -> env -> Id.t -> definition_entry -> constant_def * types * constant_universes -val translate_local_assum : chkguard:bool -> env -> types -> types +val translate_local_assum : flags:typing_flags -> env -> types -> types val mk_pure_proof : constr -> proof_output @@ -28,7 +28,7 @@ val handle_entry_side_effects : env -> definition_entry -> definition_entry {!Entries.const_entry_body} field. It is meant to get a term out of a not yet type checked proof. *) -val translate_constant : chkguard:bool -> env -> constant -> constant_entry -> constant_body +val translate_constant : flags:typing_flags -> env -> constant -> constant_entry -> constant_body val translate_mind : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body @@ -37,11 +37,11 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body (** Internal functions, mentioned here for debug purpose only *) -val infer_declaration : chkguard:bool -> env -> constant option -> +val infer_declaration : flags:typing_flags -> env -> constant option -> constant_entry -> Cooking.result val build_constant_declaration : - chkguard:bool -> constant -> env -> Cooking.result -> constant_body + flags:typing_flags -> constant -> env -> Cooking.result -> constant_body val set_suggest_proof_using : (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 9e9f18aaa9..1c3117725c 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -494,13 +494,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 ~chk:true 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 ~chk:true env cofix; + check_cofix ~flags:{check_guarded=true} env cofix; (make_judge (mkCoFix cofix) fix_ty) (* Partial proofs: unsupported by the kernel *) |