summaryrefslogtreecommitdiff
path: root/Source/Forro/Parser.fsy
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Forro/Parser.fsy')
-rw-r--r--Source/Forro/Parser.fsy115
1 files changed, 115 insertions, 0 deletions
diff --git a/Source/Forro/Parser.fsy b/Source/Forro/Parser.fsy
new file mode 100644
index 00000000..6fa41431
--- /dev/null
+++ b/Source/Forro/Parser.fsy
@@ -0,0 +1,115 @@
+%{
+
+open Forro
+
+exception ParseError of string
+
+let StringsToVariables ss = [ for s in ss -> Var(s) ]
+
+let IdToField id =
+ match id with
+ | "head" -> Field.Head
+ | "tail" -> Field.Tail
+ | "valid" -> Field.Valid
+ | _ -> raise (ParseError ("illegal field selector: '" + id + "' (legal selectors are 'head', 'tail', and 'valid')"))
+
+%}
+
+// The start token becomes a parser function in the compiled code:
+%start start
+
+// These are the terminal tokens of the grammar along with the types of
+// the data carried by each token:
+%token <string> ID
+%token <System.Int32> INT32
+%token NULL
+%token DOT
+%token NOT
+%token PLUS MINUS
+%token STAR
+%token EQ NEQ LESS ATMOST
+%token AND OR
+%token OLD LPAREN RPAREN SEMI ASSIGN
+%token PROCEDURE REQUIRES ENSURES DO END
+%token NEW IF THEN ELSE WHILE INVARIANT CALL ASSERT
+%token EOF
+
+// This is the type of the data produced by a successful reduction of the 'start'
+// symbol:
+%type < Forro.Program > start
+
+%%
+
+// These are the rules of the grammar along with the F# code of the
+// actions executed as rules are reduced. In this case the actions
+// produce data using F# data construction terms.
+start: Prog EOF { Prog(List.rev($1)) }
+
+Prog: Proc { [$1] }
+ | Prog Proc { $2 :: $1 }
+
+Proc:
+ PROCEDURE Signature
+ REQUIRES Expression ENSURES Expression
+ DO StmtList END SEMI
+ { match $2 with outs,id,ins -> Proc(id, StringsToVariables ins, StringsToVariables outs, $4, $6, $8) }
+
+Signature:
+ IdList { [], List.head $1, List.tail $1 }
+ | IdList ASSIGN IdList { $1, List.head $3, List.tail $3 }
+
+IdList: ID { [$1] }
+ | ID IdList { $1 :: $2 }
+
+Expression:
+ AtomicExpr { $1 }
+ | NOT Expression { Not($2) }
+ | Expression PLUS Expression { Binary(Operator.Plus, $1, $3) }
+ | Expression MINUS Expression { Binary(Operator.Minus, $1, $3) }
+ | Expression STAR Expression { Binary(Operator.Times, $1, $3) }
+ | Expression EQ Expression { Binary(Operator.Eq, $1, $3) }
+ | Expression NEQ Expression { Binary(Operator.Neq, $1, $3) }
+ | Expression LESS Expression { Binary(Operator.Less, $1, $3) }
+ | Expression ATMOST Expression { Binary(Operator.AtMost, $1, $3) }
+ | Expression AND Expression { Binary(Operator.And, $1, $3) }
+ | Expression OR Expression { Binary(Operator.Or, $1, $3) }
+
+AtomicExpr:
+ INT32 { Constant($1) }
+ | NULL { Null }
+ | ID { Identifier(Var($1)) }
+ | OLD LPAREN Expression RPAREN { Old($3) }
+ | LPAREN Expression RPAREN { $2 }
+ | FieldSelect { match $1 with e,f -> Select(e,f) }
+
+FieldSelect:
+ AtomicExpr DOT ID { $1, IdToField $3 }
+
+ExprList: // possibly empty
+ { [] }
+ | Expression ExprList { $1::$2 }
+
+VarList: // nonempty
+ | ID ASSIGN { [Var($1)] }
+ | ID VarList { Var($1)::$2 }
+
+StmtList:
+ StmtListX { Block($1) }
+
+StmtListX:
+ { [] }
+ | Stmt StmtListX { $1::$2 }
+
+Stmt:
+ ID ASSIGN Expression SEMI { Assign(Var($1), $3) }
+ | ID ASSIGN NEW Expression Expression SEMI { Alloc(Var($1), $4, $5) }
+ | FieldSelect ASSIGN Expression SEMI { match $1 with e,f -> Update(e, f, $3) }
+ | IF Expression THEN StmtList ELSE StmtList END SEMI { IfStmt($2,$4,$6) }
+ | WHILE Expression Invariants DO StmtList END SEMI { WhileStmt($2,$3,$5) }
+ | CALL ID LPAREN ExprList RPAREN SEMI { CallStmt([],$2,$4) }
+ | CALL VarList ID LPAREN ExprList RPAREN SEMI { CallStmt($2,$3,$5) }
+ | ASSERT Expression SEMI { Assert($2) }
+
+Invariants:
+ { [] }
+ | INVARIANT Expression Invariants { $2::$3 }