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 baacd7deb8c..b36f846a55a 100644 --- a/Source/DafnyCore/Compilers/Compiler-go.cs +++ b/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); 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..2a3dfb02902 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,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) { diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs index b13788c4004..e3ad9996a00 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..ee2c22093f6 100644 --- a/Source/DafnyCore/Plugins/Compiler.cs +++ b/Source/DafnyCore/Plugins/Compiler.cs @@ -56,6 +56,13 @@ public virtual string TargetBaseDir(string dafnyProgramName) => /// Change name into a valid identifier in the target language. /// public abstract string PublicIdProtect(string name); + + /// + /// 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. /// diff --git a/Test/comp/Extern.dfy b/Test/comp/Extern.dfy index 2ab51545ff6..17336d0664a 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" +// 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() + } +} 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/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()) +} diff --git a/Test/comp/Extern5Nested.py b/Test/comp/Extern5Nested.py new file mode 100644 index 00000000000..2d38fbf9e06 --- /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 + +assert "Nested.Library" == __name__ +Nested_Library = sys.modules[__name__] + +class default__: + def Foo(): + print("Nested.Library.Foo\n") 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"); + } +}