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)

11 files changed, 280 insertions, 81 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index 9a93a340..1c4275c5 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -323,6 +323,10 @@ namespace Microsoft.Dafny
         var e = (SeqUpdateExpr)expr;

         return new SeqUpdateExpr(Tok(e.tok), CloneExpr(e.Seq), CloneExpr(e.Index), CloneExpr(e.Value));

 

+      } else if (expr is DatatypeUpdateExpr) {

+        var e = (DatatypeUpdateExpr)expr;

+        return new DatatypeUpdateExpr(Tok(e.tok), CloneExpr(e.Root), e.Updates.ConvertAll(t => Tuple.Create(Tok(t.Item1), t.Item2, CloneExpr(t.Item3))));

+

       } else if (expr is FunctionCallExpr) {

         var e = (FunctionCallExpr)expr;

         return new FunctionCallExpr(Tok(e.tok), e.Name, CloneExpr(e.Receiver), e.OpenParen == null ? null : Tok(e.OpenParen), e.Args.ConvertAll(CloneExpr));

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 66dff8a2..5fa1085d 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -16,7 +16,7 @@ COMPILER Dafny
 /*--------------------------------------------------------------------------*/

 readonly Expression/*!*/ dummyExpr;

 readonly AssignmentRhs/*!*/ dummyRhs;

-readonly FrameExpression/*!*/ dummyFrameExpr;

+readonly FrameExpression/*!*/ dummyFrameExpr;  

 readonly Statement/*!*/ dummyStmt;

 readonly ModuleDecl theModule;

 readonly BuiltIns theBuiltIns;

@@ -2791,8 +2791,17 @@ Suffix<ref Expression e>
      Expression e0 = null;  Expression e1 = null;  Expression ee;  bool anyDots = false;

      List<Expression> multipleLengths = null; bool takeRest = false; // takeRest is relevant only if multipleLengths is non-null

      List<Expression> multipleIndices = null;

+     List<Tuple<IToken, string, Expression>> updates;

+     Expression v;

   .)

-  ( DotSuffix<out id, out x>                   (. if (x != null) {

+  ( "."

+    ( "("                                             (. x = t; updates = new List<Tuple<IToken, string, Expression>>(); .)

+        MemberBindingUpdate<out id, out v>            (. updates.Add(Tuple.Create(id, id.val, v)); .)

+        { "," MemberBindingUpdate<out id, out v>      (. updates.Add(Tuple.Create(id, id.val, v)); .)

+        }

+      ")"

+      (. e = new DatatypeUpdateExpr(x, e, updates); .)

+    | DotSuffix<out id, out x>                 (. if (x != null) {

                                                     // process id as a Suffix in its own right

                                                     e = new ExprDotName(id, e, id.val, null);

                                                     id = x;  // move to the next Suffix

@@ -2801,17 +2810,18 @@ Suffix<ref Expression e>
                                                .)

 

 

-    ( IF(IsGenericInstantiation())

-      (. typeArgs = new List<Type>(); .)

-      GenericInstantiation<typeArgs>

-    | HashCall<id, out openParen, out typeArgs, out args>

-    | /* empty */

+      ( IF(IsGenericInstantiation())

+        (. typeArgs = new List<Type>(); .)

+        GenericInstantiation<typeArgs>

+      | HashCall<id, out openParen, out typeArgs, out args>

+      | /* empty */

+      )

+      (. e = new ExprDotName(id, e, id.val, typeArgs);

+         if (openParen != null) {

+           e = new ApplySuffix(openParen, e, args);

+         }

+      .)

     )

-    (. e = new ExprDotName(id, e, id.val, typeArgs);

-       if (openParen != null) {

-         e = new ApplySuffix(openParen, e, args);

-       }

-    .)

   | "["                                        (. x = t; .)

       ( Expression<out ee, true, true>         (. e0 = ee; .)

         ( ".."                                 (. anyDots = true; .)

@@ -2969,10 +2979,10 @@ Ident<out IToken/*!*/ x>
   ident            (. x = t; .)

   .

 // Identifier or sequence of digits

-// Parse one of the following:

-//      . ident

-//      . digits

-//      . digits . digits

+// Parse one of the following, which are supposed to follow a ".":

+//        ident

+//        digits

+//        digits . digits

 // In the first two cases, x returns as the token for the ident/digits and y returns as null.

 // In the third case, x and y return as the tokens for the first and second digits.

 // This parser production solves a problem where the scanner might parse a real number instead

@@ -2982,7 +2992,6 @@ DotSuffix<out IToken x, out IToken y>
      x = Token.NoToken;

      y = null;

   .)

-  "."

   ( ident          (. x = t; .)

   | digits         (. x = t; .)

   | decimaldigits  (. x = t;

@@ -3008,6 +3017,15 @@ DotSuffix<out IToken x, out IToken y>
   | "reads"       (. x = t; .)

   )

   .

+MemberBindingUpdate<out IToken id, out Expression e>

+= (. id = Token.NoToken; e = dummyExpr; .)

+  ( ident          (. id = t; .)

+  | digits         (. id = t; .)

+  )

+  ":="

+  Expression<out e, true, true>

+  .

+

 // Identifier, disallowing leading underscores

 NoUSIdent<out IToken/*!*/ x>

 = (. Contract.Ensures(Contract.ValueAtReturn(out x) != null); .)

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)

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index c79c1051..6a5f32ab 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -88,7 +88,7 @@ public class Parser {
 

 readonly Expression/*!*/ dummyExpr;

 readonly AssignmentRhs/*!*/ dummyRhs;

-readonly FrameExpression/*!*/ dummyFrameExpr;

+readonly FrameExpression/*!*/ dummyFrameExpr;  

 readonly Statement/*!*/ dummyStmt;

 readonly ModuleDecl theModule;

 readonly BuiltIns theBuiltIns;

@@ -3640,28 +3640,45 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expression e0 = null;  Expression e1 = null;  Expression ee;  bool anyDots = false;

 		List<Expression> multipleLengths = null; bool takeRest = false; // takeRest is relevant only if multipleLengths is non-null

 		List<Expression> multipleIndices = null;

+		List<Tuple<IToken, string, Expression>> updates;

+		Expression v;

 		

 		if (la.kind == 27) {

-			DotSuffix(out id, out x);

-			if (x != null) {

-			 // process id as a Suffix in its own right

-			 e = new ExprDotName(id, e, id.val, null);

-			 id = x;  // move to the next Suffix

-			}

-			IToken openParen = null;  List<Type> typeArgs = null;  List<Expression> args = null;

-			

-			if (IsGenericInstantiation()) {

-				typeArgs = new List<Type>(); 

-				GenericInstantiation(typeArgs);

-			} else if (la.kind == 106) {

-				HashCall(id, out openParen, out typeArgs, out args);

+			Get();

+			if (la.kind == 50) {

+				Get();

+				x = t; updates = new List<Tuple<IToken, string, Expression>>(); 

+				MemberBindingUpdate(out id, out v);

+				updates.Add(Tuple.Create(id, id.val, v)); 

+				while (la.kind == 22) {

+					Get();

+					MemberBindingUpdate(out id, out v);

+					updates.Add(Tuple.Create(id, id.val, v)); 

+				}

+				Expect(51);

+				e = new DatatypeUpdateExpr(x, e, updates); 

 			} else if (StartOf(30)) {

-			} else SynErr(225);

-			e = new ExprDotName(id, e, id.val, typeArgs);

-			if (openParen != null) {

-			 e = new ApplySuffix(openParen, e, args);

-			}

-			

+				DotSuffix(out id, out x);

+				if (x != null) {

+				 // process id as a Suffix in its own right

+				 e = new ExprDotName(id, e, id.val, null);

+				 id = x;  // move to the next Suffix

+				}

+				IToken openParen = null;  List<Type> typeArgs = null;  List<Expression> args = null;

+				

+				if (IsGenericInstantiation()) {

+					typeArgs = new List<Type>(); 

+					GenericInstantiation(typeArgs);

+				} else if (la.kind == 106) {

+					HashCall(id, out openParen, out typeArgs, out args);

+				} else if (StartOf(31)) {

+				} else SynErr(225);

+				e = new ExprDotName(id, e, id.val, typeArgs);

+				if (openParen != null) {

+				 e = new ApplySuffix(openParen, e, args);

+				}

+				

+			} else SynErr(226);

 		} else if (la.kind == 48) {

 			Get();

 			x = t; 

@@ -3709,7 +3726,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(226);

+				} else SynErr(227);

 			} else if (la.kind == 137) {

 				Get();

 				anyDots = true; 

@@ -3717,7 +3734,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 					Expression(out ee, true, true);

 					e1 = ee; 

 				}

-			} else SynErr(227);

+			} else SynErr(228);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			 // make sure an array class with this dimensionality exists

@@ -3761,7 +3778,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			Expect(51);

 			e = new ApplySuffix(openParen, e, args); 

-		} else SynErr(228);

+		} else SynErr(229);

 	}

 

 	void ISetDisplayExpr(IToken/*!*/ setToken, bool finite, out Expression e) {

@@ -3803,7 +3820,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				}

 			}

 			Expect(51);

-		} else SynErr(229);

+		} else SynErr(230);

 		while (la.kind == 44 || la.kind == 45) {

 			if (la.kind == 44) {

 				Get();

@@ -3886,7 +3903,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			NamedExpr(out e, allowSemi, allowLambda);

 			break;

 		}

-		default: SynErr(230); break;

+		default: SynErr(231); break;

 		}

 	}

 

@@ -3900,8 +3917,8 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			GenericInstantiation(typeArgs);

 		} else if (la.kind == 106) {

 			HashCall(id, out openParen, out typeArgs, out args);

-		} else if (StartOf(30)) {

-		} else SynErr(231);

+		} else if (StartOf(31)) {

+		} else SynErr(232);

 		e = new NameSegment(id, id.val, typeArgs);

 		if (openParen != null) {

 		 e = new ApplySuffix(openParen, e, args);

@@ -3930,7 +3947,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			}

 			e = new SeqDisplayExpr(x, elements); 

 			Expect(49);

-		} else SynErr(232);

+		} else SynErr(233);

 	}

 

 	void MultiSetExpr(out Expression e) {

@@ -3954,7 +3971,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			Expression(out e, true, true);

 			e = new MultiSetFormingExpr(x, e); 

 			Expect(51);

-		} else SynErr(233);

+		} else SynErr(234);

 	}

 

 	void ConstAtomExpression(out Expression e, bool allowSemi, bool allowLambda) {

@@ -4050,7 +4067,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			ParensExpression(out e, allowSemi, allowLambda);

 			break;

 		}

-		default: SynErr(234); break;

+		default: SynErr(235); break;

 		}

 	}

 

@@ -4079,7 +4096,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 n = BigInteger.Zero;

 			}

 			

-		} else SynErr(235);

+		} else SynErr(236);

 	}

 

 	void Dec(out Basetypes.BigDec d) {

@@ -4123,7 +4140,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 30) {

 			Get();

 			oneShot = true; 

-		} else SynErr(236);

+		} else SynErr(237);

 	}

 

 	void MapLiteralExpressions(out List<ExpressionPair> elements) {

@@ -4181,12 +4198,12 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				cases.Add(c); 

 			}

 			Expect(47);

-		} else if (StartOf(31)) {

+		} else if (StartOf(32)) {

 			while (la.kind == _case) {

 				CaseExpression(out c, allowSemi, allowLambda);

 				cases.Add(c); 

 			}

-		} else SynErr(237);

+		} else SynErr(238);

 		e = new MatchExpr(x, e, cases, usesOptionalBrace); 

 	}

 

@@ -4204,7 +4221,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 124 || la.kind == 125) {

 			Exists();

 			x = t; 

-		} else SynErr(238);

+		} else SynErr(239);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body, allowSemi, allowLambda);

@@ -4253,7 +4270,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			AssumeStmt(out s);

 		} else if (la.kind == 32) {

 			CalcStmt(out s);

-		} else SynErr(239);

+		} else SynErr(240);

 	}

 

 	void LetExpr(out Expression e, bool allowSemi, bool allowLambda) {

@@ -4297,7 +4314,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 			 }

 			}

 			

-		} else SynErr(240);

+		} else SynErr(241);

 		Expression(out e, false, true);

 		letRHSs.Add(e); 

 		while (la.kind == 22) {

@@ -4357,7 +4374,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 				arguments.Add(pat); 

 			}

 			Expect(51);

-		} else SynErr(241);

+		} else SynErr(242);

 		Expect(29);

 		Expression(out body, allowSemi, allowLambda);

 		c = new MatchCaseExpr(x, name, arguments, body); 

@@ -4383,12 +4400,24 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		Expect(51);

 	}

 

+	void MemberBindingUpdate(out IToken id, out Expression e) {

+		id = Token.NoToken; e = dummyExpr; 

+		if (la.kind == 1) {

+			Get();

+			id = t; 

+		} else if (la.kind == 2) {

+			Get();

+			id = t; 

+		} else SynErr(243);

+		Expect(95);

+		Expression(out e, true, true);

+	}

+

 	void DotSuffix(out IToken x, out IToken y) {

 		Contract.Ensures(Contract.ValueAtReturn(out x) != null);

 		x = Token.NoToken;

 		y = null;

 		

-		Expect(27);

 		if (la.kind == 1) {

 			Get();

 			x = t; 

@@ -4422,7 +4451,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		} else if (la.kind == 44) {

 			Get();

 			x = t; 

-		} else SynErr(242);

+		} else SynErr(244);

 	}

 

 

@@ -4467,6 +4496,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
 		{_x,_x,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_x,_x,_x},

 		{_T,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_T, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_T,_x, _T,_T,_x,_x, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_x,_x,_x},

 		{_x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_T,_x, _x,_T,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_T,_x,_x, _x,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_x,_x,_x, _x,_x,_T,_x, _T,_T,_x,_T, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},

+		{_x,_T,_T,_x, _T,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _T,_T,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x, _x,_x,_x,_x},

 		{_T,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_T,_T,_x, _x,_T,_x,_x, _x,_x,_T,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x},

 		{_T,_T,_T,_T, _T,_x,_x,_x, _T,_x,_T,_x, _x,_x,_x,_x, _x,_x,_x,_T, _T,_T,_T,_T, _T,_x,_T,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _x,_T,_T,_x, _x,_T,_x,_x, _x,_x,_T,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_x,_T,_T, _T,_T,_T,_T, _T,_T,_x,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x, _x,_x,_T,_T, _T,_T,_T,_T, _T,_T,_T,_T, _T,_T,_x,_x}

 

@@ -4725,20 +4755,22 @@ public class Errors {
 			case 226: s = "invalid Suffix"; break;

 			case 227: s = "invalid Suffix"; break;

 			case 228: s = "invalid Suffix"; break;

-			case 229: s = "invalid LambdaExpression"; break;

-			case 230: s = "invalid EndlessExpression"; break;

-			case 231: s = "invalid NameSegment"; break;

-			case 232: s = "invalid DisplayExpr"; break;

-			case 233: s = "invalid MultiSetExpr"; break;

-			case 234: s = "invalid ConstAtomExpression"; break;

-			case 235: s = "invalid Nat"; break;

-			case 236: s = "invalid LambdaArrow"; break;

-			case 237: s = "invalid MatchExpression"; break;

-			case 238: s = "invalid QuantifierGuts"; break;

-			case 239: s = "invalid StmtInExpr"; break;

-			case 240: s = "invalid LetExpr"; break;

-			case 241: s = "invalid CaseExpression"; break;

-			case 242: s = "invalid DotSuffix"; break;

+			case 229: s = "invalid Suffix"; break;

+			case 230: s = "invalid LambdaExpression"; break;

+			case 231: s = "invalid EndlessExpression"; break;

+			case 232: s = "invalid NameSegment"; break;

+			case 233: s = "invalid DisplayExpr"; break;

+			case 234: s = "invalid MultiSetExpr"; break;

+			case 235: s = "invalid ConstAtomExpression"; break;

+			case 236: s = "invalid Nat"; break;

+			case 237: s = "invalid LambdaArrow"; break;

+			case 238: s = "invalid MatchExpression"; break;

+			case 239: s = "invalid QuantifierGuts"; break;

+			case 240: s = "invalid StmtInExpr"; break;

+			case 241: s = "invalid LetExpr"; break;

+			case 242: s = "invalid CaseExpression"; break;

+			case 243: s = "invalid MemberBindingUpdate"; break;

+			case 244: s = "invalid DotSuffix"; break;

 

 			default: s = "error " + n; break;

 		}

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
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 3cb98f65..74ff60e7 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -7632,12 +7632,27 @@ namespace Microsoft.Dafny
           }

           var let = ResolveDatatypeUpdate(expr.tok, eIter, e.Seq.Type.AsDatatype, memberUpdates, true, opts);

           if (let != null) {

+            reporter.Warning(MessageSource.Resolver, expr.tok, "datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)");

             e.ResolvedUpdateExpr = let;

             expr.Type = e.Seq.Type;

           }

 

         } else {

-          reporter.Error(MessageSource.Resolver, expr, "update requires a sequence, map, or datatype (got {0})", e.Seq.Type);

+          reporter.Error(MessageSource.Resolver, expr, "update requires a sequence, map, multiset, or datatype (got {0})", e.Seq.Type);

+        }

+

+      } else if (expr is DatatypeUpdateExpr) {

+        var e = (DatatypeUpdateExpr)expr;

+        ResolveExpression(e.Root, opts);

+        var ty = e.Root.Type;

+        if (!ty.IsDatatype) {

+          reporter.Error(MessageSource.Resolver, expr, "datatype update expression requires a root expression of a datatype (got {0})", ty);

+        } else {

+          var let = ResolveDatatypeUpdate(expr.tok, e.Root, ty.AsDatatype, e.Updates, false, opts);

+          if (let != null) {

+            e.ResolvedExpression = let;

+            expr.Type = ty;

+          }

         }

 

       } else if (expr is FunctionCallExpr) {

@@ -8080,9 +8095,9 @@ namespace Microsoft.Dafny
     /// <summary>

     /// Attempts to produce a let expression from the given datatype updates.  Returns that let expression upon success, and null otherwise.

     /// </summary>

-    Expression ResolveDatatypeUpdate(IToken tok, Expression orig, DatatypeDecl dt, List<Tuple<IToken, string, Expression>> memberUpdates, bool sequentialUpdates, ResolveOpts opts) {

+    Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, List<Tuple<IToken, string, Expression>> memberUpdates, bool sequentialUpdates, ResolveOpts opts) {

       Contract.Requires(tok != null);

-      Contract.Requires(orig != null);

+      Contract.Requires(root != null);

       Contract.Requires(dt != null);

       Contract.Requires(memberUpdates != null);

       Contract.Requires(opts != null);

@@ -8129,13 +8144,13 @@ namespace Microsoft.Dafny
       if (ctor != null) {

         // Rewrite an update of the form "dt[dtor := E]" to be "let d' := dt in dtCtr(E, d'.dtor2, d'.dtor3,...)"

         // Wrapping it in a let expr avoids exponential growth in the size of the expression

-        // More generally, rewrite "E0[dtor1 := E1][dtor2 := E2]...[dtorn := En]" where "E0" is "orig" to

+        // More generally, rewrite "E0[dtor1 := E1][dtor2 := E2]...[dtorn := En]" where "E0" is "root" to

         //   "let d' := E0 in dtCtr(...mixtures of Ek and d'.dtorj...)"

 

         // Create a unique name for d', the variable we introduce in the let expression

         var tmpName = FreshTempVarName("dt_update_tmp#", opts.codeContext);

         var tmpVarIdExpr = new IdentifierExpr(tok, tmpName);

-        var tmpVarBv = new BoundVar(tok, tmpName, orig.Type);

+        var tmpVarBv = new BoundVar(tok, tmpName, root.Type);

 

         // Build the arguments to the datatype constructor, using the updated value in the appropriate slot

         var ctor_args = new List<Expression>();

@@ -8151,7 +8166,7 @@ namespace Microsoft.Dafny
         DatatypeValue ctor_call = new DatatypeValue(tok, ctor.EnclosingDatatype.Name, ctor.Name, ctor_args);

 

         CasePattern tmpVarPat = new CasePattern(tok, tmpVarBv);

-        LetExpr let = new LetExpr(tok, new List<CasePattern>() { tmpVarPat }, new List<Expression>() { orig }, ctor_call, true);

+        LetExpr let = new LetExpr(tok, new List<CasePattern>() { tmpVarPat }, new List<Expression>() { root }, ctor_call, true);

 

         ResolveExpression(let, opts);

         return let;

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;

 

diff --git a/Test/dafny0/DatatypeUpdate.dfy b/Test/dafny0/DatatypeUpdate.dfy
index 76cce5ce..b7905928 100644
--- a/Test/dafny0/DatatypeUpdate.dfy
+++ b/Test/dafny0/DatatypeUpdate.dfy
@@ -1,6 +1,6 @@
 // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

-

+module OldSyntax {

 datatype MyDataType = MyConstructor(myint:int, mybool:bool) 

                     | MyOtherConstructor(otherbool:bool) 

                     | MyNumericConstructor(42:int)

@@ -35,3 +35,51 @@ method UpdateNumNam(nn: NumericNames, y: int) returns (pp: NumericNames)
 {

   pp := nn[010 := y];  // not to be confused with a field name 10

 }

+}

+

+module NewSyntax {

+datatype MyDataType = MyConstructor(myint:int, mybool:bool) 

+                    | MyOtherConstructor(otherbool:bool) 

+                    | MyNumericConstructor(42:int)

+

+method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi:MyDataType, jkl:MyDataType)

+    requires foo.MyConstructor?;

+    ensures abc == foo.(myint := x + 2);

+    ensures def == foo.(otherbool := !foo.mybool);

+    ensures ghi == foo.(myint := 2).(mybool := false);

+    //ensures jkl == foo.(non_destructor := 5);      // Resolution error: no non_destructor in MyDataType

+    ensures jkl == foo.(42 := 7);

+{

+    abc := MyConstructor(x + 2, foo.mybool); 

+    abc := foo.(myint := x + 2);

+    def := MyOtherConstructor(!foo.mybool);

+    ghi := MyConstructor(2, false);

+    jkl := foo.(42 := 7);

+

+    assert abc.(myint := abc.myint - 2) == foo.(myint := x);

+}

+

+// regression test (for a previous bug in the Translator.Substituter):

+datatype Dt = Ctor(x: int, y: bool)

+function F(d: Dt): Dt

+{

+  d.(x := 5)

+}

+

+datatype NumericNames = NumNam(010: int, 10: real, f: bool)

+

+method UpdateNumNam(nn: NumericNames, y: int) returns (pp: NumericNames)

+{

+  pp := nn.(010 := y);  // not to be confused with a field name 10

+}

+

+method MultipleUpdates(nn: NumericNames, y: int) returns (pp: NumericNames)

+  ensures pp.010 == y

+{

+  if * {

+    pp := nn.(10 := 0.10, 010 := y);

+  } else {

+    pp := nn.(010 := y, f := true, 10 := 0.10);

+  }

+}

+}

diff --git a/Test/dafny0/DatatypeUpdate.dfy.expect b/Test/dafny0/DatatypeUpdate.dfy.expect
index 790f6509..9a924214 100644
--- a/Test/dafny0/DatatypeUpdate.dfy.expect
+++ b/Test/dafny0/DatatypeUpdate.dfy.expect
@@ -1,2 +1,13 @@
+DatatypeUpdate.dfy(10,22): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(11,22): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(12,22): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(12,34): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(14,22): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(17,14): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(20,14): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(22,14): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(22,45): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(29,3): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

+DatatypeUpdate.dfy(36,10): Warning: datatype update syntax D[f := E] is deprecated; the new syntax is D.(f := E)

 

-Dafny program verifier finished with 5 verified, 0 errors

+Dafny program verifier finished with 12 verified, 0 errors

diff --git a/Test/dafny0/DatatypeUpdateResolution.dfy b/Test/dafny0/DatatypeUpdateResolution.dfy
new file mode 100644
index 00000000..26142fa8
--- /dev/null
+++ b/Test/dafny0/DatatypeUpdateResolution.dfy
@@ -0,0 +1,20 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+datatype MyDataType = MyConstructor(myint:int, mybool:bool) 

+                    | MyOtherConstructor(otherbool:bool) 

+                    | MyNumericConstructor(42:int)

+datatype SomeOtherType = S_O_T(non_destructor: int)

+

+method test(foo:MyDataType, x:int) returns (abc:MyDataType, def:MyDataType, ghi:MyDataType, jkl:MyDataType)

+  requires foo.MyConstructor?

+  ensures abc == foo.(myint := x + 2)

+  ensures jkl == foo.(non_destructor := 5)      // error: 'non_destructor' is not a destructor in MyDataType

+  ensures jkl == foo.(mybool := true, 40 := 100, myint := 200)  // error: '40' is not a destructor

+{

+  abc := MyConstructor(x + 2, foo.mybool).(myint := x + 3);

+  abc := foo.(myint := x + 2, mybool := true).(mybool := false);  // allowed

+  def := MyOtherConstructor(!foo.mybool).(otherbool := true, otherbool := true);  // error: duplicated member

+  ghi := MyConstructor(2, false).(otherbool := true);  // allowed, and will generate verification error

+  jkl := foo.(42 := 7, otherbool := true);  // error: members are from different constructors

+}

diff --git a/Test/dafny0/DatatypeUpdateResolution.dfy.expect b/Test/dafny0/DatatypeUpdateResolution.dfy.expect
new file mode 100644
index 00000000..db3e1fe2
--- /dev/null
+++ b/Test/dafny0/DatatypeUpdateResolution.dfy.expect
@@ -0,0 +1,5 @@
+DatatypeUpdateResolution.dfy(12,22): Error: member 'non_destructor' does not exist in datatype 'MyDataType'

+DatatypeUpdateResolution.dfy(13,38): Error: member '40' does not exist in datatype 'MyDataType'

+DatatypeUpdateResolution.dfy(17,61): Error: duplicate update member 'otherbool'

+DatatypeUpdateResolution.dfy(19,23): Error: updated datatype members must belong to the same constructor ('otherbool' belongs to 'MyOtherConstructor' and '42' belongs to 'MyNumericConstructor'

+4 resolution/type errors detected in DatatypeUpdateResolution.dfy