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, 4 insertions, 0 deletions

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index fa5fdfbe..39c8f667 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -959,6 +959,10 @@ namespace Microsoft.Dafny
         reqs.AddRange(generateAutoReqs(e.Seq));

         reqs.AddRange(generateAutoReqs(e.Index));

         reqs.AddRange(generateAutoReqs(e.Value));

+      } else if (expr is DatatypeUpdateExpr) {

+        foreach (var ee in expr.SubExpressions) {

+          reqs.AddRange(generateAutoReqs(ee));

+        }

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;