interface.mli and serialize.ml reworked to avoid copy/paste of types

With this commit the types involved in the protocol between Coq and
Coqide are written once and for all in interface.mli

serialize.ml is monkey code that contains a reified version of these
types and the related machinery needed to marshal values in these types
to/from xml in a modular way.  This file should be automatically
generated from the spec of the protocol in an ideal world.
Phantom types are used to statically check that the reified form
of the types is in sync with the one declared in interface.mli

The benefit of this commit is that changing the protocol is easier:
one changes the types in interface.mli and lets ocamlc spot all the
places that needs to be modified.
This is a necessity if one plays with the protocol very often, like
in my Paral-ITP branch.

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

5 files changed, 398 insertions, 339 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index fd6de80d1..121981110 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -540,13 +540,18 @@ let eval_call ?(logger=default_logger) call handle k =
   Minilib.log "End eval_call";
   Void
 
-let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) s =
-  eval_call ~logger (Serialize.interp (raw,verbose,s))
+let interp ?(logger=default_logger) ?(raw=false) ?(verbose=true) s h k =
+  eval_call ~logger (Serialize.interp (raw,verbose,s)) h
+    (function
+     | Interface.Good (Util.Inl v) -> k (Interface.Good v)
+     | Interface.Good (Util.Inr v) -> k (Interface.Unsafe v)
+     | Interface.Fail v -> k (Interface.Fail v)
+     | Interface.Unsafe _ -> assert false)
 let rewind i = eval_call (Serialize.rewind i)
 let inloadpath s = eval_call (Serialize.inloadpath s)
 let mkcases s = eval_call (Serialize.mkcases s)
-let status = eval_call Serialize.status
-let hints = eval_call Serialize.hints
+let status = eval_call (Serialize.status ())
+let hints = eval_call (Serialize.hints ())
 let search flags = eval_call (Serialize.search flags)
 
 module PrintOpt =
@@ -612,7 +617,7 @@ struct
 end
 
 let goals h k =
-  PrintOpt.enforce h (fun () -> eval_call Serialize.goals h k)
+  PrintOpt.enforce h (fun () -> eval_call (Serialize.goals ()) h k)
 
 let evars h k =
-  PrintOpt.enforce h (fun () -> eval_call Serialize.evars h k)
+  PrintOpt.enforce h (fun () -> eval_call (Serialize.evars ()) h k)
diff --git a/lib/interface.mli b/lib/interface.mli
index f8a382aef..f655921d7 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -86,8 +86,8 @@ type search_constraint =
     the flag should be negated. *)
 type search_flags = (search_constraint * bool) list
 
-(** A named object in Coq. [coq_object_qualid] is the shortest path defined for 
-    the user. [coq_object_prefix] is the missing part to recover the fully 
+(** A named object in Coq. [coq_object_qualid] is the shortest path defined for
+    the user. [coq_object_prefix] is the missing part to recover the fully
     qualified name, i.e [fully_qualified = coq_object_prefix + coq_object_qualid].
     [coq_object_object] is the actual content of the object. *)
 type 'a coq_object = {
@@ -123,3 +123,98 @@ type 'a value =
   | Good of 'a
   | Unsafe of 'a
   | Fail of (location * string)
+
+(* Request/Reply message protocol between Coq and CoqIde *)
+
+(** Running a command (given as a string).
+    The 1st flag indicates whether to use "raw" mode
+    (less sanity checks, no impact on the undo stack).
+    Suitable e.g. for queries, or for the Set/Unset
+    of display options that coqide performs all the time.
+    The 2nd flag controls the verbosity.
+    The returned string contains the messages produced
+    by this command, but not the updated goals (they are
+    to be fetch by a separated [current_goals]). *)
+type interp_sty = raw * verbose * string
+(* spiwack: [Inl] for safe and [Inr] for unsafe. *)
+type interp_rty = (string,string) Util.union
+
+(** Backtracking by at least a certain number of phrases.
+    No finished proofs will be re-opened. Instead,
+    we continue backtracking until before these proofs,
+    and answer the amount of extra backtracking performed.
+    Backtracking by more than the number of phrases already
+    interpreted successfully (and not yet undone) will fail. *)
+type rewind_sty = int
+type rewind_rty = int
+
+(** Fetching the list of current goals. Return [None] if no proof is in
+    progress, [Some gl] otherwise. *)
+type goals_sty = unit
+type goals_rty = goals option
+
+(** Retrieve the list of unintantiated evars in the current proof. [None] if no
+    proof is in progress. *)
+type evars_sty = unit
+type evars_rty = evar list option
+
+(** Retrieving the tactics applicable to the current goal. [None] if there is
+    no proof in progress. *)
+type hints_sty = unit
+type hints_rty = (hint list * hint) option
+
+(** The status, for instance "Ready in SomeSection, proving Foo" *)
+type status_sty = unit
+type status_rty = status
+
+(** Search for objects satisfying the given search flags. *)
+type search_sty = search_flags
+type search_rty = string coq_object list
+
+(** Retrieve the list of options of the current toplevel *)
+type get_options_sty = unit
+type get_options_rty = (option_name * option_state) list
+
+(** Set the options to the given value. Warning: this is not atomic, so whenever
+    the call fails, the option state can be messed up... This is the caller duty
+    to check that everything is correct. *)
+type set_options_sty = (option_name * option_value) list
+type set_options_rty = unit
+
+(** Is a directory part of Coq's loadpath ? *)
+type inloadpath_sty = string
+type inloadpath_rty = bool
+
+(** Create a "match" template for a given inductive type.
+    For each branch of the match, we list the constructor name
+    followed by enough pattern variables. *)
+type mkcases_sty = string
+type mkcases_rty = string list list
+
+(** Quit gracefully the interpreter. *)
+type quit_sty = unit
+type quit_rty = unit
+
+type about_sty = unit
+type about_rty = coq_info
+
+type handle_exn_rty = location * string
+type handle_exn_sty = exn
+
+type handler = {
+  interp      : interp_sty      -> interp_rty;
+  rewind      : rewind_sty      -> rewind_rty;
+  goals       : goals_sty       -> goals_rty;
+  evars       : evars_sty       -> evars_rty;
+  hints       : hints_sty       -> hints_rty;
+  status      : status_sty      -> status_rty;
+  search      : search_sty      -> search_rty;
+  get_options : get_options_sty -> get_options_rty;
+  set_options : set_options_sty -> set_options_rty;
+  inloadpath  : inloadpath_sty  -> inloadpath_rty;
+  mkcases     : mkcases_sty     -> mkcases_rty;
+  quit        : quit_sty        -> quit_rty;
+  about       : about_sty       -> about_rty;
+  handle_exn  : handle_exn_sty  -> handle_exn_rty;
+}
+
diff --git a/lib/serialize.ml b/lib/serialize.ml
index 7c82d6b80..9899bae24 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -23,86 +23,143 @@ type xml =
 (** We use phantom types and GADT to protect ourselves against wild casts *)
 
 type 'a call =
-  | Interp of raw * verbose * string
-  | Rewind of int
-  | Goal
-  | Evars
-  | Hints
-  | Status
-  | Search of search_flags
-  | GetOptions
-  | SetOptions of (option_name * option_value) list
-  | InLoadPath of string
-  | MkCases of string
-  | Quit
-  | About
+  | Interp     of interp_sty
+  | Rewind     of rewind_sty
+  | Goal       of goals_sty
+  | Evars      of evars_sty
+  | Hints      of hints_sty
+  | Status     of status_sty
+  | Search     of search_sty
+  | GetOptions of get_options_sty
+  | SetOptions of set_options_sty
+  | InLoadPath of inloadpath_sty
+  | MkCases    of mkcases_sty
+  | Quit       of quit_sty
+  | About      of about_sty
 
 type unknown
 
-(** The structure that coqtop should implement *)
-
-type handler = {
-  (* spiwack: [Inl] for safe and [Inr] for unsafe. *)
-  interp : raw * verbose * string -> (string,string) Util.union;
-  rewind : int -> int;
-  goals : unit -> goals option;
-  evars : unit -> evar list option;
-  hints : unit -> (hint list * hint) option;
-  status : unit -> status;
-  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;
-  mkcases : string -> string list list;
-  quit : unit -> unit;
-  about : unit -> coq_info;
-  handle_exn : exn -> location * string;
-}
-
 (** The actual calls *)
 
-let interp (r,b,s) : string call = Interp (r,b,s)
-let rewind i : int call = Rewind i
-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 get_options : (option_name * option_state) list call = GetOptions
-let set_options l : unit call = SetOptions l
-let inloadpath s : bool call = InLoadPath s
-let mkcases s : string list list call = MkCases s
-let search flags : string coq_object list call = Search flags
-let quit : unit call = Quit
+let interp x      : interp_rty call      = Interp x
+let rewind x      : rewind_rty call      = Rewind x
+let goals x       : goals_rty call       = Goal x
+let evars x       : evars_rty call       = Evars x
+let hints x       : hints_rty call       = Hints x
+let status x      : status_rty call      = Status x
+let get_options x : get_options_rty call = GetOptions x
+let set_options x : set_options_rty call = SetOptions x
+let inloadpath x  : inloadpath_rty call  = InLoadPath x
+let mkcases x     : mkcases_rty call     = MkCases x
+let search x      : search_rty call      = Search x
+let quit x        : quit_rty call        = Quit x
 
 (** * Coq answers to CoqIde *)
 
-let abstract_eval_call handler c =
+let abstract_eval_call handler (c : 'a call) =
+  let mkGood x : 'a value = Good (Obj.magic x) in
   try
     match c with
-      | Interp (r,b,s) ->
-          begin match handler.interp (r,b,s) with
-            | Util.Inl v -> Good (Obj.magic (v:string))
-            | Util.Inr v -> Unsafe (Obj.magic (v:string))
-          end
-      | c ->
-          let res = match c with
-            | Interp (r,b,s) -> assert false
-            | Rewind i -> Obj.magic (handler.rewind i : int)
-            | Goal -> Obj.magic (handler.goals () : goals option)
-            | 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 : 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)
-            | MkCases s -> Obj.magic (handler.mkcases s : string list list)
-            | Quit -> Obj.magic (handler.quit () : unit)
-            | About -> Obj.magic (handler.about () : coq_info)
-          in Good res
+      | Interp x     -> mkGood (handler.interp x)
+      | Rewind x     -> mkGood (handler.rewind x)
+      | Goal x       -> mkGood (handler.goals x)
+      | Evars x      -> mkGood (handler.evars x)
+      | Hints x      -> mkGood (handler.hints x)
+      | Status x     -> mkGood (handler.status x)
+      | Search x     -> mkGood (handler.search x)
+      | GetOptions x -> mkGood (handler.get_options x)
+      | SetOptions x -> mkGood (handler.set_options x)
+      | InLoadPath x -> mkGood (handler.inloadpath x)
+      | MkCases x    -> mkGood (handler.mkcases x)
+      | Quit x       -> mkGood (handler.quit x)
+      | About x      -> mkGood (handler.about x)
   with any ->
-    let (l, str) = handler.handle_exn any in
-    Fail (l,str)
+    Fail (handler.handle_exn any)
+
+(* To read and typecheck the answers we give a description of the types,
+   and a way to statically check that the reified version is in sync *)
+module ReifType : sig
+
+  type 'a val_t
+
+  val unit_t         : unit val_t
+  val string_t       : string val_t
+  val int_t          : int val_t
+  val bool_t         : bool val_t
+  val goals_t        : goals val_t
+  val evar_t         : evar val_t
+  val state_t        : status val_t
+  val coq_info_t     : coq_info val_t
+  val option_state_t : option_state val_t
+  val option_t       : 'a val_t -> 'a option val_t
+  val list_t         : 'a val_t -> 'a list val_t
+  val coq_object_t   : 'a val_t -> 'a coq_object val_t
+  val pair_t         : 'a val_t -> 'b val_t -> ('a * 'b) val_t
+  val union_t        : 'a val_t -> 'b val_t -> ('a ,'b) Util.union val_t
+
+  type value_type = private
+    | 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
+    | Union of value_type * value_type
+
+  val check : 'a val_t -> value_type
+
+end = struct
+
+  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
+    | Union of value_type * value_type
+
+  type 'a val_t = value_type
+  let check x = x
+
+  let unit_t         = Unit
+  let string_t       = String
+  let int_t          = Int
+  let bool_t         = Bool
+  let goals_t        = Goals
+  let evar_t         = Evar
+  let state_t        = State
+  let coq_info_t     = Coq_info
+  let option_state_t = Option_state
+  let option_t x     = Option x
+  let list_t x       = List x
+  let coq_object_t x = Coq_object x
+  let pair_t x y     = Pair (x, y)
+  let union_t x y    = Union (x, y)
+
+end
+
+open ReifType
+
+(* For every (call : 'a call), we build the reification of 'a.
+ * In OCaml 4 we could use GATDs to do that I guess *)
+let expected_answer_type call : value_type =
+  let hint = list_t (pair_t string_t string_t) in
+  let hints = pair_t (list_t hint) hint in
+  let options = pair_t (list_t string_t) option_state_t in
+  let objs = coq_object_t string_t in
+  match call with
+  | Interp _     -> check (union_t string_t string_t     : interp_rty      val_t)
+  | Rewind _     -> check (int_t                         : rewind_rty      val_t)
+  | Goal _       -> check (option_t goals_t              : goals_rty       val_t)
+  | Evars _      -> check (option_t (list_t evar_t)      : evars_rty       val_t)
+  | Hints  _     -> check (option_t hints                : hints_rty       val_t)
+  | Status _     -> check (state_t                       : status_rty      val_t)
+  | Search _     -> check (list_t objs                   : search_rty      val_t)
+  | GetOptions _ -> check (list_t options                : get_options_rty val_t)
+  | SetOptions _ -> check (unit_t                        : set_options_rty val_t)
+  | InLoadPath _ -> check (bool_t                        : inloadpath_rty  val_t)
+  | MkCases _    -> check (list_t (list_t string_t)      : mkcases_rty     val_t)
+  | Quit _       -> check (unit_t                        : quit_rty        val_t)
+  | About _      -> check (coq_info_t                    : about_rty       val_t)
 
 (** * XML data marshalling *)
 
@@ -137,56 +194,68 @@ let bool_arg tag b = if b then [tag, ""] else []
 
 let of_unit () = Element ("unit", [], [])
 
-let to_unit = function
+let to_unit : xml -> unit = function
   | Element ("unit", [], []) -> ()
   | _ -> raise Marshal_error
 
-let of_bool b =
+let of_bool (b : bool) : xml =
   if b then constructor "bool" "true" []
   else constructor "bool" "false" []
 
-let to_bool xml = do_match xml "bool"
+let to_bool xml : bool = do_match xml "bool"
   (fun s _ -> match s with
   | "true" -> true
   | "false" -> false
   | _ -> raise Marshal_error)
 
-let of_list f l =
+let of_list (f : 'a -> xml) (l : 'a list) =
   Element ("list", [], List.map f l)
 
-let to_list f = function
+let to_list (f : xml -> 'a) : xml -> 'a list = function
 | Element ("list", [], l) ->
   List.map f l
 | _ -> raise Marshal_error
 
-let of_option f = function
+let of_option (f : 'a -> xml) : 'a option -> xml = function
 | None -> Element ("option", ["val", "none"], [])
 | Some x -> Element ("option", ["val", "some"], [f x])
 
-let to_option f = function
+let to_option (f : xml -> 'a) : xml -> 'a option = function
 | Element ("option", ["val", "none"], []) -> None
 | Element ("option", ["val", "some"], [x]) -> Some (f x)
 | _ -> raise Marshal_error
 
-let of_string s = Element ("string", [], [PCData s])
+let of_string (s : string) : xml = Element ("string", [], [PCData s])
 
-let to_string = function
+let to_string : xml -> string = function
 | Element ("string", [], l) -> raw_string l
 | _ -> raise Marshal_error
 
-let of_int i = Element ("int", [], [PCData (string_of_int i)])
+let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)])
 
-let to_int = function
+let to_int : xml -> int = function
 | 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])
+let of_pair (f : 'a -> xml) (g : 'b -> xml) : 'a * 'b -> xml =
+  function (x,y) -> Element ("pair", [], [f x; g y])
 
-let to_pair f g = function
+let to_pair (f : xml -> 'a) (g : xml -> 'b) : xml -> 'a * 'b = function
 | Element ("pair", [], [x; y]) -> (f x, g y)
 | _ -> raise Marshal_error
 
+let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) Util.union -> xml =
+function
+| Util.Inl x -> Element ("union", ["val","in_l"], [f x])
+| Util.Inr x -> Element ("union", ["val","in_r"], [g x])
+
+let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) Util.union=
+function
+| Element ("union", ["val","in_l"], [x]) -> Util.Inl (f x)
+| Element ("union", ["val","in_r"], [x]) -> Util.Inr (g x)
+| _ -> raise Marshal_error
+
 (** More elaborate types *)
 
 let of_option_value = function
@@ -295,18 +364,18 @@ let of_call = function
   Element ("call", ("val", "interp") :: flags, [PCData cmd])
 | Rewind n ->
   Element ("call", ("val", "rewind") :: ["steps", string_of_int n], [])
-| Goal ->
+| Goal () ->
   Element ("call", ["val", "goal"], [])
-| Evars ->
+| Evars () ->
   Element ("call", ["val", "evars"], [])
-| Hints ->
+| Hints () ->
   Element ("call", ["val", "hints"], [])
-| Status ->
+| 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 ->
+| GetOptions () ->
   Element ("call", ["val", "getoptions"], [])
 | SetOptions opts ->
   let args = List.map (of_pair (of_list of_string) of_option_value) opts in
@@ -315,9 +384,9 @@ let of_call = function
   Element ("call", ["val", "inloadpath"], [PCData file])
 | MkCases ind ->
   Element ("call", ["val", "mkcases"], [PCData ind])
-| Quit ->
+| Quit () ->
   Element ("call", ["val", "quit"], [])
-| About ->
+| About () ->
   Element ("call", ["val", "about"], [])
 
 let to_call = function
@@ -331,21 +400,21 @@ let to_call = function
   | "rewind" ->
     let steps = int_of_string (massoc "steps" attrs) in
     Rewind steps
-  | "goal" -> Goal
-  | "evars" -> Evars
-  | "status" -> Status
+  | "goal" -> Goal ()
+  | "evars" -> Evars ()
+  | "status" -> Status ()
   | "search" ->
     let args = List.map (to_pair to_search_constraint to_bool) l in
     Search args
-  | "getoptions" -> GetOptions
+  | "getoptions" -> GetOptions ()
   | "setoptions" ->
     let args = List.map (to_pair (to_list to_string) to_option_value) l in
     SetOptions args
   | "inloadpath" -> InLoadPath (raw_string l)
   | "mkcases" -> MkCases (raw_string l)
-  | "hints" -> Hints
-  | "quit" -> Quit
-  | "about" -> About
+  | "hints" -> Hints ()
+  | "quit" -> Quit ()
+  | "about" -> About ()
   | _ -> raise Marshal_error
   end
 | _ -> raise Marshal_error
@@ -461,92 +530,91 @@ let is_message = function
   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
+  is "xxx", and raise [Marshal_error] if anything goes wrong.  *)
 
 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))
+    | 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))
+    | Union (t1,t2) -> Obj.magic (of_union (convert t1) (convert t2))
   in
   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))
+    | 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))
+    | Union (t1,t2) -> Obj.magic (to_union (convert t1) (convert t2))
   in
   to_value (convert (expected_answer_type c)) xml
 
 (** * Debug printing *)
 
+let pr_unit () = ""
+let pr_string s = Printf.sprintf "%S" s
+let pr_int i = string_of_int i
+let pr_bool b = Printf.sprintf "%B" b
+let pr_goal (g : goals) =
+  if g.fg_goals = [] then
+    if g.bg_goals = [] then "Proof completed."
+    else
+      let rec pr_focus _ = function
+        | [] -> assert false
+        | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg)
+        | (lg, rg) :: l ->
+          Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l in
+      Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
+  else
+    let pr_menu s = s in
+    let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
+      "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^
+          pr_menu goal ^ "]" in
+    String.concat " " (List.map pr_goal g.fg_goals)
+let pr_evar (e : evar) = "[" ^ e.evar_info ^ "]"
+let pr_status (s : status) =
+  let path =
+    let l = String.concat "." s.status_path in
+    "path=" ^ l ^ ";" in
+  let name = match s.status_proofname with
+    | None -> "no proof;"
+    | Some n -> "proof = " ^ n ^ ";" in
+  "Status: " ^ path ^ name
+let pr_coq_info (i : coq_info) = "FIXME"
 let pr_option_value = function
-| IntValue None -> "none"
-| IntValue (Some i) -> string_of_int i
-| StringValue s -> s
-| BoolValue b -> if b then "true" else "false"
-
-let pr_setoptions opts =
-  let map (key, v) =
-    let key = String.concat " " key in
-    key ^ " := " ^ (pr_option_value v)
-  in
-  String.concat "; " (List.map map opts)
-
-let pr_getoptions opts =
-  let map (key, s) =
-    let key = String.concat " " key in
-    Printf.sprintf "%s: sync := %b; depr := %b; name := %s; value := %s\n"
-      key s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
-  in
-  "\n" ^ String.concat "" (List.map map opts)
+  | IntValue None -> "none"
+  | IntValue (Some i) -> string_of_int i
+  | StringValue s -> s
+  | BoolValue b -> if b then "true" else "false"
+let pr_option_state (s : option_state) =
+  Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n"
+    s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
+let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]"
+let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")"
+let pr_coq_object (o : 'a coq_object) = "FIXME"
+let pr_pair pr1 pr2 (a,b) = "("^pr1 a^","^pr2 b^")"
+let pr_union pr1 pr2 = function Util.Inl x -> pr1 x | Util.Inr x -> pr2 x
 
 let pr_call = function
   | Interp (r,b,s) ->
@@ -554,84 +622,39 @@ let pr_call = function
     let verb = if b then "" else "SILENT" in
     "INTERP"^raw^verb^" ["^s^"]"
   | Rewind i -> "REWIND "^(string_of_int i)
-  | Goal -> "GOALS"
-  | Evars -> "EVARS"
-  | Hints -> "HINTS"
-  | Status -> "STATUS"
+  | Goal _ -> "GOALS"
+  | Evars _ -> "EVARS"
+  | Hints _ -> "HINTS"
+  | Status _ -> "STATUS"
   | Search _ -> "SEARCH"
-  | GetOptions -> "GETOPTIONS"
-  | SetOptions l -> "SETOPTIONS" ^ " [" ^ pr_setoptions l ^ "]"
+  | GetOptions _ -> "GETOPTIONS"
+  | SetOptions l -> "SETOPTIONS" ^ " [" ^
+      String.concat ";"
+        (List.map (pr_pair (pr_list pr_string) pr_option_value) l) ^ "]"
   | InLoadPath s -> "INLOADPATH "^s
   | MkCases s -> "MKCASES "^s
-  | Quit -> "QUIT"
-  | About -> "ABOUT"
-
+  | Quit _ -> "QUIT"
+  | About _ -> "ABOUT"
 let pr_value_gen pr = function
   | Good v -> "GOOD " ^ pr v
   | Unsafe v -> "UNSAFE" ^ pr v
   | Fail (_,str) -> "FAIL ["^str^"]"
-
-let pr_value v = pr_value_gen (fun _ -> "") v
-
-let pr_string s = "["^s^"]"
-let pr_bool b = if b then "true" else "false"
-
-let pr_status s =
-  let path =
-    let l = String.concat "." s.status_path in
-    "path=" ^ l ^ ";"
-  in
-  let name = match s.status_proofname with
-  | None -> "no proof;"
-  | Some n -> "proof = " ^ n ^ ";"
-  in
-  "Status: " ^ path ^ name
-
-let pr_mkcases l =
-  let l = List.map (String.concat " ") l in
-  "[" ^ String.concat " | " l ^ "]"
-
-let pr_goals_aux g =
-  if g.fg_goals = [] then
-    if g.bg_goals = [] then "Proof completed."
-    else
-      let rec pr_focus _ = function
-      | [] -> assert false
-      | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg)
-      | (lg, rg) :: l ->
-        Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l
-      in
-      Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
-  else
-    let pr_menu s = s in
-    let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
-      "[" ^ String.concat "; " (List.map pr_menu hyps) ^ " |- " ^ pr_menu goal ^ "]"
-    in
-    String.concat " " (List.map pr_goal g.fg_goals)
-
-let pr_goals = function
-| None -> "No proof in progress."
-| Some g -> pr_goals_aux g
-
-let pr_evar ev = "[" ^ ev.evar_info ^ "]"
-
-let pr_evars = function
-| None -> "No proof in progress."
-| Some evars -> String.concat " " (List.map pr_evar evars)
-
+let pr_value v = pr_value_gen (fun _ -> "FIXME") v
 let pr_full_value call value =
-  match call with
-    | Interp _ -> pr_value_gen pr_string (Obj.magic value : string value)
-    | Rewind i -> pr_value_gen string_of_int (Obj.magic value : int value)
-    | Goal -> pr_value_gen pr_goals (Obj.magic value : goals option 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)
-    | MkCases s -> pr_value_gen pr_mkcases (Obj.magic value : string list list value)
-    | Quit -> pr_value value
-    | About -> pr_value value
-
+  let rec pr = function
+  | Unit          -> Obj.magic pr_unit
+  | Bool          -> Obj.magic pr_bool
+  | String        -> Obj.magic pr_string
+  | Int           -> Obj.magic pr_int
+  | State         -> Obj.magic pr_status
+  | Option_state  -> Obj.magic pr_option_state
+  | Coq_info      -> Obj.magic pr_coq_info
+  | Goals         -> Obj.magic pr_goal
+  | Evar          -> Obj.magic pr_evar
+  | List t        -> Obj.magic (pr_list (pr t))
+  | Option t      -> Obj.magic (pr_option (pr t))
+  | Coq_object t  -> Obj.magic pr_coq_object
+  | Pair (t1,t2)  -> Obj.magic (pr_pair (pr t1) (pr t2))
+  | Union (t1,t2) -> Obj.magic (pr_union (pr t1) (pr t2))
+  in
+  pr_value_gen (pr (expected_answer_type call)) value
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 6a6d2740a..3ecf066be 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -18,82 +18,18 @@ type 'a call
 
 type unknown
 
-(** Running a command (given as a string).
-    - The 1st flag indicates whether to use "raw" mode
-      (less sanity checks, no impact on the undo stack).
-      Suitable e.g. for queries, or for the Set/Unset
-      of display options that coqide performs all the time.
-    - The 2nd flag controls the verbosity.
-    - The returned string contains the messages produced
-      by this command, but not the updated goals (they are
-      to be fetch by a separated [current_goals]). *)
-val interp : raw * verbose * string -> string call
-
-(** Backtracking by at least a certain number of phrases.
-    No finished proofs will be re-opened. Instead,
-    we continue backtracking until before these proofs,
-    and answer the amount of extra backtracking performed.
-    Backtracking by more than the number of phrases already
-    interpreted successfully (and not yet undone) will fail. *)
-val rewind : int -> int call
-
-(** Fetching the list of current goals. Return [None] if no proof is in 
-    progress, [Some gl] otherwise. *)
-val goals : goals option call
-
-(** Retrieving the tactics applicable to the current goal. [None] if there is 
-    no proof in progress. *)
-val hints : (hint list * hint) option call
-
-(** The status, for instance "Ready in SomeSection, proving Foo" *)
-val status : status call
-
-(** Is a directory part of Coq's loadpath ? *)
-val inloadpath : string -> bool call
-
-(** Create a "match" template for a given inductive type.
-    For each branch of the match, we list the constructor name
-    followed by enough pattern variables. *)
-val mkcases : string -> string list list call
-
-(** Retrieve the list of unintantiated evars in the current proof. [None] if no
-    proof is in progress. *)
-val evars : evar list option call
-
-(** Search for objects satisfying the given search flags. *)
-val search : search_flags -> string coq_object list call
-
-(** Retrieve the list of options of the current toplevel, together with their 
-    state. *)
-val get_options : (option_name * option_state) list call
-
-(** Set the options to the given value. Warning: this is not atomic, so whenever
-    the call fails, the option state can be messed up... This is the caller duty
-    to check that everything is correct. *)
-val set_options : (option_name * option_value) list -> unit call
-
-(** Quit gracefully the interpreter. *)
-val quit : unit call
-
-(** The structure that coqtop should implement *)
-
-type handler = {
-  (* spiwack: [Inl] for safe and [Inr] for unsafe. *)
-  interp : raw * verbose * string -> (string,string) Util.union;
-  rewind : int -> int;
-  goals : unit -> goals option;
-  evars : unit -> evar list option;
-  hints : unit -> (hint list * hint) option;
-  status : unit -> status;
-  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;
-  mkcases : string -> string list list;
-  quit : unit -> unit;
-  about : unit -> coq_info;
-  handle_exn : exn -> location * string;
-}
+val interp      : interp_sty      -> interp_rty call
+val rewind      : rewind_sty      -> rewind_rty call
+val goals       : goals_sty       -> goals_rty call
+val hints       : hints_sty       -> hints_rty call
+val status      : status_sty      -> status_rty call
+val inloadpath  : inloadpath_sty  -> inloadpath_rty call
+val mkcases     : mkcases_sty     -> mkcases_rty call
+val evars       : evars_sty       -> evars_rty call
+val search      : search_sty      -> search_rty call
+val get_options : get_options_sty -> get_options_rty call
+val set_options : set_options_sty -> set_options_rty call
+val quit        : quit_sty        -> quit_rty call
 
 val abstract_eval_call : handler -> 'a call -> 'a value
 
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 681f0f2c8..bd3067d96 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -305,20 +305,20 @@ let eval_call c =
     r
   in
   let handler = {
-    Serialize.interp = interruptible interp;
-    Serialize.rewind = interruptible Backtrack.back;
-    Serialize.goals = interruptible goals;
-    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;
-    Serialize.mkcases = interruptible Vernacentries.make_cases;
-    Serialize.quit = (fun () -> quit := true);
-    Serialize.about = interruptible about;
-    Serialize.handle_exn = handle_exn; }
+    Interface.interp = interruptible interp;
+    Interface.rewind = interruptible Backtrack.back;
+    Interface.goals = interruptible goals;
+    Interface.evars = interruptible evars;
+    Interface.hints = interruptible hints;
+    Interface.status = interruptible status;
+    Interface.search = interruptible search;
+    Interface.inloadpath = interruptible inloadpath;
+    Interface.get_options = interruptible get_options;
+    Interface.set_options = interruptible set_options;
+    Interface.mkcases = interruptible Vernacentries.make_cases;
+    Interface.quit = (fun () -> quit := true);
+    Interface.about = interruptible about;
+    Interface.handle_exn = handle_exn; }
   in
   (* If the messages of last command are still there, we remove them *)
   ignore (read_stdout ());