Print and translate "match" expressions in general positions, not just at the top-level of function bodies. (Note, resolver also needs to allow this before the user can take advantage of this.)

3 files changed, 152 insertions, 25 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index d4e7575e..8e18f229 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -479,6 +479,7 @@ axiom (forall<U, V> m: Map U V, m': Map U V ::
 // ---------------------------------------------------------------

 

 type BoxType;

+const $ArbitraryBoxValue: BoxType;

 

 function $Box<T>(T): BoxType;

 function $Unbox<T>(BoxType): T;

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index d9d6adcd..24375f7b 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -350,7 +350,7 @@ namespace Microsoft.Dafny {
       if (f.Body != null) {

         Indent(indent);

         wr.WriteLine("{");

-        PrintExtendedExpr(f.Body, ind, true, false, false);

+        PrintExtendedExpr(f.Body, ind, true, false);

         Indent(indent);

         wr.WriteLine("}");

       }

@@ -953,35 +953,42 @@ namespace Microsoft.Dafny {
 

     // ----------------------------- PrintExpression -----------------------------

 

-    public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, bool endWithCloseParen, bool isFollowedBySemicolon) {

+    /// <summary>

+    /// PrintExtendedExpr prints an expression, but formats top-level if-then-else and match expressions across several lines.

+    /// Its intended use is thus to print the body of a function.

+    /// </summary>

+    public void PrintExtendedExpr(Expression expr, int indent, bool isRightmost, bool endWithCloseParen) {

       Contract.Requires(expr != null);

-      Indent(indent);

       if (expr is ITEExpr) {

+        Indent(indent);

         while (true) {

-          ITEExpr ite = (ITEExpr)expr;

+          var ite = (ITEExpr)expr;

           wr.Write("if ");

           PrintExpression(ite.Test, false);

           wr.WriteLine(" then");

-          PrintExtendedExpr(ite.Thn, indent + IndentAmount, true, false, false);

+          PrintExtendedExpr(ite.Thn, indent + IndentAmount, true, false);

           expr = ite.Els;

           if (expr is ITEExpr) {

             Indent(indent);  wr.Write("else ");

           } else {

             Indent(indent);  wr.WriteLine("else");

             Indent(indent + IndentAmount);

-            PrintExpression(expr, isFollowedBySemicolon);

+            PrintExpression(expr, isRightmost, false);

             wr.WriteLine(endWithCloseParen ? ")" : "");

             return;

           }

         }

       } else if (expr is MatchExpr) {

-        MatchExpr me = (MatchExpr)expr;

+        var e = (MatchExpr)expr;

+        Indent(indent);

+        var parensNeeded = !isRightmost;

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

         wr.Write("match ");

-        PrintExpression(me.Source, isFollowedBySemicolon);

-        wr.WriteLine();

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

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

         int i = 0;

-        foreach (MatchCaseExpr mc in me.Cases) {

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

+        foreach (var mc in e.Cases) {

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

           Indent(indent);

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

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

@@ -992,26 +999,27 @@ namespace Microsoft.Dafny {
             }

             wr.Write(")");

           }

-          bool parensNeeded = !isLastCase && mc.Body.WasResolved() && mc.Body.Resolved is MatchExpr;

-          if (parensNeeded) {

-            wr.WriteLine(" => (");

-          } else {

-            wr.WriteLine(" =>");

-          }

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

+          wr.WriteLine(" =>");

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

           i++;

         }

       } else if (expr is ParensExpression) {

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

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

       } else {

-        PrintExpression(expr, isFollowedBySemicolon, indent);

+        Indent(indent);

+        PrintExpression(expr, false, indent);

         wr.WriteLine(endWithCloseParen ? ")" : "");

       }

     }

 

     public void PrintExpression(Expression expr, bool isFollowedBySemicolon) {

       Contract.Requires(expr != null);

-      PrintExpr(expr, 0, false, true, isFollowedBySemicolon, - 1);

+      PrintExpr(expr, 0, false, true, isFollowedBySemicolon, -1);

+    }

+

+    public void PrintExpression(Expression expr, bool isRightmost, bool isFollowedBySemicolon) {

+      Contract.Requires(expr != null);

+      PrintExpr(expr, 0, false, isRightmost, isFollowedBySemicolon, -1);

     }

 

     /// <summary>

@@ -1487,7 +1495,29 @@ namespace Microsoft.Dafny {
         }

 

       } else if (expr is MatchExpr) {

-        Contract.Assert(false); throw new cce.UnreachableException();  // MatchExpr is an extended expression and should be printed only using PrintExtendedExpr

+        var e = (MatchExpr)expr;

+        var parensNeeded = !isRightmost;

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

+        wr.Write("match ");

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

+        int i = 0;

+        foreach (var mc in e.Cases) {

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

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

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

+            string sep = "(";

+            foreach (BoundVar bv in mc.Arguments) {

+              wr.Write("{0}{1}", sep, bv.DisplayName);

+              sep = ", ";

+            }

+            wr.Write(")");

+          }

+          wr.Write(" => ");

+          PrintExpression(mc.Body, isRightmost && isLastCase, !parensNeeded && isFollowedBySemicolon);

+          i++;

+        }

+        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

         var e = (BoxingCastExpr)expr;

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index a13832c4..210b9e98 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -2525,7 +2525,7 @@ namespace Microsoft.Dafny {
       using (var writer = new System.IO.StringWriter())

       {

         var printer = new Printer(writer);

-        printer.PrintExtendedExpr(e, 0, false, false, true);

+        printer.PrintExpression(e, false);

         data = Encoding.UTF8.GetBytes(writer.ToString());

       }

 

@@ -2550,7 +2550,7 @@ namespace Microsoft.Dafny {
         printer.PrintDecreasesSpec(f.Decreases, 0);

         if (!specificationOnly && f.Body != null)

         {

-          printer.PrintExtendedExpr(f.Body, 0, false, false, true);

+          printer.PrintExpression(f.Body, false);

         }

         data = Encoding.UTF8.GetBytes(writer.ToString());

       }

@@ -3313,6 +3313,10 @@ namespace Microsoft.Dafny {
       } else if (expr is BoogieFunctionCall) {

         var e = (BoogieFunctionCall)expr;

         return CanCallAssumption(e.Args, etran);

+      } else if (expr is MatchExpr) {

+        var e = (MatchExpr)expr;

+        var ite = etran.DesugarMatchExpr(e);

+        return CanCallAssumption(ite, etran);

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

       }

@@ -7832,10 +7836,23 @@ namespace Microsoft.Dafny {
       public Bpl.IdentifierExpr Tick() {

         Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>() != null);

         Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>().Type != null);

-

         return new Bpl.IdentifierExpr(Token.NoToken, "$Tick", predef.TickType);

       }

 

+      public Bpl.IdentifierExpr ArbitraryBoxValue() {

+        Contract.Ensures(Contract.Result<Bpl.IdentifierExpr>() != null);

+        return new Bpl.IdentifierExpr(Token.NoToken, "$ArbitraryBoxValue", predef.BoxType);

+      }

+      public Bpl.Expr ArbitraryValue(Type type) {

+        Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+        var bx = ArbitraryBoxValue();

+        if (!ModeledAsBoxType(type)) {

+          return translator.FunctionCall(Token.NoToken, BuiltinFunction.Unbox, translator.TrType(type), bx);

+        } else {

+          return bx;

+        }

+      }

+

       public Bpl.Expr LayerZero() {

         Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

         return new Bpl.IdentifierExpr(Token.NoToken, "$LZ", predef.LayerType);

@@ -8490,6 +8507,11 @@ namespace Microsoft.Dafny {
           Bpl.Expr els = TrExpr(e.Els);

           return new NAryExpr(expr.tok, new IfThenElse(expr.tok), new List<Bpl.Expr> { g, thn, els });

 

+        } else if (expr is MatchExpr) {

+          var e = (MatchExpr)expr;

+          var ite = DesugarMatchExpr(e);

+          return TrExpr(ite);

+

         } else if (expr is ConcreteSyntaxExpression) {

           var e = (ConcreteSyntaxExpression)expr;

           return TrExpr(e.ResolvedExpression);

@@ -8507,6 +8529,54 @@ namespace Microsoft.Dafny {
         }

       }

 

+      public Expression DesugarMatchExpr(MatchExpr e) {

+        Contract.Requires(e != null);

+        // Translate:

+        //   match S

+        //   case C(i, j) => X

+        //   case D(k, l) => Y

+        //   case E(m, n) => Z

+        // into:

+        //   if S.C? then

+        //     X[i,j := S.dC0, S.dC1]

+        //   else if S.D? then

+        //     Y[k,l := S.dD0, S.dD1]

+        //   else

+        //     Z[m,n := S.dE0, S.dE1]

+        // As a special case, when there are no cases at all (which, in a correct program, means the

+        // match expression is unreachable), the translation is:

+        //   t

+        // where is "t" is some value (in particular, the default value) of the expected type.

+        Expression r = null;

+        for (int i = e.Cases.Count; 0 <= --i; ) {

+          var mc = e.Cases[i];

+          var substMap = new Dictionary<IVariable, Expression>();

+          var argIndex = 0;

+          foreach (var bv in mc.Arguments) {

+            if (!VarDecl.HasWildcardName(bv)) {

+              var dtor = mc.Ctor.Destructors[argIndex];

+              var dv = new FieldSelectExpr(bv.tok, e.Source, dtor.Name);

+              dv.Field = dtor;  // resolve here

+              dv.Type = bv.Type;  // resolve here

+              substMap.Add(bv, dv);

+            }

+            argIndex++;

+          }

+          var c = translator.Substitute(mc.Body, null, substMap);

+          if (r == null) {

+            r = c;

+          } else {

+            var test = new FieldSelectExpr(mc.tok, e.Source, mc.Ctor.QueryField.Name);

+            test.Field = mc.Ctor.QueryField;  // resolve here

+            test.Type = Type.Bool;  // resolve here

+            var ite = new ITEExpr(mc.tok, test, c, r);

+            ite.Type = e.Type;

+            r = ite;

+          }

+        }

+        return r ?? new BoogieWrapper(ArbitraryValue(e.Type), e.Type);

+      }

+

       public Bpl.Expr TrBoundVariables(List<BoundVar/*!*/> boundVars, List<Variable> bvars) {

         return TrBoundVariables(boundVars, bvars, false);

       }

@@ -10465,6 +10535,32 @@ namespace Microsoft.Dafny {
             newExpr = newLet;

           }

 

+        } else if (expr is MatchExpr) {

+          var e = (MatchExpr)expr;

+          var src = Substitute(e.Source);

+          bool anythingChanged = src != e.Source;

+          var cases = new List<MatchCaseExpr>();

+          foreach (var mc in e.Cases) {

+            var newBoundVars = CreateBoundVarSubstitutions(mc.Arguments);

+            var body = Substitute(mc.Body);

+            // undo any changes to substMap (could be optimized to do this only if newBoundVars != mc.Arguments)

+            foreach (var bv in mc.Arguments) {

+              substMap.Remove(bv);

+            }

+            // Put things together

+            if (newBoundVars != mc.Arguments || body != mc.Body) {

+              anythingChanged = true;

+            }

+            var newCaseExpr = new MatchCaseExpr(mc.tok, mc.Id, newBoundVars, body);

+            newCaseExpr.Ctor = mc.Ctor;  // resolve here

+            cases.Add(newCaseExpr);

+          }

+          if (anythingChanged) {

+            var newME = new MatchExpr(expr.tok, src, cases);

+            newME.MissingCases.AddRange(e.MissingCases);

+            newExpr = newME;

+          }

+

         } else if (expr is NamedExpr) {

           var e = (NamedExpr)expr;

           var body = Substitute(e.Body);