1 files changed, 91 insertions, 61 deletions

diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 0df24c7a..28f97dc8 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.ml
@@ -45,7 +45,7 @@ type handler = {
   evars : unit -> evar list option;
   hints : unit -> (hint list * hint) option;
   status : unit -> status;
-  search : search_flags -> search_answer list;
+  search : search_flags -> string coq_object list;
   get_options : unit -> (option_name * option_state) list;
   set_options : (option_name * option_value) list -> unit;
   inloadpath : string -> bool;
@@ -63,7 +63,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 search flags : string coq_object 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
@@ -81,7 +81,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)
+      | Search flags -> Obj.magic (handler.search flags : string coq_object 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)
@@ -130,6 +130,12 @@ let bool_arg tag b = if b then [tag, ""] else []
 
 (** Base types *)
 
+let of_unit () = Element ("unit", [], [])
+
+let to_unit = function
+  | Element ("unit", [], []) -> ()
+  | _ -> raise Marshal_error
+
 let of_bool b =
   if b then constructor "bool" "true" []
   else constructor "bool" "false" []
@@ -166,7 +172,8 @@ let to_string = function
 let of_int i = Element ("int", [], [PCData (string_of_int i)])
 
 let to_int = function
-| Element ("int", [], [PCData s]) -> int_of_string s
+| Element ("int", [], [PCData s]) ->
+  (try int_of_string s with Failure _ -> raise Marshal_error)
 | _ -> raise Marshal_error
 
 let of_pair f g (x, y) = Element ("pair", [], [f x; g y])
@@ -232,20 +239,20 @@ let to_search_constraint xml = do_match xml "search_constraint"
   | "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;
+let of_coq_object f ans =
+  let prefix = of_list of_string ans.coq_object_prefix in
+  let qualid = of_list of_string ans.coq_object_qualid in
+  let obj = f ans.coq_object_object in
+  Element ("coq_object", [], [prefix; qualid; obj])
+
+let to_coq_object f = function
+| Element ("coq_object", [], [prefix; qualid; obj]) ->
+  let prefix = to_list to_string prefix in
+  let qualid = to_list to_string qualid in
+  let obj = f obj in {
+    coq_object_prefix = prefix;
+    coq_object_qualid = qualid;
+    coq_object_object = obj;
   }
 | _ -> raise Marshal_error
 
@@ -412,51 +419,74 @@ let to_coq_info = function
   }
 | _ -> raise Marshal_error
 
-let of_hints =
-  let of_hint = of_list (of_pair of_string of_string) in
-  of_option (of_pair (of_list of_hint) of_hint)
-
-let of_answer (q : 'a call) (r : 'a value) =
-  let convert = match q with
-  | Interp _ -> Obj.magic (of_string : string -> xml)
-  | Rewind _ -> Obj.magic (of_int : int -> xml)
-  | Goal -> Obj.magic (of_option of_goals : goals option -> xml)
-  | 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)
-  | MkCases _ -> Obj.magic (of_list (of_list of_string) : string list list -> xml)
-  | Quit -> Obj.magic (fun _ -> Element ("unit", [], []))
-  | About -> Obj.magic (of_coq_info : coq_info -> xml)
+(** Conversions between ['a value] and xml answers
+
+  When decoding an xml answer, we dynamically check that it is compatible
+  with the original call. For that we now rely on the fact that all
+  sub-fonctions [to_xxx : xml -> xxx] check that the current xml element
+  is "xxx", and raise [Marshal_error] if anything goes wrong.
+*)
+
+type value_type =
+  | Unit | String | Int | Bool | Goals | Evar | State | Option_state | Coq_info
+  | Option of value_type
+  | List of value_type
+  | Coq_object of value_type
+  | Pair of value_type * value_type
+
+let hint = List (Pair (String, String))
+let option_name = List String
+
+let expected_answer_type = function
+  | Interp _ -> String
+  | Rewind _ -> Int
+  | Goal -> Option Goals
+  | Evars -> Option (List Evar)
+  | Hints -> Option (Pair (List hint, hint))
+  | Status -> State
+  | Search _ -> List (Coq_object String)
+  | GetOptions -> List (Pair (option_name, Option_state))
+  | SetOptions _ -> Unit
+  | InLoadPath _ -> Bool
+  | MkCases _ -> List (List String)
+  | Quit -> Unit
+  | About -> Coq_info
+
+let of_answer (q : 'a call) (r : 'a value) : xml =
+  let rec convert ty : 'a -> xml = match ty with
+    | Unit -> Obj.magic of_unit
+    | Bool -> Obj.magic of_bool
+    | String -> Obj.magic of_string
+    | Int -> Obj.magic of_int
+    | State -> Obj.magic of_status
+    | Option_state -> Obj.magic of_option_state
+    | Coq_info -> Obj.magic of_coq_info
+    | Goals -> Obj.magic of_goals
+    | Evar -> Obj.magic of_evar
+    | List t -> Obj.magic (of_list (convert t))
+    | Option t -> Obj.magic (of_option (convert t))
+    | Coq_object t -> Obj.magic (of_coq_object (convert t))
+    | Pair (t1,t2) -> Obj.magic (of_pair (convert t1) (convert t2))
   in
-  of_value convert r
-
-let to_answer xml =
-  let rec convert elt = match elt with
-  | Element (tpe, attrs, l) ->
-    begin match tpe with
-    | "unit" -> Obj.magic ()
-    | "string" -> Obj.magic (to_string elt : string)
-    | "int" -> Obj.magic (to_int elt : int)
-    | "status" -> Obj.magic (to_status elt : status)
-    | "bool" -> Obj.magic (to_bool elt : bool)
-    | "list" -> Obj.magic (to_list convert elt : 'a list)
-    | "option" -> Obj.magic (to_option convert elt : 'a option)
-    | "pair" -> Obj.magic (to_pair convert convert elt : ('a * 'b))
-    | "goals" -> Obj.magic (to_goals elt : goals)
-    | "evar" -> Obj.magic (to_evar elt : evar)
-    | "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
+  of_value (convert (expected_answer_type q)) r
+
+let to_answer xml (c : 'a call) : 'a value =
+  let rec convert ty : xml -> 'a = match ty with
+    | Unit -> Obj.magic to_unit
+    | Bool -> Obj.magic to_bool
+    | String -> Obj.magic to_string
+    | Int -> Obj.magic to_int
+    | State -> Obj.magic to_status
+    | Option_state -> Obj.magic to_option_state
+    | Coq_info -> Obj.magic to_coq_info
+    | Goals -> Obj.magic to_goals
+    | Evar -> Obj.magic to_evar
+    | List t -> Obj.magic (to_list (convert t))
+    | Option t -> Obj.magic (to_option (convert t))
+    | Coq_object t -> Obj.magic (to_coq_object (convert t))
+    | Pair (t1,t2) -> Obj.magic (to_pair (convert t1) (convert t2))
   in
-  to_value convert xml
+  to_value (convert (expected_answer_type c)) xml
 
 (** * Debug printing *)