summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Cloner.cs2
-rw-r--r--Source/Dafny/Dafny.atg101
-rw-r--r--Source/Dafny/DafnyAst.cs25
-rw-r--r--Source/Dafny/Parser.cs354
-rw-r--r--Source/Dafny/Printer.cs12
-rw-r--r--Source/Dafny/Resolver.cs58
-rw-r--r--Source/Dafny/Scanner.cs68
-rw-r--r--Source/Dafny/Translator.cs53
-rw-r--r--Test/dafny0/Answer39
-rw-r--r--Test/dafny0/Calculations.dfy37
-rw-r--r--Test/dafny0/ParseErrors.dfy58
-rw-r--r--Test/dafny0/ResolutionErrors.dfy29
-rw-r--r--Test/dafny0/runtest.bat3
-rw-r--r--Test/dafny2/Calculations.dfy7
14 files changed, 543 insertions, 303 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index a5865a6f..c972c5c4 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/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/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 646d6ee4..e2d90f20 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1221,39 +1221,42 @@ 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;
- .)
- "calc" (. x = t; .)
- [ CalcOp<out opTok, out calcOp> ] (. resOp = calcOp; .)
+ BlockStmt/*!*/ h;
+ IToken opTok;
+ .)
+ "calc" (. x = t; .)
+ [ CalcOp<out opTok, out calcOp> (. maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(calcOp, calcOp); // guard against non-trasitive calcOp (like !=)
+ if (maybeOp == null) {
+ SemErr(opTok, "the main operator of a calculation must be transitive");
+ }
+ 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); .)
";"
- }
+ {
+ 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
+ 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); .)
.
@@ -1262,23 +1265,33 @@ CalcOp<out IToken x, out BinaryExpr.Opcode/*!*/ op>
op = BinaryExpr.Opcode.Eq; // Returns Eq if parsing fails because it is compatible with any other operator
x = null;
.)
- ( RelOp<out x, out op> (. if (op == BinaryExpr.Opcode.Add) {
- // Parsing of RelOp failed, do not report an error again and return Eq
- op = BinaryExpr.Opcode.Eq;
- } else if (!Microsoft.Dafny.CalcStmt.ValidOp(op)) {
- // Invalid operator: resport an error and return Eq
- SemErr(x, "this operator is not allowed in calculations");
- op = BinaryExpr.Opcode.Eq;
- }
- .)
- | EquivOp (. op = BinaryExpr.Opcode.Iff;
- x = t;
- .)
- | ImpliesOp (. op = BinaryExpr.Opcode.Imp;
- x = t;
- .)
+ ( "==" (. x = t; op = BinaryExpr.Opcode.Eq; .)
+ | "<" (. x = t; op = BinaryExpr.Opcode.Lt; .)
+ | ">" (. x = t; op = BinaryExpr.Opcode.Gt; .)
+ | "<=" (. x = t; op = BinaryExpr.Opcode.Le; .)
+ | ">=" (. x = t; op = BinaryExpr.Opcode.Ge; .)
+ | "!=" (. x = t; op = BinaryExpr.Opcode.Neq; .)
+ | '\u2260' (. x = t; op = BinaryExpr.Opcode.Neq; .)
+ | '\u2264' (. x = t; op = BinaryExpr.Opcode.Le; .)
+ | '\u2265' (. x = t; op = BinaryExpr.Opcode.Ge; .)
+ | EquivOp (. x = t; op = BinaryExpr.Opcode.Iff; .)
+ | ImpliesOp (. x = t; op = BinaryExpr.Opcode.Imp; .)
)
.
+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/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 36f0aace..84154174 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<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; // 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,22 @@ 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?
+ public CalcStmt(IToken tok, BinaryExpr.Opcode/*!*/ op, List<Expression/*!*/> lines, List<BlockStmt/*!*/> hints, List<BinaryExpr.Opcode?> customOps)
: 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(cce.NonNullElements(hints));
+ 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;
@@ -2711,7 +2709,7 @@ namespace Microsoft.Dafny {
{
get {
foreach (var h in Hints) {
- if (h != null) yield return h;
+ yield return h;
}
}
}
@@ -2730,6 +2728,7 @@ namespace Microsoft.Dafny {
[Pure]
public static bool ValidOp(BinaryExpr.Opcode op) {
return op == BinaryExpr.Opcode.Eq || op == BinaryExpr.Opcode.Lt || op == BinaryExpr.Opcode.Le || op == BinaryExpr.Opcode.Gt || op == BinaryExpr.Opcode.Ge
+ || op == BinaryExpr.Opcode.Neq
|| op == BinaryExpr.Opcode.Iff || op == BinaryExpr.Opcode.Imp;
}
@@ -2739,6 +2738,8 @@ namespace Microsoft.Dafny {
[Pure]
private static bool Subsumes(BinaryExpr.Opcode op1, BinaryExpr.Opcode op2) {
Contract.Requires(ValidOp(op1) && ValidOp(op2));
+ if (op1 == BinaryExpr.Opcode.Neq || op2 == BinaryExpr.Opcode.Neq)
+ return op2 == BinaryExpr.Opcode.Eq;
if (op1 == op2)
return true;
if (op1 == BinaryExpr.Opcode.Iff || op1 == BinaryExpr.Opcode.Imp || op2 == BinaryExpr.Opcode.Iff || op2 == BinaryExpr.Opcode.Imp)
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 3a310cd9..61af3111 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1620,52 +1620,51 @@ 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;
if (StartOf(14)) {
CalcOp(out opTok, out calcOp);
+ maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(calcOp, calcOp); // guard against non-trasitive calcOp (like !=)
+ if (maybeOp == null) {
+ SemErr(opTok, "the main operator of a calculation must be transitive");
+ }
+ resOp = calcOp;
+
}
- 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)) {
+ Hint(out h);
+ hints.Add(h);
+ 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);
@@ -1991,35 +1990,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
op = BinaryExpr.Opcode.Eq; // Returns Eq if parsing fails because it is compatible with any other operator
x = null;
- if (StartOf(19)) {
- RelOp(out x, out op);
- if (op == BinaryExpr.Opcode.Add) {
- // Parsing of RelOp failed, do not report an error again and return Eq
- op = BinaryExpr.Opcode.Eq;
- } else if (!Microsoft.Dafny.CalcStmt.ValidOp(op)) {
- // Invalid operator: resport an error and return Eq
- SemErr(x, "this operator is not allowed in calculations");
- op = BinaryExpr.Opcode.Eq;
- }
-
- } else if (la.kind == 76 || la.kind == 77) {
- EquivOp();
- op = BinaryExpr.Opcode.Iff;
- x = t;
-
- } else if (la.kind == 78 || la.kind == 79) {
- ImpliesOp();
- op = BinaryExpr.Opcode.Imp;
- x = t;
-
- } else SynErr(173);
- }
-
- void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
- Contract.Ensures(Contract.ValueAtReturn(out x) != null);
- x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
- IToken y;
-
switch (la.kind) {
case 27: {
Get();
@@ -2036,88 +2006,91 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 84: {
+ case 76: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 85: {
+ case 77: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 86: {
+ case 78: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 87: {
+ case 79: {
Get();
- x = t; op = BinaryExpr.Opcode.Disjoint;
+ x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 88: {
+ case 80: {
Get();
- x = t; op = BinaryExpr.Opcode.In;
+ x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 89: {
+ case 81: {
Get();
- x = t; y = Token.NoToken;
- if (la.kind == 88) {
- Get();
- y = t;
- }
- if (y == Token.NoToken) {
- SemErr(x, "invalid RelOp");
- } else if (y.pos != x.pos + 1) {
- SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)");
- } else {
- x.val = "!in";
- op = BinaryExpr.Opcode.NotIn;
- }
-
+ x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 90: {
- Get();
- x = t; op = BinaryExpr.Opcode.Neq;
+ case 82: case 83: {
+ EquivOp();
+ x = t; op = BinaryExpr.Opcode.Iff;
break;
}
- case 91: {
- Get();
- x = t; op = BinaryExpr.Opcode.Le;
+ case 84: case 85: {
+ ImpliesOp();
+ x = t; op = BinaryExpr.Opcode.Imp;
break;
}
- case 92: {
- Get();
- x = t; op = BinaryExpr.Opcode.Ge;
- break;
+ default: SynErr(173); break;
}
- default: SynErr(174); break;
+ }
+
+ 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 EquivOp() {
- if (la.kind == 76) {
+ if (la.kind == 82) {
Get();
- } else if (la.kind == 77) {
+ } else if (la.kind == 83) {
Get();
- } else SynErr(175);
+ } else SynErr(174);
}
void ImpliesOp() {
- if (la.kind == 78) {
+ if (la.kind == 84) {
Get();
- } else if (la.kind == 79) {
+ } else if (la.kind == 85) {
Get();
- } else SynErr(176);
+ } else SynErr(175);
}
void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpression(out e0);
- while (la.kind == 76 || la.kind == 77) {
+ while (la.kind == 82 || la.kind == 83) {
EquivOp();
x = t;
ImpliesExpression(out e1);
@@ -2128,7 +2101,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void ImpliesExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0);
- if (la.kind == 78 || la.kind == 79) {
+ if (la.kind == 84 || la.kind == 85) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -2139,13 +2112,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
void LogicalExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
- if (StartOf(20)) {
- if (la.kind == 80 || la.kind == 81) {
+ if (StartOf(19)) {
+ if (la.kind == 86 || la.kind == 87) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 80 || la.kind == 81) {
+ while (la.kind == 86 || la.kind == 87) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -2156,7 +2129,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Or, e0, e1);
- while (la.kind == 82 || la.kind == 83) {
+ while (la.kind == 88 || la.kind == 89) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -2180,7 +2153,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
Term(out e0);
e = e0;
- if (StartOf(19)) {
+ if (StartOf(20)) {
RelOp(out x, out op);
firstOpTok = x;
Term(out e1);
@@ -2188,7 +2161,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
if (op == BinaryExpr.Opcode.Disjoint)
acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.
- while (StartOf(19)) {
+ while (StartOf(20)) {
if (chain == null) {
chain = new List<Expression>();
ops = new List<BinaryExpr.Opcode>();
@@ -2257,19 +2230,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void AndOp() {
- if (la.kind == 80) {
+ if (la.kind == 86) {
Get();
- } else if (la.kind == 81) {
+ } else if (la.kind == 87) {
Get();
- } else SynErr(177);
+ } else SynErr(176);
}
void OrOp() {
- if (la.kind == 82) {
+ if (la.kind == 88) {
Get();
- } else if (la.kind == 83) {
+ } else if (la.kind == 89) {
Get();
- } else SynErr(178);
+ } else SynErr(177);
}
void Term(out Expression/*!*/ e0) {
@@ -2282,6 +2255,89 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
}
+ void RelOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {
+ Contract.Ensures(Contract.ValueAtReturn(out x) != null);
+ x = Token.NoToken; op = BinaryExpr.Opcode.Add/*(dummy)*/;
+ IToken y;
+
+ switch (la.kind) {
+ case 27: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Eq;
+ break;
+ }
+ case 29: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Lt;
+ break;
+ }
+ case 30: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Gt;
+ break;
+ }
+ case 76: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Le;
+ break;
+ }
+ case 77: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Ge;
+ break;
+ }
+ case 78: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Neq;
+ break;
+ }
+ case 90: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Disjoint;
+ break;
+ }
+ case 91: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.In;
+ break;
+ }
+ case 92: {
+ Get();
+ x = t; y = Token.NoToken;
+ if (la.kind == 91) {
+ Get();
+ y = t;
+ }
+ if (y == Token.NoToken) {
+ SemErr(x, "invalid RelOp");
+ } else if (y.pos != x.pos + 1) {
+ SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)");
+ } else {
+ x.val = "!in";
+ op = BinaryExpr.Opcode.NotIn;
+ }
+
+ break;
+ }
+ case 79: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Neq;
+ break;
+ }
+ case 80: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Le;
+ break;
+ }
+ case 81: {
+ Get();
+ x = t; op = BinaryExpr.Opcode.Ge;
+ break;
+ }
+ default: SynErr(178); break;
+ }
+ }
+
void Factor(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1; BinaryExpr.Opcode op;
UnaryExpression(out e0);
@@ -2313,7 +2369,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
e = new BinaryExpr(x, BinaryExpr.Opcode.Sub, new LiteralExpr(x, 0), e);
break;
}
- case 89: case 97: {
+ case 92: case 97: {
NegOp();
x = t;
UnaryExpression(out e);
@@ -2386,7 +2442,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
void NegOp() {
- if (la.kind == 89) {
+ if (la.kind == 92) {
Get();
} else if (la.kind == 97) {
Get();
@@ -2937,22 +2993,22 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,T,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,T,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, x,T,x,x, x,T,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,T,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{T,T,T,x, x,x,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, T,x,x,x, x,T,x,x, x,T,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,T, T,T,T,T, x,x,x,x, T,T,T,T, T,T,T,T, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
- {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,T,x, x,x,x,x, T,T,T,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,T, T,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
+ {x,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, T,x,T,x, x,x,x,x, T,T,T,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},
{x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,x,x,x, x,x,T,x, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,x,T, x,x,T,T, T,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x},
{x,x,x,x, x,x,T,T, x,x,x,x, x,x,T,x, x,T,x,x, x,x,T,x, T,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,T,x,x, x,x,T,T, x,x,T,T, T,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,T, T,x,x,x, x,x,x,x, T,T,x,x, x,x,T,T, x,x},
- {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}
+ {x,T,T,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,T,x, x,x,x,x, x,x,T,x, x,x,x,x, T,x,T,x, x,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x}
};
} // end Parser
@@ -3053,23 +3109,23 @@ public class Errors {
case 73: s = "\"print\" expected"; break;
case 74: s = "\"parallel\" expected"; break;
case 75: s = "\"calc\" expected"; break;
- case 76: s = "\"<==>\" expected"; break;
- case 77: s = "\"\\u21d4\" expected"; break;
- case 78: s = "\"==>\" expected"; break;
- case 79: s = "\"\\u21d2\" expected"; break;
- case 80: s = "\"&&\" expected"; break;
- case 81: s = "\"\\u2227\" expected"; break;
- case 82: s = "\"||\" expected"; break;
- case 83: s = "\"\\u2228\" expected"; break;
- case 84: s = "\"<=\" expected"; break;
- case 85: s = "\">=\" expected"; break;
- case 86: s = "\"!=\" expected"; break;
- case 87: s = "\"!!\" expected"; break;
- case 88: s = "\"in\" expected"; break;
- case 89: s = "\"!\" expected"; break;
- case 90: s = "\"\\u2260\" expected"; break;
- case 91: s = "\"\\u2264\" expected"; break;
- case 92: s = "\"\\u2265\" expected"; break;
+ case 76: s = "\"<=\" expected"; break;
+ case 77: s = "\">=\" expected"; break;
+ case 78: s = "\"!=\" expected"; break;
+ case 79: s = "\"\\u2260\" expected"; break;
+ case 80: s = "\"\\u2264\" expected"; break;
+ case 81: s = "\"\\u2265\" expected"; break;
+ case 82: s = "\"<==>\" expected"; break;
+ case 83: s = "\"\\u21d4\" expected"; break;
+ case 84: s = "\"==>\" expected"; break;
+ case 85: s = "\"\\u21d2\" expected"; break;
+ case 86: s = "\"&&\" expected"; break;
+ case 87: s = "\"\\u2227\" expected"; break;
+ case 88: s = "\"||\" expected"; break;
+ case 89: s = "\"\\u2228\" expected"; break;
+ case 90: s = "\"!!\" expected"; break;
+ case 91: s = "\"in\" expected"; break;
+ case 92: s = "\"!\" expected"; break;
case 93: s = "\"+\" expected"; break;
case 94: s = "\"-\" expected"; break;
case 95: s = "\"/\" expected"; break;
@@ -3151,11 +3207,11 @@ public class Errors {
case 171: s = "this symbol not expected in Invariant"; break;
case 172: s = "invalid AttributeArg"; break;
case 173: s = "invalid CalcOp"; break;
- case 174: s = "invalid RelOp"; break;
- case 175: s = "invalid EquivOp"; break;
- case 176: s = "invalid ImpliesOp"; break;
- case 177: s = "invalid AndOp"; break;
- case 178: s = "invalid OrOp"; break;
+ case 174: s = "invalid EquivOp"; break;
+ case 175: s = "invalid ImpliesOp"; break;
+ case 176: s = "invalid AndOp"; break;
+ case 177: s = "invalid OrOp"; break;
+ case 178: s = "invalid RelOp"; break;
case 179: s = "invalid AddOp"; break;
case 180: s = "invalid UnaryExpression"; break;
case 181: s = "invalid UnaryExpression"; break;
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 2051a54e..b284f539 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -569,16 +569,18 @@ 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];
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/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index a2710c38..d5aef85c 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3134,41 +3134,43 @@ 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 lines in a calculation 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) {
+ foreach (var h in s.Hints) {
ResolveStatement(h, true, method);
}
+ if (prevErrorCount == ErrorCount && s.Steps.Count > 0) {
+ // do not build Result if there were errors, as it might be ill-typed and produce unnecessary resolution errors
+ 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/Scanner.cs b/Source/Dafny/Scanner.cs
index 936f699c..8de52992 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -274,15 +274,15 @@ public class Scanner {
start[96] = 25;
start[91] = 28;
start[93] = 29;
- start[8660] = 33;
- start[8658] = 35;
- start[38] = 36;
- start[8743] = 38;
- start[8744] = 40;
start[33] = 62;
- start[8800] = 44;
- start[8804] = 45;
- start[8805] = 46;
+ start[8800] = 33;
+ start[8804] = 34;
+ start[8805] = 35;
+ start[8660] = 38;
+ start[8658] = 40;
+ start[38] = 41;
+ start[8743] = 43;
+ start[8744] = 45;
start[43] = 47;
start[45] = 48;
start[47] = 49;
@@ -538,7 +538,7 @@ public class Scanner {
case "print": t.kind = 73; break;
case "parallel": t.kind = 74; break;
case "calc": t.kind = 75; break;
- case "in": t.kind = 88; break;
+ case "in": t.kind = 91; break;
case "false": t.kind = 98; break;
case "true": t.kind = 99; break;
case "null": t.kind = 100; break;
@@ -677,39 +677,39 @@ public class Scanner {
case 30:
{t.kind = 68; break;}
case 31:
- if (ch == '>') {AddCh(); goto case 32;}
- else {goto case 0;}
+ {t.kind = 77; break;}
case 32:
- {t.kind = 76; break;}
+ {t.kind = 78; break;}
case 33:
- {t.kind = 77; break;}
+ {t.kind = 79; break;}
case 34:
- {t.kind = 78; break;}
+ {t.kind = 80; break;}
case 35:
- {t.kind = 79; break;}
+ {t.kind = 81; break;}
case 36:
- if (ch == '&') {AddCh(); goto case 37;}
+ if (ch == '>') {AddCh(); goto case 37;}
else {goto case 0;}
case 37:
- {t.kind = 80; break;}
+ {t.kind = 82; break;}
case 38:
- {t.kind = 81; break;}
+ {t.kind = 83; break;}
case 39:
- {t.kind = 82; break;}
+ {t.kind = 84; break;}
case 40:
- {t.kind = 83; break;}
- case 41:
{t.kind = 85; break;}
+ case 41:
+ if (ch == '&') {AddCh(); goto case 42;}
+ else {goto case 0;}
case 42:
{t.kind = 86; break;}
case 43:
{t.kind = 87; break;}
case 44:
- {t.kind = 90; break;}
+ {t.kind = 88; break;}
case 45:
- {t.kind = 91; break;}
+ {t.kind = 89; break;}
case 46:
- {t.kind = 92; break;}
+ {t.kind = 90; break;}
case 47:
{t.kind = 93; break;}
case 48:
@@ -745,7 +745,7 @@ public class Scanner {
else {t.kind = 17; break;}
case 59:
recEnd = pos; recKind = 22;
- if (ch == '|') {AddCh(); goto case 39;}
+ if (ch == '|') {AddCh(); goto case 44;}
else {t.kind = 22; break;}
case 60:
recEnd = pos; recKind = 29;
@@ -753,25 +753,25 @@ public class Scanner {
else {t.kind = 29; break;}
case 61:
recEnd = pos; recKind = 30;
- if (ch == '=') {AddCh(); goto case 41;}
+ if (ch == '=') {AddCh(); goto case 31;}
else {t.kind = 30; break;}
case 62:
- recEnd = pos; recKind = 89;
- if (ch == '=') {AddCh(); goto case 42;}
- else if (ch == '!') {AddCh(); goto case 43;}
- else {t.kind = 89; break;}
+ recEnd = pos; recKind = 92;
+ if (ch == '=') {AddCh(); goto case 32;}
+ else if (ch == '!') {AddCh(); goto case 46;}
+ else {t.kind = 92; break;}
case 63:
recEnd = pos; recKind = 27;
- if (ch == '>') {AddCh(); goto case 34;}
+ if (ch == '>') {AddCh(); goto case 39;}
else {t.kind = 27; break;}
case 64:
recEnd = pos; recKind = 105;
if (ch == '.') {AddCh(); goto case 23;}
else {t.kind = 105; break;}
case 65:
- recEnd = pos; recKind = 84;
- if (ch == '=') {AddCh(); goto case 31;}
- else {t.kind = 84; break;}
+ recEnd = pos; recKind = 76;
+ if (ch == '=') {AddCh(); goto case 36;}
+ else {t.kind = 76; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 9bd16f3f..ccc9ff4f 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -3986,11 +3986,13 @@ namespace Microsoft.Dafny {
} else if (stmt is CalcStmt) {
/* Translate into:
if (*) {
+ // line well-formedness checks;
+ } else if (*) {
hint0;
assert t0 op t1;
assume false;
- } else if ...
- } else {
+ } else if (*) { ...
+ } else if (*) {
hint<n-1>;
assert t<n-1> op tn;
assume false;
@@ -4000,33 +4002,40 @@ namespace Microsoft.Dafny {
var s = (CalcStmt)stmt;
Contract.Assert(s.Steps.Count == s.Hints.Count); // established by the resolver
AddComment(builder, stmt, "calc statement");
- // NadiaTodo: check well-formedness of lines
- if (s.Steps.Count > 0) {
+ if (s.Lines.Count > 0) {
Bpl.IfCmd ifCmd = null;
- Bpl.StmtList els = null;
-
+ Bpl.StmtListBuilder b;
+ // check steps:
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);
- }
- b.Add(Assert(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "this calculation step might not hold"));
- b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
- if (i == s.Steps.Count - 1) {
- // first iteration (last step)
- els = b.Collect(s.Tok);
+ b = new Bpl.StmtListBuilder();
+ TrStmt(s.Hints[i], b, locals, etran);
+ bool splitHappened;
+ var ss = TrSplitExpr(s.Steps[i], etran, out splitHappened);
+ if (!splitHappened) {
+ b.Add(AssertNS(s.Lines[i + 1].tok, etran.TrExpr(s.Steps[i]), "the calculation step between the previous line and this line might not hold"));
} else {
- ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, els);
- els = null;
+ foreach (var split in ss) {
+ if (!split.IsFree) {
+ b.Add(AssertNS(s.Lines[i + 1].tok, split.E, "the calculation step between the previous line and this line might not hold"));
+ }
+ }
}
+ b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
+ ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null);
}
- if (ifCmd == null) {
- // single step: generate an if without else parts
- ifCmd = new Bpl.IfCmd(s.Tok, null, els, null, null);
+ // check well-formedness of lines:
+ b = new Bpl.StmtListBuilder();
+ foreach (var e in s.Lines) {
+ TrStmt_CheckWellformed(e, b, locals, etran, false);
}
+ b.Add(new Bpl.AssumeCmd(s.Tok, Bpl.Expr.False));
+ ifCmd = new Bpl.IfCmd(s.Tok, null, b.Collect(s.Tok), ifCmd, null);
builder.Add(ifCmd);
- builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Result)));
+ // assume result:
+ if (s.Steps.Count > 0) {
+ Contract.Assert(s.Result != null); // established by the resolver
+ builder.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Result)));
+ }
}
} else if (stmt is MatchStmt) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 2cd923f9..571377e8 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -542,7 +542,16 @@ ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specificat
ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
-48 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(363,4): Error: arguments to + must be int or a collection type (instead got bool)
+ResolutionErrors.dfy(368,4): Error: all lines in a calculation must have the same type (got int after bool)
+ResolutionErrors.dfy(371,4): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(371,4): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(372,8): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(372,8): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(377,8): Error: first argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(377,8): Error: second argument to ==> must be of type bool (instead got int)
+ResolutionErrors.dfy(382,4): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+57 resolution/type errors detected in ResolutionErrors.dfy
-------------------- ParseErrors.dfy --------------------
ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator
@@ -553,7 +562,13 @@ ParseErrors.dfy(15,18): error: this operator cannot be part of a chain
ParseErrors.dfy(16,19): error: this operator cannot be part of a chain
ParseErrors.dfy(17,18): error: this operator cannot be part of a chain
ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator
-8 parse errors detected in ParseErrors.dfy
+ParseErrors.dfy(46,8): error: the main operator of a calculation must be transitive
+ParseErrors.dfy(62,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(63,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(68,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(69,2): error: this operator cannot continue this calculation
+ParseErrors.dfy(75,2): error: this operator cannot continue this calculation
+14 parse errors detected in ParseErrors.dfy
-------------------- Array.dfy --------------------
Array.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
@@ -1615,6 +1630,26 @@ TailCalls.dfy(42,12): Error: 'decreases *' is allowed only on tail-recursive met
TailCalls.dfy(64,12): Error: 'decreases *' is allowed only on tail-recursive methods
5 resolution/type errors detected in TailCalls.dfy
+-------------------- Calculations.dfy --------------------
+Calculations.dfy(3,4): Error: index out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon11_Then
+Calculations.dfy(8,13): Error: index out of range
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+Calculations.dfy(8,17): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+Calculations.dfy(36,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Calculations.dfy(31,2): anon5_Else
+
+Dafny program verifier finished with 4 verified, 4 errors
+
-------------------- Superposition.dfy --------------------
Verifying CheckWellformed$$_0_M0.C.M ...
diff --git a/Test/dafny0/Calculations.dfy b/Test/dafny0/Calculations.dfy
new file mode 100644
index 00000000..9e44f62e
--- /dev/null
+++ b/Test/dafny0/Calculations.dfy
@@ -0,0 +1,37 @@
+method CalcTest0(s: seq<int>) {
+ calc {
+ s[0]; // error: ill-formed line
+ }
+
+ calc {
+ 2;
+ { assert s[0] == 1; } // error: ill-formed hint
+ 1 + 1;
+ }
+
+ if (|s| > 0) {
+ calc {
+ s[0]; // OK: well-formed in this context
+ { assert s[0] == s[0]; }
+ <= s[0];
+ }
+ }
+}
+
+method CalcTest1(x: int, y: int) {
+ calc {
+ x + y;
+ { assume x == 0; }
+ y;
+ }
+ assert x == 0; // OK: follows from x + y == y;
+}
+
+method CalcTest2(x: int, y: int) {
+ calc {
+ x + y;
+ { assume x == 0; }
+ y + x;
+ }
+ assert x == 0; // error: even though assumed above, is not exported by the calculation
+} \ No newline at end of file
diff --git a/Test/dafny0/ParseErrors.dfy b/Test/dafny0/ParseErrors.dfy
index 41df50eb..9a3cc18b 100644
--- a/Test/dafny0/ParseErrors.dfy
+++ b/Test/dafny0/ParseErrors.dfy
@@ -18,3 +18,61 @@ method TestChaining1<T>(s: set<T>, t: set<T>, u: set<T>, x: T, SuperSet: set<set
ensures x in s == t; // error: 'in' is not chaining
{
}
+
+// ---------------------- calc statements -----------------------------------
+
+method TestCalc()
+{
+ calc {} // OK, empty calculations are allowed
+ calc {
+ 2 + 3; // OK, single-line calculations are allowed
+ }
+ calc {
+ 2 + 3;
+ calc { // OK: a calc statement is allowed as a sub-hint
+ 2;
+ 1 + 1;
+ }
+ calc {
+ 3;
+ 1 + 2;
+ }
+ { assert true; } // OK: multiple subhints are allowed between two lines
+ 1 + 1 + 1 + 2;
+ { assert 1 + 1 + 1 == 3; }
+ { assert true; }
+ 3 + 2;
+ }
+ calc != { // error: != is not allowed as the main operator of a calculation
+ 2 + 3;
+ 4;
+ }
+ calc { // OK, these operators are compatible
+ 2 + 3;
+ > 4;
+ >= 2 + 2;
+ }
+ calc < { // OK, these operators are compatible
+ 2 + 3;
+ == 5;
+ <= 3 + 3;
+ }
+ calc < { // error: cannot mix < and >= or >
+ 2 + 3;
+ >= 5;
+ > 2 + 2;
+ 6;
+ }
+ calc >= { // error: cannot mix >= and <= or !=
+ 2 + 3;
+ <= 5;
+ != 2 + 2;
+ 3;
+ }
+ calc { // error: cannot have more than one != per calc
+ 2 + 3;
+ != 4;
+ != 1 + 2;
+ 3;
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 274cc95a..c615c5ec 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -354,3 +354,32 @@ method MG1(l: GList, n: nat)
var t := GCons(100, GNil);
t := GCons(120, l); // error: types don't match up (List<T$0> versus List<int>)
}
+
+// ------------------- calc statements ------------------------------
+
+method TestCalc(m: int, n: int, a: bool, b: bool)
+{
+ calc {
+ a + b; // error: invalid line
+ n + m;
+ }
+ calc {
+ a && b;
+ n + m; // error: all lines must have the same type
+ }
+ calc ==> {
+ n + m; // error: ==> operator requires boolean lines
+ n + m + 1;
+ n + m + 2;
+ }
+ calc {
+ n + m;
+ n + m + 1;
+ ==> n + m + 2; // error: ==> operator requires boolean lines
+ }
+ calc {
+ n + m;
+ { print n + m; } // error: non-ghost statements are not allowed in hints
+ m + n;
+ }
+}
diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index 2055e283..23dc20e0 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -23,7 +23,8 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy
ReturnErrors.dfy ReturnTests.dfy ChainingDisjointTests.dfy
CallStmtTests.dfy MultiSets.dfy PredExpr.dfy LetExpr.dfy
Predicates.dfy Skeletons.dfy Maps.dfy LiberalEquality.dfy
- RefinementModificationChecking.dfy TailCalls.dfy) do (
+ RefinementModificationChecking.dfy TailCalls.dfy
+ Calculations.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 /print:out.bpl.tmp /dprint:out.dfy.tmp %* %%f
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
index 8e3a4426..8c13457b 100644
--- a/Test/dafny2/Calculations.dfy
+++ b/Test/dafny2/Calculations.dfy
@@ -80,10 +80,7 @@ ghost method Lemma_Revacc_calc(xs: List, ys: List)
concat(revacc(xrest, Cons(x, Nil)), ys);
{ Lemma_RevCatCommute(); } // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)
revacc(xrest, concat(Cons(x, Nil), ys));
- {
- assert forall g, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);
- assert concat(Cons(x, Nil), ys) == Cons(x, ys);
- }
+ // def. concat (x2)
revacc(xrest, Cons(x, ys));
// def. revacc
revacc(xs, ys);
@@ -209,4 +206,4 @@ ghost method Window(xs: List, ys: List)
length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(xs));
true;
}
-}
+} \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 19:13:08 +0000