Dafny: more correct checking of co-inductive productivity

1 files changed, 6 insertions, 1 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index aba2bd92..ebc3782e 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -262,6 +262,11 @@ namespace Microsoft.Dafny {
         }

       }

     }

+    public bool InvolvesCoDatatype {

+      get {

+        return IsCoDatatype;  // TODO: should really check structure of the type recursively

+      }

+    }

     public bool IsTypeParameter {

       get {

         UserDefinedType ct = this as UserDefinedType;

@@ -2570,7 +2575,7 @@ 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 enum CoCallResolution { No, Yes, NoBecauseFunctionHasSideEffects, NoBecauseRecursiveCallsAreNotAllowedInThisContext, NoBecauseIsNotGuarded }

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

 

     [ContractInvariantMethod]