From ecc659a04d8c0995f6f2cc7aad2ecda4579f35f2 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Thu, 27 Oct 2022 15:29:29 -0700 Subject: [PATCH 1/6] Add test case for a nested extern module, get it working for all except Go --- Source/DafnyCore/Compilers/Compiler-java.cs | 5 +++-- Source/DafnyCore/Compilers/Compiler-python.cs | 9 +++++++-- Test/comp/Extern.dfy | 12 +++++++++--- Test/comp/Extern.dfy.expect | 5 +++++ Test/comp/Extern2.cs | 10 ++++++++++ Test/comp/Extern3.js | 16 ++++++++++++++++ Test/comp/Extern5Nested.py | 13 +++++++++++++ Test/comp/__default.java | 7 +++++++ 8 files changed, 70 insertions(+), 7 deletions(-) create mode 100644 Test/comp/Extern5Nested.py create mode 100644 Test/comp/__default.java diff --git a/Source/DafnyCore/Compilers/Compiler-java.cs b/Source/DafnyCore/Compilers/Compiler-java.cs index bdb4f5e99f8..46dd70904dd 100644 --- a/Source/DafnyCore/Compilers/Compiler-java.cs +++ b/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 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) { diff --git a/Source/DafnyCore/Compilers/Compiler-python.cs b/Source/DafnyCore/Compilers/Compiler-python.cs index 217ff3a430d..f1c32036b78 100644 --- a/Source/DafnyCore/Compilers/Compiler-python.cs +++ b/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,14 @@ static bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram outputWriter.WriteLine($"Unable to determine module name: {externFilename}"); return false; } + + var segments = moduleName.Split("."); + var baseName = segments.Last(); 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, baseName + ".py"); + Directory.CreateDirectory(tgtDir); var file = new FileInfo(externFilename); file.CopyTo(tgtFilename, true); if (DafnyOptions.O.CompileVerbose) { diff --git a/Test/comp/Extern.dfy b/Test/comp/Extern.dfy index 2ab51545ff6..8ea8f9c4922 100644 --- a/Test/comp/Extern.dfy +++ b/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" +// RON: %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 %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,7 @@ module {:extern "Library"} Library { static method {:extern} P() } } + +module {:extern "Nested.Library"} Nested.Library { + method {:extern} Foo() +} diff --git a/Test/comp/Extern.dfy.expect b/Test/comp/Extern.dfy.expect index 79b5b50f3cc..aeb564be504 100644 --- a/Test/comp/Extern.dfy.expect +++ b/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 diff --git a/Test/comp/Extern2.cs b/Test/comp/Extern2.cs index 8ea42b9a2b4..2ab0a64172a 100644 --- a/Test/comp/Extern2.cs +++ b/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"); + } + } + } +} diff --git a/Test/comp/Extern3.js b/Test/comp/Extern3.js index 0992fc65dcb..61eca29c0c6 100644 --- a/Test/comp/Extern3.js +++ b/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; +})(); diff --git a/Test/comp/Extern5Nested.py b/Test/comp/Extern5Nested.py new file mode 100644 index 00000000000..ff18cc1d56a --- /dev/null +++ b/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, _dafny + +assert "Nested.Library" == __name__ +Nested_Library = sys.modules[__name__] + +class default__: + def Foo(): + _dafny.print(_dafny.Seq("Nested.Library.Foo\n")) \ No newline at end of file diff --git a/Test/comp/__default.java b/Test/comp/__default.java new file mode 100644 index 00000000000..486e40ef87d --- /dev/null +++ b/Test/comp/__default.java @@ -0,0 +1,7 @@ +package Nested.Library; + +public class __default { + public static void Foo() { + System.out.println("Nested.Library.Foo"); + } +} From 023c7c51ff8caca873f12e26f5b370b3857c343b Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Fri, 28 Oct 2022 16:16:07 -0700 Subject: [PATCH 2/6] Progress on Go --- Source/DafnyCore/Compilers/Compiler-go.cs | 1 + Test/comp/Extern.dfy | 16 +++++++++------- Test/comp/Extern4Nested.go | 1 + Test/comp/Extern4Nested_Library.go | 14 ++++++++++++++ 4 files changed, 25 insertions(+), 7 deletions(-) create mode 100644 Test/comp/Extern4Nested.go create mode 100644 Test/comp/Extern4Nested_Library.go diff --git a/Source/DafnyCore/Compilers/Compiler-go.cs b/Source/DafnyCore/Compilers/Compiler-go.cs index baacd7deb8c..6444c3eefad 100644 --- a/Source/DafnyCore/Compilers/Compiler-go.cs +++ b/Source/DafnyCore/Compilers/Compiler-go.cs @@ -148,6 +148,7 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef } else { // Go ignores all filenames starting with underscores. So we're forced // to rewrite "__default" to "default__". + moduleName = moduleName.Replace(".", "_"); pkgName = moduleName; if (pkgName != "" && pkgName.All(c => c == '_')) { UnsupportedFeatureError(Token.NoToken, Feature.AllUnderscoreExternalModuleNames, diff --git a/Test/comp/Extern.dfy b/Test/comp/Extern.dfy index 8ea8f9c4922..8b3865680db 100644 --- a/Test/comp/Extern.dfy +++ b/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" -// RON: %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 %S/__default.java >> "%t" -// RUN: %dafny /compile:3 /compileTarget:py "%s" %S/Extern5.py %S/Extern5Nested.py >> "%t" +// RON: %dafny /compile:3 /compileTarget:cs "%s" %S/Extern2.cs > "%t" +// RON: %dafny /compile:3 /compileTarget:js "%s" %S/Extern3.js >> "%t" +// RUN: %dafny /compile:3 /compileTarget:go "%s" %S/Extern4.go %S/Extern4Nested.go %S/Extern4Nested_Library.go >> "%t" +// RON: %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" +// RON: %dafny /compile:3 /compileTarget:py "%s" %S/Extern5.py %S/Extern5Nested.py >> "%t" // RUN: %diff "%s.expect" "%t" method Main() { @@ -54,6 +54,8 @@ module {:extern "Library"} Library { } } -module {:extern "Nested.Library"} Nested.Library { - method {:extern} Foo() +module {:extern "Nested"} Nested { + module {:extern "Nested.Library"} Library { + method {:extern} Foo() + } } diff --git a/Test/comp/Extern4Nested.go b/Test/comp/Extern4Nested.go new file mode 100644 index 00000000000..ddf7f4d6cbf --- /dev/null +++ b/Test/comp/Extern4Nested.go @@ -0,0 +1 @@ +package Nested diff --git a/Test/comp/Extern4Nested_Library.go b/Test/comp/Extern4Nested_Library.go new file mode 100644 index 00000000000..d78c2c19d10 --- /dev/null +++ b/Test/comp/Extern4Nested_Library.go @@ -0,0 +1,14 @@ +package Nested_Library + +import ( + "dafny" +) + +type CompanionStruct_Default___ struct { +} +var Companion_Default___ = CompanionStruct_Default___ { +} + +func (_static *CompanionStruct_Default___) Foo() { + dafny.Print((dafny.SeqOfString("Nested.Library.Foo\n")).SetString()) +} From e8e4ace1813fe5ccd93eecc48809c810f4e26081 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Sat, 29 Oct 2022 11:57:40 -0700 Subject: [PATCH 3/6] Working for Go! * Fixed the fact that {:compile false} had no effect on modules * Added Compiler.GetModuleCompileName so Go can further sanitize extern strings Still not ideal because you have to explicitly attach {:compile false} to each intermediate extern module --- Source/DafnyCore/AST/TopLevelDeclarations.cs | 2 +- Source/DafnyCore/Compilers/Compiler-go.cs | 5 ++++- Source/DafnyCore/Compilers/SinglePassCompiler.cs | 5 +++++ Source/DafnyCore/Plugins/Compiler.cs | 6 ++++++ Test/comp/Extern.dfy | 12 ++++++------ Test/comp/Extern4Nested.go | 2 ++ Test/comp/Extern4Nested_Library.go | 14 -------------- Test/comp/Extern4Nested_mLibrary.go | 9 +++++++++ 8 files changed, 33 insertions(+), 22 deletions(-) delete mode 100644 Test/comp/Extern4Nested_Library.go create mode 100644 Test/comp/Extern4Nested_mLibrary.go diff --git a/Source/DafnyCore/AST/TopLevelDeclarations.cs b/Source/DafnyCore/AST/TopLevelDeclarations.cs index ae2fb95392b..4df0f2fc788 100644 --- a/Source/DafnyCore/AST/TopLevelDeclarations.cs +++ b/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 { diff --git a/Source/DafnyCore/Compilers/Compiler-go.cs b/Source/DafnyCore/Compilers/Compiler-go.cs index 6444c3eefad..b764f559281 100644 --- a/Source/DafnyCore/Compilers/Compiler-go.cs +++ b/Source/DafnyCore/Compilers/Compiler-go.cs @@ -67,6 +67,10 @@ private struct Import { public bool SuppressDummy; } + public override string GetModuleCompileName(bool isDefaultModule, string moduleName) { + return moduleName.Replace(".", "_m"); + } + protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) { wr.WriteLine("// Dafny program {0} compiled into Go", program.Name); @@ -148,7 +152,6 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef } else { // Go ignores all filenames starting with underscores. So we're forced // to rewrite "__default" to "default__". - moduleName = moduleName.Replace(".", "_"); pkgName = moduleName; if (pkgName != "" && pkgName.All(c => c == '_')) { UnsupportedFeatureError(Token.NoToken, Feature.AllUnderscoreExternalModuleNames, diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs index 4c726aca7be..83a2d3be450 100644 --- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs +++ b/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) { diff --git a/Source/DafnyCore/Plugins/Compiler.cs b/Source/DafnyCore/Plugins/Compiler.cs index 71337574d6c..bce247fdf99 100644 --- a/Source/DafnyCore/Plugins/Compiler.cs +++ b/Source/DafnyCore/Plugins/Compiler.cs @@ -56,6 +56,12 @@ public virtual string TargetBaseDir(string dafnyProgramName) => /// Change name into a valid identifier in the target language. /// public abstract string PublicIdProtect(string name); + /// + /// Qualify the name moduleName. + /// + public virtual string GetModuleCompileName(bool isDefaultModule, string moduleName) => + PublicIdProtect(moduleName); + /// /// Qualify the name compileName in module moduleName. /// diff --git a/Test/comp/Extern.dfy b/Test/comp/Extern.dfy index 8b3865680db..43e1d27f77e 100644 --- a/Test/comp/Extern.dfy +++ b/Test/comp/Extern.dfy @@ -1,8 +1,8 @@ -// RON: %dafny /compile:3 /compileTarget:cs "%s" %S/Extern2.cs > "%t" -// RON: %dafny /compile:3 /compileTarget:js "%s" %S/Extern3.js >> "%t" -// RUN: %dafny /compile:3 /compileTarget:go "%s" %S/Extern4.go %S/Extern4Nested.go %S/Extern4Nested_Library.go >> "%t" -// RON: %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" -// RON: %dafny /compile:3 /compileTarget:py "%s" %S/Extern5.py %S/Extern5Nested.py >> "%t" +// 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 %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() { @@ -54,7 +54,7 @@ module {:extern "Library"} Library { } } -module {:extern "Nested"} Nested { +module {:compile false} {:extern "Nested"} Nested { module {:extern "Nested.Library"} Library { method {:extern} Foo() } diff --git a/Test/comp/Extern4Nested.go b/Test/comp/Extern4Nested.go index ddf7f4d6cbf..17cbe70980b 100644 --- a/Test/comp/Extern4Nested.go +++ b/Test/comp/Extern4Nested.go @@ -1 +1,3 @@ package Nested + +type Dummy__ struct{} \ No newline at end of file diff --git a/Test/comp/Extern4Nested_Library.go b/Test/comp/Extern4Nested_Library.go deleted file mode 100644 index d78c2c19d10..00000000000 --- a/Test/comp/Extern4Nested_Library.go +++ /dev/null @@ -1,14 +0,0 @@ -package Nested_Library - -import ( - "dafny" -) - -type CompanionStruct_Default___ struct { -} -var Companion_Default___ = CompanionStruct_Default___ { -} - -func (_static *CompanionStruct_Default___) Foo() { - dafny.Print((dafny.SeqOfString("Nested.Library.Foo\n")).SetString()) -} diff --git a/Test/comp/Extern4Nested_mLibrary.go b/Test/comp/Extern4Nested_mLibrary.go new file mode 100644 index 00000000000..84ad94251aa --- /dev/null +++ b/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()) +} From 6a8feeda37530062ab419c42ee4f659515fc9e50 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 31 Oct 2022 12:49:03 -0700 Subject: [PATCH 4/6] Cleanup --- Test/comp/Extern.dfy | 4 +++- Test/comp/Extern4Nested.go | 3 --- 2 files changed, 3 insertions(+), 4 deletions(-) delete mode 100644 Test/comp/Extern4Nested.go diff --git a/Test/comp/Extern.dfy b/Test/comp/Extern.dfy index 43e1d27f77e..17336d0664a 100644 --- a/Test/comp/Extern.dfy +++ b/Test/comp/Extern.dfy @@ -54,7 +54,9 @@ module {:extern "Library"} Library { } } -module {:compile false} {:extern "Nested"} Nested { +// 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() } diff --git a/Test/comp/Extern4Nested.go b/Test/comp/Extern4Nested.go deleted file mode 100644 index 17cbe70980b..00000000000 --- a/Test/comp/Extern4Nested.go +++ /dev/null @@ -1,3 +0,0 @@ -package Nested - -type Dummy__ struct{} \ No newline at end of file From 35f47cb61882829dc8e457aa47e70d0e83adec9e Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 31 Oct 2022 12:58:01 -0700 Subject: [PATCH 5/6] Comment --- Source/DafnyCore/Compilers/Compiler-go.cs | 4 ++++ Source/DafnyCore/Plugins/Compiler.cs | 5 +++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/Source/DafnyCore/Compilers/Compiler-go.cs b/Source/DafnyCore/Compilers/Compiler-go.cs index b764f559281..b36f846a55a 100644 --- a/Source/DafnyCore/Compilers/Compiler-go.cs +++ b/Source/DafnyCore/Compilers/Compiler-go.cs @@ -68,6 +68,10 @@ private struct Import { } 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"); } diff --git a/Source/DafnyCore/Plugins/Compiler.cs b/Source/DafnyCore/Plugins/Compiler.cs index bce247fdf99..ee2c22093f6 100644 --- a/Source/DafnyCore/Plugins/Compiler.cs +++ b/Source/DafnyCore/Plugins/Compiler.cs @@ -56,12 +56,13 @@ public virtual string TargetBaseDir(string dafnyProgramName) => /// Change name into a valid identifier in the target language. /// public abstract string PublicIdProtect(string name); + /// - /// Qualify the name moduleName. + /// Get the compile name for the given moduleName. /// public virtual string GetModuleCompileName(bool isDefaultModule, string moduleName) => PublicIdProtect(moduleName); - + /// /// Qualify the name compileName in module moduleName. /// From 33d24683e09fa56486d62d14c0db7a55ce76f635 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Tue, 1 Nov 2022 09:34:55 -0700 Subject: [PATCH 6/6] Apply suggestions from code review Co-authored-by: Fabio Madge --- Source/DafnyCore/Compilers/Compiler-python.cs | 3 +-- Test/comp/Extern5Nested.py | 4 ++-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/Source/DafnyCore/Compilers/Compiler-python.cs b/Source/DafnyCore/Compilers/Compiler-python.cs index f1c32036b78..2a3dfb02902 100644 --- a/Source/DafnyCore/Compilers/Compiler-python.cs +++ b/Source/DafnyCore/Compilers/Compiler-python.cs @@ -1715,11 +1715,10 @@ static bool CopyExternLibraryIntoPlace(string externFilename, string mainProgram } var segments = moduleName.Split("."); - var baseName = segments.Last(); var mainDir = Path.GetDirectoryName(mainProgram); Contract.Assert(mainDir != null); var tgtDir = segments[..^1].Aggregate(mainDir, Path.Combine); - var tgtFilename = Path.Combine(tgtDir, baseName + ".py"); + var tgtFilename = Path.Combine(tgtDir, segments[^1] + ".py"); Directory.CreateDirectory(tgtDir); var file = new FileInfo(externFilename); file.CopyTo(tgtFilename, true); diff --git a/Test/comp/Extern5Nested.py b/Test/comp/Extern5Nested.py index ff18cc1d56a..2d38fbf9e06 100644 --- a/Test/comp/Extern5Nested.py +++ b/Test/comp/Extern5Nested.py @@ -3,11 +3,11 @@ entire module must be supplied. """ -import sys, _dafny +import sys assert "Nested.Library" == __name__ Nested_Library = sys.modules[__name__] class default__: def Foo(): - _dafny.print(_dafny.Seq("Nested.Library.Foo\n")) \ No newline at end of file + print("Nested.Library.Foo\n")