diff options
-rw-r--r-- | Source/Dafny/Printer.cs | 18 | ||||
-rw-r--r-- | Source/Dafny/Resolver.cs | 3 |
2 files changed, 18 insertions, 3 deletions
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs index 2c6fb96a..38ec17fc 100644 --- a/Source/Dafny/Printer.cs +++ b/Source/Dafny/Printer.cs @@ -881,6 +881,12 @@ namespace Microsoft.Dafny { PrintExpressionList(e.Elements);
wr.Write(e is SetDisplayExpr || e is MultiSetDisplayExpr ? "}" : "]");
+ } else if (expr is MapDisplayExpr) {
+ MapDisplayExpr e = (MapDisplayExpr)expr;
+ wr.Write("map");
+ wr.Write("{");
+ PrintExpressionPairList(e.Elements);
+ wr.Write("}");
} else if (expr is ExprDotName) {
var e = (ExprDotName)expr;
// determine if parens are needed
@@ -1259,6 +1265,18 @@ namespace Microsoft.Dafny { PrintExpression(e);
}
}
+ void PrintExpressionPairList(List<ExpressionPair> exprs) {
+ Contract.Requires(exprs != null);
+ string sep = "";
+ foreach (ExpressionPair p in exprs) {
+ Contract.Assert(p != null);
+ wr.Write(sep);
+ sep = ", ";
+ PrintExpression(p.A);
+ wr.Write(":=");
+ PrintExpression(p.B);
+ }
+ }
void PrintFrameExpressionList(List<FrameExpression/*!*/>/*!*/ fexprs) {
Contract.Requires(fexprs != null);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 9f3f474b..4402e5b1 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -4082,7 +4082,6 @@ namespace Microsoft.Dafny { } else if(operandType is MapType) {
return BinaryExpr.ResolvedOpcode.MapDisjoint;
} else {
- Contract.Assert(operandType is SetType);
return BinaryExpr.ResolvedOpcode.Disjoint;
}
case BinaryExpr.Opcode.Lt:
@@ -4161,7 +4160,6 @@ namespace Microsoft.Dafny { } else if (operandType is MapType) {
return BinaryExpr.ResolvedOpcode.InMap;
} else {
- Contract.Assert(operandType is SeqType);
return BinaryExpr.ResolvedOpcode.InSeq;
}
case BinaryExpr.Opcode.NotIn:
@@ -4172,7 +4170,6 @@ namespace Microsoft.Dafny { } else if (operandType is MapType) {
return BinaryExpr.ResolvedOpcode.NotInMap;
} else {
- Contract.Assert(operandType is SeqType);
return BinaryExpr.ResolvedOpcode.NotInSeq;
}
case BinaryExpr.Opcode.Div: return BinaryExpr.ResolvedOpcode.Div;
|