CoqIDE protocol/serialization revised

- both requests and responses are serialized using the same generic code
- no more interp message.  Replaced by:
  - query: performs a query (Search/Check...) at a given state
  - add: adds to the document a new sentence at the current edit point
  - edit_at: changes the edit point.  the result could be a rewind _or_
    a focus to a specific zone that can be edited without rewinding the
    whole document

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

3 files changed, 591 insertions, 575 deletions

diff --git a/lib/interface.mli b/lib/interface.mli
index 144b98252b..0a92e87dd8 100644
--- a/lib/interface.mli
+++ b/lib/interface.mli
@@ -142,23 +142,32 @@ type 'a value =
   | Good of 'a
   | Fail of (state_id * location * string)
 
+type ('a, 'b) union = ('a, 'b) Util.union
+
 (* Request/Reply message protocol between Coq and CoqIde *)
 
-(** Running a command (given as its id and its text).
-    "raw" mode (less sanity checks, no impact on the undo stack)
-    is suitable for queries, or for the Set/Unset
-    of display options that coqide performs all the time.
-    The returned string contains the messages produced
-    but not the updated goals (they are
-    to be fetch by a separated [current_goals]).
-    If edit_id=0 then the command is not part of the proof script,
-    and the resulting state_id is going to be dummy *)
-type interp_sty = edit_id * raw * verbose * string
-type interp_rty = state_id * string
-
-(** Backtracking to a particular state *)
-type backto_sty = state_id
-type backto_rty = unit
+(**  [add ((s,eid),(sid,v))] adds the phrase [s] with edit id [eid]
+     on top of the current edit position (that is asserted to be [sid])
+     verbosely if [v] is true.  The response [(is,(rc,s)] is the new state
+     [id] assigned to the phrase, some output [s].  [rc] is [Inl] if the new
+     state id is the tip of the edit point, or [Inr tip] if the new phrase
+     closes a focus and [tip] is the new edit tip *)
+type add_sty = (string * edit_id) * (state_id * verbose)
+type add_rty = state_id * ((unit, state_id) union * string)
+
+(** [edit_at id] declares the user wants to edit just after [id].
+    The response is [Inl] if the document has been rewound to that point,
+    [Inr (start,(stop,tip))] if [id] is in a zone that can be focused.
+    In that case the zone is delimited by [start] and [stop] while [tip]
+    is the new document [tip].  Edits made by subsequent [add] are always
+    performend on top of [id]. *)
+type edit_at_sty = state_id
+type edit_at_rty = (unit, state_id * (state_id * state_id)) union
+
+(** [query s id] executes [s] at state [id] and does not record any state
+    change but for the printings that are sent in response *)
+type query_sty = string * state_id
+type query_rty = string
 
 (** Fetching the list of current goals. Return [None] if no proof is in
     progress, [Some gl] otherwise. *)
@@ -220,8 +229,9 @@ type handle_exn_sty = exn
 type handle_exn_rty = state_id * location * string
 
 type handler = {
-  interp      : interp_sty      -> interp_rty;
-  backto      : backto_sty      -> backto_rty;
+  add         : add_sty         -> add_rty;
+  edit_at     : edit_at_sty     -> edit_at_rty;
+  query       : query_sty       -> query_rty;
   goals       : goals_sty       -> goals_rty;
   evars       : evars_sty       -> evars_rty;
   hints       : hints_sty       -> hints_rty;
diff --git a/lib/serialize.ml b/lib/serialize.ml
index c1933ad90c..aded47984b 100644
--- a/lib/serialize.ml
+++ b/lib/serialize.ml
@@ -10,215 +10,53 @@
 
 (** WARNING: TO BE UPDATED WHEN MODIFIED! *)
 
-let protocol_version = "20130516"
+let protocol_version = "20130918"
 
 (** * Interface of calls to Coq by CoqIde *)
 
+open Util
 open Interface
 open Xml_datatype
 
-(** We use phantom types and GADT to protect ourselves against wild casts *)
-
-type 'a call =
-  | Interp     of interp_sty
-  | Backto     of backto_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
-  | Init       of init_sty
-
-type unknown
-
-(** The actual calls *)
-
-let interp x      : interp_rty call      = Interp x
-let backto x      : backto_rty call      = Backto 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
-let init x        : init_rty call        = Init x
-
-(** * Coq answers to CoqIde *)
-
-let abstract_eval_call handler (c : 'a call) =
-  let mkGood x : 'a value = Good (Obj.magic x) in
-  try
-    match c with
-      | Interp x     -> mkGood (handler.interp x)
-      | Backto x     -> mkGood (handler.backto 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)
-      | Init x       -> mkGood (handler.init x)
-  with any ->
-    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 option_t       : 'a val_t -> 'a option val_t
-  val list_t         : 'a val_t -> 'a list 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
-
-  val goals_t        : goals val_t
-  val evar_t         : evar val_t
-  val state_t        : status val_t
-  val option_state_t : option_state val_t
-  val coq_info_t     : coq_info val_t
-  val coq_object_t   : 'a val_t -> 'a coq_object val_t
-  val state_id_t     : state_id val_t
-
-  type value_type = private
-    | Unit | String | Int | Bool
-
-    | Option of value_type
-    | List of value_type
-    | Pair of value_type * value_type
-    | Union of value_type * value_type
-    
-    | Goals | Evar | State | Option_state | Coq_info
-    | Coq_object of value_type
-    | State_id
-
-  val check : 'a val_t -> value_type
-
-end = struct
-
-  type value_type =
-    | Unit | String | Int | Bool
-
-    | Option of value_type
-    | List of value_type
-    | Pair of value_type * value_type
-    | Union of value_type * value_type
-    
-    | Goals | Evar | State | Option_state | Coq_info
-    | Coq_object of value_type
-    | State_id
-
-  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 option_t x     = Option x
-  let list_t x       = List x
-  let pair_t x y     = Pair (x, y)
-  let union_t x y    = Union (x, y)
-
-  let goals_t        = Goals
-  let evar_t         = Evar
-  let state_t        = State
-  let option_state_t = Option_state
-  let coq_info_t     = Coq_info
-  let coq_object_t x = Coq_object x
-  let state_id_t     = State_id
-
-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
-  let interp_t = pair_t state_id_t string_t in
-  match call with
-  | Interp _     -> check (interp_t                     : interp_rty      val_t)
-  | Backto _     -> check (unit_t                       : backto_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)
-  | Init _       -> check (state_id_t                   : init_rty        val_t)
-
-(** * XML data marshalling *)
+(* Marshalling of basic types and type constructors *)
+module Xml_marshalling = struct (* {{{ *)
 
 exception Marshal_error
 
 (** Utility functions *)
 
 let rec has_flag (f : string) = function
-| [] -> false
-| (k, _) :: l -> CString.equal k f || has_flag f l
+  | [] -> false
+  | (k, _) :: l -> CString.equal k f || has_flag f l
 
 let rec get_attr attr = function
-| [] -> raise Not_found
-| (k, v) :: l ->
-  if CString.equal k attr then v else get_attr attr l
+  | [] -> raise Not_found
+  | (k, v) :: l when CString.equal k attr -> v
+  | _ :: l -> get_attr attr l
 
 let massoc x l =
   try get_attr x l
   with Not_found -> raise Marshal_error
 
 let constructor t c args = Element (t, ["val", c], args)
-
-let do_match constr t mf = match constr with
-| Element (s, attrs, args) when CString.equal s t ->
-    let c = massoc "val" attrs in
-    mf c args
-| _ -> raise Marshal_error
+let do_match t mf = function
+  | Element (s, attrs, args) when CString.equal s t ->
+      let c = massoc "val" attrs in
+      mf c args
+  | _ -> raise Marshal_error
 
 let singleton = function
-| [x] -> x
-| _ -> raise Marshal_error
+  | [x] -> x
+  | _ -> raise Marshal_error
 
 let raw_string = function
-| [] -> ""
-| [PCData s] -> s
-| _ -> raise Marshal_error
-
-let bool_arg tag b = if b then [tag, ""] else []
+  | [] -> ""
+  | [PCData s] -> s
+  | _ -> raise Marshal_error
 
 (** Base types *)
 
 let of_unit () = Element ("unit", [], [])
-
 let to_unit : xml -> unit = function
   | Element ("unit", [], []) -> ()
   | _ -> raise Marshal_error
@@ -226,111 +64,88 @@ let to_unit : xml -> unit = function
 let of_bool (b : bool) : xml =
   if b then constructor "bool" "true" []
   else constructor "bool" "false" []
-
-let to_bool xml : bool = do_match xml "bool"
-  (fun s _ -> match s with
+let to_bool : xml -> bool = do_match "bool" (fun s _ -> match s with
   | "true" -> true
   | "false" -> false
   | _ -> raise Marshal_error)
 
 let of_list (f : 'a -> xml) (l : 'a list) =
   Element ("list", [], List.map f l)
-
 let to_list (f : xml -> 'a) : xml -> 'a list = function
-| Element ("list", [], l) ->
-  List.map f l
-| _ -> raise Marshal_error
+  | Element ("list", [], l) -> List.map f l
+  | _ -> raise Marshal_error
 
 let of_option (f : 'a -> xml) : 'a option -> xml = function
-| None -> Element ("option", ["val", "none"], [])
-| Some x -> Element ("option", ["val", "some"], [f x])
-
+  | None -> Element ("option", ["val", "none"], [])
+  | Some x -> Element ("option", ["val", "some"], [f x])
 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
+  | Element ("option", ["val", "none"], []) -> None
+  | Element ("option", ["val", "some"], [x]) -> Some (f x)
+  | _ -> raise Marshal_error
 
 let of_string (s : string) : xml = Element ("string", [], [PCData s])
-
 let to_string : xml -> string = function
-| Element ("string", [], l) -> raw_string l
-| _ -> raise Marshal_error
+  | Element ("string", [], l) -> raw_string l
+  | _ -> raise Marshal_error
 
 let of_int (i : int) : xml = Element ("int", [], [PCData (string_of_int i)])
-
 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 : 'a -> xml) (g : 'b -> xml) : 'a * 'b -> xml =
-  function (x,y) -> Element ("pair", [], [f x; g y])
+  | Element ("int", [], [PCData s]) ->
+    (try int_of_string s with Failure _ -> raise Marshal_error)
+  | _ -> raise Marshal_error
 
+let of_pair (f : 'a -> xml) (g : 'b -> xml) (x : 'a * 'b) : xml =
+  Element ("pair", [], [f (fst x); g (snd x)])
 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])
+  | Element ("pair", [], [x; y]) -> (f x, g y)
+  | _ -> raise Marshal_error
 
-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
+let of_union (f : 'a -> xml) (g : 'b -> xml) : ('a,'b) union -> xml = function
+  | Inl x -> Element ("union", ["val","in_l"], [f x])
+  | Inr x -> Element ("union", ["val","in_r"], [g x])
+let to_union (f : xml -> 'a) (g : xml -> 'b) : xml -> ('a,'b) union = function
+  | Element ("union", ["val","in_l"], [x]) -> Inl (f x)
+  | Element ("union", ["val","in_r"], [x]) -> Inr (g x)
+  | _ -> raise Marshal_error
 
 (** More elaborate types *)
 
 let of_option_value = function
-| IntValue i ->
-  constructor "option_value" "intvalue" [of_option of_int i]
-| BoolValue b ->
-  constructor "option_value" "boolvalue" [of_bool b]
-| StringValue s ->
-  constructor "option_value" "stringvalue" [of_string s]
-
-let to_option_value xml = do_match xml "option_value"
-  (fun s args -> match s with
+  | IntValue i -> constructor "option_value" "intvalue" [of_option of_int i]
+  | BoolValue b -> constructor "option_value" "boolvalue" [of_bool b]
+  | StringValue s -> constructor "option_value" "stringvalue" [of_string s]
+let to_option_value = do_match "option_value" (fun s args -> match s with
   | "intvalue" -> IntValue (to_option to_int (singleton args))
   | "boolvalue" -> BoolValue (to_bool (singleton args))
   | "stringvalue" -> StringValue (to_string (singleton args))
-  | _ -> raise Marshal_error
-  )
+  | _ -> raise Marshal_error)
 
 let of_option_state s =
   Element ("option_state", [], [
     of_bool s.opt_sync;
     of_bool s.opt_depr;
     of_string s.opt_name;
-    of_option_value s.opt_value]
-  )
-
+    of_option_value s.opt_value])
 let to_option_state = function
-| Element ("option_state", [], [sync; depr; name; value]) ->
-  {
-    opt_sync = to_bool sync;
-    opt_depr = to_bool depr;
-    opt_name = to_string name;
-    opt_value = to_option_value value;
-  }
-| _ -> raise Marshal_error
+  | Element ("option_state", [], [sync; depr; name; value]) -> {
+      opt_sync = to_bool sync;
+      opt_depr = to_bool depr;
+      opt_name = to_string name;
+      opt_value = to_option_value value }
+  | _ -> 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
+let of_search_cst = function
+  | Name_Pattern s ->
+    constructor "search_cst" "name_pattern" [of_string s]
+  | Type_Pattern s ->
+    constructor "search_cst" "type_pattern" [of_string s]
+  | SubType_Pattern s ->
+    constructor "search_cst" "subtype_pattern" [of_string s]
+  | In_Module m ->
+    constructor "search_cst" "in_module" [of_list of_string m]
+  | Include_Blacklist ->
+    constructor "search_cst" "include_blacklist" []
+let to_search_cst = do_match "search_cst" (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))
@@ -405,131 +220,52 @@ let to_value f = function
   else raise Marshal_error
 | _ -> raise Marshal_error
 
-let of_call = function
-| Interp (id,raw, vrb, cmd) ->
-  let flags = (bool_arg "raw" raw) @ (bool_arg "verbose" vrb) in
-  Element ("call", ("val", "interp") :: ("id", string_of_int id) :: flags,
-  [PCData cmd])
-| Backto id ->
-  Element ("call", ["val", "backto"], [of_state_id id])
-| Goal () ->
-  Element ("call", ["val", "goal"], [])
-| Evars () ->
-  Element ("call", ["val", "evars"], [])
-| Hints () ->
-  Element ("call", ["val", "hints"], [])
-| Status b ->
-  Element ("call", ["val", "status";"force",string_of_bool b], [])
-| 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 ->
-  let args = List.map (of_pair (of_list of_string) of_option_value) opts in
-  Element ("call", ["val", "setoptions"], args)
-| InLoadPath file ->
-  Element ("call", ["val", "inloadpath"], [PCData file])
-| MkCases ind ->
-  Element ("call", ["val", "mkcases"], [PCData ind])
-| Quit () ->
-  Element ("call", ["val", "quit"], [])
-| About () ->
-  Element ("call", ["val", "about"], [])
-| Init () ->
-  Element ("call", ["val", "init"], [])
-
-let to_call = function
-| Element ("call", attrs, l) ->
-  let ans = massoc "val" attrs in
-  begin match ans with
-  | "interp" ->
-    let id = get_attr "id" attrs in
-    let raw = has_flag "raw" attrs in
-    let vrb = has_flag "verbose" attrs in
-    Interp (int_of_string id, raw, vrb, raw_string l)
-  | "backto" ->
-      (match l with
-      | [id] -> Backto(to_state_id id)
-      | _ -> raise Marshal_error)
-  | "goal" -> Goal ()
-  | "evars" -> Evars ()
-  | "status" ->
-      let force = get_attr "force" attrs in
-      Status (bool_of_string force)
-  | "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
-    SetOptions args
-  | "inloadpath" -> InLoadPath (raw_string l)
-  | "mkcases" -> MkCases (raw_string l)
-  | "hints" -> Hints ()
-  | "quit" -> Quit ()
-  | "about" -> About ()
-  | "init" -> Init ()
-  | _ -> raise Marshal_error
-  end
-| _ -> raise Marshal_error
-
 let of_status s =
   let of_so = of_option of_string in
   let of_sl = of_list of_string in
-  Element ("status", [],
-    [
+  Element ("status", [], [
       of_sl s.status_path;
       of_so s.status_proofname;
       of_sl s.status_allproofs;
-      of_int s.status_proofnum;
-    ]
-  )
-
+      of_int s.status_proofnum; ])
 let to_status = function
-| Element ("status", [], [path; name; prfs; pnum]) ->
-  {
-    status_path = to_list to_string path;
-    status_proofname = to_option to_string name;
-    status_allproofs = to_list to_string prfs;
-    status_proofnum = to_int pnum;
-  }
-| _ -> raise Marshal_error
-
-let of_evar s =
-  Element ("evar", [], [PCData s.evar_info])
+  | Element ("status", [], [path; name; prfs; pnum]) -> {
+      status_path = to_list to_string path;
+      status_proofname = to_option to_string name;
+      status_allproofs = to_list to_string prfs;
+      status_proofnum = to_int pnum; }
+  | _ -> raise Marshal_error
 
+let of_evar s = Element ("evar", [], [PCData s.evar_info])
 let to_evar = function
-| Element ("evar", [], data) -> { evar_info = raw_string data; }
-| _ -> raise Marshal_error
+  | Element ("evar", [], data) -> { evar_info = raw_string data; }
+  | _ -> raise Marshal_error
 
 let of_goal g =
   let hyp = of_list of_string g.goal_hyp in
   let ccl = of_string g.goal_ccl in
   let id = of_string g.goal_id in
   Element ("goal", [], [id; hyp; ccl])
-
 let to_goal = function
-| Element ("goal", [], [id; hyp; ccl]) ->
-  let hyp = to_list to_string hyp in
-  let ccl = to_string ccl in
-  let id = to_string id in
-  { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
-| _ -> raise Marshal_error
+  | Element ("goal", [], [id; hyp; ccl]) ->
+    let hyp = to_list to_string hyp in
+    let ccl = to_string ccl in
+    let id = to_string id in
+    { goal_hyp = hyp; goal_ccl = ccl; goal_id = id; }
+  | _ -> raise Marshal_error
 
 let of_goals g =
   let of_glist = of_list of_goal in
   let fg = of_list of_goal g.fg_goals in
   let bg = of_list (of_pair of_glist of_glist) g.bg_goals in
   Element ("goals", [], [fg; bg])
-
 let to_goals = function
-| Element ("goals", [], [fg; bg]) ->
-  let to_glist = to_list to_goal in
-  let fg = to_list to_goal fg in
-  let bg = to_list (to_pair to_glist to_glist) bg in
-  { fg_goals = fg; bg_goals = bg; }
-| _ -> raise Marshal_error
+  | Element ("goals", [], [fg; bg]) ->
+    let to_glist = to_list to_goal in
+    let fg = to_list to_goal fg in
+    let bg = to_list (to_pair to_glist to_glist) bg in
+    { fg_goals = fg; bg_goals = bg; }
+  | _ -> raise Marshal_error
 
 let of_coq_info info =
   let version = of_string info.coqtop_version in
@@ -537,26 +273,21 @@ let of_coq_info info =
   let release = of_string info.release_date in
   let compile = of_string info.compile_date in
   Element ("coq_info", [], [version; protocol; release; compile])
-
 let to_coq_info = function
-| Element ("coq_info", [], [version; protocol; release; compile]) ->
-  {
-    coqtop_version = to_string version;
-    protocol_version = to_string protocol;
-    release_date = to_string release;
-    compile_date = to_string compile;
-  }
-| _ -> raise Marshal_error
+  | Element ("coq_info", [], [version; protocol; release; compile]) -> {
+      coqtop_version = to_string version;
+      protocol_version = to_string protocol;
+      release_date = to_string release;
+      compile_date = to_string compile; }
+  | _ -> raise Marshal_error
 
 let of_message_level = function
-| Debug s -> constructor "message_level" "debug" [PCData s]
-| Info -> constructor "message_level" "info" []
-| Notice -> constructor "message_level" "notice" []
-| Warning -> constructor "message_level" "warning" []
-| Error -> constructor "message_level" "error" []
-
-let to_message_level xml = do_match xml "message_level"
-  (fun s args -> match s with
+  | Debug s -> constructor "message_level" "debug" [PCData s]
+  | Info -> constructor "message_level" "info" []
+  | Notice -> constructor "message_level" "notice" []
+  | Warning -> constructor "message_level" "warning" []
+  | Error -> constructor "message_level" "error" []
+let to_message_level = do_match "message_level" (fun s args -> match s with
   | "debug" -> Debug (raw_string args)
   | "info" -> Info
   | "notice" -> Notice
@@ -568,217 +299,491 @@ let of_message msg =
   let lvl = of_message_level msg.message_level in
   let content = of_string msg.message_content in
   Element ("message", [], [lvl; content])
-
 let to_message xml = match xml with
-| Element ("message", [], [lvl; content]) ->
-  { message_level = to_message_level lvl; message_content = to_string content }
-| _ -> raise Marshal_error
+  | Element ("message", [], [lvl; content]) -> {
+      message_level = to_message_level lvl;
+      message_content = to_string content }
+  | _ -> raise Marshal_error
 
 let is_message = function
-| Element ("message", _, _) -> true
-| _ -> false
+  | Element ("message", _, _) -> true
+  | _ -> false
 
 let of_loc loc =
   let start, stop = Loc.unloc loc in
   Element ("loc",[("start",string_of_int start);("stop",string_of_int stop)],[])
-
 let to_loc xml = match xml with
-| Element ("loc", l,[]) ->
-    (try
-      let start = get_attr "start" l in
-      let stop = get_attr "stop" l in
-      Loc.make_loc (int_of_string start, int_of_string stop)
-    with Not_found | Invalid_argument _ -> raise Marshal_error)
-| _ -> raise Marshal_error
+  | Element ("loc", l,[]) ->
+      (try
+        let start = massoc "start" l in
+        let stop = massoc "stop" l in
+        Loc.make_loc (int_of_string start, int_of_string stop)
+      with Not_found | Invalid_argument _ -> raise Marshal_error)
+  | _ -> raise Marshal_error
 
-let to_feedback_content xml = do_match xml "feedback_content"
-  (fun s args -> match s with
-  | "addedaxiom" -> AddedAxiom
-  | "processed" -> Processed
-  | "globref" ->
-       (match args with
-       | [loc; filepath; modpath; ident; ty] ->
-            GlobRef(to_loc loc, to_string filepath, to_string modpath,
-                    to_string ident, to_string ty)
-       | _ -> raise Marshal_error)
-  | "errormsg" ->
-       (match args with
-       | [loc;  s] -> ErrorMsg (to_loc loc, to_string s)
-       | _ -> raise Marshal_error)
-  | "inprogress" -> 
-       (match args with
-       | [n] -> InProgress (to_int n)
-       | _ -> raise Marshal_error)
+let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
+  | "addedaxiom", _ -> AddedAxiom
+  | "processed", _ -> Processed
+  | "globref", [loc; filepath; modpath; ident; ty] ->
+       GlobRef(to_loc loc, to_string filepath,
+         to_string modpath, to_string ident, to_string ty)
+  | "errormsg", [loc;  s] -> ErrorMsg (to_loc loc, to_string s)
+  | "inprogress", [n] -> InProgress (to_int n)
   | _ -> raise Marshal_error)
-
 let of_feedback_content = function
-| AddedAxiom -> constructor "feedback_content" "addedaxiom" []
-| Processed -> constructor "feedback_content" "processed" []
-| GlobRef(loc, filepath, modpath, ident, ty) ->
-    constructor "feedback_content" "globref" [
-      of_loc loc;
-      of_string filepath;
-      of_string modpath;
-      of_string ident;
-      of_string ty
-    ]
-| ErrorMsg(loc, s) ->
-    constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
-| InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
+  | AddedAxiom -> constructor "feedback_content" "addedaxiom" []
+  | Processed -> constructor "feedback_content" "processed" []
+  | GlobRef(loc, filepath, modpath, ident, ty) ->
+      constructor "feedback_content" "globref" [
+        of_loc loc;
+        of_string filepath;
+        of_string modpath;
+        of_string ident;
+        of_string ty ]
+  | ErrorMsg(loc, s) ->
+      constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
+  | InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
 
 let of_feedback msg =
   let content = of_feedback_content msg.content in
   let obj, id = of_edit_or_state_id msg.id in
   Element ("feedback", obj, [id;content])
-
 let to_feedback xml = match xml with
-| Element ("feedback", ["object","edit"], [id;content]) ->
-  { id = Interface.Edit(to_edit_id id); content = to_feedback_content content }
-| Element ("feedback", ["object","state"], [id;content]) ->
-  { id = Interface.State(to_state_id id);
-    content = to_feedback_content content }
-| _ -> raise Marshal_error
+  | Element ("feedback", ["object","edit"], [id;content]) -> {
+      id = Interface.Edit(to_edit_id id);
+      content = to_feedback_content content }
+  | Element ("feedback", ["object","state"], [id;content]) -> { 
+      id = Interface.State(to_state_id id);
+      content = to_feedback_content content }
+  | _ -> raise Marshal_error
 
-let is_feedback = function
-| Element ("feedback", _, _) -> true
-| _ -> false
-
-(** 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.  *)
-
-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))
-    | Union (t1,t2) -> Obj.magic (of_union (convert t1) (convert t2))
-    | State_id      -> Obj.magic of_state_id
-  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))
-    | Union (t1,t2) -> Obj.magic (to_union (convert t1) (convert t2))
-    | State_id      -> Obj.magic to_state_id
-  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."
+end (* }}} *)
+include Xml_marshalling
+
+(* Reification of basic types and type constructors, and functions
+   from to xml *)
+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 option_t       : 'a val_t -> 'a option val_t
+  val list_t         : 'a val_t -> 'a list 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) union val_t
+
+  val goals_t        : goals val_t
+  val evar_t         : evar val_t
+  val state_t        : status val_t
+  val option_state_t : option_state val_t
+  val option_value_t : option_value val_t
+  val coq_info_t     : coq_info val_t
+  val coq_object_t   : 'a val_t -> 'a coq_object val_t
+  val state_id_t     : state_id val_t
+  val search_cst_t   : search_constraint val_t
+
+  val of_value_type : 'a val_t -> 'a -> xml
+  val to_value_type : 'a val_t -> xml -> 'a
+
+  val print         : 'a val_t -> 'a -> string
+
+end = struct
+
+  type value_type =
+    | Unit | String | Int | Bool
+
+    | Option of value_type
+    | List of value_type
+    | Pair of value_type * value_type
+    | Union of value_type * value_type
+    
+    | Goals | Evar | State | Option_state | Option_value | Coq_info
+    | Coq_object of value_type
+    | State_id
+    | Search_cst
+
+  type 'a val_t = value_type
+
+  let unit_t         = Unit
+  let string_t       = String
+  let int_t          = Int
+  let bool_t         = Bool
+
+  let option_t x     = Option x
+  let list_t x       = List x
+  let pair_t x y     = Pair (x, y)
+  let union_t x y    = Union (x, y)
+
+  let goals_t        = Goals
+  let evar_t         = Evar
+  let state_t        = State
+  let option_state_t = Option_state
+  let option_value_t = Option_value
+  let coq_info_t     = Coq_info
+  let coq_object_t x = Coq_object x
+  let state_id_t     = State_id
+  let search_cst_t   = Search_cst
+
+  let of_value_type (ty : 'a val_t) : 'a -> 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
+      | Option_value  -> Obj.magic of_option_value
+      | 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))
+      | State_id      -> Obj.magic of_state_id
+      | Search_cst    -> Obj.magic of_search_cst
+    in
+      convert ty
+  
+  let to_value_type (ty : 'a val_t) : xml -> 'a =
+    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
+      | Option_value  -> Obj.magic to_option_value
+      | 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))
+      | State_id      -> Obj.magic to_state_id
+      | Search_cst    -> Obj.magic to_search_cst
+    in
+      convert ty
+
+  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 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_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 (id,r,b,s) ->
-    let raw = if r then "RAW" else "" in
-    let verb = if b then "" else "SILENT" in
-    "INTERP"^raw^verb^" "^string_of_int id^" ["^s^"]"
-  | Backto i -> "BACKTO "^(Stateid.to_string i)
-  | Goal _ -> "GOALS"
-  | Evars _ -> "EVARS"
-  | Hints _ -> "HINTS"
-  | Status b -> "STATUS " ^ string_of_bool b
-  | Search _ -> "SEARCH"
-  | 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"
-  | Init _ -> "INIT"
-let pr_value_gen pr = function
-  | Good v -> "GOOD " ^ pr v
-  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^str^"]"
-  | Fail (id,Some(i,j),str) ->
-      "FAIL "^Stateid.to_string id^
-        " ("^string_of_int i^","^string_of_int j^")["^str^"]"
-let pr_value v = pr_value_gen (fun _ -> "FIXME") v
-let pr_full_value call value =
-  let rec pr = function
+      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_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 Inl x -> "Inl "^pr1 x | Inr x -> "Inr "^pr2 x
+
+  let pr_search_cst = function
+    | Name_Pattern s -> "Name_Pattern " ^ s
+    | Type_Pattern s -> "Type_Pattern " ^ s
+    | SubType_Pattern s -> "SubType_Pattern " ^ s
+    | In_Module s -> "In_Module " ^ String.concat "." s
+    | Include_Blacklist -> "Include_Blacklist"
+
+  let rec print = 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
+  | Option_value  -> Obj.magic pr_option_value
+  | Search_cst    -> Obj.magic pr_search_cst
   | 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))
+  | List t        -> Obj.magic (pr_list (print t))
+  | Option t      -> Obj.magic (pr_option (print 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))
+  | Pair (t1,t2)  -> Obj.magic (pr_pair (print t1) (print t2))
+  | Union (t1,t2) -> Obj.magic (pr_union (print t1) (print t2))
   | State_id      -> Obj.magic pr_int
-  in
-  pr_value_gen (pr (expected_answer_type call)) value
+
+end  (* }}} *)
+open ReifType
+
+type 'a call =
+  | Add        of add_sty
+  | Edit_at    of edit_at_sty
+  | Query      of query_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
+  | Init       of init_sty
+
+let str_of_call = function
+  | Add _        -> "Add"
+  | Edit_at _    -> "Edit_at"
+  | Query _      -> "Query"
+  | Goal _       -> "Goal"
+  | Evars _      -> "Evars"
+  | Hints _      -> "Hints"
+  | Status _     -> "Status"
+  | Search _     -> "Search"
+  | GetOptions _ -> "GetOptions"
+  | SetOptions _ -> "SetOptions"
+  | InLoadPath _ -> "InLoadPath"
+  | MkCases _    -> "MkCases"
+  | Quit _       -> "Quit"
+  | About _      -> "About"
+  | Init _       -> "Init"
+
+type unknown
+
+(** We use phantom types and GADT to protect ourselves against wild casts *)
+let add x         : add_rty call         = Add x
+let edit_at x     : edit_at_rty call     = Edit_at x
+let query x       : query_rty call       = Query 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
+let init x        : init_rty call        = Init x
+
+let abstract_eval_call handler (c : 'a call) : 'a value =
+  let mkGood x : 'a value = Good (Obj.magic x) in
+  try
+    match c with
+    | Add x        -> mkGood (handler.add x)
+    | Edit_at x    -> mkGood (handler.edit_at x)
+    | Query x      -> mkGood (handler.query 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)
+    | Init x       -> mkGood (handler.init x)
+  with any ->
+    Fail (handler.handle_exn any)
+
+(** Types reification, checked with explicit casts *)
+let add_sty_t : add_sty val_t = 
+  pair_t (pair_t string_t int_t) (pair_t state_id_t bool_t)
+let edit_at_sty_t : edit_at_sty val_t = state_id_t
+let query_sty_t : query_sty val_t = pair_t string_t state_id_t
+let goals_sty_t : goals_sty val_t = unit_t
+let evars_sty_t : evars_sty val_t = unit_t
+let hints_sty_t : hints_sty val_t = unit_t
+let status_sty_t : status_sty val_t = bool_t
+let search_sty_t : search_sty val_t = list_t (pair_t search_cst_t bool_t)
+let get_options_sty_t : get_options_sty val_t = unit_t
+let set_options_sty_t : set_options_sty val_t =
+  list_t (pair_t (list_t string_t) option_value_t)
+let inloadpath_sty_t : inloadpath_sty val_t = string_t
+let mkcases_sty_t : mkcases_sty val_t = string_t
+let quit_sty_t : quit_sty val_t = unit_t
+let about_sty_t : about_sty val_t = unit_t
+let init_sty_t : init_sty val_t = unit_t
+
+let add_rty_t : add_rty val_t =
+  pair_t state_id_t (pair_t (union_t unit_t state_id_t) string_t)
+let edit_at_rty_t : edit_at_rty val_t =
+  union_t unit_t (pair_t state_id_t (pair_t state_id_t state_id_t))
+let query_rty_t : query_rty val_t = string_t
+let goals_rty_t : goals_rty val_t = option_t goals_t
+let evars_rty_t : evars_rty val_t = option_t (list_t evar_t)
+let hints_rty_t : hints_rty val_t =
+  let hint = list_t (pair_t string_t string_t) in
+  option_t (pair_t (list_t hint) hint)
+let status_rty_t : status_rty val_t = state_t
+let search_rty_t : search_rty val_t = list_t (coq_object_t string_t)
+let get_options_rty_t : get_options_rty val_t =
+  list_t (pair_t (list_t string_t) option_state_t) 
+let set_options_rty_t : set_options_rty val_t = unit_t
+let inloadpath_rty_t : inloadpath_rty val_t = bool_t
+let mkcases_rty_t : mkcases_rty val_t = list_t (list_t string_t)
+let quit_rty_t : quit_rty val_t = unit_t
+let about_rty_t : about_rty val_t = coq_info_t
+let init_rty_t : init_rty val_t = state_id_t
+
+(** brain dead code, edit if protocol messages are added/removed {{{ *)
+let of_answer (q : 'a call) (v : 'a value) : xml = match q with
+  | Add _        -> of_value (of_value_type add_rty_t        ) (Obj.magic v)
+  | Edit_at _    -> of_value (of_value_type edit_at_rty_t    ) (Obj.magic v)
+  | Query _      -> of_value (of_value_type query_rty_t      ) (Obj.magic v)
+  | Goal _       -> of_value (of_value_type goals_rty_t      ) (Obj.magic v)
+  | Evars _      -> of_value (of_value_type evars_rty_t      ) (Obj.magic v)
+  | Hints _      -> of_value (of_value_type hints_rty_t      ) (Obj.magic v)
+  | Status _     -> of_value (of_value_type status_rty_t     ) (Obj.magic v)
+  | Search _     -> of_value (of_value_type search_rty_t     ) (Obj.magic v)
+  | GetOptions _ -> of_value (of_value_type get_options_rty_t) (Obj.magic v)
+  | SetOptions _ -> of_value (of_value_type set_options_rty_t) (Obj.magic v)
+  | InLoadPath _ -> of_value (of_value_type inloadpath_rty_t ) (Obj.magic v)
+  | MkCases _    -> of_value (of_value_type mkcases_rty_t    ) (Obj.magic v)
+  | Quit _       -> of_value (of_value_type quit_rty_t       ) (Obj.magic v)
+  | About _      -> of_value (of_value_type about_rty_t      ) (Obj.magic v)
+  | Init _       -> of_value (of_value_type init_rty_t       ) (Obj.magic v)
+
+let to_answer (q : 'a call) (x : xml) : 'a value = match q with
+  | Add _        -> Obj.magic (to_value (to_value_type add_rty_t        ) x)
+  | Edit_at _    -> Obj.magic (to_value (to_value_type edit_at_rty_t    ) x)
+  | Query _      -> Obj.magic (to_value (to_value_type query_rty_t      ) x)
+  | Goal _       -> Obj.magic (to_value (to_value_type goals_rty_t      ) x)
+  | Evars _      -> Obj.magic (to_value (to_value_type evars_rty_t      ) x)
+  | Hints _      -> Obj.magic (to_value (to_value_type hints_rty_t      ) x)
+  | Status _     -> Obj.magic (to_value (to_value_type status_rty_t     ) x)
+  | Search _     -> Obj.magic (to_value (to_value_type search_rty_t     ) x)
+  | GetOptions _ -> Obj.magic (to_value (to_value_type get_options_rty_t) x)
+  | SetOptions _ -> Obj.magic (to_value (to_value_type set_options_rty_t) x)
+  | InLoadPath _ -> Obj.magic (to_value (to_value_type inloadpath_rty_t ) x)
+  | MkCases _    -> Obj.magic (to_value (to_value_type mkcases_rty_t    ) x)
+  | Quit _       -> Obj.magic (to_value (to_value_type quit_rty_t       ) x)
+  | About _      -> Obj.magic (to_value (to_value_type about_rty_t      ) x)
+  | Init _       -> Obj.magic (to_value (to_value_type init_rty_t       ) x)
+
+let of_call (q : 'a call) : xml =
+  let mkCall x = constructor "call" (str_of_call q) [x] in
+  match q with
+  | Add x        -> mkCall (of_value_type add_sty_t         x) 
+  | Edit_at x    -> mkCall (of_value_type edit_at_sty_t     x) 
+  | Query x      -> mkCall (of_value_type query_sty_t       x) 
+  | Goal x       -> mkCall (of_value_type goals_sty_t       x) 
+  | Evars x      -> mkCall (of_value_type evars_sty_t       x) 
+  | Hints x      -> mkCall (of_value_type hints_sty_t       x) 
+  | Status x     -> mkCall (of_value_type status_sty_t      x) 
+  | Search x     -> mkCall (of_value_type search_sty_t      x) 
+  | GetOptions x -> mkCall (of_value_type get_options_sty_t x) 
+  | SetOptions x -> mkCall (of_value_type set_options_sty_t x) 
+  | InLoadPath x -> mkCall (of_value_type inloadpath_sty_t  x) 
+  | MkCases x    -> mkCall (of_value_type mkcases_sty_t     x) 
+  | Quit x       -> mkCall (of_value_type quit_sty_t        x) 
+  | About x      -> mkCall (of_value_type about_sty_t       x) 
+  | Init x       -> mkCall (of_value_type init_sty_t        x)
+
+let to_call : xml -> unknown call =
+  do_match "call" (fun s a ->
+    let mkCallArg vt a = to_value_type vt (singleton a) in
+    match s with
+    | "Add"        -> Add        (mkCallArg add_sty_t         a)
+    | "Edit_at"    -> Edit_at    (mkCallArg edit_at_sty_t     a)
+    | "Query"      -> Query      (mkCallArg query_sty_t       a)
+    | "Goal"       -> Goal       (mkCallArg goals_sty_t       a)
+    | "Evars"      -> Evars      (mkCallArg evars_sty_t       a)
+    | "Hints"      -> Hints      (mkCallArg hints_sty_t       a)
+    | "Status"     -> Status     (mkCallArg status_sty_t      a)
+    | "Search"     -> Search     (mkCallArg search_sty_t      a)
+    | "GetOptions" -> GetOptions (mkCallArg get_options_sty_t a)
+    | "SetOptions" -> SetOptions (mkCallArg set_options_sty_t a)
+    | "InLoadPath" -> InLoadPath (mkCallArg inloadpath_sty_t  a)
+    | "MkCases"    -> MkCases    (mkCallArg mkcases_sty_t     a)
+    | "Quit"       -> Quit       (mkCallArg quit_sty_t        a)
+    | "About"      -> About      (mkCallArg about_sty_t       a)
+    | "Init"       -> Init       (mkCallArg init_sty_t        a)
+    | _ -> raise Marshal_error)
+(* }}} *)
+
+(** misc *)
+
+let is_feedback = function
+  | Element ("feedback", _, _) -> true
+  | _ -> false
+
+(** {{{ Debug printing *)
+
+let pr_value_gen pr = function
+  | Good v -> "GOOD " ^ pr v
+  | Fail (id,None,str) -> "FAIL "^Stateid.to_string id^" ["^str^"]"
+  | Fail (id,Some(i,j),str) ->
+      "FAIL "^Stateid.to_string id^
+        " ("^string_of_int i^","^string_of_int j^")["^str^"]"
+let pr_value v = pr_value_gen (fun _ -> "FIXME") v
+let pr_full_value call value = match call with
+  | Add _        -> pr_value_gen (print add_rty_t        ) (Obj.magic value) 
+  | Edit_at _    -> pr_value_gen (print edit_at_rty_t    ) (Obj.magic value) 
+  | Query _      -> pr_value_gen (print query_rty_t      ) (Obj.magic value) 
+  | Goal _       -> pr_value_gen (print goals_rty_t      ) (Obj.magic value) 
+  | Evars _      -> pr_value_gen (print evars_rty_t      ) (Obj.magic value) 
+  | Hints _      -> pr_value_gen (print hints_rty_t      ) (Obj.magic value) 
+  | Status _     -> pr_value_gen (print status_rty_t     ) (Obj.magic value) 
+  | Search _     -> pr_value_gen (print search_rty_t     ) (Obj.magic value) 
+  | GetOptions _ -> pr_value_gen (print get_options_rty_t) (Obj.magic value) 
+  | SetOptions _ -> pr_value_gen (print set_options_rty_t) (Obj.magic value) 
+  | InLoadPath _ -> pr_value_gen (print inloadpath_rty_t ) (Obj.magic value) 
+  | MkCases _    -> pr_value_gen (print mkcases_rty_t    ) (Obj.magic value) 
+  | Quit _       -> pr_value_gen (print quit_rty_t       ) (Obj.magic value) 
+  | About _      -> pr_value_gen (print about_rty_t      ) (Obj.magic value) 
+  | Init _       -> pr_value_gen (print init_rty_t       ) (Obj.magic value)
+let pr_call call = match call with
+  | Add x        -> str_of_call call ^ " " ^ print add_sty_t         x
+  | Edit_at x    -> str_of_call call ^ " " ^ print edit_at_sty_t     x
+  | Query x      -> str_of_call call ^ " " ^ print query_sty_t       x
+  | Goal x       -> str_of_call call ^ " " ^ print goals_sty_t       x
+  | Evars x      -> str_of_call call ^ " " ^ print evars_sty_t       x
+  | Hints x      -> str_of_call call ^ " " ^ print hints_sty_t       x
+  | Status x     -> str_of_call call ^ " " ^ print status_sty_t      x
+  | Search x     -> str_of_call call ^ " " ^ print search_sty_t      x
+  | GetOptions x -> str_of_call call ^ " " ^ print get_options_sty_t x
+  | SetOptions x -> str_of_call call ^ " " ^ print set_options_sty_t x
+  | InLoadPath x -> str_of_call call ^ " " ^ print inloadpath_sty_t  x
+  | MkCases x    -> str_of_call call ^ " " ^ print mkcases_sty_t     x
+  | Quit x       -> str_of_call call ^ " " ^ print quit_sty_t        x
+  | About x      -> str_of_call call ^ " " ^ print about_sty_t       x
+  | Init x       -> str_of_call call ^ " " ^ print init_sty_t        x
+
+(* }}} *)
+
+(* vim: set foldmethod=marker: *)
diff --git a/lib/serialize.mli b/lib/serialize.mli
index 00e95be2ed..2b1718bf76 100644
--- a/lib/serialize.mli
+++ b/lib/serialize.mli
@@ -15,8 +15,9 @@ type 'a call
 
 type unknown
 
-val interp      : interp_sty      -> interp_rty call
-val backto      : backto_sty      -> backto_rty call
+val add         : add_sty         -> add_rty call
+val edit_at     : edit_at_sty     -> edit_at_rty call
+val query       : query_sty       -> query_rty call
 val goals       : goals_sty       -> goals_rty call
 val hints       : hints_sty       -> hints_rty call
 val status      : status_sty      -> status_rty call
@@ -51,7 +52,7 @@ val to_feedback : xml -> feedback
 val is_feedback : xml -> bool
 
 val of_answer : 'a call -> 'a value -> xml
-val to_answer : xml -> 'a call -> 'a value
+val to_answer : 'a call -> xml -> 'a value
 
 (** * Debug printing *)