diff options
| -rw-r--r-- | vernac/comSearch.ml | 133 | ||||
| -rw-r--r-- | vernac/comSearch.mli | 14 | ||||
| -rw-r--r-- | vernac/search.ml | 4 | ||||
| -rw-r--r-- | vernac/vernac.mllib | 1 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 118 |
5 files changed, 153 insertions, 117 deletions
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 *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Interpretation of search commands *) + +open CErrors +open Names +open Util +open Pp +open Printer +open Search +open Vernacexpr +open Goptions + +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 " ++ 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 *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* Interpretation of search commands *) + +val interp_search : Environ.env -> 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 |