Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewrite

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

6 files changed, 69 insertions, 76 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index ec7c84b47b..cb15d64324 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -11,7 +11,7 @@ open Vernac
 GEXTEND Gram
   GLOBAL: identarg ne_identarg_list numarg ne_numarg_list numarg_list
           stringarg ne_stringarg_list constrarg sortarg tacarg 
-          qualidarg qualidconstarg;
+          ne_qualidarg_list qualidarg qualidconstarg;
 
   identarg:
     [ [ id = Constr.ident -> id ] ]
@@ -22,6 +22,10 @@ GEXTEND Gram
   qualidarg:
     [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >> ] ]
   ;
+  ne_qualidarg_list:
+    [ [ q = qualidarg; l = ne_qualidarg_list -> q::l
+      | q = qualidarg -> [q] ] ]
+  ;
   qualidconstarg:
     [ [ l = Constr.qualid -> <:ast< (QUALIDCONSTARG ($LIST l)) >> ] ]
   ;
@@ -119,7 +123,8 @@ GEXTEND Gram
           <:ast< (PrintOpaqueId $id) >>
 (* Pris en compte dans PrintOption ci-dessous (CADUC) *)
       | IDENT "Print"; id = qualidarg; "." -> <:ast< (PrintId $id) >>
-      | IDENT "Search"; id = qualidarg; "." -> <:ast< (SEARCH $id) >>
+      | IDENT "Search"; id = qualidarg; l = in_or_out_modules; "." ->
+	  <:ast< (SEARCH $id ($LIST $l)) >>
       | IDENT "Inspect"; n = numarg; "." -> <:ast< (INSPECT $n) >>
       | IDENT "SearchPattern"; c = constrarg; l = in_or_out_modules; "." ->
 	  <:ast< (SearchPattern $c ($LIST $l)) >>
@@ -223,8 +228,8 @@ GEXTEND Gram
       | "Type" -> <:ast< "PRINTTYPE" >> ] ] (* pas dans le RefMan *)
   ;
   in_or_out_modules:
-    [ [ IDENT "inside"; l = ne_identarg_list -> <:ast< "inside" >> :: l
-      | IDENT "outside"; l = ne_identarg_list -> <:ast< "outside" >> :: l
+    [ [ IDENT "inside"; l = ne_qualidarg_list -> <:ast< "inside" >> :: l
+      | IDENT "outside"; l = ne_qualidarg_list -> <:ast< "outside" >> :: l
       | -> [] ] ]
   ;
 END;
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 4fba8e8911..fbbec9b34f 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -349,6 +349,7 @@ module Vernac =
     let ne_identarg_list = gec_list "ne_identarg_list"
     let qualidarg = gec "qualidarg"
     let qualidconstarg = gec "qualidconstarg"
+    let ne_qualidarg_list = gec_list "ne_qualidarg_list"
     let numarg = gec "numarg"
     let numarg_list = gec_list "numarg_list"
     let ne_numarg_list = gec_list "ne_numarg_list"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 26ff046048..960a59be7f 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -161,6 +161,7 @@ module Vernac :
     val ne_identarg_list : Coqast.t list Gram.Entry.e
     val qualidarg : Coqast.t Gram.Entry.e
     val qualidconstarg : Coqast.t Gram.Entry.e
+    val ne_qualidarg_list : Coqast.t list Gram.Entry.e
     val numarg : Coqast.t Gram.Entry.e
     val numarg_list : Coqast.t list Gram.Entry.e
     val ne_numarg_list : Coqast.t list Gram.Entry.e
diff --git a/parsing/search.ml b/parsing/search.ml
index 8369ba98c2..8edf175757 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -16,18 +16,17 @@ open Pattern
 open Printer
 
 (* The functions print_constructors and crible implement the behavior needed
-   for the Coq Search command.
+   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 fn env_ar mip = 
-  let _ =
-    array_map2 (fun id c -> fn (pr_id id) (* il faudrait qualifier... *)
-		    env_ar (body_of_type c))
-    mip.mind_consnames (mind_user_lc mip)
-  in ()
+let print_constructors indsp fn env_ar mip =
+  let lc = mind_user_lc mip in
+  for i=1 to Array.length lc do
+      fn (ConstructRef (indsp,i)) env_ar (lc.(i-1))
+  done
 
 let rec head_const c = match kind_of_term c with
   | IsProd (_,_,d) -> head_const d
@@ -36,21 +35,21 @@ let rec head_const c = match kind_of_term c with
   | IsCast (d,_)   -> head_const d
   | _            -> c
 
-let crible (fn : std_ppcmds -> env -> constr -> unit) ref =
+let crible (fn : global_reference -> env -> constr -> unit) ref =
   let env = Global.env () in
   let imported = Library.opened_modules() in
   let const = constr_of_reference Evd.empty env ref in 
   let crible_rec sp lobj =
     match object_tag lobj with
       | "VARIABLE" ->
-	  let ((idc,_,typ),_,_) = get_variable sp in 
-          if (head_const (body_of_type typ)) = const then  
-            fn (pr_id idc) env (body_of_type typ)
+	  (try 
+	     let ((idc,_,typ),_,_) = get_variable sp in 
+             if (head_const typ) = const then fn (VarRef sp) env typ
+	   with Not_found -> (* we are in a section *) ())
       | "CONSTANT" 
       | "PARAMETER" ->
 	  let {const_type=typ} = Global.lookup_constant sp in
-	  if (head_const (body_of_type typ)) = const then
-            fn (pr_global (ConstRef sp)) env (body_of_type typ)
+	  if (head_const typ) = const then fn (ConstRef sp) env typ
       | "INDUCTIVE" -> 
           let mib = Global.lookup_mind sp in 
 	  let arities =
@@ -60,24 +59,19 @@ let crible (fn : std_ppcmds -> env -> constr -> unit) ref =
 	      mib.mind_packets in
 	  let env_ar = push_rels arities env in
           (match kind_of_term const with 
-	     | IsMutInd ((sp',tyi),_) -> 
-		 if sp=sp' then (*Suffit pas, cf les inds de Ensemble.v*)
-		   print_constructors fn env_ar
+	     | IsMutInd ((sp',tyi) as indsp,_) -> 
+		 if sp=sp' then
+		   print_constructors indsp fn env_ar
 		     (mind_nth_type_packet mib tyi)
 	     | _ -> ())
       | _ -> ()
   in 
   try 
-    Library.iter_all_segments false crible_rec 
+    Library.iter_all_segments true crible_rec 
   with Not_found -> 
     errorlabstrm "search"
       [< pr_global ref; 'sPC; 'sTR "not declared" >]
 
-let search_by_head ref =
-  crible (fun pname ass_name constr -> 
-            let pc = prterm_env ass_name constr in
-            mSG [< hOV 2 [< pname; 'sTR":"; 'sPC; pc >]; 'fNL >]) ref
-
 (* Fine Search. By Yves Bertot. *)
 
 exception No_section_path
@@ -94,16 +88,17 @@ let constr_to_section_path c = match kind_of_term c with
       
 let xor a b = (a or b) & (not (a & b))
 
-let plain_display s a c =
-  let pc = Printer.prterm_env a c in
-  mSG [< hOV 2 [< s; 'sTR":"; 'sPC; pc >]; 'fNL>]
+let plain_display ref a c =
+  let pc = prterm_env a c in
+  let pr = pr_global ref in
+  mSG [< hOV 2 [< pr; 'sTR":"; 'sPC; pc >]; 'fNL>]
 
-let filter_by_module module_list accept _ _ c =
+let filter_by_module module_list accept ref env _ =
   try
-    let sp = constr_to_section_path c in
+    let sp = sp_of_global env ref in
     let sl = dirpath sp in
     let rec filter_aux = function
-      | m :: tl -> (not (List.mem m sl)) && (filter_aux tl)
+      | m :: tl -> (not (dirpath_prefix_of m sl)) && (filter_aux tl)
       | [] -> true 
     in
     xor accept (filter_aux module_list)
@@ -168,9 +163,9 @@ let text_search_rewrite extra_filter =
 
 let filter_by_module_from_list = function
   | [], _ -> (fun _ _ _ -> true)
-  | l, s -> filter_by_module l (s = "inside")
+  | l, outside -> filter_by_module l (not outside)
 
-let search_modules ref inout = 
+let search_by_head ref inout = 
   filtered_search (filter_by_module_from_list inout) plain_display ref
 
 let search_rewrite pat inout =
diff --git a/parsing/search.mli b/parsing/search.mli
index c0c003ad8a..8e813c5108 100644
--- a/parsing/search.mli
+++ b/parsing/search.mli
@@ -2,16 +2,13 @@
 (*i $Id$ i*)
 
 open Pp
+open Names
 open Term
 open Environ
 open Pattern
 
 (*s Search facilities. *)
 
-val crible : (std_ppcmds -> env -> constr -> unit) -> global_reference -> unit
-
-val search_by_head : global_reference -> unit
-
-val search_modules : global_reference -> string list * string -> unit
-val search_rewrite : Pattern.constr_pattern  -> string list * string -> unit
-val search_pattern : Pattern.constr_pattern  -> string list * string -> unit
+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
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 012dc2ca3a..9b11040d23 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -914,45 +914,19 @@ let _ =
        | _  -> bad_vernac_args "PrintExtract")
     ***)
 
-let _ =
-  add "SEARCH"
-    (function 
-       | [VARG_QUALID qid] ->
-	   (fun () ->
-	      let ref =
-		try 
-		  Nametab.locate qid
-		with Not_found ->
-		  Pretype_errors.error_global_not_found_loc loc qid
-	      in 
-	      Search.search_by_head ref)
-       | _ -> bad_vernac_args "SEARCH")
-
-let _ =
-  add "INSPECT"
-    (function 
-       | [VARG_NUMBER n] -> (fun () -> mSG(inspect n))
-       | _ -> bad_vernac_args "INSPECT")
-
-let string_of_id_list =
-  List.map (function 
-	      | VARG_IDENTIFIER s -> string_of_id s
-	      | _ -> bad_vernac_args "string_of_id_list")
+let extract_qualid = function 
+  | VARG_QUALID qid ->
+      (try wd_of_sp (fst (Nametab.locate_module qid))
+       with Not_found -> 
+	 error ("Module/section "^(string_of_qualid qid)^" not found"))
+  | _ -> bad_vernac_args "extract_qualid"
 
 let inside_outside = function
-  | (VARG_STRING s) :: l -> string_of_id_list l, s
-  | [] -> [], ""
+  | (VARG_STRING "outside") :: l -> List.map extract_qualid l, true
+  | (VARG_STRING "inside") :: l -> List.map extract_qualid l, false
+  | [] -> [], true
   | _ -> bad_vernac_args "inside/outside"
 
-let _ =
-  add "SearchModules"
-    (function
-       | (VARG_IDENTIFIER id) :: l ->
-           (fun () -> 
-	      let ref = Nametab.sp_of_id CCI id in
-              Search.search_modules ref (inside_outside l))
-       | _ -> bad_vernac_args "SearchModules")
-
 let _ = 
   add "SearchRewrite"
     (function
@@ -972,6 +946,26 @@ let _ =
        | _ -> bad_vernac_args "SearchPattern")
 
 let _ =
+  add "SEARCH"
+    (function 
+       | (VARG_QUALID qid) :: l ->
+	   (fun () ->
+	      let ref =
+		try 
+		  Nametab.locate qid
+		with Not_found ->
+		  Pretype_errors.error_global_not_found_loc loc qid
+	      in 
+	      Search.search_by_head ref (inside_outside l))
+       | _ -> bad_vernac_args "SEARCH")
+
+let _ =
+  add "INSPECT"
+    (function 
+       | [VARG_NUMBER n] -> (fun () -> mSG(inspect n))
+       | _ -> bad_vernac_args "INSPECT")
+
+let _ =
   add "SETUNDO"
     (function 
        | [VARG_NUMBER n] -> (fun () -> set_undo n)