Unfinished code -- please forgive (I'm switching machines and will fix shortly)

2 files changed, 72 insertions, 6 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index a8c3f56d..45ea1e83 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -2039,6 +2039,21 @@ namespace Microsoft.Dafny {
     public bool SignatureIsOmitted { get { return SignatureEllipsis != null; } }  // is "false" for all Function objects that survive into resolution

     public readonly IToken SignatureEllipsis;

     public bool IsBuiltin;

+

+    /// <summary>

+    /// The "AllCalls" field is used for non-CoPredicate, non-PrefixPredicate functions only (so its value should not be relied upon for CoPredicate and PrefixPredicate functions).

+    /// It records all function calls made by the Function, including calls made in the body as well as in the specification.

+    /// The field is filled in during resolution (and used toward the end of resolution, to attach a helpful "decreases" prefix to functions in clusters

+    /// with co-recursive calls.

+    /// </summary>

+    public readonly List<FunctionCallExpr> AllCalls = new List<FunctionCallExpr>();

+    public enum CoCallClusterInvolvement {

+      None,  // the SCC containing the function does not involve any co-recursive calls

+      IsMutuallyRecursiveTarget,  // the SCC contains co-recursive calls, and this function is the target of some non-self recursive call

+      CoRecursiveTargetAllTheWay,  // the SCC contains co-recursive calls, and this function is the target only of self-recursive calls and co-recursive calls

+    }

+    public CoCallClusterInvolvement CoClusterTarget = CoCallClusterInvolvement.None;

+

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(cce.NonNullElements(TypeArgs));

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index ccbd9a29..29b4e9a3 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -362,9 +362,9 @@ namespace Microsoft.Dafny
             m = clbl;

             s = "";

           }

-          FillInDefaultDecreases(m);

+          var anyChangeToDecreases = FillInDefaultDecreases(m, true);

 

-          if (m.InferredDecreases || m is PrefixLemma) {

+          if (anyChangeToDecreases || m is PrefixLemma) {

             bool showIt = false;

             if (m is Function) {

               // show the inferred decreases clause only if it will ever matter, i.e., if the function is recursive

@@ -394,15 +394,22 @@ namespace Microsoft.Dafny
       }

     }

 

-    void FillInDefaultDecreases(ICallable clbl) {

+    /// <summary>

+    /// Return "true" if this routine makes any change to the decreases clause.  If the decreases clause

+    /// starts off essentially empty and a default is provided, then clbl.InferredDecreases is also set

+    /// to true.

+    /// </summary>

+    bool FillInDefaultDecreases(ICallable clbl, bool addPrefixInCoClusters) {

       Contract.Requires(clbl != null);

 

       if (clbl is CoPredicate) {

         // copredicates don't have decreases clauses

-        return;

+        return false;

       }

+      var anyChangeToDecreases = false;

       var decr = clbl.Decreases.Expressions;

       if (decr.Count == 0 || (clbl is PrefixLemma && decr.Count == 1)) {

+        var defaultAdded = false;

         // The default for a function starts with the function's reads clause, if any

         if (clbl is Function) {

           var fn = (Function)clbl;

@@ -410,6 +417,7 @@ namespace Microsoft.Dafny
             // start the default lexicographic tuple with the reads clause

             var r = FrameToObjectSet(fn.Reads);

             decr.Add(AutoGeneratedExpression.Create(r));

+            defaultAdded = true;

           }

         }

 

@@ -420,11 +428,36 @@ namespace Microsoft.Dafny
             var ie = new IdentifierExpr(p.tok, p.Name);

             ie.Var = p; ie.Type = p.Type;  // resolve it here

             decr.Add(AutoGeneratedExpression.Create(ie));

+            defaultAdded = true;

           }

         }

 

-        clbl.InferredDecreases = true;

+        if (defaultAdded) {

+          clbl.InferredDecreases = true;

+          anyChangeToDecreases = true;

+        }

       }

+      if (addPrefixInCoClusters && clbl is Function) {

+        var fn = (Function)clbl;

+        switch (fn.CoClusterTarget) {

+          case Function.CoCallClusterInvolvement.None:

+            break;

+          case Function.CoCallClusterInvolvement.IsMutuallyRecursiveTarget:

+            // prefix: 1,

+            clbl.Decreases.Expressions.Insert(0, Expression.CreateIntLiteral(fn.tok, 1));

+            anyChangeToDecreases = true;

+            break;

+          case Function.CoCallClusterInvolvement.CoRecursiveTargetAllTheWay:

+            // prefix: 0,

+            clbl.Decreases.Expressions.Insert(0, Expression.CreateIntLiteral(fn.tok, 0));

+            anyChangeToDecreases = true;

+            break;

+          default:

+            Contract.Assume(false);  // unexpected case

+            break;

+        }

+      }

+      return anyChangeToDecreases;

     }

 

     public static Expression FrameToObjectSet(List<FrameExpression> fexprs) {

@@ -773,7 +806,7 @@ namespace Microsoft.Dafny
             iter.Members.Add(field);

           }

           // finally, add special variables to hold the components of the (explicit or implicit) decreases clause

-          FillInDefaultDecreases(iter);

+          FillInDefaultDecreases(iter, false);

           // create the fields; unfortunately, we don't know their types yet, so we'll just insert type proxies for now

           var i = 0;

           foreach (var p in iter.Decreases.Expressions) {

@@ -1504,6 +1537,21 @@ namespace Microsoft.Dafny
                 c.EnclosingCoConstructor.IsCoCall = true;

                 ReportAdditionalInformation(c.CandidateCall.tok, "co-recursive call", c.CandidateCall.Name.Length);

               }

+              // Finally, fill in the CoClusterTarget field

+              // Start by setting all the CoClusterTarget fields to CoRecursiveTargetAllTheWay.

+              foreach (var m in module.CallGraph.GetSCC(repr)) {

+                var f = (Function)m;  // the cast is justified on account of that we allow co-recursive calls only in clusters that have no methods at all

+                f.CoClusterTarget = Function.CoCallClusterInvolvement.CoRecursiveTargetAllTheWay;

+              }

+              // Then change the field to IsMutuallyRecursiveTarget whenever we see a non-self recursive non-co-recursive call

+              foreach (var m in module.CallGraph.GetSCC(repr)) {

+                var f = (Function)m;  // cast is justified just like above

+                foreach (var call in f.AllCalls) {

+                  if (call.CoCall != FunctionCallExpr.CoCallResolution.Yes && call.Function != f && ModuleDefinition.InSameSCC(f, call.Function)) {

+                    call.Function.CoClusterTarget = Function.CoCallClusterInvolvement.IsMutuallyRecursiveTarget;

+                  }

+                }

+              }

             }

           }

         }

@@ -6662,6 +6710,9 @@ namespace Microsoft.Dafny
             callerModule.CallGraph.AddEdge(((IteratorDecl)codeContext).Member_MoveNext, function);

           } else {

             callerModule.CallGraph.AddEdge(caller, function);

+            if (caller is Function) {

+              ((Function)caller).AllCalls.Add(e);

+            }

             if (caller == function) {

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

             }