Fix: Ability to enumerate multisets in the Dafny-to-Rust code generator

Source/DafnyCore/Backends/Dafny/AST.dfy

@@ -317,6 +317,7 @@ module {:extern "DAST"} DAST {
     SetBoundedPool(of: Expression) |
     MapBoundedPool(of: Expression) |
     SeqBoundedPool(of: Expression, includeDuplicates: bool) |
+    MultisetBoundedPool(of: Expression, includeDuplicates: bool) |
     ExactBoundedPool(of: Expression) |
     IntRange(elemType: Type, lo: Expression, hi: Expression, up: bool) |
     UnboundedIntRange(start: Expression, up: bool) |

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -2428,7 +2428,13 @@ protected override void EmitSetBoundedPool(Expression of, string propertySuffix,
     }
 
     protected override void EmitMultiSetBoundedPool(Expression of, bool includeDuplicates, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
-      AddUnsupported("<i>EmitMultiSetBoundedPool</i>");
+      if (GetExprConverter(wr, wStmts, out var exprBuilder, out var convert)) {
+        exprBuilder.Builder.AddExpr((DAST.Expression)DAST.Expression.create_MultisetBoundedPool(
+          convert(of), includeDuplicates
+        ));
+      } else {
+        throw new InvalidOperationException();
+      }
     }
 
     protected override void EmitSubSetBoundedPool(Expression of, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {

Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy

@@ -1,8 +1,8 @@
 include "../Dafny/AST.dfy"
-  // Dafny to Rust compilation tenets:
-  // - The Compiled Dafny AST should be minimal
-  // - The generated code should look idiomatic and close to the original Dafny file if possible
 
+// Dafny to Rust compilation tenets:
+// - The Compiled Dafny AST should be minimal
+// - The generated code should look idiomatic and close to the original Dafny file if possible
 module {:extern "DCOMP"} DafnyToRustCompiler {
   import opened DafnyToRustCompilerDefinitions
   import FactorPathsOptimization
@@ -3609,6 +3609,16 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           readIdents := recIdents;
           return;
         }
+        case MultisetBoundedPool(of, includeDuplicates) => {
+          var exprGen, _, recIdents := GenExpr(of, selfIdent, env, OwnershipBorrowed);
+          r := exprGen.Sel("iter").Apply0();
+          if !includeDuplicates {
+            r := R.dafny_runtime.MSel("itertools").MSel("Itertools").AsExpr().FSel("unique").Apply1(r);
+          }
+          r, resultingOwnership := FromOwned(r, expectedOwnership);
+          readIdents := recIdents;
+          return;
+        }
         case MapBoundedPool(of) => {
           var exprGen, _, recIdents := GenExpr(of, selfIdent, env, OwnershipBorrowed);
           r := exprGen.Sel("keys").Apply0().Sel("iter").Apply0();
@@ -3671,7 +3681,11 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           // Integer collections are owned because they are computed number by number.
           // Sequence bounded pools are also owned
           var extraAttributes := [];
-          if collection.IntRange? || collection.UnboundedIntRange? || collection.SeqBoundedPool? || collection.ExactBoundedPool? {
+          if collection.IntRange?
+             || collection.UnboundedIntRange?
+             || collection.SeqBoundedPool?
+             || collection.ExactBoundedPool?
+             || collection.MultisetBoundedPool? {
             extraAttributes := [AttributeOwned];
           }
 

Source/DafnyCore/GeneratedFromDafny/DAST.cs

@@ -5969,6 +5969,7 @@ public interface _IExpression {
     bool is_SetBoundedPool { get; }
     bool is_MapBoundedPool { get; }
     bool is_SeqBoundedPool { get; }
+    bool is_MultisetBoundedPool { get; }
     bool is_ExactBoundedPool { get; }
     bool is_IntRange { get; }
     bool is_UnboundedIntRange { get; }
@@ -6194,6 +6195,9 @@ public static _IExpression create_MapBoundedPool(DAST._IExpression of) {
     public static _IExpression create_SeqBoundedPool(DAST._IExpression of, bool includeDuplicates) {
       return new Expression_SeqBoundedPool(of, includeDuplicates);
     }
+    public static _IExpression create_MultisetBoundedPool(DAST._IExpression of, bool includeDuplicates) {
+      return new Expression_MultisetBoundedPool(of, includeDuplicates);
+    }
     public static _IExpression create_ExactBoundedPool(DAST._IExpression of) {
       return new Expression_ExactBoundedPool(of);
     }
@@ -6252,6 +6256,7 @@ public static _IExpression create_Quantifier(DAST._IType elemType, DAST._IExpres
     public bool is_SetBoundedPool { get { return this is Expression_SetBoundedPool; } }
     public bool is_MapBoundedPool { get { return this is Expression_MapBoundedPool; } }
     public bool is_SeqBoundedPool { get { return this is Expression_SeqBoundedPool; } }
+    public bool is_MultisetBoundedPool { get { return this is Expression_MultisetBoundedPool; } }
     public bool is_ExactBoundedPool { get { return this is Expression_ExactBoundedPool; } }
     public bool is_IntRange { get { return this is Expression_IntRange; } }
     public bool is_UnboundedIntRange { get { return this is Expression_UnboundedIntRange; } }
@@ -6669,13 +6674,15 @@ public DAST._IExpression dtor_of {
         if (d is Expression_SetBoundedPool) { return ((Expression_SetBoundedPool)d)._of; }
         if (d is Expression_MapBoundedPool) { return ((Expression_MapBoundedPool)d)._of; }
         if (d is Expression_SeqBoundedPool) { return ((Expression_SeqBoundedPool)d)._of; }
+        if (d is Expression_MultisetBoundedPool) { return ((Expression_MultisetBoundedPool)d)._of; }
         return ((Expression_ExactBoundedPool)d)._of;
       }
     }
     public bool dtor_includeDuplicates {
       get {
         var d = this;
-        return ((Expression_SeqBoundedPool)d)._includeDuplicates;
+        if (d is Expression_SeqBoundedPool) { return ((Expression_SeqBoundedPool)d)._includeDuplicates; }
+        return ((Expression_MultisetBoundedPool)d)._includeDuplicates;
       }
     }
     public DAST._IExpression dtor_lo {
@@ -8253,6 +8260,38 @@ public override string ToString() {
       return s;
     }
   }
+  public class Expression_MultisetBoundedPool : Expression {
+    public readonly DAST._IExpression _of;
+    public readonly bool _includeDuplicates;
+    public Expression_MultisetBoundedPool(DAST._IExpression of, bool includeDuplicates) : base() {
+      this._of = of;
+      this._includeDuplicates = includeDuplicates;
+    }
+    public override _IExpression DowncastClone() {
+      if (this is _IExpression dt) { return dt; }
+      return new Expression_MultisetBoundedPool(_of, _includeDuplicates);
+    }
+    public override bool Equals(object other) {
+      var oth = other as DAST.Expression_MultisetBoundedPool;
+      return oth != null && object.Equals(this._of, oth._of) && this._includeDuplicates == oth._includeDuplicates;
+    }
+    public override int GetHashCode() {
+      ulong hash = 5381;
+      hash = ((hash << 5) + hash) + 46;
+      hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._of));
+      hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._includeDuplicates));
+      return (int) hash;
+    }
+    public override string ToString() {
+      string s = "DAST.Expression.MultisetBoundedPool";
+      s += "(";
+      s += Dafny.Helpers.ToString(this._of);
+      s += ", ";
+      s += Dafny.Helpers.ToString(this._includeDuplicates);
+      s += ")";
+      return s;
+    }
+  }
   public class Expression_ExactBoundedPool : Expression {
     public readonly DAST._IExpression _of;
     public Expression_ExactBoundedPool(DAST._IExpression of) : base() {
@@ -8268,7 +8307,7 @@ public override bool Equals(object other) {
     }
     public override int GetHashCode() {
       ulong hash = 5381;
-      hash = ((hash << 5) + hash) + 46;
+      hash = ((hash << 5) + hash) + 47;
       hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._of));
       return (int) hash;
     }
@@ -8301,7 +8340,7 @@ public override bool Equals(object other) {
     }
     public override int GetHashCode() {
       ulong hash = 5381;
-      hash = ((hash << 5) + hash) + 47;
+      hash = ((hash << 5) + hash) + 48;
       hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._elemType));
       hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._lo));
       hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._hi));
@@ -8339,7 +8378,7 @@ public override bool Equals(object other) {
     }
     public override int GetHashCode() {
       ulong hash = 5381;
-      hash = ((hash << 5) + hash) + 48;
+      hash = ((hash << 5) + hash) + 49;
       hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._start));
       hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._up));
       return (int) hash;
@@ -8375,7 +8414,7 @@ public override bool Equals(object other) {
     }
     public override int GetHashCode() {
       ulong hash = 5381;
-      hash = ((hash << 5) + hash) + 49;
+      hash = ((hash << 5) + hash) + 50;
       hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._elemType));
       hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._collection));
       hash = ((hash << 5) + hash) + ((ulong)Dafny.Helpers.GetHashCode(this._is__forall));