From 245b94cd075b6be527590c425a98262d89577909 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 Mar 2020 11:29:40 +0100 Subject: Hack a non-superglobal mode for hints. The current implementation was seemingly never thought for this kind of semantics. Everything is superglobal by construction, notably hint database creation and naming schemes. The new mode feels a bit hackish to me, at some point this should be fully reimplemented from scratch with a clear design in mind. --- plugins/ltac/g_auto.mlg | 2 +- pretyping/typeclasses.ml | 3 --- pretyping/typeclasses.mli | 3 --- tactics/hints.ml | 51 +++++++++++++++++++++++++++-------------------- tactics/hints.mli | 2 +- vernac/classes.ml | 20 +++++++++---------- vernac/declareObl.ml | 2 +- vernac/obligations.ml | 6 +++--- vernac/record.ml | 2 +- vernac/vernacentries.ml | 2 +- 10 files changed, 47 insertions(+), 46 deletions(-) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 82c64a9857..336c5a4bb0 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -249,7 +249,7 @@ END VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF | #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints ~local:(Locality.make_section_locality locality) + Hints.add_hints ~local:(Locality.make_section_locality locality) ~superglobal:true (match dbnames with None -> ["core"] | Some l -> l) entry; } END diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index aa2e96c2d7..d4f59d7a36 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -34,9 +34,6 @@ let get_typeclasses_unique_solutions = ~key:["Typeclasses";"Unique";"Solutions"] ~value:false -let (set_typeclass_transparency, set_typeclass_transparency_hook) = Hook.make () -let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency gr local c - let (classes_transparent_state, classes_transparent_state_hook) = Hook.make () let classes_transparent_state () = Hook.get classes_transparent_state () diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 2715c1eda5..c350f97107 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -122,9 +122,6 @@ val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool -> ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> evar_map * EConstr.constr -val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t -val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit - val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t val classes_transparent_state : unit -> TransparentState.t diff --git a/tactics/hints.ml b/tactics/hints.ml index e9ed43e3de..8b81b36fa2 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1031,7 +1031,7 @@ let remove_hint dbname grs = type hint_action = | CreateDB of bool * TransparentState.t | AddTransparency of evaluable_global_reference hints_transparency_target * bool - | AddHints of hint_entry list + | AddHints of { superglobal : bool; hints : hint_entry list } | RemoveHints of GlobRef.t list | AddCut of hints_path | AddMode of GlobRef.t * hint_mode array @@ -1057,14 +1057,21 @@ let load_autohint _ (kn, h) = match h.hint_action with | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty ~name st b) | AddTransparency (grs, b) -> add_transparency name grs b - | AddHints hints -> add_hint name hints + | AddHints { superglobal; hints } -> + if superglobal then add_hint name hints | RemoveHints grs -> remove_hint name grs | AddCut path -> add_cut name path | AddMode (l, m) -> add_mode name l m let open_autohint i (kn, h) = if Int.equal i 1 then match h.hint_action with - | AddHints hints -> + | AddHints { superglobal; hints } -> + let () = + if not superglobal then + (* Import-bound hints must be declared when not imported yet *) + let filter (_, h) = not @@ KNmap.mem h.code.uid !statustable in + add_hint h.hint_name (List.filter filter hints) + in let add (_, hint) = statustable := KNmap.add hint.code.uid true !statustable in List.iter add hints | _ -> () @@ -1133,9 +1140,9 @@ let subst_autohint (subst, obj) = else HintsReferences grs' in if target' == target then obj.hint_action else AddTransparency (target', b) - | AddHints hintlist -> - let hintlist' = List.Smart.map subst_hint hintlist in - if hintlist' == hintlist then obj.hint_action else AddHints hintlist' + | AddHints { superglobal; hints } -> + let hints' = List.Smart.map subst_hint hints in + if hints' == hints then obj.hint_action else AddHints { superglobal; hints = hints' } | RemoveHints grs -> let grs' = List.Smart.map (subst_global_reference subst) grs in if grs == grs' then obj.hint_action else RemoveHints grs' @@ -1150,7 +1157,7 @@ let subst_autohint (subst, obj) = let classify_autohint obj = match obj.hint_action with - | AddHints [] -> Dispose + | AddHints { hints = [] } -> Dispose | _ -> if obj.hint_local then Dispose else Substitute obj let inAutoHint : hint_obj -> obj = @@ -1182,7 +1189,7 @@ let remove_hints local dbnames grs = (**************************************************************************) (* The "Hint" vernacular command *) (**************************************************************************) -let add_resolves env sigma clist local dbnames = +let add_resolves env sigma clist ~local ~superglobal dbnames = List.iter (fun dbname -> let r = @@ -1190,14 +1197,14 @@ let add_resolves env sigma clist local dbnames = make_resolves env sigma (true,hnf,not !Flags.quiet) pri ~poly ~name:path gr) clist) in - let hint = make_hint ~local dbname (AddHints r) in + let hint = make_hint ~local dbname (AddHints { superglobal; hints = r }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_unfolds l local dbnames = +let add_unfolds l ~local ~superglobal dbnames = List.iter (fun dbname -> - let hint = make_hint ~local dbname (AddHints (List.map make_unfold l)) in + let hint = make_hint ~local dbname (AddHints { superglobal; hints = List.map make_unfold l }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames @@ -1223,23 +1230,23 @@ let add_transparency l b local dbnames = Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_extern info tacast local dbname = +let add_extern info tacast ~local ~superglobal dbname = let pat = match info.hint_pattern with | None -> None | Some (_, pat) -> Some pat in let hint = make_hint ~local dbname - (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in + (AddHints { superglobal; hints = [make_extern (Option.get info.hint_priority) pat tacast] }) in Lib.add_anonymous_leaf (inAutoHint hint) -let add_externs info tacast local dbnames = - List.iter (add_extern info tacast local) dbnames +let add_externs info tacast ~local ~superglobal dbnames = + List.iter (add_extern info tacast ~local ~superglobal) dbnames -let add_trivials env sigma l local dbnames = +let add_trivials env sigma l ~local ~superglobal dbnames = List.iter (fun dbname -> let l = List.map (fun (name, poly, c) -> make_trivial env sigma poly ~name c) l in - let hint = make_hint ~local dbname (AddHints l) in + let hint = make_hint ~local dbname (AddHints { superglobal; hints = l }) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames @@ -1403,22 +1410,22 @@ let interp_hints ~poly = let _, tacexp = Genintern.generic_intern env tacexp in HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp) -let add_hints ~local dbnames h = +let add_hints ~local ~superglobal dbnames h = if String.List.mem "nocore" dbnames then user_err Pp.(str "The hint database \"nocore\" is meant to stay empty."); assert (not (List.is_empty dbnames)); let env = Global.env() in let sigma = Evd.from_env env in match h with - | HintsResolveEntry lhints -> add_resolves env sigma lhints local dbnames - | HintsImmediateEntry lhints -> add_trivials env sigma lhints local dbnames + | HintsResolveEntry lhints -> add_resolves env sigma lhints ~local ~superglobal dbnames + | HintsImmediateEntry lhints -> add_trivials env sigma lhints ~local ~superglobal dbnames | HintsCutEntry lhints -> add_cuts lhints local dbnames | HintsModeEntry (l,m) -> add_mode l m local dbnames - | HintsUnfoldEntry lhints -> add_unfolds lhints local dbnames + | HintsUnfoldEntry lhints -> add_unfolds lhints ~local ~superglobal dbnames | HintsTransparencyEntry (lhints, b) -> add_transparency lhints b local dbnames | HintsExternEntry (info, tacexp) -> - add_externs info tacexp local dbnames + add_externs info tacexp ~local ~superglobal dbnames let expand_constructor_hints env sigma lems = List.map_append (fun (evd,lem) -> diff --git a/tactics/hints.mli b/tactics/hints.mli index 2663f65851..3fd4d6ea9e 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -219,7 +219,7 @@ val current_pure_db : unit -> hint_db list val interp_hints : poly:bool -> hints_expr -> hints_entry -val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit +val add_hints : local:bool -> superglobal:bool -> hint_db_name list -> hints_entry -> unit val prepare_hint : bool (* Check no remaining evars *) -> env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t) diff --git a/vernac/classes.ml b/vernac/classes.ml index 16b9e07fb2..ee27a9f58b 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -29,7 +29,8 @@ module NamedDecl = Context.Named.Declaration (*i*) let set_typeclass_transparency c local b = - Hints.add_hints ~local [typeclasses_db] + let superglobal = true in + Hints.add_hints ~local ~superglobal [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) let classes_transparent_state () = @@ -38,12 +39,11 @@ let classes_transparent_state () = with Not_found -> TransparentState.empty let () = - Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency; Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state -let add_instance_hint inst path local info poly = +let add_instance_hint inst path ~local ~superglobal info poly = Flags.silently (fun () -> - Hints.add_hints ~local [typeclasses_db] + Hints.add_hints ~local ~superglobal [typeclasses_db] (Hints.HintsResolveEntry [info, poly, false, Hints.PathHints path, inst])) () @@ -55,16 +55,16 @@ let is_local_for_hint i = add_instance_hint; don't ask hints to take discharge into account itself *) -let add_instance check inst = +let add_instance_base inst = let poly = Global.is_polymorphic inst.is_impl in let local = is_local_for_hint inst in - add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] local + add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~local ~superglobal:true inst.is_info poly; List.iter (fun (path, pri, c) -> let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in add_instance_hint h path - local pri poly) - (build_subclasses ~check:(check && not (isVarRef inst.is_impl)) + ~local ~superglobal:true pri poly) + (build_subclasses ~check:(not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) let mk_instance cl info glob impl = @@ -104,7 +104,7 @@ let discharge_instance (_, inst) = let is_local i = (i.is_global == None) let rebuild_instance inst = - add_instance true inst; + add_instance_base inst; inst let classify_instance inst = @@ -124,7 +124,7 @@ let instance_input : instance -> obj = let add_instance i = Lib.add_anonymous_leaf (instance_input i); - add_instance true i + add_instance_base i let warning_not_a_class = let name = "not-a-class" in diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index eb9b896ec6..527c6e24c8 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -123,7 +123,7 @@ let shrink_body c ty = let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] let add_hint local prg cst = - Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) + Hints.add_hints ~local ~superglobal:false [Id.to_string prg.prg_name] (unfold_entry cst) (***********************************************************************) (* Saving an obligation *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 27eb821a6a..7ce2d2a49c 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -295,8 +295,8 @@ open Evd let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] -let add_hint local prg cst = - Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst) +let add_local_hint prg cst = + Hints.add_hints ~local:true ~superglobal:false [Id.to_string prg.prg_name] (unfold_entry cst) let init_prog_info ?(opaque = false) ?hook n udecl b t ctx deps fixkind notations obls impls ~scope ~poly ~kind reduce = @@ -461,7 +461,7 @@ let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } Univ.UContext.instance uctx, ctx' in let obl = { obl with obl_body = Some (DefinedObl (cst, inst)) } in - let () = if transparent then add_hint true prg cst in + let () = if transparent then add_local_hint prg cst in let obls = Array.copy obls in let () = obls.(num) <- obl in let prg = { prg with prg_ctx = ctx' } in diff --git a/vernac/record.ml b/vernac/record.ml index 065641989d..75e1088108 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -613,7 +613,7 @@ let add_constant_class env sigma cst = } in Classes.add_class env sigma tc; - set_typeclass_transparency (EvalConstRef cst) false false + Classes.set_typeclass_transparency (EvalConstRef cst) false false let add_inductive_class env sigma ind = let mind, oneind = Inductive.lookup_mind_specif env ind in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c78b470e3b..be6ffa07b9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1180,7 +1180,7 @@ let vernac_hints ~atts dbnames h = in let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in let local = enforce_module_locality local in - Hints.add_hints ~local dbnames (Hints.interp_hints ~poly h) + Hints.add_hints ~local ~superglobal:true dbnames (Hints.interp_hints ~poly h) let vernac_syntactic_definition ~atts lid x only_parsing = let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in -- cgit v1.2.3 From 96ec58df041dc0111df0e681269aed9d0e9b571a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Mar 2020 15:11:35 +0100 Subject: Use a 3-valued flag for hint locality. We reuse the same type as for options, even though it is a bit ill-named. At least it allows to share code with it. --- plugins/ltac/g_auto.mlg | 3 ++- tactics/hints.ml | 7 ++++++- tactics/hints.mli | 2 +- vernac/classes.ml | 14 +++++++------- vernac/declareObl.ml | 3 ++- vernac/obligations.ml | 2 +- vernac/vernacentries.ml | 3 ++- 7 files changed, 21 insertions(+), 13 deletions(-) diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 336c5a4bb0..c43018022e 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -249,7 +249,8 @@ END VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF | #[ locality = Attributes.locality; ] [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints ~local:(Locality.make_section_locality locality) ~superglobal:true + let locality = if Locality.make_section_locality locality then Goptions.OptLocal else Goptions.OptGlobal in + Hints.add_hints ~locality (match dbnames with None -> ["core"] | Some l -> l) entry; } END diff --git a/tactics/hints.ml b/tactics/hints.ml index 8b81b36fa2..7cde342662 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1410,7 +1410,12 @@ let interp_hints ~poly = let _, tacexp = Genintern.generic_intern env tacexp in HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp) -let add_hints ~local ~superglobal dbnames h = +let add_hints ~locality dbnames h = + let local, superglobal = match locality with + | Goptions.OptDefault | Goptions.OptGlobal -> false, true + | Goptions.OptExport -> false, false + | Goptions.OptLocal -> true, false + in if String.List.mem "nocore" dbnames then user_err Pp.(str "The hint database \"nocore\" is meant to stay empty."); assert (not (List.is_empty dbnames)); diff --git a/tactics/hints.mli b/tactics/hints.mli index 3fd4d6ea9e..c9d4231d77 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -219,7 +219,7 @@ val current_pure_db : unit -> hint_db list val interp_hints : poly:bool -> hints_expr -> hints_entry -val add_hints : local:bool -> superglobal:bool -> hint_db_name list -> hints_entry -> unit +val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit val prepare_hint : bool (* Check no remaining evars *) -> env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t) diff --git a/vernac/classes.ml b/vernac/classes.ml index ee27a9f58b..99c92604ba 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -29,8 +29,8 @@ module NamedDecl = Context.Named.Declaration (*i*) let set_typeclass_transparency c local b = - let superglobal = true in - Hints.add_hints ~local ~superglobal [typeclasses_db] + let locality = if local then Goptions.OptLocal else Goptions.OptGlobal in + Hints.add_hints ~locality [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) let classes_transparent_state () = @@ -41,9 +41,9 @@ let classes_transparent_state () = let () = Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state -let add_instance_hint inst path ~local ~superglobal info poly = +let add_instance_hint inst path ~locality info poly = Flags.silently (fun () -> - Hints.add_hints ~local ~superglobal [typeclasses_db] + Hints.add_hints ~locality [typeclasses_db] (Hints.HintsResolveEntry [info, poly, false, Hints.PathHints path, inst])) () @@ -57,13 +57,13 @@ let is_local_for_hint i = let add_instance_base inst = let poly = Global.is_polymorphic inst.is_impl in - let local = is_local_for_hint inst in - add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~local ~superglobal:true + let locality = if is_local_for_hint inst then Goptions.OptLocal else Goptions.OptGlobal in + add_instance_hint (Hints.IsGlobRef inst.is_impl) [inst.is_impl] ~locality inst.is_info poly; List.iter (fun (path, pri, c) -> let h = Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty) [@ocaml.warning "-3"] in add_instance_hint h path - ~local ~superglobal:true pri poly) + ~locality pri poly) (build_subclasses ~check:(not (isVarRef inst.is_impl)) (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info) diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index 527c6e24c8..c973c84827 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -123,7 +123,8 @@ let shrink_body c ty = let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] let add_hint local prg cst = - Hints.add_hints ~local ~superglobal:false [Id.to_string prg.prg_name] (unfold_entry cst) + let locality = if local then Goptions.OptLocal else Goptions.OptExport in + Hints.add_hints ~locality [Id.to_string prg.prg_name] (unfold_entry cst) (***********************************************************************) (* Saving an obligation *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 7ce2d2a49c..dd90af0223 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -296,7 +296,7 @@ open Evd let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst] let add_local_hint prg cst = - Hints.add_hints ~local:true ~superglobal:false [Id.to_string prg.prg_name] (unfold_entry cst) + Hints.add_hints ~locality:Goptions.OptLocal [Id.to_string prg.prg_name] (unfold_entry cst) let init_prog_info ?(opaque = false) ?hook n udecl b t ctx deps fixkind notations obls impls ~scope ~poly ~kind reduce = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index be6ffa07b9..c4027c6598 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1180,7 +1180,8 @@ let vernac_hints ~atts dbnames h = in let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in let local = enforce_module_locality local in - Hints.add_hints ~local ~superglobal:true dbnames (Hints.interp_hints ~poly h) + let locality = if local then OptLocal else OptGlobal in + Hints.add_hints ~locality dbnames (Hints.interp_hints ~poly h) let vernac_syntactic_definition ~atts lid x only_parsing = let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in -- cgit v1.2.3 From d583f810be066929301864765601ff53497bc335 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Mar 2020 15:31:26 +0100 Subject: Export the user-facing attribute for hint locality. --- tactics/hints.ml | 21 +++++++++++++++------ test-suite/success/export_hint.v | 22 ++++++++++++++++++++++ vernac/attributes.ml | 10 ++++++++++ vernac/attributes.mli | 1 + vernac/vernacentries.ml | 15 ++++++++++++--- 5 files changed, 60 insertions(+), 9 deletions(-) create mode 100644 test-suite/success/export_hint.v diff --git a/tactics/hints.ml b/tactics/hints.ml index 7cde342662..9c0cf03854 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1189,6 +1189,12 @@ let remove_hints local dbnames grs = (**************************************************************************) (* The "Hint" vernacular command *) (**************************************************************************) + +let check_no_export ~local ~superglobal () = + (* TODO: implement export for these entries *) + if not local && not superglobal then + CErrors.user_err Pp.(str "This command does not support the \"export\" attribute") + let add_resolves env sigma clist ~local ~superglobal dbnames = List.iter (fun dbname -> @@ -1208,14 +1214,16 @@ let add_unfolds l ~local ~superglobal dbnames = Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_cuts l local dbnames = +let add_cuts l ~local ~superglobal dbnames = + let () = check_no_export ~local ~superglobal () in List.iter (fun dbname -> let hint = make_hint ~local dbname (AddCut l) in Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_mode l m local dbnames = +let add_mode l m ~local ~superglobal dbnames = + let () = check_no_export ~local ~superglobal () in List.iter (fun dbname -> let m' = make_mode l m in @@ -1223,7 +1231,8 @@ let add_mode l m local dbnames = Lib.add_anonymous_leaf (inAutoHint hint)) dbnames -let add_transparency l b local dbnames = +let add_transparency l b ~local ~superglobal dbnames = + let () = check_no_export ~local ~superglobal () in List.iter (fun dbname -> let hint = make_hint ~local dbname (AddTransparency (l, b)) in @@ -1424,11 +1433,11 @@ let add_hints ~locality dbnames h = match h with | HintsResolveEntry lhints -> add_resolves env sigma lhints ~local ~superglobal dbnames | HintsImmediateEntry lhints -> add_trivials env sigma lhints ~local ~superglobal dbnames - | HintsCutEntry lhints -> add_cuts lhints local dbnames - | HintsModeEntry (l,m) -> add_mode l m local dbnames + | HintsCutEntry lhints -> add_cuts lhints ~local ~superglobal dbnames + | HintsModeEntry (l,m) -> add_mode l m ~local ~superglobal dbnames | HintsUnfoldEntry lhints -> add_unfolds lhints ~local ~superglobal dbnames | HintsTransparencyEntry (lhints, b) -> - add_transparency lhints b local dbnames + add_transparency lhints b ~local ~superglobal dbnames | HintsExternEntry (info, tacexp) -> add_externs info tacexp ~local ~superglobal dbnames diff --git a/test-suite/success/export_hint.v b/test-suite/success/export_hint.v new file mode 100644 index 0000000000..e18f7c1bef --- /dev/null +++ b/test-suite/success/export_hint.v @@ -0,0 +1,22 @@ +Create HintDb foo. + +Module Foo. + +Axiom F : False. + +#[export] +Hint Immediate F : foo. + +End Foo. + +Goal False. +Proof. +Fail solve [auto with foo]. +Abort. + +Import Foo. + +Goal False. +Proof. +auto with foo. +Qed. diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 7213ba4829..96f126503d 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -163,6 +163,16 @@ let program = let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global" +let option_locality = + let name = "Locality" in + attribute_of_list [ + ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal); + ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal); + ("export", single_key_parser ~name ~key:"export" Goptions.OptExport); + ] >>= function + | None -> return Goptions.OptDefault + | Some l -> return l + let ukey = "universes" let universe_polymorphism_option_name = ["Universe"; "Polymorphism"] diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 7ecb7e4fb0..660652081f 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -47,6 +47,7 @@ val polymorphic : bool attribute val program : bool attribute val template : bool option attribute val locality : bool option attribute +val option_locality : Goptions.option_locality attribute val deprecation : Deprecation.t option attribute val canonical_field : bool attribute val canonical_instance : bool attribute diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c4027c6598..ba6d869589 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1178,9 +1178,18 @@ let vernac_hints ~atts dbnames h = (warn_implicit_core_hint_db (); ["core"]) else dbnames in - let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in - let local = enforce_module_locality local in - let locality = if local then OptLocal else OptGlobal in + let locality, poly = Attributes.(parse Notations.(option_locality ++ polymorphic) atts) in + let () = match locality with + | OptGlobal -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the global attribute in sections."); + | OptExport -> + if Global.sections_are_opened () then + CErrors.user_err Pp.(str + "This command does not support the export attribute in sections."); + | OptDefault | OptLocal -> () + in Hints.add_hints ~locality dbnames (Hints.interp_hints ~poly h) let vernac_syntactic_definition ~atts lid x only_parsing = -- cgit v1.2.3 From 7b124ee24aa6ebaf14c5f7019949a7c2a877dedb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Mar 2020 16:24:27 +0100 Subject: Add documentation for the export hint. --- .../11812-export-hint-globality.rst | 5 +++++ doc/sphinx/proof-engine/tactics.rst | 25 ++++++++++++++++------ doc/sphinx/proof-engine/vernacular-commands.rst | 6 ++++++ 3 files changed, 29 insertions(+), 7 deletions(-) create mode 100644 doc/changelog/07-commands-and-options/11812-export-hint-globality.rst diff --git a/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst b/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst new file mode 100644 index 0000000000..9341eebb58 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11812-export-hint-globality.rst @@ -0,0 +1,5 @@ +- **Added:** + the :cmd:`Hint` commands now accept the :attr:`export` locality as + an attribute, allowing to make import-scoped hints + (`#11812 `_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 4f2f74aae4..be185e885b 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3759,6 +3759,24 @@ automatically created. .. cmd:: Hint @hint_definition : {+ @ident} The general command to add a hint to some databases :n:`{+ @ident}`. + + This command supports the :attr:`local`, :attr:`global` and :attr:`export` + locality attributes. When no locality is explictly given, the + command is :attr:`local` inside a section and :attr:`global` otherwise. + + + :attr:`local` hints are never visible from other modules, even if they + require or import the current module. Inside a section, the :attr:`local` + attribute is useless since hints do not survive anyway to the closure of + sections. + + + :attr:`export` are visible from other modules when they import the current + module. Requiring it is not enough. This attribute is only effective for + the :cmd:`Hint Resolve`, :cmd:`Hint Immediate`, :cmd:`Hint Unfold` and + :cmd:`Hint Extern` variants of the command. + + + :attr:`global` hints are made available by merely requiring the current + module. + The various possible :production:`hint_definition`\s are given below. .. cmdv:: Hint @hint_definition @@ -3767,13 +3785,6 @@ automatically created. .. deprecated:: 8.10 - .. cmdv:: Local Hint @hint_definition : {+ @ident} - - This is used to declare hints that must not be exported to the other modules - that require and import the current module. Inside a section, the flag - Local is useless since hints do not survive anyway to the closure of - sections. - .. cmdv:: Hint Resolve @qualid {? | {? @num} {? @pattern}} : @ident :name: Hint Resolve diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index d1f3dcc309..4401f8fa2f 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1190,6 +1190,12 @@ Controlling the locality of commands occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. +.. attr:: export + + Some commands support an :attr:`export` attribute. The effect of the attribute + is to make the effect of the command available when the module containing it + is imported. The :cmd:`Hint` command accepts it for instance. + .. _controlling-typing-flags: Controlling Typing Flags -- cgit v1.2.3 From c685a8a3690b3345dbc2770530e3da1b6639a654 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 12 Mar 2020 21:57:58 +0100 Subject: Adding overlays. --- dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh diff --git a/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh b/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh new file mode 100644 index 0000000000..8dae29adb6 --- /dev/null +++ b/dev/ci/user-overlays/11812-ppedrot-export-hint-globality.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "11812" ] || [ "$CI_BRANCH" = "export-hint-globality" ]; then + + equations_CI_REF="export-hint-globality" + equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations + + fiat_parsers_CI_REF="export-hint-globality" + fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat + +fi -- cgit v1.2.3