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
|
%{
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 }
|
