Added resolution and translation of algebraic datatypes and (in function bodies) match expressions.

Addressed a couple of todos, including checking the well-formedness of quantifiers and if-then-else expressions in function bodies.

1 files changed, 18 insertions, 0 deletions

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index ee9d9613..39361b7b 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -76,4 +76,22 @@ class Termination {
       }

     }

   }

+

+  method Q<T>(list: List<T>) {

+    var l := list;

+    while (l != #List.Nil)

+      decreases l;

+    {

+      call x, l := Traverse(l);

+    }

+  }

+

+  method Traverse<T>(a: List<T>) returns (val: T, b: List<T>);

+    requires a != #List.Nil;

+    ensures a == #List.Cons(val, b);

+}

+

+datatype List<T> {

+  Nil;

+  Cons(T, List<T>);

 }