diff options
Diffstat (limited to 'frontend/parser.mly')
| -rw-r--r-- | frontend/parser.mly | 187 |
1 files changed, 68 insertions, 119 deletions
diff --git a/frontend/parser.mly b/frontend/parser.mly index 9db1bd5..2c1ac25 100644 --- a/frontend/parser.mly +++ b/frontend/parser.mly @@ -2,62 +2,32 @@ open Ast %} -/* tokens */ -/**********/ - -%token BOOL -%token INT -%token REAL +%token BOOL INT REAL %token PROBE -%token TRUE -%token THEN -%token FALSE -%token IF -%token ELSE -%token NOT -%token AND -%token OR +%token TRUE FALSE +%token IF THEN ELSE +%token NOT AND OR %token MOD -%token CONST -%token NODE -%token RETURNS -%token VAR -%token LET -%token TEL +%token CONST NODE RETURNS +%token VAR LET TEL %token PRE -%token ASSUME -%token GUARANTEE - -%token LPAREN -%token RPAREN -%token LCURLY -%token RCURLY -%token STAR -%token PLUS -%token MINUS -%token EXCLAIM -%token DIVIDE -%token PERCENT -%token LESS -%token GREATER -%token LESS_EQUAL -%token GREATER_EQUAL -%token EQUAL_EQUAL -%token DIFF -%token AND_AND -%token BAR_BAR -%token SEMICOLON -%token COLON -%token COMMA -%token EQUAL +%token ASSUME GUARANTEE + +%token LPAREN RPAREN +%token LCURLY RCURLY +%token STAR PLUS MINUS DIVIDE +%token LESS GREATER LESS_EQUAL GREATER_EQUAL +%token DIFF EQUAL +%token SEMICOLON COLON COMMA %token ARROW %token <string> IDENT %token <string> INTVAL +%token <string> REALVAL %token EOF -/* priorities of binary operators (lowest to highest) */ +(* Lowest priorities first *) %left ARROW %left OR %left AND @@ -66,53 +36,46 @@ open Ast %left PLUS MINUS %left STAR DIVIDE MOD - -/* entry-points */ -/****************/ - +(* Root token *) %start<Ast.toplevel list> file - %% - -/* toplevel */ -/************/ - -file: t=list(toplevel) EOF { t } +file: +| t=list(toplevel) EOF { t } toplevel: -| d=ext(const_decl) { AST_const_decl d } -| d=ext(node_decl) { AST_node_decl d } - +| d=ext(const_decl) { AST_const_decl d } +| d=ext(node_decl) { AST_node_decl d } -/* expressions */ -/***************/ primary_expr: -| LPAREN e=expr RPAREN { e } -| e=ext(IDENT) { AST_identifier e } -| e=ext(INTVAL) { AST_int_const e } -| TRUE { AST_bool_const true } -| FALSE { AST_bool_const false } +| LPAREN e=expr RPAREN { e } +| e=ext(IDENT) { AST_identifier e } +| e=ext(INTVAL) { AST_int_const e } +| e=ext(REALVAL) { AST_real_const e } +| 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) } unary_expr: | e=primary_expr { e } +| NOT e=ext(unary_expr) { AST_not(e) } +| PRE e=ext(unary_expr) { AST_pre(e) } | o=unary_op e=ext(unary_expr) { AST_unary (o, e) } %inline unary_op: | PLUS { AST_UPLUS } | MINUS { AST_UMINUS } -| NOT { AST_NOT } -| PRE { AST_PRE } binary_expr: | e=unary_expr { e } +| e=ext(binary_expr) ARROW f=ext(binary_expr) { AST_arrow(e, f) } | e=ext(binary_expr) o=binary_op f=ext(binary_expr) { AST_binary (o, e, f) } +| e=ext(binary_expr) o=binary_rel f=ext(binary_expr) { AST_binary_rel (o, e, f) } +| e=ext(binary_expr) o=binary_bool f=ext(binary_expr) { AST_binary_bool (o, e, f) } %inline binary_op: | STAR { AST_MUL } @@ -120,55 +83,44 @@ binary_expr: | MOD { AST_MOD } | PLUS { AST_PLUS } | MINUS { AST_MINUS } +%inline binary_rel: | LESS { AST_LT } | GREATER { AST_GT } | LESS_EQUAL { AST_LE } | GREATER_EQUAL { AST_GE } | EQUAL { AST_EQ} | DIFF { AST_NE } +%inline binary_bool: | AND { AST_AND } | OR { AST_OR } -| ARROW { AST_ARROW } if_expr: -| IF c=ext(expr) THEN t=ext(expr) ELSE e=ext(expr) - { AST_if(c, t, e) } -| e=binary_expr { e } +| IF c=ext(expr) THEN t=ext(expr) ELSE e=ext(expr) { AST_if(c, t, e) } +| e=binary_expr { e } expr: -| e=if_expr { e } - -lvalue: -| i=IDENT { i } +| e=if_expr { e } -/* equations */ -/****************/ - +(* Equations (can be asserts, automata, ...) *) eqn: -| i=ext(lvalue) 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) } +| i=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 } +(* Declarations *) dbody: -| e=ext(eqn) SEMICOLON - { [e] } +| e=ext(eqn) SEMICOLON { [e] } | LET l=nonempty_list(terminated(ext(eqn), SEMICOLON)) TEL - { l } - -/* declarations */ + { l } var: -| p=boption(PROBE) i=ext(IDENT) - { (p, i) } +| p=boption(PROBE) i=ext(IDENT) { (p, i) } vari: | vn=separated_list(COMMA, var) COLON t=typ @@ -179,43 +131,40 @@ vars: { List.flatten v } const_decl: -| CONST i=ext(IDENT) COLON t=typ EQUAL e=ext(expr) SEMICOLON - { (i, t, e) } +| CONST i=IDENT COLON t=typ EQUAL e=ext(expr) SEMICOLON + { { + name = i; + typ = t; + value = e; + } } var_decl: | VAR l=nonempty_list(terminated(vari, SEMICOLON)) { List.flatten l } node_decl: -| NODE id=IDENT - LPAREN v=vars RPAREN +| NODE id=IDENT LPAREN v=vars RPAREN RETURNS LPAREN rv=vars RPAREN e = dbody - { { name = id; - args = v; - ret = rv; - var = []; - body = e; - } } -| NODE id=IDENT - LPAREN v=vars RPAREN +{ { name = id; + args = v; + ret = rv; + var = []; + body = e; +} } +| NODE id=IDENT LPAREN v=vars RPAREN RETURNS LPAREN rv=vars RPAREN lv=var_decl LET b=nonempty_list(terminated(ext(eqn), SEMICOLON)) TEL - { { name = id; - args = v; - ret = rv; - var = lv; - body = b; - } } - - -/* utilities */ -/*************/ - -/* adds extent information to rule */ +{ { name = id; + args = v; + ret = rv; + var = lv; + body = b; +} } + +(* Utility : add extent information *) %inline ext(X): | x=X { x, ($startpos, $endpos) } - %% |