diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-19 13:58:23 +0200 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-19 13:58:23 +0200 |
| commit | 1f91d2e97ef23a5182d0db8fdfbe4716fec46dd2 (patch) | |
| tree | d16e8a32e9ce16ddadeaa34808efc2f1111fb392 /Source/Dafny/Dafny.atg | |
| parent | b1530597d97bf6adbdc64b6f7698e1e1bee6966b (diff) | |
Allow empty calc statements
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 45 |
1 files changed, 23 insertions, 22 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 646d6ee4..90ff7bc5 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1230,30 +1230,31 @@ CalcStmt<out Statement/*!*/ s> Statement/*!*/ h;
IToken bodyStart, bodyEnd, opTok;
.)
- "calc" (. x = t; .)
- [ CalcOp<out opTok, out calcOp> ] (. resOp = calcOp; .)
+ "calc" (. x = t; .)
+ [ CalcOp<out opTok, out calcOp> ] (. resOp = calcOp; .)
"{"
- Expression<out e> (. lines.Add(e); .)
- ";"
- {
- ( BlockStmt<out block, out bodyStart, out bodyEnd> (. hints.Add(block); .)
- | CalcStmt<out h> (. hints.Add(h); .)
- | (. hints.Add(null); .)
- )
- ( CalcOp<out opTok, out op> (. maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(resOp, op);
- if (maybeOp == null) {
- customOps.Add(null); // pretend the operator was not there to satisfy the precondition of the CalcStmt contructor
- SemErr(opTok, "this operator cannot continue this calculation");
- } else {
- customOps.Add(op);
- resOp = (BinaryExpr.Opcode)maybeOp;
- }
- .)
- | (. customOps.Add(null); .)
- )
- Expression<out e> (. lines.Add(e); .)
+ [ Expression<out e> (. lines.Add(e); .)
";"
- }
+ {
+ ( BlockStmt<out block, out bodyStart, out bodyEnd> (. hints.Add(block); .)
+ | CalcStmt<out h> (. hints.Add(h); .)
+ | (. hints.Add(null); .)
+ )
+ ( CalcOp<out opTok, out op> (. maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(resOp, op);
+ if (maybeOp == null) {
+ customOps.Add(null); // pretend the operator was not there to satisfy the precondition of the CalcStmt contructor
+ SemErr(opTok, "this operator cannot continue this calculation");
+ } else {
+ customOps.Add(op);
+ resOp = (BinaryExpr.Opcode)maybeOp;
+ }
+ .)
+ | (. customOps.Add(null); .)
+ )
+ Expression<out e> (. lines.Add(e); .)
+ ";"
+ }
+ ]
"}"
(. s = new CalcStmt(x, calcOp, lines, hints, customOps); .)
.
|