diff options
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 45 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 17 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 56 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 8 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 62 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 1 |
6 files changed, 98 insertions, 91 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); .)
.
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 36f0aace..36fadb07 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -2666,10 +2666,10 @@ 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 an empty hint
+ public readonly List<Statement> Hints; // Hints[i] comes after line i; null denotes an empty hint
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; // expressions l0 op ln, 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
public static readonly BinaryExpr.Opcode/*!*/ DefaultOp = BinaryExpr.Opcode.Eq;
@@ -2681,24 +2681,21 @@ namespace Microsoft.Dafny { Contract.Invariant(Hints != null);
Contract.Invariant(CustomOps != null);
Contract.Invariant(Steps != null);
- Contract.Invariant(Lines.Count > 0);
- Contract.Invariant(Hints.Count == Lines.Count - 1);
- Contract.Invariant(CustomOps.Count == Lines.Count - 1);
+ Contract.Invariant(Hints.Count == Math.Max(Lines.Count - 1, 0));
+ Contract.Invariant(CustomOps.Count == Hints.Count);
}
public CalcStmt(IToken tok, BinaryExpr.Opcode/*!*/ op, List<Expression/*!*/> lines, List<Statement> hints, List<BinaryExpr.Opcode?> customOps)
- // Attributes attrs?
: base(tok)
{
Contract.Requires(tok != null);
Contract.Requires(ValidOp(op));
Contract.Requires(lines != null);
- Contract.Requires(cce.NonNullElements(lines));
Contract.Requires(hints != null);
- Contract.Requires(lines.Count > 0);
- Contract.Requires(hints.Count == lines.Count - 1);
Contract.Requires(customOps != null);
- Contract.Requires(customOps.Count == lines.Count - 1);
+ Contract.Requires(cce.NonNullElements(lines));
+ Contract.Requires(hints.Count == Math.Max(lines.Count - 1, 0));
+ Contract.Requires(customOps.Count == hints.Count);
this.Op = op;
this.Lines = lines;
this.Hints = hints;
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index 3a310cd9..e255a317 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1636,36 +1636,38 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
resOp = calcOp;
Expect(6);
- Expression(out e);
- 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);
- }
- if (StartOf(14)) {
- 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;
- }
-
- } else if (StartOf(10)) {
- customOps.Add(null);
- } else SynErr(162);
+ if (StartOf(10)) {
Expression(out e);
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);
+ }
+ if (StartOf(14)) {
+ 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;
+ }
+
+ } else if (StartOf(10)) {
+ customOps.Add(null);
+ } else SynErr(162);
+ Expression(out e);
+ lines.Add(e);
+ Expect(14);
+ }
}
Expect(7);
s = new CalcStmt(x, calcOp, lines, hints, customOps);
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 2051a54e..eab62134 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -569,9 +569,11 @@ namespace Microsoft.Dafny { }
wr.WriteLine("{");
int lineInd = indent + IndentAmount;
- Indent(lineInd);
- PrintExpression(s.Lines.First(), lineInd);
- wr.WriteLine(";");
+ if (s.Lines.Count > 0) {
+ Indent(lineInd);
+ PrintExpression(s.Lines.First(), lineInd);
+ wr.WriteLine(";");
+ }
for (var i = 1; i < s.Lines.Count; i++){
var e = s.Lines[i];
var h = s.Hints[i - 1];
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a2710c38..0876d0eb 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3134,41 +3134,45 @@ namespace Microsoft.Dafny var prevErrorCount = ErrorCount;
CalcStmt s = (CalcStmt)stmt;
s.IsGhost = true;
- Contract.Assert(s.Lines.Count > 0); // follows from the invariant of CalcStatement
- var resOp = s.Op;
- var e0 = s.Lines.First();
- ResolveExpression(e0, true);
- Contract.Assert(e0.Type != null); // follows from postcondition of ResolveExpression
- for (int i = 1; i < s.Lines.Count; i++) {
- var e1 = s.Lines[i];
- ResolveExpression(e1, true);
- Contract.Assert(e1.Type != null); // follows from postcondition of ResolveExpression
- if (!UnifyTypes(e0.Type, e1.Type)) {
- Error(e1, "all calculation steps must have the same type (got {0} after {1})", e1.Type, e0.Type);
- } else {
- BinaryExpr step;
- var op = s.CustomOps[i - 1];
- if (op == null) {
- step = new BinaryExpr(e0.tok, s.Op, e0, e1); // Use calc-wide operator
+ if (s.Lines.Count > 0) {
+ var resOp = s.Op;
+ var e0 = s.Lines.First();
+ ResolveExpression(e0, true);
+ Contract.Assert(e0.Type != null); // follows from postcondition of ResolveExpression
+ for (int i = 1; i < s.Lines.Count; i++) {
+ var e1 = s.Lines[i];
+ ResolveExpression(e1, true);
+ Contract.Assert(e1.Type != null); // follows from postcondition of ResolveExpression
+ if (!UnifyTypes(e0.Type, e1.Type)) {
+ Error(e1, "all calculation steps must have the same type (got {0} after {1})", e1.Type, e0.Type);
} else {
- step = new BinaryExpr(e0.tok, (BinaryExpr.Opcode)op, e0, e1); // Use custom line operator
- Contract.Assert(CalcStmt.ResultOp(resOp, (BinaryExpr.Opcode)op) != null); // This was checked during parsing
- resOp = (BinaryExpr.Opcode)CalcStmt.ResultOp(resOp, (BinaryExpr.Opcode)op);
+ BinaryExpr step;
+ var op = s.CustomOps[i - 1];
+ if (op == null) {
+ step = new BinaryExpr(e0.tok, s.Op, e0, e1); // Use calc-wide operator
+ } else {
+ step = new BinaryExpr(e0.tok, (BinaryExpr.Opcode)op, e0, e1); // Use custom line operator
+ Contract.Assert(CalcStmt.ResultOp(resOp, (BinaryExpr.Opcode)op) != null); // This was checked during parsing
+ resOp = (BinaryExpr.Opcode)CalcStmt.ResultOp(resOp, (BinaryExpr.Opcode)op);
+ }
+ ResolveExpression(step, true);
+ s.Steps.Add(step);
}
- ResolveExpression(step, true);
- s.Steps.Add(step);
+ e0 = e1;
}
- e0 = e1;
- }
- foreach (var h in s.Hints)
- {
- if (h != null) {
- ResolveStatement(h, true, method);
+ foreach (var h in s.Hints)
+ {
+ if (h != null) {
+ ResolveStatement(h, true, method);
+ }
+ }
+ if (s.Steps.Count > 0) {
+ s.Result = new BinaryExpr(s.Tok, resOp, s.Lines.First(), s.Lines.Last());
+ ResolveExpression(s.Result, true);
}
}
- s.Result = new BinaryExpr(s.Tok, resOp, s.Lines.First(), s.Lines.Last());
- ResolveExpression(s.Result, true);
Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == s.Hints.Count);
+ Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == 0 || s.Result != null);
} else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 9bd16f3f..675e62e8 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4002,6 +4002,7 @@ namespace Microsoft.Dafny { AddComment(builder, stmt, "calc statement");
// NadiaTodo: check well-formedness of lines
if (s.Steps.Count > 0) {
+ Contract.Assert(s.Result != null); // established by the resolver
Bpl.IfCmd ifCmd = null;
Bpl.StmtList els = null;
|