Fix: --rust-module-name with externs (#5865)

Fixes #5864

### Description
This PR adds the ability to use `--rust-module-name` along with externs,
by detecting that we are not generating an entry library file, and in
that case it removes the "pub mod" declaration for the externs since
side files do not have the ability to import externs themselves.
Since the Rust compiler is internal, we don't advertise this change yet.

### How has this been tested?
The test `translate_additional/more_dafny.dfy` was updated to include
externs. The test was not working without this PR, reproducing
faithfully the issue.

<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/Rust/Dafny-compiler-rust.dfy

@@ -3744,8 +3744,10 @@ module {:extern "DCOMP"} DafnyToRustCompiler {
         } else {
           error := Some("Unrecognized external file " + externalFile + ". External file must be *.rs files");
         }
-        var externMod := R.ExternMod(externalMod);
-        s := s + externMod.ToString("") + "\n";
+        if rootType.RootCrate? {
+          var externMod := R.ExternMod(externalMod);
+          s := s + externMod.ToString("") + "\n";
+        }
         externUseDecls := externUseDecls + [
           R.UseDecl(R.Use(R.PUB, R.crate.MSel(externalMod).MSel("*")))
         ];

Source/DafnyCore/GeneratedFromDafny/DCOMP.cs

@@ -6679,9 +6679,11 @@ public RAST._IExpr Error(Dafny.ISequence<Dafny.Rune> message, RAST._IExpr defaul
         } else {
           (this).error = Std.Wrappers.Option<Dafny.ISequence<Dafny.Rune>>.create_Some(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("Unrecognized external file "), _2_externalFile), Dafny.Sequence<Dafny.Rune>.UnicodeFromString(". External file must be *.rs files")));
         }
-        RAST._IMod _4_externMod;
-        _4_externMod = RAST.Mod.create_ExternMod(_3_externalMod);
-        s = Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(s, (_4_externMod)._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""))), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"));
+        if (((this).rootType).is_RootCrate) {
+          RAST._IMod _4_externMod;
+          _4_externMod = RAST.Mod.create_ExternMod(_3_externalMod);
+          s = Dafny.Sequence<Dafny.Rune>.Concat(Dafny.Sequence<Dafny.Rune>.Concat(s, (_4_externMod)._ToString(Dafny.Sequence<Dafny.Rune>.UnicodeFromString(""))), Dafny.Sequence<Dafny.Rune>.UnicodeFromString("\n"));
+        }
         _0_externUseDecls = Dafny.Sequence<RAST._IModDecl>.Concat(_0_externUseDecls, Dafny.Sequence<RAST._IModDecl>.FromElements(RAST.ModDecl.create_UseDecl(RAST.Use.create(RAST.Visibility.create_PUB(), ((RAST.__default.crate).MSel(_3_externalMod)).MSel(Dafny.Sequence<Dafny.Rune>.UnicodeFromString("*"))))));
       }
       if (!(_0_externUseDecls).Equals(Dafny.Sequence<RAST._IModDecl>.FromElements())) {

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny.dfy

@@ -1,12 +1,16 @@
-// RUN: %baredafny translate rs --rust-module-name additional_module "%s"
+// RUN: %baredafny translate rs --rust-module-name additional_module "%S/more_dafny_extern.rs" "%s"
 // RUN: %exits-with -any %rm -f "%S/project_depending_on_dafny/src/additional_module.rs"
+// RUN: %exits-with -any %rm -f "%S/project_depending_on_dafny/src/more_dafny_extern.rs"
 // RUN: %mv "%S/more_dafny-rust/src/more_dafny.rs" "%S/project_depending_on_dafny/src/additional_module.rs"
+// RUN: %mv "%S/more_dafny-rust/src/more_dafny_extern.rs" "%S/project_depending_on_dafny/src/more_dafny_extern.rs"
 // RUN: "%S/project_depending_on_dafny/cargo" run > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module SubModule {
+  function {:axiom} {:extern "extern_dafny", "eight"} Eight(): (r: bv16) ensures r == 8
+
   function reverse(input: bv16): bv16 {
-    ((input & 0xFF) << 8) | ((input & 0xFF00) >> 8)
+    ((input & 0xFF) << Eight()) | ((input & 0xFF00) >> Eight())
   }
 }
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/more_dafny_extern.rs

@@ -0,0 +1,5 @@
+pub mod extern_dafny {
+  pub fn eight() -> u16 {
+    8
+  }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/.gitignore

@@ -1,2 +1,3 @@
 src/additional_module.rs
+src/more_dafny_extern.rs
 target/

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/translate-additional/project_depending_on_dafny/src/project_depending_on_dafny.rs

@@ -1,4 +1,5 @@
 pub mod additional_module;
+pub mod more_dafny_extern;
 
 fn main() {
   let x = additional_module::_module::_default::reverse(10);