Added some co- test cases. Fixed some bugs.

12 files changed, 328 insertions, 103 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index fa72c6e4..cdc37efa 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -607,29 +607,38 @@ namespace Microsoft.Dafny
     public override Statement CloneStmt(Statement stmt) {

       if (stmt is UpdateStmt) {

         var s = (UpdateStmt)stmt;

-        if (s.ResolvedStatements.Count == 1) {

-          var r = CloneStmt(s.ResolvedStatements[0]);

-          // don't forget to add labels to the cloned statement

-          AddStmtLabels(r, stmt.Labels);

-          r.Attributes = CloneAttributes(stmt.Attributes);

-          return r;

+        if (s.ResolvedStatements.Count == 1 && s.ResolvedStatements[0] is CallStmt) {

+          var call = (CallStmt)s.ResolvedStatements[0];

+          var moduleCaller = context.EnclosingClass.Module;

+          var moduleCallee = call.Method.EnclosingClass.Module;

+          if (call.Method is CoMethod && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(call.Method)) {

+            // we're looking at a recursive call to a comethod

+            var args = new List<Expression>();

+            args.Add(k);

+            foreach (var arg in call.Args) {

+              args.Add(CloneExpr(arg));

+            }

+            var rhs = new CallRhs(Tok(call.Tok), CloneExpr(call.Receiver), call.MethodName + "#", args);

+            var r = new UpdateStmt(Tok(s.Tok), s.Lhss.ConvertAll(CloneExpr), new List<AssignmentRhs>() { rhs }, s.CanMutateKnownState);

+            // don't forget to add labels to the cloned statement

+            AddStmtLabels(r, stmt.Labels);

+            r.Attributes = CloneAttributes(stmt.Attributes);

+            return r;

+          }

         }

       } else if (stmt is CallStmt) {

         var s = (CallStmt)stmt;

         if (s.Method is CoMethod) {

           var moduleCaller = context.EnclosingClass.Module;

           var moduleCallee = s.Method.EnclosingClass.Module;

-          if (moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) {

+          if (s.Method is CoMethod && moduleCaller == moduleCallee && moduleCaller.CallGraph.GetSCCRepresentative(context) == moduleCaller.CallGraph.GetSCCRepresentative(s.Method)) {

             // we're looking at a recursive call to a comethod

-            var lhs = s.Lhs.ConvertAll(CloneExpr);

-            var receiver = CloneExpr(s.Receiver);

             var args = new List<Expression>();

             args.Add(k);

             foreach (var arg in s.Args) {

               args.Add(CloneExpr(arg));

             }

-            var r = new CallStmt(Tok(s.Tok), lhs, receiver, s.MethodName + "#", args);

-

+            var r = new CallStmt(Tok(s.Tok), s.Lhs.ConvertAll(CloneExpr), CloneExpr(s.Receiver), s.MethodName + "#", args);

             // don't forget to add labels to the cloned statement

             AddStmtLabels(r, stmt.Labels);

             r.Attributes = CloneAttributes(stmt.Attributes);

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 07ce8e8d..cee1e7e7 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1310,6 +1310,7 @@ CalcStmt<out Statement/*!*/ s>
      BinaryExpr.Opcode op, calcOp = BinaryExpr.Opcode.Eq, resOp = BinaryExpr.Opcode.Eq;     

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

      var hints = new List<BlockStmt/*!*/>(); 

+     BinaryExpr.Opcode? customOp;

      var customOps = new List<BinaryExpr.Opcode?>();

      BinaryExpr.Opcode? maybeOp;

      Expression/*!*/ e;

@@ -1328,18 +1329,16 @@ CalcStmt<out Statement/*!*/ s>
   [ Expression<out e>                                     (. lines.Add(e); .)

     ";"

     {

-      Hint<out h>                                         (. hints.Add(h); .)

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

+      Hint<out h>                                         (. hints.Add(h); customOp = 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);

+                                                               customOp = op;

                                                                resOp = (BinaryExpr.Opcode)maybeOp;                                                              

                                                              }

                                                           .)

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

-      )

+      ]                                                   (. customOps.Add(customOp); .)

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

       ";"

     }

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 7b62344c..9085a3d2 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1813,6 +1813,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		BinaryExpr.Opcode op, calcOp = BinaryExpr.Opcode.Eq, resOp = BinaryExpr.Opcode.Eq;     

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

 		var hints = new List<BlockStmt/*!*/>(); 

+		BinaryExpr.Opcode? customOp;

 		var customOps = new List<BinaryExpr.Opcode?>();

 		BinaryExpr.Opcode? maybeOp;

 		Expression/*!*/ e;

@@ -1837,21 +1838,19 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(14);

 			while (StartOf(19)) {

 				Hint(out h);

-				hints.Add(h); 

+				hints.Add(h); customOp = null; 

 				if (StartOf(18)) {

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

+					 customOp = op;

 					 resOp = (BinaryExpr.Opcode)maybeOp;                                                              

 					}

 					

-				} else if (StartOf(14)) {

-					customOps.Add(null); 

-				} else SynErr(176);

+				}

+				customOps.Add(customOp); 

 				Expression(out e);

 				lines.Add(e); 

 				Expect(14);

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

 			Get();

 			returnTok = t; isYield = true; 

-		} else SynErr(177);

+		} else SynErr(176);

 		if (StartOf(20)) {

 			Rhs(out r, null);

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

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

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(178);

+		} else SynErr(177);

 		while (la.kind == 6) {

 			Attribute(ref attrs);

 		}

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

 				Suffix(ref e);

 			}

-		} else SynErr(179);

+		} else SynErr(178);

 	}

 

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

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

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(180);

+		} else SynErr(179);

 		Expect(29);

 	}

 

@@ -2058,20 +2057,20 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		while (StartOf(22)) {

 			if (la.kind == 40 || la.kind == 75) {

 				Invariant(out invariant);

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

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

 				Expect(14);

 				invariants.Add(invariant); 

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

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref decAttrs);

 				}

 				DecreasesList(decreases, true);

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

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

 				Expect(14);

 			} else {

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

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

 				Get();

 				while (IsAttribute()) {

 					Attribute(ref modAttrs);

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

 					}

 				}

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

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

 				Expect(14);

 			}

 		}

@@ -2094,7 +2093,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 == 40 || la.kind == 75)) {SynErr(186); Get();}

+		while (!(la.kind == 0 || la.kind == 40 || la.kind == 75)) {SynErr(185); Get();}

 		if (la.kind == 40) {

 			Get();

 			isFree = true; 

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

 			Expression(out e);

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

-		} else SynErr(187);

+		} else SynErr(186);

 	}

 

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

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

 			break;

 		}

-		default: SynErr(188); break;

+		default: SynErr(187); break;

 		}

 	}

 

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

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

 			Get();

-		} else SynErr(189);

+		} else SynErr(188);

 	}

 

 	void ImpliesOp() {

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

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

 			Get();

-		} else SynErr(190);

+		} else SynErr(189);

 	}

 

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

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

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

 			Get();

-		} else SynErr(191);

+		} else SynErr(190);

 	}

 

 	void OrOp() {

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

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

 			Get();

-		} else SynErr(192);

+		} else SynErr(191);

 	}

 

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

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

 			break;

 		}

-		default: SynErr(193); break;

+		default: SynErr(192); break;

 		}

 	}

 

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

 			Get();

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

-		} else SynErr(194);

+		} else SynErr(193);

 	}

 

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

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

 			} else if (StartOf(25)) {

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

-			} else SynErr(195);

+			} else SynErr(194);

 			break;

 		}

 		case 2: case 23: case 27: case 104: case 105: case 106: case 107: case 108: case 109: {

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

 			break;

 		}

-		default: SynErr(196); break;

+		default: SynErr(195); break;

 		}

 	}

 

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

 			Get();

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

-		} else SynErr(197);

+		} else SynErr(196);

 	}

 

 	void NegOp() {

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

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

 			Get();

-		} else SynErr(198);

+		} else SynErr(197);

 	}

 

 	void EndlessExpression(out Expression e) {

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

 			break;

 		}

-		default: SynErr(199); break;

+		default: SynErr(198); break;

 		}

 	}

 

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

 						

 					}

-				} else SynErr(200);

+				} else SynErr(199);

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

 				Get();

 				anyDots = true; 

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

 					e1 = ee; 

 				}

-			} else SynErr(201);

+			} else SynErr(200);

 			if (multipleIndices != null) {

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

 			 // make sure an array class with this dimensionality exists

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

 			

 			Expect(68);

-		} else SynErr(202);

+		} else SynErr(201);

 	}

 

 	void DisplayExpr(out Expression e) {

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

 			e = new SeqDisplayExpr(x, elements); 

 			Expect(68);

-		} else SynErr(203);

+		} else SynErr(202);

 	}

 

 	void MultiSetExpr(out Expression e) {

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

 		} else if (StartOf(26)) {

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

-		} else SynErr(204);

+		} else SynErr(203);

 	}

 

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

@@ -2985,7 +2984,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expect(29);

 			break;

 		}

-		default: SynErr(205); break;

+		default: SynErr(204); break;

 		}

 	}

 

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

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

 			Get();

-		} else SynErr(206);

+		} else SynErr(205);

 	}

 

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

@@ -3052,7 +3051,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 114 || la.kind == 115) {

 			Exists();

 			x = t; 

-		} else SynErr(207);

+		} else SynErr(206);

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

 		QSep();

 		Expression(out body);

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

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

 			Get();

-		} else SynErr(208);

+		} else SynErr(207);

 	}

 

 	void Exists() {

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

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

 			Get();

-		} else SynErr(209);

+		} else SynErr(208);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -3438,40 +3437,39 @@ public class Errors {
 			case 173: s = "invalid IfStmt"; break;

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

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

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

-			case 177: s = "invalid ReturnStmt"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-			case 194: s = "invalid AddOp"; break;

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

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

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

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

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

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

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

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

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

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

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

-			case 196: s = "invalid UnaryExpression"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

 

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

 		}

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 270392cd..ed3c51aa 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -872,6 +872,14 @@ namespace Microsoft.Dafny {
           PrintExpressionList(t.Arguments);

           wr.Write(")");

         }

+      } else if (rhs is CallRhs) {

+        var r = (CallRhs)rhs;

+        if (!(r.Receiver is ImplicitThisExpr)) {

+          PrintExpr(r.Receiver, 0x70, false, false, -1);

+          wr.Write(".");

+        }

+        wr.Write("{0}", r.MethodName);

+        PrintActualArguments(r.Args, r.MethodName);

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected RHS

       }

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index a3749372..cc26eea2 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1167,6 +1167,9 @@ namespace Microsoft.Dafny
         // fill in the postconditions and bodies of prefix methods

         foreach (var com in ModuleDefinition.AllCoMethods(declarations)) {

           var prefixMethod = com.PrefixMethod;

+          if (prefixMethod == null) {

+            continue;  // something went wrong during registration of the prefix method (probably a duplicated comethod name)

+          }

           Contract.Assume(prefixMethod.Ens.Count == 0 && prefixMethod.Body == null);  // there are not supposed have have been filled in before

           // compute the postconditions of the prefix method

           var k = prefixMethod.Ins[0];

@@ -2146,8 +2149,10 @@ namespace Microsoft.Dafny
           ResolveTypeParameters(m.TypeArgs, true, m);

           ResolveMethodSignature(m);

           allTypeParameters.PopMarker();

-          if (m is CoMethod && ec == ErrorCount) {

-            var mm = ((CoMethod)m).PrefixMethod;

+          var com = m as CoMethod;

+          if (com != null && com.PrefixMethod != null && ec == ErrorCount) {

+            var mm = com.PrefixMethod;

+            // resolve signature of the prefix method

             mm.EnclosingClass = cl;

             allTypeParameters.PushMarker();

             ResolveTypeParameters(mm.TypeArgs, true, mm);

@@ -2684,10 +2689,11 @@ namespace Microsoft.Dafny
 

       // Resolve body

       if (m.Body != null) {

-        if (m is CoMethod) {

+        var com = m as CoMethod;

+        if (com != null && com.PrefixMethod != null) {

           // The body may mentioned the implicitly declared parameter _k.  Throw it into the

           // scope before resolving the body.

-          var k = ((CoMethod)m).PrefixMethod.Ins[0];

+          var k = com.PrefixMethod.Ins[0];

           scope.Push(k.Name, k);  // we expect no name conflict for _k

         }

         var codeContext = m;

@@ -3981,6 +3987,10 @@ namespace Microsoft.Dafny
           isEffectful = tr.InitCall != null;

         } else if (rhs is HavocRhs) {

           isEffectful = false;

+        } else if (rhs is CallRhs) {

+          // (a CallRhs is never parsed; we must have got here from an act of cloning)

+          isEffectful = true;

+          callRhs = callRhs ?? (CallRhs)rhs;

         } else {

           var er = (ExprRhs)rhs;

           if (er.Expr is IdentifierSequence) {

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index d097de11..afc075e5 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5852,20 +5852,13 @@ namespace Microsoft.Dafny {
       // Figure out if the call is recursive or not, which will be used below to determine the need for a

       // termination check and the need to include an implicit _k-1 argument.

       bool isRecursiveCall = false;

-      if (method is PrefixMethod) {

-        // An explicit call to a prefix method is allowed only within the corresponding comethod's SCC, so

-        // this is really a recursive call.

-        Contract.Assert(codeContext is PrefixMethod);  // sanity check

-        isRecursiveCall = true;

-      } else {

-        // consult the call graph to figure out if this is a recursive call

-        var module = method.EnclosingClass.Module;

-        if (module == currentModule) {

-          // Note, prefix methods are not recorded in the call graph, but their corresponding comethods are.

-          Method cllr = caller is PrefixMethod ? ((PrefixMethod)caller).Co : caller;

-          if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(cllr)) {

-            isRecursiveCall = true;

-          }

+      // consult the call graph to figure out if this is a recursive call

+      var module = method.EnclosingClass.Module;

+      if (module == currentModule) {

+        // Note, prefix methods are not recorded in the call graph, but their corresponding comethods are.

+        Method cllr = caller is PrefixMethod ? ((PrefixMethod)caller).Co : caller;

+        if (module.CallGraph.GetSCCRepresentative(method) == module.CallGraph.GetSCCRepresentative(cllr)) {

+          isRecursiveCall = true;

         }

       }

 

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 760e6880..13e7a8b0 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1336,6 +1336,20 @@ CoResolution.dfy(92,4): Error: a recursive call from a comethod can go only to o
 10 resolution/type errors detected in CoResolution.dfy

 

 -------------------- CoPrefix.dfy --------------------

+CoPrefix.dfy(161,3): Error BP5003: A postcondition might not hold on this return path.

+CoPrefix.dfy(160,15): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+CoPrefix.dfy(166,3): Error BP5003: A postcondition might not hold on this return path.

+CoPrefix.dfy(165,15): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Else

+CoPrefix.dfy(173,5): Error: cannot prove termination; try supplying a decreases clause

+Execution trace:

+    (0,0): anon0

+    (0,0): anon3_Then

 CoPrefix.dfy(60,7): Error: failure to decrease termination measure

 Execution trace:

     (0,0): anon0

@@ -1370,7 +1384,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon3_Else

 

-Dafny program verifier finished with 24 verified, 6 errors

+Dafny program verifier finished with 41 verified, 9 errors

 

 -------------------- CoinductiveProofs.dfy --------------------

 CoinductiveProofs.dfy(26,12): Error: assertion violation

diff --git a/Test/dafny0/CoPrefix.dfy b/Test/dafny0/CoPrefix.dfy
index 991e160f..d3cecc28 100644
--- a/Test/dafny0/CoPrefix.dfy
+++ b/Test/dafny0/CoPrefix.dfy
@@ -148,3 +148,44 @@ comethod {:induction false} BadTheorem(s: IList)
 {  // error: postcondition violation

   BadTheorem(s.tail);

 }

+

+// ---------------------------------

+

+// Make sure recursive calls get checked for termination

+module Recursion {

+  comethod X() { Y(); }

+  comethod Y() { X(); }

+

+  comethod G(x: int)

+    ensures x < 100;

+  {  // error: postcondition violation (when _k == 0)

+    H(x);

+  }

+  comethod H(x: int)

+    ensures x < 100;

+  {  // error: postcondition violation (when _k == 0)

+    G(x);

+  }

+  

+  comethod A(x: int) { B(x); }

+  comethod B(x: int)

+  {

+    A#[10](x);  // error: this is a recursive call, and the termination metric may not be going down

+  }

+  

+  comethod A'(x: int) { B'(x); }

+  comethod B'(x: int)

+  {

+    if (10 < _k) {

+      A'#[10](x);

+    }

+  }

+  

+  comethod A''(x: int) { B''(x); }

+  comethod B''(x: int)

+  {

+    if (0 < x) {

+      A''#[_k](x-1);

+    }

+  }

+}

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index 9cd8fc82..c4e75986 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -14,3 +14,11 @@ Dafny program verifier finished with 11 verified, 0 errors
 -------------------- CachedContainer.dfy --------------------

 

 Dafny program verifier finished with 47 verified, 0 errors

+

+-------------------- SimpleCoinduction.dfy --------------------

+

+Dafny program verifier finished with 28 verified, 0 errors

+

+-------------------- CalcExample.dfy --------------------

+

+Dafny program verifier finished with 6 verified, 0 errors

diff --git a/Test/dafny3/CalcExample.dfy b/Test/dafny3/CalcExample.dfy
new file mode 100644
index 00000000..c94c18d2
--- /dev/null
+++ b/Test/dafny3/CalcExample.dfy
@@ -0,0 +1,27 @@
+function f(x: int, y: int): int

+

+ghost method Associativity(x: int, y: int, z: int)

+  ensures f(x, f(y, z)) == f(f(x, y), z);

+

+ghost method Monotonicity(y: int, z: int)

+  requires y <= z;

+  ensures forall x :: f(x, y) <= f(x, z);

+

+ghost method DiagonalIdentity(x: int)

+  ensures f(x, x) == x;

+

+method M(a: int, b: int, c: int, x: int)

+  requires c <= x == f(a, b);

+{

+  calc {

+    f(a, f(b, c));

+    { Associativity(a, b, c); }

+    f(f(a, b), c);

+    { assert f(a, b) == x; }

+    f(x, c);

+    { assert c <= x; Monotonicity(c, x); }

+    <= f(x, x);

+    { DiagonalIdentity(x); }

+    x;

+  }

+}

diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy
new file mode 100644
index 00000000..5a8ab288
--- /dev/null
+++ b/Test/dafny3/SimpleCoinduction.dfy
@@ -0,0 +1,115 @@
+codatatype Stream<T> = Cons(head: T, tail: Stream);

+codatatype IList<T> = Nil | ICons(head: T, tail: IList);

+

+// -----------------------------------------------------------------------

+

+copredicate Pos(s: Stream<int>)

+{

+  s.head > 0 && Pos(s.tail)

+}

+

+function Up(n: int): Stream<int>

+{

+  Cons(n, Up(n+1))

+}

+

+function Inc(s: Stream<int>): Stream<int>

+{

+  Cons(s.head + 1, Inc(s.tail))

+}

+

+ghost method {:induction false} UpLemma(k: nat, n: int)

+  ensures Inc(Up(n)) ==#[k] Up(n+1);

+{

+  if (k != 0) {

+    UpLemma(k-1, n+1);

+  }

+}

+

+comethod {:induction false} CoUpLemma(n: int)

+  ensures Inc(Up(n)) == Up(n+1);

+{

+  CoUpLemma(n+1);

+}

+

+ghost method UpLemma_Auto(k: nat, n: int)

+  ensures Inc(Up(n)) ==#[k] Up(n+1);

+{

+}

+

+comethod CoUpLemma_Auto(n: int)

+  ensures Inc(Up(n)) == Up(n+1);

+{

+}

+

+// -----------------------------------------------------------------------

+

+function Repeat(n: int): Stream<int>

+{

+  Cons(n, Repeat(n))

+}

+

+comethod RepeatLemma(n: int)

+  ensures Inc(Repeat(n)) == Repeat(n+1);

+{

+}

+

+// -----------------------------------------------------------------------

+

+copredicate True(s: Stream)

+{

+  True(s.tail)

+}

+

+comethod AlwaysTrue(s: Stream)

+  ensures True(s);

+{

+  AlwaysTrue(s.tail);  // WHY does this not happen automatically? (Because 's' is not quantified over)

+}

+

+copredicate AlsoTrue(s: Stream)

+{

+  AlsoTrue(s)

+}

+

+comethod AlsoAlwaysTrue(s: Stream)

+  ensures AlsoTrue(s);

+{

+  // AlsoAlwaysTrue(s);  // here, the recursive call is not needed, because it uses the same 's', so 's' does not need to be quantified over

+}

+

+// -----------------------------------------------------------------------

+

+function Append(M: IList, N: IList): IList

+{

+  match M

+  case Nil => N

+  case ICons(x, M') => ICons(x, Append(M', N))

+}

+

+function zeros(): IList<int>

+{

+  ICons(0, zeros())

+}

+

+function ones(): IList<int>

+{

+  ICons(1, ones())

+}

+

+copredicate AtMost(a: IList<int>, b: IList<int>)

+{

+  match a

+  case Nil => true

+  case ICons(h,t) => b.ICons? && h <= b.head && AtMost(t, b.tail)

+}

+

+comethod ZerosAndOnes_Theorem0()

+  ensures AtMost(zeros(), ones());

+{

+}

+

+comethod ZerosAndOnes_Theorem1()

+  ensures Append(zeros(), ones()) == zeros();

+{

+}

diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat
index 2ebba74a..83d2bba9 100644
--- a/Test/dafny3/runtest.bat
+++ b/Test/dafny3/runtest.bat
@@ -4,7 +4,10 @@ setlocal
 set BINARIES=..\..\Binaries

 set DAFNY_EXE=%BINARIES%\Dafny.exe

 

-for %%f in (Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy) do (

+for %%f in (

+  Iter.dfy Streams.dfy Dijkstra.dfy CachedContainer.dfy

+  SimpleCoinduction.dfy CalcExample.dfy

+) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f