diff options
Diffstat (limited to 'Source/Jennisys/Parser.fsy')
| -rw-r--r-- | Source/Jennisys/Parser.fsy | 214 |
1 files changed, 214 insertions, 0 deletions
diff --git a/Source/Jennisys/Parser.fsy b/Source/Jennisys/Parser.fsy new file mode 100644 index 00000000..de8e1fb8 --- /dev/null +++ b/Source/Jennisys/Parser.fsy @@ -0,0 +1,214 @@ +%{
+
+open Ast
+open Getters
+open AstUtils
+
+let rec MyFold ee acc =
+ match ee with
+ | [] -> acc
+ | x::rest -> BinaryAnd x (MyFold rest acc)
+
+%}
+
+// 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 <int> INTEGER
+%token DOT
+%token NOT
+%token STAR DIV MOD
+%token PLUS MINUS
+%token OLD
+%token DOTDOT DOTDOTDOT
+%token EQ NEQ LESS ATMOST ATLEAST GREATER IN NOTIN
+%token AND OR
+%token IMPLIES
+%token IFF
+%token LPAREN RPAREN LBRACKET RBRACKET LCURLY RCURLY VERTBAR
+%token GETS COLON COLONCOLON COMMA QMARK
+%token INTERFACE DATAMODEL CODE
+%token VAR CONSTRUCTOR METHOD FRAME INVARIANT RETURNS REQUIRES ENSURES FORALL
+%token INTTYPE BOOLTYPE SEQTYPE SETTYPE
+%token EOF
+
+// This is the type of the data produced by a successful reduction of the 'start'
+// symbol:
+%type < Ast.SyntacticProgram > 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: TopLevelDecls EOF { SProgram($1) }
+
+TopLevelDecls:
+ | { [] }
+ | TopLevelDecl TopLevelDecls { $1 :: $2 }
+
+TopLevelDecl:
+ | INTERFACE ID TypeParams LCURLY Members RCURLY { Interface($2, $3, $5) }
+ | DATAMODEL ID TypeParams LCURLY FrameMembers RCURLY { match $5 with (vv,fr,inv) -> DataModel($2, $3, vv, fr, inv) }
+ | CODE ID TypeParams LCURLY RCURLY { Code($2, $3) }
+
+TypeParams:
+ | { [] }
+ | LBRACKET IdList RBRACKET { $2 }
+
+IdList:
+ | ID { [$1] }
+ | ID IdList { $1 :: $2 }
+
+Members:
+ | { [] }
+ | Member Members { $1 :: $2 }
+
+Signature:
+ | LPAREN VarDeclList RPAREN { Sig($2, []) }
+ | LPAREN VarDeclList RPAREN RETURNS LPAREN VarDeclList RPAREN { Sig($2, $6) }
+
+Pre:
+ | { TrueLiteral }
+ | REQUIRES Expr Pre { BinaryAnd $2 $3 }
+
+Post:
+ | { TrueLiteral }
+ | ENSURES Expr Post { BinaryAnd $2 $3 }
+ | ID GETS Expr Post { BinaryAnd (BinaryExpr(40,"=",IdLiteral($1),$3)) $4 }
+
+StmtList:
+ | { [] }
+ | Stmt StmtList { $1 :: $2 }
+
+Stmt:
+ | BlockStmt { $1 }
+ | Expr GETS Expr { Assign($1, $3) }
+
+BlockStmt:
+ | LCURLY StmtList RCURLY { Block $2 }
+
+Member:
+ | VAR VarDecl { Field($2) }
+ | CONSTRUCTOR ID Signature Pre Post { Method($2, $3, RewriteVars (GetSigVars $3) $4, RewriteVars (GetSigVars $3) $5, true) }
+ | METHOD ID Signature Pre Post { Method($2, $3, RewriteVars (GetSigVars $3) $4, RewriteVars (GetSigVars $3) $5, false) }
+ | INVARIANT ExprList { Invariant($2) }
+
+FrameMembers:
+ | { [], [], TrueLiteral }
+ | VAR VarDecl FrameMembers { match $3 with (vv,fr,inv) -> $2 :: vv, fr, inv }
+ | FRAME FrameMembers { $2 }
+ | FRAME FramePartitionList FrameMembers { match $3 with (vv,fr,inv) -> vv, List.append $2 fr, inv }
+ | INVARIANT ExprList FrameMembers { match $3 with (vv,fr,inv) -> vv, fr, MyFold $2 inv }
+
+FramePartitionList:
+ | FramePartition { $1 }
+ | FramePartition FramePartitionList { List.append $1 $2 }
+
+VarDeclList:
+ | { [] }
+ | VarDecl { [$1] }
+ | VarDecl COMMA VarDeclList { $1 :: $3 }
+
+VarDecl:
+ | ID { Var($1,None, false) }
+ | ID COLON Type { Var($1,Some($3), false) }
+
+Type:
+ | INTTYPE { IntType }
+ | BOOLTYPE { BoolType }
+ | ID { NamedType($1, []) }
+ | SEQTYPE LBRACKET Type RBRACKET { SeqType($3) }
+ | SETTYPE LBRACKET Type RBRACKET { SetType($3) }
+ | ID LBRACKET Type RBRACKET { InstantiatedType($1, [$3]) }
+
+ExprList:
+ | { [] }
+ | Expr { [$1] }
+ | Expr ExprList { $1 :: $2 }
+
+Expr:
+ | Expr10 { $1 }
+
+Expr10:
+ | Expr20 { $1 }
+ | Expr10 IFF Expr20 { BinaryExpr(10,"<==>",$1,$3) }
+
+Expr20:
+ | Expr25 { $1 }
+ | Expr25 IMPLIES Expr20 { BinaryExpr(20,"==>",$1,$3) }
+
+Expr25:
+ | Expr30 { $1 }
+ | Expr30 QMARK Expr25 COLON Expr25 { IteExpr($1,$3,$5) }
+Expr30:
+ | Expr40 { $1 }
+ | Expr40 AND Expr30and { BinaryAnd $1 $3 }
+ | Expr40 OR Expr30or { BinaryOr $1 $3 }
+Expr30and:
+ | Expr40 { $1 }
+ | Expr40 AND Expr30and { BinaryAnd $1 $3 }
+Expr30or:
+ | Expr40 { $1 }
+ | Expr40 AND Expr30or { BinaryOr $1 $3 }
+
+Expr40:
+ | Expr50 { $1 }
+ | Expr50 EQ Expr50 { BinaryExpr(40,"=",$1,$3) }
+ | Expr50 NEQ Expr50 { BinaryExpr(40,"!=",$1,$3) }
+ | Expr50 LESS Expr50 { BinaryExpr(40,"<",$1,$3) }
+ | Expr50 ATMOST Expr50 { BinaryExpr(40,"<=",$1,$3) }
+ | Expr50 ATLEAST Expr50 { BinaryExpr(40,">=",$1,$3) }
+ | Expr50 GREATER Expr50 { BinaryExpr(40,">",$1,$3) }
+ | Expr50 IN Expr50 { BinaryExpr(40,"in",$1,$3) }
+ | Expr50 NOTIN Expr50 { BinaryExpr(40,"!in",$1,$3) }
+
+Expr50:
+ | Expr55 { $1 }
+ | Expr55 DOTDOTDOT Expr55 { BinaryExpr(50,"...",$1,$3) }
+
+Expr55:
+ | Expr60 { $1 }
+ | Expr55 PLUS Expr60 { BinaryExpr(55,"+",$1,$3) }
+ | Expr55 MINUS Expr60 { BinaryExpr(55,"-",$1,$3) }
+
+Expr60:
+ | Expr90 { $1 }
+ | Expr60 STAR Expr90 { BinaryExpr(60,"*",$1,$3) }
+ | Expr60 DIV Expr90 { BinaryExpr(60,"div",$1,$3) }
+ | Expr60 MOD Expr90 { BinaryExpr(60,"mod",$1,$3) }
+
+Expr90:
+ | Expr100 { $1 }
+ | OLD LPAREN Expr90 RPAREN { OldExpr($3) }
+ | NOT Expr90 { UnaryExpr("!", $2) }
+ | MINUS Expr90 { UnaryExpr("-", $2) }
+ | Expr90 DOTDOT { LCIntervalExpr($1) }
+
+Expr100:
+ | INTEGER { IntLiteral($1) }
+ | ID { if $1 = "this" then
+ ObjLiteral("this")
+ elif $1 = "null" then
+ ObjLiteral("null")
+ else
+ IdLiteral($1) }
+ | Expr100 DOT ID { Dot($1, $3) }
+ | Expr100 LBRACKET StarExpr RBRACKET { SelectExpr($1, $3) }
+ | Expr100 LBRACKET Expr GETS Expr RBRACKET { UpdateExpr($1, $3, $5) }
+ | LPAREN Expr RPAREN { $2 }
+ | LBRACKET ExprList RBRACKET { SequenceExpr($2) }
+ | LCURLY ExprList RCURLY { SetExpr($2) }
+ | VERTBAR Expr VERTBAR { SeqLength($2) }
+ | FORALL VarDeclList COLONCOLON Expr { ForallExpr($2, RewriteVars $2 $4) }
+
+StarExpr:
+ | STAR { Star }
+ | Expr { $1 }
+
+FramePartition:
+ | Expr100 { [$1] }
+ | Expr100 STAR FramePartition { $1 :: $3 }
|