Searchxxx now search also the hypothesis and support goal selector.

Documentation also updated.

3 files changed, 45 insertions, 25 deletions

diff --git a/toplevel/search.ml b/toplevel/search.ml
index 9632e1c79e..8336b488a1 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -49,6 +49,18 @@ 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) 
+
+(* General search over hypothesis of a goal *)
+let iter_hypothesis glnum (fn : global_reference -> env -> constr -> unit) =
+  try
+    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
+  with _ -> ()
+
 (* General search over declarations *)
 let iter_declarations (fn : global_reference -> env -> constr -> unit) =
   let env = Global.env () in
@@ -81,7 +93,9 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) =
   try Declaremods.iter_all_segments iter_obj
   with Not_found -> ()
 
-let generic_search = iter_declarations
+let generic_search glnum fn =
+  iter_hypothesis glnum fn;
+  iter_declarations fn
 
 (** Standard display *)
 
@@ -118,8 +132,8 @@ let full_name_of_reference ref =
 
 (** Whether a reference is blacklisted *)
 let blacklist_filter ref env typ =
-  let name = full_name_of_reference ref in
   let l = SearchBlacklist.elements () in
+  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
 
@@ -142,7 +156,7 @@ let search_about_filter query gr env typ = match query with
 
 (** SearchPattern *)
 
-let search_pattern pat mods =
+let search_pattern g pat mods =
   let ans = ref [] in
   let filter ref env typ =
     let f_module = module_filter mods ref env typ in
@@ -153,7 +167,7 @@ let search_pattern pat mods =
   let iter ref env typ =
     if filter ref env typ then plain_display ans ref env typ
   in
-  let () = generic_search iter in
+  let () = generic_search g iter in
   format_display !ans
 
 (** SearchRewrite *)
@@ -166,7 +180,7 @@ let rewrite_pat1 pat =
 let rewrite_pat2 pat =
   PApp (PRef eq, [| PMeta None; PMeta None; pat |])
 
-let search_rewrite pat mods =
+let search_rewrite g pat mods =
   let pat1 = rewrite_pat1 pat in
   let pat2 = rewrite_pat2 pat in
   let ans = ref [] in
@@ -182,12 +196,12 @@ let search_rewrite pat mods =
   let iter ref env typ =
     if filter ref env typ then plain_display ans ref env typ
   in
-  let () = generic_search iter in
+  let () = generic_search g iter in
   format_display !ans
 
 (** Search *)
 
-let search_by_head pat mods =
+let search_by_head g pat mods =
   let ans = ref [] in
   let filter ref env typ =
     let f_module = module_filter mods ref env typ in
@@ -198,12 +212,12 @@ let search_by_head pat mods =
   let iter ref env typ =
     if filter ref env typ then plain_display ans ref env typ
   in
-  let () = generic_search iter in
+  let () = generic_search g iter in
   format_display !ans
 
 (** SearchAbout *)
 
-let search_about items mods =
+let search_about g items mods =
   let ans = ref [] in
   let filter ref env typ =
     let eqb b1 b2 = if b1 then b2 else not b2 in
@@ -215,7 +229,7 @@ let search_about items mods =
   let iter ref env typ =
     if filter ref env typ then plain_display ans ref env typ
   in
-  let () = generic_search iter in
+  let () = generic_search g iter in
   format_display !ans
 
 type search_constraint =
@@ -319,5 +333,5 @@ 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 iter in
+  let () = generic_search 1 iter in (* TODO: chose a goal number? *)
   !ans
diff --git a/toplevel/search.mli b/toplevel/search.mli
index a69a8db79c..f5d1d13ed2 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -33,13 +33,17 @@ val module_filter : DirPath.t list * bool -> filter_function
 val search_about_filter : glob_search_about_item -> filter_function
 (** Check whether a reference matches a SearchAbout query. *)
 
-(** {6 Specialized search functions} *)
+(** {6 Specialized search functions}
 
-val search_by_head : constr_pattern -> DirPath.t list * bool -> std_ppcmds
-val search_rewrite : constr_pattern -> DirPath.t list * bool -> std_ppcmds
-val search_pattern : constr_pattern -> DirPath.t list * bool -> std_ppcmds
-val search_about   : (bool * glob_search_about_item) list ->
-  DirPath.t list * bool -> std_ppcmds
+[search_xxx gl pattern modinout] searches the hypothesis of the [gl]th
+goal and the global environment for things matching [pattern] and
+satisfying module exclude/include clauses of [modinout]. *)
+
+val search_by_head : int -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
+val search_rewrite : int -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
+val search_pattern : int -> constr_pattern -> DirPath.t list * bool -> std_ppcmds
+val search_about   : int -> (bool * glob_search_about_item) list
+  -> DirPath.t list * bool -> std_ppcmds
 
 type search_constraint =
   (** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
@@ -64,5 +68,6 @@ val interface_search : (search_constraint * bool) list ->
 
 (** {6 Generic search function} *)
 
-val generic_search : display_function -> unit
-(** This function iterates over all known declarations *)
+val generic_search : int -> display_function -> unit
+(** This function iterates over all hypothesis of the goal numbered
+    [glnum] (if present) and all known declarations. *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 93c12c3351..8fb2d320ca 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1610,19 +1610,20 @@ let interp_search_about_item = function
 	error ("Unable to interp \""^s^"\" either as a reference or \
           	as an identifier component")
 
-let vernac_search s r =
+let vernac_search s gopt r =
+  let g = un_opt gopt 1 in
   let r = interp_search_restriction r in
   let env = Global.env () in
   let get_pattern c = snd (Constrintern.intern_constr_pattern env c) in
   match s with
   | SearchPattern c ->
-      msg_notice (Search.search_pattern (get_pattern c) r)
+      msg_notice (Search.search_pattern g (get_pattern c) r)
   | SearchRewrite c ->
-      msg_notice (Search.search_rewrite (get_pattern c) r)
+      msg_notice (Search.search_rewrite g (get_pattern c) r)
   | SearchHead c ->
-      msg_notice (Search.search_by_head (get_pattern c) r)
+      msg_notice (Search.search_by_head g (get_pattern c) r)
   | SearchAbout sl ->
-      msg_notice (Search.search_about (List.map (on_snd interp_search_about_item) sl) r)
+     msg_notice (Search.search_about g (List.map (on_snd interp_search_about_item) sl) r)
 
 let vernac_locate = function
   | LocateAny (AN qid) -> msg_notice (print_located_qualid qid)
@@ -1886,7 +1887,7 @@ let interp ?proof locality poly c =
   | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r
   | VernacGlobalCheck c -> vernac_global_check c
   | VernacPrint p -> vernac_print p
-  | VernacSearch (s,r) -> vernac_search s r
+  | VernacSearch (s,g,r) -> vernac_search s g r
   | VernacLocate l -> vernac_locate l
   | VernacRegister (id, r) -> vernac_register id r
   | VernacComments l -> if_verbose msg_info (str "Comments ok\n")