diff options
| -rw-r--r-- | Source/Dafny/Cloner.cs | 13 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 62 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 142 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 186 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 20 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 17 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 48 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 25 | ||||
| -rw-r--r-- | Test/dafny3/Paulson.dfy | 46 |
9 files changed, 272 insertions, 287 deletions
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs index dbbb6a40..f4b0cfaf 100644 --- a/Source/Dafny/Cloner.cs +++ b/Source/Dafny/Cloner.cs @@ -454,7 +454,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(CloneBlockStmt), new List<Nullable<BinaryExpr.Opcode>>(s.CustomOps));
+ r = new CalcStmt(Tok(s.Tok), CloneCalcOp(s.Op), s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp));
} else if (stmt is MatchStmt) {
var s = (MatchStmt)stmt;
@@ -484,6 +484,17 @@ namespace Microsoft.Dafny return r;
}
+ public CalcStmt.CalcOp CloneCalcOp(CalcStmt.CalcOp op) {
+ if (op is CalcStmt.BinaryCalcOp) {
+ return new CalcStmt.BinaryCalcOp(((CalcStmt.BinaryCalcOp) op).Op);
+ } else if (op is CalcStmt.TernaryCalcOp) {
+ return new CalcStmt.TernaryCalcOp(CloneExpr(((CalcStmt.TernaryCalcOp) op).Index));
+ } else {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
+ }
+
public void AddStmtLabels(Statement s, LList<Label> node) {
if (node != null) {
AddStmtLabels(s, node.Next);
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index f67ae73f..4509eb97 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1341,18 +1341,18 @@ ForallStmt<out Statement/*!*/ s> CalcStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x;
- BinaryExpr.Opcode op, calcOp = BinaryExpr.Opcode.Eq, resOp = BinaryExpr.Opcode.Eq;
+ CalcStmt.CalcOp/*!*/ op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;
var lines = new List<Expression/*!*/>();
var hints = new List<BlockStmt/*!*/>();
- BinaryExpr.Opcode? customOp;
- var customOps = new List<BinaryExpr.Opcode?>();
- BinaryExpr.Opcode? maybeOp;
+ CalcStmt.CalcOp stepOp;
+ var stepOps = new List<CalcStmt.CalcOp>();
+ CalcStmt.CalcOp maybeOp;
Expression/*!*/ e;
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 !=)
+ [ CalcOp<out opTok, out calcOp> (. maybeOp = calcOp.ResultOp(calcOp); // guard against non-trasitive calcOp (like !=)
if (maybeOp == null) {
SemErr(opTok, "the main operator of a calculation must be transitive");
}
@@ -1360,44 +1360,52 @@ CalcStmt<out Statement/*!*/ s> .)
]
"{"
- [ Expression<out e> (. lines.Add(e); customOp = null; .)
+ [ Expression<out e> (. lines.Add(e); stepOp = calcOp; .)
";"
{
- [ CalcOp<out opTok, out op> (. maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(resOp, op);
+ [ CalcOp<out opTok, out op> (. maybeOp = resOp.ResultOp(op);
if (maybeOp == null) {
SemErr(opTok, "this operator cannot continue this calculation");
} else {
- customOp = op;
- resOp = (BinaryExpr.Opcode)maybeOp;
+ stepOp = op;
+ resOp = maybeOp;
}
.)
- ] (. customOps.Add(customOp); .)
+ ] (. stepOps.Add(stepOp); .)
Hint<out h> (. hints.Add(h); .)
- Expression<out e> (. lines.Add(e); customOp = null; .)
+ Expression<out e> (. lines.Add(e); stepOp = calcOp; .)
";"
}
]
"}"
- (. s = new CalcStmt(x, calcOp, lines, hints, customOps); .)
+ (. s = new CalcStmt(x, calcOp, lines, hints, stepOps, resOp); .)
.
-CalcOp<out IToken x, out BinaryExpr.Opcode/*!*/ op>
-= (. Contract.Ensures(Microsoft.Dafny.CalcStmt.ValidOp(Contract.ValueAtReturn(out op)));
- op = BinaryExpr.Opcode.Eq; // Returns Eq if parsing fails because it is compatible with any other operator
+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
+ Expression k = null;
x = null;
.)
- ( "==" (. 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; .)
- | ExpliesOp (. x = t; op = BinaryExpr.Opcode.Exp; .)
+ ( "==" (. x = t; binOp = BinaryExpr.Opcode.Eq; .)
+ [ "#" "[" Expression<out k> "]" ]
+ | "<" (. x = t; binOp = BinaryExpr.Opcode.Lt; .)
+ | ">" (. x = t; binOp = BinaryExpr.Opcode.Gt; .)
+ | "<=" (. x = t; binOp = BinaryExpr.Opcode.Le; .)
+ | ">=" (. x = t; binOp = BinaryExpr.Opcode.Ge; .)
+ | "!=" (. x = t; binOp = BinaryExpr.Opcode.Neq; .)
+ | '\u2260' (. x = t; binOp = BinaryExpr.Opcode.Neq; .)
+ | '\u2264' (. x = t; binOp = BinaryExpr.Opcode.Le; .)
+ | '\u2265' (. x = t; binOp = BinaryExpr.Opcode.Ge; .)
+ | EquivOp (. x = t; binOp = BinaryExpr.Opcode.Iff; .)
+ | ImpliesOp (. x = t; binOp = BinaryExpr.Opcode.Imp; .)
+ | ExpliesOp (. x = t; binOp = BinaryExpr.Opcode.Exp; .)
)
+ (.
+ if (k == null) {
+ op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
+ } else {
+ op = new Microsoft.Dafny.CalcStmt.TernaryCalcOp(k);
+ }
+ .)
.
Hint<out BlockStmt s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); // returns an empty block statement if the hint is empty
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs index 358cb857..9de908ac 100644 --- a/Source/Dafny/DafnyAst.cs +++ b/Source/Dafny/DafnyAst.cs @@ -3049,18 +3049,23 @@ namespace Microsoft.Dafny { public class CalcStmt : Statement
{
- abstract class CalcOp {
+ public abstract class CalcOp {
/// <summary>
- /// Resulting operator x op z if x this y other z.
- /// Returns null if neither of op1 or op2 subsumes the other.
+ /// Resulting operator "x op z" if "x this y" and "y other z".
+ /// Returns null if this and other are incompatible.
/// </summary>
[Pure]
public abstract CalcOp ResultOp(CalcOp other);
+ /// <summary>
+ /// Returns an expression "line0 this line1".
+ /// </summary>
+ [Pure]
public abstract Expression StepExpr(Expression line0, Expression line1);
+
}
- class BinaryCalcOp : CalcOp {
+ public class BinaryCalcOp : CalcOp {
public readonly BinaryExpr.Opcode/*!*/ Op;
[ContractInvariantMethod]
@@ -3111,7 +3116,6 @@ namespace Microsoft.Dafny { }
public override CalcOp ResultOp(CalcOp other) {
- Contract.Requires(other != null);
if (other is BinaryCalcOp) {
var o = (BinaryCalcOp) other;
if (this.Subsumes(o)) {
@@ -3135,13 +3139,13 @@ namespace Microsoft.Dafny { public override string ToString()
{
- return Op.ToString();
+ return BinaryExpr.OpcodeString(Op);
}
+
}
- class TernaryCalcOp : CalcOp {
+ public class TernaryCalcOp : CalcOp {
public readonly Expression Index; // the only allowed ternary operator is ==#, so we only store the index
- public readonly TernaryCalcOp Prev; // when non-null, this represents ==#[min(Index, Prev.Index)]
[ContractInvariantMethod]
void ObjectInvariant()
@@ -3149,23 +3153,22 @@ namespace Microsoft.Dafny { Contract.Invariant(Index != null);
}
- public TernaryCalcOp(Expression idx) : this(idx, null) { }
-
- private TernaryCalcOp(Expression idx, TernaryCalcOp prev) {
+ public TernaryCalcOp(Expression idx) {
Contract.Requires(idx != null);
Index = idx;
- Prev = prev;
}
public override CalcOp ResultOp(CalcOp other) {
- Contract.Requires(other != null);
if (other is BinaryCalcOp) {
if (((BinaryCalcOp) other).Op == BinaryExpr.Opcode.Eq) {
return this;
}
return null;
} else if (other is TernaryCalcOp) {
- return new TernaryCalcOp(Index, (TernaryCalcOp) other); // ToDo: if we could compare expressions for syntactic equalty, we could use this here to optimize
+ var a = Index;
+ var b = ((TernaryCalcOp) other).Index;
+ var minIndex = new ITEExpr(a.tok, new BinaryExpr(a.tok, BinaryExpr.Opcode.Le, a, b), a, b);
+ return new TernaryCalcOp(minIndex); // ToDo: if we could compare expressions for syntactic equalty, we could use this here to optimize
} else {
Contract.Assert(false);
throw new cce.UnreachableException();
@@ -3179,48 +3182,53 @@ namespace Microsoft.Dafny { public override string ToString()
{
- return TernaryExpr.Opcode.PrefixEqOp.ToString();
+ return "==#";
}
+
}
- public readonly BinaryExpr.Opcode Op; // main operator of the calculation
+ public readonly CalcOp/*!*/ Op; // main operator of the calculation
public readonly List<Expression/*!*/> Lines;
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
+ public readonly List<CalcOp/*!*/> StepOps; // StepOps[i] comes after line i
+ public readonly List<Expression/*!*/> Steps; // expressions li op l<i + 1>, filled in during resolution
+ public CalcOp/*!*/ ResultOp; // conclusion operator
+ public Expression Result; // expression l0 ResultOp ln, filled in during resolution
- public static readonly BinaryExpr.Opcode/*!*/ DefaultOp = BinaryExpr.Opcode.Eq;
+ public static readonly CalcOp/*!*/ DefaultOp = new BinaryCalcOp(BinaryExpr.Opcode.Eq);
[ContractInvariantMethod]
void ObjectInvariant()
{
- Contract.Invariant(ValidOp(Op));
+ Contract.Invariant(Op != null);
Contract.Invariant(Lines != null);
Contract.Invariant(Hints != null);
- Contract.Invariant(CustomOps != null);
+ Contract.Invariant(StepOps != null);
Contract.Invariant(Steps != null);
Contract.Invariant(Hints.Count == Math.Max(Lines.Count - 1, 0));
- Contract.Invariant(CustomOps.Count == Hints.Count);
+ Contract.Invariant(StepOps.Count == Hints.Count);
}
- public CalcStmt(IToken tok, BinaryExpr.Opcode/*!*/ op, List<Expression/*!*/> lines, List<BlockStmt/*!*/> hints, List<BinaryExpr.Opcode?> customOps)
+ public CalcStmt(IToken tok, CalcOp op, List<Expression/*!*/> lines, List<BlockStmt/*!*/> hints, List<CalcOp> stepOps, CalcOp resultOp)
: base(tok)
{
Contract.Requires(tok != null);
- Contract.Requires(ValidOp(op));
+ Contract.Requires(op != null);
Contract.Requires(lines != null);
Contract.Requires(hints != null);
- Contract.Requires(customOps != null);
+ Contract.Requires(stepOps != null);
+ Contract.Requires(resultOp != null); // ToDo: we should allow null and recalculate in that case
Contract.Requires(cce.NonNullElements(lines));
Contract.Requires(cce.NonNullElements(hints));
+ Contract.Requires(cce.NonNullElements(stepOps));
Contract.Requires(hints.Count == Math.Max(lines.Count - 1, 0));
- Contract.Requires(customOps.Count == hints.Count);
+ Contract.Requires(stepOps.Count == hints.Count);
this.Op = op;
this.Lines = lines;
this.Hints = hints;
- this.CustomOps = customOps;
- this.Steps = new List<BinaryExpr>();
+ this.StepOps = stepOps;
+ this.ResultOp = resultOp;
+ this.Steps = new List<Expression>();
this.Result = null;
}
@@ -3241,74 +3249,24 @@ namespace Microsoft.Dafny { }
}
- /// <summary>
- /// The line whose well-formedness is independant from other lines.
- /// (Last line in case of explies-calculation, first line otherwise).
- /// </summary>
- public Expression InitalLine()
+ public static Expression Lhs(Expression step)
{
- Contract.Requires(Lines.Count > 0);
- Contract.Requires(Result != null); // Available after resolution
- if (Result.Op == BinaryExpr.Opcode.Exp) {
- return Lines.Last();
+ Contract.Requires(step is BinaryExpr || step is TernaryExpr);
+ if (step is BinaryExpr) {
+ return ((BinaryExpr) step).E0;
} else {
- return Lines.First();
+ return ((TernaryExpr) step).E1;
}
}
- /// <summary>
- /// Is op a valid calculation operator?
- /// </summary>
- [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
- || LogicOp(op);
- }
-
- /// <summary>
- /// Is op a valid operator only for Boolean lines?
- /// </summary>
- [Pure]
- public static bool LogicOp(BinaryExpr.Opcode op) {
- return op == BinaryExpr.Opcode.Iff || op == BinaryExpr.Opcode.Imp || op == BinaryExpr.Opcode.Exp;
- }
-
- /// <summary>
- /// Does op1 subsume op2 (i.e. forall x, y, z :: (x op1 y op2 z) || (x op2 y op1 z) ==> x op1 z)?
- /// </summary>
- [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 (LogicOp(op1) || LogicOp(op2))
- return op2 == BinaryExpr.Opcode.Eq ||
- (op1 == BinaryExpr.Opcode.Imp && op2 == BinaryExpr.Opcode.Iff) ||
- (op1 == BinaryExpr.Opcode.Exp && op2 == BinaryExpr.Opcode.Iff) ||
- (op1 == BinaryExpr.Opcode.Eq && op2 == BinaryExpr.Opcode.Iff);
- return op2 == BinaryExpr.Opcode.Eq ||
- (op1 == BinaryExpr.Opcode.Lt && op2 == BinaryExpr.Opcode.Le) ||
- (op1 == BinaryExpr.Opcode.Gt && op2 == BinaryExpr.Opcode.Ge);
- }
-
- /// <summary>
- /// Resulting operator x op z if x op1 y op2 z.
- /// (Least upper bound in the Subsumes order).
- /// Returns null if neither of op1 or op2 subsumes the other.
- /// </summary>
- [Pure]
- public static BinaryExpr.Opcode? ResultOp(BinaryExpr.Opcode op1, BinaryExpr.Opcode op2) {
- Contract.Requires(ValidOp(op1) && ValidOp(op2));
- Contract.Ensures(Contract.Result<BinaryExpr.Opcode?>() == null || ValidOp((BinaryExpr.Opcode)Contract.Result<BinaryExpr.Opcode?>()));
- if (Subsumes(op1, op2)) {
- return op1;
- } else if (Subsumes(op2, op1)) {
- return op2;
- }
- return null;
+ public static Expression Rhs(Expression step)
+ {
+ Contract.Requires(step is BinaryExpr || step is TernaryExpr);
+ if (step is BinaryExpr) {
+ return ((BinaryExpr) step).E1;
+ } else {
+ return ((TernaryExpr) step).E2;
+ }
}
}
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index d79ef23c..16be7285 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1841,12 +1841,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void CalcStmt(out Statement/*!*/ s) {
Contract.Ensures(Contract.ValueAtReturn(out s) != null);
Token x;
- BinaryExpr.Opcode op, calcOp = BinaryExpr.Opcode.Eq, resOp = BinaryExpr.Opcode.Eq;
+ CalcStmt.CalcOp/*!*/ op, calcOp = Microsoft.Dafny.CalcStmt.DefaultOp, resOp = Microsoft.Dafny.CalcStmt.DefaultOp;
var lines = new List<Expression/*!*/>();
var hints = new List<BlockStmt/*!*/>();
- BinaryExpr.Opcode? customOp;
- var customOps = new List<BinaryExpr.Opcode?>();
- BinaryExpr.Opcode? maybeOp;
+ CalcStmt.CalcOp stepOp;
+ var stepOps = new List<CalcStmt.CalcOp>();
+ CalcStmt.CalcOp maybeOp;
Expression/*!*/ e;
BlockStmt/*!*/ h;
IToken opTok;
@@ -1855,7 +1855,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
if (StartOf(19)) {
CalcOp(out opTok, out calcOp);
- maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(calcOp, calcOp); // guard against non-trasitive calcOp (like !=)
+ maybeOp = calcOp.ResultOp(calcOp); // guard against non-trasitive calcOp (like !=)
if (maybeOp == null) {
SemErr(opTok, "the main operator of a calculation must be transitive");
}
@@ -1865,30 +1865,30 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expect(6);
if (StartOf(14)) {
Expression(out e);
- lines.Add(e); customOp = null;
+ lines.Add(e); stepOp = calcOp;
Expect(15);
while (StartOf(20)) {
if (StartOf(19)) {
CalcOp(out opTok, out op);
- maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(resOp, op);
+ maybeOp = resOp.ResultOp(op);
if (maybeOp == null) {
SemErr(opTok, "this operator cannot continue this calculation");
} else {
- customOp = op;
- resOp = (BinaryExpr.Opcode)maybeOp;
+ stepOp = op;
+ resOp = maybeOp;
}
}
- customOps.Add(customOp);
+ stepOps.Add(stepOp);
Hint(out h);
hints.Add(h);
Expression(out e);
- lines.Add(e); customOp = null;
+ lines.Add(e); stepOp = calcOp;
Expect(15);
}
}
Expect(7);
- s = new CalcStmt(x, calcOp, lines, hints, customOps);
+ s = new CalcStmt(x, calcOp, lines, hints, stepOps, resOp);
}
void ReturnStmt(out Statement/*!*/ s) {
@@ -2209,74 +2209,86 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
}
- void CalcOp(out IToken x, out BinaryExpr.Opcode/*!*/ op) {
- Contract.Ensures(Microsoft.Dafny.CalcStmt.ValidOp(Contract.ValueAtReturn(out op)));
- op = BinaryExpr.Opcode.Eq; // Returns Eq if parsing fails because it is compatible with any other operator
+ void 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
+ Expression k = null;
x = null;
switch (la.kind) {
case 29: {
Get();
- x = t; op = BinaryExpr.Opcode.Eq;
+ x = t; binOp = BinaryExpr.Opcode.Eq;
+ if (la.kind == 83) {
+ Get();
+ Expect(68);
+ Expression(out k);
+ Expect(69);
+ }
break;
}
case 35: {
Get();
- x = t; op = BinaryExpr.Opcode.Lt;
+ x = t; binOp = BinaryExpr.Opcode.Lt;
break;
}
case 36: {
Get();
- x = t; op = BinaryExpr.Opcode.Gt;
- break;
- }
- case 83: {
- Get();
- x = t; op = BinaryExpr.Opcode.Le;
+ x = t; binOp = BinaryExpr.Opcode.Gt;
break;
}
case 84: {
Get();
- x = t; op = BinaryExpr.Opcode.Ge;
+ x = t; binOp = BinaryExpr.Opcode.Le;
break;
}
case 85: {
Get();
- x = t; op = BinaryExpr.Opcode.Neq;
+ x = t; binOp = BinaryExpr.Opcode.Ge;
break;
}
case 86: {
Get();
- x = t; op = BinaryExpr.Opcode.Neq;
+ x = t; binOp = BinaryExpr.Opcode.Neq;
break;
}
case 87: {
Get();
- x = t; op = BinaryExpr.Opcode.Le;
+ x = t; binOp = BinaryExpr.Opcode.Neq;
break;
}
case 88: {
Get();
- x = t; op = BinaryExpr.Opcode.Ge;
+ x = t; binOp = BinaryExpr.Opcode.Le;
break;
}
- case 89: case 90: {
+ case 89: {
+ Get();
+ x = t; binOp = BinaryExpr.Opcode.Ge;
+ break;
+ }
+ case 90: case 91: {
EquivOp();
- x = t; op = BinaryExpr.Opcode.Iff;
+ x = t; binOp = BinaryExpr.Opcode.Iff;
break;
}
- case 91: case 92: {
+ case 92: case 93: {
ImpliesOp();
- x = t; op = BinaryExpr.Opcode.Imp;
+ x = t; binOp = BinaryExpr.Opcode.Imp;
break;
}
- case 93: case 94: {
+ case 94: case 95: {
ExpliesOp();
- x = t; op = BinaryExpr.Opcode.Exp;
+ x = t; binOp = BinaryExpr.Opcode.Exp;
break;
}
default: SynErr(192); break;
}
+ if (k == null) {
+ op = new Microsoft.Dafny.CalcStmt.BinaryCalcOp(binOp);
+ } else {
+ op = new Microsoft.Dafny.CalcStmt.TernaryCalcOp(k);
+ }
+
}
void Hint(out BlockStmt s) {
@@ -2301,25 +2313,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void EquivOp() {
- if (la.kind == 89) {
+ if (la.kind == 90) {
Get();
- } else if (la.kind == 90) {
+ } else if (la.kind == 91) {
Get();
} else SynErr(193);
}
void ImpliesOp() {
- if (la.kind == 91) {
+ if (la.kind == 92) {
Get();
- } else if (la.kind == 92) {
+ } else if (la.kind == 93) {
Get();
} else SynErr(194);
}
void ExpliesOp() {
- if (la.kind == 93) {
+ if (la.kind == 94) {
Get();
- } else if (la.kind == 94) {
+ } else if (la.kind == 95) {
Get();
} else SynErr(195);
}
@@ -2327,7 +2339,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo void EquivExpression(out Expression/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
ImpliesExpliesExpression(out e0);
- while (la.kind == 89 || la.kind == 90) {
+ while (la.kind == 90 || la.kind == 91) {
EquivOp();
x = t;
ImpliesExpliesExpression(out e1);
@@ -2339,7 +2351,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
LogicalExpression(out e0);
if (StartOf(24)) {
- if (la.kind == 91 || la.kind == 92) {
+ if (la.kind == 92 || la.kind == 93) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -2349,7 +2361,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t;
LogicalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.Exp, e0, e1);
- while (la.kind == 93 || la.kind == 94) {
+ while (la.kind == 94 || la.kind == 95) {
ExpliesOp();
x = t;
LogicalExpression(out e1);
@@ -2363,12 +2375,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expression/*!*/ e1;
RelationalExpression(out e0);
if (StartOf(25)) {
- if (la.kind == 95 || la.kind == 96) {
+ if (la.kind == 96 || la.kind == 97) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = new BinaryExpr(x, BinaryExpr.Opcode.And, e0, e1);
- while (la.kind == 95 || la.kind == 96) {
+ while (la.kind == 96 || la.kind == 97) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -2379,7 +2391,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 == 97 || la.kind == 98) {
+ while (la.kind == 98 || la.kind == 99) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -2392,7 +2404,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 == 91 || la.kind == 92) {
+ if (la.kind == 92 || la.kind == 93) {
ImpliesOp();
x = t;
ImpliesExpression(out e1);
@@ -2502,17 +2514,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo }
void AndOp() {
- if (la.kind == 95) {
+ if (la.kind == 96) {
Get();
- } else if (la.kind == 96) {
+ } else if (la.kind == 97) {
Get();
} else SynErr(196);
}
void OrOp() {
- if (la.kind == 97) {
+ if (la.kind == 98) {
Get();
- } else if (la.kind == 98) {
+ } else if (la.kind == 99) {
Get();
} else SynErr(197);
}
@@ -2537,7 +2549,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo case 29: {
Get();
x = t; op = BinaryExpr.Opcode.Eq;
- if (la.kind == 99) {
+ if (la.kind == 83) {
Get();
Expect(68);
Expression(out k);
@@ -2555,20 +2567,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo x = t; op = BinaryExpr.Opcode.Gt;
break;
}
- case 83: {
+ case 84: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 84: {
+ case 85: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
}
- case 85: {
+ case 86: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
- if (la.kind == 99) {
+ if (la.kind == 83) {
Get();
Expect(68);
Expression(out k);
@@ -2604,17 +2616,17 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo break;
}
- case 86: {
+ case 87: {
Get();
x = t; op = BinaryExpr.Opcode.Neq;
break;
}
- case 87: {
+ case 88: {
Get();
x = t; op = BinaryExpr.Opcode.Le;
break;
}
- case 88: {
+ case 89: {
Get();
x = t; op = BinaryExpr.Opcode.Ge;
break;
@@ -2812,9 +2824,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Ident(out id);
idents.Add(id);
}
- if (la.kind == 28 || la.kind == 99) {
+ if (la.kind == 28 || la.kind == 83) {
args = new List<Expression>();
- if (la.kind == 99) {
+ if (la.kind == 83) {
Get();
id.val = id.val + "#"; Expression k;
Expect(68);
@@ -2841,9 +2853,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo if (la.kind == 18) {
Get();
Ident(out id);
- if (la.kind == 28 || la.kind == 99) {
+ if (la.kind == 28 || la.kind == 83) {
args = new List<Expression/*!*/>(); func = true;
- if (la.kind == 99) {
+ if (la.kind == 83) {
Get();
id.val = id.val + "#"; Expression k;
Expect(68);
@@ -3320,16 +3332,16 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo {T,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,T,x,x, T,x,x,x, x,x,T,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, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,T, 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,T, T,T,T,T, T,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,x,x, T,T,x,x, T,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,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,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,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,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,T,T, x,T,x,x, x,x,T,x, T,x,x,x, x,x,T,x, T,x,x,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,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,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,x, x,x,x,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, x,x,x,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,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,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, T,x,T,T, 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,x,x, x,x},
+ {x,x,x,x, x,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,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, T,T,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,T,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, T,T,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, x,T,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, T,x,T,x, T,T,T,T, T,T,T,T, T,T,T,T, x,x,x,x, x,T,x,T, x,x,T,T, T,T,T,T, T,x,x,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,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,T,T, x,T,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, T,x,T,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,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, 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, 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, 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,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,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,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,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, T,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,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,T, T,T,T,T, T,x,x,x, x,x,x,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,x},
- {x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,T, T,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, T,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, T,T,T,T, T,T,x,x, x,x,x,x, x,T,T,x, x,x,T,T, x,x},
- {x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,T, T,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, T,x,x,x, x,x,x,T, T,T,T,T, T,T,T,T, T,T,T,T, T,T,T,x, T,T,T,T, T,T,x,x, x,x,x,x, x,T,T,x, x,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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, T,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,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, T,T,T,T, T,T,x,x, x,x,x,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,x},
+ {x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,T, T,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, 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,T,x,x, x,x,x,x, x,T,T,x, x,x,T,T, x,x},
+ {x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,T,x, x,x,x,x, T,x,T,x, x,T,T,x, x,x,T,T, T,x,x,x, T,T,x,T, T,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, 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,T,x,x, x,x,x,x, x,T,T,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,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,T,T, x,T,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, T,x,T,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,x,x, x,x}
};
@@ -3438,23 +3450,23 @@ public class Errors { case 80: s = "\"forall\" expected"; break;
case 81: s = "\"parallel\" expected"; break;
case 82: s = "\"calc\" expected"; break;
- case 83: s = "\"<=\" expected"; break;
- case 84: s = "\">=\" expected"; break;
- case 85: s = "\"!=\" expected"; break;
- case 86: s = "\"\\u2260\" expected"; break;
- case 87: s = "\"\\u2264\" expected"; break;
- case 88: s = "\"\\u2265\" expected"; break;
- case 89: s = "\"<==>\" expected"; break;
- case 90: s = "\"\\u21d4\" expected"; break;
- case 91: s = "\"==>\" expected"; break;
- case 92: s = "\"\\u21d2\" expected"; break;
- case 93: s = "\"<==\" expected"; break;
- case 94: s = "\"\\u21d0\" expected"; break;
- case 95: s = "\"&&\" expected"; break;
- case 96: s = "\"\\u2227\" expected"; break;
- case 97: s = "\"||\" expected"; break;
- case 98: s = "\"\\u2228\" expected"; break;
- case 99: s = "\"#\" expected"; break;
+ case 83: s = "\"#\" expected"; break;
+ case 84: s = "\"<=\" expected"; break;
+ case 85: s = "\">=\" expected"; break;
+ case 86: s = "\"!=\" expected"; break;
+ case 87: s = "\"\\u2260\" expected"; break;
+ case 88: s = "\"\\u2264\" expected"; break;
+ case 89: s = "\"\\u2265\" expected"; break;
+ case 90: s = "\"<==>\" expected"; break;
+ case 91: s = "\"\\u21d4\" expected"; break;
+ case 92: s = "\"==>\" expected"; break;
+ case 93: s = "\"\\u21d2\" expected"; break;
+ case 94: s = "\"<==\" expected"; break;
+ case 95: s = "\"\\u21d0\" expected"; break;
+ case 96: s = "\"&&\" expected"; break;
+ case 97: s = "\"\\u2227\" expected"; break;
+ case 98: s = "\"||\" expected"; break;
+ case 99: s = "\"\\u2228\" expected"; break;
case 100: s = "\"in\" expected"; break;
case 101: s = "\"!\" expected"; break;
case 102: s = "\"+\" expected"; break;
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 7f75ec1d..e6fe3468 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -648,8 +648,8 @@ namespace Microsoft.Dafny { } else if (stmt is CalcStmt) {
CalcStmt s = (CalcStmt)stmt;
wr.Write("calc ");
- if (s.Op != CalcStmt.DefaultOp) {
- wr.Write(BinaryExpr.OpcodeString(s.Op));
+ if (!s.Op.Equals(CalcStmt.DefaultOp)) {
+ PrintCalcOp(s.Op);
wr.Write(" ");
}
wr.WriteLine("{");
@@ -662,15 +662,15 @@ namespace Microsoft.Dafny { 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];
+ var op = s.StepOps[i - 1];
foreach (var st in h.Body) {
Indent(lineInd);
PrintStatement(st, lineInd);
wr.WriteLine();
}
Indent(lineInd);
- if (op != null && (BinaryExpr.Opcode)op != s.Op) {
- wr.Write(BinaryExpr.OpcodeString((BinaryExpr.Opcode)op));
+ if (!s.Op.Equals(op)) {
+ PrintCalcOp(op);
wr.Write(" ");
}
PrintExpression(e, lineInd);
@@ -901,6 +901,16 @@ namespace Microsoft.Dafny { }
}
+ void PrintCalcOp(CalcStmt.CalcOp op) {
+ Contract.Requires(op != null);
+ wr.Write(op.ToString());
+ if (op is CalcStmt.TernaryCalcOp) {
+ wr.Write("[");
+ PrintExpression(((CalcStmt.TernaryCalcOp) op).Index);
+ wr.Write("]");
+ }
+ }
+
// ----------------------------- PrintExpression -----------------------------
public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, bool endWithCloseParen) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index a8e3d5fa..8d1485f7 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -3863,7 +3863,6 @@ namespace Microsoft.Dafny var prevErrorCount = ErrorCount;
CalcStmt s = (CalcStmt)stmt;
s.IsGhost = true;
- var resOp = s.Op;
if (s.Lines.Count > 0) {
var e0 = s.Lines.First();
ResolveExpression(e0, true, codeContext);
@@ -3875,15 +3874,7 @@ namespace Microsoft.Dafny 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 {
- 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);
- }
+ var step = s.StepOps[i - 1].StepExpr(e0, e1); // Use custom line operator
ResolveExpression(step, true, codeContext);
s.Steps.Add(step);
}
@@ -3903,11 +3894,11 @@ namespace Microsoft.Dafny loopStack = prevLoopStack;
}
- if (prevErrorCount == ErrorCount && s.Lines.Count > 0 && s.Steps.Count > 0) {
+ if (prevErrorCount == ErrorCount && s.Lines.Count > 0) {
// do not build Result from the lines 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());
+ s.Result = s.ResultOp.StepExpr(s.Lines.First(), s.Lines.Last());
} else {
- s.Result = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Eq, CreateResolvedLiteral(s.Tok, 0), CreateResolvedLiteral(s.Tok, 0));
+ s.Result = CalcStmt.DefaultOp.StepExpr(CreateResolvedLiteral(s.Tok, 0), CreateResolvedLiteral(s.Tok, 0));
}
ResolveExpression(s.Result, true, codeContext);
Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == s.Hints.Count);
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index 7f9fb0b1..e67fa46e 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/Scanner.cs @@ -275,16 +275,16 @@ public class Scanner { start[96] = 28;
start[91] = 31;
start[93] = 32;
- start[8800] = 36;
- start[8804] = 37;
- start[8805] = 38;
- start[8660] = 40;
- start[8658] = 42;
- start[8656] = 43;
- start[38] = 44;
- start[8743] = 46;
- start[8744] = 48;
- start[35] = 49;
+ start[35] = 34;
+ start[8800] = 37;
+ start[8804] = 38;
+ start[8805] = 39;
+ start[8660] = 41;
+ start[8658] = 43;
+ start[8656] = 44;
+ start[38] = 45;
+ start[8743] = 47;
+ start[8744] = 49;
start[43] = 50;
start[45] = 51;
start[47] = 52;
@@ -696,7 +696,7 @@ public class Scanner { case 33:
{t.kind = 74; break;}
case 34:
- {t.kind = 84; break;}
+ {t.kind = 83; break;}
case 35:
{t.kind = 85; break;}
case 36:
@@ -714,12 +714,12 @@ public class Scanner { case 42:
{t.kind = 92; break;}
case 43:
- {t.kind = 94; break;}
+ {t.kind = 93; break;}
case 44:
- if (ch == '&') {AddCh(); goto case 45;}
- else {goto case 0;}
- case 45:
{t.kind = 95; break;}
+ case 45:
+ if (ch == '&') {AddCh(); goto case 46;}
+ else {goto case 0;}
case 46:
{t.kind = 96; break;}
case 47:
@@ -755,7 +755,7 @@ public class Scanner { case 60:
recEnd = pos; recKind = 101;
if (ch == 'i') {AddCh(); goto case 12;}
- else if (ch == '=') {AddCh(); goto case 35;}
+ else if (ch == '=') {AddCh(); goto case 36;}
else {t.kind = 101; break;}
case 61:
recEnd = pos; recKind = 14;
@@ -768,7 +768,7 @@ public class Scanner { else {t.kind = 18; break;}
case 63:
recEnd = pos; recKind = 24;
- if (ch == '|') {AddCh(); goto case 47;}
+ if (ch == '|') {AddCh(); goto case 48;}
else {t.kind = 24; break;}
case 64:
recEnd = pos; recKind = 35;
@@ -776,24 +776,24 @@ public class Scanner { else {t.kind = 35; break;}
case 65:
recEnd = pos; recKind = 36;
- if (ch == '=') {AddCh(); goto case 34;}
+ if (ch == '=') {AddCh(); goto case 35;}
else {t.kind = 36; break;}
case 66:
recEnd = pos; recKind = 29;
- if (ch == '>') {AddCh(); goto case 41;}
+ if (ch == '>') {AddCh(); goto case 42;}
else {t.kind = 29; break;}
case 67:
recEnd = pos; recKind = 114;
if (ch == '.') {AddCh(); goto case 26;}
else {t.kind = 114; break;}
case 68:
- recEnd = pos; recKind = 83;
+ recEnd = pos; recKind = 84;
if (ch == '=') {AddCh(); goto case 69;}
- else {t.kind = 83; break;}
+ else {t.kind = 84; break;}
case 69:
- recEnd = pos; recKind = 93;
- if (ch == '>') {AddCh(); goto case 39;}
- else {t.kind = 93; break;}
+ recEnd = pos; recKind = 94;
+ if (ch == '>') {AddCh(); goto case 40;}
+ else {t.kind = 94; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 257cdf3b..a988db16 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -4874,25 +4874,30 @@ namespace Microsoft.Dafny { for (int i = s.Steps.Count; 0 <= --i; ) {
b = new Bpl.StmtListBuilder();
// assume wf[line<i>]:
- AddComment(b, stmt, "assume wf[line" + i.ToString() + "]");
+ AddComment(b, stmt, "assume wf[lhs]");
assertAsAssume = true;
- TrStmt_CheckWellformed(s.Steps[i].E0, b, locals, etran, false);
+ TrStmt_CheckWellformed(CalcStmt.Lhs(s.Steps[i]), b, locals, etran, false);
assertAsAssume = false;
- if (s.Steps[i].ResolvedOp == BinaryExpr.ResolvedOpcode.Imp) {
+ if (s.Steps[i] is BinaryExpr && (((BinaryExpr)s.Steps[i]).ResolvedOp == BinaryExpr.ResolvedOpcode.Imp)) {
// assume line<i>:
- AddComment(b, stmt, "assume line" + i.ToString());
- b.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(s.Steps[i].E0)));
+ AddComment(b, stmt, "assume lhs");
+ b.Add(new Bpl.AssumeCmd(s.Tok, etran.TrExpr(CalcStmt.Lhs(s.Steps[i]))));
}
// hint:
AddComment(b, stmt, "Hint" + i.ToString());
TrStmt(s.Hints[i], b, locals, etran);
// check well formedness of the goal line:
- AddComment(b, stmt, "assert wf[line" + (i + 1).ToString() + "]");
- TrStmt_CheckWellformed(s.Steps[i].E1, b, locals, etran, false);
+ AddComment(b, stmt, "assert wf[rhs]");
+ if (s.Steps[i] is TernaryExpr) {
+ // check the prefix-equality limit
+ var index = ((TernaryExpr) s.Steps[i]).E0;
+ b.Add(AssertNS(index.tok, Bpl.Expr.Le(Bpl.Expr.Literal(0), etran.TrExpr(index)), "prefix-equality limit must be at least 0"));
+ }
+ TrStmt_CheckWellformed(CalcStmt.Rhs(s.Steps[i]), b, locals, etran, false);
bool splitHappened;
var ss = TrSplitExpr(s.Steps[i], etran, out splitHappened);
// assert step:
- AddComment(b, stmt, "assert line" + i.ToString() + " " + s.Steps[i].ResolvedOp.ToString() + " line" + (i + 1).ToString());
+ AddComment(b, stmt, "assert line" + i.ToString() + " " + s.StepOps[i].ToString() + " line" + (i + 1).ToString());
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 {
@@ -4907,8 +4912,8 @@ namespace Microsoft.Dafny { }
// check well formedness of the first line:
b = new Bpl.StmtListBuilder();
- AddComment(b, stmt, "assume wf[line0]");
- TrStmt_CheckWellformed(s.InitalLine(), b, locals, etran, false);
+ AddComment(b, stmt, "assert wf[initial]");
+ TrStmt_CheckWellformed(CalcStmt.Lhs(s.Result), 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);
diff --git a/Test/dafny3/Paulson.dfy b/Test/dafny3/Paulson.dfy index ce9df5fe..c1721af3 100644 --- a/Test/dafny3/Paulson.dfy +++ b/Test/dafny3/Paulson.dfy @@ -35,21 +35,14 @@ comethod Example6(f: FunctionHandle, g: FunctionHandle, M: LList) match M {
case Nil =>
case Cons(x, xs) =>
- assert Lmap(After(f, g), M)
- == Lmap(After(f, g), Cons(x, xs))
- == // def. Lmap
- Cons(Apply(After(f, g), x), Lmap(After(f, g), xs));
- Definition_After(f, g, x);
- assert Cons(Apply(After(f, g), x), Lmap(After(f, g), xs))
- == Cons(Apply(f, Apply(g, x)), Lmap(After(f, g), xs));
-
- // use co-induction hypothesis
- assert
- Cons(Apply(f, Apply(g, x)), Lmap(After(f, g), xs))
- ==#[_k]
- Cons(Apply(f, Apply(g, x)), Lmap(f, Lmap(g, xs)));
-
calc {
+ Lmap(After(f, g), M);
+ Lmap(After(f, g), Cons(x, xs));
+ // def. Lmap
+ Cons(Apply(After(f, g), x), Lmap(After(f, g), xs));
+ { Definition_After(f, g, x); }
+ Cons(Apply(f, Apply(g, x)), Lmap(After(f, g), xs));
+ ==#[_k] // use co-induction hypothesis
Cons(Apply(f, Apply(g, x)), Lmap(f, Lmap(g, xs)));
// def. Lmap
Lmap(f, Cons(Apply(g, x), Lmap(g, xs)));
@@ -75,14 +68,12 @@ comethod Eq24<A>(f: FunctionHandle<LList<A>>, M: LList<A>) Lmap(f, Iterates(f, M));
Lmap(f, Cons(M, Iterates(f, Apply(f, M))));
Cons(Apply(f, M), Lmap(f, Iterates(f, Apply(f, M))));
- }
-
- Eq24(f, Apply(f, M)); // co-induction hypothesis
- assert Lmap(f, Iterates(f, Apply(f, M)))
- ==#[_k-1]
- Iterates(f, Apply(f, Apply(f, M)));
-
- calc {
+ ==#[_k]
+ calc {
+ Lmap(f, Iterates(f, Apply(f, M)));
+ ==#[_k-1] { Eq24(f, Apply(f, M)); } // co-induction hypothesis
+ Iterates(f, Apply(f, Apply(f, M)));
+ }
Cons(Apply(f, M), Iterates(f, Apply(f, Apply(f, M))));
// def. Iterates
Iterates(f, Apply(f, M));
@@ -139,13 +130,12 @@ comethod BisimulationLemma<A>(n: nat, f: FunctionHandle<LList<A>>, u: LList<A>) Cons(Iter(n, f, u), LmapIter(n, f, Lmap(f, h(f, u))));
{ Lemma26(n, f, h(f, u)); }
Cons(Iter(n, f, u), LmapIter(n+1, f, h(f, u)));
- }
-
- assert LmapIter(n+1, f, h(f, u))
+ ==#[_k]
+ calc {
+ LmapIter(n+1, f, h(f, u));
==#[_k-1]
- LmapIter(n+1, f, Iterates(f, u));
-
- calc {
+ LmapIter(n+1, f, Iterates(f, u));
+ }
Cons(Iter(n, f, u), LmapIter(n+1, f, Iterates(f, u)));
{ Lemma26(n, f, Iterates(f, u)); }
Cons(Iter(n, f, u), LmapIter(n, f, Lmap(f, Iterates(f, u))));
|