Make syntax of "match" expressions and "match" statements the same -- curly braces around the cases are now supported for both and are optional for both

1 files changed, 27 insertions, 12 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 8239fb75..0a970498 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -790,9 +790,12 @@ namespace Microsoft.Dafny {
         MatchStmt s = (MatchStmt)stmt;

         wr.Write("match ");

         PrintExpression(s.Source, false);

-        wr.WriteLine(" {");

-        int caseInd = indent + IndentAmount;

+        if (s.UsesOptionalBraces) {

+          wr.Write(" {");

+        }

+        int caseInd = indent + (s.UsesOptionalBraces ? IndentAmount : 0);

         foreach (MatchCaseStmt mc in s.Cases) {

+          wr.WriteLine();

           Indent(caseInd);

           wr.Write("case {0}", mc.Id);

           if (mc.Arguments.Count != 0) {

@@ -803,15 +806,18 @@ namespace Microsoft.Dafny {
             }

             wr.Write(")");

           }

-          wr.WriteLine(" =>");

+          wr.Write(" =>");

           foreach (Statement bs in mc.Body) {

+            wr.WriteLine();

             Indent(caseInd + IndentAmount);

             PrintStatement(bs, caseInd + IndentAmount);

-            wr.WriteLine();

           }

         }

-        Indent(indent);

-        wr.Write("}");

+        if (s.UsesOptionalBraces) {

+          wr.WriteLine();

+          Indent(indent);

+          wr.Write("}");

+        }

 

       } else if (stmt is ConcreteUpdateStatement) {

         var s = (ConcreteUpdateStatement)stmt;

@@ -1083,15 +1089,18 @@ namespace Microsoft.Dafny {
       } else if (expr is MatchExpr) {

         var e = (MatchExpr)expr;

         Indent(indent);

-        var parensNeeded = !isRightmost;

+        var parensNeeded = !isRightmost && !e.UsesOptionalBraces;

         if (parensNeeded) { wr.Write("("); }

         wr.Write("match ");

         PrintExpression(e.Source, isRightmost && e.Cases.Count == 0, false);

-        if (parensNeeded && e.Cases.Count == 0) { wr.WriteLine(")"); } else { wr.WriteLine(); }

+        if (e.UsesOptionalBraces) { wr.WriteLine(" {"); }

+        else if (parensNeeded && e.Cases.Count == 0) { wr.WriteLine(")"); }

+        else { wr.WriteLine(); }

         int i = 0;

+        int ind = indent + (e.UsesOptionalBraces ? IndentAmount : 0);

         foreach (var mc in e.Cases) {

           bool isLastCase = i == e.Cases.Count - 1;

-          Indent(indent);

+          Indent(ind);

           wr.Write("case {0}", mc.Id);

           if (mc.Arguments.Count != 0) {

             string sep = "(";

@@ -1102,9 +1111,13 @@ namespace Microsoft.Dafny {
             wr.Write(")");

           }

           wr.WriteLine(" =>");

-          PrintExtendedExpr(mc.Body, indent + IndentAmount, isLastCase, isLastCase && (parensNeeded || endWithCloseParen));

+          PrintExtendedExpr(mc.Body, ind + IndentAmount, isLastCase, isLastCase && (parensNeeded || endWithCloseParen));

           i++;

         }

+        if (e.UsesOptionalBraces) {

+          Indent(indent);

+          wr.WriteLine("}");

+        }

       } else if (expr is ParensExpression) {

         PrintExtendedExpr(((ParensExpression)expr).E, indent, isRightmost, endWithCloseParen);

       } else {

@@ -1636,10 +1649,11 @@ namespace Microsoft.Dafny {
 

       } else if (expr is MatchExpr) {

         var e = (MatchExpr)expr;

-        var parensNeeded = !isRightmost;

+        var parensNeeded = !isRightmost && !e.UsesOptionalBraces;

         if (parensNeeded) { wr.Write("("); }

         wr.Write("match ");

         PrintExpression(e.Source, isRightmost && e.Cases.Count == 0, !parensNeeded && isFollowedBySemicolon);

+        if (e.UsesOptionalBraces) { wr.Write(" {"); }

         int i = 0;

         foreach (var mc in e.Cases) {

           bool isLastCase = i == e.Cases.Count - 1;

@@ -1656,7 +1670,8 @@ namespace Microsoft.Dafny {
           PrintExpression(mc.Body, isRightmost && isLastCase, !parensNeeded && isFollowedBySemicolon);

           i++;

         }

-        if (parensNeeded) { wr.Write(")"); }

+        if (e.UsesOptionalBraces) { wr.Write(" }"); }

+        else if (parensNeeded) { wr.Write(")"); }

 

       } else if (expr is BoxingCastExpr) {

         // this is not expected for a parsed program, but we may be called for /trace purposes in the translator