From aa6921029400e5dfa4186e0eff420c46d9b68f1d Mon Sep 17 00:00:00 2001
From: Unknown <t-jasonk@Z3507288.redmond.corp.microsoft.com>
Date: Fri, 25 May 2012 14:13:09 -0700
Subject: Dafny: Added compilation of finite maps

---
 Binaries/DafnyRuntime.cs | 69 ++++++++++++++++++++++++++++++++++++++++++++++++
 Source/Dafny/Compiler.cs | 39 +++++++++++++++++++++++++++
 Source/Dafny/Resolver.cs |  3 +++
 3 files changed, 111 insertions(+)

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index 2f8d2764..67669245 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -275,6 +275,75 @@ namespace Dafny
       return new MultiSet<T>(r);
     }
   }
+
+  public class Map<U, V>
+  {
+    Dictionary<U, V> dict;
+    public Map() { }
+    Map(Dictionary<U, V> d) {
+      dict = d;
+    }
+    public static Map<U, V> Empty {
+      get {
+        return new Map<U, V>(new Dictionary<U,V>());
+      }
+    }
+    public static Map<U, V> FromElements(params Pair<U,V>[] values) {
+      Dictionary<U, V> d = new Dictionary<U, V>(values.Length);
+      foreach (Pair<U,V> p in values) {
+        d[p.Car] = p.Cdr;
+      }
+      return new Map<U, V>(d);
+    }
+    public bool Equals(Map<U, V> other) {
+      foreach (U u in dict.Keys) {
+        V v1, v2;
+        if (!dict.TryGetValue(u, out v1)) {
+          return false; // this shouldn't happen
+        }
+        if (!other.dict.TryGetValue(u, out v2)) {
+          return false; // other dictionary does not contain this element
+        }
+        if (!v1.Equals(v2)) {
+          return false;
+        }
+      }
+      foreach (U u in other.dict.Keys) {
+        if (!dict.ContainsKey(u)) {
+          return false; // this shouldn't happen
+        }
+      }
+      return true;
+    }
+    public override bool Equals(object other) {
+      return other is Map<U, V> && Equals((Map<U, V>)other);
+    }
+    public override int GetHashCode() {
+      return dict.GetHashCode();
+    }
+    public bool IsDisjointFrom(Map<U, V> other) {
+      foreach (U u in dict.Keys) {
+        if (other.dict.ContainsKey(u))
+          return false;
+      }
+      foreach (U u in other.dict.Keys) {
+        if (dict.ContainsKey(u))
+          return false;
+      }
+      return true;
+    }
+    public bool Contains(U u) {
+      return dict.ContainsKey(u);
+    }
+    public V Select(U index) {
+      return dict[index];
+    }
+    public Map<U, V> Update(U index, V val) {
+      Dictionary<U, V> d = new Dictionary<U, V>(dict);
+      d[index] = val;
+      return new Map<U, V>(d);
+    }
+  }
   public class Sequence<T>
   {
     T[] elmts;
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 138cf635..232224b0 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -685,6 +685,7 @@ namespace Microsoft.Dafny {
     readonly string DafnySetClass = "Dafny.Set";
     readonly string DafnyMultiSetClass = "Dafny.MultiSet";
     readonly string DafnySeqClass = "Dafny.Sequence";
+    readonly string DafnyMapClass = "Dafny.Map";
 
     string TypeName(Type type)
     {
@@ -746,6 +747,13 @@ namespace Microsoft.Dafny {
           Error("compilation of seq<object> is not supported; consider introducing a ghost");
         }
         return DafnyMultiSetClass + "<" + TypeName(argType) + ">";
+      } else if (type is MapType) {
+        Type domType = ((MapType)type).Domain;
+        Type ranType = ((MapType)type).Range;
+        if (domType is ObjectType || ranType is ObjectType) {
+          Error("compilation of map<object, _> or map<_, object> is not supported; consider introducing a ghost");
+        }
+        return DafnyMapClass + "<" + TypeName(domType) + "," + TypeName(ranType) + ">";
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type
       }
@@ -816,6 +824,8 @@ namespace Microsoft.Dafny {
         return DafnyMultiSetClass + "<" + TypeName(((MultiSetType)type).Arg) + ">.Empty";
       } else if (type is SeqType) {
         return DafnySeqClass + "<" + TypeName(((SeqType)type).Arg) + ">.Empty";
+      } else if (type is MapType) {
+        return TypeName(type)+".Empty";
       } else {
         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type
       }
@@ -1530,6 +1540,25 @@ namespace Microsoft.Dafny {
       }
       wr.Write(")");
     }
+    void TrExprPairList(List<ExpressionPair/*!*/>/*!*/ exprs) {
+      Contract.Requires(cce.NonNullElements(exprs));
+      wr.Write("(");
+      string sep = "";
+      foreach (ExpressionPair p in exprs) {
+        wr.Write(sep);
+        wr.Write("new Dafny.Pair<");
+        wr.Write(TypeName(p.A.Type));
+        wr.Write(",");
+        wr.Write(TypeName(p.B.Type));
+        wr.Write(">(");
+        TrExpr(p.A);
+        wr.Write(",");
+        TrExpr(p.B);
+        wr.Write(")");
+        sep = ", ";
+      }
+      wr.Write(")");
+    }
 
     /// <summary>
     /// Before calling TrExpr(expr), the caller must have spilled the let variables declared in "expr".
@@ -1579,6 +1608,11 @@ namespace Microsoft.Dafny {
         wr.Write("{0}<{1}>.FromElements", DafnySeqClass, TypeName(elType));
         TrExprList(e.Elements);
 
+      } else if (expr is MapDisplayExpr) {
+        MapDisplayExpr e = (MapDisplayExpr)expr;
+        wr.Write("{0}.FromElements", TypeName(e.Type));
+        TrExprPairList(e.Elements);
+
       } else if (expr is FieldSelectExpr) {
         FieldSelectExpr e = (FieldSelectExpr)expr;
         SpecialField sf = e.Field as SpecialField;
@@ -1829,10 +1863,12 @@ namespace Microsoft.Dafny {
           case BinaryExpr.ResolvedOpcode.SetEq:
           case BinaryExpr.ResolvedOpcode.MultiSetEq:
           case BinaryExpr.ResolvedOpcode.SeqEq:
+          case BinaryExpr.ResolvedOpcode.MapEq:
             callString = "Equals";  break;
           case BinaryExpr.ResolvedOpcode.SetNeq:
           case BinaryExpr.ResolvedOpcode.MultiSetNeq:
           case BinaryExpr.ResolvedOpcode.SeqNeq:
+          case BinaryExpr.ResolvedOpcode.MapNeq:
             preOpString = "!";  callString = "Equals";  break;
           case BinaryExpr.ResolvedOpcode.ProperSubset:
           case BinaryExpr.ResolvedOpcode.ProperMultiSubset:
@@ -1848,9 +1884,11 @@ namespace Microsoft.Dafny {
             callString = "IsProperSupersetOf";  break;
           case BinaryExpr.ResolvedOpcode.Disjoint:
           case BinaryExpr.ResolvedOpcode.MultiSetDisjoint:
+          case BinaryExpr.ResolvedOpcode.MapDisjoint:
             callString = "IsDisjointFrom";  break;
           case BinaryExpr.ResolvedOpcode.InSet:
           case BinaryExpr.ResolvedOpcode.InMultiSet:
+          case BinaryExpr.ResolvedOpcode.InMap:
             TrParenExpr(e.E1);
             wr.Write(".Contains(");
             TrExpr(e.E0);
@@ -1858,6 +1896,7 @@ namespace Microsoft.Dafny {
             break;
           case BinaryExpr.ResolvedOpcode.NotInSet:
           case BinaryExpr.ResolvedOpcode.NotInMultiSet:
+          case BinaryExpr.ResolvedOpcode.NotInMap:
             wr.Write("!");
             TrParenExpr(e.E1);
             wr.Write(".Contains(");
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 6688a0a4..9f3f474b 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -4205,6 +4205,9 @@ namespace Microsoft.Dafny {
       } else if (expr is DisplayExpression) {
         DisplayExpression e = (DisplayExpression)expr;
         return e.Elements.Exists(ee => UsesSpecFeatures(ee));
+      } else if (expr is MapDisplayExpr) {
+        MapDisplayExpr e = (MapDisplayExpr)expr;
+        return e.Elements.Exists(p => UsesSpecFeatures(p.A) || UsesSpecFeatures(p.B));
       } else if (expr is FieldSelectExpr) {
         FieldSelectExpr e = (FieldSelectExpr)expr;
         return cce.NonNull(e.Field).IsGhost || UsesSpecFeatures(e.Obj);
-- 
cgit v1.2.3