1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
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 }
|
