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

…or (#5803)

Fixes #5802

### Description
Multiset iteration was implemented in the runtime but not imported to
the Dafny-to-Rust code generator. Moreover, it did not iterate elements
with multiplicity, which might be needed.
This PR adds support for multiset bounded pools so that multisets can be
used in quantifiers and comprehensions.

### How has this been tested?
A test in the runtime verifies the multiplicity, and I updated an
existing test to test the enumeration in quantifiers and comprehensions.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

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