1 files changed, 37 insertions, 4 deletions
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 4868be10..cf1a8630 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -256,7 +256,7 @@ namespace Microsoft.Dafny {
       this.Arg = arg;
     }
   }
-
+  
   public class SetType : CollectionType {
     public SetType(Type arg) : base(arg) {
       Contract.Requires(arg != null);
@@ -269,6 +269,19 @@ namespace Microsoft.Dafny {
     }
   }
 
+  public class MultiSetType : CollectionType
+  {
+    public MultiSetType(Type arg) : base(arg) {
+      Contract.Requires(arg != null);
+    }
+    [Pure]
+    public override string ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      Contract.Assume(cce.IsPeerConsistent(Arg));
+      return "multiset<" + base.Arg + ">";
+    }
+  }
+
   public class SeqType : CollectionType {
     public SeqType(Type arg) : base(arg) {
       Contract.Requires(arg != null);
@@ -487,9 +500,9 @@ namespace Microsoft.Dafny {
 
   /// <summary>
   /// This proxy stands for either:
-  ///     int or set or seq
+  ///     int or set or multiset or seq
   /// if AllowSeq, or:
-  ///     int or set
+  ///     int or set or multiset
   /// if !AllowSeq.
   /// </summary>  
   public class OperationTypeProxy : RestrictedTypeProxy {
@@ -2062,7 +2075,7 @@ namespace Microsoft.Dafny {
       get { return Elements; }
     }
   }
-
+  
   public class SetDisplayExpr : DisplayExpression {
     public SetDisplayExpr(IToken tok, List<Expression/*!*/>/*!*/ elements)
       : base(tok, elements) {
@@ -2071,6 +2084,13 @@ namespace Microsoft.Dafny {
     }
   }
 
+  public class MultiSetDisplayExpr : DisplayExpression {
+    public MultiSetDisplayExpr(IToken tok, List<Expression/*!*/>/*!*/ elements) : base(tok, elements) {
+      Contract.Requires(tok != null);
+      Contract.Requires(cce.NonNullElements(elements));
+    }
+  }
+
   public class SeqDisplayExpr : DisplayExpression {
     public SeqDisplayExpr(IToken tok, List<Expression/*!*/>/*!*/ elements)
       : base(tok, elements) {
@@ -2378,6 +2398,19 @@ namespace Microsoft.Dafny {
       Union,
       Intersection,
       SetDifference,
+      // multi-sets
+      MultiSetEq,
+      MultiSetNeq,
+      MultiSubset,
+      MultiSuperset,
+      ProperMultiSubset,
+      ProperMultiSuperset,
+      MultiSetDisjoint,
+      InMultiSet,
+      NotInMultiSet,
+      MultiSetUnion,
+      MultiSetIntersection,
+      MultiSetDifference,
       // sequences
       SeqEq,
       SeqNeq,