Allow co-predicates to be wrapped inside bounded existential quantifiers

3 files changed, 48 insertions, 15 deletions

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 94ff6dd3..81980936 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1865,10 +1865,10 @@ namespace Microsoft.Dafny
             if (!(e.Function is CoPredicate)) {

               Error(e, "a recursive call from a copredicate can go only to other copredicates");

             } else if (cp != CallingPosition.Positive) {

-              var msg = "a recursive copredicate call can only be done in positive positions";

+              var msg = "a copredicate can be called recursively only in positive positions";

               if (cp == CallingPosition.Neither) {

-                // this may be inside a 

-                msg += " and cannot sit inside an existential quantifier";

+                // this may be inside an existential quantifier

+                msg += " and cannot sit inside an unbounded existential quantifier";

               } else {

                 // the co-call is not inside an existential quantifier, so don't bother mentioning the part of existentials in the error message

               }

@@ -1921,14 +1921,12 @@ namespace Microsoft.Dafny
         } else if (expr is QuantifierExpr) {

           var e = (QuantifierExpr)expr;

           if ((cp == CallingPosition.Positive && e is ExistsExpr) || (cp == CallingPosition.Negative && e is ForallExpr)) {

-            // Don't allow any co-recursive calls under an existential, because that can be unsound.

-            // (TODO: be more liberal here--also allow this if the range is finite)

-            cp = CallingPosition.Neither;

-          }

-          if (e.Range != null) {

-            Visit(e.Range, e is ExistsExpr ? Invert(cp) : cp);

+            if (e.MissingBounds != null && e.MissingBounds.Count != 0) {

+              // Don't allow any co-recursive calls under an existential with an unbounded range, because that can be unsound.

+              cp = CallingPosition.Neither;

+            }

           }

-          Visit(e.Term, cp);

+          Visit(e.LogicalBody(), cp);

           return false;

         } else if (expr is ConcreteSyntaxExpression) {

           // do the sub-parts with the same "cp"

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index b462465d..7e5baa4b 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1195,11 +1195,18 @@ Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor
 Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed

 Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed

 Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed

-Coinductive.dfy(90,8): Error: a recursive copredicate call can only be done in positive positions

-Coinductive.dfy(91,8): Error: a recursive copredicate call can only be done in positive positions

-Coinductive.dfy(92,8): Error: a recursive copredicate call can only be done in positive positions and cannot sit inside an existential quantifier

-Coinductive.dfy(92,21): Error: a recursive copredicate call can only be done in positive positions and cannot sit inside an existential quantifier

-8 resolution/type errors detected in Coinductive.dfy

+Coinductive.dfy(90,8): Error: a copredicate can be called recursively only in positive positions

+Coinductive.dfy(91,8): Error: a copredicate can be called recursively only in positive positions

+Coinductive.dfy(92,8): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

+Coinductive.dfy(92,21): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

+Coinductive.dfy(98,5): Error: a copredicate can be called recursively only in positive positions

+Coinductive.dfy(101,27): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

+Coinductive.dfy(102,28): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

+Coinductive.dfy(103,17): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

+Coinductive.dfy(113,24): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

+Coinductive.dfy(119,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

+Coinductive.dfy(120,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

+15 resolution/type errors detected in Coinductive.dfy

 

 -------------------- Corecursion.dfy --------------------

 Corecursion.dfy(15,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively)

diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy
index 4d197dd7..b31dc5be 100644
--- a/Test/dafny0/Coinductive.dfy
+++ b/Test/dafny0/Coinductive.dfy
@@ -92,6 +92,34 @@ module CoPredicateResolutionErrors {
     && (Even(s) <==> Even(s))  // error (x2): recursive copredicate calls allowed only in positive positions

   }

 

+  copredicate CP(i: int)

+  {

+    CP(i) &&

+    !CP(i) &&  // error: not in a positive position

+    (forall j :: CP(j)) &&

+    (exists k :: 0 <= k < i*i && CP(k)) &&

+    (exists k :: 0 <= k && CP(k)) &&  // error: unbounded range

+    (exists k :: k < i*i && CP(k)) &&  // error: unbounded range

+    (exists l :: CP(l))  // error: unbounded range

+  }

+

+  copredicate CQ(i: int, j: int)

+  {

+    exists i :: i == 6 && if j % 2 == 0 then CQ(i, i) else CQ(j, j)

+  }

+

+  copredicate CR(i: int, j: int)

+  {

+    exists i :: i == if CR(i, j) then 6 else j  // error: not allowed to call CR recursively here

+  }

+

+  copredicate CS(i: int, j: int)

+  {

+    exists i ::

+      i <= (if CS(i, j) then 6 else j) &&  // error: not allowed to call CS recursively here

+      (if CS(i, j) then 6 else j) <= i     // error: not allowed to call CS recursively here

+  }

+

   copredicate Another(s: Stream<int>)

   {

     !Even(s)  // here, negation is fine