diff options
Diffstat (limited to 'frontend/parser.mly')
| -rw-r--r-- | frontend/parser.mly | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/frontend/parser.mly b/frontend/parser.mly index ec283c3..2483f09 100644 --- a/frontend/parser.mly +++ b/frontend/parser.mly @@ -9,7 +9,7 @@ open Util %token IF THEN ELSE %token NOT AND OR %token MOD -%token CONST NODE RETURNS +%token CONST NODE FUNCTION RETURNS %token VAR LET TEL %token PRE %token ASSUME GUARANTEE @@ -188,8 +188,11 @@ var_decl: | VAR l=nonempty_list(terminated(vari, SEMICOLON)) { List.flatten l } +node_kw: +| NODE {} +| FUNCTION {} node_decl: -| NODE id=IDENT LPAREN v=vars RPAREN +| node_kw id=IDENT LPAREN v=vars RPAREN RETURNS LPAREN rv=vars RPAREN e = dbody { { name = id; @@ -198,7 +201,7 @@ node_decl: var = []; body = e; } } -| NODE id=IDENT LPAREN v=vars RPAREN +| node_kw id=IDENT LPAREN v=vars RPAREN RETURNS LPAREN rv=vars RPAREN lv=var_decl b=body |