Allow custom operators on a line

7 files changed, 215 insertions, 123 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 3cd6dabd..a5865a6f 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));

+          r = new CalcStmt(Tok(s.Tok), s.Op, s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneStmt), 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 88045004..646d6ee4 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1220,22 +1220,18 @@ ParallelStmt<out Statement/*!*/ s>
 CalcStmt<out Statement/*!*/ s>

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

      Token x;

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

+     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?>();

+     BinaryExpr.Opcode? maybeOp;

      Expression/*!*/ e;

      BlockStmt/*!*/ block;

      Statement/*!*/ h;

-     IToken bodyStart, bodyEnd, calcOpPos;

+     IToken bodyStart, bodyEnd, opTok;

   .)

   "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; .)

-  ]

+  [ CalcOp<out opTok, out calcOp> ]                     (. resOp = calcOp; .)

   "{"

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

   ";"

@@ -1244,11 +1240,44 @@ CalcStmt<out Statement/*!*/ s>
     | CalcStmt<out h>                                   (. hints.Add(h); .)

     |                                                   (. hints.Add(null); .)

     )

+    ( CalcOp<out opTok, out op>                         (. maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(resOp, op);

+                                                           if (maybeOp == null) {

+                                                             customOps.Add(null); // pretend the operator was not there to satisfy the precondition of the CalcStmt contructor

+                                                             SemErr(opTok, "this operator cannot continue this calculation");

+                                                           } else {

+                                                             customOps.Add(op);

+                                                             resOp = (BinaryExpr.Opcode)maybeOp;                                                              

+                                                           }

+                                                        .)

+    |                                                   (. customOps.Add(null); .)

+    )

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

     ";"

   }

   "}"

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

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

+  .

+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 

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

+                          .)

+  )

   .

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

 Expression<out Expression/*!*/ e>

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index ba0c8536..36f0aace 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2664,9 +2664,10 @@ namespace Microsoft.Dafny {
 

   public class CalcStmt : Statement

   {

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

+    public readonly BinaryExpr.Opcode/*!*/ Op; // main operator of the calculation

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

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

+    public readonly List<Statement> Hints;  // Hints[i] comes after line i; null denotes an empty an empty hint

+    public readonly List<BinaryExpr.Opcode?> CustomOps; // CustomOps[i] comes after line i; null denotes the absence of a custom operator

     public readonly List<BinaryExpr/*!*/> Steps; // expressions li op l<i + 1>, filled in during resolution in order to get the correct op

     public BinaryExpr Result; // expressions l0 op ln, filled in during resolution in order to get the correct op

 

@@ -2678,12 +2679,14 @@ namespace Microsoft.Dafny {
       Contract.Invariant(ValidOp(Op));

       Contract.Invariant(Lines != null);

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

     }

 

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

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

       // Attributes attrs?

       : base(tok)

     {

@@ -2694,9 +2697,12 @@ namespace Microsoft.Dafny {
       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);

       this.Op = op;

       this.Lines = lines;

       this.Hints = hints;

+      this.CustomOps = customOps;

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

       this.Result = null;

     }

@@ -2721,35 +2727,42 @@ namespace Microsoft.Dafny {
     /// <summary>

     /// Is op a valid calculation operator (i.e. a transitive relational 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.Iff || op == BinaryExpr.Opcode.Imp;

     }

 

     /// <summary>

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

+    /// Does op1 subsume op2 (i.e. forall x, y, z :: (x op1 y op2 z) || (x op2 y op1 z) ==> x op1 z)?

     /// </summary>

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

+    [Pure]    

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

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

-      return op1 == op2 ||

+      if (op1 == op2) 

+        return true;

+      if (op1 == BinaryExpr.Opcode.Iff || op1 == BinaryExpr.Opcode.Imp || op2 == BinaryExpr.Opcode.Iff || op2 == BinaryExpr.Opcode.Imp)

+        return op2 == BinaryExpr.Opcode.Eq ||

+          (op1 == BinaryExpr.Opcode.Imp && 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.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);

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

     }

 

     /// <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.

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

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

-        }

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

     }

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index ecfcbbb1..3a310cd9 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1619,36 +1619,27 @@ 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;

+		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?>();

+		BinaryExpr.Opcode? maybeOp;

 		Expression/*!*/ e;

 		BlockStmt/*!*/ block;

 		Statement/*!*/ h;

-		IToken bodyStart, bodyEnd, calcOpPos;

+		IToken bodyStart, bodyEnd, opTok;

 		

 		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; 

-			}

+			CalcOp(out opTok, out calcOp);

 		}

+		resOp = calcOp; 

 		Expect(6);

 		Expression(out e);

 		lines.Add(e); 

 		Expect(14);

-		while (StartOf(16)) {

+		while (StartOf(15)) {

 			if (la.kind == 6) {

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

 				hints.Add(block); 

@@ -1658,12 +1649,26 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			} else {

 				hints.Add(null); 

 			}

+			if (StartOf(14)) {

+				CalcOp(out opTok, out op);

+				maybeOp = Microsoft.Dafny.CalcStmt.ResultOp(resOp, op);

+				if (maybeOp == null) {

+				 customOps.Add(null); // pretend the operator was not there to satisfy the precondition of the CalcStmt contructor

+				 SemErr(opTok, "this operator cannot continue this calculation");

+				} else {

+				 customOps.Add(op);

+				 resOp = (BinaryExpr.Opcode)maybeOp;                                                              

+				}

+				

+			} else if (StartOf(10)) {

+				customOps.Add(null); 

+			} else SynErr(162);

 			Expression(out e);

 			lines.Add(e); 

 			Expect(14);

 		}

 		Expect(7);

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

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

 	}

 

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

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

 		Expect(58);

 		returnTok = t; 

-		if (StartOf(17)) {

+		if (StartOf(16)) {

 			Rhs(out r, null);

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

 			while (la.kind == 24) {

@@ -1792,7 +1797,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(10)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(162);

+		} else SynErr(163);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

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

 				Suffix(ref e);

 			}

-		} else if (StartOf(18)) {

+		} else if (StartOf(17)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

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

 				Suffix(ref e);

 			}

-		} else SynErr(163);

+		} else SynErr(164);

 	}

 

 	void Expressions(List<Expression/*!*/>/*!*/ args) {

@@ -1836,7 +1841,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(10)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(164);

+		} else SynErr(165);

 		Expect(28);

 	}

 

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

 		mod = null;

 		

-		while (StartOf(19)) {

+		while (StartOf(18)) {

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

 				Invariant(out invariant);

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

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

 				Expect(14);

 				invariants.Add(invariant); 

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

-				while (!(la.kind == 0 || la.kind == 39)) {SynErr(166); Get();}

+				while (!(la.kind == 0 || la.kind == 39)) {SynErr(167); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

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

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

 				Expect(14);

 			} else {

-				while (!(la.kind == 0 || la.kind == 35)) {SynErr(168); Get();}

+				while (!(la.kind == 0 || la.kind == 35)) {SynErr(169); Get();}

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

@@ -1899,7 +1904,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						mod.Add(fe); 

 					}

 				}

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

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

 				Expect(14);

 			}

 		}

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

 	void Invariant(out MaybeFreeExpression/*!*/ invariant) {

 		bool isFree = false; Expression/*!*/ e; List<string> ids = new List<string>(); invariant = null; Attributes attrs = null; 

-		while (!(la.kind == 0 || la.kind == 36 || la.kind == 70)) {SynErr(170); Get();}

+		while (!(la.kind == 0 || la.kind == 36 || la.kind == 70)) {SynErr(171); Get();}

 		if (la.kind == 36) {

 			Get();

 			isFree = true; 

@@ -1956,7 +1961,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (StartOf(10)) {

 			Expression(out e);

 			arg = new Attributes.Argument(t, e); 

-		} else SynErr(171);

+		} else SynErr(172);

 	}

 

 	void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {

@@ -1981,6 +1986,35 @@ 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 

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

@@ -2060,7 +2094,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(172); break;

+		default: SynErr(174); break;

 		}

 	}

 

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

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

 			Get();

-		} else SynErr(173);

+		} else SynErr(175);

 	}

 

 	void ImpliesOp() {

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

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

 			Get();

-		} else SynErr(174);

+		} else SynErr(176);

 	}

 

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

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

 		Term(out e0);

 		e = e0; 

-		if (StartOf(15)) {

+		if (StartOf(19)) {

 			RelOp(out x, out op);

 			firstOpTok = x; 

 			Term(out e1);

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

+			while (StartOf(19)) {

 				if (chain == null) {

 				 chain = new List<Expression>();

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

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

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

 			Get();

-		} else SynErr(175);

+		} else SynErr(177);

 	}

 

 	void OrOp() {

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

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

 			Get();

-		} else SynErr(176);

+		} else SynErr(178);

 	}

 

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

@@ -2266,7 +2300,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 94) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Sub; 

-		} else SynErr(177);

+		} else SynErr(179);

 	}

 

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

@@ -2323,7 +2357,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				MapComprehensionExpr(x, out e);

 			} else if (StartOf(21)) {

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

-			} else SynErr(178);

+			} else SynErr(180);

 			break;

 		}

 		case 2: case 22: case 26: case 98: case 99: case 100: case 101: case 102: case 103: {

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

 			break;

 		}

-		default: SynErr(179); break;

+		default: SynErr(181); break;

 		}

 	}

 

@@ -2348,7 +2382,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 96) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mod; 

-		} else SynErr(180);

+		} else SynErr(182);

 	}

 

 	void NegOp() {

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

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

 			Get();

-		} else SynErr(181);

+		} else SynErr(183);

 	}

 

 	void EndlessExpression(out Expression e) {

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

 			break;

 		}

-		default: SynErr(182); break;

+		default: SynErr(184); break;

 		}

 	}

 

@@ -2488,7 +2522,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(183);

+				} else SynErr(185);

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

 				Get();

 				anyDots = true; 

@@ -2496,7 +2530,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Expression(out ee);

 					e1 = ee; 

 				}

-			} else SynErr(184);

+			} else SynErr(186);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			 // make sure an array class with this dimensionality exists

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

 			

 			Expect(63);

-		} else SynErr(185);

+		} else SynErr(187);

 	}

 

 	void DisplayExpr(out Expression e) {

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

 			e = new SeqDisplayExpr(x, elements); 

 			Expect(63);

-		} else SynErr(186);

+		} else SynErr(188);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -2570,7 +2604,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(28);

 		} else if (StartOf(22)) {

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

-		} else SynErr(187);

+		} else SynErr(189);

 	}

 

 	void MapDisplayExpr(IToken/*!*/ mapToken, out Expression e) {

@@ -2670,7 +2704,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(28);

 			break;

 		}

-		default: SynErr(188); break;

+		default: SynErr(190); break;

 		}

 	}

 

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

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

 			Get();

-		} else SynErr(189);

+		} else SynErr(191);

 	}

 

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

@@ -2737,7 +2771,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 108 || la.kind == 109) {

 			Exists();

 			x = t; 

-		} else SynErr(190);

+		} else SynErr(192);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body);

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

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

 			Get();

-		} else SynErr(191);

+		} else SynErr(193);

 	}

 

 	void Exists() {

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

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

 			Get();

-		} else SynErr(192);

+		} else SynErr(194);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2910,11 +2944,11 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{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,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,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,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},

@@ -3105,37 +3139,39 @@ public class Errors {
 			case 159: s = "invalid IfStmt"; break;

 			case 160: s = "invalid WhileStmt"; break;

 			case 161: s = "invalid WhileStmt"; break;

-			case 162: s = "invalid Rhs"; break;

-			case 163: s = "invalid Lhs"; break;

-			case 164: s = "invalid Guard"; break;

-			case 165: s = "this symbol not expected in LoopSpec"; break;

+			case 162: s = "invalid CalcStmt"; break;

+			case 163: s = "invalid Rhs"; break;

+			case 164: s = "invalid Lhs"; break;

+			case 165: s = "invalid Guard"; break;

 			case 166: s = "this symbol not expected in LoopSpec"; break;

 			case 167: s = "this symbol not expected in LoopSpec"; break;

 			case 168: s = "this symbol not expected in LoopSpec"; break;

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

-			case 180: s = "invalid MulOp"; break;

-			case 181: s = "invalid NegOp"; break;

-			case 182: s = "invalid EndlessExpression"; break;

-			case 183: s = "invalid Suffix"; break;

-			case 184: s = "invalid Suffix"; break;

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

+			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 179: s = "invalid AddOp"; break;

+			case 180: s = "invalid UnaryExpression"; break;

+			case 181: s = "invalid UnaryExpression"; break;

+			case 182: s = "invalid MulOp"; break;

+			case 183: s = "invalid NegOp"; break;

+			case 184: s = "invalid EndlessExpression"; break;

 			case 185: s = "invalid Suffix"; break;

-			case 186: s = "invalid DisplayExpr"; break;

-			case 187: s = "invalid MultiSetExpr"; break;

-			case 188: s = "invalid ConstAtomExpression"; break;

-			case 189: s = "invalid QSep"; break;

-			case 190: s = "invalid QuantifierGuts"; break;

-			case 191: s = "invalid Forall"; break;

-			case 192: s = "invalid Exists"; break;

+			case 186: s = "invalid Suffix"; break;

+			case 187: s = "invalid Suffix"; break;

+			case 188: s = "invalid DisplayExpr"; break;

+			case 189: s = "invalid MultiSetExpr"; break;

+			case 190: s = "invalid ConstAtomExpression"; break;

+			case 191: s = "invalid QSep"; break;

+			case 192: s = "invalid QuantifierGuts"; break;

+			case 193: s = "invalid Forall"; break;

+			case 194: s = "invalid Exists"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 7f0e8102..2051a54e 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -572,16 +572,22 @@ namespace Microsoft.Dafny {
         Indent(lineInd);

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

         wr.WriteLine(";");

-        var pairs = s.Hints.Zip(s.Lines.Skip(1), (h, e) => Tuple.Create(h, e));

-        foreach (var pair in pairs) {

-          if (pair.Item1 != null) {

+        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) {

             Indent(lineInd);

-            PrintStatement(pair.Item1, lineInd);

+            PrintStatement(h, lineInd);

             wr.WriteLine();

           }

           Indent(lineInd);

-          PrintExpression(pair.Item2, lineInd);

-          wr.WriteLine(";");

+          if (op != null && (BinaryExpr.Opcode)op != s.Op) {

+            wr.Write(BinaryExpr.OpcodeString((BinaryExpr.Opcode)op));

+            wr.Write(" ");

+          }          

+          PrintExpression(e, lineInd);

+          wr.WriteLine(";");          

         }

         Indent(indent);

         wr.Write("}");

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 3baf986b..a2710c38 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -3131,21 +3131,30 @@ namespace Microsoft.Dafny
         }

 		

       } else if (stmt is CalcStmt) {

-        int prevErrorCount = ErrorCount;

+        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

-        foreach (var e1 in s.Lines.Skip(1))

-        {

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

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

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

           }

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

           }

         }

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

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

 

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 6d272c07..9bd16f3f 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -7,7 +7,6 @@ using System;
 using System.Collections.Generic;

 using System.Numerics;

 using System.Diagnostics.Contracts;

-using System.Linq;

 using Bpl = Microsoft.Boogie;

 using System.Text;

 using Microsoft.Boogie;