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

1 files changed, 12 insertions, 76 deletions

diff --git a/lib/serialize.mli b/lib/serialize.mli
index 6a6d2740ab..3ecf066bef 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