Added compilation support for multisets and sequences from arrays.

2 files changed, 203 insertions, 11 deletions

diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index c03ac643..82de380d 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -132,11 +132,154 @@ namespace Dafny
       return default(T);

     }

   }

+  public class MultiSet<T>

+  {

+    Dictionary<T, int> dict;

+    public MultiSet() { }

+    MultiSet(Dictionary<T, int> d) {

+      dict = d;

+    }

+    public static MultiSet<T> Empty {

+      get {

+        return new MultiSet<T>(new Dictionary<T, int>(0));

+      }

+    }

+    public static MultiSet<T> FromElements(params T[] values) {

+      Dictionary<T, int> d = new Dictionary<T, int>(values.Length);

+      foreach (T t in values) {

+        var i = 0;

+        if (!d.TryGetValue(t, out i)) {

+          i = 0;

+        }

+        d[t] = i + 1;

+      }

+      return new MultiSet<T>(d);

+    }

+    public static MultiSet<T> FromCollection(ICollection<T> values) {

+      Dictionary<T, int> d = new Dictionary<T, int>();

+      foreach (T t in values) {

+        var i = 0;

+        if (!d.TryGetValue(t, out i)) {

+          i = 0;

+        }

+        d[t] = i + 1;

+      }

+      return new MultiSet<T>(d);

+    }

+    public static MultiSet<T> FromSeq(Sequence<T> values) {

+      Dictionary<T, int> d = new Dictionary<T, int>();

+      foreach (T t in values.Elements) {

+        var i = 0;

+        if (!d.TryGetValue(t, out i)) {

+          i = 0;

+        }

+        d[t] = i + 1;

+      }

+      return new MultiSet<T>(d);

+    }

+    public static MultiSet<T> FromSet(Set<T> values) {

+      Dictionary<T, int> d = new Dictionary<T, int>();

+      foreach (T t in values.Elements) {

+        d[t] = 1;

+      }

+      return new MultiSet<T>(d);

+    }

+

+    public bool Equals(MultiSet<T> other) {

+      return other.IsSubsetOf(this) && this.IsSubsetOf(other);

+    }

+    public override bool Equals(object other) {

+      return other is MultiSet<T> && Equals((MultiSet<T>)other);

+    }

+    public override int GetHashCode() {

+      return dict.GetHashCode();

+    }

+    public bool IsProperSubsetOf(MultiSet<T> other) {

+      return !Equals(other) && IsSubsetOf(other);

+    }

+    public bool IsSubsetOf(MultiSet<T> other) {

+      foreach (T t in dict.Keys) {

+        if (!other.dict.ContainsKey(t) || other.dict[t] < dict[t])

+          return false;

+      }

+      return true;

+    }

+    public bool IsSupersetOf(MultiSet<T> other) {

+      return other.IsSubsetOf(this);

+    }

+    public bool IsProperSupersetOf(MultiSet<T> other) {

+      return other.IsProperSubsetOf(this);

+    }

+    public bool IsDisjointFrom(MultiSet<T> other) {

+      foreach (T t in dict.Keys) {

+        if (other.dict.ContainsKey(t))

+          return false;

+      }

+      foreach (T t in other.dict.Keys) {

+        if (dict.ContainsKey(t))

+          return false;

+      }

+      return true;

+    }

+    public bool Contains(T t) {

+      return dict.ContainsKey(t);

+    }

+    public MultiSet<T> Union(MultiSet<T> other) {

+      if (dict.Count == 0)

+        return other;

+      else if (other.dict.Count == 0)

+        return this;

+      var r = new Dictionary<T, int>();

+      foreach (T t in dict.Keys) {

+        var i = 0;

+        if (!r.TryGetValue(t, out i)) {

+          i = 0;

+        }

+        r[t] = i + dict[t];

+      }

+      foreach (T t in other.dict.Keys) {

+        var i = 0;

+        if (!r.TryGetValue(t, out i)) {

+          i = 0;

+        }

+        r[t] = i + other.dict[t];

+      }

+      return new MultiSet<T>(r);

+    }

+    public MultiSet<T> Intersect(MultiSet<T> other) {

+      if (dict.Count == 0)

+        return this;

+      else if (other.dict.Count == 0)

+        return other;

+      var r = new Dictionary<T, int>();

+      foreach (T t in dict.Keys) {

+        if (other.dict.ContainsKey(t)) {

+          r.Add(t, other.dict[t] < dict[t] ? other.dict[t] : dict[t]);

+        }

+      }

+      return new MultiSet<T>(r);

+    }

+    public MultiSet<T> Difference(MultiSet<T> other) { // \result == this - other

+      if (dict.Count == 0)

+        return this;

+      else if (other.dict.Count == 0)

+        return this;

+      var r = new Dictionary<T, int>();

+      foreach (T t in dict.Keys) {

+        if (!other.dict.ContainsKey(t)) {

+          r.Add(t, dict[t]);

+        } else if (other.dict[t] < dict[t]) {

+          r.Add(t, dict[t] - other.dict[t]);

+        }

+      }

+      return new MultiSet<T>(r);

+    }

+  }

   public class Sequence<T>

   {

     T[] elmts;

     public Sequence() { }

-    Sequence(T[] ee) {

+    public Sequence(T[] ee) {

       elmts = ee;

     }

     public static Sequence<T> Empty {

@@ -303,5 +446,8 @@ namespace Dafny
         return c.IsZero ? c : BigInteger.Subtract(bp, c);

       }

     }

+    public static Sequence<T> SeqFromArray<T>(T[] array) {

+      return new Sequence<T>(array);

+    }

   }

 }

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index d61d653d..6fa9440a 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -483,8 +483,9 @@ namespace Microsoft.Dafny {
     }

 

     // ----- Type ---------------------------------------------------------------------------------

-    

+

     readonly string DafnySetClass = "Dafny.Set";

+    readonly string DafnyMultiSetClass = "Dafny.MultiSet";

     readonly string DafnySeqClass = "Dafny.Sequence";

     

     string TypeName(Type type)

@@ -541,6 +542,12 @@ namespace Microsoft.Dafny {
           Error("compilation of seq<object> is not supported; consider introducing a ghost");

         }

         return DafnySeqClass + "<" + TypeName(argType) + ">";

+      } else if (type is MultiSetType) {

+        Type argType = ((MultiSetType)type).Arg;

+        if (argType is ObjectType) {

+          Error("compilation of seq<object> is not supported; consider introducing a ghost");

+        }

+        return DafnyMultiSetClass + "<" + TypeName(argType) + ">";

       } else {

         Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

       }

@@ -607,6 +614,8 @@ namespace Microsoft.Dafny {
         return "default(@" + udt.Name + ")";

       } else if (type is SetType) {

         return DafnySetClass + "<" + TypeName(((SetType)type).Arg) + ">.Empty";

+      } else if (type is MultiSetType) {

+        return DafnyMultiSetClass + "<" + TypeName(((MultiSetType)type).Arg) + ">.Empty";

       } else if (type is SeqType) {

         return DafnySeqClass + "<" + TypeName(((SeqType)type).Arg) + ">.Empty";

       } else {

@@ -1186,12 +1195,18 @@ namespace Microsoft.Dafny {
       } else if (expr is IdentifierExpr) {

         IdentifierExpr e = (IdentifierExpr)expr;

         wr.Write("@" + e.Var.Name);

-      

+

       } else if (expr is SetDisplayExpr) {

         SetDisplayExpr e = (SetDisplayExpr)expr;

         Type elType = cce.NonNull((SetType)e.Type).Arg;

         wr.Write("{0}<{1}>.FromElements", DafnySetClass, TypeName(elType));

         TrExprList(e.Elements);

+

+      } else if (expr is MultiSetDisplayExpr) {

+        MultiSetDisplayExpr e = (MultiSetDisplayExpr)expr;

+        Type elType = cce.NonNull((MultiSetType)e.Type).Arg;

+        wr.Write("{0}<{1}>.FromElements", DafnyMultiSetClass, TypeName(elType));

+        TrExprList(e.Elements);

         

       } else if (expr is SeqDisplayExpr) {

         SeqDisplayExpr e = (SeqDisplayExpr)expr;

@@ -1214,18 +1229,29 @@ namespace Microsoft.Dafny {
         

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

-        TrParenExpr(e.Seq);

         Contract.Assert(e.Seq.Type != null);

         if (e.Seq.Type.IsArrayType) {

-          Contract.Assert(e.SelectOne);

-          Contract.Assert(e.E0 != null && e.E1 == null);

-          wr.Write("[(int)");

-          TrParenExpr(e.E0);

-          wr.Write("]");

+          if (e.SelectOne) {

+            Contract.Assert(e.E0 != null && e.E1 == null);

+            TrParenExpr(e.Seq);

+            wr.Write("[(int)");

+            TrParenExpr(e.E0);

+            wr.Write("]");

+          } else {

+            TrParenExpr("Dafny.Helpers.SeqFromArray", e.Seq);

+            if (e.E1 != null) {

+              TrParenExpr(".Take", e.E1);

+            }

+            if (e.E0 != null) {

+              TrParenExpr(".Drop", e.E0);

+            }

+          }

         } else if (e.SelectOne) {

           Contract.Assert(e.E0 != null && e.E1 == null);

+          TrParenExpr(e.Seq);

           TrParenExpr(".Select", e.E0);

         } else {

+          TrParenExpr(e.Seq);

           if (e.E1 != null) {

             TrParenExpr(".Take", e.E1);

           }

@@ -1233,7 +1259,16 @@ namespace Microsoft.Dafny {
             TrParenExpr(".Drop", e.E0);

           }

         }

-      

+      } else if (expr is MultiSetFormingExpr) {

+        MultiSetFormingExpr e = (MultiSetFormingExpr)expr;

+        wr.Write("{0}<{1}>", DafnyMultiSetClass, TypeName(((CollectionType)e.E.Type).Arg));

+        if (e.E.Type is SeqType) {

+          TrParenExpr(".FromSeq", e.E);

+        } else if (e.E.Type is SetType) {

+          TrParenExpr(".FromSet", e.E);

+        } else {

+          Contract.Assert(false); throw new cce.UnreachableException();

+        }

       } else if (expr is MultiSelectExpr) {

         MultiSelectExpr e = (MultiSelectExpr)expr;

         TrParenExpr(e.Array);

@@ -1389,29 +1424,37 @@ namespace Microsoft.Dafny {
             wr.Write(")");

             break;

           case BinaryExpr.ResolvedOpcode.SetEq:

+          case BinaryExpr.ResolvedOpcode.MultiSetEq:

           case BinaryExpr.ResolvedOpcode.SeqEq:

             callString = "Equals";  break;

           case BinaryExpr.ResolvedOpcode.SetNeq:

+          case BinaryExpr.ResolvedOpcode.MultiSetNeq:

           case BinaryExpr.ResolvedOpcode.SeqNeq:

             preOpString = "!";  callString = "Equals";  break;

-

           case BinaryExpr.ResolvedOpcode.ProperSubset:

+          case BinaryExpr.ResolvedOpcode.ProperMultiSubset:

             callString = "IsProperSubsetOf";  break;

           case BinaryExpr.ResolvedOpcode.Subset:

+          case BinaryExpr.ResolvedOpcode.MultiSubset:

             callString = "IsSubsetOf";  break;

           case BinaryExpr.ResolvedOpcode.Superset:

+          case BinaryExpr.ResolvedOpcode.MultiSuperset:

             callString = "IsSupersetOf";  break;

           case BinaryExpr.ResolvedOpcode.ProperSuperset:

+          case BinaryExpr.ResolvedOpcode.ProperMultiSuperset:

             callString = "IsProperSupersetOf";  break;

           case BinaryExpr.ResolvedOpcode.Disjoint:

+          case BinaryExpr.ResolvedOpcode.MultiSetDisjoint:

             callString = "IsDisjointFrom";  break;

           case BinaryExpr.ResolvedOpcode.InSet:

+          case BinaryExpr.ResolvedOpcode.InMultiSet:

             TrParenExpr(e.E1);

             wr.Write(".Contains(");

             TrExpr(e.E0);

             wr.Write(")");

             break;

           case BinaryExpr.ResolvedOpcode.NotInSet:

+          case BinaryExpr.ResolvedOpcode.NotInMultiSet:

             wr.Write("!");

             TrParenExpr(e.E1);

             wr.Write(".Contains(");

@@ -1419,10 +1462,13 @@ namespace Microsoft.Dafny {
             wr.Write(")");

             break;

           case BinaryExpr.ResolvedOpcode.Union:

+          case BinaryExpr.ResolvedOpcode.MultiSetUnion:

             callString = "Union";  break;

           case BinaryExpr.ResolvedOpcode.Intersection:

+          case BinaryExpr.ResolvedOpcode.MultiSetIntersection:

             callString = "Intersect";  break;

           case BinaryExpr.ResolvedOpcode.SetDifference:

+          case BinaryExpr.ResolvedOpcode.MultiSetDifference:

             callString = "Difference";  break;

 

           case BinaryExpr.ResolvedOpcode.ProperPrefix: