Merge branch 'master' into fix-5647-tail-recursion-rust-fixup

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/AST/TypeDeclarations/NonNullTypeDecl.cs

@@ -35,7 +35,7 @@ private NonNullTypeDecl(ClassLikeDecl cl, List<TypeParameter> tps, BoundVar id)
   }
 
   public override List<Type> ParentTypes(List<Type> typeArgs, bool includeTypeBounds) {
-    List<Type> result = new List<Type>(base.ParentTypes(typeArgs, includeTypeBounds));
+    var result = new List<Type>(base.ParentTypes(typeArgs, includeTypeBounds));
 
     foreach (var rhsParentType in Class.ParentTypes(typeArgs, includeTypeBounds)) {
       var rhsParentUdt = (UserDefinedType)rhsParentType; // all parent types of .Class are expected to be possibly-null class types

Source/DafnyCore/AST/TypeDeclarations/TopLevelDeclWithMembers.cs

@@ -104,15 +104,19 @@ public void SetMembersBeforeResolution() {
     MembersBeforeResolution = Members.ToImmutableList();
   }
 
-  private List<Type> RawTraitsWithArgument(List<Type> typeArgs) {
+  public List<Type> RawTraitsWithArgument(List<Type> typeArgs) {
     Contract.Requires(typeArgs != null);
     Contract.Requires(typeArgs.Count == TypeArgs.Count);
     // Instantiate with the actual type arguments
     var subst = TypeParameter.SubstitutionMap(TypeArgs, typeArgs);
-    return ParentTraits.ConvertAll(traitType => {
+    var isReferenceType = this is ClassLikeDecl { IsReferenceTypeDecl: true };
+    var results = new List<Type>();
+    foreach (var traitType in ParentTraits) {
       var ty = (UserDefinedType)traitType.Subst(subst);
-      return (Type)UserDefinedType.CreateNullableTypeIfReferenceType(ty);
-    });
+      Contract.Assert(isReferenceType || !ty.IsRefType);
+      results.Add(UserDefinedType.CreateNullableTypeIfReferenceType(ty));
+    }
+    return results;
   }
 
   public override List<Type> ParentTypes(List<Type> typeArgs, bool includeTypeBounds) {

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -2443,7 +2443,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

@@ -2391,11 +2391,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());
@@ -2787,6 +2797,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/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Expression.cs

@@ -370,7 +370,7 @@ void EmitExpr(Expression e2, ConcreteSyntaxTree wr2, bool inLetExpr, ConcreteSyn
                 }
 
                 TrAssignSuchThat(new List<IVariable>(e.BoundVars).ConvertAll(bv => (IVariable)bv), e.RHSs[0],
-                  e.Constraint_Bounds, e.tok.line, w, inLetExprBody);
+                  e.Constraint_Bounds, w, inLetExprBody);
                 EmitReturnExpr(e.Body, e.Body.Type, true, w);
               }
             }

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.Statement.cs

@@ -158,7 +158,7 @@ protected void TrStmt(Statement stmt, ConcreteSyntaxTree wr, ConcreteSyntaxTree
               }
             } else {
               Contract.Assert(s.Bounds != null);
-              TrAssignSuchThat(lhss, s.Expr, s.Bounds, s.Tok.line, wr, false);
+              TrAssignSuchThat(lhss, s.Expr, s.Bounds, wr, false);
             }
 
             break;

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

@@ -3538,7 +3538,7 @@ private void IntroduceAndAssignBoundVars(ExistsExpr exists, ConcreteSyntaxTree w
         TrLocalVar(bv, false, wr);
       }
       var ivars = exists.BoundVars.ConvertAll(bv => (IVariable)bv);
-      TrAssignSuchThat(ivars, exists.Term, exists.Bounds, exists.tok.line, wr, false);
+      TrAssignSuchThat(ivars, exists.Term, exists.Bounds, wr, false);
     }
 
     private bool CanSequentializeForall(List<BoundVar> bvs, List<BoundedPool> bounds, Expression range, Expression lhs, Expression rhs) {
@@ -3665,7 +3665,7 @@ protected override bool VisitOneExpr(Expression expr, ref object st) {
       }
     }
 
-    private void TrAssignSuchThat(List<IVariable> lhss, Expression constraint, List<BoundedPool> bounds, int debuginfoLine, ConcreteSyntaxTree wr, bool inLetExprBody) {
+    private void TrAssignSuchThat(List<IVariable> lhss, Expression constraint, List<BoundedPool> bounds, ConcreteSyntaxTree wr, bool inLetExprBody) {
       Contract.Requires(lhss != null);
       Contract.Requires(constraint != null);
       Contract.Requires(bounds != null);
@@ -3741,7 +3741,7 @@ private void TrAssignSuchThat(List<IVariable> lhss, Expression constraint, List<
       copyInstrWriters.Pop();
 
       // Java compiler throws unreachable error when absurd statement is written after unbounded for-loop, so we don't write it then.
-      EmitAbsurd(string.Format("assign-such-that search produced no value (line {0})", debuginfoLine), wrOuter, needIterLimit);
+      EmitAbsurd("assign-such-that search produced no value", wrOuter, needIterLimit);
     }
 
     protected interface ILvalue {