summaryrefslogtreecommitdiff
path: root/frontend
diff options
context:
space:
mode:
Diffstat (limited to 'frontend')
-rw-r--r--frontend/ast.ml25
-rw-r--r--frontend/ast_printer.ml38
-rw-r--r--frontend/lexer.mll51
-rw-r--r--frontend/parser.mly41
4 files changed, 110 insertions, 45 deletions
diff --git a/frontend/ast.ml b/frontend/ast.ml
index b245119..50fa3f4 100644
--- a/frontend/ast.ml
+++ b/frontend/ast.ml
@@ -14,7 +14,6 @@ type typ =
| AST_TINT
| AST_TBOOL
| AST_TREAL
- | AST_TGROUP of typ list
type unary_op =
| AST_UPLUS
@@ -56,20 +55,29 @@ type expr =
| AST_binary_bool of bin_bool_op * (expr ext) * (expr ext)
| AST_not of expr ext
(* temporal primitives *)
- | AST_pre of expr ext
+ | AST_pre of expr ext * id
| AST_arrow of (expr ext) * (expr ext)
(* other *)
| AST_if of (expr ext) * (expr ext) * (expr ext)
- | AST_instance of (id ext) * (expr ext list)
- (* (TODO) and more : when, merge, activate instances, ... *)
+ | AST_instance of (id ext) * (expr ext list) * id
-type eqn =
+type var_def = bool * (id ext) * typ
+
+type automaton = id * state ext list * id list
+and state = {
+ initial : bool;
+ name : id;
+ locals : var_def list;
+ body : eqn ext list;
+ until : transition list;
+}
+and transition = (expr ext) * (id ext)
+
+and eqn =
| AST_assign of (id ext list) * (expr ext)
| AST_guarantee of (id ext) * (expr ext)
| AST_assume of (id ext) * (expr ext)
- (* (TODO) and more : automaton, activate... *)
-
-type var_def = bool * (id ext) * typ
+ | AST_automaton of automaton
type node_decl = {
name : id;
@@ -90,3 +98,4 @@ type toplevel =
| AST_const_decl of const_decl ext
type prog = toplevel list
+
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index 611e802..857e01d 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -57,7 +57,7 @@ let arrow_precedence = 20
let if_precedence = 10
let expr_precedence = function
- | AST_unary (_, _) | AST_pre(_) | AST_not(_) -> 99
+ | AST_unary (_, _) | AST_pre(_, _) | AST_not(_) -> 99
| AST_binary(op, _, _) -> binary_op_precedence op
| AST_binary_rel(r, _, _) -> binary_rel_precedence r
| AST_binary_bool(r, _, _) -> binary_bool_precedence r
@@ -84,11 +84,6 @@ let rec string_of_typ = function
| AST_TINT -> "int"
| AST_TBOOL -> "bool"
| AST_TREAL -> "real"
- | AST_TGROUP its ->
- List.fold_left (fun s t ->
- (if s = "" then "" else s ^ ", ") ^ (string_of_typ t))
- ""
- its
(* expressions *)
@@ -108,7 +103,7 @@ let rec print_expr fmt e =
if expr_precedence e1 <= expr_precedence e
then Format.fprintf fmt "(%a)" print_expr e1
else Format.fprintf fmt "%a" print_expr e1
- | AST_pre (e1,_) ->
+ | AST_pre ((e1,_), _) ->
Format.pp_print_string fmt "pre ";
if expr_precedence e1 <= expr_precedence e
then Format.fprintf fmt "(%a)" print_expr e1
@@ -158,7 +153,7 @@ let rec print_expr fmt e =
| AST_identifier (v,_) -> print_id fmt v
- | AST_instance ((i,_),l) ->
+ | AST_instance ((i,_),l, _) ->
Format.fprintf fmt "%a(%a)"
print_id i (print_list print_expr ", ") (List.map fst l)
@@ -176,19 +171,42 @@ let rec print_eqn ind fmt = function
| AST_guarantee((i, _), (e, _)) ->
Format.fprintf fmt "%sguarantee %s: %a;@\n"
ind i print_expr e
+ | AST_automaton a -> print_automaton ind fmt a
+
+and print_automaton ind fmt (n, sts, r) =
+ Format.fprintf fmt "%sautomaton %s@\n" ind n;
+ List.iter (print_state (indent ind) fmt) sts;
+ Format.fprintf fmt "%sreturns %a;@\n" ind (print_list print_id ", ") 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;
+ 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)
+ st.until
+ end
and print_block ind fmt b =
List.iter (fun (bb,_) -> print_eqn (indent ind) fmt bb) b
(* declarations *)
-let print_var_decl fmt (pr, (i, _), ty) =
+and print_var_decl fmt (pr, (i, _), ty) =
Format.fprintf fmt "%s%s: %s"
(if pr then "probe " else "")
i
(string_of_typ ty)
-let print_node_decl fmt (d : node_decl) =
+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
diff --git a/frontend/lexer.mll b/frontend/lexer.mll
index 1fd638b..9dc7da3 100644
--- a/frontend/lexer.mll
+++ b/frontend/lexer.mll
@@ -6,32 +6,39 @@
let kwd_table = Hashtbl.create 10
let () = List.iter (fun (a, b) -> Hashtbl.add kwd_table a b)
[
- "bool", BOOL;
- "int", INT;
- "real", REAL;
+ "bool", BOOL;
+ "int", INT;
+ "real", REAL;
- "const", CONST;
- "node", NODE;
- "returns", RETURNS;
- "var", VAR;
- "let", LET;
- "tel", TEL;
+ "const", CONST;
+ "node", NODE;
+ "returns", RETURNS;
+ "var", VAR;
+ "let", LET;
+ "tel", TEL;
- "if", IF;
- "then", THEN;
- "else", ELSE;
- "pre", PRE;
- "not", NOT;
- "and", AND;
- "or", OR;
- "mod", MOD;
+ "if", IF;
+ "then", THEN;
+ "else", ELSE;
+ "pre", PRE;
+ "not", NOT;
+ "and", AND;
+ "or", OR;
+ "mod", MOD;
- "true", TRUE;
- "false", FALSE;
+ "automaton", AUTOMATON;
+ "state", STATE;
+ "initial", INITIAL;
+ "unless", UNLESS;
+ "until", UNTIL;
+ "resume", RESUME;
- "assume", ASSUME;
- "guarantee",GUARANTEE;
- "probe", PROBE;
+ "true", TRUE;
+ "false", FALSE;
+
+ "assume", ASSUME;
+ "guarantee", GUARANTEE;
+ "probe", PROBE;
]
}
diff --git a/frontend/parser.mly b/frontend/parser.mly
index 51974d1..fb00478 100644
--- a/frontend/parser.mly
+++ b/frontend/parser.mly
@@ -1,5 +1,6 @@
%{
open Ast
+open Util
%}
%token BOOL INT REAL
@@ -12,6 +13,7 @@ open Ast
%token VAR LET TEL
%token PRE
%token ASSUME GUARANTEE
+%token AUTOMATON STATE INITIAL UNTIL UNLESS RESUME
%token LPAREN RPAREN
%token LCURLY RCURLY
@@ -57,12 +59,12 @@ primary_expr:
| TRUE { AST_bool_const true }
| FALSE { AST_bool_const false }
| e=ext(IDENT) LPAREN l=separated_list(COMMA,ext(expr)) RPAREN
- { AST_instance (e, l) }
+ { AST_instance (e, l, fst e ^ uid ()) }
unary_expr:
| e=primary_expr { e }
| NOT e=ext(unary_expr) { AST_not(e) }
-| PRE e=ext(unary_expr) { AST_pre(e) }
+| PRE e=ext(unary_expr) { AST_pre(e, "pre"^uid()) }
| o=unary_op e=ext(unary_expr) { AST_unary (o, e) }
%inline unary_op:
@@ -103,23 +105,52 @@ expr:
(* Equations (can be asserts, automata, ...) *)
+automaton:
+| AUTOMATON a=IDENT? s=list(ext(state)) RETURNS r=separated_list(COMMA, IDENT)
+ { ((match a with Some n -> n | None -> "aut") ^ uid (), s, r) }
+
+state:
+| i=boption(INITIAL) STATE n=IDENT
+ unless=trans(UNLESS)
+ v=option(var_decl)
+ b=body
+ until=trans(UNTIL)
+{ if unless <> [] then failwith "UNLESS transitions not supported.";
+ { initial = i;
+ name = n;
+ locals = (match v with Some v -> v | None -> []);
+ body = b;
+ until = until;
+} }
+
+trans(TT):
+| TT t=nonempty_list(terminated(transition, SEMICOLON)) { t }
+| { [] }
+
+transition:
+| IF e=ext(expr) RESUME s=ext(IDENT) { (e, s) }
+
+
eqn:
| i=separated_list(COMMA, ext(IDENT)) EQUAL e=ext(expr)
{ AST_assign(i, e) }
| 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) }
typ:
| INT { AST_TINT }
| BOOL { AST_TBOOL }
| REAL { AST_TREAL }
-| LPAREN l=separated_list(COMMA, typ) RPAREN { AST_TGROUP(l) }
(* Declarations *)
dbody:
| e=ext(eqn) SEMICOLON { [e] }
+| l=body { l }
+
+body:
| LET l=nonempty_list(terminated(ext(eqn), SEMICOLON)) TEL
- { l }
+ { l }
var:
| p=boption(PROBE) i=ext(IDENT) { (p, i) }
@@ -157,7 +188,7 @@ node_decl:
| NODE id=IDENT LPAREN v=vars RPAREN
RETURNS LPAREN rv=vars RPAREN
lv=var_decl
- LET b=nonempty_list(terminated(ext(eqn), SEMICOLON)) TEL
+ b=body
{ { name = id;
args = v;
ret = rv;
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-21 17:12:04 +0000