From 42cbdfccf0c0500935d619dccaa00476690229f8 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Fri, 17 Jun 2016 16:24:37 +0200
Subject: par: like all: but in parallel

This commit documents par:, fixes its semantics so that is
behaves like all:, supports (toplevel) abstract and optimizes
toplevel solve.

`par: solve [tac]` is equivalent to `Ltac tac1 := solve[tac]...par: tac1`
but is optimized for failures: if one goal fails all are aborted
immediately.

`par: abstract tac` runs abstract on the generated proof terms.  Nested
abstract calls are not supported.
---
 stm/vernac_classifier.ml | 17 +++++++++++------
 1 file changed, 11 insertions(+), 6 deletions(-)

(limited to 'stm/vernac_classifier.ml')

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index a602d6b8a..f6d8c327e 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -14,6 +14,11 @@ let default_proof_mode () = Proof_global.get_default_proof_mode_name ()
 
 let string_of_in_script b = if b then " (inside script)" else ""
 
+let string_of_parallel = function
+  | `Yes (solve,abs) ->
+       "par" ^ if solve then "solve" else "" ^ if abs then "abs" else ""
+  | `No -> ""
+
 let string_of_vernac_type = function
   | VtUnknown -> "Unknown"
   | VtStartProof _ -> "StartProof"
@@ -22,7 +27,7 @@ let string_of_vernac_type = function
   | VtQed VtKeepAsAxiom -> "Qed(admitted)"
   | VtQed VtDrop -> "Qed(drop)"
   | VtProofStep { parallel; proof_block_detection } ->
-      "ProofStep " ^ if parallel then "par " else "" ^ 
+      "ProofStep " ^ string_of_parallel parallel ^
         Option.default "" proof_block_detection
   | VtProofMode s -> "ProofMode " ^ s
   | VtQuery (b,(id,route)) ->
@@ -95,7 +100,7 @@ let rec classify_vernac e =
         | ( VtQuery _ | VtProofStep _ | VtSideff _
           | VtStm _ | VtProofMode _ ), _ as x -> x
         | VtQed _, _ ->
-            VtProofStep { parallel = false; proof_block_detection = None },
+            VtProofStep { parallel = `No; proof_block_detection = None },
             VtNow
         | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow)
     (* Qed *)
@@ -113,12 +118,12 @@ let rec classify_vernac e =
     | VernacCheckGuard
     | VernacUnfocused
     | VernacSolveExistential _ ->
-        VtProofStep { parallel = false; proof_block_detection = None }, VtLater
+        VtProofStep { parallel = `No; proof_block_detection = None }, VtLater
     | VernacBullet _ ->
-        VtProofStep { parallel = false; proof_block_detection = Some "bullet" },
+        VtProofStep { parallel = `No; proof_block_detection = Some "bullet" },
         VtLater
     | VernacEndSubproof -> 
-        VtProofStep { parallel = false;
+        VtProofStep { parallel = `No;
                       proof_block_detection = Some "curly" },
         VtLater
     (* Options changing parser *)
@@ -229,4 +234,4 @@ let rec classify_vernac e =
 let classify_as_query =
   VtQuery (true,(Stateid.dummy,Feedback.default_route)), VtLater
 let classify_as_sideeff = VtSideff [], VtLater
-let classify_as_proofstep = VtProofStep { parallel = false; proof_block_detection = None}, VtLater
+let classify_as_proofstep = VtProofStep { parallel = `No; proof_block_detection = None}, VtLater
-- 
cgit v1.2.3