diff options
| -rw-r--r-- | Source/Dafny/Cloner.cs | 4 | ||||
| -rw-r--r-- | Source/Dafny/Dafny.atg | 52 | ||||
| -rw-r--r-- | Source/Dafny/DafnyAst.cs | 25 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 140 | ||||
| -rw-r--r-- | Source/Dafny/Printer.cs | 21 | ||||
| -rw-r--r-- | Source/Dafny/Resolver.cs | 27 | ||||
| -rw-r--r-- | Source/Dafny/Rewriter.cs | 4 | ||||
| -rw-r--r-- | Test/dafny0/DatatypeUpdate.dfy | 50 | ||||
| -rw-r--r-- | Test/dafny0/DatatypeUpdate.dfy.expect | 13 | ||||
| -rw-r--r-- | Test/dafny0/DatatypeUpdateResolution.dfy | 20 | ||||
| -rw-r--r-- | Test/dafny0/DatatypeUpdateResolution.dfy.expect | 5 |
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
|