Fix issue #79. Allow tuple pattern matching with parenthesis only.

4 files changed, 44 insertions, 2 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 3f684ff6..16cc09eb 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -2625,7 +2625,18 @@ CasePattern<out CasePattern pat>
         }

       ]

     ")"                                (. pat = new CasePattern(id, id.val, arguments); .)

-

+  | "("                                (. id = t;                                                           

+                                          arguments = new List<CasePattern>(); 

+                                       .)

+      [ CasePattern<out pat>           (. arguments.Add(pat); .)

+        { "," CasePattern<out pat>     (. arguments.Add(pat); .)

+        }

+      ]

+    ")"                                (. // Parse parenthesis without an identifier as a built in tuple type.

+                                          theBuiltIns.TupleType(id, arguments.Count, true); // make sure the tuple type exists

+                                          string ctor = BuiltIns.TupleTypeCtorName;  //use the TupleTypeCtors

+                                          pat = new CasePattern(id, ctor, arguments); 

+                                       .)

   | IdentTypeOptional<out bv>          (. // This could be a BoundVar of a parameter-less constructor and we may not know until resolution.

                                           // Nevertheless, we do put the "bv" into the CasePattern here (even though it will get thrown out

                                           // later if resolution finds the CasePattern to denote a parameter-less constructor), because this

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index d0924169..162e23a3 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -2934,7 +2934,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Ident(out id);

 			Expect(48);

 			arguments = new List<CasePattern>(); 

-			if (la.kind == 1) {

+			if (la.kind == 1 || la.kind == 48) {

 				CasePattern(out pat);

 				arguments.Add(pat); 

 				while (la.kind == 21) {

@@ -2945,6 +2945,25 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			Expect(49);

 			pat = new CasePattern(id, id.val, arguments); 

+		} else if (la.kind == 48) {

+			Get();

+			id = t;                                                           

+			arguments = new List<CasePattern>(); 

+			

+			if (la.kind == 1 || la.kind == 48) {

+				CasePattern(out pat);

+				arguments.Add(pat); 

+				while (la.kind == 21) {

+					Get();

+					CasePattern(out pat);

+					arguments.Add(pat); 

+				}

+			}

+			Expect(49);

+			theBuiltIns.TupleType(id, arguments.Count, true); // make sure the tuple type exists

+			string ctor = BuiltIns.TupleTypeCtorName;  //use the TupleTypeCtors

+			pat = new CasePattern(id, ctor, arguments); 

+			

 		} else if (la.kind == 1) {

 			IdentTypeOptional(out bv);

 			pat = new CasePattern(bv.tok, bv);

diff --git a/Test/dafny4/Bug79.dfy b/Test/dafny4/Bug79.dfy
new file mode 100644
index 00000000..49f2421b
--- /dev/null
+++ b/Test/dafny4/Bug79.dfy
@@ -0,0 +1,10 @@
+// RUN: %dafny /compile:0  "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+function foo(s:int) : (int, int)

+

+function bar(s:int) : bool

+{

+    var (x, rest) := foo(s);

+    x > 0

+}
\ No newline at end of file
diff --git a/Test/dafny4/Bug79.dfy.expect b/Test/dafny4/Bug79.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/dafny4/Bug79.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 2 verified, 0 errors