From 8e7fafa273dae843248f6b98d0552e279ba5a121 Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 28 Apr 2023 02:22:07 +0200 Subject: [PATCH 1/2] feat: Semantics for dots in extern module names in Python --- .../Compilers/Python/Compiler-python.cs | 7 +++++-- .../Compilers/Python/PythonBackend.cs | 8 +++++--- .../ConcreteSyntax/ConcreteSyntaxTree.cs | 8 ++++++-- Source/DafnyDriver/DafnyDriver.cs | 2 +- Test/comp/ExternNestedModule.dfy | 11 +++++++++++ Test/comp/ExternNestedModule.dfy.expect | 3 +++ Test/comp/ExternNestedModule.py | 19 +++++++++++++++++++ docs/dev/news/3919.feat | 1 + 8 files changed, 51 insertions(+), 8 deletions(-) create mode 100644 Test/comp/ExternNestedModule.dfy create mode 100644 Test/comp/ExternNestedModule.dfy.expect create mode 100644 Test/comp/ExternNestedModule.py create mode 100644 docs/dev/news/3919.feat diff --git a/Source/DafnyCore/Compilers/Python/Compiler-python.cs b/Source/DafnyCore/Compilers/Python/Compiler-python.cs index e7403f27393..4b28d452cb7 100644 --- a/Source/DafnyCore/Compilers/Python/Compiler-python.cs +++ b/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); } diff --git a/Source/DafnyCore/Compilers/Python/PythonBackend.cs b/Source/DafnyCore/Compilers/Python/PythonBackend.cs index 010ddac5053..2abaa8a8b02 100644 --- a/Source/DafnyCore/Compilers/Python/PythonBackend.cs +++ b/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}"); diff --git a/Source/DafnyCore/ConcreteSyntax/ConcreteSyntaxTree.cs b/Source/DafnyCore/ConcreteSyntax/ConcreteSyntaxTree.cs index 82b4f16d189..a744e62a03e 100644 --- a/Source/DafnyCore/ConcreteSyntax/ConcreteSyntaxTree.cs +++ b/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(); - 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(); diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs index 0512428424f..8402c0edd58 100644 --- a/Source/DafnyDriver/DafnyDriver.cs +++ b/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; diff --git a/Test/comp/ExternNestedModule.dfy b/Test/comp/ExternNestedModule.dfy new file mode 100644 index 00000000000..17f193150c4 --- /dev/null +++ b/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 +} \ No newline at end of file diff --git a/Test/comp/ExternNestedModule.dfy.expect b/Test/comp/ExternNestedModule.dfy.expect new file mode 100644 index 00000000000..641ab97d123 --- /dev/null +++ b/Test/comp/ExternNestedModule.dfy.expect @@ -0,0 +1,3 @@ + +Dafny program verifier finished with 0 verified, 0 errors +3 diff --git a/Test/comp/ExternNestedModule.py b/Test/comp/ExternNestedModule.py new file mode 100644 index 00000000000..2c3b8828f57 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/docs/dev/news/3919.feat b/docs/dev/news/3919.feat new file mode 100644 index 00000000000..2cc921f7bf5 --- /dev/null +++ b/docs/dev/news/3919.feat @@ -0,0 +1 @@ +Semantic interpretation of dots in names for `{:extern}` modules when compiling to Python From f3554ce8375889c53cd533d731233d3d00b8a34e Mon Sep 17 00:00:00 2001 From: Fabio Madge Date: Fri, 28 Apr 2023 02:57:28 +0200 Subject: [PATCH 2/2] Test everywhere