summaryrefslogtreecommitdiff
path: root/toplevel/search.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/search.ml')
-rw-r--r--toplevel/search.ml465
1 files changed, 278 insertions, 187 deletions
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 28c14a77..59283edf 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -9,19 +9,23 @@
open Pp
open Util
open Names
-open Nameops
open Term
-open Glob_term
open Declarations
open Libobject
-open Declare
open Environ
open Pattern
-open Matching
open Printer
open Libnames
+open Globnames
open Nametab
+type filter_function = global_reference -> env -> constr -> bool
+type display_function = global_reference -> env -> constr -> unit
+
+type glob_search_about_item =
+ | GlobSearchSubPattern of constr_pattern
+ | GlobSearchString of string
+
module SearchBlacklist =
Goptions.MakeStringTable
(struct
@@ -32,215 +36,302 @@ module SearchBlacklist =
let synchronous = true
end)
-(* The functions print_constructors and crible implement the behavior needed
- for the Coq searching commands.
+(* The functions iter_constructors and iter_declarations implement the behavior
+ needed for the Coq searching commands.
These functions take as first argument the procedure
that will be called to treat each entry. This procedure receives the name
of the object, the assumptions that will make it possible to print its type,
and the constr term that represent its type. *)
-let print_constructors indsp fn env nconstr =
+let iter_constructors indsp u fn env nconstr =
for i = 1 to nconstr do
- fn (ConstructRef (indsp,i)) env (Inductiveops.type_of_constructor env (indsp,i))
+ let typ = Inductiveops.type_of_constructor env ((indsp, i), u) in
+ fn (ConstructRef (indsp, i)) env typ
done
-let rec head_const c = match kind_of_term c with
- | Prod (_,_,d) -> head_const d
- | LetIn (_,_,_,d) -> head_const d
- | App (f,_) -> head_const f
- | Cast (d,_,_) -> head_const d
- | _ -> c
+let iter_named_context_name_type f = List.iter (fun (nme,_,typ) -> f nme typ)
-(* General search, restricted to head constant if [only_head] *)
+(* General search over hypothesis of a goal *)
+let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
+ let env = Global.env () in
+ let iter_hyp idh typ = fn (VarRef idh) env typ in
+ let evmap,e = Pfedit.get_goal_context glnum in
+ let pfctxt = named_context e in
+ iter_named_context_name_type iter_hyp pfctxt
-let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
+(* General search over declarations *)
+let iter_declarations (fn : global_reference -> env -> constr -> unit) =
let env = Global.env () in
- let crible_rec (sp,kn) lobj = match object_tag lobj with
- | "VARIABLE" ->
- (try
- let (id,_,typ) = Global.lookup_named (basename sp) in
- if refopt = None
- || head_const typ = constr_of_global (Option.get refopt)
- then
- fn (VarRef id) env typ
- with Not_found -> (* we are in a section *) ())
- | "CONSTANT" ->
- let cst = Global.constant_of_delta_kn kn in
- let typ = Typeops.type_of_constant env cst in
- if refopt = None
- || head_const typ = constr_of_global (Option.get refopt)
- then
- fn (ConstRef cst) env typ
- | "INDUCTIVE" ->
- let mind = Global.mind_of_delta_kn kn in
- let mib = Global.lookup_mind mind in
- (match refopt with
- | Some (IndRef ((kn',tyi) as ind)) when eq_mind mind kn' ->
- print_constructors ind fn env
- (Array.length (mib.mind_packets.(tyi).mind_user_lc))
- | Some _ -> ()
- | _ ->
- Array.iteri
- (fun i mip -> print_constructors (mind,i) fn env
- (Array.length mip.mind_user_lc)) mib.mind_packets)
- | _ -> ()
+ 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
+ with Not_found -> (* we are in a section *) () end
+ | "CONSTANT" ->
+ let cst = Global.constant_of_delta_kn kn in
+ let gr = ConstRef cst in
+ let typ = Global.type_of_global_unsafe gr in
+ fn gr env typ
+ | "INDUCTIVE" ->
+ let mind = Global.mind_of_delta_kn kn in
+ let mib = Global.lookup_mind mind in
+ let iter_packet i mip =
+ let ind = (mind, i) in
+ let u = Declareops.inductive_instance mib in
+ let i = (ind, u) in
+ let typ = Inductiveops.type_of_inductive env i in
+ let () = fn (IndRef ind) env typ in
+ let len = Array.length mip.mind_user_lc in
+ iter_constructors ind u fn env len
+ in
+ Array.iteri iter_packet mib.mind_packets
+ | _ -> ()
in
- try
- Declaremods.iter_all_segments crible_rec
- with Not_found ->
- ()
-
-let crible ref = gen_crible (Some ref)
-
-(* Fine Search. By Yves Bertot. *)
+ try Declaremods.iter_all_segments iter_obj
+ with Not_found -> ()
-exception No_full_path
+let generic_search glnumopt fn =
+ (match glnumopt with
+ | None -> ()
+ | Some glnum -> iter_hypothesis glnum fn);
+ iter_declarations fn
-let rec head c =
- let c = strip_outer_cast c in
- match kind_of_term c with
- | Prod (_,_,c) -> head c
- | LetIn (_,_,_,c) -> head c
- | _ -> c
+(** Standard display *)
-let xor a b = (a or b) & (not (a & b))
-
-let plain_display ref a c =
- let pc = pr_lconstr_env a c in
+let plain_display accu ref env c =
+ let pc = pr_lconstr_env env Evd.empty c in
let pr = pr_global ref in
- msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ())
-
-let filter_by_module (module_list:dir_path list) (accept:bool)
- (ref:global_reference) _ _ =
- try
- let sp = path_of_global ref in
- let sl = dirpath sp in
- let rec filter_aux = function
- | m :: tl -> (not (is_dirpath_prefix_of m sl)) && (filter_aux tl)
- | [] -> true
- in
- xor accept (filter_aux module_list)
- with No_full_path ->
- false
-
-let ref_eq = Libnames.encode_mind Coqlib.logic_module (id_of_string "eq"), 0
-let c_eq = mkInd ref_eq
-let gref_eq = IndRef ref_eq
-
-let mk_rewrite_pattern1 eq pattern =
- PApp (PRef eq, [| PMeta None; pattern; PMeta None |])
-
-let mk_rewrite_pattern2 eq pattern =
- PApp (PRef eq, [| PMeta None; PMeta None; pattern |])
-
-let pattern_filter pat _ a c =
- try
- try
- is_matching pat (head c)
- with e when Errors.noncritical e ->
- is_matching
- pat (head (Typing.type_of (Global.env()) Evd.empty c))
- with UserError _ ->
- false
-
-let filtered_search filter_function display_function ref =
- crible ref
- (fun s a c -> if filter_function s a c then display_function s a c)
-
-let rec id_from_pattern = function
- | PRef gr -> gr
-(* should be appear as a PRef (VarRef sp) !!
- | PVar id -> Nametab.locate (make_qualid [] (string_of_id id))
- *)
- | PApp (p,_) -> id_from_pattern p
- | _ -> error "The pattern is not simple enough."
-
-let raw_pattern_search extra_filter display_function pat =
- let name = id_from_pattern pat in
- filtered_search
- (fun s a c -> (pattern_filter pat s a c) & extra_filter s a c)
- display_function name
-
-let raw_search_rewrite extra_filter display_function pattern =
- filtered_search
- (fun s a c ->
- ((pattern_filter (mk_rewrite_pattern1 gref_eq pattern) s a c) ||
- (pattern_filter (mk_rewrite_pattern2 gref_eq pattern) s a c))
- && extra_filter s a c)
- display_function gref_eq
-
-let raw_search_by_head extra_filter display_function pattern =
- Util.todo "raw_search_by_head"
-
-let name_of_reference ref = string_of_id (basename_of_global ref)
+ 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. *)
+(** FIXME: this is quite dummy, we may find a more efficient algorithm. *)
+let rec pattern_filter pat ref env typ =
+ let typ = strip_outer_cast typ in
+ if Constr_matching.is_matching env Evd.empty pat typ then true
+ else match kind_of_term typ with
+ | Prod (_, _, typ)
+ | LetIn (_, _, _, typ) -> pattern_filter pat ref env typ
+ | _ -> false
+
+let rec head_filter pat ref env typ =
+ let typ = strip_outer_cast typ in
+ if Constr_matching.is_matching_head env Evd.empty pat typ then true
+ else match kind_of_term typ with
+ | Prod (_, _, typ)
+ | LetIn (_, _, _, typ) -> head_filter pat ref env typ
+ | _ -> false
let full_name_of_reference ref =
let (dir,id) = repr_path (path_of_global ref) in
- string_of_dirpath dir ^ "." ^ string_of_id id
-
-(*
- * functions to use the new Libtypes facility
- *)
+ DirPath.to_string dir ^ "." ^ Id.to_string id
-let raw_search search_function extra_filter display_function pat =
- let env = Global.env() in
- List.iter
- (fun (gr,_,_) ->
- let typ = Global.type_of_global gr in
- if extra_filter gr env typ then
- display_function gr env typ
- ) (search_function pat)
-
-let text_pattern_search extra_filter =
- raw_search Libtypes.search_concl extra_filter plain_display
-
-let text_search_rewrite extra_filter =
- raw_search (Libtypes.search_eq_concl c_eq) extra_filter plain_display
-
-let text_search_by_head extra_filter =
- raw_search Libtypes.search_head_concl extra_filter plain_display
-
-let filter_by_module_from_list = function
- | [], _ -> (fun _ _ _ -> true)
- | l, outside -> filter_by_module l (not outside)
-
-let filter_blacklist gr _ _ =
- let name = full_name_of_reference gr in
+(** Whether a reference is blacklisted *)
+let blacklist_filter ref env typ =
let l = SearchBlacklist.elements () in
- List.for_all (fun str -> not (string_string_contains ~where:name ~what:str)) l
+ 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
+
+let module_filter (mods, outside) ref env typ =
+ let sp = path_of_global ref in
+ let sl = dirpath sp in
+ let is_outside md = not (is_dirpath_prefix_of md sl) in
+ let is_inside md = is_dirpath_prefix_of md sl in
+ if outside then List.for_all is_outside mods
+ else List.is_empty mods || List.exists is_inside mods
+
+let name_of_reference ref = Id.to_string (basename_of_global ref)
+
+let search_about_filter query gr env typ = match query with
+| GlobSearchSubPattern pat ->
+ Constr_matching.is_matching_appsubterm ~closed:false env Evd.empty pat typ
+| GlobSearchString s ->
+ String.string_contains ~where:(name_of_reference gr) ~what:s
+
+
+(** SearchPattern *)
+
+let search_pattern gopt pat mods =
+ let ans = ref [] 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
+ in
+ let iter ref env typ =
+ if filter ref env typ then plain_display ans ref env typ
+ in
+ let () = generic_search gopt iter in
+ format_display !ans
-let (&&&&&) f g x y z = f x y z && g x y z
+(** SearchRewrite *)
-let search_by_head pat inout =
- text_search_by_head (filter_by_module_from_list inout &&&&& filter_blacklist) pat
+let eq = Coqlib.glob_eq
-let search_rewrite pat inout =
- text_search_rewrite (filter_by_module_from_list inout &&&&& filter_blacklist) pat
+let rewrite_pat1 pat =
+ PApp (PRef eq, [| PMeta None; pat; PMeta None |])
-let search_pattern pat inout =
- text_pattern_search (filter_by_module_from_list inout &&&&& filter_blacklist) pat
+let rewrite_pat2 pat =
+ PApp (PRef eq, [| PMeta None; PMeta None; pat |])
-let gen_filtered_search filter_function display_function =
- gen_crible None
- (fun s a c -> if filter_function s a c then display_function s a c)
+let search_rewrite gopt pat mods =
+ let pat1 = rewrite_pat1 pat in
+ let pat2 = rewrite_pat2 pat in
+ let ans = ref [] 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
+ in
+ let iter ref env typ =
+ if filter ref env typ then plain_display ans ref env typ
+ in
+ let () = generic_search gopt iter in
+ format_display !ans
+
+(** Search *)
+
+let search_by_head gopt pat mods =
+ let ans = ref [] 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
+ in
+ let iter ref env typ =
+ if filter ref env typ then plain_display ans ref env typ
+ in
+ let () = generic_search gopt iter in
+ format_display !ans
(** SearchAbout *)
-type glob_search_about_item =
- | GlobSearchSubPattern of constr_pattern
- | GlobSearchString of string
-
-let search_about_item (itemref,typ) = function
- | GlobSearchSubPattern pat -> is_matching_appsubterm ~closed:false pat typ
- | GlobSearchString s -> string_string_contains ~where:(name_of_reference itemref) ~what:s
-
-let raw_search_about filter_modules display_function l =
- let filter ref' env typ =
- filter_modules ref' env typ &&
- List.for_all (fun (b,i) -> b = search_about_item (ref',typ) i) l &&
- filter_blacklist ref' () ()
+let search_about gopt items mods =
+ let ans = ref [] 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
in
- gen_filtered_search filter display_function
-
-let search_about ref inout =
- raw_search_about (filter_by_module_from_list inout) plain_display ref
+ let iter ref env typ =
+ if filter ref env typ then plain_display ans ref env typ
+ in
+ let () = generic_search gopt iter in
+ format_display !ans
+
+type search_constraint =
+ | Name_Pattern of string
+ | Type_Pattern of string
+ | SubType_Pattern of string
+ | In_Module of string list
+ | Include_Blacklist
+
+type 'a coq_object = {
+ coq_object_prefix : string list;
+ coq_object_qualid : string list;
+ coq_object_object : 'a;
+}
+
+let interface_search flags =
+ let env = Global.env () in
+ 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.error ("Invalid regexp: " ^ s)
+ in
+ 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
+ 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
+ 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.error ("Module " ^ path ^ " not found.")
+ in
+ extract_flags name tpe subtpe ((id, b) :: mods) blacklist l
+ | (Include_Blacklist, b) :: l ->
+ extract_flags name tpe subtpe mods b l
+ in
+ let (name, tpe, subtpe, mods, blacklist) =
+ extract_flags [] [] [] [] false flags
+ 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
+ let toggle x b = if x then b else not b in
+ let match_name (regexp, flag) =
+ toggle (Str.string_match regexp id 0) flag
+ in
+ let match_type (pat, flag) =
+ toggle (Constr_matching.is_matching env Evd.empty pat constr) flag
+ in
+ let match_subtype (pat, flag) =
+ toggle
+ (Constr_matching.is_matching_appsubterm ~closed:false
+ env Evd.empty pat constr) flag
+ in
+ 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
+ in
+ let ans = ref [] in
+ let print_function ref env constr =
+ let fullpath = DirPath.repr (Nametab.dirpath_of_global ref) in
+ let qualid = Nametab.shortest_qualid_of_global Id.Set.empty ref in
+ let (shortpath, basename) = Libnames.repr_qualid qualid in
+ let shortpath = DirPath.repr shortpath in
+ (* [shortpath] is a suffix of [fullpath] and we're looking for the missing
+ prefix *)
+ let rec prefix full short accu = match full, short with
+ | _, [] ->
+ let full = List.rev_map Id.to_string full in
+ (full, accu)
+ | _ :: full, m :: short ->
+ prefix full short (Id.to_string m :: accu)
+ | _ -> assert false
+ in
+ let (prefix, qualid) = prefix fullpath shortpath [Id.to_string basename] in
+ let answer = {
+ coq_object_prefix = prefix;
+ coq_object_qualid = qualid;
+ coq_object_object = string_of_ppcmds (pr_lconstr_env env Evd.empty constr);
+ } in
+ ans := answer :: !ans;
+ in
+ 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? *)
+ !ans
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-27 07:52:52 +0000