Module Interface

* Declarative part of the interface of CoqIDE calls to Coq

type raw = bool
type verbose = bool
type goal = {
goal_id : string;

Unique goal identifier

goal_hyp : Pp.t list;

List of hypotheses

goal_ccl : Pp.t;

Goal conclusion

goal_name : string option;

User-level goal name

}

The type of coqtop goals

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 focused 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 focused 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
type option_state = {
opt_sync : bool;

Whether an option is synchronous

opt_depr : bool;

Whether an option is deprecated

opt_value : option_value;

The current value of the option

}

Summary of an option status

type search_constraint =
| Name_Pattern of string

Whether the name satisfies a regexp (uses Ocaml Str syntax)

| Type_Pattern of string

Whether the object type satisfies a pattern

| SubType_Pattern of string

Whether some subtype of object type satisfies a pattern

| In_Module of string list

Whether the object pertains to a module

| Include_Blacklist

Bypass the Search blacklist

type search_flags = (search_constraint * bool) list

A list of search constraints; the boolean flag is set to false whenever the flag should be negated.

type 'a coq_object = {
coq_object_prefix : string list;
coq_object_qualid : string list;
coq_object_object : 'a;
}

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 coq_info = {
coqtop_version : string;
protocol_version : string;
release_date : string;
compile_date : string;
}
type db_continue_opt =
| StepIn
| StepOver
| StepOut
| Continue
| Interrupt
type location = (int * int) option
type state_id = Stateid.t
type route_id = Feedback.route_id
type edit_id = int
type 'a value =
| Good of 'a
| Fail of state_id * location * Pp.t
type ('a, 'b) union = ('a, 'b) Util.union
type add_sty = (((string * edit_id) * (state_id * verbose)) * int) * (int * int)

add ((((s,eid),(sid,v)), bp), (line_nb, bol_pos) adds the phrase s with edit id eid on top of the current edit position (that is asserted to be sid). v set to true indicates "verbose". The response (id,rc) 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. bp, line_nb and bol_pos are the Loc.t values for the phrase in the buffer, needed to return the correct location for s to the debugger

type add_rty = state_id * (unit, state_id) union
type edit_at_sty = state_id

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_rty = (unit, state_id * (state_id * state_id)) union
type query_sty = route_id * (string * state_id)

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_rty = unit
type goals_sty = unit

Fetching the list of current goals. Return None if no proof is in progress, Some gl otherwise.

type goals_rty = goals option
type evars_sty = unit

Retrieve the list of uninstantiated evars in the current proof. None if no proof is in progress.

type evars_rty = evar list option
type hints_sty = unit

Retrieving the tactics applicable to the current goal. None if there is no proof in progress.

type hints_rty = (hint list * hint) option
type status_sty = bool

The status, for instance "Ready in SomeSection, proving Foo", the input boolean (if true) forces the evaluation of all unevaluated statements

type status_rty = status
type search_sty = search_flags

Search for objects satisfying the given search flags.

type search_rty = string coq_object list
type proof_diff_sty = string * Stateid.t

Diffs between the proof term at a given stateid and the previous one

type proof_diff_rty = Pp.t
type db_cmd_sty = string

A debugger command

type db_cmd_rty = unit
type db_upd_bpts_sty = ((string * int) * bool) list

update one or more breakpoints in the specified file

type db_upd_bpts_rty = unit
type db_continue_sty = db_continue_opt

continue execution (in various ways)

type db_continue_rty = unit
type db_stack_sty = unit

fetch the stack

type db_stack_rty = (string * (string * int list) option) list
type db_vars_sty = int

fetch variable names and values for a stack frame

type db_vars_rty = (string * Pp.t) list
type db_configd_sty = unit

indicate debugger config is complete

type db_configd_rty = unit
type get_options_sty = unit

Retrieve the list of options of the current toplevel

type get_options_rty = (option_name * option_state) list
type set_options_sty = (option_name * option_value) list

Set the options to the given values. 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_rty = unit
type mkcases_sty = string

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_rty = string list list
type quit_sty = unit

Quit gracefully the interpreter.

type quit_rty = unit
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
type interp_sty = (raw * verbose) * string
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;
proof_diff : proof_diff_sty -> proof_diff_rty;
db_cmd : db_cmd_sty -> db_cmd_rty;
db_upd_bpts : db_upd_bpts_sty -> db_upd_bpts_rty;
db_continue : db_continue_sty -> db_continue_rty;
db_stack : db_stack_sty -> db_stack_rty;
db_vars : db_vars_sty -> db_vars_rty;
db_configd : db_configd_sty -> db_configd_rty;
handle_exn : handle_exn_sty -> handle_exn_rty;
init : init_sty -> init_rty;
quit : quit_sty -> quit_rty;
wait : wait_sty -> wait_rty;
interp : interp_sty -> interp_rty;
}