Ajout d'une fonction de recherche sur les composantes du nom des objets

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

6 files changed, 71 insertions, 70 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 14f1061ed8..3337fbc0be 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -104,6 +104,8 @@ GEXTEND Gram
 	  VernacSearch (SearchRewrite c, l)
       | IDENT "SearchAbout"; qid = global; l = in_or_out_modules -> 
 	  VernacSearch (SearchAbout qid, l)
+      | IDENT "SearchNamed"; sl = LIST1 string; l = in_or_out_modules -> 
+	  VernacSearch (SearchNamed sl, l)
 
       (* TODO: rapprocher Eval et Check *)
       | IDENT "Eval"; r = Tactic.red_expr; "in";
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 4d1226b9c5..7475566b70 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -521,6 +521,8 @@ GEXTEND Gram
 	  VernacSearch (SearchRewrite c, l)
       | IDENT "SearchAbout"; qid = global; l = in_or_out_modules -> 
 	  VernacSearch (SearchAbout qid, l)
+      | IDENT "SearchNamed"; sl = LIST1 string; l = in_or_out_modules -> 
+	  VernacSearch (SearchNamed sl, l)
 
       | IDENT "Add"; IDENT "ML"; IDENT "Path"; dir = STRING ->
 	  VernacAddMLPath (false, dir)
diff --git a/parsing/search.ml b/parsing/search.ml
index 5e2fc7f2c3..231656f6df 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -32,13 +32,9 @@ open Nametab
    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 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)))))
+let print_constructors indsp fn env nconstr =
+  for i = 1 to nconstr do
+    fn (ConstructRef (indsp,i)) env (Inductive.type_of_constructor env (indsp,i))
   done
 
 let rec head_const c = match kind_of_term c with
@@ -48,41 +44,46 @@ let rec head_const c = match kind_of_term c with
   | Cast (d,_)   -> head_const d
   | _            -> c
 
-let crible (fn : global_reference -> env -> constr -> unit) ref =
+(* General search, restricted to head constant if [only_head] *)
+
+let gen_crible refopt (fn : global_reference -> env -> constr -> unit) =
   let env = Global.env () in
   let imported = Library.opened_libraries() in
-  let const = constr_of_reference ref in 
-  let crible_rec (sp,_) lobj =
-    match object_tag lobj with
-      | "VARIABLE" ->
-	  (try 
-	     let (idc,_,typ) = get_variable (basename sp) in 
-             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 {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 mib = Global.lookup_mind kn in 
-(*	  let arities =
-	    array_map_to_list 
-	      (fun mip ->
-		 (Name mip.mind_typename, None, mip.mind_nf_arity))
-	      mib.mind_packets in*)
-          (match kind_of_term const with 
-	     | Ind ((kn',tyi) as ind) -> 
-		 if kn=kn' then
-		   print_constructors ind fn env mib.mind_packets.(tyi)
-	     | _ -> ())
-      | _ -> ()
+  let crible_rec (sp,_) lobj = match object_tag lobj with
+    | "VARIABLE" ->
+	(try 
+	   let (idc,_,typ) = get_variable (basename sp) in 
+           if refopt = None
+	     || head_const typ = constr_of_reference (out_some refopt)
+	   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 {const_type=typ} = Global.lookup_constant kn in
+        if refopt = None
+	  || head_const typ = constr_of_reference (out_some refopt)
+	then
+	  fn (ConstRef kn) env typ
+    | "INDUCTIVE" -> 
+	let kn = locate_mind (qualid_of_sp sp) in
+        let mib = Global.lookup_mind kn in 
+        (match refopt with 
+	  | Some (IndRef ((kn',tyi) as ind)) when kn=kn' ->
+	      print_constructors ind fn env
+	        (Array.length (mib.mind_packets.(tyi).mind_user_lc))
+	  | _ ->
+              Array.iteri 
+	        (fun i mip -> print_constructors (kn,i) fn env
+	          (Array.length mip.mind_user_lc)) mib.mind_packets)
+    | _ -> ()
   in 
-    try 
-      Declaremods.iter_all_segments false crible_rec
-    with Not_found -> 
-      errorlabstrm "search"
-      (pr_global ref ++ spc () ++ str "not declared")
+  try 
+    Declaremods.iter_all_segments false crible_rec
+  with Not_found -> 
+    ()
+
+let crible ref = gen_crible (Some ref)
 
 (* Fine Search. By Yves Bertot. *)
 
@@ -140,9 +141,8 @@ let pattern_filter pat _ a c =
       false
 
 let filtered_search filter_function display_function ref =
-  crible 
+  crible ref
     (fun s a c -> if filter_function s a c then display_function s a c) 
-    ref
 
 let rec id_from_pattern = function
   | PRef gr -> gr
@@ -164,13 +164,16 @@ let raw_search_rewrite extra_filter display_function pattern =
        ((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;
+    display_function gref_eq
+(*
+  ;
   filtered_search
     (fun s a c ->
        ((pattern_filter (mk_rewrite_pattern1 gref_eqT pattern) s a c) ||
         (pattern_filter (mk_rewrite_pattern2 gref_eqT pattern) s a c)) 
        && extra_filter s a c)
     display_function gref_eqT
+*)
 
 let text_pattern_search extra_filter =
   raw_pattern_search extra_filter plain_display
@@ -192,35 +195,8 @@ 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 
+  gen_crible None
     (fun s a c -> if filter_function s a c then display_function s a c) 
 
 let raw_search_about filter_modules display_function ref =
@@ -234,5 +210,23 @@ let raw_search_about filter_modules display_function ref =
 let search_about ref inout = 
   raw_search_about (filter_by_module_from_list inout) plain_display ref
 
+let name_of_reference ref = string_of_id (id_of_global ref)
+
+let occur_string_in_name name s =
+  let l = String.length s + 1 in
+  let l' = String.length name in
+  string_string_contains name ("_"^s^"_")
+  || l' >= l && String.sub name 0 l = (s^"_")
+  || l' >= l && String.sub name (l'-l) l = ("_"^s)
+
+let raw_search_named filter_modules display_function strings =
+  let filter ref' env typ =
+    filter_modules ref' env typ &&
+    List.for_all (occur_string_in_name (name_of_reference ref')) strings
+  in
+  gen_filtered_search filter display_function
+
 
+let search_named strings inout =
+  raw_search_named (filter_by_module_from_list inout) plain_display strings
 
diff --git a/parsing/search.mli b/parsing/search.mli
index f7e384e96b..d477659e34 100644
--- a/parsing/search.mli
+++ b/parsing/search.mli
@@ -22,6 +22,7 @@ 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
+val search_named   : string list -> 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/vernacexpr.ml b/toplevel/vernacexpr.ml
index 5f3ff5444b..beb26e41f8 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -60,6 +60,7 @@ type searchable =
   | SearchRewrite of pattern_expr
   | SearchHead of reference
   | SearchAbout of reference
+  | SearchNamed of string list
 
 type locatable =
   | LocateTerm of reference
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 4f94658aae..035b6978ad 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -170,6 +170,7 @@ let pr_search a b pr_p = match a with
   | SearchPattern c -> str"SearchPattern" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b
   | SearchAbout qid -> str"SearchAbout" ++ spc() ++ pr_reference qid ++ pr_in_out_modules b
+  | SearchNamed sl -> str"SearchNamed" ++ spc() ++ prlist_with_sep spc qsnew sl ++ pr_in_out_modules b
 
 let pr_locality local = if local then str "Local " else str ""