diff options
Diffstat (limited to 'Source/Dafny/Translator.cs')
| -rw-r--r-- | Source/Dafny/Translator.cs | 214 |
1 files changed, 204 insertions, 10 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index d1c77122..be18b658 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -43,6 +43,7 @@ namespace Microsoft.Dafny { public readonly Bpl.Type BoxType;
public readonly Bpl.Type TickType;
private readonly Bpl.TypeSynonymDecl setTypeCtor;
+ private readonly Bpl.TypeSynonymDecl multiSetTypeCtor;
private readonly Bpl.TypeCtorDecl seqTypeCtor;
readonly Bpl.TypeCtorDecl fieldName;
public readonly Bpl.Type HeapType;
@@ -58,6 +59,7 @@ namespace Microsoft.Dafny { Contract.Invariant(BoxType != null);
Contract.Invariant(TickType != null);
Contract.Invariant(setTypeCtor != null);
+ Contract.Invariant(multiSetTypeCtor != null);
Contract.Invariant(seqTypeCtor != null);
Contract.Invariant(fieldName != null);
Contract.Invariant(HeapType != null);
@@ -78,6 +80,14 @@ namespace Microsoft.Dafny { return new Bpl.TypeSynonymAnnotation(Token.NoToken, setTypeCtor, new Bpl.TypeSeq(ty));
}
+ public Bpl.Type MultiSetType(IToken tok, Bpl.Type ty) {
+ Contract.Requires(tok != null);
+ Contract.Requires(ty != null);
+ Contract.Ensures(Contract.Result<Bpl.Type>() != null);
+
+ return new Bpl.TypeSynonymAnnotation(Token.NoToken, multiSetTypeCtor, new Bpl.TypeSeq(ty));
+ }
+
public Bpl.Type SeqType(IToken tok, Bpl.Type ty) {
Contract.Requires(tok != null);
Contract.Requires(ty != null);
@@ -101,7 +111,7 @@ namespace Microsoft.Dafny { }
public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType,
- Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
+ Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType,
Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,
Bpl.Constant allocField) {
@@ -110,6 +120,7 @@ namespace Microsoft.Dafny { Contract.Requires(boxType != null);
Contract.Requires(tickType != null);
Contract.Requires(setTypeCtor != null);
+ Contract.Requires(multiSetTypeCtor != null);
Contract.Requires(seqTypeCtor != null);
Contract.Requires(fieldNameType != null);
Contract.Requires(heap != null);
@@ -124,6 +135,7 @@ namespace Microsoft.Dafny { this.BoxType = new Bpl.CtorType(Token.NoToken, boxType, new Bpl.TypeSeq());
this.TickType = new Bpl.CtorType(Token.NoToken, tickType, new Bpl.TypeSeq());
this.setTypeCtor = setTypeCtor;
+ this.multiSetTypeCtor = multiSetTypeCtor;
this.seqTypeCtor = seqTypeCtor;
this.fieldName = fieldNameType;
this.HeapType = heap.TypedIdent.Type;
@@ -142,9 +154,10 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: resolution errors encountered in Dafny prelude");
return null;
}
-
+
Bpl.TypeCtorDecl refType = null;
Bpl.TypeSynonymDecl setTypeCtor = null;
+ Bpl.TypeSynonymDecl multiSetTypeCtor = null;
Bpl.TypeCtorDecl seqTypeCtor = null;
Bpl.TypeCtorDecl fieldNameType = null;
Bpl.TypeCtorDecl classNameType = null;
@@ -179,6 +192,9 @@ namespace Microsoft.Dafny { if (dt.Name == "Set") {
setTypeCtor = dt;
}
+ if (dt.Name == "MultiSet") {
+ multiSetTypeCtor = dt;
+ }
} else if (d is Bpl.Constant) {
Bpl.Constant c = (Bpl.Constant)d;
if (c.Name == "alloc") {
@@ -195,6 +211,8 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of type Seq");
} else if (setTypeCtor == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Set");
+ } else if (multiSetTypeCtor == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type MultiSet");
} else if (fieldNameType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");
} else if (classNameType == null) {
@@ -215,7 +233,7 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc");
} else {
return new PredefinedDecls(refType, boxType, tickType,
- setTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
+ setTypeCtor, multiSetTypeCtor, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
allocField);
}
return null;
@@ -435,6 +453,20 @@ namespace Microsoft.Dafny { rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
+ } else if (arg.Type is MultiSetType) {
+ // axiom (forall params, d: Datatype :: 0 < arg[d] ==> DtRank(d) < DtRank(#dt.ctor(params)));
+ // that is:
+ // axiom (forall params, d: Datatype :: 0 < arg[Box(d)] ==> DtRank(d) < DtRank(#dt.ctor(params)));
+ CreateBoundVariables(ctor.Formals, out bvs, out args);
+ Bpl.Variable dVar = new Bpl.BoundVariable(arg.tok, new Bpl.TypedIdent(arg.tok, "d", predef.DatatypeType));
+ bvs.Add(dVar);
+ Bpl.IdentifierExpr ie = new Bpl.IdentifierExpr(arg.tok, dVar);
+ Bpl.Expr ante = Bpl.Expr.Gt(Bpl.Expr.SelectTok(arg.tok, args[i], FunctionCall(arg.tok, BuiltinFunction.Box, null, ie)), Bpl.Expr.Literal(0));
+ lhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, ie);
+ Bpl.Expr rhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);
+ rhs = FunctionCall(ctor.tok, BuiltinFunction.DtRank, null, rhs);
+ q = new Bpl.ForallExpr(ctor.tok, bvs, Bpl.Expr.Imp(ante, Bpl.Expr.Lt(lhs, rhs)));
+ sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
}
i++;
}
@@ -2355,7 +2387,7 @@ namespace Microsoft.Dafny { if (a == null) {
return null;
}
- Bpl.Expr t = new Bpl.IdentifierExpr(tok, ct is SetType ? "class.set" : "class.seq", predef.ClassNameType);
+ Bpl.Expr t = new Bpl.IdentifierExpr(tok, ct is SetType ? "class.set" : "class.seq", predef.ClassNameType); // ^^^ todo: this needs to talk about multisets too.
return FunctionCall(tok, BuiltinFunction.TypeTuple, null, t, a);
} else {
UserDefinedType ct = (UserDefinedType)type;
@@ -2891,6 +2923,8 @@ namespace Microsoft.Dafny { return predef.DatatypeType;
} else if (type is SetType) {
return predef.SetType(Token.NoToken, predef.BoxType);
+ } else if (type is MultiSetType) {
+ return predef.MultiSetType(Token.NoToken, predef.BoxType);
} else if (type is SeqType) {
return predef.SeqType(Token.NoToken, predef.BoxType);
} else {
@@ -3194,6 +3228,10 @@ namespace Microsoft.Dafny { Bpl.Expr oInS;
if (s.Collection.Type is SetType) {
oInS = etran.TrInSet(stmt.Tok, o, s.Collection, ((SetType)s.Collection.Type).Arg);
+ } else if (s.Collection.Type is MultiSetType) {
+ // should not be reached.
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
} else {
Bpl.BoundVariable iVar = new Bpl.BoundVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$i", Bpl.Type.Int));
Bpl.IdentifierExpr i = new Bpl.IdentifierExpr(stmt.Tok, iVar);
@@ -4016,7 +4054,22 @@ namespace Microsoft.Dafny { Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));
return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));
}
-
+
+ } else if (type is MultiSetType) {
+ MultiSetType st = (MultiSetType)type;
+ // (forall t: BoxType :: { x[t] } 0 < x[t] ==> Unbox(t)-has-the-expected-type)
+ Bpl.BoundVariable tVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$t#" + otherTmpVarCount, predef.BoxType));
+ otherTmpVarCount++;
+ Bpl.Expr t = new Bpl.IdentifierExpr(tok, tVar);
+ Bpl.Expr xSubT = Bpl.Expr.Gt(Bpl.Expr.SelectTok(tok, x, t), Bpl.Expr.Literal(0));
+ Bpl.Expr unboxT = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), t);
+
+ Bpl.Expr wh = GetWhereClause(tok, unboxT, st.Arg, etran);
+ if (wh != null) {
+ Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(xSubT));
+ return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));
+ }
+
} else if (type is SeqType) {
SeqType st = (SeqType)type;
// (forall i: int :: { Seq#Index(x,i) }
@@ -4607,7 +4660,7 @@ namespace Microsoft.Dafny { } else if (expr is BoogieWrapper) {
var e = (BoogieWrapper)expr;
return e.Expr;
-
+
} else if (expr is SetDisplayExpr) {
SetDisplayExpr e = (SetDisplayExpr)expr;
Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SetEmpty, predef.BoxType);
@@ -4616,7 +4669,16 @@ namespace Microsoft.Dafny { s = translator.FunctionCall(expr.tok, BuiltinFunction.SetUnionOne, predef.BoxType, s, ss);
}
return s;
-
+
+ } else if (expr is MultiSetDisplayExpr) { //^^^ todo: add multiset to BuiltinFunction
+ MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr;
+ Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEmpty, predef.BoxType);
+ foreach (Expression ee in e.Elements) {
+ Bpl.Expr ss = BoxIfNecessary(expr.tok, TrExpr(ee), cce.NonNull(ee.Type));
+ s = translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetUnionOne, predef.BoxType, s, ss);
+ }
+ return s;
+
} else if (expr is SeqDisplayExpr) {
SeqDisplayExpr e = (SeqDisplayExpr)expr;
Bpl.Expr s = translator.FunctionCall(expr.tok, BuiltinFunction.SeqEmpty, predef.BoxType);
@@ -4798,6 +4860,11 @@ namespace Microsoft.Dafny { } else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInSet) {
Bpl.Expr arg = TrInSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type)); // let TrInSet translate e.E1
return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, arg);
+ } else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.InMultiSet) {
+ return TrInMultiSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type)); // let TrInMultiSet translate e.E1
+ } else if (e.ResolvedOp == BinaryExpr.ResolvedOpcode.NotInMultiSet) {
+ Bpl.Expr arg = TrInMultiSet(expr.tok, e0, e.E1, cce.NonNull(e.E0.Type)); // let TrInMultiSet translate e.E1
+ return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, arg);
}
Bpl.Expr e1 = TrExpr(e.E1);
BinaryOperator.Opcode bOpcode;
@@ -4840,7 +4907,9 @@ namespace Microsoft.Dafny { case BinaryExpr.ResolvedOpcode.SetNeq:
return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, translator.FunctionCall(expr.tok, BuiltinFunction.SetEqual, null, e0, e1));
case BinaryExpr.ResolvedOpcode.ProperSubset:
- return ProperSubset(expr.tok, e0, e1);
+ return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And,
+ translator.FunctionCall(expr.tok, BuiltinFunction.SetSubset, null, e0, e1),
+ Bpl.Expr.Not(translator.FunctionCall(expr.tok, BuiltinFunction.SetEqual, null, e0, e1)));
case BinaryExpr.ResolvedOpcode.Subset:
return translator.FunctionCall(expr.tok, BuiltinFunction.SetSubset, null, e0, e1);
case BinaryExpr.ResolvedOpcode.Superset:
@@ -4853,12 +4922,43 @@ namespace Microsoft.Dafny { return translator.FunctionCall(expr.tok, BuiltinFunction.SetDisjoint, null, e0, e1);
case BinaryExpr.ResolvedOpcode.InSet:
Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above
+ case BinaryExpr.ResolvedOpcode.NotInSet:
+ Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above
case BinaryExpr.ResolvedOpcode.Union:
return translator.FunctionCall(expr.tok, BuiltinFunction.SetUnion, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.Intersection:
return translator.FunctionCall(expr.tok, BuiltinFunction.SetIntersection, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.SetDifference:
return translator.FunctionCall(expr.tok, BuiltinFunction.SetDifference, translator.TrType(cce.NonNull((SetType)expr.Type).Arg), e0, e1);
+
+ case BinaryExpr.ResolvedOpcode.MultiSetEq:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1);
+ case BinaryExpr.ResolvedOpcode.MultiSetNeq:
+ return Bpl.Expr.Unary(expr.tok, UnaryOperator.Opcode.Not, translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1));
+ case BinaryExpr.ResolvedOpcode.ProperMultiSubset:
+ return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And,
+ translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetSubset, null, e0, e1),
+ Bpl.Expr.Not(translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1)));
+ case BinaryExpr.ResolvedOpcode.MultiSubset:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetSubset, null, e0, e1);
+ case BinaryExpr.ResolvedOpcode.MultiSuperset:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetSubset, null, e1, e0);
+ case BinaryExpr.ResolvedOpcode.ProperMultiSuperset:
+ return Bpl.Expr.Binary(expr.tok, BinaryOperator.Opcode.And,
+ translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetSubset, null, e1, e0),
+ Bpl.Expr.Not(translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetEqual, null, e0, e1)));
+ case BinaryExpr.ResolvedOpcode.MultiSetDisjoint:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetDisjoint, null, e0, e1);
+ case BinaryExpr.ResolvedOpcode.InMultiSet:
+ Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above
+ case BinaryExpr.ResolvedOpcode.NotInMultiSet:
+ Contract.Assert(false); throw new cce.UnreachableException(); // this case handled above
+ case BinaryExpr.ResolvedOpcode.MultiSetUnion:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetUnion, translator.TrType(cce.NonNull((MultiSetType)expr.Type).Arg), e0, e1);
+ case BinaryExpr.ResolvedOpcode.MultiSetIntersection:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetIntersection, translator.TrType(cce.NonNull((MultiSetType)expr.Type).Arg), e0, e1);
+ case BinaryExpr.ResolvedOpcode.MultiSetDifference:
+ return translator.FunctionCall(expr.tok, BuiltinFunction.MultiSetDifference, translator.TrType(cce.NonNull((MultiSetType)expr.Type).Arg), e0, e1);
case BinaryExpr.ResolvedOpcode.SeqEq:
return translator.FunctionCall(expr.tok, BuiltinFunction.SeqEqual, null, e0, e1);
@@ -5173,7 +5273,49 @@ namespace Microsoft.Dafny { }
return Bpl.Expr.SelectTok(tok, TrExpr(s), BoxIfNecessary(tok, elmt, elmtType));
}
-
+
+ /// <summary>
+ /// Translate like 0 < s[Box(elmt)], but try to avoid as many set functions as possible in the
+ /// translation, because such functions can mess up triggering.
+ /// </summary>
+ public Bpl.Expr TrInMultiSet(IToken tok, Bpl.Expr elmt, Expression s, Type elmtType) {
+ Contract.Requires(tok != null);
+ Contract.Requires(elmt != null);
+ Contract.Requires(s != null);
+ Contract.Requires(elmtType != null);
+
+ Contract.Ensures(Contract.Result<Bpl.Expr>() != null);
+
+ if (s is BinaryExpr) {
+ BinaryExpr bin = (BinaryExpr)s;
+ switch (bin.ResolvedOp) {
+ case BinaryExpr.ResolvedOpcode.MultiSetUnion:
+ return Bpl.Expr.Or(TrInMultiSet(tok, elmt, bin.E0, elmtType), TrInMultiSet(tok, elmt, bin.E1, elmtType));
+ case BinaryExpr.ResolvedOpcode.MultiSetIntersection:
+ return Bpl.Expr.And(TrInMultiSet(tok, elmt, bin.E0, elmtType), TrInMultiSet(tok, elmt, bin.E1, elmtType));
+ default:
+ break;
+ }
+ } else if (s is MultiSetDisplayExpr) {
+ MultiSetDisplayExpr disp = (MultiSetDisplayExpr)s;
+ Bpl.Expr disjunction = null;
+ foreach (Expression a in disp.Elements) {
+ Bpl.Expr disjunct = Bpl.Expr.Eq(elmt, TrExpr(a));
+ if (disjunction == null) {
+ disjunction = disjunct;
+ } else {
+ disjunction = Bpl.Expr.Or(disjunction, disjunct);
+ }
+ }
+ if (disjunction == null) {
+ return Bpl.Expr.False;
+ } else {
+ return disjunction;
+ }
+ }
+ return Bpl.Expr.Gt(Bpl.Expr.SelectTok(tok, TrExpr(s), BoxIfNecessary(tok, elmt, elmtType)), Bpl.Expr.Literal(0));
+ }
+
Bpl.QKeyValue TrAttributes(Attributes attrs) {
Bpl.QKeyValue kv = null;
while (attrs != null) {
@@ -5301,7 +5443,16 @@ namespace Microsoft.Dafny { SetSubset,
SetDisjoint,
SetChoose,
-
+
+ MultiSetEmpty,
+ MultiSetUnionOne,
+ MultiSetUnion,
+ MultiSetIntersection,
+ MultiSetDifference,
+ MultiSetEqual,
+ MultiSetSubset,
+ MultiSetDisjoint,
+
SeqLength,
SeqEmpty,
SeqBuild,
@@ -5387,6 +5538,47 @@ namespace Microsoft.Dafny { Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "Set#Choose", typeInstantiation, args);
+
+ case BuiltinFunction.MultiSetEmpty: {
+ Contract.Assert(args.Length == 0);
+ Contract.Assert(typeInstantiation != null);
+ Bpl.Type resultType = predef.MultiSetType(tok, typeInstantiation);
+ return Bpl.Expr.CoerceType(tok, FunctionCall(tok, "MultiSet#Empty", resultType, args), resultType);
+ }
+ case BuiltinFunction.MultiSetUnionOne:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "MultiSet#UnionOne", predef.MultiSetType(tok, typeInstantiation), args);
+ case BuiltinFunction.MultiSetUnion:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "MultiSet#Union", predef.MultiSetType(tok, typeInstantiation), args);
+ case BuiltinFunction.MultiSetIntersection:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "MultiSet#Intersection", predef.MultiSetType(tok, typeInstantiation), args);
+ case BuiltinFunction.MultiSetDifference:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "MultiSet#Difference", predef.MultiSetType(tok, typeInstantiation), args);
+ case BuiltinFunction.MultiSetEqual:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "MultiSet#Equal", Bpl.Type.Bool, args);
+ case BuiltinFunction.MultiSetSubset:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "MultiSet#Subset", Bpl.Type.Bool, args);
+ case BuiltinFunction.MultiSetDisjoint:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation == null);
+ return FunctionCall(tok, "MultiSet#Disjoint", Bpl.Type.Bool, args);
+ // avoiding this for now
+ /*case BuiltinFunction.SetChoose:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "Set#Choose", typeInstantiation, args);*/
+
case BuiltinFunction.SeqLength:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation == null);
@@ -6033,6 +6225,8 @@ namespace Microsoft.Dafny { if (newElements != e.Elements) {
if (expr is SetDisplayExpr) {
newExpr = new SetDisplayExpr(expr.tok, newElements);
+ } else if (expr is MultiSetDisplayExpr) {
+ newExpr = new MultiSetDisplayExpr(expr.tok, newElements);
} else {
newExpr = new SeqDisplayExpr(expr.tok, newElements);
}
|