STM: proof block detection for bullets and { block }

5 files changed, 180 insertions, 3 deletions

diff --git a/engine/proofview.mli b/engine/proofview.mli
index 7996b7969..93ba55c61 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -303,6 +303,9 @@ val guard_no_unifiable : Names.Name.t list option tactic
     goals of p *)
 val unshelve : Goal.goal list -> proofview -> proofview
 
+(** [depends_on g1 g2 sigma] checks if g1 occurs in the type/ctx of g2 *)
+val depends_on : Evd.evar_map -> Goal.goal -> Goal.goal -> bool
+
 (** [with_shelf tac] executes [tac] and returns its result together with the set
     of goals shelved by [tac]. The current shelf is unchanged. *)
 val with_shelf : 'a tactic -> (Goal.goal list * 'a) tactic
diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
new file mode 100644
index 000000000..1e37209ed
--- /dev/null
+++ b/stm/proofBlockDelimiter.ml
@@ -0,0 +1,127 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Stm
+
+module Util : sig
+
+val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
+val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+
+type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
+
+val crawl :
+  document_view -> ?init:document_node option ->
+  ('a -> document_node -> 'a until) -> 'a ->
+    static_block_declaration option
+
+val unit_val : Stm.DynBlockData.t
+val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
+
+end = struct
+
+let unit_tag = DynBlockData.create "unit"
+let unit_val = DynBlockData.Easy.inj () unit_tag
+
+let of_bullet_val, to_bullet_val = DynBlockData.Easy.make_dyn "bullet"
+
+let simple_goal sigma g gs =
+  let open Evar in
+  let open Evd in
+  let open Evarutil in
+  let evi = Evd.find sigma g in
+  Set.is_empty (evars_of_term evi.evar_concl) &&
+  Set.is_empty (evars_of_filtered_evar_info (nf_evar_info sigma evi)) &&
+  not (List.exists (Proofview.depends_on sigma g) gs)
+
+let is_focused_goal_simple id =
+  match state_of_id id with
+  | `Expired | `Error _ | `Valid None -> `Not
+  | `Valid (Some { proof }) ->
+       let proof = Proof_global.proof_of_state proof in
+       let focused, r1, r2, r3, sigma = Proof.proof proof in
+       let rest = List.(flatten (map (fun (x,y) -> x @ y) r1)) @ r2 @ r3 in
+       if List.for_all (fun x -> simple_goal sigma x rest) focused
+       then `Simple focused
+       else `Not
+
+type 'a until = [ `Stop | `Found of static_block_declaration | `Cont of 'a ]
+
+let crawl { entry_point; prev_node } ?(init=Some entry_point) f acc =
+  let rec crawl node acc =
+    match node with
+    | None -> None
+    | Some node ->
+        match f acc node with
+        | `Stop -> None
+        | `Found x -> Some x
+        | `Cont acc -> crawl (prev_node node) acc in
+  crawl init acc
+
+end
+
+include Util
+
+(* ****************** - foo - bar - baz *********************************** *)
+
+let static_bullet ({ entry_point; prev_node } as view) =
+  match entry_point.ast with
+  | Vernacexpr.VernacBullet b ->
+      let base = entry_point.indentation in
+      let last_tac = prev_node entry_point in
+      crawl view ~init:last_tac (fun prev node ->
+        if node.indentation < base then `Stop else
+        if node.indentation > base then `Cont node else
+        match node.ast with
+        | Vernacexpr.VernacBullet b' when b = b' ->
+          `Found { stop = entry_point.id; start = prev.id;
+                   dynamic_switch = node.id; carry_on_data = of_bullet_val b }
+        | _ -> `Stop) entry_point
+  | _ -> assert false
+
+let dynamic_bullet { dynamic_switch = id; carry_on_data = b } =
+  match is_focused_goal_simple id with
+  | `Simple focused ->
+      `ValidBlock {
+         base_state = id;
+         goals_to_admit = focused;
+         recovery_command = Some (Vernacexpr.VernacBullet (to_bullet_val b))
+      }
+  | `Not -> `Leaks
+
+let () = register_proof_block_delimiter
+  "bullet" static_bullet dynamic_bullet
+
+(* ******************** { block } ***************************************** *)
+  
+let static_curly_brace ({ entry_point; prev_node } as view) =
+  assert(entry_point.ast = Vernacexpr.VernacEndSubproof);
+  crawl view (fun (nesting,prev) node ->
+    match node.ast with
+    | Vernacexpr.VernacSubproof _ when nesting = 0 ->
+      `Found { stop = entry_point.id; start = prev.id;
+               dynamic_switch = node.id; carry_on_data = unit_val }
+    | Vernacexpr.VernacSubproof _ ->
+      `Cont (nesting - 1,node)
+    | Vernacexpr.VernacEndSubproof ->
+      `Cont (nesting + 1,node)
+    | _ -> `Cont (nesting,node)) (-1, entry_point)
+
+let dynamic_curly_brace { dynamic_switch = id } =
+  match is_focused_goal_simple id with
+  | `Simple focused ->
+      `ValidBlock {
+         base_state = id;
+         goals_to_admit = focused;
+         recovery_command = Some Vernacexpr.VernacEndSubproof
+      }
+  | `Not -> `Leaks
+
+let () = register_proof_block_delimiter
+  "proof-block" static_curly_brace dynamic_curly_brace
diff --git a/stm/proofBlockDelimiter.mli b/stm/proofBlockDelimiter.mli
new file mode 100644
index 000000000..8455c1848
--- /dev/null
+++ b/stm/proofBlockDelimiter.mli
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This file implements proof block detection for:
+   - blocks delimited by { and }
+   - bullets with indentation
+
+   It exports utility functions to ease the development of other proof block
+   detection code.
+*)
+
+(** A goal is simple if it nor depends on nor impacts on any other goal.
+    This function is used to detect, dynamically, if a proof block leaks,
+    i.e. if skipping it could impact other goals (like not instantiating their
+    type).  `Simple carries the list of focused goals.
+*)
+val simple_goal : Evd.evar_map -> Goal.goal -> Goal.goal list -> bool
+val is_focused_goal_simple : Stateid.t -> [ `Simple of Goal.goal list | `Not ]
+
+type 'a until = [ `Stop | `Found of Stm.static_block_declaration | `Cont of 'a ]
+
+(* Simpler function to crawl the document backward to detect the block.
+ * ?init is the entry point of the document view if not given *)
+val crawl :
+  Stm.document_view -> ?init:Stm.document_node option ->
+  ('a -> Stm.document_node -> 'a until) -> 'a ->
+    Stm.static_block_declaration option
+
+(* Dummy value for static_block_declaration when no real value is needed *)
+val unit_val : Stm.DynBlockData.t
+
+(* Bullets *)
+val of_bullet_val : Vernacexpr.bullet -> Stm.DynBlockData.t
+val to_bullet_val : Stm.DynBlockData.t -> Vernacexpr.bullet
diff --git a/stm/stm.mllib b/stm/stm.mllib
index bd792b01f..939ee187a 100644
--- a/stm/stm.mllib
+++ b/stm/stm.mllib
@@ -8,4 +8,5 @@ Lemmas
 CoqworkmgrApi
 AsyncTaskQueue
 Stm
+ProofBlockDelimiter
 Vio_checking
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index aa9907045..11e973bf5 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -108,12 +108,19 @@ let rec classify_vernac e =
         VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
     (* ProofStep *)
     | VernacProof _ 
-    | VernacBullet _ 
     | VernacFocus _ | VernacUnfocus
-    | VernacSubproof _ | VernacEndSubproof
+    | VernacSubproof _
     | VernacCheckGuard
     | VernacUnfocused
-    | VernacSolveExistential _ -> VtProofStep { parallel = false; proof_block_detection = None }, VtLater
+    | VernacSolveExistential _ ->
+        VtProofStep { parallel = false; proof_block_detection = None }, VtLater
+    | VernacBullet _ ->
+        VtProofStep { parallel = false; proof_block_detection = Some "bullet" },
+        VtLater
+    | VernacEndSubproof -> 
+        VtProofStep { parallel = false;
+                      proof_block_detection = Some "proof-block" },
+        VtLater
     (* Options changing parser *)
     | VernacUnsetOption (["Default";"Proof";"Using"])
     | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow