Parse activate blocks.

7 files changed, 203 insertions, 96 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 }
diff --git a/interpret/interpret.ml b/interpret/interpret.ml
index d141bc6..373ed5f 100644
--- a/interpret/interpret.ml
+++ b/interpret/interpret.ml
@@ -20,18 +20,63 @@ let find_node_decl p id =
   | AST_node_decl d -> d
   | _ -> assert false
 
+(* Utility : build subscopes of equation ; extract pre declarations *)
+
+(* subscopes :
+      prog -> expr ext -> (id * eqs * (id * expr ext) list) list
+*)
+let rec subscopes p e = match fst e with
+  | AST_identifier _ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
+  | AST_unary (_, e') | AST_pre (e', _) | AST_not e' -> subscopes p e'
+  | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
+  | AST_arrow(e1, e2) ->
+    subscopes p e1 @ subscopes p e2
+  | AST_if(e1, e2, e3) ->
+    subscopes p e1 @ subscopes p e2 @ subscopes p e3
+  | AST_instance((f, _), args, id) ->
+    let more = List.flatten (List.map (subscopes p) args) in
+    let (node, _) = find_node_decl p f in
+    let args_x = List.map2 (fun id arg -> id, arg) node.args args in
+    (id, node.body, args_x)::more
+
+(* extract_pre : expr ext -> (id * expr ext) list *)
+let rec extract_pre e = match fst e with
+  | AST_identifier _ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
+  | AST_unary (_, e') | AST_not e' -> extract_pre e'
+  | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
+  | AST_arrow(e1, e2) ->
+    extract_pre e1 @ extract_pre e2
+  | AST_if(e1, e2, e3) ->
+    extract_pre e1 @ extract_pre e2 @ extract_pre e3
+  | AST_instance((f, _), args, id) ->
+    List.flatten (List.map extract_pre args)
+  | AST_pre(e', n) ->
+    (n, e')::(extract_pre e')
+
+
 (* Expression evaluation *)
 
+type eval_env = {
+  p: prog;
+  c: calc_map;
+  scopes: string list;
+}
+
 (*
-  eval_expr : prog -> calc_map -> state -> string -> expr ext -> (state * value)
+  eval_expr : eval_env -> string -> expr ext -> (state * value)
 *)
-let rec eval_expr p c scope st exp =
-  let sub_eval = eval_expr p c scope in
+let rec eval_expr env st exp =
+  let sub_eval = eval_expr env in
+  let scope = List.hd env.scopes in
   match fst exp with
   | AST_identifier (id, _) ->
-    begin try let st, v = get_var st c (scope^"/"^id) in st, [v]
-    with No_variable _ -> let st, v = get_var st c ("cst/"^id) in st, [v]
-    end
+    let rec aux = function
+      | [] ->
+        let st, v = get_var st env.c ("cst/"^id) in st, [v]
+      | sc::q ->
+        try let st, v = get_var st env.c (sc^"/"^id) in st, [v]
+        with No_variable _ -> aux q
+    in aux env.scopes
   (* on numerical values *)
   | AST_int_const (i, _) -> st, [VInt (int_of_string i)]
   | AST_real_const (r, _) -> st, [VReal (float_of_string r)]
@@ -111,16 +156,18 @@ let rec eval_expr p c scope st exp =
     | _ -> type_error "Invalid condition in if."
     end
   | AST_instance((f, _), args, nid) ->
-    let (n, _) = find_node_decl p f in
+    let (n, _) = find_node_decl env.p f in
     List.fold_left
-      (fun (st, vs) (_, (id,_), _) -> let st, v = get_var st c (scope^"/"^nid^"/"^id) in
+      (fun (st, vs) (_, (id,_), _) ->
+          let st, v = get_var st env.c (scope^"/"^nid^"/"^id) in
           st, vs @ [v])
       (st, []) n.ret
 
 (* Constant calculation *)
 
 let rec calc_const p d st c =
-  match eval_expr p c "cst" st d.value with
+  let env = { p = p; c = c; scopes = ["cst"] } in
+  match eval_expr env st d.value with
   | st, [v] -> VarMap.add ("cst/"^d.name) v st
   | _ -> type_error ("Cannot assign tuple to constant" ^ d.name)
 
@@ -140,46 +187,41 @@ let program_consts p =
     VarMap.empty
     cdecl
 
-(* Program execution *)
-
-(* subscopes :
-      prog -> expr ext -> (id * eqs * (id * expr ext) list) list
-*)
-let rec subscopes p e = match fst e with
-  | AST_identifier _ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
-  | AST_unary (_, e') | AST_pre (e', _) | AST_not e' -> subscopes p e'
-  | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
-  | AST_arrow(e1, e2) ->
-    subscopes p e1 @ subscopes p e2
-  | AST_if(e1, e2, e3) ->
-    subscopes p e1 @ subscopes p e2 @ subscopes p e3
-  | AST_instance((f, _), args, id) ->
-    let more = List.flatten (List.map (subscopes p) args) in
-    let (node, _) = find_node_decl p f in
-    let args_x = List.map2 (fun id arg -> id, arg) node.args args in
-    (id, node.body, args_x)::more
+(* get initial state for program *)
+let program_init_state p root_node =
+  let (n, _) = find_node_decl p root_node in
+  let rec aux st p scope eqs =
+    let st = VarMap.add (scope^"/init") (VBool true) st in
+    let add_subscopes =
+      List.fold_left (fun st (ss_id, ss_eqs, _) -> aux st p (scope^"/"^ss_id) ss_eqs)
+    in
+    let add_eq st eq = match fst eq with
+        | AST_assign(_, e) -> add_subscopes st (subscopes p e)
+        | AST_assume _ | AST_guarantee _ -> st
+        | AST_automaton (aid, astates, ret) ->
+          let (initial, _) = List.find (fun (s, _) -> s.initial) astates in
+          let st = VarMap.add (scope^":"^aid^".state") (VState initial.name) st in
+          let add_astate st ((astate:Ast.state), _) =
+            aux st p (scope^":"^aid^"."^astate.name) astate.body
+          in
+          List.fold_left add_astate st astates
+        | AST_activate _ -> not_implemented "program_init_state activate"
+    in
+    List.fold_left add_eq st eqs
+  in
+    aux (program_consts p) p "" n.body
 
-(* extract_pre : expr ext -> (id * expr ext) list *)
-let rec extract_pre e = match fst e with
-  | AST_identifier _ | AST_int_const _ | AST_real_const _ | AST_bool_const _ -> []
-  | AST_unary (_, e') | AST_not e' -> extract_pre e'
-  | AST_binary(_, e1, e2) | AST_binary_rel (_, e1, e2) | AST_binary_bool (_, e1, e2)
-  | AST_arrow(e1, e2) ->
-    extract_pre e1 @ extract_pre e2
-  | AST_if(e1, e2, e3) ->
-    extract_pre e1 @ extract_pre e2 @ extract_pre e3
-  | AST_instance((f, _), args, id) ->
-    List.flatten (List.map extract_pre args)
-  | AST_pre(e', n) ->
-    (n, e')::(extract_pre e')
+(* Program execution *)
 
 
 (* build calc map *)
-let rec build_prog_ccmap p scope eqs st =
+let rec build_prog_ccmap p scopes eqs st =
+  let scope = List.hd scopes in
   let add_eq c eq = match fst eq with
     | AST_assign(vars, e) ->
       let calc st c =
-        let st, vals = eval_expr p c scope st e in
+        let env = { p = p; c = c; scopes = scopes } in
+        let st, vals = eval_expr env st e in
         List.fold_left2
           (fun st (id,_) v -> VarMap.add (scope^"/"^id) v st)
           st vars vals
@@ -187,15 +229,13 @@ let rec build_prog_ccmap p scope eqs st =
       let c = List.fold_left (fun c (id, _) -> VarMap.add (scope^"/"^id) (F calc) c) c vars in
 
       let add_subscope c (ss_id, ss_eqs, ss_args) =
-        let c = VarMap.merge (fun _ a b -> match a, b with
-          | Some x, None -> Some x
-          | None, Some y -> Some y
-          | _ -> assert false) c
-          (build_prog_ccmap p (scope^"/"^ss_id) ss_eqs st)
+        let c = VarMap.merge disjoint_union c
+          (build_prog_ccmap p [scope^"/"^ss_id] ss_eqs st)
         in
         let add_v c ((_, (id, _), _), eq) =
           let calc st c =
-            let st, vals = eval_expr p c scope st eq in
+            let env = { p = p; c = c; scopes = scopes } in
+            let st, vals = eval_expr env st eq in
             match vals with
             | [v] -> VarMap.add (scope^"/"^ss_id^"/"^id) v st
             | _ -> type_error "invalid arity"
@@ -207,15 +247,18 @@ let rec build_prog_ccmap p scope eqs st =
       List.fold_left add_subscope c (subscopes p e)
     | AST_assume _ | AST_guarantee _ -> c
     | AST_automaton _ -> not_implemented "build_prog_ccmap for automaton"
+    | AST_activate _ -> not_implemented "build_prog_ccmap for activate"
   in
   List.fold_left add_eq VarMap.empty eqs
 
-let extract_next_state active p scope eqs st ccmap =
+let extract_next_state active env eqs st =
   let csts = VarMap.filter
     (fun k _ -> String.length k > 4 && String.sub k 0 4 = "cst/")
     st
   in
-  let rec aux active scope eqs st nst =
+  let rec aux active scopes eqs st nst =
+    let scope = List.hd env.scopes in
+
     let r = VarMap.add (scope^"/init")
         (if active then VBool false
           else try VarMap.find (scope^"/init") st with Not_found -> assert false)
@@ -223,13 +266,13 @@ let extract_next_state active p scope eqs st ccmap =
     in
     let add_subscopes active =
       List.fold_left (fun (st, nst) (ss_id, ss_eqs, _) ->
-        aux active (scope^"/"^ss_id) ss_eqs st nst)
+        aux active [scope^"/"^ss_id] ss_eqs st nst)
     in
     let add_eq (st, nst) eq = match fst eq with
       | AST_assign(vars, e) ->
-        let st, nst = add_subscopes active (st, nst) (subscopes p e) in
+        let st, nst = add_subscopes active (st, nst) (subscopes env.p e) in
         List.fold_left (fun (st, nst) (pn, pe) ->
-            let st, v = if active then eval_expr p ccmap scope st pe
+            let st, v = if active then eval_expr { env with scopes = scopes } st pe
               else st,
                 try match VarMap.find (scope^"/"^pn) st with VPrevious x -> x | _ -> []
                 with Not_found -> []
@@ -238,24 +281,11 @@ let extract_next_state active p scope eqs st ccmap =
           (st, nst) (extract_pre e)
       | AST_assume _ | AST_guarantee _ -> st, nst
       | AST_automaton _ -> not_implemented "extract_next_state automaton"
+      | AST_activate _ -> not_implemented "extract_next_state activate"
     in
     List.fold_left add_eq (st, r) eqs
-  in aux active scope eqs st csts
+  in aux active env.scopes eqs st csts
 
-let program_init_state p root_node =
-  let (n, _) = find_node_decl p root_node in
-  let rec aux st p scope eqs =
-    let st = VarMap.add (scope^"/init") (VBool true) st in
-    let add_subscopes =
-      List.fold_left (fun st (ss_id, ss_eqs, _) -> aux st p (scope^"/"^ss_id) ss_eqs)
-    in
-    List.fold_left (fun st eq -> match fst eq with
-        | AST_assign(_, e) -> add_subscopes st (subscopes p e)
-        | AST_assume _ | AST_guarantee _ -> st
-        | AST_automaton _ -> not_implemented "prog_init_state aux automaton")
-      st eqs
-  in
-    aux (program_consts p) p "" n.body
 
 
 let program_step p st inputs root_node =
@@ -263,7 +293,7 @@ let program_step p st inputs root_node =
   let st = List.fold_left
     (fun st (n, v) -> VarMap.add ("/"^n) v st) st inputs in
 
-  let ccmap = build_prog_ccmap p "" n.body st in
+  let ccmap = build_prog_ccmap p [""] n.body st in
 
   let st = List.fold_left
     (fun st (_, (id, _), _) -> let st, _ = get_var st ccmap ("/"^id) in st)
@@ -271,7 +301,8 @@ let program_step p st inputs root_node =
   let outputs = List.map
     (fun (_, (id, _), _) -> let _, v = get_var st ccmap ("/"^id) in (id, v))
     n.ret in
-  let st, next_st = extract_next_state true p "" n.body st ccmap in
+
+  let st, next_st = extract_next_state true { p = p; scopes = [""]; c = ccmap } n.body st in
 
   st, outputs, next_st
   
diff --git a/libs/util.ml b/libs/util.ml
index cfa1619..522c3ec 100644
--- a/libs/util.ml
+++ b/libs/util.ml
@@ -1,6 +1,11 @@
 exception TypeError
 
 module VarMap = Mapext.Make(String)
+exception Duplicate of string
+let disjoint_union k a b = match a, b with
+  | Some x, None -> Some x
+  | None, Some y -> Some y 
+  | _ -> raise (Duplicate k)
 
 let rec fix equal f s =
   let fs = f s in
diff --git a/tests/limitera.scade b/tests/limitera.scade
new file mode 100644
index 0000000..1e4927e
--- /dev/null
+++ b/tests/limitera.scade
@@ -0,0 +1,26 @@
+const bound: int = 128;
+
+node limiter(x: int; d: int) returns (probe y: int)
+    var s, r: int;
+    let
+        assume in_bounded: x >= -bound and x <= bound;
+        guarantee out_bounded: y >= -bound and y <= bound;
+        s = 0 -> pre y;
+        r = x - s;
+        activate
+          if r <= -d then
+            let y = s - d; tel
+          else if r >= d then
+            let y = s + d; tel
+          else 
+            let y = x; tel
+        returns y;
+    tel
+
+node test(i: int) returns(a, b, c: int; exit: bool)
+    let
+        exit = i >= 30;
+        a = (i * 21 + 122) mod (2 * bound) - bound;  -- not really random
+        b = 16;
+        c = limiter(a, b);
+    tel