Added a SearchAbout-like primitive in coqtop interface.

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

5 files changed, 154 insertions, 0 deletions

diff --git a/lib/interface.mli b/lib/interface.mli
index 02ca25a9de..47692191de 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -70,6 +70,28 @@ type option_state = {
   (** The current value of the option *)
 }
 
+type search_constraint =
+(** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
+| Name_Pattern of string
+(** Whether the object type satisfies a pattern *)
+| Type_Pattern of string
+(** Whether some subtype of object type satisfies a pattern *)
+| SubType_Pattern of string
+(** Whether the object pertains to a module *)
+| In_Module of string list
+(** Bypass the Search blacklist *)
+| Include_Blacklist
+
+(** A list of search constraints; the boolean flag is set to [false] whenever
+    the flag should be negated. *)
+type search_flags = (search_constraint * bool) list
+
+type search_answer = {
+  search_answer_full_path : string list;
+  search_answer_base_name : string;
+  search_answer_type : string;
+}
+
 type coq_info = {
   coqtop_version : string;
   protocol_version : string;
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 8d677ffbf1..105775bda6 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -29,6 +29,7 @@ type 'a call =
   | Evars
   | Hints
   | Status
+  | Search of search_flags
   | GetOptions
   | SetOptions of (option_name * option_value) list
   | InLoadPath of string
@@ -45,6 +46,7 @@ type handler = {
   evars : unit -> evar list option;
   hints : unit -> (hint list * hint) option;
   status : unit -> status;
+  search : search_flags -> search_answer list;
   get_options : unit -> (option_name * option_state) list;
   set_options : (option_name * option_value) list -> unit;
   inloadpath : string -> bool;
@@ -62,6 +64,7 @@ let goals : goals option call = Goal
 let evars : evar list option call = Evars
 let hints : (hint list * hint) option call = Hints
 let status : status call = Status
+let search flags : search_answer list call = Search flags
 let get_options : (option_name * option_state) list call = GetOptions
 let set_options l : unit call = SetOptions l
 let inloadpath s : bool call = InLoadPath s
@@ -79,6 +82,7 @@ let abstract_eval_call handler c =
       | Evars -> Obj.magic (handler.evars () : evar list option)
       | Hints -> Obj.magic (handler.hints () : (hint list * hint) option)
       | Status -> Obj.magic (handler.status () : status)
+      | Search flags -> Obj.magic (handler.search flags : search_answer list)
       | GetOptions -> Obj.magic (handler.get_options () : (option_name * option_state) list)
       | SetOptions opts -> Obj.magic (handler.set_options opts : unit)
       | InLoadPath s -> Obj.magic (handler.inloadpath s : bool)
@@ -208,6 +212,44 @@ let to_option_state = function
   }
 | _ -> raise Marshal_error
 
+let of_search_constraint = function
+| Name_Pattern s ->
+  constructor "search_constraint" "name_pattern" [of_string s]
+| Type_Pattern s ->
+  constructor "search_constraint" "type_pattern" [of_string s]
+| SubType_Pattern s ->
+  constructor "search_constraint" "subtype_pattern" [of_string s]
+| In_Module m ->
+  constructor "search_constraint" "in_module" [of_list of_string m]
+| Include_Blacklist ->
+  constructor "search_constraint" "include_blacklist" []
+
+let to_search_constraint xml = do_match xml "search_constraint"
+  (fun s args -> match s with
+  | "name_pattern" -> Name_Pattern (to_string (singleton args))
+  | "type_pattern" -> Type_Pattern (to_string (singleton args))
+  | "subtype_pattern" -> SubType_Pattern (to_string (singleton args))
+  | "in_module" -> In_Module (to_list to_string (singleton args))
+  | "include_blacklist" -> Include_Blacklist
+  | _ -> raise Marshal_error)
+
+let of_search_answer ans =
+  let path = of_list of_string ans.search_answer_full_path in
+  let name = of_string ans.search_answer_base_name in
+  let tpe = of_string ans.search_answer_type in
+  Element ("search_answer", [], [path; name; tpe])
+
+let to_search_answer = function
+| Element ("search_answer", [], [path; name; tpe]) ->
+  let path = to_list to_string path in
+  let name = to_string name in
+  let tpe = to_string tpe in {
+    search_answer_full_path = path;
+    search_answer_base_name = name;
+    search_answer_type = tpe;
+  }
+| _ -> raise Marshal_error
+
 let of_value f = function
 | Good x -> Element ("value", ["val", "good"], [f x])
 | Fail (loc, msg) ->
@@ -248,6 +290,9 @@ let of_call = function
   Element ("call", ["val", "hints"], [])
 | Status ->
   Element ("call", ["val", "status"], [])
+| Search flags ->
+  let args = List.map (of_pair of_search_constraint of_bool) flags in
+  Element ("call", ["val", "search"], args)
 | GetOptions ->
   Element ("call", ["val", "getoptions"], [])
 | SetOptions opts ->
@@ -276,6 +321,9 @@ let to_call = function
   | "goal" -> Goal
   | "evars" -> Evars
   | "status" -> Status
+  | "search" ->
+    let args = List.map (to_pair to_search_constraint to_bool) l in
+    Search args
   | "getoptions" -> GetOptions
   | "setoptions" ->
     let args = List.map (to_pair (to_list to_string) to_option_value) l in
@@ -375,6 +423,7 @@ let of_answer (q : 'a call) (r : 'a value) =
   | Evars -> Obj.magic (of_option (of_list of_evar) : evar list option -> xml)
   | Hints -> Obj.magic (of_hints : (hint list * hint) option -> xml)
   | Status -> Obj.magic (of_status : status -> xml)
+  | Search _ -> Obj.magic (of_list of_search_answer : search_answer list -> xml)
   | GetOptions -> Obj.magic (of_list (of_pair (of_list of_string) of_option_state) : (option_name * option_state) list -> xml)
   | SetOptions _ -> Obj.magic (fun _ -> Element ("unit", [], []))
   | InLoadPath _ -> Obj.magic (of_bool : bool -> xml)
@@ -401,6 +450,7 @@ let to_answer xml =
     | "option_value" -> Obj.magic (to_option_value elt : option_value)
     | "option_state" -> Obj.magic (to_option_state elt : option_state)
     | "coq_info" -> Obj.magic (to_coq_info elt : coq_info)
+    | "search_answer" -> Obj.magic (to_search_answer elt : search_answer)
     | _ -> raise Marshal_error
     end
   | _ -> raise Marshal_error
@@ -440,6 +490,7 @@ let pr_call = function
   | Evars -> "EVARS"
   | Hints -> "HINTS"
   | Status -> "STATUS"
+  | Search _ -> "SEARCH"
   | GetOptions -> "GETOPTIONS"
   | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]"
   | InLoadPath s -> "INLOADPATH "^s
@@ -500,6 +551,7 @@ let pr_full_value call value =
     | Evars -> pr_value_gen pr_evars (Obj.magic value : evar list option value)
     | Hints -> pr_value value
     | Status -> pr_value_gen pr_status (Obj.magic value : status value)
+    | Search _ -> pr_value value
     | GetOptions -> pr_value_gen pr_getoptions (Obj.magic value : (option_name * option_state) list value)
     | SetOptions _ -> pr_value value
     | InLoadPath s -> pr_value_gen pr_bool (Obj.magic value : bool value)
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 112472d4e3..357b8815b5 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -79,6 +79,7 @@ type handler = {
   evars : unit -> evar list option;
   hints : unit -> (hint list * hint) option;
   status : unit -> status;
+  search : search_flags -> search_answer list;
   get_options : unit -> (option_name * option_state) list;
   set_options : (option_name * option_value) list -> unit;
   inloadpath : string -> bool;
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index ba8463515e..292c288a86 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -248,6 +248,82 @@ let status () =
     Interface.status_proofnum = Pfedit.current_proof_depth ();
   }
 
+(** This should be elsewhere... *)
+let search flags =
+  let env = Global.env () in
+  let rec extract_flags name tpe subtpe mods blacklist = function
+  | [] -> (name, tpe, subtpe, mods, blacklist)
+  | (Interface.Name_Pattern s, b) :: l ->
+    let regexp =
+      try Str.regexp s
+      with _ -> Errors.error ("Invalid regexp: " ^ s)
+    in
+    extract_flags ((regexp, b) :: name) tpe subtpe mods blacklist l
+  | (Interface.Type_Pattern s, b) :: l ->
+    let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
+    let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in
+    extract_flags name ((pat, b) :: tpe) subtpe mods blacklist l
+  | (Interface.SubType_Pattern s, b) :: l ->
+    let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in
+    let (_, pat) = Constrintern.intern_constr_pattern Evd.empty env constr in
+    extract_flags name tpe ((pat, b) :: subtpe) mods blacklist l
+  | (Interface.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
+  | (Interface.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.string_of_id (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 (Matching.is_matching pat constr) flag
+    in
+    let match_subtype (pat, flag) =
+      toggle (Matching.is_matching_appsubterm ~closed:false pat constr) flag
+    in
+    let match_module (mdl, flag) =
+      toggle (Libnames.is_dirpath_prefix_of mdl path) flag
+    in
+    let in_blacklist =
+      blacklist || (Search.filter_blacklist 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 name = Names.string_of_id (Nametab.basename_of_global ref) in
+    let make_path = Names.string_of_id in
+    let path =
+      List.rev_map make_path (Names.repr_dirpath (Nametab.dirpath_of_global ref))
+    in
+    let answer = {
+      Interface.search_answer_full_path = path;
+      Interface.search_answer_base_name = name;
+      Interface.search_answer_type = string_of_ppcmds (pr_lconstr_env env constr);
+    } in
+    ans := answer :: !ans;
+  in
+  let () = Search.gen_filtered_search filter_function print_function in
+  !ans
+
 let get_options () =
   let table = Goptions.get_tables () in
   let fold key state accu = (key, state) :: accu in
@@ -308,6 +384,7 @@ let eval_call c =
     Serialize.evars = interruptible evars;
     Serialize.hints = interruptible hints;
     Serialize.status = interruptible status;
+    Serialize.search = interruptible search;
     Serialize.inloadpath = interruptible inloadpath;
     Serialize.get_options = interruptible get_options;
     Serialize.set_options = interruptible set_options;
diff --git a/toplevel/search.mli b/toplevel/search.mli
index d2d5c53849..95827d54b4 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -33,6 +33,8 @@ val search_about  :
 val filter_by_module_from_list :
   dir_path list * bool -> global_reference -> env -> 'a -> bool
 
+val filter_blacklist : global_reference -> env -> constr -> bool
+
 (** raw search functions can be used for various extensions.
    They are also used for pcoq. *)
 val gen_filtered_search : (global_reference -> env -> constr -> bool) ->