STM: proof block detection/error resilience API

This commit introduces the concept of proof blocks that are
resilient to errors.  They are represented as ErrorBound boxes
in the STM document with the topological invariant that they never
overlap.

The detection and error recovery of ErrorBound boxes is defined outside
the STM.  One can define a box by providing a function to detect it
statically by crawling the parsed document and a function to recover
from an error at run time.

1 files changed, 81 insertions, 2 deletions

diff --git a/stm/stm.mli b/stm/stm.mli
index d825ff33e..20dd40bcd 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -20,7 +20,9 @@ open Loc
    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) ->
+val add :
+  ontop:Stateid.t -> ?newtip:Stateid.t ->
+  ?check:(vernac_expr located -> unit) ->
   bool -> edit_id -> string ->
     Stateid.t * [ `NewTip | `Unfocus of Stateid.t ]
 
@@ -96,6 +98,82 @@ module ProofTask : AsyncTaskQueue.Task
 module TacTask   : AsyncTaskQueue.Task
 module QueryTask : AsyncTaskQueue.Task
 
+(** document structure customization *************************************** **)
+
+(* A proof block delimiter defines a syntactic delimiter for sub proofs
+   that, when contain an error, do not impact the rest of the proof.
+   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. } ..
+
+   Corresponding DAG:
+
+      .. (3) <-- { -- (4) <-- tac1 -- (5) <-- tac2 -- (6) <-- } -- (7) ..
+                       
+   Declaration of block  [-------------------------------------------]
+
+      start = 5            the first state_id that could fail in the block
+      stop = 6             the node that may absorb the error
+      dynamic_switch = 4   dynamic check on this node
+      carry_on_data = ()   no need to carry extra data from static to dynamic
+                           checks
+*)
+
+module DynBlockData : Dyn.S
+
+type static_block_declaration = {
+  start : Stateid.t;
+  stop : Stateid.t;
+  dynamic_switch : Stateid.t;
+  carry_on_data : DynBlockData.t;
+}
+
+type document_node = {
+  indentation : int;
+  ast : Vernacexpr.vernac_expr;
+  id : Stateid.t;
+}
+
+type document_view = {
+  entry_point : document_node;
+  prev_node : document_node -> document_node option;
+}
+
+type static_block_detection =
+  document_view -> static_block_declaration option
+
+type recovery_action = {
+  base_state : Stateid.t;
+  goals_to_admit : Goal.goal list;
+  recovery_command : Vernacexpr.vernac_expr option;
+}
+
+type dynamic_block_error_recovery =
+  static_block_declaration -> [ `ValidBlock of recovery_action | `Leaks ]
+
+val register_proof_block_delimiter :
+  Vernacexpr.proof_block_name ->
+  static_block_detection ->
+  dynamic_block_error_recovery ->
+    unit
+
 (** customization ********************************************************** **)
 
 (* From the master (or worker, but beware that to install the hook
@@ -122,7 +200,8 @@ type state = {
   proof : Proof_global.state;
   shallow : bool
 }
-val state_of_id : Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
+val state_of_id :
+  Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
 
 (** read-eval-print loop compatible interface ****************************** **)