Introduced new datatype update syntax: D.(f := E)

The old syntax, D[f := E], is still supported for a short while, but generates a warning about that syntax being deprecated.
The new syntax also supports multiple updates:  D.(f := E0, g := E1, h := E2)

1 files changed, 20 insertions, 1 deletions

diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 5e69bce8..54de4905 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -1509,7 +1509,26 @@ namespace Microsoft.Dafny {
           PrintExpression(e.Value, false);
           wr.Write("]");
           if (parensNeeded) { wr.Write(")"); }
-        }
+        }

+

+      } else if (expr is DatatypeUpdateExpr) {

+        var e = (DatatypeUpdateExpr)expr;

+        // determine if parens are needed

+        int opBindingStrength = 0x70;

+        bool parensNeeded = ParensNeeded(opBindingStrength, contextBindingStrength, fragileContext);

+

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

+        PrintExpr(e.Root, opBindingStrength, false, false, !parensNeeded && isFollowedBySemicolon, indent);

+        wr.Write(".(");

+        var sep = "";

+        foreach (var update in e.Updates) {

+          wr.Write("{0}{1} := ", sep, update.Item2);

+          PrintExpression(update.Item3, false);

+          sep = ", ";

+        }

+        wr.Write(")");

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

+

       } else if (expr is ApplyExpr) {
         var e = (ApplyExpr)expr;
         // determine if parens are needed