diff options
Diffstat (limited to 'stm/stm.mli')
| -rw-r--r-- | stm/stm.mli | 223 |
1 files changed, 144 insertions, 79 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index b8a2a385..35ce77a3 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -1,36 +1,120 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* * 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 *) +(* // * 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) *) (************************************************************************) -open Vernacexpr open Names -open Feedback -open Loc (** state-transaction-machine interface *) -(* [add ontop check vebose eid s] adds a new command [s] on the state [ontop] - having edit id [eid]. [check] is called on the AST. - The [ontop] parameter is just for asserting the GUI is on sync, but - will eventually call edit_at on the fly if needed. - The sentence [s] is parsed in the state [ontop]. - If [newtip] is provided, then the returned state id is guaranteed to be - [newtip] *) -val add : - ontop:Stateid.t -> ?newtip:Stateid.t -> - ?check:(vernac_expr located -> unit) -> - bool -> edit_id -> string -> - Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] - -(* parses and executes a command at a given state, throws away its side effects - but for the printings. Feedback is sent with report_with (defaults to dummy - state id) *) -val query : - at:Stateid.t -> ?report_with:(Stateid.t * Feedback.route_id) -> string -> unit +(* Flags *) +module AsyncOpts : sig + + type cache = Force + type async_proofs = APoff | APonLazy | APon + type tac_error_filter = [ `None | `Only of string list | `All ] + + type stm_opt = { + async_proofs_n_workers : int; + async_proofs_n_tacworkers : int; + + async_proofs_cache : cache option; + async_proofs_mode : async_proofs; + + async_proofs_private_flags : string option; + async_proofs_full : bool; + async_proofs_never_reopen_branch : bool; + + async_proofs_tac_error_resilience : tac_error_filter; + async_proofs_cmd_error_resilience : bool; + async_proofs_delegation_threshold : float; + } + + val default_opts : stm_opt + +end + +(** The STM document type [stm_doc_type] determines some properties + such as what uncompleted proofs are allowed and what gets recorded + to aux files. *) +type stm_doc_type = + | VoDoc of string (* file path *) + | VioDoc of string (* file path *) + | Interactive of DirPath.t (* module path *) + +(** Coq initalization options: + + - [doc_type]: Type of document being created. + + - [require_libs]: list of libraries/modules to be pre-loaded at + startup. A tuple [(modname,modfrom,import)] is equivalent to [From + modfrom Require modname]; [import] works similarly to + [Library.require_library_from_dirpath], [Some false] will import + the module, [Some true] will additionally export it. + +*) +type stm_init_options = { + (* The STM will set some internal flags differently depending on the + specified [doc_type]. This distinction should dissappear at some + some point. *) + doc_type : stm_doc_type; + + (* Initial load path in scope for the document. Usually extracted + from -R options / _CoqProject *) + iload_path : Mltop.coq_path list; + + (* Require [require_libs] before the initial state is + ready. Parameters follow [Library], that is to say, + [lib,prefix,import_export] means require library [lib] from + optional [prefix] and [import_export] if [Some false/Some true] + is used. *) + require_libs : (string * string option * bool option) list; + + (* STM options that apply to the current document. *) + stm_options : AsyncOpts.stm_opt; +} +(* fb_handler : Feedback.feedback -> unit; *) + +(** The type of a STM document *) +type doc + +(** [init_core] performs some low-level initalization; should go away + in future releases. *) +val init_core : unit -> unit + +(** [new_doc opt] Creates a new document with options [opt] *) +val new_doc : stm_init_options -> doc * Stateid.t + +(** [parse_sentence sid pa] Reads a sentence from [pa] with parsing + state [sid] Returns [End_of_input] if the stream ends *) +val parse_sentence : doc:doc -> Stateid.t -> Pcoq.Gram.coq_parsable -> + Vernacexpr.vernac_control CAst.t + +(* Reminder: A parsable [pa] is constructed using + [Pcoq.Gram.coq_parsable stream], where [stream : char Stream.t]. *) + +exception End_of_input + +(* [add ~ontop ?newtip verbose cmd] adds a new command [cmd] ontop of + the state [ontop]. + The [ontop] parameter just asserts that the GUI is on + sync, but it will eventually call edit_at on the fly if needed. + If [newtip] is provided, then the returned state id is guaranteed + to be [newtip] *) +val add : doc:doc -> ontop:Stateid.t -> ?newtip:Stateid.t -> + bool -> Vernacexpr.vernac_control CAst.t -> + doc * Stateid.t * [ `NewTip | `Unfocus of Stateid.t ] + +(* [query at ?report_with cmd] Executes [cmd] at a given state [at], + throwing away side effects except messages. Feedback will + be sent with [report_with], which defaults to the dummy state id *) +val query : doc:doc -> + at:Stateid.t -> route:Feedback.route_id -> Pcoq.Gram.coq_parsable -> unit (* [edit_at id] is issued to change the editing zone. [`NewTip] is returned if the requested id is the new document tip hence the document portion following @@ -42,24 +126,28 @@ val query : If Flags.async_proofs_full is set, then [id] is not [observe]d, else it is. *) type focus = { start : Stateid.t; stop : Stateid.t; tip : Stateid.t } -val edit_at : Stateid.t -> [ `NewTip | `Focus of focus ] +val edit_at : doc:doc -> Stateid.t -> doc * [ `NewTip | `Focus of focus ] + +(* [observe doc sid]] Check / execute span [sid] *) +val observe : doc:doc -> Stateid.t -> doc -(* Evaluates the tip of the current branch *) -val finish : unit -> unit +(* [finish doc] Fully checks a document up to the "current" tip. *) +val finish : doc:doc -> doc -val observe : Stateid.t -> unit +(* Internal use (fake_ide) only, do not use *) +val wait : doc:doc -> doc val stop_worker : string -> unit (* Joins the entire document. Implies finish, but also checks proofs *) -val join : unit -> unit +val join : doc:doc -> doc (* Saves on the disk a .vio corresponding to the current status: - if the worker pool is empty, all tasks are saved - if the worker proof is not empty, then it waits until all workers are done with their current jobs and then dumps (or fails if one of the completed tasks is a failure) *) -val snapshot_vio : DirPath.t -> string -> unit +val snapshot_vio : doc:doc -> DirPath.t -> string -> doc (* Empties the task queue, can be used only if the worker pool is empty (E.g. * after having built a .vio in batch mode *) @@ -74,23 +162,17 @@ val finish_tasks : string -> tasks -> Library.seg_univ * Library.seg_proofs (* Id of the tip of the current branch *) -val get_current_state : unit -> Stateid.t - -(* Misc *) -val init : unit -> unit +val get_current_state : doc:doc -> Stateid.t +val get_ldir : doc:doc -> Names.DirPath.t (* This returns the node at that position *) -val get_ast : Stateid.t -> (Vernacexpr.vernac_expr * Loc.t) option +val get_ast : doc:doc -> Stateid.t -> (Vernacexpr.vernac_control Loc.located) option (* Filename *) val set_compilation_hints : string -> unit (* Reorders the task queue putting forward what is in the perspective *) -val set_perspective : Stateid.t list -> unit - -type document -val backup : unit -> document -val restore : document -> unit +val set_perspective : doc:doc -> Stateid.t list -> unit (** workers **************************************************************** **) @@ -105,20 +187,20 @@ module QueryTask : AsyncTaskQueue.Task While checking a proof, if an error occurs in a (valid) block then processing can skip the entire block and go on to give feedback on the rest of the proof. - + static_block_detection and dynamic_block_validation are run when the closing block marker is parsed/executed respectively. - + static_block_detection is for example called when "}" is parsed and declares a block containing all proof steps between it and the matching "{". - + dynamic_block_validation is called when an error "crosses" the "}" statement. Depending on the nature of the goal focused by "{" the block may absorb the error or not. For example if the focused goal occurs in the type of another goal, then the block is leaky. Note that one can design proof commands that need no dynamic validation. - + Example of document: .. { tac1. tac2. } .. @@ -126,7 +208,7 @@ module QueryTask : AsyncTaskQueue.Task Corresponding DAG: .. (3) <-- { -- (4) <-- tac1 -- (5) <-- tac2 -- (6) <-- } -- (7) .. - + Declaration of block [-------------------------------------------] start = 5 the first state_id that could fail in the block @@ -147,7 +229,7 @@ type static_block_declaration = { type document_node = { indentation : int; - ast : Vernacexpr.vernac_expr; + ast : Vernacexpr.vernac_control; id : Stateid.t; } @@ -162,11 +244,11 @@ type static_block_detection = type recovery_action = { base_state : Stateid.t; goals_to_admit : Goal.goal list; - recovery_command : Vernacexpr.vernac_expr option; + recovery_command : Vernacexpr.vernac_control option; } type dynamic_block_error_recovery = - static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ] + doc -> static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ] val register_proof_block_delimiter : Vernacexpr.proof_block_name -> @@ -182,43 +264,26 @@ val register_proof_block_delimiter : * the name of the Task(s) above) *) val state_computed_hook : (Stateid.t -> in_cache:bool -> unit) Hook.t -val parse_error_hook : - (Feedback.edit_or_state_id -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t -val execution_error_hook : (Stateid.t -> Loc.t -> Pp.std_ppcmds -> unit) Hook.t val unreachable_state_hook : (Stateid.t -> Exninfo.iexn -> unit) Hook.t + (* ready means that master has it at hand *) val state_ready_hook : (Stateid.t -> unit) Hook.t -(* called with true before and with false after a tactic explicitly - * in the document is run *) -val tactic_being_run_hook : (bool -> unit) Hook.t (* Messages from the workers to the master *) val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t -type state = { - system : States.state; - proof : Proof_global.state; - shallow : bool -} -val state_of_id : - Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] - -(** read-eval-print loop compatible interface ****************************** **) +val get_doc : Feedback.doc_id -> doc -(* Adds a new line to the document. It replaces the core of Vernac.interp. - [finish] is called as the last bit of this function if the system - is running interactively (-emacs or coqtop). *) -val interp : bool -> vernac_expr located -> unit +val state_of_id : doc:doc -> + Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ] (* Queries for backward compatibility *) -val current_proof_depth : unit -> int -val get_all_proof_names : unit -> Id.t list -val get_current_proof_name : unit -> Id.t option -val show_script : ?proof:Proof_global.closed_proof -> unit -> unit - -(* Hooks to be set by other Coq components in order to break file cycles *) -val process_error_hook : Future.fix_exn Hook.t -val interp_hook : (?verbosely:bool -> ?proof:Proof_global.closed_proof -> - Loc.t * Vernacexpr.vernac_expr -> unit) Hook.t -val with_fail_hook : (bool -> (unit -> unit) -> unit) Hook.t -val get_fix_exn : unit -> (Exninfo.iexn -> Exninfo.iexn) +val current_proof_depth : doc:doc -> int +val get_all_proof_names : doc:doc -> Id.t list + +(** Enable STM debugging *) +val stm_debug : bool ref + +type document +val backup : unit -> document +val restore : document -> unit |