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

3 files changed, 75 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;