Dafny: Added compilation of finite maps

3 files changed, 111 insertions, 0 deletions

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);