summaryrefslogtreecommitdiff
path: root/toplevel/search.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/search.ml')
-rw-r--r--toplevel/search.ml148
1 files changed, 62 insertions, 86 deletions
diff --git a/toplevel/search.ml b/toplevel/search.ml
index d7a4cbe7..ff3c7a4f 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -18,10 +18,17 @@ open Printer
open Libnames
open Globnames
open Nametab
+open Goptions
type filter_function = global_reference -> env -> constr -> bool
type display_function = global_reference -> env -> constr -> unit
+(* This option restricts the output of [SearchPattern ...],
+[SearchAbout ...], etc. to the names of the symbols matching the
+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 thorugh the types of all symbols. *)
+
type glob_search_about_item =
| GlobSearchSubPattern of constr_pattern
| GlobSearchString of string
@@ -49,7 +56,9 @@ let iter_constructors indsp u fn env nconstr =
fn (ConstructRef (indsp, i)) env typ
done
-let iter_named_context_name_type f = List.iter (fun (nme,_,typ) -> f nme typ)
+let iter_named_context_name_type f =
+ let open Context.Named.Declaration in
+ List.iter (fun decl -> f (get_id decl) (get_type decl))
(* General search over hypothesis of a goal *)
let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
@@ -61,12 +70,13 @@ let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
(* General search over declarations *)
let iter_declarations (fn : global_reference -> env -> constr -> unit) =
+ let open Context.Named.Declaration in
let env = Global.env () in
let iter_obj (sp, kn) lobj = match object_tag lobj with
| "VARIABLE" ->
begin try
- let (id, _, typ) = Global.lookup_named (basename sp) in
- fn (VarRef id) env typ
+ let decl = Global.lookup_named (basename sp) in
+ fn (VarRef (get_id decl)) env (get_type decl)
with Not_found -> (* we are in a section *) () end
| "CONSTANT" ->
let cst = Global.constant_of_delta_kn kn in
@@ -97,15 +107,6 @@ let generic_search glnumopt fn =
| Some glnum -> iter_hypothesis glnum fn);
iter_declarations fn
-(** Standard display *)
-
-let plain_display accu ref env c =
- let pc = pr_lconstr_env env Evd.empty c in
- let pr = pr_global ref in
- accu := hov 2 (pr ++ str":" ++ spc () ++ pc) :: !accu
-
-let format_display l = prlist_with_sep fnl (fun x -> x) (List.rev l)
-
(** Filters *)
(** This function tries to see whether the conclusion matches a pattern. *)
@@ -131,8 +132,9 @@ 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_aux () =
let l = SearchBlacklist.elements () in
+ fun 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
@@ -156,19 +158,17 @@ let search_about_filter query gr env typ = match query with
(** SearchPattern *)
-let search_pattern gopt pat mods =
- let ans = ref [] in
+let search_pattern gopt pat mods pr_search =
+ let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
- let f_module = module_filter mods ref env typ in
- let f_blacklist = blacklist_filter ref env typ in
- let f_pattern () = pattern_filter pat ref env typ in
- f_module && f_pattern () && f_blacklist
+ module_filter mods ref env typ &&
+ pattern_filter pat ref env typ &&
+ blacklist_filter ref env typ
in
let iter ref env typ =
- if filter ref env typ then plain_display ans ref env typ
+ if filter ref env typ then pr_search ref env typ
in
- let () = generic_search gopt iter in
- format_display !ans
+ generic_search gopt iter
(** SearchRewrite *)
@@ -180,63 +180,56 @@ let rewrite_pat1 pat =
let rewrite_pat2 pat =
PApp (PRef eq, [| PMeta None; PMeta None; pat |])
-let search_rewrite gopt pat mods =
+let search_rewrite gopt pat mods pr_search =
let pat1 = rewrite_pat1 pat in
let pat2 = rewrite_pat2 pat in
- let ans = ref [] in
+ let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
- let f_module = module_filter mods ref env typ in
- let f_blacklist = blacklist_filter ref env typ in
- let f_pattern () =
- pattern_filter pat1 ref env typ ||
- pattern_filter pat2 ref env typ
- in
- f_module && f_pattern () && f_blacklist
+ module_filter mods ref env typ &&
+ (pattern_filter pat1 ref env typ ||
+ pattern_filter pat2 ref env typ) &&
+ blacklist_filter ref env typ
in
let iter ref env typ =
- if filter ref env typ then plain_display ans ref env typ
+ if filter ref env typ then pr_search ref env typ
in
- let () = generic_search gopt iter in
- format_display !ans
+ generic_search gopt iter
(** Search *)
-let search_by_head gopt pat mods =
- let ans = ref [] in
+let search_by_head gopt pat mods pr_search =
+ let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
- let f_module = module_filter mods ref env typ in
- let f_blacklist = blacklist_filter ref env typ in
- let f_pattern () = head_filter pat ref env typ in
- f_module && f_pattern () && f_blacklist
+ module_filter mods ref env typ &&
+ head_filter pat ref env typ &&
+ blacklist_filter ref env typ
in
let iter ref env typ =
- if filter ref env typ then plain_display ans ref env typ
+ if filter ref env typ then pr_search ref env typ
in
- let () = generic_search gopt iter in
- format_display !ans
+ generic_search gopt iter
(** SearchAbout *)
-let search_about gopt items mods =
- let ans = ref [] in
+let search_about 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
- let f_module = module_filter mods ref env typ in
- let f_about (b, i) = eqb b (search_about_filter i ref env typ) in
- let f_blacklist = blacklist_filter ref env typ in
- f_module && List.for_all f_about items && f_blacklist
+ module_filter mods ref env typ &&
+ List.for_all
+ (fun (b,i) -> eqb b (search_about_filter i ref env typ)) items &&
+ blacklist_filter ref env typ
in
let iter ref env typ =
- if filter ref env typ then plain_display ans ref env typ
+ if filter ref env typ then pr_search ref env typ
in
- let () = generic_search gopt iter in
- format_display !ans
+ generic_search gopt iter
type search_constraint =
- | Name_Pattern of string
- | Type_Pattern of string
- | SubType_Pattern of string
- | In_Module of string list
+ | Name_Pattern of Str.regexp
+ | Type_Pattern of Pattern.constr_pattern
+ | SubType_Pattern of Pattern.constr_pattern
+ | In_Module of Names.DirPath.t
| Include_Blacklist
type 'a coq_object = {
@@ -245,43 +238,25 @@ type 'a coq_object = {
coq_object_object : 'a;
}
-let interface_search flags =
- let env = Global.env () in
+let interface_search =
let rec extract_flags name tpe subtpe mods blacklist = function
| [] -> (name, tpe, subtpe, mods, blacklist)
- | (Name_Pattern s, b) :: l ->
- let regexp =
- try Str.regexp s
- with e when Errors.noncritical e ->
- Errors.errorlabstrm "Search.interface_search"
- (str "Invalid regexp: " ++ str s)
- in
+ | (Name_Pattern regexp, b) :: l ->
extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
- | (Type_Pattern s, b) :: l ->
- let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
- let (_, pat) = Constrintern.intern_constr_pattern env constr in
+ | (Type_Pattern pat, b) :: l ->
extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l
- | (SubType_Pattern s, b) :: l ->
- let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
- let (_, pat) = Constrintern.intern_constr_pattern env constr in
+ | (SubType_Pattern pat, b) :: l ->
extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l
- | (In_Module m, b) :: l ->
- let path = String.concat "." m in
- let m = Pcoq.parse_string Pcoq.Constr.global path in
- let (_, qid) = Libnames.qualid_of_reference m in
- let id =
- try Nametab.full_name_module qid
- with Not_found ->
- Errors.errorlabstrm "Search.interface_search"
- (str "Module " ++ str path ++ str " not found.")
- in
+ | (In_Module id, b) :: l ->
extract_flags name tpe subtpe ((id, b) :: mods) blacklist l
| (Include_Blacklist, b) :: l ->
extract_flags name tpe subtpe mods b l
in
+ fun ?glnum flags ->
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
@@ -300,13 +275,11 @@ let interface_search flags =
let match_module (mdl, flag) =
toggle (Libnames.is_dirpath_prefix_of mdl path) flag
in
- let in_blacklist =
- blacklist || (blacklist_filter ref env constr)
- in
List.for_all match_name name &&
List.for_all match_type tpe &&
List.for_all match_subtype subtpe &&
- List.for_all match_module mods && in_blacklist
+ List.for_all match_module mods &&
+ (blacklist || blacklist_filter ref env constr)
in
let ans = ref [] in
let print_function ref env constr =
@@ -335,5 +308,8 @@ let interface_search flags =
let iter ref env typ =
if filter_function ref env typ then print_function ref env typ
in
- let () = generic_search None iter in (* TODO: chose a goal number? *)
+ let () = generic_search glnum iter in
!ans
+
+let blacklist_filter ref env typ =
+ blacklist_filter_aux () ref env typ
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-05 21:23:11 +0000