Parse activate blocks.

1 files changed, 16 insertions, 3 deletions

diff --git a/frontend/parser.mly b/frontend/parser.mly
index fb00478..ec283c3 100644
--- a/frontend/parser.mly
+++ b/frontend/parser.mly
@@ -13,7 +13,8 @@ open Util
 %token VAR LET TEL
 %token PRE
 %token ASSUME GUARANTEE
-%token AUTOMATON STATE INITIAL UNTIL UNLESS RESUME
+%token ACTIVATE
+%token AUTOMATON STATE INITIAL UNTIL UNLESS RESUME RESTART
 
 %token LPAREN RPAREN
 %token LCURLY RCURLY
@@ -128,8 +129,19 @@ trans(TT):
 |                                                         { [] }
 
 transition:
-| IF e=ext(expr) RESUME s=ext(IDENT)                      { (e, s) }
-
+| IF e=ext(expr) RESUME s=ext(IDENT)                      { (e, s, false) }
+| IF e=ext(expr) RESTART s=ext(IDENT)                     { (e, s, true) }
+
+activate:
+| ACTIVATE a=activate_if RETURNS r=separated_list(COMMA, IDENT)  { (a, r) }
+activate_if:
+| IF c=ext(expr) THEN t=activate_if ELSE e=activate_if           { AST_activate_if(c, t, e) }
+| lv=option(var_decl) b=body
+{ AST_activate_body {
+      id = "activate"^uid();
+      locals = (match lv with Some v -> v | None -> []);
+      body = b;
+} }
 
 eqn:
 | i=separated_list(COMMA, ext(IDENT)) EQUAL e=ext(expr)         
@@ -137,6 +149,7 @@ eqn:
 | ASSUME i=ext(IDENT) COLON e=ext(expr)         { AST_assume(i, e) }
 | GUARANTEE i=ext(IDENT) COLON e=ext(expr)      { AST_guarantee(i, e) }
 | a=automaton                                   { AST_automaton(a) }
+| a=activate                                    { AST_activate(a) }
 
 typ:
 | INT                                           { AST_TINT }