Add test case for a nested extern module, get it working for all exce…

Source/DafnyCore/AST/TopLevelDeclarations.cs

@@ -729,7 +729,7 @@ public string CompileName {
       if (compileName == null) {
         var externArgs = DafnyOptions.O.DisallowExterns ? null : Attributes.FindExpressions(this.Attributes, "extern");
         if (externArgs != null && 1 <= externArgs.Count && externArgs[0] is StringLiteralExpr) {
-          compileName = (string)((StringLiteralExpr)externArgs[0]).Value;
+          compileName = DafnyOptions.O.Compiler.GetModuleCompileName(IsDefaultModule, (string)((StringLiteralExpr)externArgs[0]).Value);
         } else if (externArgs != null) {
           compileName = Name;
         } else {

Source/DafnyCore/Compilers/Compiler-go.cs

@@ -67,6 +67,14 @@ private struct Import {
       public bool SuppressDummy;
     }
 
+    public override string GetModuleCompileName(bool isDefaultModule, string moduleName) {
+      // Go doesn't really support nested module names in the same way Dafny does,
+      // only nested paths to modules, but where module names do not contain any such separators.
+      // So we "escape" periods in the same way we do non-extern modules
+      // so that attributes like `{:extern "A.B.C"}` can function for all targets.
+      return moduleName.Replace(".", "_m");
+    }
+
     protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
       wr.WriteLine("// Dafny program {0} compiled into Go", program.Name);
 

Source/DafnyCore/Compilers/Compiler-java.cs

@@ -2347,7 +2347,8 @@ static bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram
       string baseName = Path.GetFileNameWithoutExtension(externFilename);
       var mainDir = Path.GetDirectoryName(mainProgram);
       Contract.Assert(mainDir != null);
-      var tgtDir = Path.Combine(mainDir, pkgName);
+      var segments = pkgName.Split(".");
+      var tgtDir = segments.Aggregate(mainDir, Path.Combine);
       var tgtFilename = Path.Combine(tgtDir, baseName + ".java");
       Directory.CreateDirectory(tgtDir);
       FileInfo file = new FileInfo(externFilename);
@@ -2381,7 +2382,7 @@ protected override void EmitReturn(List<Formal> outParams, ConcreteSyntaxTree wr
       }
     }
 
-    private static readonly Regex PackageLine = new Regex(@"^\s*package\s+([a-zA-Z0-9_]+)\s*;$");
+    private static readonly Regex PackageLine = new Regex(@"^\s*package\s+([a-zA-Z0-9_]+(\.[a-zA-Z0-9_]+)*)\s*;$");
 
     // TODO: See if more types need to be added
     bool IsDirectlyComparable(Type t) {

Source/DafnyCore/Compilers/Compiler-python.cs

@@ -1693,7 +1693,7 @@ protected override void EmitHaltRecoveryStmt(Statement body, string haltMessageV
       TrStmt(recoveryBody, exceptBlock);
     }
 
-    private static readonly Regex ModuleLine = new(@"^\s*assert\s+""([a-zA-Z0-9_]+)""\s*==\s*__name__\s*$");
+    private static readonly Regex ModuleLine = new(@"^\s*assert\s+""(([a-zA-Z0-9_]+)(\.[a-zA-Z0-9_]+)*)""\s*==\s*__name__\s*$");
 
     private static string FindModuleName(string externFilename) {
       using var rd = new StreamReader(new FileStream(externFilename, FileMode.Open, FileAccess.Read));
@@ -1713,9 +1713,13 @@ static bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram
         outputWriter.WriteLine($"Unable to determine module name: {externFilename}");
         return false;
       }
+
+      var segments = moduleName.Split(".");
       var mainDir = Path.GetDirectoryName(mainProgram);
       Contract.Assert(mainDir != null);
-      var tgtFilename = Path.Combine(mainDir, moduleName + ".py");
+      var tgtDir = segments[..^1].Aggregate(mainDir, Path.Combine);
+      var tgtFilename = Path.Combine(tgtDir, segments[^1] + ".py");
+      Directory.CreateDirectory(tgtDir);
       var file = new FileInfo(externFilename);
       file.CopyTo(tgtFilename, true);
       if (DafnyOptions.O.CompileVerbose) {

Source/DafnyCore/Compilers/SinglePassCompiler.cs

@@ -1269,6 +1269,11 @@ public override void Compile(Program program, ConcreteSyntaxTree wrx) {
         if (!m.IsToBeCompiled) {
           continue;
         }
+
+        bool compileModule = true;
+        if (Attributes.ContainsBool(m.Attributes, "compile", ref compileModule) && !compileModule) {
+          continue;
+        }
         var moduleIsExtern = false;
         string libraryName = null;
         if (!DafnyOptions.O.DisallowExterns) {

Source/DafnyCore/Plugins/Compiler.cs

@@ -56,6 +56,13 @@ public virtual string TargetBaseDir(string dafnyProgramName) =>
   /// Change <c>name</c> into a valid identifier in the target language.
   /// </summary>
   public abstract string PublicIdProtect(string name);
+
+  /// <summary>
+  /// Get the compile name for the given <c>moduleName</c>.
+  /// </summary>
+  public virtual string GetModuleCompileName(bool isDefaultModule, string moduleName) =>
+    PublicIdProtect(moduleName);
+
   /// <summary>
   /// Qualify the name <c>compileName</c> in module <c>moduleName</c>.
   /// </summary>

Test/comp/Extern.dfy

@@ -1,8 +1,8 @@
 // RUN: %dafny /compile:3 /compileTarget:cs "%s" %S/Extern2.cs > "%t"
 // RUN: %dafny /compile:3 /compileTarget:js "%s" %S/Extern3.js >> "%t"
-// RUN: %dafny /compile:3 /compileTarget:go "%s" %S/Extern4.go >> "%t"
-// RUN: %dafny /compile:3 /compileTarget:java "%s" %S/LibClass.java %S/OtherClass.java %S/AllDafny.java %S/Mixed.java %S/AllExtern.java >> "%t"
-// RUN: %dafny /compile:3 /compileTarget:py "%s" %S/Extern5.py >> "%t"
+// RUN: %dafny /compile:3 /compileTarget:go "%s" %S/Extern4.go %S/Extern4Nested_mLibrary.go >> "%t"
+// RUN: %dafny /compile:3 /compileTarget:java "%s" %S/LibClass.java %S/OtherClass.java %S/AllDafny.java %S/Mixed.java %S/AllExtern.java %S/__default.java >> "%t"
+// RUN: %dafny /compile:3 /compileTarget:py "%s" %S/Extern5.py %S/Extern5Nested.py >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Main() {
@@ -20,6 +20,8 @@ method Main() {
   print m.IF(), "\n";
   Library.AllExtern.P();
   assert Library.AllDafny.Seven() == Library.Mixed.Seven() == Library.AllExtern.Seven();
+
+  Nested.Library.Foo();
 }
 
 module {:extern "Library"} Library {
@@ -51,3 +53,11 @@ module {:extern "Library"} Library {
     static method {:extern} P()
   }
 }
+
+// Expanded like this for the benefit of Go.
+// See https://github.com/dafny-lang/dafny/issues/2953.
+module {:compile false} Nested {
+  module {:extern "Nested.Library"} Library {
+    method {:extern} Foo()
+  }
+}

Test/comp/Extern.dfy.expect

@@ -8,6 +8,7 @@ Extern static method says: Mixed.P
 Extern instance method says: Mixed.IP
 2002
 AllExtern.P
+Nested.Library.Foo
 
 Dafny program verifier finished with 4 verified, 0 errors
 Hello
@@ -18,6 +19,7 @@ Extern static method says: Mixed.P
 Extern instance method says: Mixed.IP
 2002
 AllExtern.P
+Nested.Library.Foo
 
 Dafny program verifier finished with 4 verified, 0 errors
 Hello
@@ -28,6 +30,7 @@ Extern static method says: Mixed.P
 Extern instance method says: Mixed.IP
 2002
 AllExtern.P
+Nested.Library.Foo
 
 Dafny program verifier finished with 4 verified, 0 errors
 Hello
@@ -38,6 +41,7 @@ Extern static method says: Mixed.P
 Extern instance method says: Mixed.IP
 2002
 AllExtern.P
+Nested.Library.Foo
 
 Dafny program verifier finished with 4 verified, 0 errors
 Hello
@@ -48,3 +52,4 @@ Extern static method says: Mixed.P
 Extern instance method says: Mixed.IP
 2002
 AllExtern.P
+Nested.Library.Foo

Test/comp/Extern2.cs

@@ -44,3 +44,13 @@ public static void P() {
     }
   }
 }
+
+namespace Nested {
+  namespace Library {
+    class __default {
+      public static void Foo() {
+        System.Console.WriteLine("Nested.Library.Foo");
+      }
+    }
+  }
+}

Test/comp/Extern3.js

@@ -53,3 +53,19 @@ let Library = (function() {
 
   return $module;
 })();
+
+let Nested = (function() {
+  let $module = {};
+
+  $module.Library = (function() {
+    let $module2 = {};
+
+    $module2.Foo = function() {
+      process.stdout.write("Nested.Library.Foo\n");
+    }
+
+    return $module2;
+  })();
+
+  return $module;
+})();

Test/comp/Extern4Nested_mLibrary.go

@@ -0,0 +1,9 @@
+package Nested_mLibrary
+
+import (
+  "dafny"
+)
+
+func Foo() {
+  dafny.Print((dafny.SeqOfString("Nested.Library.Foo\n")).SetString())
+}

Test/comp/Extern5Nested.py

@@ -0,0 +1,13 @@
+"""
+The Python compiler only supports {:extern} code on a module level, so the
+entire module must be supplied.
+"""
+
+import sys
+
+assert "Nested.Library" == __name__
+Nested_Library = sys.modules[__name__]
+
+class default__:
+    def Foo():
+        print("Nested.Library.Foo\n")

Test/comp/__default.java

@@ -0,0 +1,7 @@
+package Nested.Library;
+
+public class __default {
+    public static void Foo() {
+        System.out.println("Nested.Library.Foo");
+    }
+}