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
|
%{
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 PLUS MINUS
%token STAR
%token EQ NEQ LESS ATMOST
%token AND OR
%token OLD LPAREN RPAREN SEMI 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
REQUIRES Expression ENSURES Expression
DO StmtList END SEMI
{ match $2 with outs,id,ins -> Proc(id, StringsToVariables ins, StringsToVariables outs, $4, $6, $8) }
Signature:
IdList { [], List.head $1, List.tail $1 }
| IdList ASSIGN IdList { $1, List.head $3, List.tail $3 }
IdList: ID { [$1] }
| ID IdList { $1 :: $2 }
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: // possibly empty
{ [] }
| Expression ExprList { $1::$2 }
VarList: // nonempty
| ID ASSIGN { [Var($1)] }
| ID VarList { Var($1)::$2 }
StmtList:
StmtListX { Block($1) }
StmtListX:
{ [] }
| Stmt StmtListX { $1::$2 }
Stmt:
ID ASSIGN Expression SEMI { Assign(Var($1), $3) }
| ID ASSIGN NEW Expression Expression SEMI { Alloc(Var($1), $4, $5) }
| 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 ExprList RPAREN SEMI { CallStmt([],$2,$4) }
| CALL VarList ID LPAREN ExprList RPAREN SEMI { CallStmt($2,$3,$5) }
| ASSERT Expression SEMI { Assert($2) }
Invariants:
{ [] }
| INVARIANT Expression Invariants { $2::$3 }
|