Allow several calculation operators (for the whole calculation)

6 files changed, 199 insertions, 130 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 2997b343..3cd6dabd 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.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneStmt));

+          r = new CalcStmt(Tok(s.Tok), s.Op, s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneStmt));

 

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 7e608945..88045004 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1220,14 +1220,22 @@ ParallelStmt<out Statement/*!*/ s>
 CalcStmt<out Statement/*!*/ s>

 = (. Contract.Ensures(Contract.ValueAtReturn(out s) != null);

      Token x;

+     BinaryExpr.Opcode/*!*/ op = BinaryExpr.Opcode.Eq;

      List<Expression/*!*/> lines = new List<Expression/*!*/>();

      List<Statement> hints = new List<Statement>(); 

      Expression/*!*/ e;

      BlockStmt/*!*/ block;

      Statement/*!*/ h;

-     IToken bodyStart, bodyEnd;

+     IToken bodyStart, bodyEnd, calcOpPos;

   .)

   "calc"                                                (. x = t; .)

+  [ RelOp<out calcOpPos, out op>                        (. if (!Microsoft.Dafny.CalcStmt.ValidOp(op)) {

+                                                             SemErr(calcOpPos, "this operator is not allowed in calculations");

+                                                           }

+                                                        .)

+    | EquivOp                                           (. op = BinaryExpr.Opcode.Iff; .)

+    | ImpliesOp                                         (. op = BinaryExpr.Opcode.Imp; .)

+  ]

   "{"

   Expression<out e>                                     (. lines.Add(e); .)

   ";"

@@ -1240,7 +1248,7 @@ CalcStmt<out Statement/*!*/ s>
     ";"

   }

   "}"

-  (. s = new CalcStmt(x, lines, hints); .)

+  (. s = new CalcStmt(x, op, lines, hints); .)

   .

 /*------------------------------------------------------------------------*/

 Expression<out Expression/*!*/ e>

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 714d87e7..ba0c8536 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2664,14 +2664,18 @@ namespace Microsoft.Dafny {
 

   public class CalcStmt : Statement

   {

+    public readonly BinaryExpr.Opcode/*!*/ Op;

     public readonly List<Expression/*!*/> Lines;

     public readonly List<Statement> Hints;  // an empty hint is represented with null

     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 static readonly BinaryExpr.Opcode/*!*/ DefaultOp = BinaryExpr.Opcode.Eq; 

+

     [ContractInvariantMethod]

     void ObjectInvariant()

     {

+      Contract.Invariant(ValidOp(Op));

       Contract.Invariant(Lines != null);

       Contract.Invariant(Hints != null);

       Contract.Invariant(Steps != null);

@@ -2679,16 +2683,18 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Hints.Count == Lines.Count - 1);

     }

 

-    public CalcStmt(IToken tok, List<Expression/*!*/> lines, List<Statement> hints)

+    public CalcStmt(IToken tok, BinaryExpr.Opcode/*!*/ op, List<Expression/*!*/> lines, List<Statement> hints)

       // 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);

+      this.Op = op;

       this.Lines = lines;

       this.Hints = hints;

       this.Steps = new List<BinaryExpr>();  

@@ -2711,6 +2717,42 @@ namespace Microsoft.Dafny {
         }

       }

     }

+

+    /// <summary>

+    /// Is op a valid calculation operator (i.e. a transitive relational operator)?

+    /// </summary>

+    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.Iff || op == BinaryExpr.Opcode.Imp;

+    }

+

+    /// <summary>

+    /// Is op1 a subrelation of op2 (i.e. x op1 y ==> x op2 y)?

+    /// </summary>

+    private static bool SubRelation(BinaryExpr.Opcode op1, BinaryExpr.Opcode op2) {

+      Contract.Requires(ValidOp(op1) && ValidOp(op2));

+      return op1 == op2 ||

+        (op1 == BinaryExpr.Opcode.Lt && op2 == BinaryExpr.Opcode.Le) ||

+        (op1 == BinaryExpr.Opcode.Eq && op2 == BinaryExpr.Opcode.Le) ||

+        (op1 == BinaryExpr.Opcode.Gt && op2 == BinaryExpr.Opcode.Ge) ||

+        (op1 == BinaryExpr.Opcode.Eq && op2 == BinaryExpr.Opcode.Ge) ||

+        (op1 == BinaryExpr.Opcode.Iff && op2 == BinaryExpr.Opcode.Imp);

+    }

+

+    /// <summary>

+    /// Least upper bound of relations op1 and op2.

+    /// Returns null if op1 or op2 is not a valid calculation operator, or if the least upper bound is top.

+    /// </summary>

+    public static Nullable<BinaryExpr.Opcode> Lub(BinaryExpr.Opcode op1, BinaryExpr.Opcode op2) {

+      if (ValidOp(op1) && ValidOp(op2)) {

+        if (SubRelation(op1, op2)) {

+          return op2;

+        } else if (SubRelation(op2, op1)) {

+          return op1;

+        }

+      }

+      return null;

+    }

   }

 

   public class MatchStmt : Statement

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 89bf8292..ecfcbbb1 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1619,20 +1619,36 @@ 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 = BinaryExpr.Opcode.Eq;

 		List<Expression/*!*/> lines = new List<Expression/*!*/>();

 		List<Statement> hints = new List<Statement>(); 

 		Expression/*!*/ e;

 		BlockStmt/*!*/ block;

 		Statement/*!*/ h;

-		IToken bodyStart, bodyEnd;

+		IToken bodyStart, bodyEnd, calcOpPos;

 		

 		Expect(75);

 		x = t; 

+		if (StartOf(14)) {

+			if (StartOf(15)) {

+				RelOp(out calcOpPos, out op);

+				if (!Microsoft.Dafny.CalcStmt.ValidOp(op)) {

+				 SemErr(calcOpPos, "this operator is not allowed in calculations");

+				}

+				

+			} else if (la.kind == 76 || la.kind == 77) {

+				EquivOp();

+				op = BinaryExpr.Opcode.Iff; 

+			} else {

+				ImpliesOp();

+				op = BinaryExpr.Opcode.Imp; 

+			}

+		}

 		Expect(6);

 		Expression(out e);

 		lines.Add(e); 

 		Expect(14);

-		while (StartOf(14)) {

+		while (StartOf(16)) {

 			if (la.kind == 6) {

 				BlockStmt(out block, out bodyStart, out bodyEnd);

 				hints.Add(block); 

@@ -1647,7 +1663,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(14);

 		}

 		Expect(7);

-		s = new CalcStmt(x, lines, hints); 

+		s = new CalcStmt(x, op, lines, hints); 

 	}

 

 	void ReturnStmt(out Statement/*!*/ s) {

@@ -1657,7 +1673,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Expect(58);

 		returnTok = t; 

-		if (StartOf(15)) {

+		if (StartOf(17)) {

 			Rhs(out r, null);

 			rhss = new List<AssignmentRhs>(); rhss.Add(r); 

 			while (la.kind == 24) {

@@ -1791,7 +1807,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			while (la.kind == 17 || la.kind == 62) {

 				Suffix(ref e);

 			}

-		} else if (StartOf(16)) {

+		} else if (StartOf(18)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

 			while (la.kind == 17 || la.kind == 62) {

@@ -1852,7 +1868,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		decreases = new List<Expression/*!*/>();

 		mod = null;

 		

-		while (StartOf(17)) {

+		while (StartOf(19)) {

 			if (la.kind == 36 || la.kind == 70) {

 				Invariant(out invariant);

 				while (!(la.kind == 0 || la.kind == 14)) {SynErr(165); Get();}

@@ -1965,6 +1981,105 @@ 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 84: {

+			Get();

+			x = t;  op = BinaryExpr.Opcode.Le; 

+			break;

+		}

+		case 85: {

+			Get();

+			x = t;  op = BinaryExpr.Opcode.Ge; 

+			break;

+		}

+		case 86: {

+			Get();

+			x = t;  op = BinaryExpr.Opcode.Neq; 

+			break;

+		}

+		case 87: {

+			Get();

+			x = t;  op = BinaryExpr.Opcode.Disjoint; 

+			break;

+		}

+		case 88: {

+			Get();

+			x = t;  op = BinaryExpr.Opcode.In; 

+			break;

+		}

+		case 89: {

+			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;

+			}

+			

+			break;

+		}

+		case 90: {

+			Get();

+			x = t;  op = BinaryExpr.Opcode.Neq; 

+			break;

+		}

+		case 91: {

+			Get();

+			x = t;  op = BinaryExpr.Opcode.Le; 

+			break;

+		}

+		case 92: {

+			Get();

+			x = t;  op = BinaryExpr.Opcode.Ge; 

+			break;

+		}

+		default: SynErr(172); break;

+		}

+	}

+

+	void EquivOp() {

+		if (la.kind == 76) {

+			Get();

+		} else if (la.kind == 77) {

+			Get();

+		} else SynErr(173);

+	}

+

+	void ImpliesOp() {

+		if (la.kind == 78) {

+			Get();

+		} else if (la.kind == 79) {

+			Get();

+		} else SynErr(174);

+	}

+

 	void EquivExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		ImpliesExpression(out e0);

@@ -1987,18 +2102,10 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 	}

 

-	void EquivOp() {

-		if (la.kind == 76) {

-			Get();

-		} else if (la.kind == 77) {

-			Get();

-		} else SynErr(172);

-	}

-

 	void LogicalExpression(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		RelationalExpression(out e0);

-		if (StartOf(18)) {

+		if (StartOf(20)) {

 			if (la.kind == 80 || la.kind == 81) {

 				AndOp();

 				x = t; 

@@ -2025,14 +2132,6 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		}

 	}

 

-	void ImpliesOp() {

-		if (la.kind == 78) {

-			Get();

-		} else if (la.kind == 79) {

-			Get();

-		} else SynErr(173);

-	}

-

 	void RelationalExpression(out Expression/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null);

 		IToken x, firstOpTok = null;  Expression e0, e1, acc = null;  BinaryExpr.Opcode op;

@@ -2047,7 +2146,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		

 		Term(out e0);

 		e = e0; 

-		if (StartOf(19)) {

+		if (StartOf(15)) {

 			RelOp(out x, out op);

 			firstOpTok = x; 

 			Term(out e1);

@@ -2055,7 +2154,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(15)) {

 				if (chain == null) {

 				 chain = new List<Expression>();

 				 ops = new List<BinaryExpr.Opcode>();

@@ -2128,7 +2227,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 81) {

 			Get();

-		} else SynErr(174);

+		} else SynErr(175);

 	}

 

 	void OrOp() {

@@ -2136,7 +2235,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Get();

 		} else if (la.kind == 83) {

 			Get();

-		} else SynErr(175);

+		} else SynErr(176);

 	}

 

 	void Term(out Expression/*!*/ e0) {

@@ -2149,89 +2248,6 @@ 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 84: {

-			Get();

-			x = t;  op = BinaryExpr.Opcode.Le; 

-			break;

-		}

-		case 85: {

-			Get();

-			x = t;  op = BinaryExpr.Opcode.Ge; 

-			break;

-		}

-		case 86: {

-			Get();

-			x = t;  op = BinaryExpr.Opcode.Neq; 

-			break;

-		}

-		case 87: {

-			Get();

-			x = t;  op = BinaryExpr.Opcode.Disjoint; 

-			break;

-		}

-		case 88: {

-			Get();

-			x = t;  op = BinaryExpr.Opcode.In; 

-			break;

-		}

-		case 89: {

-			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;

-			}

-			

-			break;

-		}

-		case 90: {

-			Get();

-			x = t;  op = BinaryExpr.Opcode.Neq; 

-			break;

-		}

-		case 91: {

-			Get();

-			x = t;  op = BinaryExpr.Opcode.Le; 

-			break;

-		}

-		case 92: {

-			Get();

-			x = t;  op = BinaryExpr.Opcode.Ge; 

-			break;

-		}

-		default: SynErr(176); break;

-		}

-	}

-

 	void Factor(out Expression/*!*/ e0) {

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1;  BinaryExpr.Opcode op; 

 		UnaryExpression(out e0);

@@ -2305,7 +2321,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				}

 			} else if (la.kind == 1) {

 				MapComprehensionExpr(x, out e);

-			} else if (StartOf(20)) {

+			} else if (StartOf(21)) {

 				SemErr("map must be followed by literal in brackets or comprehension."); 

 			} else SynErr(178);

 			break;

@@ -2552,7 +2568,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expression(out e);

 			e = new MultiSetFormingExpr(x, e); 

 			Expect(28);

-		} else if (StartOf(21)) {

+		} else if (StartOf(22)) {

 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 

 		} else SynErr(187);

 	}

@@ -2854,7 +2870,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(5);

 		Expect(1);

 		aName = t.val; 

-		if (StartOf(22)) {

+		if (StartOf(23)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

 			while (la.kind == 24) {

@@ -2893,12 +2909,13 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{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},

 		{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,x,x,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,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,T, 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,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,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,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, 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,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,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}

@@ -3098,11 +3115,11 @@ public class Errors {
 			case 169: s = "this symbol not expected in LoopSpec"; break;

 			case 170: s = "this symbol not expected in Invariant"; break;

 			case 171: s = "invalid AttributeArg"; break;

-			case 172: s = "invalid EquivOp"; break;

-			case 173: s = "invalid ImpliesOp"; break;

-			case 174: s = "invalid AndOp"; break;

-			case 175: s = "invalid OrOp"; break;

-			case 176: s = "invalid RelOp"; break;

+			case 172: s = "invalid RelOp"; break;

+			case 173: s = "invalid EquivOp"; break;

+			case 174: s = "invalid ImpliesOp"; break;

+			case 175: s = "invalid AndOp"; break;

+			case 176: s = "invalid OrOp"; break;

 			case 177: s = "invalid AddOp"; break;

 			case 178: s = "invalid UnaryExpression"; break;

 			case 179: s = "invalid UnaryExpression"; break;

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index f9f1f005..7f0e8102 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -562,8 +562,12 @@ namespace Microsoft.Dafny {
 

       } else if (stmt is CalcStmt) {

         CalcStmt s = (CalcStmt)stmt;

-        wr.Write("calc");

-        wr.WriteLine(" {");

+        wr.Write("calc ");

+        if (s.Op != CalcStmt.DefaultOp) {

+          wr.Write(BinaryExpr.OpcodeString(s.Op));

+          wr.Write(" ");

+        }

+        wr.WriteLine("{");

         int lineInd = indent + IndentAmount;

         Indent(lineInd);

         PrintExpression(s.Lines.First(), lineInd);

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 771ea477..3baf986b 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1317,8 +1317,6 @@ namespace Microsoft.Dafny
           }

           return TailRecursionStatus.NotTailRecursive;

         }

-      } else if (stmt is CalcStmt) {

-          // NadiaTodo		

       } else if (stmt is MatchStmt) {

         var s = (MatchStmt)stmt;

         var status = TailRecursionStatus.CanBeFollowedByAnything;

@@ -1709,7 +1707,7 @@ namespace Microsoft.Dafny
         CheckTypeInference(s.Range);

         CheckTypeInference(s.Body);

       } else if (stmt is CalcStmt) {

-        // NadiaToDo: what does this even do?

+        // NadiaToDo: is this correct?

         var s = (CalcStmt)stmt;

         s.SubExpressions.Iter(e => CheckTypeInference(e));

         s.SubStatements.Iter(CheckTypeInference);		

@@ -3147,7 +3145,7 @@ namespace Microsoft.Dafny
           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 {

-            var step = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Eq, e0, e1);

+            var step = new BinaryExpr(e0.tok, s.Op, e0, e1);

             ResolveExpression(step, true);

             s.Steps.Add(step);            

           }

@@ -3159,7 +3157,7 @@ namespace Microsoft.Dafny
             ResolveStatement(h, true, method);

           }

         }

-        s.Result = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Eq, s.Lines.First(), s.Lines.Last());

+        s.Result = new BinaryExpr(s.Tok, s.Op, s.Lines.First(), s.Lines.Last());

         ResolveExpression(s.Result, true);

         Contract.Assert(prevErrorCount != ErrorCount || s.Steps.Count == s.Hints.Count);