diff options
Diffstat (limited to 'Source/Forro/Parser.fsy')
| -rw-r--r-- | Source/Forro/Parser.fsy | 244 |
1 files changed, 122 insertions, 122 deletions
diff --git a/Source/Forro/Parser.fsy b/Source/Forro/Parser.fsy index 5dbb8a4c..af64d267 100644 --- a/Source/Forro/Parser.fsy +++ b/Source/Forro/Parser.fsy @@ -1,122 +1,122 @@ -%{
-
-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 STAR
-%token PLUS MINUS
-%token EQ NEQ LESS ATMOST
-%token AND OR
-%token OLD LPAREN RPAREN LCURLY RCURLY SEMI COMMA 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 ProcedureSpec
- DO StmtList END SEMI
- { match $2, $3 with (outs,id,ins), (req,ens) -> Proc(id, StringsToVariables ins, StringsToVariables outs, req, ens, $5) }
-
-ProcedureSpec:
- REQUIRES Expression ENSURES Expression { $2, $4 }
-
-Signature:
- ID LPAREN IdList RPAREN { [], $1, $3 }
- | ID LPAREN RPAREN { [], $1, [] }
- | IdList ASSIGN ID LPAREN IdList RPAREN { $1, $3, $5 }
- | IdList ASSIGN ID LPAREN RPAREN { $1, $3, [] }
-
-IdList: ID { [$1] }
- | ID COMMA IdList { $1 :: $3 }
-
-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:
- | Expression { [$1] }
- | Expression COMMA ExprList { $1::$3 }
-
-VarList:
- | ID ASSIGN { [Var($1)] }
- | ID COMMA VarList { Var($1)::$3 }
-
-StmtList:
- StmtListX { Block($1) }
-
-StmtListX:
- { [] }
- | Stmt StmtListX { $1::$2 }
-
-Stmt:
- ID ASSIGN Expression SEMI { Assign(Var($1), $3) }
- | ID ASSIGN NEW LPAREN Expression COMMA
- Expression RPAREN SEMI { Alloc(Var($1), $5, $7) }
- | 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 RPAREN SEMI { CallStmt([],$2,[]) }
- | CALL ID LPAREN ExprList RPAREN SEMI { CallStmt([],$2,$4) }
- | CALL VarList ID LPAREN RPAREN SEMI { CallStmt($2,$3,[]) }
- | CALL VarList ID LPAREN ExprList RPAREN SEMI { CallStmt($2,$3,$5) }
- | ASSERT Expression SEMI { Assert($2) }
-
-Invariants:
- { [] }
- | INVARIANT Expression Invariants { $2::$3 }
+%{ + +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 STAR +%token PLUS MINUS +%token EQ NEQ LESS ATMOST +%token AND OR +%token OLD LPAREN RPAREN LCURLY RCURLY SEMI COMMA 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 ProcedureSpec + DO StmtList END SEMI + { match $2, $3 with (outs,id,ins), (req,ens) -> Proc(id, StringsToVariables ins, StringsToVariables outs, req, ens, $5) } + +ProcedureSpec: + REQUIRES Expression ENSURES Expression { $2, $4 } + +Signature: + ID LPAREN IdList RPAREN { [], $1, $3 } + | ID LPAREN RPAREN { [], $1, [] } + | IdList ASSIGN ID LPAREN IdList RPAREN { $1, $3, $5 } + | IdList ASSIGN ID LPAREN RPAREN { $1, $3, [] } + +IdList: ID { [$1] } + | ID COMMA IdList { $1 :: $3 } + +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: + | Expression { [$1] } + | Expression COMMA ExprList { $1::$3 } + +VarList: + | ID ASSIGN { [Var($1)] } + | ID COMMA VarList { Var($1)::$3 } + +StmtList: + StmtListX { Block($1) } + +StmtListX: + { [] } + | Stmt StmtListX { $1::$2 } + +Stmt: + ID ASSIGN Expression SEMI { Assign(Var($1), $3) } + | ID ASSIGN NEW LPAREN Expression COMMA + Expression RPAREN SEMI { Alloc(Var($1), $5, $7) } + | 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 RPAREN SEMI { CallStmt([],$2,[]) } + | CALL ID LPAREN ExprList RPAREN SEMI { CallStmt([],$2,$4) } + | CALL VarList ID LPAREN RPAREN SEMI { CallStmt($2,$3,[]) } + | CALL VarList ID LPAREN ExprList RPAREN SEMI { CallStmt($2,$3,$5) } + | ASSERT Expression SEMI { Assert($2) } + +Invariants: + { [] } + | INVARIANT Expression Invariants { $2::$3 } |