[ide] Move common protocol library to its own folder/object.

The `ide` folder contains two different binaries, the language server
`coqidetop` and `coqide` itself.

Even if these binaries are in the same folder, the only thing they
have in common is that they link to the protocol files. In the OCaml
world, having "doubly" linked files in the same project is considered
a bit of an ugly practice, and some build tools such as Dune disallow it.q

Thus, to clean up the build, we move the common protocol files to its
own library `ideprotocol`.

This helps towards Dune integration and towards having an IDE
standalone target, such as the one that was implemented here:
https://github.com/ejgallego/coqide-exp

1 files changed, 261 insertions, 0 deletions

diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml
new file mode 100644
index 0000000000..debbc8301e
--- /dev/null
+++ b/ide/protocol/interface.ml
@@ -0,0 +1,261 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** * Declarative part of the interface of CoqIde calls to Coq *)
+
+(** * Generic structures *)
+
+type raw = bool
+type verbose = bool
+
+(** The type of coqtop goals *)
+type goal = {
+  goal_id : string;
+  (** Unique goal identifier *)
+  goal_hyp : Pp.t list;
+  (** List of hypotheses *)
+  goal_ccl : Pp.t;
+  (** Goal conclusion *)
+}
+
+type evar = {
+  evar_info : string;
+  (** A string describing an evar: type, number, environment *)
+}
+
+type status = {
+  status_path : string list;
+  (** Module path of the current proof *)
+  status_proofname : string option;
+  (** Current proof name. [None] if no focussed proof is in progress *)
+  status_allproofs : string list;
+  (** List of all pending proofs. Order is not significant *)
+  status_proofnum : int;
+  (** An id describing the state of the current proof. *)
+}
+
+type 'a pre_goals = {
+  fg_goals : 'a list;
+  (** List of the focussed goals *)
+  bg_goals : ('a list * 'a list) list;
+  (** Zipper representing the unfocused background goals *)
+  shelved_goals : 'a list;
+  (** List of the goals on the shelf. *)
+  given_up_goals : 'a list;
+  (** List of the goals that have been given up *)
+}
+
+type goals = goal pre_goals
+
+type hint = (string * string) list
+(** A list of tactics applicable and their appearance *)
+
+type option_name = string list
+
+type option_value =
+  | BoolValue   of bool
+  | IntValue    of int option
+  | StringValue of string
+  | StringOptValue of string option
+
+(** Summary of an option status *)
+type option_state = {
+  opt_sync  : bool;
+  (** Whether an option is synchronous *)
+  opt_depr  : bool;
+  (** Wheter an option is deprecated *)
+  opt_name  : string;
+  (** A short string that is displayed when using [Test] *)
+  opt_value : option_value;
+  (** The current value of the option *)
+}
+
+type search_constraint =
+(** Whether the name satisfies a regexp (uses Ocaml Str syntax) *)
+| Name_Pattern of string
+(** Whether the object type satisfies a pattern *)
+| Type_Pattern of string
+(** Whether some subtype of object type satisfies a pattern *)
+| SubType_Pattern of string
+(** Whether the object pertains to a module *)
+| In_Module of string list
+(** Bypass the Search blacklist *)
+| Include_Blacklist
+
+(** A list of search constraints; the boolean flag is set to [false] whenever
+    the flag should be negated. *)
+type search_flags = (search_constraint * bool) list
+
+(** 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 = {
+  coq_object_prefix : string list;
+  coq_object_qualid : string list;
+  coq_object_object : 'a;
+}
+
+type coq_info = {
+  coqtop_version : string;
+  protocol_version : string;
+  release_date : string;
+  compile_date : string;
+}
+
+(** Calls result *)
+
+type location = (int * int) option (* start and end of the error *)
+type state_id = Stateid.t
+type route_id = Feedback.route_id
+
+(* Obsolete *)
+type edit_id  = int
+
+(* The fail case carries the current state_id of the prover, the GUI
+   should probably retract to that point *)
+type 'a value =
+  | Good of 'a
+  | Fail of (state_id * location * Pp.t)
+
+type ('a, 'b) union = ('a, 'b) Util.union
+
+(* Request/Reply message protocol between Coq and CoqIde *)
+
+(**  [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 [(id,(rc,s)] is the new state
+     [id] assigned to the phrase. [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
+
+     [s] used to contain Coq's console output and has been deprecated
+     in favor of sending feedback, it will be removed in a future
+     version of the protocol.  *)
+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
+    performed 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].
+
+    query used to reply with the contents of Coq's console output, and
+    has been deprecated in favor of sending the query answers as
+    feedback. It will be removed in a future version of the protocol.
+*)
+type query_sty = route_id * (string * state_id)
+type query_rty = unit
+
+(** 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 uninstantiated 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", the
+    input boolean (if true) forces the evaluation of all unevaluated
+    statements *)
+type status_sty = bool
+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
+
+(** 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
+
+(* Initialize, and return the initial state id.  The argument is the filename.
+ * If its directory is not in dirpath, it adds it.  It also loads
+ * compilation hints for the filename. *)
+type init_sty = string option
+type init_rty = state_id
+
+type about_sty = unit
+type about_rty = coq_info
+
+type handle_exn_sty = Exninfo.iexn
+type handle_exn_rty = state_id * location * Pp.t
+
+(* Retrocompatibility stuff *)
+type interp_sty = (raw * verbose) * string
+(* spiwack: [Inl] for safe and [Inr] for unsafe. *)
+type interp_rty = state_id * (string,string) Util.union
+
+type stop_worker_sty = string
+type stop_worker_rty = unit
+
+type print_ast_sty = state_id
+type print_ast_rty = Xml_datatype.xml
+
+type annotate_sty = string
+type annotate_rty = Xml_datatype.xml
+
+type wait_sty = unit
+type wait_rty = unit
+
+type handler = {
+  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;
+  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;
+  mkcases     : mkcases_sty     -> mkcases_rty;
+  about       : about_sty       -> about_rty;
+  stop_worker : stop_worker_sty -> stop_worker_rty;
+  print_ast   : print_ast_sty   -> print_ast_rty;
+  annotate    : annotate_sty    -> annotate_rty;
+  handle_exn  : handle_exn_sty  -> handle_exn_rty;
+  init        : init_sty        -> init_rty;
+  quit        : quit_sty        -> quit_rty;
+  (* for internal use (fake_id) only, do not use *)
+  wait        : wait_sty        -> wait_rty;
+  (* Retrocompatibility stuff *)
+  interp      : interp_sty      -> interp_rty;
+}
+