Parse activate blocks.

4 files changed, 71 insertions, 26 deletions

diff --git a/frontend/ast.ml b/frontend/ast.ml
index 50fa3f4..cf04166 100644
--- a/frontend/ast.ml
+++ b/frontend/ast.ml
@@ -71,13 +71,24 @@ and  state = {
     body    : eqn ext list;
     until   : transition list;
 }
-and transition = (expr ext) * (id ext)
+and transition = (expr ext) * (id ext) * bool   (* bool : does it reset ? *)
+
+and activate_block = {
+  id        : id;
+  locals    : var_def list;
+  body      : eqn ext list;
+}
+and activate_if =
+  | AST_activate_body of activate_block
+  | AST_activate_if of expr ext * activate_if * activate_if
+and activate = activate_if * id list
 
 and eqn =
     | AST_assign     of (id ext list) * (expr ext)
     | AST_guarantee  of (id ext) * (expr ext)
     | AST_assume     of (id ext) * (expr ext)
     | AST_automaton  of automaton
+    | AST_activate   of activate
 
 type node_decl = {
     name : id;
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index 857e01d..25b1c11 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -157,11 +157,29 @@ let rec print_expr fmt e =
         Format.fprintf fmt "%a(%a)"
           print_id i (print_list print_expr ", ") (List.map fst l)
 
+
 (* equations *)
 
 let indent ind = ind^"  "
 
-let rec print_eqn ind fmt = function
+let rec print_vars ind fmt = function
+  | [] -> ()
+  | v ->
+    Format.fprintf fmt "%svar" ind;
+    List.iter (fun d -> Format.fprintf fmt " %a;" print_var_decl d) v;
+    Format.fprintf fmt "@\n";
+
+and print_var_decl fmt (pr, (i, _), ty) =
+    Format.fprintf fmt "%s%s: %s"
+      (if pr then "probe " else "")
+      i
+      (string_of_typ ty)
+
+and print_body ind fmt body =
+  Format.fprintf fmt "%slet@\n%a%stel@\n"
+    ind (print_block ind) body ind
+
+and print_eqn ind fmt = function
   | AST_assign (l,(e,_)) ->
       Format.fprintf fmt "%s%a = %a;@\n" 
         ind (print_list print_id_ext ", ") l print_expr e
@@ -172,6 +190,22 @@ let rec print_eqn ind fmt = function
       Format.fprintf fmt "%sguarantee %s: %a;@\n"
           ind i print_expr e
   | AST_automaton a -> print_automaton ind fmt a
+  | AST_activate a -> print_activate ind fmt a
+
+and print_activate ind fmt (x, r) =
+  Format.fprintf fmt "%sactivate@\n" ind;
+  print_activate_if (indent ind) fmt x;
+  Format.fprintf fmt "%sreturns %a;@\n" ind (print_list print_id ", ") r
+
+and print_activate_if ind fmt = function
+  | AST_activate_if((c, _), t, e) ->
+    Format.fprintf fmt "%sif %a then@\n" ind print_expr c;
+    print_activate_if (indent ind) fmt t;
+    Format.fprintf fmt "%selse@\n" ind;
+    print_activate_if (indent ind) fmt e
+  | AST_activate_body(b) ->
+    print_vars ind fmt b.locals;
+    print_body ind fmt b.body
 
 and print_automaton ind fmt (n, sts, r) =
   Format.fprintf fmt "%sautomaton %s@\n" ind n;
@@ -181,17 +215,12 @@ and print_automaton ind fmt (n, sts, r) =
 and print_state ind fmt (st, _) =
   Format.fprintf fmt "%s%sstate %s@\n"
     ind (if st.initial then "initial " else "") st.name;
-  if st.locals <> [] then begin
-    Format.fprintf fmt "%svar" ind;
-    List.iter (fun d -> Format.fprintf fmt " %a;" print_var_decl d) st.locals;
-    Format.fprintf fmt "@\n";
-  end;
-  Format.fprintf fmt "%slet@\n%a%stel@\n"
-    ind (print_block ind) st.body ind;
+  print_vars ind fmt st.locals;
+  print_body ind fmt st.body;
   if st.until <> [] then begin
     Format.fprintf fmt "%suntil@\n" ind;
-    List.iter (fun ((e, _),(s, _)) -> 
-        Format.fprintf fmt "%sif %a resume %s;@\n" (indent ind) print_expr e s)
+    List.iter (fun ((e, _),(s, _), reset) -> 
+        Format.fprintf fmt "%sif %a %s %s;@\n" (indent ind) print_expr e (if reset then "restart" else "resume") s)
       st.until
   end
 
@@ -200,24 +229,14 @@ and print_block ind fmt b =
 
 (* declarations *)
 
-and print_var_decl fmt (pr, (i, _), ty) =
-    Format.fprintf fmt "%s%s: %s"
-      (if pr then "probe " else "")
-      i
-      (string_of_typ ty)
 
 and print_node_decl fmt (d : node_decl) =
     Format.fprintf fmt "node %s(%a) returns(%a)@\n"
       d.name
       (print_list print_var_decl "; ") d.args
       (print_list print_var_decl "; ") d.ret;
-    if d.var <> [] then begin
-      Format.fprintf fmt "var";
-      List.iter (fun d -> Format.fprintf fmt " %a;" print_var_decl d) d.var;
-      Format.fprintf fmt "@\n"
-    end;
-    Format.fprintf fmt "let@\n%atel@\n@\n"
-      (print_block "") d.body
+    print_vars "" fmt d.var;
+    print_body "" fmt d.body
 
 let print_const_decl fmt (d : const_decl) =
     Format.fprintf fmt
diff --git a/frontend/lexer.mll b/frontend/lexer.mll
index 9dc7da3..8a4ef26 100644
--- a/frontend/lexer.mll
+++ b/frontend/lexer.mll
@@ -26,12 +26,14 @@
       "or",         OR;
       "mod",        MOD;
 
+      "activate",   ACTIVATE;
       "automaton",  AUTOMATON;
       "state",      STATE;
       "initial",    INITIAL;
       "unless",     UNLESS;
       "until",      UNTIL;
       "resume",     RESUME;
+      "restart",    RESTART;
 
       "true",       TRUE;
       "false",      FALSE;
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 }