Co-recursion, now sounder than ever!

- prefix equality is destructive
- co-methods are not allowed to have out-parameters
- in an SCC with both co-recursive and recursive calls, the latter are allowed only in non-destructive contexts

1 files changed, 45 insertions, 0 deletions

diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy
index 5025dae9..3193db12 100644
--- a/Test/dafny0/Corecursion.dfy
+++ b/Test/dafny0/Corecursion.dfy
@@ -79,3 +79,48 @@ module EqualityIsSuperDestructive {
     assert false;

   }

 }

+

+// --------------------------------------------------

+

+module MixRecursiveAndCorecursive {

+  codatatype Stream<T> = Cons(head: T, tail: Stream)

+  

+  function F(n: nat): Stream<int>

+  {

+    if n == 0 then

+      Cons(0, F(5))  // error: cannot prove termination -- by itself, this would look like a properly guarded co-recursive call...

+    else

+      F(n - 1).tail  // but the fact that this recursive call is not tail recursive means that call in the 'then' branch is not

+                     // allowed to be a co-recursive

+  }

+

+  // same thing but with some mutual recursion going on

+  function G(n: nat): Stream<int>

+  {

+    if n == 0 then

+      Cons(0, H(5))  // error: cannot prove termination

+    else

+      H(n)

+  }

+  function H(n: nat): Stream<int>

+    requires n != 0;

+    decreases n, 0;

+  {

+    G(n-1).tail

+  }

+

+  // but if all the recursive calls are tail recursive, then all is cool

+  function X(n: nat): Stream<int>

+  {

+    if n == 0 then

+      Cons(0, Y(5))  // error: cannot prove termination

+    else

+      Y(n)

+  }

+  function Y(n: nat): Stream<int>

+    requires n != 0;

+    decreases n, 0;

+  {

+    X(n-1)

+  }

+}