feat: python-module-name (#5461)

### Description
<!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md
-->
<!-- Is this a bug fix for an issue visible in the latest release?
Mention this in the PR details and ensure a patch release is considered
-->

#### 1

Add a `--python-module-name` option to the (new) Dafny CLI.
This option takes in a string that will be prefixed to translated module
imports.

ex. If a module has a generated Python import statement `import
MyModule`,
then translating with `--python-module-name=my_python_module`
will result in an import statement `import my_python_module.MyModule as
MyModule`.

I intend that Smithy-Dafny will use this with
`--python-module-name=[module_name].internaldafny.generated`.

#### 2

Do not generate `import module_` for `System_.py` in the DafnyRuntime
Python.
Before this change `System_.py` in the DafnyRuntimePython generates this
import. This removes that import.
Two problems with this import:
1. (Correctness problem, i.e. "why this change is necessary") The
DafnyRuntimePython does not include a `module_.py`. Having `import
module_` prevents the DafnyRuntimeModule from being used on its own.
2. (My problem, i.e. "why I'm making this change now") `import module_`
is an invalid import statement with module mode. `module_` will be
located at `[python_module_name].module_`, and isn't able to be imported
without qualifiers.

An alternative to removing the import is to generate a `module_.py` in
the DafnyRuntimePython. I don't know why DafnyRuntimePython doesn't have
this file, so this was easier for me. I don't have an opinion on which
approach happens; I'll defer to the Dafny team on the approach.

#### 3

Python: Do not generate import statements for empty modules.
"Empty modules" might come from prefixes of nested modules.
This is a follow-up to
4ce2f7e,
which stopped generating empty modules.

### How has this been tested?
<!-- Tests can be added to
`Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to
`Source/*.Test/…` and run with `dotnet test` -->

Some tests in the directory above:

* singlemodule (validating compiling and running with 1 module)
* multimodule (validating compiling and running with 2 modules with a
dependency relationship)
* nestedmodule (validating depending on a (Python) module with a nested
(Dafny) module name)

I've tested this with Smithy-Dafny-Python and the (WIP) Python MPL, and
this behavior works as I'd expect.

<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>

---------

Co-authored-by: Shubham Chaturvedi <[email protected]>
Co-authored-by: Robin Salkeld <[email protected]>

Source/DafnyCore/Backends/Python/PythonBackend.cs

@@ -1,11 +1,13 @@
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
+using System.CommandLine;
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Linq;
 using System.Text.RegularExpressions;
 using System.Runtime.InteropServices;
 using System.Threading.Tasks;
+using DafnyCore.Options;
 
 namespace Microsoft.Dafny.Compilers;
 
@@ -26,10 +28,29 @@ public override string TargetBaseDir(string dafnyProgramName) =>
   public override bool SupportsInMemoryCompilation => false;
   public override bool TextualTargetIsExecutable => true;
 
+  public bool PythonModuleMode { get; set; } = true;
+  public string PythonModuleName;
+
+  public static readonly Option<string> PythonModuleNameCliOption = new("--python-module-name",
+    @"This Option is used to specify the Python Module Name for the translated code".TrimStart()) {
+  };
+  public override IEnumerable<Option<string>> SupportedOptions => new List<Option<string>> { PythonModuleNameCliOption };
+
+  static PythonBackend() {
+    TranslationRecord.RegisterLibraryChecks(new Dictionary<Option, OptionCompatibility.OptionCheck> {
+      { PythonModuleNameCliOption, OptionCompatibility.NoOpOptionCheck }
+    });
+  }
+
   public override IReadOnlySet<string> SupportedNativeTypes =>
     new HashSet<string> { "byte", "sbyte", "ushort", "short", "uint", "int", "number", "ulong", "long" };
 
   protected override SinglePassCodeGenerator CreateCodeGenerator() {
+    var pythonModuleName = Options.Get(PythonModuleNameCliOption);
+    PythonModuleMode = pythonModuleName != null;
+    if (PythonModuleMode) {
+      PythonModuleName = pythonModuleName;
+    }
     return new PythonCodeGenerator(Options, Reporter);
   }
 

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

@@ -4,19 +4,34 @@
 using System.Linq;
 using System.Numerics;
 using DafnyCore.Backends.Python;
+using DafnyCore.Options;
 using JetBrains.Annotations;
 using Microsoft.BaseTypes;
 
 namespace Microsoft.Dafny.Compilers {
 
   class PythonCodeGenerator : SinglePassCodeGenerator {
+
+    private bool PythonModuleMode;
+    private string PythonModuleName;
+
     public PythonCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(options, reporter) {
+      var pythonModuleName = Options.Get(PythonBackend.PythonModuleNameCliOption);
+      PythonModuleMode = pythonModuleName != null;
+      if (PythonModuleMode) {
+        PythonModuleName = pythonModuleName.ToString();
+      }
+
       if (Options?.CoverageLegendFile != null) {
-        Imports.Add("DafnyProfiling");
+        Imports.Add("DafnyProfiling", "DafnyProfiling");
       }
     }
 
-    private readonly List<string> Imports = new() { DafnyDefaultModule };
+    // Key: Fully-qualified module name with python-module-name/outer-module
+    // Value: Dafny-generated Python module name without python-module-name/outer-module
+    // This separation is used to identify nested extern modules,
+    //   which currently cannot be used with python-module-name/outer-module.
+    private readonly Dictionary<string, string> Imports = new Dictionary<string, string>();
 
     public override IReadOnlySet<Feature> UnsupportedFeatures => new HashSet<Feature> {
       Feature.SubsetTypeTests,
@@ -28,6 +43,8 @@ public PythonCodeGenerator(DafnyOptions options, ErrorReporter reporter) : base(
 
     private const string DafnyRuntimeModule = "_dafny";
     private const string DafnyDefaultModule = "module_";
+    private const string DafnySystemModule = "System_";
+    private static readonly ISet<string> DafnyRuntimeGeneratedModuleNames = new HashSet<string> { DafnySystemModule, };
     const string DafnySetClass = $"{DafnyRuntimeModule}.Set";
     const string DafnyMultiSetClass = $"{DafnyRuntimeModule}.MultiSet";
     const string DafnySeqClass = $"{DafnyRuntimeModule}.Seq";
@@ -56,8 +73,8 @@ protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {
         EmitRuntimeSource("DafnyStandardLibraries_py", wr);
       }
 
-      Imports.Add(DafnyRuntimeModule);
-      EmitImports(null, wr);
+      Imports.Add(DafnyRuntimeModule, DafnyRuntimeModule);
+      EmitImports(null, null, wr);
       wr.WriteLine();
     }
 
@@ -83,29 +100,111 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
 
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
       string libraryName, ConcreteSyntaxTree wr) {
+      var pythonModuleName = PythonModuleMode ? PythonModuleName + "." : "";
+
       moduleName = PublicModuleIdProtect(moduleName);
-      var file = wr.NewFile($"{moduleName}.py");
-      EmitImports(moduleName, file);
+      // Nested extern modules should be written inside a folder
+      var file = wr.NewFile($"{moduleName.Replace(".", "/")}.py");
+      EmitImports(moduleName, pythonModuleName, file);
       return file;
     }
 
     protected override void DependOnModule(Program program, ModuleDefinition module, ModuleDefinition externModule,
       string libraryName) {
-      var moduleName = IdProtect(module.GetCompileName(Options));
-      Imports.Add(moduleName);
+      var dependencyPythonModuleName = "";
+
+      // If the module being depended on was compiled using module mode,
+      // this module needs to rely on it using the dependency's translation record,
+      // even if this module is not using module mode
+      var translatedRecord = program.Compilation.AlreadyTranslatedRecord;
+      translatedRecord.OptionsByModule.TryGetValue(module.FullDafnyName, out var moduleOptions);
+      object dependencyModuleName = null;
+      moduleOptions?.TryGetValue(PythonBackend.PythonModuleNameCliOption.Name, out dependencyModuleName);
+      if (dependencyModuleName is string && !string.IsNullOrEmpty((string)dependencyModuleName)) {
+        dependencyPythonModuleName = dependencyModuleName is string name ? (string)dependencyModuleName + "." : "";
+        if (String.IsNullOrEmpty(dependencyPythonModuleName)) {
+          Reporter.Warning(MessageSource.Compiler, ResolutionErrors.ErrorId.none, Token.Cli,
+            $"Python Module Name not found for the module {module.GetCompileName(Options)}");
+        }
+      }
+
+      var dependencyCompileName = IdProtect(module.GetCompileName(Options));
+      // Don't import an empty module.
+      // Empty modules aren't generated, so their imports aren't valid.
+      if (!TranslationRecord.ModuleEmptyForCompilation(module)) {
+        Imports.Add(dependencyPythonModuleName + dependencyCompileName, dependencyCompileName);
+      }
     }
 
-    private void EmitImports(string moduleName, ConcreteSyntaxTree wr) {
+    private void EmitImports(string moduleName, string pythonModuleName, ConcreteSyntaxTree wr) {
       wr.WriteLine("import sys");
       wr.WriteLine("from typing import Callable, Any, TypeVar, NamedTuple");
       wr.WriteLine("from math import floor");
       wr.WriteLine("from itertools import count");
       wr.WriteLine();
-      Imports.ForEach(module => wr.WriteLine($"import {module}"));
+      // Don't emit `import module_` for generated modules in the DafnyRuntimePython.
+      // The DafnyRuntimePython doesn't have a module.py file, so the import isn't valid.
+      if (!(DafnyRuntimeGeneratedModuleNames.Contains(moduleName))) {
+        wr.WriteLine($"import {(PythonModuleMode ? PythonModuleName + "." + DafnyDefaultModule : DafnyDefaultModule)} as {DafnyDefaultModule}");
+      }
+      foreach (var module in Imports) {
+        if (module.Value.Contains(".")) {
+          // This code branch only applies to extern modules. (ex. module {:extern "a.b.c"})
+          // If module.Value has `.`s in it, it is a nested extern module.
+          // (Non-extern nested modules with `.`s in their names
+          // will have their `.`s replaced with `_` before this code is executed,
+          // ex. module M.N --> "M_N", and will not hit this branch.)
+          // 
+          // Nested externs currently CANNOT be used with python-module-name:
+          //
+          // 1. (Python behavior; not able to be changed)
+          // Aliased Python modules cannot have `.`s in their name.
+          // ex. with `import X as Y`, `Y` cannot have `.`s.
+          //
+          // 2. (Dafny behavior; able to be changed, but don't need to change)
+          // Inside Dafny-generated Python modules,
+          // references to modules do not contain the python-module-name prefix.
+          // ex. If python-module-name=X.Y, and we have nested extern module "a.b.c",
+          //     code generation ignores the prefix and writes `a.b.c`.
+          //     Similarly, an extern non-nested module `E` is not prefixed and is generated as `E`,
+          //     and a non-extern nested module `M.N` is prefixed and generated as `X.Y.M_N`.
+          // (Similarly, extern modules do not contain the outer-module prefix).
+          // 
+          // 1. and 2. taken together prevent nested extern modules from being used with python-module-name.
+          // The reference to the nested extern inside generated code MUST be `a.b.c` due to 1).
+          // However, the aliased import cannot have `.`s in it due to 2).
+          // So nested externs cannot be aliased.
+          // Nested non-externs can be aliased (since, in 2., any nested `.`s are replaced with `_`s).
+          // Non-nested externs can be aliased (since, in 2., `Y` does not have `.`s).
+          //
+          // There are several possible paths to supporting these features together:
+          // - Modify behavior in 1 to apply prefixe (python-module-name/outer-module) to externs.
+          //   This is out of scope for python-module-name, since the outer-module prefix also does not apply to externs.
+          //   These are both "prefixes", and I expect any solution for python-module-name should also apply to outer-module.
+          // - Modify nested extern behavior to replace `.`s with `_`s, similar to nested non-externs.
+          if (!module.Value.Equals(module.Key)) {
+            throw new NotSupportedException($"Nested extern modules cannot be used with python-module-name. Nested extern: {module.Value}");
+          }
+          // Import the nested extern module directly.
+          // ex. module {:extern "a.b.c"} ==> `import a.b.c`
+          wr.WriteLine($"import {module.Value}");
+        } else {
+          // Here, module.Key == [python-module-name][outer-module][module.Value].
+          // However, in the body of the generated module, Dafny-generated code only references module.Value.
+          // Alias the import to module.Value so generated code can use the module.
+          //
+          // ex. python-module-name `X.Y`, outer-module=`A.B`:
+          // module `M` ==> `import X.Y.A_B_M as M`
+          // module `M.N` ==> `import X.Y.A_B_M_N as M_N`
+          // non-nested extern module `E` ==> `import X.Y.E as E` (outer-module prefix not applied to externs)
+          // nested extern modules not supported with python-module-name/outer-module prefixes.
+          wr.WriteLine($"import {module.Key} as {module.Value}");
+        }
+      }
       if (moduleName != null) {
         wr.WriteLine();
         wr.WriteLine($"# Module: {moduleName}");
-        Imports.Add(moduleName);
+        Imports.Add(pythonModuleName + moduleName, moduleName);
       }
     }
 

Source/DafnyCore/Options/CommonOptionBag.cs

@@ -5,6 +5,7 @@
 using DafnyCore;
 using DafnyCore.Options;
 using Serilog.Events;
+using Microsoft.Dafny.Compilers;
 
 namespace Microsoft.Dafny;
 
@@ -616,6 +617,7 @@ void ParsePrintMode(Option<PrintModes> option, Boogie.CommandLineParseState ps,
     DooFile.RegisterNoChecksNeeded(ExtractCounterexample, false);
     DooFile.RegisterNoChecksNeeded(ShowProofObligationExpressions, false);
     DooFile.RegisterNoChecksNeeded(GoBackend.GoModuleNameCliOption, false);
+    DooFile.RegisterNoChecksNeeded(PythonBackend.PythonModuleNameCliOption, false);
   }
 }
 

Source/DafnyCore/Options/TranslationRecord.cs

@@ -48,7 +48,7 @@ public TranslationRecord(Program program) {
     }
   }
 
-  private static bool ModuleEmptyForCompilation(ModuleDefinition module) {
+  public static bool ModuleEmptyForCompilation(ModuleDefinition module) {
     return !(module.DefaultClass?.Members.Any() ?? false)   // DefaultClass is null for _System
            && module.TopLevelDecls.All(d => d is DefaultClassDecl or ModuleDecl);
   }

Source/DafnyRuntime/DafnyRuntimePython/System_.py

@@ -3,8 +3,7 @@
 from math import floor
 from itertools import count
 
-import module_
-import _dafny
+import _dafny as _dafny
 
 # Module: System_
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/DerivedModule.dfy

@@ -0,0 +1,13 @@
+// RUN: %baredafny translate py  --python-module-name=PythonModule2 --library="%S/PythonModule1.doo" --translation-record "%S/PythonModule1-py.dtr" --output "%S/PythonModule2" "%s"
+// RUN: rm -rf "%S/PythonModule2"
+// RUN: mv "%S/PythonModule2-py" "%S/PythonModule2"
+// RUN: pip3 install "%S"
+// RUN: python3 %S/PythonModule2/ > %t
+// RUN: %diff "%s.expect" "%t"
+module DafnyModule3 {
+import DafnyModule1
+
+method Main() {
+        DafnyModule1.HelloWorld();
+}
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/DerivedModule.dfy.expect

@@ -0,0 +1 @@
+Hello World

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1-py.dtr

@@ -0,0 +1,4 @@
+file_format_version = "1.0"
+dafny_version = "4.6.0.0"
+[options_by_module.DafnyModule1]
+python-module-name = "PythonModule1"

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1/DafnyModule1.py

@@ -0,0 +1,19 @@
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import PythonModule1.module_ as module_
+import _dafny as _dafny
+import System_ as System_
+
+# Module: PythonModule1.DafnyModule1
+
+class default__:
+    def  __init__(self):
+        pass
+
+    @staticmethod
+    def HelloWorld():
+        _dafny.print((_dafny.SeqWithoutIsStrInference(map(_dafny.CodePoint, "Hello World"))).VerbatimString(False))
+

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1/__main__.py

@@ -0,0 +1,9 @@
+# Dafny program helloworld.dfy compiled into Python
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import PythonModule1.module_ as module_
+import _dafny as _dafny
+

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule1/module_.py

@@ -0,0 +1,12 @@
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import PythonModule1.module_ as module_
+import _dafny as _dafny
+import System_ as System_
+import PythonModule1.DafnyModule1 as DafnyModule1
+
+# Module: PythonModule1.module_
+

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/setup.py

@@ -0,0 +1,13 @@
+# setup.py
+# installs the committed PythonModule1 and generated PythonModule2 as a Python module
+from setuptools import setup
+
+setup(
+    name="testpythonmodulemultimodule",
+    version="0.1.0",
+    packages=["PythonModule1", "PythonModule2"],
+    python_requires='>=3.6',
+    install_requires=[
+        'DafnyRuntimePython',
+    ],
+)

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/Some.py

@@ -0,0 +1,13 @@
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import SomeNestedModule.module_ as module_
+import _dafny as _dafny
+import System_ as System_
+import SomeNestedModule.Some_Nested_Module as Some_Nested_Module
+import SomeNestedModule.Some_Nested as Some_Nested
+
+# Module: Some
+

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/SomeNestedModule-py.dtr

@@ -0,0 +1,4 @@
+file_format_version = "1.0"
+dafny_version = "4.6.0.0"
+[options_by_module."Some.Nested.Module"]
+python-module-name = "SomeNestedModule"

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/Some_Nested.py

@@ -0,0 +1,12 @@
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import SomeNestedModule.module_ as module_
+import _dafny as _dafny
+import System_ as System_
+import SomeNestedModule.Some_Nested_Module as Some_Nested_Module
+
+# Module: Some_Nested
+

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/Some_Nested_Module.py

@@ -0,0 +1,19 @@
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import SomeNestedModule.module_ as module_
+import _dafny as _dafny
+import System_ as System_
+
+# Module: Some_Nested_Module
+
+class default__:
+    def  __init__(self):
+        pass
+
+    @staticmethod
+    def HelloWorld():
+        _dafny.print((_dafny.SeqWithoutIsStrInference(map(_dafny.CodePoint, "Hello World"))).VerbatimString(False))
+

Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/nestedmodule/SomeNestedModule/__main__.py

@@ -0,0 +1,9 @@
+# Dafny program SomeNestedModule.dfy compiled into Python
+import sys
+from typing import Callable, Any, TypeVar, NamedTuple
+from math import floor
+from itertools import count
+
+import SomeNestedModule.module_ as module_
+import _dafny as _dafny
+