From 8baf120d5cf5045d188f7d926162643a6e7ebcd0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Mon, 23 May 2016 13:46:43 +0200
Subject: STM: proof block detection for par:

"par: tac" is a terminator, if it fails we can admit all focused goals
and continue.
---
 stm/proofBlockDelimiter.ml | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'stm/proofBlockDelimiter.ml')

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 1e37209ed..8c50ad969 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -125,3 +125,25 @@ let dynamic_curly_brace { dynamic_switch = id } =
 
 let () = register_proof_block_delimiter
   "proof-block" static_curly_brace dynamic_curly_brace
+
+(* ***************** par: ************************************************* *)
+
+let static_par { entry_point; prev_node } =
+  match prev_node entry_point with
+  | None -> None
+  | Some { id = pid } ->
+      Some { stop = entry_point.id; start = pid;
+             dynamic_switch = pid; carry_on_data = unit_val }
+
+let dynamic_par { dynamic_switch = id } =
+  match is_focused_goal_simple id with
+  | `Simple focused ->
+      `ValidBlock {
+         base_state = id;
+         goals_to_admit = focused;
+         recovery_command = None;
+      }
+  | `Not -> `Leaks
+
+let () = register_proof_block_delimiter "par" static_par dynamic_par
+
-- 
cgit v1.2.3