From 628acc07a07bd5516551dc2caa2c4612f70d2688 Mon Sep 17 00:00:00 2001 From: leino Date: Fri, 23 Oct 2015 18:30:11 -0700 Subject: 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) --- Source/Dafny/Cloner.cs | 4 ++ Source/Dafny/Dafny.atg | 52 ++++++++++++------ Source/Dafny/DafnyAst.cs | 25 ++++++++- Source/Dafny/Parser.cs | 140 +++++++++++++++++++++++++++++------------------ Source/Dafny/Printer.cs | 21 ++++++- Source/Dafny/Resolver.cs | 27 +++++++-- Source/Dafny/Rewriter.cs | 4 ++ 7 files changed, 194 insertions(+), 79 deletions(-) (limited to 'Source') 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 Expression e0 = null; Expression e1 = null; Expression ee; bool anyDots = false; List multipleLengths = null; bool takeRest = false; // takeRest is relevant only if multipleLengths is non-null List multipleIndices = null; + List> updates; + Expression v; .) - ( DotSuffix (. if (x != null) { + ( "." + ( "(" (. x = t; updates = new List>(); .) + MemberBindingUpdate (. updates.Add(Tuple.Create(id, id.val, v)); .) + { "," MemberBindingUpdate (. updates.Add(Tuple.Create(id, id.val, v)); .) + } + ")" + (. e = new DatatypeUpdateExpr(x, e, updates); .) + | DotSuffix (. 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 .) - ( IF(IsGenericInstantiation()) - (. typeArgs = new List(); .) - GenericInstantiation - | HashCall - | /* empty */ + ( IF(IsGenericInstantiation()) + (. typeArgs = new List(); .) + GenericInstantiation + | HashCall + | /* 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 (. e0 = ee; .) ( ".." (. anyDots = true; .) @@ -2969,10 +2979,10 @@ Ident 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 x = Token.NoToken; y = null; .) - "." ( ident (. x = t; .) | digits (. x = t; .) | decimaldigits (. x = t; @@ -3008,6 +3017,15 @@ DotSuffix | "reads" (. x = t; .) ) . +MemberBindingUpdate += (. id = Token.NoToken; e = dummyExpr; .) + ( ident (. id = t; .) + | digits (. id = t; .) + ) + ":=" + Expression + . + // Identifier, disallowing leading underscores NoUSIdent = (. 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 SubExpressions { get { yield return Obj; } } @@ -7785,6 +7784,30 @@ namespace Microsoft.Dafny { } } + public class DatatypeUpdateExpr : ConcreteSyntaxExpression + { + public readonly Expression Root; + public readonly List> Updates; + public DatatypeUpdateExpr(IToken tok, Expression root, List> 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 SubExpressions { + get { + yield return Root; + foreach (var update in Updates) { + yield return update.Item3; + } + } + } + } + /// /// 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/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression e0 = null; Expression e1 = null; Expression ee; bool anyDots = false; List multipleLengths = null; bool takeRest = false; // takeRest is relevant only if multipleLengths is non-null List multipleIndices = null; + List> 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 typeArgs = null; List args = null; - - if (IsGenericInstantiation()) { - typeArgs = new List(); - 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>(); + 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 typeArgs = null; List args = null; + + if (IsGenericInstantiation()) { + typeArgs = new List(); + 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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 elements) { @@ -4181,12 +4198,12 @@ List/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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/*!*/ 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 /// /// Attempts to produce a let expression from the given datatype updates. Returns that let expression upon success, and null otherwise. /// - Expression ResolveDatatypeUpdate(IToken tok, Expression orig, DatatypeDecl dt, List> memberUpdates, bool sequentialUpdates, ResolveOpts opts) { + Expression ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, List> 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(); @@ -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() { tmpVarPat }, new List() { orig }, ctor_call, true); + LetExpr let = new LetExpr(tok, new List() { tmpVarPat }, new List() { 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; -- cgit v1.2.3