From 4541d28ba3c50bc8e45c4ccf418bbdd225454dec Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 3 Jun 2019 14:32:18 +0200 Subject: Expose set interface to option tables This lets us avoid having to cache the SearchBlacklist.elements call in search as we can just use the set module's for_all function. --- kernel/names.ml | 1 + kernel/names.mli | 1 + library/goptions.ml | 19 ++++++++++--------- library/goptions.mli | 28 ++++++++++++++-------------- pretyping/classops.ml | 2 +- pretyping/detyping.ml | 2 +- pretyping/detyping.mli | 2 +- vernac/search.ml | 14 ++------------ 8 files changed, 31 insertions(+), 38 deletions(-) diff --git a/kernel/names.ml b/kernel/names.ml index 047a1d6525..39cd4548f5 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -671,6 +671,7 @@ module InductiveOrdered_env = struct let compare = ind_user_ord end +module Indset = Set.Make(InductiveOrdered) module Indmap = Map.Make(InductiveOrdered) module Indmap_env = Map.Make(InductiveOrdered_env) diff --git a/kernel/names.mli b/kernel/names.mli index 2238e932b0..e48cdf26ec 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -481,6 +481,7 @@ type constructor = inductive (* designates the inductive type *) * int (* the index of the constructor BEWARE: indexing starts from 1. *) +module Indset : CSig.SetS with type elt = inductive module Indmap : CSig.MapS with type key = inductive module Constrmap : CSig.MapS with type key = constructor module Indmap_env : CSig.MapS with type key = inductive diff --git a/library/goptions.ml b/library/goptions.ml index f4b8ce9465..2798c21c81 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -53,9 +53,9 @@ module MakeTable = functor (A : sig type t - type key - val compare : t -> t -> int - val table : (string * key table_of_A) list ref + type key + module Set : CSig.SetS with type elt = t + val table : (string * key table_of_A) list ref val encode : Environ.env -> key -> t val subst : substitution -> t -> t val printer : t -> Pp.t @@ -74,7 +74,7 @@ module MakeTable = if String.List.mem_assoc nick !A.table then user_err Pp.(str "Sorry, this table name (" ++ str nick ++ str ") is already used.") - module MySet = Set.Make (struct type t = A.t let compare = A.compare end) + module MySet = A.Set let t = Summary.ref MySet.empty ~name:nick @@ -119,8 +119,9 @@ module MakeTable = } let _ = A.table := (nick, table_of_A)::!A.table - let active c = MySet.mem c !t - let elements () = MySet.elements !t + + let v () = !t + let active x = A.Set.mem x !t end let string_table = ref [] @@ -138,7 +139,7 @@ module StringConvert = functor (A : StringConvertArg) -> struct type t = string type key = string - let compare = String.compare + module Set = CString.Set let table = string_table let encode _env x = x let subst _ x = x @@ -158,7 +159,7 @@ let get_ref_table k = String.List.assoc (nickname k) !ref_table module type RefConvertArg = sig type t - val compare : t -> t -> int + module Set : CSig.SetS with type elt = t val encode : Environ.env -> qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t @@ -171,7 +172,7 @@ module RefConvert = functor (A : RefConvertArg) -> struct type t = A.t type key = qualid - let compare = A.compare + module Set = A.Set let table = ref_table let encode = A.encode let subst = A.subst diff --git a/library/goptions.mli b/library/goptions.mli index 381ba4d34a..ba86cb66ba 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -70,8 +70,8 @@ module MakeStringTable : val member_message : string -> bool -> Pp.t end) -> sig + val v : unit -> CString.Set.t val active : string -> bool - val elements : unit -> string list end (** The functor [MakeRefTable] declares a new table of objects of type @@ -87,19 +87,19 @@ end module MakeRefTable : functor (A : sig - type t - val compare : t -> t -> int - val encode : Environ.env -> qualid -> t - val subst : substitution -> t -> t - val printer : t -> Pp.t - val key : option_name - val title : string - val member_message : t -> bool -> Pp.t - end) -> - sig - val active : A.t -> bool - val elements : unit -> A.t list - end + type t + module Set : CSig.SetS with type elt = t + val encode : Environ.env -> qualid -> t + val subst : substitution -> t -> t + val printer : t -> Pp.t + val key : option_name + val title : string + val member_message : t -> bool -> Pp.t + end) -> +sig + val v : unit -> A.Set.t + val active : A.t -> bool +end (** {6 Options. } *) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 90ce1cc594..70a9784238 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -441,7 +441,7 @@ let coercion_of_reference r = module CoercionPrinting = struct type t = coe_typ - let compare = GlobRef.Ordered.compare + module Set = GlobRef.Set let encode _env = coercion_of_reference let subst = subst_coe_typ let printer x = Nametab.pr_global_env Id.Set.empty x diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 82726eccf0..505dc529cf 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -182,7 +182,7 @@ module PrintingInductiveMake = end) -> struct type t = inductive - let compare = ind_ord + module Set = Indset let encode = Test.encode let subst subst obj = subst_ind subst obj let printer ind = Nametab.pr_global_env Id.Set.empty (IndRef ind) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 00b0578a52..af2baa9713 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -91,7 +91,7 @@ module PrintingInductiveMake : end) -> sig type t = Names.inductive - val compare : t -> t -> int + module Set = Indset val encode : Environ.env -> Libnames.qualid -> Names.inductive val subst : substitution -> t -> t val printer : t -> Pp.t diff --git a/vernac/search.ml b/vernac/search.ml index a5663d65ef..2e3a95bed2 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -200,12 +200,10 @@ let full_name_of_reference ref = DirPath.to_string dir ^ "." ^ Id.to_string id (** Whether a reference is blacklisted *) -let blacklist_filter_aux () = - let l = SearchBlacklist.elements () in - fun ref env typ -> +let blacklist_filter ref env typ = let name = full_name_of_reference ref in let is_not_bl str = not (String.string_contains ~where:name ~what:str) in - List.for_all is_not_bl l + CString.Set.for_all is_not_bl (SearchBlacklist.v ()) let module_filter (mods, outside) ref env typ = let sp = Nametab.path_of_global ref in @@ -227,7 +225,6 @@ let search_about_filter query gr env typ = match query with (** SearchPattern *) let search_pattern ?pstate gopt pat mods pr_search = - let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && @@ -251,7 +248,6 @@ let rewrite_pat2 pat = let search_rewrite ?pstate gopt pat mods pr_search = let pat1 = rewrite_pat1 pat in let pat2 = rewrite_pat2 pat in - let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && (pattern_filter pat1 ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) || @@ -266,7 +262,6 @@ let search_rewrite ?pstate gopt pat mods pr_search = (** Search *) let search_by_head ?pstate gopt pat mods pr_search = - let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = module_filter mods ref env typ && head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && @@ -280,7 +275,6 @@ let search_by_head ?pstate gopt pat mods pr_search = (** SearchAbout *) let search_about ?pstate gopt items mods pr_search = - let blacklist_filter = blacklist_filter_aux () in let filter ref env typ = let eqb b1 b2 = if b1 then b2 else not b2 in module_filter mods ref env typ && @@ -324,7 +318,6 @@ let interface_search ?pstate = let (name, tpe, subtpe, mods, blacklist) = extract_flags [] [] [] [] false flags in - let blacklist_filter = blacklist_filter_aux () in let filter_function ref env constr = let id = Names.Id.to_string (Nametab.basename_of_global ref) in let path = Libnames.dirpath (Nametab.path_of_global ref) in @@ -378,6 +371,3 @@ let interface_search ?pstate = in let () = generic_search ?pstate glnum iter in !ans - -let blacklist_filter ref env typ = - blacklist_filter_aux () ref env typ -- cgit v1.2.3