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 ++++++++++++--------
 2 files changed, 20 insertions(+), 14 deletions(-)

(limited to 'Source/Dafny')

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);
 			}
-- 
cgit v1.2.3