Fixed build and merge

dafny-lang · Jan 24, 2025 · e6c9ec2 · e6c9ec2
1 parent 50ae443
commit e6c9ec2
Show file tree

Hide file tree

Showing 5 changed files with 1,216 additions and 1,087 deletions.
diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy
@@ -960,6 +960,7 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
     }
   } */
   function DowncastImplFor(
+    rcNew: R.Expr -> R.Expr,
     rTypeParamsDecls: seq<R.TypeParamDecl>,
     datatypeType: R.Type
   ): Option<R.ModDecl> {
@@ -970,7 +971,7 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions {
       R.self.Sel("downcast_ref").ApplyType([datatypeTypeRaw]).Apply0().Sel("is_some").Apply0();
     var asBody :=
       R.self.Sel("downcast_ref").ApplyType([datatypeTypeRaw]).Apply0().Sel("unwrap").Apply0().Sel("clone").Apply0();
-    var asBody := if isRc then R.RcNew(asBody) else asBody;
+    var asBody := if isRc then rcNew(asBody) else asBody;
     Some(
       R.ImplDecl(
         R.ImplFor(

diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust.dfy
@@ -1253,14 +1253,14 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
              implBody
            ))];
       if |c.superTraitTypes| > 0 { // We will need to downcast
-        var fullType := if isRcWrapped then R.Rc(datatypeType) else datatypeType;
+        var fullType := if isRcWrapped then rc(datatypeType) else datatypeType;
         var downcastDefinitionOpt := DowncastTraitDeclFor(rTypeParamsDecls, fullType);
         if downcastDefinitionOpt.None? {
           var dummy := Error("Could not generate downcast definition for " + fullType.ToString(""));
         } else {
           s := s + [downcastDefinitionOpt.value];
         }
-        var downcastImplementationsOpt := DowncastImplFor(rTypeParamsDecls, fullType);
+        var downcastImplementationsOpt := DowncastImplFor(rcNew, rTypeParamsDecls, fullType);
         if downcastImplementationsOpt.None? {
           var dummy := Error("Could not generate downcast implementation for " + fullType.ToString(""));
         } else {
@@ -3334,7 +3334,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
         if needsObjectFromRef {
           r := R.dafny_runtime.MSel("Object").AsExpr().ApplyType([R.TIdentifier("_")]).FSel("from_ref").Apply([r]);
         } else if needsRcWrapping {
-          r := R.RcNew(r.Clone());
+          r := rcNew(r.Clone());
         } else {
           if !noNeedOfClone {
             var needUnderscoreClone := isSelf && selfIdent.IsGeneralTrait();