From 2574ef6a0731e61b3a1328677f31c42357568914 Mon Sep 17 00:00:00 2001
From: Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com>
Date: Tue, 29 May 2012 11:41:31 -0700
Subject: Dafny: fixed minor map related issues

---
 Source/Dafny/Printer.cs  | 18 ++++++++++++++++++
 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;
-- 
cgit v1.2.3