diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-17 16:24:37 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-06-17 16:27:35 +0200 |
| commit | 42cbdfccf0c0500935d619dccaa00476690229f8 (patch) | |
| tree | c72ac918e55c7a9ef6d3b74ba0e2c6f0cc3efe29 /stm/vernac_classifier.ml | |
| parent | 905e82c498d920ff5508d57c5af4a3a8e939f2a8 (diff) | |
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.
Diffstat (limited to 'stm/vernac_classifier.ml')
| -rw-r--r-- | stm/vernac_classifier.ml | 17 |
1 files changed, 11 insertions, 6 deletions
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 |