From a28c4b025439a747354c2432223a3b30912ba182 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 11 May 2020 17:41:58 +0200 Subject: Renaming search_about_item into search_item. --- vernac/search.ml | 2 +- vernac/search.mli | 6 +++--- vernac/vernacentries.ml | 6 +++--- vernac/vernacexpr.ml | 4 ++-- 4 files changed, 9 insertions(+), 9 deletions(-) (limited to 'vernac') diff --git a/vernac/search.ml b/vernac/search.ml index 8b54b696f2..92f6d140d5 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -29,7 +29,7 @@ query, separated by a newline. This type of output is useful for editors (like emacs), to generate a list of completion candidates without having to parse through the types of all symbols. *) -type glob_search_about_item = +type glob_search_item = | GlobSearchSubPattern of constr_pattern | GlobSearchString of string diff --git a/vernac/search.mli b/vernac/search.mli index d3b8444b5f..5eeb77a6d0 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -15,7 +15,7 @@ open Pattern (** {6 Search facilities. } *) -type glob_search_about_item = +type glob_search_item = | GlobSearchSubPattern of constr_pattern | GlobSearchString of string @@ -30,7 +30,7 @@ val blacklist_filter : filter_function val module_filter : DirPath.t list * bool -> filter_function (** Check whether a reference pertains or not to a set of modules *) -val search_filter : glob_search_about_item -> filter_function +val search_filter : glob_search_item -> filter_function (** {6 Specialized search functions} @@ -44,7 +44,7 @@ val search_rewrite : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> -> display_function -> unit val search_pattern : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search : ?pstate:Declare.Proof.t -> int option -> (bool * glob_search_about_item) list +val search : ?pstate:Declare.Proof.t -> int option -> (bool * glob_search_item) list -> DirPath.t list * bool -> display_function -> unit type search_constraint = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 09201d727d..62d97fb845 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1774,7 +1774,7 @@ let interp_search_restriction = function open Search -let interp_search_about_item env sigma = +let interp_search_item env sigma = function | SearchSubPattern pat -> let _,pat = Constrintern.intern_constr_pattern env sigma pat in @@ -1788,7 +1788,7 @@ let interp_search_about_item env sigma = ~head:false (fun _ -> true) s sc in GlobSearchSubPattern (Pattern.PRef ref) with UserError _ -> - user_err ~hdr:"interp_search_about_item" + user_err ~hdr:"interp_search_item" (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component") (* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the @@ -1844,7 +1844,7 @@ let vernac_search ~pstate ~atts s gopt r = | SearchHead c -> (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search | Search sl -> - (Search.search ?pstate gopt (List.map (on_snd (interp_search_about_item env Evd.(from_env env))) sl) r |> + (Search.search ?pstate gopt (List.map (on_snd (interp_search_item env Evd.(from_env env))) sl) r |> Search.prioritize_search) pr_search); Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)") diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index b622fd9801..c3ae1993cd 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -61,7 +61,7 @@ type printable = | PrintStrategy of qualid or_by_notation option | PrintRegistered -type search_about_item = +type search_item = | SearchSubPattern of constr_pattern_expr | SearchString of string * scope_name option @@ -69,7 +69,7 @@ type searchable = | SearchPattern of constr_pattern_expr | SearchRewrite of constr_pattern_expr | SearchHead of constr_pattern_expr - | Search of (bool * search_about_item) list + | Search of (bool * search_item) list type locatable = | LocateAny of qualid or_by_notation -- cgit v1.2.3 From 96333c1bf27f33c15e2475c11c7bfefe87d3a6e1 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 11 May 2020 17:41:58 +0200 Subject: Search: new clauses for searching head, conclusion, kind... - new clauses "hyp:", "concl:", "headhyp:" and "headconcl:" to restrict match to an hypothesis or the conclusion, possibly only at the head (like SearchHead in this latter case) - new clause "is:" to search by kind of object (for some list of kinds) - support for any combination of negations, disjunctions and conjunctions, using a syntax close to that of intropatterns. --- vernac/g_vernac.mlg | 61 ++++++++++++++++++++---- vernac/ppvernac.ml | 81 +++++++++++++++++++++----------- vernac/search.ml | 121 ++++++++++++++++++++++++++++++------------------ vernac/search.mli | 17 +++++-- vernac/vernacentries.ml | 47 +++++++++++++++---- vernac/vernacexpr.ml | 13 ++++-- 6 files changed, 241 insertions(+), 99 deletions(-) (limited to 'vernac') diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 42259cee10..fe3bb9b890 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -40,6 +40,8 @@ let subprf = Entry.create "vernac:subprf" let quoted_attributes = Entry.create "vernac:quoted_attributes" let class_rawexpr = Entry.create "vernac:class_rawexpr" let thm_token = Entry.create "vernac:thm_token" +let def_token = Entry.create "vernac:def_token" +let assumption_token = Entry.create "vernac:assumption_token" let def_body = Entry.create "vernac:def_body" let decl_notations = Entry.create "vernac:decl_notations" let record_field = Entry.create "vernac:record_field" @@ -70,6 +72,13 @@ let test_hash_ident = to_entry "test_hash_ident" begin lk_kw "#" >> lk_ident >> check_no_space end + +let test_id_colon = + let open Pcoq.Lookahead in + to_entry "test_id_colon" begin + lk_ident >> lk_kw ":" + end + } GRAMMAR EXTEND Gram @@ -183,7 +192,7 @@ let name_of_ident_decl : ident_decl -> name_decl = (* Gallina declarations *) GRAMMAR EXTEND Gram - GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion + GLOBAL: gallina gallina_ext thm_token def_token assumption_token def_body of_type_with_opt_coercion record_field decl_notations rec_definition ident_decl univ_decl; gallina: @@ -915,7 +924,7 @@ GRAMMAR EXTEND Gram { fun g -> VernacSearch (SearchPattern c,g, l) } | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules; "." -> { fun g -> VernacSearch (SearchRewrite c,g, l) } - | IDENT "Search"; s = searchabout_query; l = searchabout_queries; "." -> + | IDENT "Search"; s = search_query; l = search_queries; "." -> { let (sl,m) = l in fun g -> VernacSearch (Search (s::sl),g, m) } ] ] ; @@ -1012,16 +1021,50 @@ GRAMMAR EXTEND Gram positive_search_mark: [ [ "-" -> { false } | -> { true } ] ] ; - searchabout_query: - [ [ b = positive_search_mark; s = ne_string; sc = OPT scope_delimiter -> - { (b, SearchString (s,sc)) } - | b = positive_search_mark; p = constr_pattern -> - { (b, SearchSubPattern p) } + search_query: + [ [ b = positive_search_mark; s = search_item -> { (b, SearchLiteral s) } + | b = positive_search_mark; "["; l = LIST1 (LIST1 search_query) SEP "|"; "]" -> { (b, SearchDisjConj l) } + ] ] + ; + search_item: + [ [ test_id_colon; where = search_where; ":"; s = ne_string; sc = OPT scope_delimiter -> + { SearchString (where,s,sc) } + | IDENT "is"; ":"; kl = logical_kind -> + { SearchKind kl } + | s = ne_string; sc = OPT scope_delimiter -> + { SearchString ((Anywhere,false),s,sc) } + | test_id_colon; where = search_where; ":"; p = constr_pattern -> + { SearchSubPattern (where,p) } + | p = constr_pattern -> + { SearchSubPattern ((Anywhere,false),p) } ] ] ; - searchabout_queries: + logical_kind: + [ [ k = thm_token -> { IsProof k } + | k = assumption_token -> { IsAssumption (snd k) } + | k = IDENT "Context" -> { IsAssumption Context } + | k = extended_def_token -> { IsDefinition k } + | IDENT "Primitive" -> { IsPrimitive } ] ] + ; + extended_def_token: + [ [ k = def_token -> { snd k } + | IDENT "Coercion" -> { Coercion } + | IDENT "Instance" -> { Instance } + | IDENT "Scheme" -> { Scheme } + | IDENT "Canonical" -> { CanonicalStructure } + | IDENT "Field" -> { StructureComponent } + | IDENT "Method" -> { Method } ] ] + ; + search_where: + [ [ IDENT "head" -> { Anywhere, true } + | IDENT "hyp" -> { InHyp, false } + | IDENT "concl" -> { InConcl, false } + | IDENT "headhyp" -> { InHyp, true } + | IDENT "headconcl" -> { InConcl, true } ] ] + ; + search_queries: [ [ m = ne_in_or_out_modules -> { ([],m) } - | s = searchabout_query; l = searchabout_queries -> + | s = search_query; l = search_queries -> { let (sl,m) = l in (s::sl,m) } | -> { ([],SearchOutside []) } ] ] diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index b97cdfa51c..2c52c605b5 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -108,6 +108,38 @@ open Pputils let sep = fun _ -> spc() let sep_v2 = fun _ -> str"," ++ spc() + let string_of_theorem_kind = let open Decls in function + | Theorem -> "Theorem" + | Lemma -> "Lemma" + | Fact -> "Fact" + | Remark -> "Remark" + | Property -> "Property" + | Proposition -> "Proposition" + | Corollary -> "Corollary" + + let string_of_definition_object_kind = let open Decls in function + | Definition -> "Definition" + | Example -> "Example" + | Coercion -> "Coercion" + | SubClass -> "SubClass" + | CanonicalStructure -> "Canonical Structure" + | Instance -> "Instance" + | Let -> "Let" + | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> + CErrors.anomaly (Pp.str "Internal definition kind.") + + let string_of_assumption_kind = let open Decls in function + | Definitional -> "Parameter" + | Logical -> "Axiom" + | Conjectural -> "Conjecture" + | Context -> "Context" + + let string_of_logical_kind = let open Decls in function + | IsAssumption k -> string_of_assumption_kind k + | IsDefinition k -> string_of_definition_object_kind k + | IsProof k -> string_of_theorem_kind k + | IsPrimitive -> "Primitive" + let pr_notation_entry = function | InConstrEntry -> keyword "constr" | InCustomEntry s -> keyword "custom" ++ spc () ++ str s @@ -148,14 +180,28 @@ open Pputils | SearchOutside [] -> mt() | SearchOutside l -> spc() ++ keyword "outside" ++ spc() ++ prlist_with_sep sep pr_module l - let pr_search (b,c) = - (if b then str "-" else mt()) ++ - match c with - | SearchSubPattern p -> + let pr_search_where = function + | Anywhere, false -> mt () + | Anywhere, true -> str "head:" + | InHyp, true -> str "headhyp:" + | InHyp, false -> str "hyp:" + | InConcl, true -> str "headconcl:" + | InConcl, false -> str "concl:" + + let pr_search_item = function + | SearchSubPattern (where,p) -> let env = Global.env () in let sigma = Evd.from_env env in - pr_constr_pattern_expr env sigma p - | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + pr_search_where where ++ pr_constr_pattern_expr env sigma p + | SearchString (where,s,sc) -> pr_search_where where ++ qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc + | SearchKind kind -> str "is:" ++ str (string_of_logical_kind kind) + + let rec pr_search_request = function + | SearchLiteral a -> pr_search_item a + | SearchDisjConj l -> str "[" ++ prlist_with_sep spc (prlist_with_sep pr_bar pr_search_default) l ++ str "]" + + and pr_search_default (b, s) = + (if b then mt() else str "-") ++ pr_search_request s let pr_search a gopt b pr_p = pr_opt (fun g -> Goal_select.pr_goal_selector g ++ str ":"++ spc()) gopt @@ -165,7 +211,7 @@ open Pputils | SearchPattern c -> keyword "SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchRewrite c -> keyword "SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b | Search sl -> - keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search sl ++ pr_in_out_modules b + keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_default sl ++ pr_in_out_modules b let pr_option_ref_value = function | Goptions.QualidRefValue id -> pr_qualid id @@ -386,15 +432,6 @@ open Pputils prlist_with_sep pr_semicolon (pr_params pr_c) *) -let string_of_theorem_kind = let open Decls in function - | Theorem -> "Theorem" - | Lemma -> "Lemma" - | Fact -> "Fact" - | Remark -> "Remark" - | Property -> "Property" - | Proposition -> "Proposition" - | Corollary -> "Corollary" - let pr_thm_token k = keyword (string_of_theorem_kind k) let pr_syntax_modifier = let open Gramlib.Gramext in function @@ -611,18 +648,6 @@ let string_of_theorem_kind = let open Decls in function with Not_found -> hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")") - -let string_of_definition_object_kind = let open Decls in function - | Definition -> "Definition" - | Example -> "Example" - | Coercion -> "Coercion" - | SubClass -> "SubClass" - | CanonicalStructure -> "Canonical Structure" - | Instance -> "Instance" - | Let -> "Let" - | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> - CErrors.anomaly (Pp.str "Internal definition kind.") - let pr_vernac_expr v = let return = tag_vernac v in let env = Global.env () in diff --git a/vernac/search.ml b/vernac/search.ml index 92f6d140d5..181c75702d 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -17,11 +17,14 @@ open Libobject open Environ open Pattern open Libnames +open Vernacexpr module NamedDecl = Context.Named.Declaration -type filter_function = GlobRef.t -> env -> constr -> bool -type display_function = GlobRef.t -> env -> constr -> unit +type filter_function = + GlobRef.t -> Decls.logical_kind option -> env -> constr -> bool +type display_function = + GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit (* This option restricts the output of [SearchPattern ...], etc. to the names of the symbols matching the @@ -30,8 +33,14 @@ editors (like emacs), to generate a list of completion candidates without having to parse through the types of all symbols. *) type glob_search_item = - | GlobSearchSubPattern of constr_pattern + | GlobSearchSubPattern of glob_search_where * bool * constr_pattern | GlobSearchString of string + | GlobSearchKind of Decls.logical_kind + | GlobSearchFilter of (GlobRef.t -> bool) + +type glob_search_request = + | GlobSearchLiteral of glob_search_item + | GlobSearchDisjConj of (bool * glob_search_request) list list module SearchBlacklist = Goptions.MakeStringTable @@ -52,7 +61,7 @@ module SearchBlacklist = let iter_constructors indsp u fn env nconstr = for i = 1 to nconstr do let typ = Inductiveops.type_of_constructor env ((indsp, i), u) in - fn (GlobRef.ConstructRef (indsp, i)) env typ + fn (GlobRef.ConstructRef (indsp, i)) None env typ done let iter_named_context_name_type f = @@ -64,9 +73,9 @@ let get_current_or_goal_context ?pstate glnum = | Some p -> Declare.get_goal_context p glnum (* General search over hypothesis of a goal *) -let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) = +let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit) = let env = Global.env () in - let iter_hyp idh typ = fn (GlobRef.VarRef idh) env typ in + let iter_hyp idh typ = fn (GlobRef.VarRef idh) None env typ in let evmap,e = get_current_or_goal_context ?pstate glnum in let pfctxt = named_context e in iter_named_context_name_type iter_hyp pfctxt @@ -80,9 +89,9 @@ let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with | exception Not_found -> () (* General search over declarations *) -let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = +let iter_declarations (fn : GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit) = let env = Global.env () in - List.iter (fun d -> fn (GlobRef.VarRef (NamedDecl.get_id d)) env (NamedDecl.get_type d)) + List.iter (fun d -> fn (GlobRef.VarRef (NamedDecl.get_id d)) None env (NamedDecl.get_type d)) (Environ.named_context env); let iter_obj (sp, kn) lobj = match lobj with | AtomicObject o -> @@ -91,7 +100,8 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = let cst = Global.constant_of_delta_kn kn in let gr = GlobRef.ConstRef cst in let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in - fn gr env typ + let kind = Dumpglob.constant_kind cst in + fn gr (Some kind) env typ end @@ DynHandle.add DeclareInd.Internal.objInductive begin fun _ -> let mind = Global.mind_of_delta_kn kn in @@ -101,7 +111,7 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) = let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let i = (ind, u) in let typ = Inductiveops.type_of_inductive env i in - let () = fn (GlobRef.IndRef ind) env typ in + let () = fn (GlobRef.IndRef ind) None env typ in let len = Array.length mip.mind_user_lc in iter_constructors ind u fn env len in @@ -132,7 +142,7 @@ module ConstrPriority = struct (* The priority is memoised here. Because of the very localised use of this module, it is not worth it making a convenient interface. *) - type t = GlobRef.t * Environ.env * Constr.t * priority + type t = GlobRef.t * Decls.logical_kind option * Environ.env * Constr.t * priority and priority = int module ConstrSet = CSet.Make(Constr) @@ -157,7 +167,7 @@ module ConstrPriority = struct let priority t : priority = -(3*(num_symbols t) + size t) - let compare (_,_,_,p1) (_,_,_,p2) = + let compare (_,_,_,_,p1) (_,_,_,_,p2) = pervasives_compare p1 p2 end @@ -172,16 +182,16 @@ let rec iter_priority_queue q fn = with Heap.EmptyHeap -> None end in match next with - | Some (gref,env,t,_) -> - fn gref env t; + | Some (gref,kind,env,t,_) -> + fn gref kind env t; iter_priority_queue (PriorityQueue.remove q) fn | None -> () let prioritize_search seq fn = let acc = ref PriorityQueue.empty in - let iter gref env t = + let iter gref kind env t = let p = ConstrPriority.priority t in - acc := PriorityQueue.add (gref,env,t,p) !acc + acc := PriorityQueue.add (gref,kind,env,t,p) !acc in let () = seq iter in iter_priority_queue !acc fn @@ -211,12 +221,12 @@ let full_name_of_reference ref = DirPath.to_string dir ^ "." ^ Id.to_string id (** Whether a reference is blacklisted *) -let blacklist_filter ref env typ = +let blacklist_filter ref kind env typ = let name = full_name_of_reference ref in let is_not_bl str = not (String.string_contains ~where:name ~what:str) in CString.Set.for_all is_not_bl (SearchBlacklist.v ()) -let module_filter (mods, outside) ref env typ = +let module_filter (mods, outside) ref kind env typ = let sp = Nametab.path_of_global ref in let sl = dirpath sp in let is_outside md = not (is_dirpath_prefix_of md sl) in @@ -226,23 +236,40 @@ let module_filter (mods, outside) ref env typ = let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref) -let search_filter query gr env typ = match query with -| GlobSearchSubPattern pat -> - Constr_matching.is_matching_appsubterm ~closed:false env (Evd.from_env env) pat (EConstr.of_constr typ) +let search_filter query gr kind env typ = match query with +| GlobSearchSubPattern (where,head,pat) -> + let open Context.Rel.Declaration in + let collect_hyps ctx = + List.fold_left (fun acc d -> match get_value d with + | None -> get_type d :: acc + | Some b -> b :: get_type d :: acc) [] ctx in + let typl= match where with + | InHyp -> collect_hyps (fst (Term.decompose_prod_assum typ)) + | InConcl -> [snd (Term.decompose_prod_assum typ)] + | Anywhere -> + if head then + let ctx, ccl = Term.decompose_prod_assum typ in ccl :: collect_hyps ctx + else [typ] in + List.exists (fun typ -> + let f = + if head then Constr_matching.is_matching_head + else Constr_matching.is_matching_appsubterm ~closed:false in + f env (Evd.from_env env) pat (EConstr.of_constr typ)) typl | GlobSearchString s -> String.string_contains ~where:(name_of_reference gr) ~what:s - +| GlobSearchKind k -> (match kind with None -> false | Some k' -> k = k') +| GlobSearchFilter f -> f gr (** SearchPattern *) let search_pattern ?pstate gopt pat mods pr_search = - let filter ref env typ = - module_filter mods ref env typ && + let filter ref kind env typ = + module_filter mods ref kind env typ && pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && - blacklist_filter ref env typ + blacklist_filter ref kind env typ in - let iter ref env typ = - if filter ref env typ then pr_search ref env typ + let iter ref kind env typ = + if filter ref kind env typ then pr_search ref kind env typ in generic_search ?pstate gopt iter @@ -259,42 +286,44 @@ 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 filter ref env typ = - module_filter mods ref env typ && + let filter ref kind env typ = + module_filter mods ref kind env typ && (pattern_filter pat1 ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) || pattern_filter pat2 ref env (Evd.from_env env) (EConstr.of_constr typ)) && - blacklist_filter ref env typ + blacklist_filter ref kind env typ in - let iter ref env typ = - if filter ref env typ then pr_search ref env typ + let iter ref kind env typ = + if filter ref kind env typ then pr_search ref kind env typ in generic_search ?pstate gopt iter (** Search *) let search_by_head ?pstate gopt pat mods pr_search = - let filter ref env typ = - module_filter mods ref env typ && + let filter ref kind env typ = + module_filter mods ref kind env typ && head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && - blacklist_filter ref env typ + blacklist_filter ref kind env typ in - let iter ref env typ = - if filter ref env typ then pr_search ref env typ + let iter ref kind env typ = + if filter ref kind env typ then pr_search ref kind env typ in generic_search ?pstate gopt iter (** Search *) let search ?pstate gopt items mods pr_search = - let filter ref env typ = + let filter ref kind env typ = let eqb b1 b2 = if b1 then b2 else not b2 in - module_filter mods ref env typ && - List.for_all - (fun (b,i) -> eqb b (search_filter i ref env typ)) items && - blacklist_filter ref env typ + module_filter mods ref kind env typ && + let rec aux = function + | GlobSearchLiteral i -> search_filter i ref kind env typ + | GlobSearchDisjConj l -> List.exists (List.for_all aux') l + and aux' (b,s) = eqb b (aux s) in + List.for_all aux' items && blacklist_filter ref kind env typ in - let iter ref env typ = - if filter ref env typ then pr_search ref env typ + let iter ref kind env typ = + if filter ref kind env typ then pr_search ref kind env typ in generic_search ?pstate gopt iter @@ -351,7 +380,7 @@ let interface_search ?pstate = List.for_all match_type tpe && List.for_all match_subtype subtpe && List.for_all match_module mods && - (blacklist || blacklist_filter ref env constr) + (blacklist || blacklist_filter ref kind env constr) in let ans = ref [] in let print_function ref env constr = @@ -377,7 +406,7 @@ let interface_search ?pstate = } in ans := answer :: !ans; in - let iter ref env typ = + let iter ref kind env typ = if filter_function ref env typ then print_function ref env typ in let () = generic_search ?pstate glnum iter in diff --git a/vernac/search.mli b/vernac/search.mli index 5eeb77a6d0..3dc437d85a 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -12,15 +12,24 @@ open Names open Constr open Environ open Pattern +open Vernacexpr (** {6 Search facilities. } *) type glob_search_item = - | GlobSearchSubPattern of constr_pattern + | GlobSearchSubPattern of glob_search_where * bool * constr_pattern | GlobSearchString of string + | GlobSearchKind of Decls.logical_kind + | GlobSearchFilter of (GlobRef.t -> bool) -type filter_function = GlobRef.t -> env -> constr -> bool -type display_function = GlobRef.t -> env -> constr -> unit +type glob_search_request = + | GlobSearchLiteral of glob_search_item + | GlobSearchDisjConj of (bool * glob_search_request) list list + +type filter_function = + GlobRef.t -> Decls.logical_kind option -> env -> constr -> bool +type display_function = + GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit (** {6 Generic filter functions} *) @@ -44,7 +53,7 @@ val search_rewrite : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> -> display_function -> unit val search_pattern : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search : ?pstate:Declare.Proof.t -> int option -> (bool * glob_search_item) list +val search : ?pstate:Declare.Proof.t -> int option -> (bool * glob_search_request) list -> DirPath.t list * bool -> display_function -> unit type search_constraint = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 62d97fb845..80bd1ac727 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1774,22 +1774,51 @@ let interp_search_restriction = function open Search +let kind_searcher = Decls.(function + (* Kinds referring to the keyword introducing the object *) + | IsAssumption _ + | IsDefinition (Definition | Example | Fixpoint | CoFixpoint | Method | StructureComponent | Let) + | IsProof _ + | IsPrimitive as k -> Inl k + (* Kinds referring to the status of the object *) + | IsDefinition (Coercion | SubClass | IdentityCoercion as k') -> + let coercions = Coercionops.coercions () in + Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Coercionops.coe_value gr && + (k' <> SubClass && k' <> IdentityCoercion || c.Coercionops.coe_is_identity)) coercions) + | IsDefinition CanonicalStructure -> + let canonproj = Recordops.canonical_projections () in + Inr (fun gr -> List.exists (fun c -> GlobRef.equal (snd c).Recordops.o_ORIGIN gr) canonproj) + | IsDefinition Scheme -> + let schemes = DeclareScheme.all_schemes () in + Inr (fun gr -> Indset.exists (fun c -> GlobRef.equal (GlobRef.IndRef c) gr) schemes) + | IsDefinition Instance -> + let instances = Typeclasses.all_instances () in + Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Typeclasses.is_impl gr) instances)) + let interp_search_item env sigma = function - | SearchSubPattern pat -> + | SearchSubPattern ((where,head),pat) -> let _,pat = Constrintern.intern_constr_pattern env sigma pat in - GlobSearchSubPattern pat - | SearchString (s,None) when Id.is_valid s -> + GlobSearchSubPattern (where,head,pat) + | SearchString ((Anywhere,false),s,None) when Id.is_valid s -> GlobSearchString s - | SearchString (s,sc) -> - try + | SearchString ((where,head),s,sc) -> + (try let ref = Notation.interp_notation_as_global_reference ~head:false (fun _ -> true) s sc in - GlobSearchSubPattern (Pattern.PRef ref) + GlobSearchSubPattern (where,head,Pattern.PRef ref) with UserError _ -> user_err ~hdr:"interp_search_item" - (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component") + (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")) + | SearchKind k -> + match kind_searcher k with + | Inl k -> GlobSearchKind k + | Inr f -> GlobSearchFilter f + +let rec interp_search_request env sigma = function + | b, SearchLiteral i -> b, GlobSearchLiteral (interp_search_item env sigma i) + | b, SearchDisjConj l -> b, GlobSearchDisjConj (List.map (List.map (interp_search_request env sigma)) l) (* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the `search_output_name_only` option to avoid excessive printing when @@ -1823,7 +1852,7 @@ let vernac_search ~pstate ~atts s gopt r = | Some g -> snd (get_goal_or_global_context ~pstate g) , Some g in let get_pattern c = snd (Constrintern.intern_constr_pattern env Evd.(from_env env) c) in - let pr_search ref env c = + let pr_search ref kind env c = let pr = pr_global ref in let pp = if !search_output_name_only then pr @@ -1844,7 +1873,7 @@ let vernac_search ~pstate ~atts s gopt r = | SearchHead c -> (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search | Search sl -> - (Search.search ?pstate gopt (List.map (on_snd (interp_search_item env Evd.(from_env env))) sl) r |> + (Search.search ?pstate gopt (List.map (interp_search_request env Evd.(from_env env)) sl) r |> Search.prioritize_search) pr_search); Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)") diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index c3ae1993cd..0fdf9e2a7b 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -61,15 +61,22 @@ type printable = | PrintStrategy of qualid or_by_notation option | PrintRegistered +type glob_search_where = InHyp | InConcl | Anywhere + type search_item = - | SearchSubPattern of constr_pattern_expr - | SearchString of string * scope_name option + | SearchSubPattern of (glob_search_where * bool) * constr_pattern_expr + | SearchString of (glob_search_where * bool) * string * scope_name option + | SearchKind of Decls.logical_kind + +type search_request = + | SearchLiteral of search_item + | SearchDisjConj of (bool * search_request) list list type searchable = | SearchPattern of constr_pattern_expr | SearchRewrite of constr_pattern_expr | SearchHead of constr_pattern_expr - | Search of (bool * search_item) list + | Search of (bool * search_request) list type locatable = | LocateAny of qualid or_by_notation -- cgit v1.2.3 From 7c113b3a736e8a374b8a57aacde846fc5c5cbf3f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 11 May 2020 17:41:58 +0200 Subject: Addressing a suggestion from Théo Zimmermann. --- vernac/vernacentries.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac') diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 80bd1ac727..75873381bf 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1810,7 +1810,7 @@ let interp_search_item env sigma = GlobSearchSubPattern (where,head,Pattern.PRef ref) with UserError _ -> user_err ~hdr:"interp_search_item" - (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")) + (str "Unable to interpret " ++ quote (str s) ++ str " as a reference.")) | SearchKind k -> match kind_searcher k with | Inl k -> GlobSearchKind k -- cgit v1.2.3 From 34237bb07fa8663d3d9e8ca4f9459f46841fd43d Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 11 May 2020 17:41:58 +0200 Subject: Search: Displaying the "use About" notice only when really needed. --- vernac/vernacentries.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'vernac') diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 75873381bf..c7e8d9a3b9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1852,14 +1852,20 @@ let vernac_search ~pstate ~atts s gopt r = | Some g -> snd (get_goal_or_global_context ~pstate g) , Some g in let get_pattern c = snd (Constrintern.intern_constr_pattern env Evd.(from_env env) c) in + let warnlist = ref [] in let pr_search ref kind env c = let pr = pr_global ref in let pp = if !search_output_name_only then pr else begin let open Impargs in - let impargs = select_stronger_impargs (implicits_of_global ref) in + let impls = implicits_of_global ref in + let impargs = select_stronger_impargs impls in let impargs = List.map binding_kind_of_status impargs in + if List.length impls > 1 || + List.exists Glob_term.(function Explicit -> false | MaxImplicit | NonMaxImplicit -> true) + (List.skipn_at_least (Termops.nb_prod_modulo_zeta Evd.(from_env env) (EConstr.of_constr c)) impargs) + then warnlist := pr :: !warnlist; let pc = pr_ltype_env env Evd.(from_env env) ~impargs c in hov 2 (pr ++ str":" ++ spc () ++ pc) end @@ -1875,7 +1881,10 @@ let vernac_search ~pstate ~atts s gopt r = | Search sl -> (Search.search ?pstate gopt (List.map (interp_search_request env Evd.(from_env env)) sl) r |> Search.prioritize_search) pr_search); - Feedback.msg_notice (str "(use \"About\" for full details on implicit arguments)") + if !warnlist <> [] then + Feedback.msg_notice (str "(" ++ + hov 0 (strbrk "use \"About\" for full details on the implicit arguments of " ++ + pr_enum (fun x -> x) !warnlist ++ str ")")) let vernac_locate ~pstate = let open Constrexpr in function | LocateAny {v=AN qid} -> Prettyp.print_located_qualid qid -- cgit v1.2.3 From 50374354b7ced786d68d45884295a4c770642123 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 11 May 2020 17:41:58 +0200 Subject: Cleaning the use of pstate and evar_map in Search. --- vernac/search.ml | 89 ++++++++++++++++++------------------------------- vernac/search.mli | 15 ++++----- vernac/vernacentries.ml | 18 +++++----- 3 files changed, 49 insertions(+), 73 deletions(-) (limited to 'vernac') diff --git a/vernac/search.ml b/vernac/search.ml index 181c75702d..f6b5bbd8e9 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -22,7 +22,7 @@ open Vernacexpr module NamedDecl = Context.Named.Declaration type filter_function = - GlobRef.t -> Decls.logical_kind option -> env -> constr -> bool + GlobRef.t -> Decls.logical_kind option -> env -> Evd.evar_map -> constr -> bool type display_function = GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit @@ -64,22 +64,6 @@ let iter_constructors indsp u fn env nconstr = fn (GlobRef.ConstructRef (indsp, i)) None env typ done -let iter_named_context_name_type f = - List.iter (fun decl -> f (NamedDecl.get_id decl) (NamedDecl.get_type decl)) - -let get_current_or_goal_context ?pstate glnum = - match pstate with - | None -> let env = Global.env () in Evd.(from_env env, env) - | Some p -> Declare.get_goal_context p glnum - -(* General search over hypothesis of a goal *) -let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit) = - let env = Global.env () in - let iter_hyp idh typ = fn (GlobRef.VarRef idh) None env typ in - let evmap,e = get_current_or_goal_context ?pstate glnum in - let pfctxt = named_context e in - iter_named_context_name_type iter_hyp pfctxt - (* FIXME: this is a Libobject hack that should be replaced with a proper registration mechanism. *) module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> unit end) @@ -89,8 +73,7 @@ let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with | exception Not_found -> () (* General search over declarations *) -let iter_declarations (fn : GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit) = - let env = Global.env () in +let generic_search env (fn : GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit) = List.iter (fun d -> fn (GlobRef.VarRef (NamedDecl.get_id d)) None env (NamedDecl.get_type d)) (Environ.named_context env); let iter_obj (sp, kn) lobj = match lobj with @@ -125,12 +108,6 @@ let iter_declarations (fn : GlobRef.t -> Decls.logical_kind option -> env -> con try Declaremods.iter_all_segments iter_obj with Not_found -> () -let generic_search ?pstate glnumopt fn = - (match glnumopt with - | None -> () - | Some glnum -> iter_hypothesis ?pstate glnum fn); - iter_declarations fn - (** This module defines a preference on constrs in the form of a [compare] function (preferred constr must be big for this functions, so preferences such as small constr must use a reversed @@ -221,12 +198,12 @@ let full_name_of_reference ref = DirPath.to_string dir ^ "." ^ Id.to_string id (** Whether a reference is blacklisted *) -let blacklist_filter ref kind env typ = +let blacklist_filter ref kind env sigma typ = let name = full_name_of_reference ref in let is_not_bl str = not (String.string_contains ~where:name ~what:str) in CString.Set.for_all is_not_bl (SearchBlacklist.v ()) -let module_filter (mods, outside) ref kind env typ = +let module_filter (mods, outside) ref kind env sigma typ = let sp = Nametab.path_of_global ref in let sl = dirpath sp in let is_outside md = not (is_dirpath_prefix_of md sl) in @@ -236,7 +213,7 @@ let module_filter (mods, outside) ref kind env typ = let name_of_reference ref = Id.to_string (Nametab.basename_of_global ref) -let search_filter query gr kind env typ = match query with +let search_filter query gr kind env sigma typ = match query with | GlobSearchSubPattern (where,head,pat) -> let open Context.Rel.Declaration in let collect_hyps ctx = @@ -254,7 +231,7 @@ let search_filter query gr kind env typ = match query with let f = if head then Constr_matching.is_matching_head else Constr_matching.is_matching_appsubterm ~closed:false in - f env (Evd.from_env env) pat (EConstr.of_constr typ)) typl + f env sigma pat (EConstr.of_constr typ)) typl | GlobSearchString s -> String.string_contains ~where:(name_of_reference gr) ~what:s | GlobSearchKind k -> (match kind with None -> false | Some k' -> k = k') @@ -262,16 +239,16 @@ let search_filter query gr kind env typ = match query with (** SearchPattern *) -let search_pattern ?pstate gopt pat mods pr_search = +let search_pattern env sigma pat mods pr_search = let filter ref kind env typ = - module_filter mods ref kind env typ && - pattern_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && - blacklist_filter ref kind env typ + module_filter mods ref kind env sigma typ && + pattern_filter pat ref env sigma (EConstr.of_constr typ) && + blacklist_filter ref kind env sigma typ in let iter ref kind env typ = if filter ref kind env typ then pr_search ref kind env typ in - generic_search ?pstate gopt iter + generic_search env iter (** SearchRewrite *) @@ -283,49 +260,49 @@ let rewrite_pat1 pat = let rewrite_pat2 pat = PApp (PRef (eq ()), [| PMeta None; PMeta None; pat |]) -let search_rewrite ?pstate gopt pat mods pr_search = +let search_rewrite env sigma pat mods pr_search = let pat1 = rewrite_pat1 pat in let pat2 = rewrite_pat2 pat in let filter ref kind env typ = - module_filter mods ref kind env typ && - (pattern_filter pat1 ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) || - pattern_filter pat2 ref env (Evd.from_env env) (EConstr.of_constr typ)) && - blacklist_filter ref kind env typ + module_filter mods ref kind env sigma typ && + (pattern_filter pat1 ref env sigma (EConstr.of_constr typ) || + pattern_filter pat2 ref env sigma (EConstr.of_constr typ)) && + blacklist_filter ref kind env sigma typ in let iter ref kind env typ = if filter ref kind env typ then pr_search ref kind env typ in - generic_search ?pstate gopt iter + generic_search env iter (** Search *) -let search_by_head ?pstate gopt pat mods pr_search = +let search_by_head env sigma pat mods pr_search = let filter ref kind env typ = - module_filter mods ref kind env typ && - head_filter pat ref env (Evd.from_env env) (* FIXME *) (EConstr.of_constr typ) && - blacklist_filter ref kind env typ + module_filter mods ref kind env sigma typ && + head_filter pat ref env sigma (EConstr.of_constr typ) && + blacklist_filter ref kind env sigma typ in let iter ref kind env typ = if filter ref kind env typ then pr_search ref kind env typ in - generic_search ?pstate gopt iter + generic_search env iter (** Search *) -let search ?pstate gopt items mods pr_search = +let search env sigma items mods pr_search = let filter ref kind env typ = let eqb b1 b2 = if b1 then b2 else not b2 in - module_filter mods ref kind env typ && + module_filter mods ref kind env sigma typ && let rec aux = function - | GlobSearchLiteral i -> search_filter i ref kind env typ + | GlobSearchLiteral i -> search_filter i ref kind env sigma typ | GlobSearchDisjConj l -> List.exists (List.for_all aux') l and aux' (b,s) = eqb b (aux s) in - List.for_all aux' items && blacklist_filter ref kind env typ + List.for_all aux' items && blacklist_filter ref kind env sigma typ in let iter ref kind env typ = if filter ref kind env typ then pr_search ref kind env typ in - generic_search ?pstate gopt iter + generic_search env iter type search_constraint = | Name_Pattern of Str.regexp @@ -340,7 +317,7 @@ type 'a coq_object = { coq_object_object : 'a; } -let interface_search ?pstate = +let interface_search env sigma = let rec extract_flags name tpe subtpe mods blacklist = function | [] -> (name, tpe, subtpe, mods, blacklist) | (Name_Pattern regexp, b) :: l -> @@ -354,7 +331,7 @@ let interface_search ?pstate = | (Include_Blacklist, b) :: l -> extract_flags name tpe subtpe mods b l in - fun ?glnum flags -> + fun flags -> let (name, tpe, subtpe, mods, blacklist) = extract_flags [] [] [] [] false flags in @@ -366,12 +343,12 @@ let interface_search ?pstate = toggle (Str.string_match regexp id 0) flag in let match_type (pat, flag) = - toggle (Constr_matching.is_matching env (Evd.from_env env) pat (EConstr.of_constr constr)) flag + toggle (Constr_matching.is_matching env sigma pat (EConstr.of_constr constr)) flag in let match_subtype (pat, flag) = toggle (Constr_matching.is_matching_appsubterm ~closed:false - env (Evd.from_env env) pat (EConstr.of_constr constr)) flag + env sigma pat (EConstr.of_constr constr)) flag in let match_module (mdl, flag) = toggle (Libnames.is_dirpath_prefix_of mdl path) flag @@ -380,7 +357,7 @@ let interface_search ?pstate = List.for_all match_type tpe && List.for_all match_subtype subtpe && List.for_all match_module mods && - (blacklist || blacklist_filter ref kind env constr) + (blacklist || blacklist_filter ref kind env sigma constr) in let ans = ref [] in let print_function ref env constr = @@ -409,5 +386,5 @@ let interface_search ?pstate = let iter ref kind env typ = if filter_function ref env typ then print_function ref env typ in - let () = generic_search ?pstate glnum iter in + let () = generic_search env iter in !ans diff --git a/vernac/search.mli b/vernac/search.mli index 3dc437d85a..09847f4e03 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -27,7 +27,7 @@ type glob_search_request = | GlobSearchDisjConj of (bool * glob_search_request) list list type filter_function = - GlobRef.t -> Decls.logical_kind option -> env -> constr -> bool + GlobRef.t -> Decls.logical_kind option -> env -> Evd.evar_map -> constr -> bool type display_function = GlobRef.t -> Decls.logical_kind option -> env -> constr -> unit @@ -47,13 +47,13 @@ val search_filter : glob_search_item -> filter_function goal and the global environment for things matching [pattern] and satisfying module exclude/include clauses of [modinout]. *) -val search_by_head : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool +val search_by_head : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search_rewrite : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool +val search_rewrite : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search_pattern : ?pstate:Declare.Proof.t -> int option -> constr_pattern -> DirPath.t list * bool +val search_pattern : env -> Evd.evar_map -> constr_pattern -> DirPath.t list * bool -> display_function -> unit -val search : ?pstate:Declare.Proof.t -> int option -> (bool * glob_search_request) list +val search : env -> Evd.evar_map -> (bool * glob_search_request) list -> DirPath.t list * bool -> display_function -> unit type search_constraint = @@ -74,12 +74,11 @@ type 'a coq_object = { coq_object_object : 'a; } -val interface_search : ?pstate:Declare.Proof.t -> ?glnum:int -> (search_constraint * bool) list -> - constr coq_object list +val interface_search : env -> Evd.evar_map -> (search_constraint * bool) list -> constr coq_object list (** {6 Generic search function} *) -val generic_search : ?pstate:Declare.Proof.t -> int option -> display_function -> unit +val generic_search : env -> display_function -> unit (** This function iterates over all hypothesis of the goal numbered [glnum] (if present) and all known declarations. *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index c7e8d9a3b9..ea79cf7465 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1843,15 +1843,15 @@ let () = let vernac_search ~pstate ~atts s gopt r = let gopt = query_command_selector gopt in let r = interp_search_restriction r in - let env,gopt = + let sigma, env = match gopt with | None -> (* 1st goal by default if it exists, otherwise no goal at all *) - (try snd (get_goal_or_global_context ~pstate 1) , Some 1 - with _ -> Global.env (),None) + (try get_goal_or_global_context ~pstate 1 + with _ -> let env = Global.env () in (Evd.from_env env, env)) (* if goal selector is given and wrong, then let exceptions be raised. *) - | Some g -> snd (get_goal_or_global_context ~pstate g) , Some g + | Some g -> get_goal_or_global_context ~pstate g in - let get_pattern c = snd (Constrintern.intern_constr_pattern env Evd.(from_env env) c) in + let get_pattern c = snd (Constrintern.intern_constr_pattern env sigma c) in let warnlist = ref [] in let pr_search ref kind env c = let pr = pr_global ref in @@ -1873,13 +1873,13 @@ let vernac_search ~pstate ~atts s gopt r = in (match s with | SearchPattern c -> - (Search.search_pattern ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search + (Search.search_pattern env sigma (get_pattern c) r |> Search.prioritize_search) pr_search | SearchRewrite c -> - (Search.search_rewrite ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search + (Search.search_rewrite env sigma (get_pattern c) r |> Search.prioritize_search) pr_search | SearchHead c -> - (Search.search_by_head ?pstate gopt (get_pattern c) r |> Search.prioritize_search) pr_search + (Search.search_by_head env sigma (get_pattern c) r |> Search.prioritize_search) pr_search | Search sl -> - (Search.search ?pstate gopt (List.map (interp_search_request env Evd.(from_env env)) sl) r |> + (Search.search env sigma (List.map (interp_search_request env Evd.(from_env env)) sl) r |> Search.prioritize_search) pr_search); if !warnlist <> [] then Feedback.msg_notice (str "(" ++ -- cgit v1.2.3 From ac507d8f51697a9f6d760a59efe61edb5ced57c7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 11 May 2020 17:41:58 +0200 Subject: Moving interpretation of Search commands to their own file: comSearch.ml. --- vernac/comSearch.ml | 133 ++++++++++++++++++++++++++++++++++++++++++++++++ vernac/comSearch.mli | 14 +++++ vernac/search.ml | 4 +- vernac/vernac.mllib | 1 + vernac/vernacentries.ml | 118 ++---------------------------------------- 5 files changed, 153 insertions(+), 117 deletions(-) create mode 100644 vernac/comSearch.ml create mode 100644 vernac/comSearch.mli (limited to 'vernac') diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml new file mode 100644 index 0000000000..a860bc8bf6 --- /dev/null +++ b/vernac/comSearch.ml @@ -0,0 +1,133 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* + user_err ?loc:qid.CAst.loc ~hdr:"global_module" + (str "Module/section " ++ Ppconstr.pr_qualid qid ++ str " not found.") + +let interp_search_restriction = function + | SearchOutside l -> (List.map global_module l, true) + | SearchInside l -> (List.map global_module l, false) + +let kind_searcher = Decls.(function + (* Kinds referring to the keyword introducing the object *) + | IsAssumption _ + | IsDefinition (Definition | Example | Fixpoint | CoFixpoint | Method | StructureComponent | Let) + | IsProof _ + | IsPrimitive as k -> Inl k + (* Kinds referring to the status of the object *) + | IsDefinition (Coercion | SubClass | IdentityCoercion as k') -> + let coercions = Coercionops.coercions () in + Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Coercionops.coe_value gr && + (k' <> SubClass && k' <> IdentityCoercion || c.Coercionops.coe_is_identity)) coercions) + | IsDefinition CanonicalStructure -> + let canonproj = Recordops.canonical_projections () in + Inr (fun gr -> List.exists (fun c -> GlobRef.equal (snd c).Recordops.o_ORIGIN gr) canonproj) + | IsDefinition Scheme -> + let schemes = DeclareScheme.all_schemes () in + Inr (fun gr -> Indset.exists (fun c -> GlobRef.equal (GlobRef.IndRef c) gr) schemes) + | IsDefinition Instance -> + let instances = Typeclasses.all_instances () in + Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Typeclasses.is_impl gr) instances)) + +let interp_search_item env sigma = + function + | SearchSubPattern ((where,head),pat) -> + let _,pat = Constrintern.intern_constr_pattern env sigma pat in + GlobSearchSubPattern (where,head,pat) + | SearchString ((Anywhere,false),s,None) when Id.is_valid s -> + GlobSearchString s + | SearchString ((where,head),s,sc) -> + (try + let ref = + Notation.interp_notation_as_global_reference + ~head:false (fun _ -> true) s sc in + GlobSearchSubPattern (where,head,Pattern.PRef ref) + with UserError _ -> + user_err ~hdr:"interp_search_item" + (str "Unable to interpret " ++ quote (str s) ++ str " as a reference.")) + | SearchKind k -> + match kind_searcher k with + | Inl k -> GlobSearchKind k + | Inr f -> GlobSearchFilter f + +let rec interp_search_request env sigma = function + | b, SearchLiteral i -> b, GlobSearchLiteral (interp_search_item env sigma i) + | b, SearchDisjConj l -> b, GlobSearchDisjConj (List.map (List.map (interp_search_request env sigma)) l) + +(* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the + `search_output_name_only` option to avoid excessive printing when + searching. + + The motivation was to make search usable for IDE completion, + however, it is still too slow due to the non-indexed nature of the + underlying search mechanism. + + In the future we should deprecate the option and provide a fast, + indexed name-searching interface. +*) +let search_output_name_only = ref false + +let () = + declare_bool_option + { optdepr = false; + optkey = ["Search";"Output";"Name";"Only"]; + optread = (fun () -> !search_output_name_only); + optwrite = (:=) search_output_name_only } + +let interp_search env sigma s r = + let r = interp_search_restriction r in + let get_pattern c = snd (Constrintern.intern_constr_pattern env sigma c) in + let warnlist = ref [] in + let pr_search ref kind env c = + let pr = pr_global ref in + let pp = if !search_output_name_only + then pr + else begin + let open Impargs in + let impls = implicits_of_global ref in + let impargs = select_stronger_impargs impls in + let impargs = List.map binding_kind_of_status impargs in + if List.length impls > 1 || + List.exists Glob_term.(function Explicit -> false | MaxImplicit | NonMaxImplicit -> true) + (List.skipn_at_least (Termops.nb_prod_modulo_zeta Evd.(from_env env) (EConstr.of_constr c)) impargs) + then warnlist := pr :: !warnlist; + let pc = pr_ltype_env env Evd.(from_env env) ~impargs c in + hov 2 (pr ++ str":" ++ spc () ++ pc) + end + in Feedback.msg_notice pp + in + (match s with + | SearchPattern c -> + (Search.search_pattern env sigma (get_pattern c) r |> Search.prioritize_search) pr_search + | SearchRewrite c -> + (Search.search_rewrite env sigma (get_pattern c) r |> Search.prioritize_search) pr_search + | SearchHead c -> + (Search.search_by_head env sigma (get_pattern c) r |> Search.prioritize_search) pr_search + | Search sl -> + (Search.search env sigma (List.map (interp_search_request env Evd.(from_env env)) sl) r |> + Search.prioritize_search) pr_search); + if !warnlist <> [] then + Feedback.msg_notice (str "(" ++ + hov 0 (strbrk "use \"About\" for full details on the implicit arguments of " ++ + pr_enum (fun x -> x) !warnlist ++ str ")")) diff --git a/vernac/comSearch.mli b/vernac/comSearch.mli new file mode 100644 index 0000000000..42f59984ff --- /dev/null +++ b/vernac/comSearch.mli @@ -0,0 +1,14 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* Evd.evar_map -> + Vernacexpr.searchable -> Vernacexpr.search_restriction -> unit diff --git a/vernac/search.ml b/vernac/search.ml index f6b5bbd8e9..2a21184c1e 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -141,7 +141,7 @@ module ConstrPriority = struct let num_symbols t = ConstrSet.(cardinal (symbols empty t)) - let priority t : priority = + let priority gref t : priority = -(3*(num_symbols t) + size t) let compare (_,_,_,_,p1) (_,_,_,_,p2) = @@ -167,7 +167,7 @@ let rec iter_priority_queue q fn = let prioritize_search seq fn = let acc = ref PriorityQueue.empty in let iter gref kind env t = - let p = ConstrPriority.priority t in + let p = ConstrPriority.priority gref t in acc := PriorityQueue.add (gref,kind,env,t,p) !acc in let () = seq iter in diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 618a61f487..a09a473afe 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -32,6 +32,7 @@ ComPrimitive ComAssumption DeclareInd Search +ComSearch Prettyp ComInductive ComFixpoint diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index ea79cf7465..35e625859b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1762,129 +1762,17 @@ let vernac_print ~pstate ~atts = | PrintStrategy r -> print_strategy r | PrintRegistered -> print_registered () -let global_module qid = - try Nametab.full_name_module qid - with Not_found -> - user_err ?loc:qid.CAst.loc ~hdr:"global_module" - (str "Module/section " ++ pr_qualid qid ++ str " not found.") - -let interp_search_restriction = function - | SearchOutside l -> (List.map global_module l, true) - | SearchInside l -> (List.map global_module l, false) - -open Search - -let kind_searcher = Decls.(function - (* Kinds referring to the keyword introducing the object *) - | IsAssumption _ - | IsDefinition (Definition | Example | Fixpoint | CoFixpoint | Method | StructureComponent | Let) - | IsProof _ - | IsPrimitive as k -> Inl k - (* Kinds referring to the status of the object *) - | IsDefinition (Coercion | SubClass | IdentityCoercion as k') -> - let coercions = Coercionops.coercions () in - Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Coercionops.coe_value gr && - (k' <> SubClass && k' <> IdentityCoercion || c.Coercionops.coe_is_identity)) coercions) - | IsDefinition CanonicalStructure -> - let canonproj = Recordops.canonical_projections () in - Inr (fun gr -> List.exists (fun c -> GlobRef.equal (snd c).Recordops.o_ORIGIN gr) canonproj) - | IsDefinition Scheme -> - let schemes = DeclareScheme.all_schemes () in - Inr (fun gr -> Indset.exists (fun c -> GlobRef.equal (GlobRef.IndRef c) gr) schemes) - | IsDefinition Instance -> - let instances = Typeclasses.all_instances () in - Inr (fun gr -> List.exists (fun c -> GlobRef.equal c.Typeclasses.is_impl gr) instances)) - -let interp_search_item env sigma = - function - | SearchSubPattern ((where,head),pat) -> - let _,pat = Constrintern.intern_constr_pattern env sigma pat in - GlobSearchSubPattern (where,head,pat) - | SearchString ((Anywhere,false),s,None) when Id.is_valid s -> - GlobSearchString s - | SearchString ((where,head),s,sc) -> - (try - let ref = - Notation.interp_notation_as_global_reference - ~head:false (fun _ -> true) s sc in - GlobSearchSubPattern (where,head,Pattern.PRef ref) - with UserError _ -> - user_err ~hdr:"interp_search_item" - (str "Unable to interpret " ++ quote (str s) ++ str " as a reference.")) - | SearchKind k -> - match kind_searcher k with - | Inl k -> GlobSearchKind k - | Inr f -> GlobSearchFilter f - -let rec interp_search_request env sigma = function - | b, SearchLiteral i -> b, GlobSearchLiteral (interp_search_item env sigma i) - | b, SearchDisjConj l -> b, GlobSearchDisjConj (List.map (List.map (interp_search_request env sigma)) l) - -(* 05f22a5d6d5b8e3e80f1a37321708ce401834430 introduced the - `search_output_name_only` option to avoid excessive printing when - searching. - - The motivation was to make search usable for IDE completion, - however, it is still too slow due to the non-indexed nature of the - underlying search mechanism. - - In the future we should deprecate the option and provide a fast, - indexed name-searching interface. -*) -let search_output_name_only = ref false - -let () = - declare_bool_option - { optdepr = false; - optkey = ["Search";"Output";"Name";"Only"]; - optread = (fun () -> !search_output_name_only); - optwrite = (:=) search_output_name_only } - let vernac_search ~pstate ~atts s gopt r = + let open ComSearch in let gopt = query_command_selector gopt in - let r = interp_search_restriction r in let sigma, env = match gopt with | None -> (* 1st goal by default if it exists, otherwise no goal at all *) (try get_goal_or_global_context ~pstate 1 with _ -> let env = Global.env () in (Evd.from_env env, env)) (* if goal selector is given and wrong, then let exceptions be raised. *) - | Some g -> get_goal_or_global_context ~pstate g - in - let get_pattern c = snd (Constrintern.intern_constr_pattern env sigma c) in - let warnlist = ref [] in - let pr_search ref kind env c = - let pr = pr_global ref in - let pp = if !search_output_name_only - then pr - else begin - let open Impargs in - let impls = implicits_of_global ref in - let impargs = select_stronger_impargs impls in - let impargs = List.map binding_kind_of_status impargs in - if List.length impls > 1 || - List.exists Glob_term.(function Explicit -> false | MaxImplicit | NonMaxImplicit -> true) - (List.skipn_at_least (Termops.nb_prod_modulo_zeta Evd.(from_env env) (EConstr.of_constr c)) impargs) - then warnlist := pr :: !warnlist; - let pc = pr_ltype_env env Evd.(from_env env) ~impargs c in - hov 2 (pr ++ str":" ++ spc () ++ pc) - end - in Feedback.msg_notice pp - in - (match s with - | SearchPattern c -> - (Search.search_pattern env sigma (get_pattern c) r |> Search.prioritize_search) pr_search - | SearchRewrite c -> - (Search.search_rewrite env sigma (get_pattern c) r |> Search.prioritize_search) pr_search - | SearchHead c -> - (Search.search_by_head env sigma (get_pattern c) r |> Search.prioritize_search) pr_search - | Search sl -> - (Search.search env sigma (List.map (interp_search_request env Evd.(from_env env)) sl) r |> - Search.prioritize_search) pr_search); - if !warnlist <> [] then - Feedback.msg_notice (str "(" ++ - hov 0 (strbrk "use \"About\" for full details on the implicit arguments of " ++ - pr_enum (fun x -> x) !warnlist ++ str ")")) + | Some g -> get_goal_or_global_context ~pstate g in + interp_search env sigma s r let vernac_locate ~pstate = let open Constrexpr in function | LocateAny {v=AN qid} -> Prettyp.print_located_qualid qid -- cgit v1.2.3 From eae7b25e06b75f1c890215d4e6176292f10f854a Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 12 May 2020 11:30:25 +0200 Subject: Deprecate SearchHead. The main use case of SearchHead is now handled by headconcl: The secondary use case was redundant with SearchPattern. --- vernac/comSearch.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'vernac') diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml index a860bc8bf6..9de8d6fbc3 100644 --- a/vernac/comSearch.ml +++ b/vernac/comSearch.ml @@ -95,6 +95,12 @@ let () = optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } +let deprecated_searchhead = + CWarnings.create + ~name:"deprecated-searchhead" + ~category:"deprecated" + (fun () -> Pp.str("SearchHead is deprecated. Use the headconcl: clause of Search instead.")) + let interp_search env sigma s r = let r = interp_search_restriction r in let get_pattern c = snd (Constrintern.intern_constr_pattern env sigma c) in @@ -123,6 +129,7 @@ let interp_search env sigma s r = | SearchRewrite c -> (Search.search_rewrite env sigma (get_pattern c) r |> Search.prioritize_search) pr_search | SearchHead c -> + deprecated_searchhead (); (Search.search_by_head env sigma (get_pattern c) r |> Search.prioritize_search) pr_search | Search sl -> (Search.search env sigma (List.map (interp_search_request env Evd.(from_env env)) sl) r |> -- cgit v1.2.3