diff options
| -rw-r--r-- | Dafny/Cloner.cs | 2 | ||||
| -rw-r--r-- | Dafny/Dafny.atg | 32 | ||||
| -rw-r--r-- | Dafny/DafnyAst.cs | 7 | ||||
| -rw-r--r-- | Dafny/Parser.cs | 43 | ||||
| -rw-r--r-- | Dafny/Printer.cs | 4 | ||||
| -rw-r--r-- | Dafny/Resolver.cs | 7 | ||||
| -rw-r--r-- | Dafny/Translator.cs | 5 | ||||
| -rw-r--r-- | Test/dafny2/Calculations.dfy | 8 |
8 files changed, 60 insertions, 48 deletions
diff --git a/Dafny/Cloner.cs b/Dafny/Cloner.cs index a5865a6f..c972c5c4 100644 --- a/Dafny/Cloner.cs +++ b/Dafny/Cloner.cs @@ -424,7 +424,7 @@ namespace Microsoft.Dafny } else if (stmt is CalcStmt) {
var s = (CalcStmt)stmt;
- r = new CalcStmt(Tok(s.Tok), s.Op, s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneStmt), new List<Nullable<BinaryExpr.Opcode>>(s.CustomOps));
+ r = new CalcStmt(Tok(s.Tok), s.Op, s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), new List<Nullable<BinaryExpr.Opcode>>(s.CustomOps));
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 90ff7bc5..cf74fc30 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -1221,25 +1221,21 @@ CalcStmt<out Statement/*!*/ s> = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x;
BinaryExpr.Opcode op, calcOp = BinaryExpr.Opcode.Eq, resOp = BinaryExpr.Opcode.Eq;
- List<Expression/*!*/> lines = new List<Expression/*!*/>();
- List<Statement> hints = new List<Statement>();
- List<BinaryExpr.Opcode?> customOps = new List<BinaryExpr.Opcode?>();
+ var lines = new List<Expression/*!*/>();
+ var hints = new List<BlockStmt/*!*/>();
+ var customOps = new List<BinaryExpr.Opcode?>();
BinaryExpr.Opcode? maybeOp;
Expression/*!*/ e;
- BlockStmt/*!*/ block;
- Statement/*!*/ h;
- IToken bodyStart, bodyEnd, opTok;
+ BlockStmt/*!*/ h;
+ IToken opTok;
.)
"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); .)
- )
+ {
+ Hint<out h> (. hints.Add(h); .)
( 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
@@ -1280,6 +1276,20 @@ CalcOp<out IToken x, out BinaryExpr.Opcode/*!*/ op> .)
)
.
+Hint<out BlockStmt s>
+= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); // returns an empty block statement if the hint is empty
+ var subhints = new List<Statement/*!*/>();
+ IToken bodyStart, bodyEnd;
+ BlockStmt/*!*/ block;
+ Statement/*!*/ calc;
+ Token x = la;
+ .)
+ { BlockStmt<out block, out bodyStart, out bodyEnd> (. subhints.Add(block); .)
+ | CalcStmt<out calc> (. subhints.Add(calc); .)
+ }
+ (. s = new BlockStmt(x, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container
+ .)
+ .
/*------------------------------------------------------------------------*/
Expression<out Expression/*!*/ e>
=
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index 36fadb07..6ae273b6 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -2666,7 +2666,7 @@ namespace Microsoft.Dafny { {
public readonly BinaryExpr.Opcode/*!*/ Op; // main operator of the calculation
public readonly List<Expression/*!*/> Lines;
- public readonly List<Statement> Hints; // Hints[i] comes after line i; null denotes an empty hint
+ public readonly List<BlockStmt/*!*/> Hints; // Hints[i] comes after line i; block statement is used as a container for multiple sub-hints
public readonly List<BinaryExpr.Opcode?> CustomOps; // CustomOps[i] comes after line i; null denotes the absence of a custom operator
public readonly List<BinaryExpr/*!*/> Steps; // expressions li op l<i + 1>, filled in during resolution in order to get the correct op
public BinaryExpr Result; // expression l0 op ln, filled in during resolution in order to get the correct op
@@ -2685,7 +2685,7 @@ namespace Microsoft.Dafny { Contract.Invariant(CustomOps.Count == Hints.Count);
}
- public CalcStmt(IToken tok, BinaryExpr.Opcode/*!*/ op, List<Expression/*!*/> lines, List<Statement> hints, List<BinaryExpr.Opcode?> customOps)
+ public CalcStmt(IToken tok, BinaryExpr.Opcode/*!*/ op, List<Expression/*!*/> lines, List<BlockStmt/*!*/> hints, List<BinaryExpr.Opcode?> customOps)
: base(tok)
{
Contract.Requires(tok != null);
@@ -2694,6 +2694,7 @@ namespace Microsoft.Dafny { Contract.Requires(hints != null);
Contract.Requires(customOps != null);
Contract.Requires(cce.NonNullElements(lines));
+ Contract.Requires(cce.NonNullElements(hints));
Contract.Requires(hints.Count == Math.Max(lines.Count - 1, 0));
Contract.Requires(customOps.Count == hints.Count);
this.Op = op;
@@ -2708,7 +2709,7 @@ namespace Microsoft.Dafny { {
get {
foreach (var h in Hints) {
- if (h != null) yield return h;
+ yield return h;
}
}
}
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index e255a317..ff45ecf0 100644 --- a/Dafny/Parser.cs +++ b/Dafny/Parser.cs @@ -1620,14 +1620,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x;
BinaryExpr.Opcode op, calcOp = BinaryExpr.Opcode.Eq, resOp = BinaryExpr.Opcode.Eq;
- List<Expression/*!*/> lines = new List<Expression/*!*/>();
- List<Statement> hints = new List<Statement>();
- List<BinaryExpr.Opcode?> customOps = new List<BinaryExpr.Opcode?>();
+ var lines = new List<Expression/*!*/>();
+ var hints = new List<BlockStmt/*!*/>();
+ var customOps = new List<BinaryExpr.Opcode?>();
BinaryExpr.Opcode? maybeOp;
Expression/*!*/ e;
- BlockStmt/*!*/ block;
- Statement/*!*/ h;
- IToken bodyStart, bodyEnd, opTok;
+ BlockStmt/*!*/ h;
+ IToken opTok;
Expect(75);
x = t;
@@ -1641,15 +1640,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo lines.Add(e);
Expect(14);
while (StartOf(15)) {
- if (la.kind == 6) {
- BlockStmt(out block, out bodyStart, out bodyEnd);
- hints.Add(block);
- } else if (la.kind == 75) {
- CalcStmt(out h);
- hints.Add(h);
- } else {
- hints.Add(null);
- }
+ Hint(out h);
+ hints.Add(h);
if (StartOf(14)) {
CalcOp(out opTok, out op);
maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(resOp, op);
@@ -2017,6 +2009,27 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo } else SynErr(173);
}
+ void Hint(out BlockStmt s) {
+ Contract.Ensures(Contract.ValueAtReturn(out s) != null); // returns an empty block statement if the hint is empty
+ var subhints = new List<Statement/*!*/>();
+ IToken bodyStart, bodyEnd;
+ BlockStmt/*!*/ block;
+ Statement/*!*/ calc;
+ Token x = la;
+
+ while (la.kind == 6 || la.kind == 75) {
+ if (la.kind == 6) {
+ BlockStmt(out block, out bodyStart, out bodyEnd);
+ subhints.Add(block);
+ } else {
+ CalcStmt(out calc);
+ subhints.Add(calc);
+ }
+ }
+ s = new BlockStmt(x, subhints); // if the hint is empty x is the first token of the next line, but it doesn't matter cause the block statement is just used as a container
+
+ }
+
void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null);
x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs index eab62134..b284f539 100644 --- a/Dafny/Printer.cs +++ b/Dafny/Printer.cs @@ -578,9 +578,9 @@ namespace Microsoft.Dafny { var e = s.Lines[i];
var h = s.Hints[i - 1];
var op = s.CustomOps[i - 1];
- if (h != null) {
+ foreach (var st in h.Body) {
Indent(lineInd);
- PrintStatement(h, lineInd);
+ PrintStatement(st, lineInd);
wr.WriteLine();
}
Indent(lineInd);
diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs index 0876d0eb..ecb53bd5 100644 --- a/Dafny/Resolver.cs +++ b/Dafny/Resolver.cs @@ -3160,11 +3160,8 @@ namespace Microsoft.Dafny }
e0 = e1;
}
- foreach (var h in s.Hints)
- {
- if (h != null) {
- ResolveStatement(h, true, method);
- }
+ foreach (var h in s.Hints) {
+ ResolveStatement(h, true, method);
}
if (s.Steps.Count > 0) {
s.Result = new BinaryExpr(s.Tok, resOp, s.Lines.First(), s.Lines.Last());
diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs index 531bb51a..b4f5a4dc 100644 --- a/Dafny/Translator.cs +++ b/Dafny/Translator.cs @@ -4008,10 +4008,7 @@ namespace Microsoft.Dafny { for (int i = s.Steps.Count; 0 <= --i; ) {
var b = new Bpl.StmtListBuilder();
- var h = s.Hints[i];
- if (h != null) {
- TrStmt(h, b, locals, etran);
- }
+ TrStmt(s.Hints[i], b, locals, etran);
b.Add(Assert(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "the calculation step between the previous line and this line might not hold"));
b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
if (i == s.Steps.Count - 1) {
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy index c48f2000..1ddd8603 100644 --- a/Test/dafny2/Calculations.dfy +++ b/Test/dafny2/Calculations.dfy @@ -209,10 +209,4 @@ ghost method Window(xs: List, ys: List) length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(xs));
true;
}
-}
-
-// Empty calculations are also allowed, but they don't generate any Boogie code.
-ghost method Empty()
-{
- calc {}
-}
+}
\ No newline at end of file |