Dafny: added support for co-recursive calls

4 files changed, 200 insertions, 77 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 56654ccd..6e99ea93 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -186,7 +186,35 @@ namespace Microsoft.Dafny {
     }

 

     void CompileDatatypeConstructors(DatatypeDecl dt, int indent)

-    {Contract.Requires(dt != null);

+    {

+      Contract.Requires(dt != null);

+

+      string typeParams = dt.TypeArgs.Count == 0 ? "" : string.Format("<{0}>", TypeParameters(dt.TypeArgs));

+      if (dt is CoDatatypeDecl) {

+        // public class Dt__Lazy<T> : Base_Dt<T> {

+        //   public delegate Base_Dt<T> Computer();

+        //   public delegate Computer ComputerComputer();

+        //   Computer c;

+        //   public Dt__Lazy(Computer c) { this.c = c; }

+        //   public Base_Dt<T> Get() { return c(); }

+        // }

+        Indent(indent);

+        wr.WriteLine("public class {0}__Lazy{1} : Base_{0}{1} {{", dt.Name, typeParams);

+        int ind = indent + IndentAmount;

+        Indent(ind);

+        wr.WriteLine("public delegate Base_{0}{1} Computer();", dt.Name, typeParams);

+        Indent(ind);

+        wr.WriteLine("public delegate Computer ComputerComputer();");

+        Indent(ind);

+        wr.WriteLine("Computer c;");

+        Indent(ind);

+        wr.WriteLine("public {0}__Lazy(Computer c) {{ this.c = c; }}", dt.Name);

+        Indent(ind);

+        wr.WriteLine("public Base_{0}{1} Get() {{ return c(); }}", dt.Name, typeParams);

+        Indent(indent);

+        wr.WriteLine("}");

+      }

+

       foreach (DatatypeCtor ctor in dt.Ctors) {

         // class Dt_Ctor<T,U> : Base_Dt<T> {

         //   Fields;

@@ -203,11 +231,7 @@ namespace Microsoft.Dafny {
         // }

         Indent(indent);

         wr.Write("public class {0}", DtCtorName(ctor, dt.TypeArgs));

-        wr.Write(" : Base_{0}", dt.Name);

-        if (dt.TypeArgs.Count != 0) {

-          wr.Write("<{0}>", TypeParameters(dt.TypeArgs));

-        }

-        wr.WriteLine(" {");

+        wr.WriteLine(" : Base_{0}{1} {{", dt.Name, typeParams);

         int ind = indent + IndentAmount;

 

         int i = 0;

@@ -270,7 +294,14 @@ namespace Microsoft.Dafny {
       // public struct Dt<T> {

       //   Base_Dt<T> d;

       //   public Base_Dt<T> _D {

-      //     get { if (d == null) { d = Default; } return d; }

+      //     get {

+      //       if (d == null) {

+      //         d = Default;

+      //       } else if (d is Dt__Lazy<T>) {        // co-datatypes only

+      //         d = ((Dt__Lazy<T>)d).Get();         // co-datatypes only

+      //       }

+      //       return d;

+      //     }

       //   }

       //   public Dt(Base_Dt<T> d) { this.d = d; }

       //   static Base_Dt<T> theDefault;

@@ -310,7 +341,21 @@ namespace Microsoft.Dafny {
       Indent(ind);

       wr.WriteLine("public Base_{0} _D {{", DtT);

       Indent(ind + IndentAmount);

-      wr.WriteLine("get { if (d == null) { d = Default; } return d; }");

+      wr.WriteLine("get {");

+      Indent(ind + 2 * IndentAmount);

+      wr.WriteLine("if (d == null) {");

+      Indent(ind + 3 * IndentAmount);

+      wr.WriteLine("d = Default;");

+      if (dt is CoDatatypeDecl) {

+        string typeParams = dt.TypeArgs.Count == 0 ? "" : string.Format("<{0}>", TypeParameters(dt.TypeArgs));

+        Indent(ind + 2 * IndentAmount);

+        wr.WriteLine("}} else if (d is {0}__Lazy{1}) {{", dt.Name, typeParams);

+        Indent(ind + 3 * IndentAmount);

+        wr.WriteLine("d = (({0}__Lazy{1})d).Get();", dt.Name, typeParams);

+      }

+      Indent(ind + 2 * IndentAmount);  wr.WriteLine("}");

+      Indent(ind + 2 * IndentAmount);  wr.WriteLine("return d;");

+      Indent(ind + IndentAmount);  wr.WriteLine("}");

       Indent(ind);  wr.WriteLine("}");

 

       Indent(ind);

@@ -1581,43 +1626,80 @@ namespace Microsoft.Dafny {
 

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

-        Function f = cce.NonNull(e.Function);

-        if (f.IsStatic) {

-          wr.Write(TypeName(cce.NonNull(e.Receiver.Type)));

-        } else {

-          TrParenExpr(e.Receiver);

-        }

-        wr.Write(".@{0}", f.Name);

-        wr.Write("(");

-        string sep = "";

-        for (int i = 0; i < e.Args.Count; i++) {

-          if (!e.Function.Formals[i].IsGhost) {

-            wr.Write(sep);

-            TrExpr(e.Args[i]);

-            sep = ", ";

-          }

-        }

-        wr.Write(")");

+        CompileFunctionCallExpr(e, wr, TrExpr);

 

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         Contract.Assert(dtv.Ctor != null);  // since dtv has been successfully resolved

-        wr.Write("new {0}", dtv.DatatypeName);

-        if (dtv.InferredTypeArgs.Count != 0) {

-          wr.Write("<{0}>", TypeNames(dtv.InferredTypeArgs));

-        }

-        wr.Write("(new {0}", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs));

-        wr.Write("(");

-        string sep = "";

-        for (int i = 0; i < dtv.Arguments.Count; i++) {

-          Formal formal = dtv.Ctor.Formals[i];

-          if (!formal.IsGhost) {

-            wr.Write(sep);

-            TrExpr(dtv.Arguments[i]);

-            sep = ", ";

+        var typeParams = dtv.InferredTypeArgs.Count == 0 ? "" : string.Format("<{0}>", TypeNames(dtv.InferredTypeArgs));

+

+        wr.Write("new {0}{1}(", dtv.DatatypeName, typeParams);

+        if (!dtv.IsCoCall) {

+          // For an ordinary constructor (that is, one that does not guard any co-recursive calls), generate:

+          //   new Dt_Cons<T>( args )

+          wr.Write("new {0}(", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs));

+          string sep = "";

+          for (int i = 0; i < dtv.Arguments.Count; i++) {

+            Formal formal = dtv.Ctor.Formals[i];

+            if (!formal.IsGhost) {

+              wr.Write(sep);

+              TrExpr(dtv.Arguments[i]);

+              sep = ", ";

+            }

           }

+          wr.Write(")");

+        } else {

+          // In the case of a co-recursive call, generate:

+          //     new Dt__Lazy<T>( new Dt__Lazy<T>.ComputerComputer( LAMBDA )() )

+          // where LAMBDA is:

+          //     () => { var someLocals = eagerlyEvaluatedArguments;

+          //             return () => { return Dt_Cons<T>( ...args...using someLocals and including function calls to be evaluated lazily... ); };

+          //           }

+          wr.Write("new {0}__Lazy{1}", dtv.DatatypeName, typeParams);

+          wr.Write("(new {0}__Lazy{1}.ComputerComputer(() => {{ ", dtv.DatatypeName, typeParams);

+

+          // locals

+          string args = "";

+          string sep = "";

+          for (int i = 0; i < dtv.Arguments.Count; i++) {

+            Formal formal = dtv.Ctor.Formals[i];

+            if (!formal.IsGhost) {

+              Expression actual = dtv.Arguments[i].Resolved;

+              string arg;

+              var fce = actual as FunctionCallExpr;

+              if (fce == null || fce.CoCall != FunctionCallExpr.CoCallResolution.Yes) {

+                string varName = "_ac" + tmpVarCount;

+                tmpVarCount++;

+                arg = varName;

+

+                wr.Write("var {0} = ", varName);

+                TrExpr(actual);

+                wr.Write("; ");

+              } else {

+                var sw = new StringWriter();

+                CompileFunctionCallExpr(fce, sw, (exp) => {

+                  string varName = "_ac" + tmpVarCount;

+                  tmpVarCount++;

+                  sw.Write(varName);

+

+                  wr.Write("var {0} = ", varName);

+                  TrExpr(exp);

+                  wr.Write("; ");

+

+                });

+                arg = sw.ToString();

+              }

+              args += sep + arg;

+              sep = ", ";

+            }

+          }

+

+          wr.Write("return () => { return ");

+

+          wr.Write("new {0}({1}", DtCtorName(dtv.Ctor, dtv.InferredTypeArgs), args);

+          wr.Write("); }; })())");

         }

-        wr.Write("))");

+        wr.Write(")");

 

       } else if (expr is OldExpr) {

         Contract.Assert(false); throw new cce.UnreachableException();  // 'old' is always a ghost (right?)

@@ -1938,5 +2020,29 @@ namespace Microsoft.Dafny {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

       }

     }

+

+    delegate void FCE_Arg_Translator(Expression e);

+

+    void CompileFunctionCallExpr(FunctionCallExpr e, TextWriter twr, FCE_Arg_Translator tr) {

+      Function f = cce.NonNull(e.Function);

+      if (f.IsStatic) {

+        twr.Write(TypeName(cce.NonNull(e.Receiver.Type)));

+      } else {

+        twr.Write("(");

+        tr(e.Receiver);

+        twr.Write(")");

+      }

+      twr.Write(".@{0}", f.Name);

+      twr.Write("(");

+      string sep = "";

+      for (int i = 0; i < e.Args.Count; i++) {

+        if (!e.Function.Formals[i].IsGhost) {

+          twr.Write(sep);

+          tr(e.Args[i]);

+          sep = ", ";

+        }

+      }

+      twr.Write(")");

+    }

   }

 }

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index ffe39618..27f06518 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2328,6 +2328,7 @@ namespace Microsoft.Dafny {
     public readonly List<Expression/*!*/>/*!*/ Arguments;

     public DatatypeCtor Ctor;  // filled in by resolution

     public List<Type/*!*/> InferredTypeArgs = new List<Type>();  // filled in by resolution

+    public bool IsCoCall;  // filled in by resolution

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(DatatypeName != null);

@@ -2554,6 +2555,8 @@ namespace Microsoft.Dafny {
     public readonly Expression/*!*/ Receiver;

     public readonly IToken OpenParen;  // can be null if Args.Count == 0

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

+    public enum CoCallResolution { No, Yes, NoBecauseFunctionHasSideEffects }

+    public CoCallResolution CoCall = CoCallResolution.No;  // indicates whether or not the call is a co-recursive call; filled in by resolution

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index daeef80c..63048637 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -727,7 +727,7 @@ namespace Microsoft.Dafny {
       }

       if (f.Body != null) {

         List<IVariable> matchVarContext = new List<IVariable>(f.Formals);

-        ResolveExpression(f.Body, false, matchVarContext);

+        ResolveExpression(f.Body, false, matchVarContext, null);

         if (!f.IsGhost) {

           CheckIsNonGhost(f.Body);

         }

@@ -931,7 +931,7 @@ namespace Microsoft.Dafny {
                 if (allowAutoTypeArguments) {

                   // add to defaultTypeArguments the necessary number of arguments

                   for (int i = defaultTypeArguments.Count; i < d.TypeArgs.Count; i++) {

-                    defaultTypeArguments.Add(new TypeParameter(t.tok, "T$" + i));

+                    defaultTypeArguments.Add(new TypeParameter(t.tok, "_T" + i));

                   }

                 }

                 if (allowAutoTypeArguments || d.TypeArgs.Count == defaultTypeArguments.Count) {

@@ -1806,11 +1806,11 @@ namespace Microsoft.Dafny {
           } else {

             var er = (ExprRhs)rhs;

             if (er.Expr is IdentifierSequence) {

-              var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, true, true);

+              var cRhs = ResolveIdentifierSequence((IdentifierSequence)er.Expr, true, true, null);

               isEffectful = cRhs != null;

               callRhs = callRhs ?? cRhs;

             } else if (er.Expr is FunctionCallExpr) {

-              var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, true, true);

+              var cRhs = ResolveFunctionCallExpr((FunctionCallExpr)er.Expr, true, true, null);

               isEffectful = cRhs != null;

               callRhs = callRhs ?? cRhs;

             } else {

@@ -2459,14 +2459,14 @@ namespace Microsoft.Dafny {
     /// "twoState" implies that "old" and "fresh" expressions are allowed

     /// </summary>

     void ResolveExpression(Expression expr, bool twoState) {

-      ResolveExpression(expr, twoState, null);

+      ResolveExpression(expr, twoState, null, null);

     }

 

     /// <summary>

     /// "matchVarContext" says which variables are allowed to be used as the source expression in a "match" expression;

     /// if null, no "match" expression will be allowed.

     /// </summary>

-    void ResolveExpression(Expression expr, bool twoState, List<IVariable> matchVarContext) {

+    void ResolveExpression(Expression expr, bool twoState, List<IVariable> matchVarContext, DatatypeValue coContext) {

       Contract.Requires(expr != null);

       Contract.Requires(currentClass != null);

       Contract.Ensures(expr.Type != null);

@@ -2482,7 +2482,7 @@ namespace Microsoft.Dafny {
 

       if (expr is ParensExpression) {

         var e = (ParensExpression)expr;

-        ResolveExpression(e.E, twoState, matchVarContext);  // allow "match" expressions inside e.E if the parenthetic expression had been allowed to be a "match" expression

+        ResolveExpression(e.E, twoState, matchVarContext, coContext);  // allow "match" expressions inside e.E if the parenthetic expression had been allowed to be a "match" expression

         e.ResolvedExpression = e.E;

         e.Type = e.E.Type;

 

@@ -2494,7 +2494,7 @@ namespace Microsoft.Dafny {
 

       } else if (expr is IdentifierSequence) {

         var e = (IdentifierSequence)expr;

-        ResolveIdentifierSequence(e, twoState, false);

+        ResolveIdentifierSequence(e, twoState, false, coContext);

 

       } else if (expr is LiteralExpr) {

         LiteralExpr e = (LiteralExpr)expr;

@@ -2559,7 +2559,7 @@ namespace Microsoft.Dafny {
           int j = 0;

           foreach (Expression arg in dtv.Arguments) {

             Formal formal = ctor != null && j < ctor.Formals.Count ? ctor.Formals[j] : null;

-            ResolveExpression(arg, twoState);

+            ResolveExpression(arg, twoState, null, ctor != null && ctor.EnclosingDatatype is CoDatatypeDecl ? dtv : null);

             Contract.Assert(arg.Type != null);  // follows from postcondition of ResolveExpression

             if (formal != null) {

               Type st = SubstType(formal.Type, subst);

@@ -2681,14 +2681,14 @@ namespace Microsoft.Dafny {
 

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

-        ResolveFunctionCallExpr(e, twoState, false);

+        ResolveFunctionCallExpr(e, twoState, false, coContext);

 

       } else if (expr is OldExpr) {

         OldExpr e = (OldExpr)expr;

         if (!twoState) {

           Error(expr, "old expressions are not allowed in this context");

         }

-        ResolveExpression(e.E, twoState);

+        ResolveExpression(e.E, twoState, null, coContext);

         expr.Type = e.E.Type;

 

       } else if (expr is MultiSetFormingExpr) {

@@ -3100,7 +3100,7 @@ namespace Microsoft.Dafny {
             innerMatchVarContext.Remove(goodMatchVariable);  // this variable is no longer available for matching

           }

           innerMatchVarContext.AddRange(mc.Arguments);

-          ResolveExpression(mc.Body, twoState, innerMatchVarContext);

+          ResolveExpression(mc.Body, twoState, innerMatchVarContext, null);

           Contract.Assert(mc.Body.Type != null);  // follows from postcondition of ResolveExpression

           if (!UnifyTypes(expr.Type, mc.Body.Type)) {

             Error(mc.Body.tok, "type of case bodies do not agree (found {0}, previous types {1})", mc.Body.Type, expr.Type);

@@ -3228,8 +3228,9 @@ namespace Microsoft.Dafny {
     /// If "!allowMethodCall" or if what is being called does not refer to a method, resolves "e" and returns "null".

     /// Otherwise (that is, if "allowMethodCall" and what is being called refers to a method), resolves the receiver

     /// of "e" but NOT the arguments, and returns a CallRhs corresponding to the call.

+    /// "coContext" is to be non-null if this function call is a direct argument to a co-constructor.

     /// </summary>

-    CallRhs ResolveFunctionCallExpr(FunctionCallExpr e, bool twoState, bool allowMethodCall) {

+    CallRhs ResolveFunctionCallExpr(FunctionCallExpr e, bool twoState, bool allowMethodCall, DatatypeValue coContext) {

       ResolveReceiver(e.Receiver, twoState);

       Contract.Assert(e.Receiver.Type != null);  // follows from postcondition of ResolveExpression

       NonProxyType nptype;

@@ -3294,17 +3295,25 @@ namespace Microsoft.Dafny {
         }

 

         // Resolution termination check

-        if (currentFunction != null && currentFunction.EnclosingClass != null && function.EnclosingClass != null) {

-          ModuleDecl callerModule = currentFunction.EnclosingClass.Module;

-          ModuleDecl calleeModule = function.EnclosingClass.Module;

-          if (callerModule == calleeModule) {

-            // intra-module call; this is allowed; add edge in module's call graph

-            callerModule.CallGraph.AddEdge(currentFunction, function);

-            if (currentFunction == function) {

-              currentFunction.IsRecursive = true;  // self recursion (mutual recursion is determined elsewhere)

+        if (coContext != null && function.Reads.Count == 0) {

+          e.CoCall = FunctionCallExpr.CoCallResolution.Yes;

+          coContext.IsCoCall = true;

+        } else {

+          if (coContext != null) {

+            e.CoCall = FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasSideEffects;

+          }

+          if (currentFunction != null && currentFunction.EnclosingClass != null && function.EnclosingClass != null) {

+            ModuleDecl callerModule = currentFunction.EnclosingClass.Module;

+            ModuleDecl calleeModule = function.EnclosingClass.Module;

+            if (callerModule == calleeModule) {

+              // intra-module call; this is allowed; add edge in module's call graph

+              callerModule.CallGraph.AddEdge(currentFunction, function);

+              if (currentFunction == function) {

+                currentFunction.IsRecursive = true;  // self recursion (mutual recursion is determined elsewhere)

+              }

+            } else {

+              Contract.Assert(importGraph.Reaches(callerModule, calleeModule));

             }

-          } else {

-            Contract.Assert(importGraph.Reaches(callerModule, calleeModule));

           }

         }

       }

@@ -3315,7 +3324,7 @@ namespace Microsoft.Dafny {
     /// If "!allowMethodCall", or if "e" does not designate a method call, resolves "e" and returns "null".

     /// Otherwise, resolves all sub-parts of "e" and returns a (resolved) CallRhs expression representing the call.

     /// </summary>

-    CallRhs ResolveIdentifierSequence(IdentifierSequence e, bool twoState, bool allowMethodCall) {

+    CallRhs ResolveIdentifierSequence(IdentifierSequence e, bool twoState, bool allowMethodCall, DatatypeValue coContext) {

       // Look up "id" as follows:

       //  - local variable, parameter, or bound variable (if this clashes with something of interest, one can always rename the local variable locally)

       //  - unamibugous type name (class or datatype or arbitrary-type) (if two imported types have the same name, an error message is produced here)

@@ -3335,7 +3344,7 @@ namespace Microsoft.Dafny {
         // ----- root is a local variable, parameter, or bound variable

         r = new IdentifierExpr(id, id.val);

         ResolveExpression(r, twoState);

-        r = ResolveSuffix(r, e, 1, twoState, allowMethodCall, out call);

+        r = ResolveSuffix(r, e, 1, twoState, allowMethodCall, coContext, out call);

 

       } else if (classes.TryGetValue(id.val, out decl)) {

         if (decl is AmbiguousTopLevelDecl) {

@@ -3351,7 +3360,7 @@ namespace Microsoft.Dafny {
         } else if (decl is ClassDecl) {

           // ----- root is a class

           var cd = (ClassDecl)decl;

-          r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, twoState, allowMethodCall, out call);

+          r = ResolveSuffix(new StaticReceiverExpr(id, cd), e, 1, twoState, allowMethodCall, coContext, out call);

 

         } else {

           // ----- root is a datatype

@@ -3360,7 +3369,7 @@ namespace Microsoft.Dafny {
           r = new DatatypeValue(id, id.val, e.Tokens[1].val, args);

           ResolveExpression(r, twoState);

           if (e.Tokens.Count != 2) {

-            r = ResolveSuffix(r, e, 2, twoState, allowMethodCall, out call);

+            r = ResolveSuffix(r, e, 2, twoState, allowMethodCall, coContext, out call);

           }

         }

 

@@ -3374,7 +3383,7 @@ namespace Microsoft.Dafny {
           r = new DatatypeValue(id, pair.Item1.EnclosingDatatype.Name, id.val, args);

           ResolveExpression(r, twoState);

           if (e.Tokens.Count != 1) {

-            r = ResolveSuffix(r, e, 1, twoState, allowMethodCall, out call);

+            r = ResolveSuffix(r, e, 1, twoState, allowMethodCall, coContext, out call);

           }

         }

 

@@ -3391,7 +3400,7 @@ namespace Microsoft.Dafny {
           receiver = new ImplicitThisExpr(id);

           receiver.Type = GetThisType(id, currentClass);  // resolve here

         }

-        r = ResolveSuffix(receiver, e, 0, twoState, allowMethodCall, out call);

+        r = ResolveSuffix(receiver, e, 0, twoState, allowMethodCall, coContext, out call);

 

       } else {

         Error(id, "unresolved identifier: {0}", id.val);

@@ -3417,7 +3426,7 @@ namespace Microsoft.Dafny {
     /// Except, if "allowMethodCall" is "true" and the would-be-returned value designates a method

     /// call, instead returns null and returns "call" as a non-null value.

     /// </summary>

-    Expression ResolveSuffix(Expression r, IdentifierSequence e, int p, bool twoState, bool allowMethodCall, out CallRhs call) {

+    Expression ResolveSuffix(Expression r, IdentifierSequence e, int p, bool twoState, bool allowMethodCall, DatatypeValue coContext, out CallRhs call) {

       Contract.Requires(r != null);

       Contract.Requires(e != null);

       Contract.Requires(0 <= p && p <= e.Tokens.Count);

@@ -3430,7 +3439,7 @@ namespace Microsoft.Dafny {
         var resolved = ResolvePredicateOrField(e.Tokens[p], r, e.Tokens[p].val);

         if (resolved != null) {

           r = resolved;

-          ResolveExpression(r, twoState);

+          ResolveExpression(r, twoState, null, p == e.Tokens.Count - 1 ? coContext : null);

         }

       }

 

@@ -3450,7 +3459,7 @@ namespace Microsoft.Dafny {
           r = null;

         } else {

           r = new FunctionCallExpr(e.Tokens[p], e.Tokens[p].val, r, e.OpenParen, e.Arguments);

-          ResolveExpression(r, twoState);

+          ResolveExpression(r, twoState, null, coContext);

         }

       } else if (e.Arguments != null) {

         Contract.Assert(p == e.Tokens.Count);

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 982416f4..b2b2bdc9 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2319,7 +2319,7 @@ namespace Microsoft.Dafny {
             CheckFrameSubset(expr.tok, e.Function.Reads, e.Receiver, substMap, etran, builder, "insufficient reads clause to invoke function", options.AssertKv);

           }

 

-          if (options.Decr != null) {

+          if (options.Decr != null && e.CoCall != FunctionCallExpr.CoCallResolution.Yes) {

             // check that the decreases measure goes down

             ModuleDecl module = cce.NonNull(e.Function.EnclosingClass).Module;

             if (module == cce.NonNull(options.Decr.EnclosingClass).Module) {

@@ -2338,7 +2338,8 @@ namespace Microsoft.Dafny {
                     allowance = BplAnd(allowance, Bpl.Expr.Eq(etran.TrExpr(ee), new Bpl.IdentifierExpr(e.tok, ff.UniqueName, TrType(ff.Type))));

                   }

                 }

-                CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, allowance, e.Receiver, substMap, etran, builder, contextDecrInferred);

+                CheckCallTermination(expr.tok, contextDecreases, calleeDecreases, allowance, e.Receiver, substMap, etran, builder,

+                  contextDecrInferred, e.CoCall == FunctionCallExpr.CoCallResolution.NoBecauseFunctionHasSideEffects);

               }

             }

           }

@@ -4261,7 +4262,7 @@ namespace Microsoft.Dafny {
           bool contextDecrInferred, calleeDecrInferred;

           List<Expression> contextDecreases = MethodDecreasesWithDefault(currentMethod, out contextDecrInferred);

           List<Expression> calleeDecreases = MethodDecreasesWithDefault(method, out calleeDecrInferred);

-          CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, etran, builder, contextDecrInferred);

+          CheckCallTermination(tok, contextDecreases, calleeDecreases, null, receiver, substMap, etran, builder, contextDecrInferred, false);

         }

       }

 

@@ -4431,7 +4432,7 @@ namespace Microsoft.Dafny {
     void CheckCallTermination(IToken/*!*/ tok, List<Expression/*!*/>/*!*/ contextDecreases, List<Expression/*!*/>/*!*/ calleeDecreases,

                               Bpl.Expr allowance,

                               Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/>/*!*/ substMap,

-                              ExpressionTranslator/*!*/ etran, Bpl.StmtListBuilder/*!*/ builder, bool inferredDecreases) {

+                              ExpressionTranslator/*!*/ etran, Bpl.StmtListBuilder/*!*/ builder, bool inferredDecreases, bool wouldBeCoCallButCallHasSideEffects) {

       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(contextDecreases));

       Contract.Requires(cce.NonNullElements(calleeDecreases));

@@ -4467,7 +4468,11 @@ namespace Microsoft.Dafny {
       if (allowance != null) {

         decrExpr = Bpl.Expr.Or(allowance, decrExpr);

       }

-      builder.Add(Assert(tok, decrExpr, inferredDecreases ? "cannot prove termination; try supplying a decreases clause" : "failure to decrease termination measure"));

+      var msg = inferredDecreases ? "cannot prove termination; try supplying a decreases clause" : "failure to decrease termination measure";

+      if (wouldBeCoCallButCallHasSideEffects) {

+        msg += " (note that only functions without side effects can called co-recursively)";

+      }

+      builder.Add(Assert(tok, decrExpr, msg));

     }

 

     /// <summary>

@@ -6938,7 +6943,7 @@ namespace Microsoft.Dafny {
         var e = (FunctionCallExpr)expr;

         // For recursive functions:  arguments are "prominent"

         // For non-recursive function:  arguments are "prominent" if the call is

-        var rec = e.Function.IsRecursive;

+        var rec = e.Function.IsRecursive && e.CoCall != FunctionCallExpr.CoCallResolution.Yes;

         bool inferredDecreases;  // we don't actually care

         var decr = FunctionDecreasesWithDefault(e.Function, out inferredDecreases);

         bool variantArgument;