diff options
| author |  leino <unknown> | 2015-06-25 18:13:49 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-06-25 18:13:49 -0700 |
| commit | 9e0c60f26bc3c228447154f0d2f9cbeaee9c1974 (patch) | |
| tree | 00e8a823203cd10e7bc16439387481be913eee9b /Test/dafny0 | |
| parent | 91fa6b7d576a111f39cde20de5d8e612b4d712b5 (diff) | |
| parent | 819469c9ab3745ef6b99a08f9e4b08620b5c8ea5 (diff) | |
Merge
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/NestedPatterns.dfy | 124 | ||||
| -rw-r--r-- | Test/dafny0/NestedPatterns.dfy.expect | 9 |
2 files changed, 133 insertions, 0 deletions
diff --git a/Test/dafny0/NestedPatterns.dfy b/Test/dafny0/NestedPatterns.dfy new file mode 100644 index 00000000..ef597936 --- /dev/null +++ b/Test/dafny0/NestedPatterns.dfy @@ -0,0 +1,124 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype List<T> = Nil | Cons(head: T, tail: List<T>)
+
+method MethodA<T>(xs: List<T>) returns (ys: List<T>)
+{
+ match xs
+ case Nil =>
+ ys := Nil;
+ case Cons(h, Nil) =>
+ ys := Nil;
+ case Cons(h, Cons(h', tt)) =>
+ ys := tt;
+}
+
+method MethodB<T>(xs: List<T>)
+{
+ match xs
+ case Nil =>
+ case Cons(h, Nil) =>
+ var x := 12;
+ var xxs := Cons(Nil, Nil);
+ case Cons(h, Cons(h', tt)) =>
+}
+
+method MethodC<T>(xs: List<T>) returns (ys: List<T>)
+ requires xs.Cons? ==> !xs.tail.Cons?;
+{
+ match xs
+ case Nil =>
+ ys := Nil;
+ case Cons(h, Nil) =>
+ ys := Nil;
+}
+
+method MethodD<T>(xs: List<T>) returns (ys: List<T>)
+{
+ match xs
+ case Nil =>
+ ys := Nil;
+ case Cons(h, Nil) =>
+ var xxs: List<List<T>> := Cons(Nil, Nil); // BUG: type inference is not doing the right thing on this lint
+ case Cons(h, Cons(h0, tt)) =>
+}
+
+method MethodE<T>(xs: List<T>) returns (ys: List<T>)
+{
+ var xxs: List<List<T>> := Cons(Nil, Nil); // here it works! (but the same line in MethodD does not work)
+}
+
+method MethodF<T>(xs: List<T>) returns (ys: List<T>)
+ requires xs.Cons? ==> !xs.tail.Cons?;
+{
+ match xs
+ case Nil =>
+ case Cons(h, Nil) =>
+ case Cons(h0, Cons(h1, tt)) => // BUG: Dafny complains that Cons appears in more than one case; it seems to be due to the
+ // fact that the previous case uses identifier "h" as the first argument to Cons, whereas this
+ // line uses "h0"
+}
+
+method MethodG<T>(xs: List<T>) returns (xxs: List<List<T>>)
+{
+ match xs
+ case Nil =>
+ xxs := Cons(Nil, Nil); // BUG: this causes there to be an "unresolved identifier: _mc#0" error; oddly enough, the error goes away if the third case is commented out
+ case Cons(h, t) =>
+ case Cons(h, Cons(ht, tt)) =>
+}
+
+method AssertionFailure(xs: List<T>)
+{
+ match xs
+ case (Nil) => // BUG: this line causes an assertion in the Dafny implementation (what should happen is that "(Nil)" should not be allowed here)
+ case (Cons(h, t)) => // BUG: ditto
+}
+
+method DuplicateIdentifierInPattern0<T>(xs: List<T>)
+{
+ match xs
+ case Nil =>
+ case Cons(h, Nil) =>
+ case Cons(h, Cons(_, h)) => // BUG: this duplicate identifier name should give rise to an error (from the Resolver), but no error is reported
+}
+
+method DuplicateIdentifierInPattern1<T>(xs: List<T>)
+{
+ match xs
+ case Nil =>
+ case Cons(h, Nil) =>
+ case Cons(h, Cons(h, _)) => // BUG: this duplicate identifier name should give rise to an error (from the Resolver), but no error is reported
+}
+
+method DuplicateIdentifierInPattern2<T>(xs: List<T>)
+{
+ match xs
+ case Nil =>
+ case Cons(h, Nil) =>
+ case Cons(h, Cons(e, e)) => // BUG: here, the duplicate identifier is detected, but the error message is shown 3 times, which is less than ideal
+}
+
+method Tuples0(xs: List<T>, ys: List<T>)
+{
+ match (xs, ys)
+ case (Nil, Nil) =>
+ case (Cons(a, b), Nil) =>
+ case (Nil, Cons(x, y)) =>
+ case (Cons(a, b), Cons(x, y)) => // BUG: here and in some other places above, not all identifiers are highlighted in the Dafny IDE; it looks like
+ // only the identifiers in the last constructors are
+}
+
+method Tuples1(xs: List<T>, ys: List<T>)
+{
+ match (xs, ys, 4)
+ case (Nil, Nil) => // BUG: the mismatch of 3 versus 2 arguments in the previous line and this line causes Dafny to crash with an
+ // assertion failure "mc.CasePatterns.Count == e.Arguments.Count"
+}
+
+method Tuples2(xs: List<T>, ys: List<T>)
+{
+ match (xs, ys, ())
+ case (Nil, Nil, ()) => // BUG: Dafny crashes with an assertion failure "e.Arguments.Count >= 1"
+}
diff --git a/Test/dafny0/NestedPatterns.dfy.expect b/Test/dafny0/NestedPatterns.dfy.expect new file mode 100644 index 00000000..d83a7da1 --- /dev/null +++ b/Test/dafny0/NestedPatterns.dfy.expect @@ -0,0 +1,9 @@ +NestedPatterns.dfy(69,2): Error: member Cons appears in more than one case
+NestedPatterns.dfy(75,2): Error: member does not exist in datatype List
+NestedPatterns.dfy(76,2): Error: member does not exist in datatype List
+NestedPatterns.dfy(84,23): Error: Duplicate parameter name: h
+NestedPatterns.dfy(92,20): Error: Duplicate parameter name: h
+NestedPatterns.dfy(100,23): Error: Duplicate parameter name: e
+NestedPatterns.dfy(116,2): Error: case arguments count does not match source arguments count
+NestedPatterns.dfy(122,2): Error: match source tuple needs at least 1 argument
+8 resolution/type errors detected in NestedPatterns.dfy
|