Initial commit: parser for tiny subset of SCADE language...

1 files changed, 221 insertions, 0 deletions

diff --git a/frontend/parser.mly b/frontend/parser.mly
new file mode 100644
index 0000000..9db1bd5
--- /dev/null
+++ b/frontend/parser.mly
@@ -0,0 +1,221 @@
+%{
+open Ast
+%}
+
+/* tokens */
+/**********/
+
+%token BOOL
+%token INT
+%token REAL
+%token PROBE
+%token TRUE
+%token THEN
+%token FALSE
+%token IF
+%token ELSE
+%token NOT
+%token AND
+%token OR
+%token MOD
+%token CONST
+%token NODE
+%token RETURNS
+%token VAR
+%token LET
+%token 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 ARROW
+
+%token <string> IDENT
+%token <string> INTVAL
+
+%token EOF
+
+/* priorities of binary operators (lowest to highest) */
+%left ARROW
+%left OR
+%left AND
+%left EQUAL DIFF
+%left LESS GREATER LESS_EQUAL GREATER_EQUAL
+%left PLUS MINUS
+%left STAR DIVIDE MOD
+
+
+/* entry-points */
+/****************/
+
+%start<Ast.toplevel list> file
+
+
+%%
+
+
+/* toplevel */
+/************/
+
+file: t=list(toplevel) EOF { t }
+
+toplevel:
+| 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 }
+| e=ext(IDENT) LPAREN l=separated_list(COMMA,ext(expr)) RPAREN 
+   { AST_instance (e, l) }
+
+
+unary_expr:
+| e=primary_expr                   { 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) o=binary_op f=ext(binary_expr)   { AST_binary (o, e, f) }
+
+%inline binary_op:
+| STAR           { AST_MUL }
+| DIVIDE         { AST_DIV }
+| MOD            { AST_MOD }
+| PLUS           { AST_PLUS }
+| MINUS          { AST_MINUS }
+| LESS           { AST_LT }
+| GREATER        { AST_GT }
+| LESS_EQUAL     { AST_LE }
+| GREATER_EQUAL  { AST_GE }
+| EQUAL          { AST_EQ}
+| DIFF           { AST_NE }
+| 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 }
+
+expr:
+| e=if_expr { e }
+
+lvalue:
+| i=IDENT   { i }
+
+
+/* equations */
+/****************/
+
+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) }
+
+typ:
+| INT    { AST_TINT }
+| BOOL   { AST_TBOOL }
+| REAL   { AST_TREAL }
+
+dbody:
+| e=ext(eqn) SEMICOLON
+    { [e] }
+| LET l=nonempty_list(terminated(ext(eqn), SEMICOLON)) TEL
+    { l }
+
+/* declarations */
+
+var:
+|   p=boption(PROBE) i=ext(IDENT)
+    { (p, i) }
+
+vari:
+|   vn=separated_list(COMMA, var) COLON t=typ
+    { List.map (fun (p, i) -> (p, i, t)) vn }
+
+vars:
+| v=separated_list(SEMICOLON, vari)
+    { List.flatten v }
+
+const_decl:
+| CONST i=ext(IDENT) COLON t=typ EQUAL e=ext(expr) SEMICOLON
+    { (i, t, e) }
+
+var_decl:
+| VAR l=nonempty_list(terminated(vari, SEMICOLON))
+    { List.flatten l }
+
+node_decl:
+| 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
+    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 */
+%inline ext(X): 
+| x=X { x, ($startpos, $endpos) }
+
+
+%%