summaryrefslogtreecommitdiff
path: root/frontend
diff options
context:
space:
mode:
Diffstat (limited to 'frontend')
-rw-r--r--frontend/ast.ml13
-rw-r--r--frontend/ast_printer.ml63
-rw-r--r--frontend/lexer.mll2
-rw-r--r--frontend/parser.mly19
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 }
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-19 16:36:39 +0000