diff options
| author |  Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 11:41:31 -0700 |
|---|---|---|
| committer | Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com> | 2012-05-29 11:41:31 -0700 |
| commit | 2574ef6a0731e61b3a1328677f31c42357568914 (patch) | |
| tree | a3633849a9843398bcf21df09c5e8e58ab8e8eae | |
| parent | aa6921029400e5dfa4186e0eff420c46d9b68f1d (diff) | |
Dafny: fixed minor map related issues
| -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;
|