Feat: Add --rust-module-name to specify a module name

Source/DafnyCore/Backends/DafnyExecutableBackend.cs

@@ -55,13 +55,12 @@ public override void Compile(Program dafnyProgram, string dafnyProgramName, Conc
     ((DafnyCodeGenerator)codeGenerator).Start();
     codeGenerator.Compile(dafnyProgram, new ConcreteSyntaxTree());
     var dast = ((DafnyCodeGenerator)codeGenerator).Build();
-    var o = DafnyCodeGenerator.Compile(
+    DafnyCodeGenerator.Compile(
       (Sequence<DAST.Module>)Sequence<DAST.Module>.FromArray(dast.ToArray()),
       (Sequence<ISequence<Rune>>)Sequence<ISequence<Rune>>.FromArray(
         ImportFiles(dafnyProgramName).Select(fileName =>
           Sequence<Rune>.UnicodeFromString(Path.GetFileName(fileName))).ToArray()
-      ));
-    output.Write(o.ToVerbatimString(false));
+      ), output);
   }
 
   public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree output) {

Source/DafnyCore/Backends/DafnyWrittenCodeGenerator.cs

@@ -5,7 +5,7 @@ namespace Microsoft.Dafny.Compilers {
 
   public abstract class DafnyWrittenCodeGenerator {
 
-    public abstract ISequence<Rune> Compile(Sequence<DAST.Module> program, Sequence<ISequence<Rune>> otherFiles);
+    public abstract void Compile(Sequence<DAST.Module> program, Sequence<ISequence<Rune>> otherFiles, ConcreteSyntaxTree w);
 
     public abstract ISequence<Rune> EmitCallToMain(string fullName);
 

Source/DafnyCore/Backends/ResolvedDesugaredExecutableDafny/ResolvedDesugaredExecutableDafnyCodeGenerator.cs

@@ -8,8 +8,8 @@ namespace Microsoft.Dafny.Compilers;
 
 class ResolvedDesugaredExecutableDafnyCodeGenerator : DafnyWrittenCodeGenerator {
 
-  public override ISequence<Rune> Compile(Sequence<DAST.Module> program, Sequence<ISequence<Rune>> otherFiles) {
-    return COMP.Compile(program);
+  public override void Compile(Sequence<DAST.Module> program, Sequence<ISequence<Rune>> otherFiles, ConcreteSyntaxTree w) {
+    w.Write(COMP.Compile(program).ToVerbatimString(false));
   }
 
   public override ISequence<Rune> EmitCallToMain(string fullName) {

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

@@ -1675,7 +1675,9 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
       ASSIGNED_PREFIX + "_" + rustName
   }
 
-  datatype ObjectType = RawPointers | RcMut
+  datatype PointerType = Raw | RcMut
+  datatype CharType = UTF16 | Unicode
+  datatype RootType = RootCrate | RootPath(moduleName: string)
 
   datatype GenTypeContext =
     GenTypeContext(forTraitParents: bool)
@@ -1790,53 +1792,58 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
   }
 
   class COMP {
-    const UnicodeChars: bool
-    const DafnyChar := if UnicodeChars then "DafnyChar" else "DafnyCharUTF16"
-    const DafnyCharUnderlying := if UnicodeChars then R.RawType("char") else R.RawType("u16")
-    const string_of := if UnicodeChars then "string_of" else "string_utf16_of"
+    const charType: CharType
+    const pointerType: PointerType
+    const rootType: RootType
+
+    const thisFile: R.Path := if rootType.RootCrate? then R.crate else R.crate.MSel(rootType.moduleName)
+
+    const DafnyChar := if charType.Unicode? then "DafnyChar" else "DafnyCharUTF16"
+    const DafnyCharUnderlying := if charType.Unicode? then R.RawType("char") else R.RawType("u16")
+    const string_of := if charType.Unicode? then "string_of" else "string_utf16_of"
     const allocate :=
-      if ObjectType.RawPointers? then "allocate" else "allocate_object"
+      if pointerType.Raw? then "allocate" else "allocate_object"
     const allocate_fn := "_" + allocate
     const update_field_uninit_macro :=
-      if ObjectType.RawPointers? then "update_field_uninit!" else "update_field_uninit_object!"
+      if pointerType.Raw? then "update_field_uninit!" else "update_field_uninit_object!"
     const thisInConstructor :=
-      if ObjectType.RawPointers? then R.Identifier("this") else R.Identifier("this").Clone()
+      if pointerType.Raw? then R.Identifier("this") else R.Identifier("this").Clone()
     const array_construct :=
-      if ObjectType.RawPointers? then "construct" else "construct_object"
-    const modify_macro := R.dafny_runtime.MSel(if ObjectType.RawPointers? then "modify!" else "md!").AsExpr()
-    const read_macro := R.dafny_runtime.MSel(if ObjectType.RawPointers? then "read!" else "rd!").AsExpr()
+      if pointerType.Raw? then "construct" else "construct_object"
+    const modify_macro := R.dafny_runtime.MSel(if pointerType.Raw? then "modify!" else "md!").AsExpr()
+    const read_macro := R.dafny_runtime.MSel(if pointerType.Raw? then "read!" else "rd!").AsExpr()
     function Object(underlying: R.Type): R.Type {
-      if ObjectType.RawPointers? then R.PtrType(underlying) else R.ObjectType(underlying)
+      if pointerType.Raw? then R.PtrType(underlying) else R.ObjectType(underlying)
     }
-    const placebos_usize := if ObjectType.RawPointers? then "placebos_usize" else "placebos_usize_object"
+    const placebos_usize := if pointerType.Raw? then "placebos_usize" else "placebos_usize_object"
     const update_field_if_uninit_macro :=
-      if ObjectType.RawPointers? then "update_field_if_uninit!" else "update_field_if_uninit_object!"
+      if pointerType.Raw? then "update_field_if_uninit!" else "update_field_if_uninit_object!"
     const Upcast :=
-      if ObjectType.RawPointers? then "Upcast" else "UpcastObject"
+      if pointerType.Raw? then "Upcast" else "UpcastObject"
     const UpcastFnMacro :=
       Upcast + "Fn!"
     const upcast :=
-      if ObjectType.RawPointers? then "upcast" else "upcast_object"
+      if pointerType.Raw? then "upcast" else "upcast_object"
 
     const downcast :=
-      if ObjectType.RawPointers? then "cast!" else "cast_object!"
+      if pointerType.Raw? then "cast!" else "cast_object!"
 
     function UnreachablePanicIfVerified(optText: string := ""): string {
-      if ObjectType.RawPointers? then "unsafe { ::std::hint::unreachable_unchecked() }" else
+      if pointerType.Raw? then "unsafe { ::std::hint::unreachable_unchecked() }" else
       if optText == "" then "panic!()" else "panic!(\"" + optText + "\")"
     }
 
-    const ObjectType: ObjectType
 
     var error: Option<string>
 
     var optimizations: seq<R.Mod -> R.Mod>
 
     static const DAFNY_EXTERN_MODULE := "_dafny_externs"
 
-    constructor(unicodeChars: bool, objectType: ObjectType) {
-      this.UnicodeChars := unicodeChars;
-      this.ObjectType := objectType;
+    constructor(charType: CharType, pointerType: PointerType, rootType: RootType) {
+      this.charType := charType;
+      this.pointerType := pointerType;
+      this.rootType := rootType;
       this.error := None; // If error, then the generated code contains <i>Unsupported: .*</i>
       this.optimizations := [FactorPathsOptimization.apply];
       new;
@@ -1862,7 +1869,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
         var body, allmodules := GenModuleBody(mod, mod.body.value, containingPath + [Ident.Ident(innerName)]);
         if optExtern.SimpleExtern? {
           if mod.requiresExterns {
-            body := [R.UseDecl(R.Use(R.PUB, R.crate.MSel(DAFNY_EXTERN_MODULE).MSel(ReplaceDotByDoubleColon(optExtern.overrideName)).MSel("*")))] + body;
+            body := [R.UseDecl(R.Use(R.PUB, thisFile.MSel(DAFNY_EXTERN_MODULE).MSel(ReplaceDotByDoubleColon(optExtern.overrideName)).MSel("*")))] + body;
           }
         } else if optExtern.AdvancedExtern? {
           error := Some("Externs on modules can only have 1 string argument");
@@ -2872,7 +2879,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
       }
     }
 
-    static method GenPath(p: seq<Ident>, escape: bool := true) returns (r: R.Path) {
+    method GenPath(p: seq<Ident>, escape: bool := true) returns (r: R.Path) {
       if |p| == 0 {
         return R.Self();
       } else {
@@ -2882,7 +2889,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           else if p[0].id.dafny_name == "_System" then
             R.dafny_runtime
           else
-            R.Crate();
+            thisFile;
         for i := 0 to |p| {
           var name := p[i].id;
           if escape {
@@ -2899,12 +2906,12 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
       }
     }
 
-    static method GenPathType(p: seq<Ident>) returns (t: R.Type) {
+    method GenPathType(p: seq<Ident>) returns (t: R.Type) {
       var p := GenPath(p, true);
       t := p.AsType();
     }
 
-    static method GenPathExpr(p: seq<Ident>, escape: bool := true) returns (e: R.Expr) {
+    method GenPathExpr(p: seq<Ident>, escape: bool := true) returns (e: R.Expr) {
       if |p| == 0 {
         return R.self;
       }
@@ -3152,18 +3159,18 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
         if (forTrait) {
           // Mutability is required when not using raw pointers, even for functione, because
           // --release optimisations sometimes removes the code to increment the reference counting on upcasting
-          var selfFormal := if m.wasFunction && ObjectType.RawPointers? then R.Formal.selfBorrowed else R.Formal.selfBorrowedMut;
+          var selfFormal := if m.wasFunction && pointerType.Raw? then R.Formal.selfBorrowed else R.Formal.selfBorrowedMut;
           params := [selfFormal] + params;
         } else {
           var tpe := GenType(instanceType, GenTypeContext.default());
           if selfId == "this" {
-            if ObjectType.RcMut? {
+            if pointerType.RcMut? {
               tpe := R.Borrowed(tpe);
             }
             // For raw pointers, no borrowing is necessary, because it implements the Copy type
           } else if selfId == "self" {
             if tpe.IsObjectOrPointer() { // For classes and traits
-              if m.wasFunction && ObjectType.RawPointers? {
+              if m.wasFunction && pointerType.Raw? {
                 tpe := R.SelfBorrowed;
               } else {
                 tpe := R.SelfBorrowedMut;
@@ -3862,7 +3869,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
         }
         case Literal(CharLiteral(c)) => {
           r := R.LiteralInt(Strings.OfNat(c as nat));
-          if !UnicodeChars {
+          if !charType.Unicode? {
             r := R.TypeAscription(r, R.U16);
           } else {
             r :=
@@ -3877,7 +3884,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
         }
         case Literal(Null(tpe)) => {
           var tpeGen := GenType(tpe, GenTypeContext.default());
-          if ObjectType.RawPointers? {
+          if pointerType.Raw? {
             r := R.std.MSel("ptr").FSel("null_mut");
           } else {
             r := R.TypeAscription(R.dafny_runtime.MSel("Object").AsExpr().Apply1(R.RawExpr("None")), tpeGen);
@@ -4011,7 +4018,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
             match op {
               case Eq(referential) => {
                 if (referential) {
-                  if ObjectType.RawPointers? {
+                  if pointerType.Raw? {
                     error := Some("Cannot compare raw pointers yet - need to wrap them with a structure to ensure they are compared properly");
                     r := R.RawExpr(error.value);
                   } else {
@@ -4373,7 +4380,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
           case (Primitive(Int), Primitive(Char)) => {
             var rhsType := GenType(toTpe, GenTypeContext.default());
             var recursiveGen, _, recIdents := GenExpr(expr, selfIdent, env, OwnershipOwned);
-            r := R.RawExpr("::dafny_runtime::" + DafnyChar + "(" + (if UnicodeChars then "char::from_u32(<u32" else "<u16") + " as ::dafny_runtime::NumCast>::from(" + recursiveGen.ToString(IND) + ").unwrap())" + if UnicodeChars then ".unwrap())" else "");
+            r := R.RawExpr("::dafny_runtime::" + DafnyChar + "(" + (if charType.Unicode? then "char::from_u32(<u32" else "<u16") + " as ::dafny_runtime::NumCast>::from(" + recursiveGen.ToString(IND) + ").unwrap())" + if charType.Unicode? then ".unwrap())" else "");
             r, resultingOwnership := FromOwned(r, expectedOwnership);
             readIdents := recIdents;
           }
@@ -5076,12 +5083,10 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
                   r := R.Identifier("this");
                 case _ =>
               }
-              if ObjectType.RcMut?  {
-                r := r.Clone();
-              }
-              if ObjectType.RawPointers? {
+              if pointerType.Raw? {
                 r := read_macro.Apply1(r);
               } else {
+                r := r.Clone();
                 r := modify_macro.Apply1(r); // Functions have to take &mut because of upcasting
               }
             }
@@ -5130,7 +5135,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
         case IndexRange(on, isArray, low, high) => {
           var onExpectedOwnership :=
             if isArray then
-              if ObjectType.RawPointers? then
+              if pointerType.Raw? then
                 OwnershipOwned
               else
                 OwnershipBorrowed
@@ -5168,7 +5173,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
               methodName := "_" + methodName;
             }
             var object_suffix :=
-              if ObjectType.RawPointers? then "" else "_object";
+              if pointerType.Raw? then "" else "_object";
             r := R.dafny_runtime_Sequence.FSel("from_array"+methodName+object_suffix).Apply([onExpr] + arguments);
           } else {
             if methodName != "" {
@@ -5208,14 +5213,14 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
               var onExpr, recOwnership, recIdents;
               if base.Trait? || base.Class? {
                 onExpr, recOwnership, recIdents := GenExpr(on, selfIdent, env, OwnershipOwned);
-                if ObjectType.RawPointers? {
+                if pointerType.Raw? {
                   onExpr := read_macro.Apply1(onExpr);
                 } else {
                   onExpr := modify_macro.Apply1(onExpr);
                 }
                 readIdents := readIdents + recIdents;
               } else {
-                var expectedOnOwnership := if ObjectType.RawPointers? then OwnershipBorrowed else OwnershipBorrowedMut;
+                var expectedOnOwnership := if pointerType.Raw? then OwnershipBorrowed else OwnershipBorrowedMut;
                 onExpr, recOwnership, recIdents := GenExpr(on, selfIdent, env, expectedOnOwnership);
                 readIdents := readIdents + recIdents;
               }
@@ -5236,7 +5241,7 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
                       case CallName(_, Some(tpe), _, _, _) =>
                         var typ := GenType(tpe, GenTypeContext.default());
                         if typ.IsObjectOrPointer() {
-                          if ObjectType.RawPointers? {
+                          if pointerType.Raw? {
                             onExpr := read_macro.Apply1(onExpr);
                           } else {
                             onExpr := modify_macro.Apply1(onExpr);

Source/DafnyCore/Backends/Rust/RustBackend.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
+using System.CommandLine;
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Linq;
@@ -24,6 +25,15 @@ public class RustBackend : DafnyExecutableBackend {
   public override bool SupportsInMemoryCompilation => false;
   public override bool TextualTargetIsExecutable => false;
 
+  public static readonly Option<string> RustModuleNameOption = new("--rust-module-name",
+    @"This Option is used to specify the Rust Module Name for the currently translated code, i.e. what goes between crate:: ...  ::module_name".TrimStart()) {
+  };
+  public override IEnumerable<Option<string>> SupportedOptions => new List<Option<string>> { RustModuleNameOption };
+
+  static RustBackend() {
+    OptionRegistry.RegisterOption(RustModuleNameOption, OptionScope.Translation);
+  }
+
   public override IReadOnlySet<string> SupportedNativeTypes =>
     new HashSet<string> { "byte", "sbyte", "ushort", "short", "uint", "int", "ulong", "long", "udoublelong", "doublelong" };
 

Source/DafnyCore/Backends/Rust/RustCodeGenerator.cs

@@ -1,4 +1,6 @@
 using System;
+using System.CommandLine;
+using System.Configuration;
 using System.IO;
 using System.Linq;
 using Dafny;
@@ -13,15 +15,23 @@ public RustCodeGenerator(DafnyOptions options) {
       this.Options = options;
     }
 
-    public override ISequence<Rune> Compile(Sequence<DAST.Module> program, Sequence<ISequence<Rune>> otherFiles) {
+    public override void Compile(Sequence<DAST.Module> program, Sequence<ISequence<Rune>> otherFiles, ConcreteSyntaxTree w) {
       var c = new DCOMP.COMP();
-      c.__ctor(Options.Get(CommonOptionBag.UnicodeCharacters),
-        Options.Get(CommonOptionBag.RawPointers) ? ObjectType.create_RawPointers() : ObjectType.create_RcMut());
+      var charType = Options.Get(CommonOptionBag.UnicodeCharacters)
+        ? DCOMP.CharType.create_Unicode()
+        : DCOMP.CharType.create_UTF16();
+      var pointerType = Options.Get(CommonOptionBag.RawPointers)
+        ? PointerType.create_Raw()
+        : PointerType.create_RcMut();
+      var rootType = Options.Get(RustBackend.RustModuleNameOption) is var opt && opt != "" ?
+          RootType.create_RootPath(Sequence<Rune>.UnicodeFromString(opt))
+          : RootType.create_RootCrate();
+      c.__ctor(charType, pointerType, rootType);
       var s = c.Compile(program, otherFiles);
       if (!Options.Get(CommonOptionBag.EmitUncompilableCode) && c.error.is_Some) {
         throw new UnsupportedInvalidOperationException(c.error.dtor_value.ToVerbatimString(false));
       }
-      return s;
+      w.Write(s.ToVerbatimString(false));
     }
 
     public override ISequence<Rune> EmitCallToMain(string fullName) {