From b857552b6ffd5e72b5124aee9e35fc5c14607173 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 16 Jun 2016 17:44:18 +0200 Subject: Adding a default safe set of kernel typing flags to Declareops. --- kernel/declareops.ml | 4 ++++ kernel/declareops.mli | 5 +++++ 2 files changed, 9 insertions(+) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 78e2f386e..28f7e69cd 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -14,6 +14,10 @@ open Context.Rel.Declaration (** Operations concernings types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) +let safe_flags = { + check_guarded = true; +} + (** {6 Arities } *) let subst_decl_arity f g sub ar = diff --git a/kernel/declareops.mli b/kernel/declareops.mli index ad2b5d0a6..6650b6b7b 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -69,6 +69,11 @@ val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_ val inductive_instance : mutual_inductive_body -> universe_instance val inductive_context : mutual_inductive_body -> universe_context +(** {6 Kernel flags} *) + +(** A default, safe set of flags for kernel type-checking *) +val safe_flags : typing_flags + (** {6 Hash-consing} *) (** Here, strictly speaking, we don't perform true hash-consing -- cgit v1.2.3 From 0e2189a7a070dd356d5e549392d35d9d07b05058 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 16 Jun 2016 17:47:44 +0200 Subject: Factorizing the uses of Declareops.safe_flags. This allows a smooth addition of various unsafe flags without wreaking havoc in the ML codebase. --- kernel/term_typing.ml | 2 +- kernel/typeops.ml | 4 ++-- library/declare.ml | 10 +++++----- library/declare.mli | 4 ++-- plugins/funind/indfun.ml | 2 +- pretyping/inductiveops.ml | 4 ++-- pretyping/pretyping.ml | 6 +++--- pretyping/typing.ml | 4 ++-- stm/lemmas.ml | 2 +- toplevel/command.ml | 10 +++++----- toplevel/obligations.ml | 2 +- toplevel/vernacentries.ml | 2 +- 12 files changed, 26 insertions(+), 26 deletions(-) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 8d74dc390..f0c116d27 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -471,7 +471,7 @@ let translate_local_assum ~flags env t = t let translate_recipe env kn r = - build_constant_declaration ~flags:{check_guarded=true} kn env (Cooking.cook_constant env r) + build_constant_declaration ~flags:Declareops.safe_flags kn env (Cooking.cook_constant env r) let translate_local_def ~flags mb env id centry = let def,typ,proj,poly,univs,inline_code,ctx = diff --git a/kernel/typeops.ml b/kernel/typeops.ml index a94a049df..9b9792ce8 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 ~flags:{check_guarded=true} env fix; + check_fix ~flags:Declareops.safe_flags 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 ~flags:{check_guarded=true} env cofix; + check_cofix ~flags:Declareops.safe_flags env cofix; (make_judge (mkCoFix cofix) fix_ty) (* Partial proofs: unsupported by the kernel *) diff --git a/library/declare.ml b/library/declare.ml index 9ec299bed..335263f8f 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -58,11 +58,11 @@ let cache_variable ((sp,_),o) = let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *) | SectionLocalAssum ((ty,ctx),poly,impl) -> - let () = Global.push_named_assum ~flags:{check_guarded=true} ((id,ty,poly),ctx) in + let () = Global.push_named_assum ~flags:Declareops.safe_flags ((id,ty,poly),ctx) in let impl = if impl then Implicit else Explicit in impl, true, poly, ctx | SectionLocalDef (de) -> - let univs = Global.push_named_def ~flags:{check_guarded=true} (id,de) in + let univs = Global.push_named_def ~flags:Declareops.safe_flags (id,de) in Explicit, de.const_entry_opaque, de.const_entry_polymorphic, univs in Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id); @@ -180,7 +180,7 @@ let discharge_constant ((sp, kn), obj) = (* Hack to reduce the size of .vo: we keep only what load/open needs *) let dummy_constant_entry = ConstantEntry - (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), {check_guarded=true}) + (false, ParameterEntry (None,false,(mkProp,Univ.UContext.empty),None), Declareops.safe_flags) let dummy_constant cst = { cst_decl = dummy_constant_entry; @@ -246,7 +246,7 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types const_entry_feedback = None; const_entry_inline_code = inline} -let declare_constant ?(flags={check_guarded=true}) ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = +let declare_constant ?(flags=Declareops.safe_flags) ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) = let export = (* We deal with side effects *) match cd with | DefinitionEntry de when @@ -374,7 +374,7 @@ let declare_projections mind = Array.iteri (fun i kn -> let id = Label.to_id (Constant.label kn) in let entry = {proj_entry_ind = mind; proj_entry_arg = i} in - let kn' = declare_constant ~flags:{check_guarded=true} id (ProjectionEntry entry, + let kn' = declare_constant ~flags:Declareops.safe_flags id (ProjectionEntry entry, IsDefinition StructureComponent) in assert(eq_constant kn kn')) kns; true,true diff --git a/library/declare.mli b/library/declare.mli index 3ba63b5a6..41221d5c9 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -54,11 +54,11 @@ val definition_entry : ?fix_exn:Future.fix_exn -> ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry val declare_constant : - ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *) + ?flags:Declarations.typing_flags -> (** default Declareops.safe_flags *) ?internal:internal_flag -> ?local:bool -> Id.t -> ?export_seff:bool -> constant_declaration -> constant val declare_definition : - ?flags:Declarations.typing_flags -> (** default [check_guarded=true] *) + ?flags:Declarations.typing_flags -> (** default Declareops.safe_flags *) ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind -> ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> constr Univ.in_universe_context_set -> constant diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d8340dddb..8b3d3dc20 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -400,7 +400,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp in evd,List.rev rev_pconstants | _ -> - Command.do_fixpoint ~flags:{Declarations.check_guarded=true} Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; + Command.do_fixpoint ~flags:Declareops.safe_flags Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 0b488308a..1d7720454 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -592,9 +592,9 @@ let type_of_projection_knowing_arg env sigma p c ty = let control_only_guard env c = let check_fix_cofix e c = match kind_of_term c with | CoFix (_,(_,_,_) as cofix) -> - Inductive.check_cofix ~flags:{check_guarded=true} e cofix + Inductive.check_cofix ~flags:Declareops.safe_flags e cofix | Fix (_,(_,_,_) as fix) -> - Inductive.check_fix ~flags:{check_guarded=true} e fix + Inductive.check_fix ~flags:Declareops.safe_flags e fix | _ -> () in let rec iter env c = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c894d96a7..65f5b3fd0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -101,7 +101,7 @@ let search_guard ~tflags loc env possible_indexes fixdefs = will be chosen). A more robust solution may be to raise an error when totality is assumed but the strutural argument is not specified. *) - try check_fix env ~flags:{Declarations.check_guarded=true} fix; raise (Found indexes) + try check_fix env ~flags:Declareops.safe_flags fix; raise (Found indexes) with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in @@ -617,13 +617,13 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let fixdecls = (names,ftys,fdefs) in let indexes = search_guard - ~tflags:{Declarations.check_guarded=true} + ~tflags:Declareops.safe_flags loc env possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env ~flags:{Declarations.check_guarded=true} cofix + (try check_cofix env ~flags:Declareops.safe_flags cofix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 598dd16d0..f03e6c6e9 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -189,13 +189,13 @@ let rec execute env evdref cstr = | Fix ((vn,i as vni),recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let fix = (vni,recdef') in - check_fix env ~flags:{Declarations.check_guarded=true} fix; + check_fix env ~flags:Declareops.safe_flags fix; make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let cofix = (i,recdef') in - check_cofix env ~flags:{Declarations.check_guarded=true} cofix; + check_cofix env ~flags:Declareops.safe_flags cofix; make_judge (mkCoFix cofix) tys.(i) | Sort (Prop c) -> diff --git a/stm/lemmas.ml b/stm/lemmas.ml index b84b1265e..6d84219d9 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -79,7 +79,7 @@ let adjust_guardness_conditions const = function List.fold_left (fun e (_,c,cb,_) -> add c cb e) env l) env (Safe_typing.side_effects_of_private_constants eff) in let indexes = - search_guard ~tflags:{Declarations.check_guarded=true} Loc.ghost env + search_guard ~tflags:Declareops.safe_flags Loc.ghost env possible_indexes fixdecls in (mkFix ((indexes,0),fixdecls), ctx), eff | _ -> (body, ctx), eff) } diff --git a/toplevel/command.ml b/toplevel/command.ml index 6f2dd1bf1..ff43cd495 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -179,7 +179,7 @@ let declare_definition ~flags ident (local, p, k) ce pl imps hook = Lemmas.call_hook fix_exn hook local r let _ = Obligations.declare_definition_ref := - (fun i k c imps hook -> declare_definition ~flags:{Declarations.check_guarded=true} i k c [] imps hook) + (fun i k c imps hook -> declare_definition ~flags:Declareops.safe_flags i k c [] imps hook) let do_definition ident k pl bl red_option c ctypopt hook = let (ce, evd, pl', imps as def) = @@ -203,7 +203,7 @@ let do_definition ident k pl bl red_option c ctypopt hook = ignore(Obligations.add_definition ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in - ignore(declare_definition ~flags:{Declarations.check_guarded=true} ident k ce pl' imps + ignore(declare_definition ~flags:Declareops.safe_flags ident k ce pl' imps (Lemmas.mk_hook (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r))) @@ -838,7 +838,7 @@ let declare_fix ~flags ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),ef declare_definition ~flags f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r)) let _ = Obligations.declare_fix_ref := - (fun ?opaque k ctx f d t imps -> declare_fix ~flags:{Declarations.check_guarded=true} ?opaque k [] ctx f d t imps) + (fun ?opaque k ctx f d t imps -> declare_fix ~flags:Declareops.safe_flags ?opaque k [] ctx f d t imps) let prepare_recursive_declaration fixnames fixtypes fixdefs = let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in @@ -1269,11 +1269,11 @@ let do_program_recursive local p fixkind fixl ntns = in let indexes = Pretyping.search_guard - ~tflags:{Declarations.check_guarded=true} + ~tflags:Declareops.safe_flags Loc.ghost (Global.env ()) possible_indexes fixdecls in List.iteri (fun i _ -> Inductive.check_fix env - ~flags:{Declarations.check_guarded=true} + ~flags:Declareops.safe_flags ((indexes,i),fixdecls)) fixl end in diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 00fd97210..3d15f2142 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -567,7 +567,7 @@ let declare_mutual_definition l = List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes in let indexes = - Pretyping.search_guard ~tflags:{Declarations.check_guarded=true} + Pretyping.search_guard ~tflags:Declareops.safe_flags Loc.ghost (Global.env()) possible_indexes fixdecls in Some indexes, diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 0b4dc0d18..5131a4179 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1731,7 +1731,7 @@ let vernac_load interp fname = try while true do interp (snd (parse_sentence input)) done with End_of_input -> () -let all_checks = { Declarations.check_guarded = true } +let all_checks = Declareops.safe_flags (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands -- cgit v1.2.3