diff options
Diffstat (limited to 'Jennisys/Jennisys/Parser.fsy')
| -rw-r--r-- | Jennisys/Jennisys/Parser.fsy | 214 |
1 files changed, 0 insertions, 214 deletions
diff --git a/Jennisys/Jennisys/Parser.fsy b/Jennisys/Jennisys/Parser.fsy deleted file mode 100644 index de8e1fb8..00000000 --- a/Jennisys/Jennisys/Parser.fsy +++ /dev/null @@ -1,214 +0,0 @@ -%{
-
-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 }
|