Fix: Support for enumerating datatypes in the Rust backend

Makefile

@@ -100,7 +100,7 @@ update-go-module:
 update-runtime-dafny:
 	(cd "${DIR}"; cd Source/DafnyRuntime/DafnyRuntimeDafny; make update-go)
 
-pr-nogeneration: format-dfy format update-runtime-dafny update-cs-module update-rs-module update-go-module
+pr-nogeneration: format-dfy format update-runtime-dafny update-cs-module update-rs-module update-go-module update-rs-module
 
 update-standard-libraries:
 	(cd "${DIR}"; cd Source/DafnyStandardLibraries; make update-binary)

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -2439,7 +2439,21 @@ protected override void EmitSeqBoundedPool(Expression of, bool includeDuplicates
     }
 
     protected override void EmitDatatypeBoundedPool(IVariable bv, string propertySuffix, bool inLetExprBody, ConcreteSyntaxTree wr, ConcreteSyntaxTree wStmts) {
-      AddUnsupported("<i>EmitDatatypeBoundedPool</i>");
+      if (GetExprConverter(wr, wStmts, out var exprBuilder, out var convert)) {
+        if (bv.Type.IsDatatype && bv.Type.AsDatatype is { } datatypeDecl) {
+
+          var signature = Sequence<_IFormal>.FromArray(new _IFormal[] { });
+          var c = exprBuilder.Builder.Call(signature);
+          c.SetName((DAST.CallName)DAST.CallName.create_CallName(Sequence<Rune>.UnicodeFromString("_AllSingletonConstructors"),
+            Option<_IType>.create_None(), Option<_IFormal>.create_None(), false, signature));
+          var wrc = new BuilderSyntaxTree<ExprContainer>(c, this);
+          EmitTypeName_Companion(bv.Type, wrc, wr, bv.Tok, null);
+        } else {
+          throw new InvalidOperationException("Datatype Bounded pool on non-datatype value");
+        }
+      } else {
+        throw new InvalidOperationException();
+      }
     }
 
     protected override void CreateIIFE(string bvName, Type bvType, IToken bvTok, Type bodyType, IToken bodyTok,

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

@@ -2389,11 +2389,21 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
       var datatypeName := escapeName(c.name);
       var ctors: seq<R.EnumCase> := [];
       var variances := Std.Collections.Seq.Map((typeParamDecl: TypeArgDecl) => typeParamDecl.variance, c.typeParams);
+      var singletonConstructors := [];
       var usedTypeParams: set<string> := {};
       for i := 0 to |c.ctors| {
         var ctor := c.ctors[i];
         var ctorArgs: seq<R.Field> := [];
         var isNumeric := false;
+        if |ctor.args| == 0 {
+          var instantiation := R.StructBuild(R.Identifier(datatypeName).FSel(escapeName(ctor.name)), []);
+          if IsRcWrapped(c.attributes) {
+            instantiation := R.RcNew(instantiation);
+          }
+          singletonConstructors := singletonConstructors + [
+            instantiation
+          ];
+        }
         for j := 0 to |ctor.args| {
           var dtor := ctor.args[j];
           var formalType := GenType(dtor.formal.typ, GenTypeContext.default());
@@ -2785,6 +2795,31 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
         ];
       }
 
+      if |singletonConstructors| == |c.ctors| {
+        var datatypeType := R.TypeApp(R.TIdentifier(datatypeName), rTypeParams);
+        var instantiationType :=
+          if IsRcWrapped(c.attributes) then
+            R.Rc(datatypeType)
+          else
+            datatypeType;
+        s := s + [
+          R.ImplDecl(
+            R.Impl(
+              rTypeParamsDecls,
+              datatypeType,
+              "",
+              [R.FnDecl(
+                 R.PUB,
+                 R.Fn(
+                   "_AllSingletonConstructors", [],
+                   [],
+                   Some(R.dafny_runtime.MSel("SequenceIter").AsType().Apply([instantiationType])),
+                   "",
+                   Some(R.dafny_runtime.MSel("seq!").AsExpr().Apply(singletonConstructors).Sel("iter").Apply([]))
+                 )
+               )]))];
+      }
+
       // Implementation of Eq when c supports equality
       if cIsEq {
         s := s + [R.ImplDecl(

Source/DafnyRuntime/DafnyRuntimeRust/src/system/mod.rs

@@ -129,6 +129,12 @@ pub mod _System {
     }
   }
 
+  impl Tuple0 {
+    pub fn _AllSingletonConstructors() -> crate::SequenceIter<::std::rc::Rc<Tuple0>> {
+      crate::seq![::std::rc::Rc::new(Tuple0::_T0 {})].iter()
+    }
+  }
+
   impl Eq
     for Tuple0 {}
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5643.dfy

@@ -0,0 +1,13 @@
+// RUN: %testDafnyForEachCompiler "%s"
+
+datatype D = A | B
+
+const c := set d: D | true :: d
+
+datatype {:rust_rc false} E = F | G
+
+const h := set e: E | true :: e
+
+method Main() {
+  print |c|, |h|, "\n";
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5643.dfy.expect

@@ -0,0 +1 @@
+22

docs/dev/news/5643.fix

@@ -0,0 +1 @@
+Support for enumerating datatypes in the Rust backend