From 5e86a655278f8f8be38363cc3bfc2f88ec2c3e40 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 23 May 2016 11:11:30 +0200 Subject: 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. --- stm/vernac_classifier.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) (limited to 'stm/vernac_classifier.ml') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index b1df3c9ca..aa9907045 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -21,8 +21,9 @@ let string_of_vernac_type = function | VtQed VtKeep -> "Qed(keep)" | VtQed VtKeepAsAxiom -> "Qed(admitted)" | VtQed VtDrop -> "Qed(drop)" - | VtProofStep false -> "ProofStep" - | VtProofStep true -> "ProofStep (parallel)" + | VtProofStep { parallel; proof_block_detection } -> + "ProofStep " ^ if parallel then "par " else "" ^ + Option.default "" proof_block_detection | VtProofMode s -> "ProofMode " ^ s | VtQuery (b,(id,route)) -> "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ @@ -93,7 +94,9 @@ let rec classify_vernac e = (match classify_vernac e with | ( VtQuery _ | VtProofStep _ | VtSideff _ | VtStm _ | VtProofMode _ ), _ as x -> x - | VtQed _, _ -> VtProofStep false, VtNow + | VtQed _, _ -> + VtProofStep { parallel = false; proof_block_detection = None }, + VtNow | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) (* Qed *) | VernacAbort _ -> VtQed VtDrop, VtLater @@ -110,7 +113,7 @@ let rec classify_vernac e = | VernacSubproof _ | VernacEndSubproof | VernacCheckGuard | VernacUnfocused - | VernacSolveExistential _ -> VtProofStep false, VtLater + | VernacSolveExistential _ -> VtProofStep { parallel = false; proof_block_detection = None }, VtLater (* Options changing parser *) | VernacUnsetOption (["Default";"Proof";"Using"]) | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow @@ -219,4 +222,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 false, VtLater +let classify_as_proofstep = VtProofStep { parallel = false; proof_block_detection = None}, VtLater -- cgit v1.2.3