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, 24 insertions, 1 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 871d644d..16b29c2b 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -6204,7 +6204,6 @@ namespace Microsoft.Dafny {
       }

     }

 

-

     public override IEnumerable<Expression> SubExpressions {

       get { yield return Obj; }

     }

@@ -7785,6 +7784,30 @@ namespace Microsoft.Dafny {
     }

   }

 

+  public class DatatypeUpdateExpr : ConcreteSyntaxExpression

+  {

+    public readonly Expression Root;

+    public readonly List<Tuple<IToken, string, Expression>> Updates;

+    public DatatypeUpdateExpr(IToken tok, Expression root, List<Tuple<IToken, string, Expression>> updates)

+      : base(tok) {

+      Contract.Requires(tok != null);

+      Contract.Requires(root != null);

+      Contract.Requires(updates != null);

+      Contract.Requires(updates.Count != 0);

+      Root = root;

+      Updates = updates;

+    }

+

+    public override IEnumerable<Expression> SubExpressions {

+      get {

+        yield return Root;

+        foreach (var update in Updates) {

+          yield return update.Item3;

+        }

+      }

+    }

+  }

+

 

   /// <summary>

   /// An AutoGeneratedExpression is simply a wrapper around an expression.  This expression tells the generation of hover text (in the Dafny IDE)