diff options
author | qunyanm <unknown> | 2015-05-14 15:44:39 -0700 |
---|---|---|
committer | qunyanm <unknown> | 2015-05-14 15:44:39 -0700 |
commit | 454909184e73582e425cad56a526956d91b88dcc (patch) | |
tree | 7a77a99216dff39bd0aa862327e3c158694a9da1 /Test/dafny0/NestedMatch.dfy | |
parent | c13c4f3fbeae61ff152eaeeb4ae8bde9d01206be (diff) |
Allow MatchExpr and MatchStmt to have nested patterns. Such as
function last<T>(xs: List<T>): T
requires xs != Nil
{
match xs
case Cons(y, Nil) => y
case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
}
And
function minus(x: Nat, y: Nat): Nat
{
match (x, y)
case (Zero, _) => Zero
case (Suc(_), Zero) => x
case (Suc(a), Suc(b)) => minus(a, b)
}
Diffstat (limited to 'Test/dafny0/NestedMatch.dfy')
-rw-r--r-- | Test/dafny0/NestedMatch.dfy | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/Test/dafny0/NestedMatch.dfy b/Test/dafny0/NestedMatch.dfy new file mode 100644 index 00000000..e6e7c489 --- /dev/null +++ b/Test/dafny0/NestedMatch.dfy @@ -0,0 +1,59 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Nat = Zero | Suc(Nat)
+
+predicate Even(n: Nat)
+{
+ match n
+ case Zero => true
+ case Suc(Zero) => false
+ case Suc(Suc(p)) => Even(p)
+}
+
+
+method checkEven(n: Nat) {
+ assert Even(Zero) == true;
+ assert Even(Suc(Zero)) == false;
+ assert Even(Suc(Suc(n))) == Even(n);
+}
+
+datatype List<T> = Nil | Cons(T, List<T>)
+
+function last<T>(xs: List<T>): T
+ requires xs != Nil
+{
+ match xs
+ case Cons(y, Nil) => y
+ case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
+}
+
+method checkLast(y: T) {
+ assert last(Cons(y, Nil)) == y;
+ assert last(Cons(y, Cons(y, Nil))) == last(Cons(y, Nil));
+}
+
+
+function minus(x: Nat, y: Nat): Nat
+{
+ match (x, y)
+ case (Zero, _) => Zero
+ case (Suc(_), Zero) => x
+ case (Suc(a), Suc(b)) => minus(a, b)
+}
+
+method checkMinus(x:Nat, y: Nat) {
+ assert minus(Suc(x), Suc(y)) == minus(x,y);
+}
+
+
+// nested match statement
+method Last<T>(xs: List<T>) returns (x: T)
+ requires xs != Nil
+{
+
+ match xs {
+ case Cons(y, Nil) => x:= y;
+ case Cons(y, Cons(z, zs)) => x:=Last(Cons(z, zs));
+ }
+}
|