Removed the syntactic form copredicate #-form with the implicit argument.

Added syntactic support for codatatype #-form equalities.

5 files changed, 201 insertions, 85 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 964b69a4..87e6e93f 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1327,20 +1327,12 @@ Execution trace:
 Dafny program verifier finished with 5 verified, 2 errors

 

 -------------------- CoResolution.dfy --------------------

-CoResolution.dfy(22,8): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)

-CoResolution.dfy(23,3): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)

-CoResolution.dfy(24,7): Error: member Undeclared# does not exist in class _default

-CoResolution.dfy(25,7): Error: member Undeclared# does not exist in class _default

-CoResolution.dfy(26,2): Error: unresolved identifier: Undeclared#

-CoResolution.dfy(26,12): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)

-CoResolution.dfy(27,2): Error: unresolved identifier: Undeclared#

-CoResolution.dfy(30,2): Error: wrong number of function arguments (got 3, expected 2)

-CoResolution.dfy(31,5): Error: unresolved identifier: _k

-CoResolution.dfy(37,30): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)

-CoResolution.dfy(38,20): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)

-CoResolution.dfy(41,9): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)

-CoResolution.dfy(42,4): Error: a call to a prefix predicate/method in this context must explicitly specify a depth argument (given in square brackets just after the # sign)

-13 resolution/type errors detected in CoResolution.dfy

+CoResolution.dfy(43,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>)

+CoResolution.dfy(54,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

+CoResolution.dfy(22,7): Error: member Undeclared# does not exist in class _default

+CoResolution.dfy(23,2): Error: unresolved identifier: Undeclared#

+CoResolution.dfy(26,5): Error: unresolved identifier: _k

+5 resolution/type errors detected in CoResolution.dfy

 

 -------------------- CoPrefix.dfy --------------------

 CoPrefix.dfy(61,7): Error: failure to decrease termination measure

@@ -1348,7 +1340,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon5_Else

     (0,0): anon6_Then

-CoPrefix.dfy(74,7): Error: failure to decrease termination measure

+CoPrefix.dfy(74,7): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

@@ -1358,8 +1350,12 @@ CoPrefix.dfy(111,11): Related location: This is the postcondition that might not
 CoPrefix.dfy(99,17): Related location: Related location

 Execution trace:

     (0,0): anon0

+CoPrefix.dfy(136,25): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Then

 

-Dafny program verifier finished with 17 verified, 3 errors

+Dafny program verifier finished with 23 verified, 4 errors

 

 -------------------- CoinductiveProofs.dfy --------------------

 CoinductiveProofs.dfy(26,12): Error: assertion violation

@@ -1401,7 +1397,7 @@ CoinductiveProofs.dfy(152,22): Related location: This is the postcondition that
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 32 verified, 8 errors

+Dafny program verifier finished with 35 verified, 8 errors

 

 -------------------- TypeAntecedents.dfy --------------------

 TypeAntecedents.dfy(32,13): Error: assertion violation

diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy
index 233a818b..3146147e 100644
--- a/Test/dafny0/CoResolution.dfy
+++ b/Test/dafny0/CoResolution.dfy
@@ -19,25 +19,49 @@ copredicate D()
 

 copredicate S(d: set<int>)

 {

-  this.S#(d) &&  // error: the call to S# must give an explicit depth argument

-  S#(d) &&  // error: the call to S# must give an explicit depth argument

-  this.Undeclared#(d) &&  // error: 'Undeclared#' is undeclared, and depth argument is left implicit

   this.Undeclared#[5](d) &&  // error: 'Undeclared#' is undeclared

-  Undeclared#(d) &&  // error: 'Undeclared#' is undeclared, and depth argument is left implicit

   Undeclared#[5](d) &&  // error: 'Undeclared#' is undeclared

   this.S#[5](d) &&

   S#[5](d) &&

-  S#(5, d) &&  // error: the '5' here does not give the depth argument

   S#[_k](d)  // error: _k is not an identifier in scope

 }

 

 comethod CM(d: set<int>)

 {

   var b;

-  b := this.S#[5](d) && this.S#(d + d);  // error: cannot rely on implicit depth argument here

-  b := S#[5](d) && S#(d + d);  // error: cannot rely on implicit depth argument here

+  b := this.S#[5](d);

+  b := S#[5](d);

   this.CM#[5](d);

   CM#[5](d);

-  this.CM#(d + d);  // error: must give an explicit depth argument

-  CM#(d + d);  // error: must give an explicit depth argument

+}

+

+module GhostCheck0 {

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

+  method UseStream0(s: Stream)

+  {

+    var x := 3;

+    if (s == s.tail) {  // error: this operation is allowed only in ghost contexts

+      x := x + 2;

+    }

+  }

+}

+module GhostCheck1 {

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

+  method UseStream1(s: Stream)

+  {

+    var x := 3;

+    if (s ==#[20] s.tail) {  // this seems innocent enough, but it's currently not supported by the compiler, so...

+      x := x + 7;  // error: therefore, this is an error

+    }

+  }

+}

+module GhostCheck2 {

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

+  ghost method UseStreamGhost(s: Stream)

+  {

+    var x := 3;

+    if (s == s.tail) {  // fine

+      x := x + 2;

+    }

+  }

 }

diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy
index ddb23b5b..47c5f262 100644
--- a/Test/dafny0/CoinductiveProofs.dfy
+++ b/Test/dafny0/CoinductiveProofs.dfy
@@ -153,3 +153,28 @@ comethod BadEquality1(n: int)
 {  // error: postcondition does not hold

   BadEquality1(n+1);

 }

+

+// test that match statements/expressions get the correct assumption (which wasn't always the case)

+

+codatatype IList<T> = INil | ICons(head: T, tail: IList<T>);

+

+ghost method M(s: IList)

+{

+  match (s) {

+    case INil =>

+      assert s == INil;

+    case ICons(a, b) =>

+      assert s == ICons(a, b);

+  }

+}

+

+function G(s: IList): int

+{

+  match s

+  case INil =>

+    assert s == INil;

+    0

+  case ICons(a, b) =>

+    assert s == ICons(a, b);

+    0

+}

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index 5ab835e7..9cd8fc82 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -5,7 +5,7 @@ Dafny program verifier finished with 15 verified, 0 errors
 

 -------------------- Streams.dfy --------------------

 

-Dafny program verifier finished with 38 verified, 0 errors

+Dafny program verifier finished with 50 verified, 0 errors

 

 -------------------- Dijkstra.dfy --------------------

 

diff --git a/Test/dafny3/Streams.dfy b/Test/dafny3/Streams.dfy
index 1369e584..757d6a37 100644
--- a/Test/dafny3/Streams.dfy
+++ b/Test/dafny3/Streams.dfy
@@ -49,13 +49,35 @@ comethod Theorem0(M: Stream<X>)
       Theorem0(N);

   }

 }

-comethod Theorem0_alt(M: Stream<X>)

+comethod Theorem0_Alt(M: Stream<X>)

   ensures map_fg(M) == map_f(map_g(M));

 {

   if (M.Cons?) {

-    Theorem0(M.tail);

+    Theorem0_Alt(M.tail);

   }

 }

+ghost method Theorem0_Par(M: Stream<X>)

+  ensures map_fg(M) == map_f(map_g(M));

+{

+  parallel (k: nat) {

+    Theorem0_Ind(k, M);

+  }

+}

+ghost method Theorem0_Ind(k: nat, M: Stream<X>)

+  ensures map_fg(M) ==#[k] map_f(map_g(M));

+{

+  if (k != 0) {

+    match (M) {

+      case Nil =>

+      case Cons(x, N) =>

+        Theorem0_Ind(k-1, N);

+    }

+  }

+}

+ghost method Theorem0_AutoInd(k: nat, M: Stream<X>)

+  ensures map_fg(M) ==#[k] map_f(map_g(M));

+// {  // TODO: this is not working yet, apparently

+// }

 

 // map f (append M N) = append (map f M) (map f N)

 comethod Theorem1(M: Stream<X>, N: Stream<X>)

@@ -67,13 +89,40 @@ comethod Theorem1(M: Stream<X>, N: Stream<X>)
       Theorem1(M', N);

   }

 }

-comethod Theorem1_alt(M: Stream<X>, N: Stream<X>)

+comethod Theorem1_Alt(M: Stream<X>, N: Stream<X>)

   ensures map_f(append(M, N)) == append(map_f(M), map_f(N));

 {

   if (M.Cons?) {

-    Theorem1(M.tail, N);

+    Theorem1_Alt(M.tail, N);

   }

 }

+ghost method Theorem1_Par(M: Stream<X>, N: Stream<X>)

+  ensures map_f(append(M, N)) == append(map_f(M), map_f(N));

+{

+  parallel (k: nat) {

+    Theorem1_Ind(k, M, N);

+  }

+}

+ghost method Theorem1_Ind(k: nat, M: Stream<X>, N: Stream<X>)

+  ensures map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N));

+{

+  // this time, try doing the 'if' inside the 'match' (instead of the other way around)

+  match (M) {

+    case Nil =>

+    case Cons(x, M') =>

+      if (k != 0) {

+        Theorem1_Ind(k-1, M', N);

+      }

+  }

+}

+ghost method Theorem1_AutoInd(k: nat, M: Stream<X>, N: Stream<X>)

+  ensures map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N));

+// {  // TODO: this is not working yet, apparently

+// }

+ghost method Theorem1_AutoForall()

+{

+//  assert forall k: nat, M, N :: map_f(append(M, N)) ==#[k] append(map_f(M), map_f(N));  // TODO: this is not working yet, apparently

+}

 

 // append NIL M = M

 ghost method Theorem2(M: Stream<X>)

@@ -92,11 +141,11 @@ comethod Theorem3(M: Stream<X>)
       Theorem3(N);

   }

 }

-comethod Theorem3_alt(M: Stream<X>)

+comethod Theorem3_Alt(M: Stream<X>)

   ensures append(M, Nil) == M;

 {

   if (M.Cons?) {

-    Theorem3(M.tail);

+    Theorem3_Alt(M.tail);

   }

 }

 

@@ -110,11 +159,11 @@ comethod Theorem4(M: Stream<X>, N: Stream<X>, P: Stream<X>)
       Theorem4(M', N, P);

   }

 }

-comethod Theorem4_alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)

+comethod Theorem4_Alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)

   ensures append(M, append(N, P)) == append(append(M, N), P);

 {

   if (M.Cons?) {

-    Theorem4(M.tail, N, P);

+    Theorem4_Alt(M.tail, N, P);

   }

 }

 

@@ -122,7 +171,7 @@ comethod Theorem4_alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)
 

 // Flatten can't be written as just:

 //

-//     function SimpleFlatten<T>(M: Stream<Stream>): Stream

+//     function SimpleFlatten(M: Stream<Stream>): Stream

 //     {

 //       match M

 //       case Nil => Nil

@@ -130,9 +179,9 @@ comethod Theorem4_alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)
 //     }

 //

 // because this function fails to be productive given an infinite stream of Nil's.

-// Instead, here are two variations SimpleFlatten.  The first variation (FlattenStartMarker)

+// Instead, here are two variations of SimpleFlatten.  The first variation (FlattenStartMarker)

 // prepends a "startMarker" to each of the streams in "M".  The other (FlattenNonEmpties)

-// insists that "M" contains no empty streams.  One can prove a theorem that relates these

+// insists that "M" contain no empty streams.  One can prove a theorem that relates these

 // two versions.

 

 // This first variation of Flatten returns a stream of the streams in M, each preceded with

@@ -140,18 +189,18 @@ comethod Theorem4_alt(M: Stream<X>, N: Stream<X>, P: Stream<X>)
 

 function FlattenStartMarker<T>(M: Stream<Stream>, startMarker: T): Stream

 {

-  FlattenStartMarkerAcc(Nil, M, startMarker)

+  PrependThenFlattenStartMarker(Nil, M, startMarker)

 }

 

-function FlattenStartMarkerAcc<T>(accumulator: Stream, M: Stream<Stream>, startMarker: T): Stream

+function PrependThenFlattenStartMarker<T>(prefix: Stream, M: Stream<Stream>, startMarker: T): Stream

 {

-  match accumulator

+  match prefix

   case Cons(hd, tl) =>

-    Cons(hd, FlattenStartMarkerAcc(tl, M, startMarker))

+    Cons(hd, PrependThenFlattenStartMarker(tl, M, startMarker))

   case Nil =>

     match M

     case Nil => Nil

-    case Cons(s, N) => Cons(startMarker, FlattenStartMarkerAcc(s, N, startMarker))

+    case Cons(s, N) => Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker))

 }

 

 // The next variation of Flatten requires M to contain no empty streams.

@@ -166,26 +215,24 @@ copredicate StreamOfNonEmpties(M: Stream<Stream>)
 function FlattenNonEmpties(M: Stream<Stream>): Stream

   requires StreamOfNonEmpties(M);

 {

-  FlattenNonEmptiesAcc(Nil, M)

+  PrependThenFlattenNonEmpties(Nil, M)

 }

 

-function FlattenNonEmptiesAcc(accumulator: Stream, M: Stream<Stream>): Stream

+function PrependThenFlattenNonEmpties(prefix: Stream, M: Stream<Stream>): Stream

   requires StreamOfNonEmpties(M);

 {

-  match accumulator

+  match prefix

   case Cons(hd, tl) =>

-    Cons(hd, FlattenNonEmptiesAcc(tl, M))

+    Cons(hd, PrependThenFlattenNonEmpties(tl, M))

   case Nil =>

     match M

     case Nil => Nil

-    case Cons(s, N) => Cons(s.head, FlattenNonEmptiesAcc(s.tail, N))

+    case Cons(s, N) => Cons(s.head, PrependThenFlattenNonEmpties(s.tail, N))

 }

 

 // We can prove a theorem that links the previous two variations of flatten.  To

 // do that, we first define a function that prepends an element to each stream

 // of a given stream of streams.

-// The "assume" statements below are temporary workaround.  They make the proofs

-// unsound, but, as a temporary measure, they express the intent of the proofs.

 

 function Prepend<T>(x: T, M: Stream<Stream>): Stream<Stream>

   ensures StreamOfNonEmpties(Prepend(x, M));

@@ -201,58 +248,82 @@ ghost method Theorem_Flatten<T>(M: Stream<Stream>, startMarker: T)
   Lemma_Flatten(Nil, M, startMarker);

 }

 

-comethod Lemma_Flatten<T>(accumulator: Stream, M: Stream<Stream>, startMarker: T)

-  ensures FlattenStartMarkerAcc(accumulator, M, startMarker) == FlattenNonEmptiesAcc(accumulator, Prepend(startMarker, M));

+comethod Lemma_Flatten<T>(prefix: Stream, M: Stream<Stream>, startMarker: T)

+  ensures PrependThenFlattenStartMarker(prefix, M, startMarker) == PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));

 {

-  calc {

-    FlattenStartMarkerAcc(accumulator, M, startMarker);

-    { Lemma_FlattenAppend0(accumulator, M, startMarker); }

-    append(accumulator, FlattenStartMarkerAcc(Nil, M, startMarker));

-    { Lemma_Flatten(Nil, M, startMarker);

-      assume FlattenStartMarkerAcc(Nil, M, startMarker) == FlattenNonEmptiesAcc(Nil, Prepend(startMarker, M));  // postcondition of the co-recursive call

-    }

-    append(accumulator, FlattenNonEmptiesAcc(Nil, Prepend(startMarker, M)));

-    { Lemma_FlattenAppend1(accumulator, Prepend(startMarker, M)); }

-    FlattenNonEmptiesAcc(accumulator, Prepend(startMarker, M));

+  match (prefix) {

+    case Cons(hd, tl) =>

+    Lemma_Flatten(tl, M, startMarker);

+    case Nil =>

+      match (M) {

+        case Nil =>

+        case Cons(s, N) =>

+          if (*) {

+            // This is all that's needed for the proof

+            Lemma_Flatten(s, N, startMarker);

+          } else {

+            // ...but here are some calculations that try to show more of what's going on

+            // (It would be nice to have ==#[...] available as an operator in calculations.)

+

+            // massage the LHS:

+            calc {

+              PrependThenFlattenStartMarker(prefix, M, startMarker);

+            ==  // def. PrependThenFlattenStartMarker

+              Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker));

+            }

+            // massage the RHS:

+            calc {

+              PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));

+            ==  // M == Cons(s, N)

+              PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, Cons(s, N)));

+            ==  // def. Prepend

+              PrependThenFlattenNonEmpties(prefix, Cons(Cons(startMarker, s), Prepend(startMarker, N)));

+            ==  // def. PrependThenFlattenNonEmpties

+              Cons(Cons(startMarker, s).head, PrependThenFlattenNonEmpties(Cons(startMarker, s).tail, Prepend(startMarker, N)));

+            ==  // Cons, head, tail

+              Cons(startMarker, PrependThenFlattenNonEmpties(s, Prepend(startMarker, N)));

+            }

+

+            // all together now:

+            calc {

+              PrependThenFlattenStartMarker(prefix, M, startMarker) ==#[_k] PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));

+              { // by the calculation above, we have:

+                assert PrependThenFlattenStartMarker(prefix, M, startMarker) == Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker)); }

+              Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker)) ==#[_k] PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M));

+              { // and by the other calculation above, we have:

+                assert PrependThenFlattenNonEmpties(prefix, Prepend(startMarker, M)) == Cons(startMarker, PrependThenFlattenNonEmpties(s, Prepend(startMarker, N))); }

+              Cons(startMarker, PrependThenFlattenStartMarker(s, N, startMarker)) ==#[_k] Cons(startMarker, PrependThenFlattenNonEmpties(s, Prepend(startMarker, N)));

+            ==  // def. of ==#[_k] for _k != 0

+              startMarker == startMarker &&

+              PrependThenFlattenStartMarker(s, N, startMarker) ==#[_k-1] PrependThenFlattenNonEmpties(s, Prepend(startMarker, N));

+              { Lemma_Flatten(s, N, startMarker);

+                // the postcondition of the call we just made (which invokes the co-induction hypothesis) is:

+                assert PrependThenFlattenStartMarker(s, N, startMarker) ==#[_k-1] PrependThenFlattenNonEmpties(s, Prepend(startMarker, N));

+              }

+              true;

+            }

+          }

+      }

   }

 }

 

 comethod Lemma_FlattenAppend0<T>(s: Stream, M: Stream<Stream>, startMarker: T)

-  ensures FlattenStartMarkerAcc(s, M, startMarker) == append(s, FlattenStartMarkerAcc(Nil, M, startMarker));

+  ensures PrependThenFlattenStartMarker(s, M, startMarker) == append(s, PrependThenFlattenStartMarker(Nil, M, startMarker));

 {

   match (s) {

     case Nil =>

     case Cons(hd, tl) =>

-      calc {

-        FlattenStartMarkerAcc(Cons(hd, tl), M, startMarker);

-        Cons(hd, FlattenStartMarkerAcc(tl, M, startMarker));

-        { Lemma_FlattenAppend0(tl, M, startMarker);

-          assume FlattenStartMarkerAcc(tl, M, startMarker) == append(tl, FlattenStartMarkerAcc(Nil, M, startMarker));  // this is the postcondition of the co-recursive call

-        }

-        Cons(hd, append(tl, FlattenStartMarkerAcc(Nil, M, startMarker)));

-        // def. append

-        append(Cons(hd, tl), FlattenStartMarkerAcc(Nil, M, startMarker));

-      }

+      Lemma_FlattenAppend0(tl, M, startMarker);

   }

 }

 

 comethod Lemma_FlattenAppend1<T>(s: Stream, M: Stream<Stream>)

   requires StreamOfNonEmpties(M);

-  ensures FlattenNonEmptiesAcc(s, M) == append(s, FlattenNonEmptiesAcc(Nil, M));

+  ensures PrependThenFlattenNonEmpties(s, M) == append(s, PrependThenFlattenNonEmpties(Nil, M));

 {

   match (s) {

     case Nil =>

     case Cons(hd, tl) =>

-      calc {

-        FlattenNonEmptiesAcc(Cons(hd, tl), M);

-        // def. FlattenNonEmptiesAcc

-        Cons(hd, FlattenNonEmptiesAcc(tl, M));

-        { Lemma_FlattenAppend1(tl, M);

-          assume FlattenNonEmptiesAcc(tl, M) == append(tl, FlattenNonEmptiesAcc(Nil, M));  // postcondition of the co-recursive call

-        }

-        Cons(hd, append(tl, FlattenNonEmptiesAcc(Nil, M)));

-        // def. append

-        append(Cons(hd, tl), FlattenNonEmptiesAcc(Nil, M));

-      }

+      Lemma_FlattenAppend1(tl, M);

   }

 }