From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 ide/protocol/interface.ml | 261 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 261 insertions(+)
 create mode 100644 ide/protocol/interface.ml

(limited to 'ide/protocol/interface.ml')

diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml
new file mode 100644
index 00000000..debbc830
--- /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;
+}
+
-- 
cgit v1.2.3