SearchAbout

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3489 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 56 insertions, 8 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 272ca09f50..9ddf7268a3 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1373,7 +1373,8 @@ let xlate_vernac =
 	    CT_search_pattern(xlate_formula c, xlate_search_restr x)
 	| SearchHead id ->
 	    CT_search(loc_qualid_to_ct_ID id, xlate_search_restr x)
-	| SearchRewrite c -> xlate_error "TODO: SearchRewrite")
+	| SearchRewrite c -> xlate_error "TODO: SearchRewrite"
+	| SearchAbout id -> xlate_error "TODO: SearchAbout")
 
   | (*Record from tactics/Record.v *)
     VernacRecord 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index c9f753a38b..683b2ae54b 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -88,6 +88,8 @@ GEXTEND Gram
 	  VernacSearch (SearchPattern c, l)
       | IDENT "SearchRewrite"; c = constr_pattern; l = in_or_out_modules ->
 	  VernacSearch (SearchRewrite c, l)
+      | IDENT "SearchAbout"; qid = global; l = in_or_out_modules -> 
+	  VernacSearch (SearchAbout qid, l)
 
       (* TODO: rapprocher Eval et Check *)
       | IDENT "Eval"; r = Tactic.red_expr; "in";
diff --git a/parsing/search.ml b/parsing/search.ml
index c1e897fd05..831c7e13ea 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -33,11 +33,11 @@ open Nametab
 
 let print_constructors indsp fn env mip =
   let lc = mip.mind_user_lc in
-  for i=1 to Array.length lc do
-      fn (ConstructRef (indsp,i)) env
-	(Retyping.get_type_of env Evd.empty
-	   (Pretyping.understand Evd.empty env
-	      (RRef(dummy_loc, ConstructRef(indsp,i)))))
+  for i = 1 to Array.length lc do
+    fn (ConstructRef (indsp,i)) env
+      (Retyping.get_type_of env Evd.empty
+	 (Pretyping.understand Evd.empty env
+	    (RRef(dummy_loc, ConstructRef(indsp,i)))))
   done
 
 let rec head_const c = match kind_of_term c with
@@ -59,11 +59,11 @@ let crible (fn : global_reference -> env -> constr -> unit) ref =
              if (head_const typ) = const then fn (VarRef idc) env typ
 	   with Not_found -> (* we are in a section *) ())
       | "CONSTANT" ->
-	  let kn=locate_constant (qualid_of_sp sp) in
+	  let kn = locate_constant (qualid_of_sp sp) in
 	  let {const_type=typ} = Global.lookup_constant kn in
 	  if (head_const typ) = const then fn (ConstRef kn) env typ
       | "INDUCTIVE" -> 
-	  let kn=locate_mind (qualid_of_sp sp) in
+	  let kn = locate_mind (qualid_of_sp sp) in
           let mib = Global.lookup_mind kn in 
 (*	  let arities =
 	    array_map_to_list 
@@ -191,3 +191,44 @@ let search_pattern pat inout =
   text_pattern_search (filter_by_module_from_list inout) pat
 
 
+(* General search, not restricted to head constant *)
+
+let gen_crible (fn : global_reference -> env -> constr -> unit) =
+  let env = Global.env () in
+  let imported = Library.opened_libraries() in
+  let crible_rec (sp,_) lobj = match object_tag lobj with
+    | "VARIABLE" ->
+	(try 
+	   let (idc,_,typ) = get_variable (basename sp) in 
+           fn (VarRef idc) env typ
+	 with Not_found -> (* we are in a section *) ())
+    | "CONSTANT" ->
+	let kn = locate_constant (qualid_of_sp sp) in
+	let {const_type=typ} = Global.lookup_constant kn in
+	fn (ConstRef kn) env typ
+    | "INDUCTIVE" -> 
+	let kn = locate_mind (qualid_of_sp sp) in
+        let mib = Global.lookup_mind kn in 
+        Array.iteri 
+	  (fun i -> print_constructors (kn,i) fn env) mib.mind_packets
+    | _ -> ()
+  in 
+  try 
+    Declaremods.iter_all_segments false crible_rec
+  with Not_found -> 
+    ()
+
+let gen_filtered_search filter_function display_function =
+  gen_crible 
+    (fun s a c -> if filter_function s a c then display_function s a c) 
+
+let search_about ref inout =
+  let c = constr_of_reference ref in
+  let filter_modules = filter_by_module_from_list inout in
+  let filter ref' env typ =
+    filter_modules ref' env typ &&
+    Termops.occur_term c typ
+  in
+  gen_filtered_search filter plain_display
+
+
diff --git a/parsing/search.mli b/parsing/search.mli
index d1f6bccd48..073a20f87c 100644
--- a/parsing/search.mli
+++ b/parsing/search.mli
@@ -21,6 +21,7 @@ open Nametab
 val search_by_head : global_reference -> dir_path list * bool -> unit
 val search_rewrite : constr_pattern -> dir_path list * bool -> unit
 val search_pattern : constr_pattern -> dir_path list * bool -> unit
+val search_about   : global_reference -> dir_path list * bool -> unit
 
 (* The filtering function that is by standard search facilities.
    It can be passed as argument to the raw search functions.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 13acd292c1..5efbcc5d3f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -842,6 +842,8 @@ let vernac_search s r =
       Search.search_rewrite pat r
   | SearchHead locqid ->
       Search.search_by_head (Nametab.global locqid) r
+  | SearchAbout locqid ->
+      Search.search_about (Nametab.global locqid) r
 
 let vernac_locate = function
   | LocateTerm qid -> print_located_qualid qid
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index c0726c0253..4756755b4b 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -62,6 +62,7 @@ type searchable =
   | SearchPattern of pattern_expr
   | SearchRewrite of pattern_expr
   | SearchHead of reference
+  | SearchAbout of reference
 
 type locatable =
   | LocateTerm of reference