diff options
| author |  rustanleino <unknown> | 2011-03-01 02:53:16 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-03-01 02:53:16 +0000 |
| commit | 9d3dc37ca301c2f310dc10929d6c6fe317b54757 (patch) | |
| tree | 74993055f0f2ca7383bd04497dc16710b8f86fd0 /Test | |
| parent | f9cb8c7c79c2c4a6eb921a58b56d7d207bf09b50 (diff) | |
Dafny: support for nested match expressions
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 6 | ||||
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 44 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy | 53 |
3 files changed, 101 insertions, 2 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 018a29e2..9501d26d 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -408,7 +408,9 @@ Modules0.dfy(62,6): Error: inter-module calls must follow the module import rela Modules0.dfy(72,6): Error: inter-module calls must follow the module import relation (so module X0 must transitively import X1)
Modules0.dfy(91,4): Error: inter-module calls must follow the module import relation (so module _default must transitively import YY)
Modules0.dfy(116,16): Error: ghost variables are allowed only in specification contexts
-8 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(133,10): Error: match source expression 'tree' has already been used as a match source expression in this context
+Modules0.dfy(172,12): Error: match source expression 'l' has already been used as a match source expression in this context
+10 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
Modules1.dfy(55,3): Error: decreases expression must be bounded below by 0
@@ -585,7 +587,7 @@ Execution trace: (0,0): anon24_Else
(0,0): anon25_Then
-Dafny program verifier finished with 11 verified, 1 error
+Dafny program verifier finished with 17 verified, 1 error
-------------------- TypeAntecedents.dfy --------------------
TypeAntecedents.dfy(34,13): Error: assertion violation
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index a7ac03d9..998b20bc 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -93,3 +93,47 @@ method TestAllocatednessAxioms(a: List<Node>, b: List<Node>, c: List<AnotherNode }
}
}
+
+class NestedMatchExpr {
+ function Cadr<T>(a: List<T>, default: T): T
+ {
+ match a
+ case Nil => default
+ case Cons(x,t) =>
+ match t
+ case Nil => default
+ case Cons(y,tail) => y
+ }
+ // CadrAlt is the same as Cadr, but it writes its two outer cases in the opposite order
+ function CadrAlt<T>(a: List<T>, default: T): T
+ {
+ match a
+ case Cons(x,t) => (
+ match t
+ case Nil => default
+ case Cons(y,tail) => y)
+ case Nil => default
+ }
+ method TestNesting0()
+ {
+ var x := 5;
+ var list := #List.Cons(3, #List.Cons(6, #List.Nil));
+ assert Cadr(list, x) == 6;
+ match (list) {
+ case Nil => assert false;
+ case Cons(h,t) => assert Cadr(t, x) == 5;
+ }
+ }
+ method TestNesting1(a: List<NestedMatchExpr>)
+ ensures Cadr(a, this) == CadrAlt(a, this);
+ {
+ match (a) {
+ case Nil =>
+ case Cons(x,t) =>
+ match (t) {
+ case Nil =>
+ case Cons(y,tail) =>
+ }
+ }
+ }
+}
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index 3e8d1e25..adce71a8 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -120,3 +120,56 @@ class Ghosty { method Callee(a: int, ghost b: int) { }
ghost method Theorem(a: int) { }
}
+
+// ---------------------- illegal match expressions ---------------
+
+datatype Tree { Nil; Cons(int, Tree, Tree); }
+
+function NestedMatch0(tree: Tree): int
+{
+ match tree
+ case Nil => 0
+ case Cons(h,l,r) =>
+ match tree // error: cannot match on "tree" again
+ case Nil => 0
+ case Cons(hh,ll,rr) => hh
+}
+
+function NestedMatch1(tree: Tree): int
+{
+ match tree
+ case Nil => 0
+ case Cons(h,l,r) =>
+ match l
+ case Nil => 0
+ case Cons(h0,l0,r0) =>
+ match r
+ case Nil => 0
+ case Cons(h1,l1,r1) => h + h0 + h1
+}
+
+function NestedMatch2(tree: Tree): int
+{
+ match tree
+ case Nil => 0
+ case Cons(h,l,r) =>
+ match l
+ case Nil => 0
+ case Cons(h,l0,tree) => // fine to declare another "h" and "tree" here
+ match r
+ case Nil => 0
+ case Cons(h1,l1,r1) => h + h1
+}
+
+function NestedMatch3(tree: Tree): int
+{
+ match tree
+ case Nil => 0
+ case Cons(h,l,r) =>
+ match l
+ case Nil => 0
+ case Cons(h0,l0,r0) =>
+ match l // error: cannot match on "l" again
+ case Nil => 0
+ case Cons(h1,l1,r1) => h + h0 + h1
+}
|