From c606bc377095f9ef0a7587cab58e90cca82b29f0 Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Fri, 18 May 2012 18:51:38 -0700
Subject: Dafny: more correct checking of co-inductive productivity

---
 Dafny/DafnyAst.cs | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'Dafny/DafnyAst.cs')

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]
-- 
cgit v1.2.3