From f7868083de2f351b5195149870e6e77398da44f9 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Fri, 13 Jun 2014 11:31:50 +0200 Subject: Parse activate blocks. --- frontend/parser.mly | 19 ++++++++++++++++--- 1 file changed, 16 insertions(+), 3 deletions(-) (limited to 'frontend/parser.mly') 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 } -- cgit v1.2.3