From b3d6306759e450a5d004b6581e0bf3b891b93fa5 Mon Sep 17 00:00:00 2001
From: qunyanm <unknown>
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.

---
 Source/Dafny/Dafny.atg        | 14 ++++++++------
 Source/Dafny/Parser.cs        | 20 ++++++++++++--------
 Test/dafny4/Bug138.dfy        | 22 ++++++++++++++++++++++
 Test/dafny4/Bug138.dfy.expect |  2 ++
 4 files changed, 44 insertions(+), 14 deletions(-)
 create mode 100644 Test/dafny4/Bug138.dfy
 create mode 100644 Test/dafny4/Bug138.dfy.expect

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 80792ce2..af7082a4 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -2064,9 +2064,10 @@ CaseStatement<out MatchCaseStmt/*!*/ c>
   "case"                      (. x = t; .)
   ( Ident<out id>             (. name = id.val; .)
     [ "("
-      CasePattern<out pat>        (. arguments.Add(pat); .)
-      { "," CasePattern<out pat>  (. arguments.Add(pat); .)
-      }
+       [ CasePattern<out pat>        (. arguments.Add(pat); .)
+         { "," CasePattern<out pat>  (. arguments.Add(pat); .)
+         }
+       ]
     ")" ]
   | "("
       CasePattern<out pat>        (. arguments.Add(pat); .)
@@ -2881,9 +2882,10 @@ CaseExpression<out MatchCaseExpr c, bool allowSemi, bool allowLambda>
   "case"                      (. x = t; .)
   ( Ident<out id>             (. name = id.val; .)
     [ "("
-      CasePattern<out pat>        (. arguments.Add(pat); .)
-      { "," CasePattern<out pat>  (. arguments.Add(pat); .)
-      }
+       [ CasePattern<out pat>        (. arguments.Add(pat); .)
+         { "," CasePattern<out pat>  (. arguments.Add(pat); .)
+         }
+       ]
     ")" ]
   | "("
       CasePattern<out pat>        (. arguments.Add(pat); .)
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 8a1da161..f64ba7fa 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -3244,12 +3244,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			name = id.val; 
 			if (la.kind == 50) {
 				Get();
-				CasePattern(out pat);
-				arguments.Add(pat); 
-				while (la.kind == 22) {
-					Get();
+				if (la.kind == 1 || la.kind == 50) {
 					CasePattern(out pat);
 					arguments.Add(pat); 
+					while (la.kind == 22) {
+						Get();
+						CasePattern(out pat);
+						arguments.Add(pat); 
+					}
 				}
 				Expect(51);
 			}
@@ -4562,12 +4564,14 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			name = id.val; 
 			if (la.kind == 50) {
 				Get();
-				CasePattern(out pat);
-				arguments.Add(pat); 
-				while (la.kind == 22) {
-					Get();
+				if (la.kind == 1 || la.kind == 50) {
 					CasePattern(out pat);
 					arguments.Add(pat); 
+					while (la.kind == 22) {
+						Get();
+						CasePattern(out pat);
+						arguments.Add(pat); 
+					}
 				}
 				Expect(51);
 			}
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