feat: Semantics for dots in {:extern} module names in Python

Source/DafnyCore/Compilers/Python/Compiler-python.cs

@@ -89,7 +89,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern,
         string libraryName, ConcreteSyntaxTree wr) {
       moduleName = IdProtect(moduleName);
-      var file = wr.NewFile($"{moduleName}.py");
+      var modulePath = moduleName.Replace('.', Path.DirectorySeparatorChar);
+      var file = wr.NewFile($"{modulePath}.py");
       EmitImports(moduleName, file);
       return file;
     }
@@ -104,7 +105,9 @@ private void EmitImports(string moduleName, ConcreteSyntaxTree wr) {
       if (moduleName != null) {
         wr.WriteLine();
         wr.WriteLine($"assert \"{moduleName}\" == __name__");
-        wr.WriteLine($"{moduleName} = sys.modules[__name__]");
+        if (!moduleName.Contains('.')) {
+          wr.WriteLine($"{moduleName} = sys.modules[__name__]");
+        }
 
         Imports.Add(moduleName);
       }

Source/DafnyCore/Compilers/Python/PythonBackend.cs

@@ -28,7 +28,7 @@ protected override SinglePassCompiler CreateCompiler() {
     return new PythonCompiler(Options, Reporter);
   }
 
-  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));
@@ -40,7 +40,7 @@ private static string FindModuleName(string externFilename) {
       }
     }
     rd.Close();
-    return externFilename.EndsWith(".py") ? externFilename[..^3] : null;
+    return Path.GetExtension(externFilename) == ".py" ? Path.GetFileNameWithoutExtension(externFilename) : null;
   }
 
   bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextWriter outputWriter) {
@@ -52,8 +52,10 @@ bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram, TextW
     }
     var mainDir = Path.GetDirectoryName(mainProgram);
     Contract.Assert(mainDir != null);
-    var tgtFilename = Path.Combine(mainDir, moduleName + ".py");
+    var modulePath = moduleName.Replace('.', Path.DirectorySeparatorChar);
+    var tgtFilename = Path.Combine(mainDir, $"{modulePath}.py");
     var file = new FileInfo(externFilename);
+    Directory.CreateDirectory(Path.GetDirectoryName(tgtFilename)!);
     file.CopyTo(tgtFilename, true);
     if (Options.CompileVerbose) {
       outputWriter.WriteLine($"Additional input {externFilename} copied to {tgtFilename}");

Source/DafnyCore/ConcreteSyntax/ConcreteSyntaxTree.cs

@@ -200,13 +200,17 @@ public ConcreteSyntaxTree NewFile(string filename) {
     // ----- Collection ------------------------------
 
     public override string ToString() {
+      return MakeString();
+    }
+
+    public string MakeString(int indentSize = 2) {
       var sw = new StringWriter();
       var files = new Queue<FileSyntax>();
-      Render(sw, 0, new WriterState(), files);
+      Render(sw, 0, new WriterState(), files, indentSize);
       while (files.Count != 0) {
         var ftw = files.Dequeue();
         sw.WriteLine("#file {0}", ftw.Filename);
-        ftw.Render(sw, 0, new WriterState(), files);
+        ftw.Render(sw, 0, new WriterState(), files, indentSize);
       }
 
       return sw.ToString();

Source/DafnyDriver/DafnyDriver.cs

@@ -866,7 +866,7 @@ public static bool CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyP
         var callToMainTree = new ConcreteSyntaxTree();
         string baseName = Path.GetFileNameWithoutExtension(dafnyProgramName);
         compiler.EmitCallToMain(mainMethod, baseName, callToMainTree);
-        callToMain = callToMainTree.ToString(); // assume there aren't multiple files just to call main
+        callToMain = callToMainTree.MakeString(compiler.TargetIndentSize); // assume there aren't multiple files just to call main
       }
       Contract.Assert(hasMain == (callToMain != null));
       bool targetProgramHasErrors = dafnyProgram.Reporter.Count(ErrorLevel.Error) != oldErrorCount;

Test/comp/ExternNestedModule.dfy

@@ -0,0 +1,11 @@
+// RUN: %dafny /compile:4 /spillTargetCode:2 /compileTarget:py %S/ExternNestedModule.py "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main(){
+    print Library.THREE, "\n";
+}
+
+module {:extern "Nested.Library"} Library {
+    const THREE := TWO + 1; 
+    const TWO: int
+}

Test/comp/ExternNestedModule.dfy.expect

@@ -0,0 +1,3 @@
+
+Dafny program verifier finished with 0 verified, 0 errors
+3

Test/comp/ExternNestedModule.py

@@ -0,0 +1,19 @@
+import sys
+import _dafny
+
+assert "Nested.Library" == __name__
+
+class default__:
+    def  __init__(self):
+        pass
+
+    def __dafnystr__(self) -> str:
+        return "Nested.Library_Compile._default"
+
+    @_dafny.classproperty
+    def TWO(instance):
+        return 2
+
+    @_dafny.classproperty
+    def THREE(instance):
+        return default__.TWO + 1

docs/dev/news/3919.feat

@@ -0,0 +1 @@
+Semantic interpretation of dots in names for `{:extern}` modules when compiling to Python