From b3d6306759e450a5d004b6581e0bf3b891b93fa5 Mon Sep 17 00:00:00 2001 From: qunyanm Date: Fri, 26 Feb 2016 12:37:46 -0800 Subject: Fix issue 138. Allow parenthese with the nullary constructor in "case" of a match statement and match expression. --- Test/dafny4/Bug138.dfy | 22 ++++++++++++++++++++++ Test/dafny4/Bug138.dfy.expect | 2 ++ 2 files changed, 24 insertions(+) create mode 100644 Test/dafny4/Bug138.dfy create mode 100644 Test/dafny4/Bug138.dfy.expect (limited to 'Test/dafny4') diff --git a/Test/dafny4/Bug138.dfy b/Test/dafny4/Bug138.dfy new file mode 100644 index 00000000..db0e54ef --- /dev/null +++ b/Test/dafny4/Bug138.dfy @@ -0,0 +1,22 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +datatype List = Nil | Cons(int, List) + +method R(xs: List) +{ + match xs + case Nil() => // currently produces a parsing error, but shouldn't + case Cons(x, Nil()) => // currently allowed + case Cons(x, Cons(y, tail)) => +} + +function F(xs: List) : int +{ + match xs + case Nil() => 0 // currently produces a parsing error, but shouldn't + case Cons(x, Nil()) => 1 // currently allowed + case Cons(x, Cons(y, tail)) => 2 +} + + diff --git a/Test/dafny4/Bug138.dfy.expect b/Test/dafny4/Bug138.dfy.expect new file mode 100644 index 00000000..52595bf9 --- /dev/null +++ b/Test/dafny4/Bug138.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 3 verified, 0 errors -- cgit v1.2.3