From 1b92c226e563643da187b8614d5888dc4855eb43 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- toplevel/search.ml | 148 ++++++++++++++++++++++------------------------------- 1 file changed, 62 insertions(+), 86 deletions(-) (limited to 'toplevel/search.ml') 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 -- cgit v1.2.3