diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-07-31 15:01:02 +0200 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-07-31 15:01:02 +0200 |
| commit | 6c7d4a409f3ced78bd1d15c9743bb357c46320fa (patch) | |
| tree | c0abb4b38761faac61d43ecd31e43c277edc38ad /Source/Dafny/Dafny.atg | |
| parent | 97404d89e5c945d41899ed74e5aa234a61b91c65 (diff) | |
Allowing dangling hints in calculations.
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 71dec0d7..f9dff93f 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1393,10 +1393,9 @@ CalcStmt<out Statement/*!*/ s> .)
]
"{"
- [ Expression<out e> (. lines.Add(e); stepOp = calcOp; .)
+ { Expression<out e> (. lines.Add(e); stepOp = calcOp; .)
";"
- {
- [ CalcOp<out opTok, out op> (. maybeOp = resOp.ResultOp(op);
+ [ CalcOp<out opTok, out op> (. maybeOp = resOp.ResultOp(op);
if (maybeOp == null) {
SemErr(opTok, "this operator cannot continue this calculation");
} else {
@@ -1404,14 +1403,17 @@ CalcStmt<out Statement/*!*/ s> resOp = maybeOp;
}
.)
- ] (. stepOps.Add(stepOp); .)
- Hint<out h> (. hints.Add(h); .)
- Expression<out e> (. lines.Add(e); stepOp = calcOp; .)
- ";"
- }
- ]
+ ] (. stepOps.Add(stepOp); .)
+ Hint<out h> (. hints.Add(h); .)
+ }
"}"
- (. s = new CalcStmt(x, calcOp, lines, hints, stepOps, resOp); .)
+ (.
+ if (lines.Count > 0) {
+ // Repeat the last line to create a dummy line for the dangling hint
+ lines.Add(lines[lines.Count - 1]);
+ }
+ s = new CalcStmt(x, calcOp, lines, hints, stepOps, resOp);
+ .)
.
CalcOp<out IToken x, out CalcStmt.CalcOp/*!*/ op>
= (. var binOp = BinaryExpr.Opcode.Eq; // Returns Eq if parsing fails because it is compatible with any other operator
|