diff options
| -rw-r--r-- | .gitignore | 9 | ||||
| -rw-r--r-- | frontend/ast.ml | 3 | ||||
| -rw-r--r-- | frontend/ast_printer.ml | 16 | ||||
| -rw-r--r-- | frontend/parser.mly | 10 |
4 files changed, 28 insertions, 10 deletions
@@ -1,4 +1,11 @@ +# Temporary files of text editors *.swp +*~ + +# Build products _build analyze -*~ + +# Menhir automaton data +*.conflicts +*.automaton diff --git a/frontend/ast.ml b/frontend/ast.ml index 72f7049..b245119 100644 --- a/frontend/ast.ml +++ b/frontend/ast.ml @@ -14,6 +14,7 @@ type typ = | AST_TINT | AST_TBOOL | AST_TREAL + | AST_TGROUP of typ list type unary_op = | AST_UPLUS @@ -63,7 +64,7 @@ type expr = (* (TODO) and more : when, merge, activate instances, ... *) type eqn = - | AST_assign of (id ext) * (expr ext) + | 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... *) diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml index 422d446..611e802 100644 --- a/frontend/ast_printer.ml +++ b/frontend/ast_printer.ml @@ -75,12 +75,20 @@ let print_list f sep fmt l = in aux l +let print_id_ext fmt (i, _) = + Format.pp_print_string fmt i + (* types *) -let string_of_typ = function +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 *) @@ -159,9 +167,9 @@ let rec print_expr fmt e = let indent ind = ind^" " let rec print_eqn ind fmt = function - | AST_assign ((v,_),(e,_)) -> - Format.fprintf fmt "%s%s = %a;@\n" - ind v print_expr e + | AST_assign (l,(e,_)) -> + Format.fprintf fmt "%s%a = %a;@\n" + ind (print_list print_id_ext ", ") l print_expr e | AST_assume((i, _), (e, _)) -> Format.fprintf fmt "%sassume %s: %a;@\n" ind i print_expr e diff --git a/frontend/parser.mly b/frontend/parser.mly index 2c1ac25..51974d1 100644 --- a/frontend/parser.mly +++ b/frontend/parser.mly @@ -104,14 +104,16 @@ expr: (* Equations (can be asserts, automata, ...) *) eqn: -| i=ext(IDENT) EQUAL e=ext(expr) { AST_assign(i, e) } +| 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) } typ: -| INT { AST_TINT } -| BOOL { AST_TBOOL } -| REAL { AST_TREAL } +| INT { AST_TINT } +| BOOL { AST_TBOOL } +| REAL { AST_TREAL } +| LPAREN l=separated_list(COMMA, typ) RPAREN { AST_TGROUP(l) } (* Declarations *) dbody: |