Improve fix

dafny-lang · Oct 9, 2024 · 55aeb7d · 55aeb7d
1 parent 22a1bf7
commit 55aeb7d
Show file tree

Hide file tree

Showing 3 changed files with 14 additions and 13 deletions.
diff --git a/Source/DafnyCore/AST/Modules/ImportModuleDecl.cs b/Source/DafnyCore/AST/Modules/ImportModuleDecl.cs
@@ -5,9 +5,8 @@ namespace Microsoft.Dafny;
 public abstract class ImportModuleDecl : ModuleDecl {
   public readonly ModuleQualifiedId TargetQId; // generated by the parser, this is looked up
 
-  protected ImportModuleDecl(Cloner cloner, ImportModuleDecl original, ModuleDefinition parent) : 
-    base(cloner, original, parent)
-  {
+  protected ImportModuleDecl(Cloner cloner, ImportModuleDecl original, ModuleDefinition parent) :
+    base(cloner, original, parent) {
     if (original.TargetQId != null) { // TODO is this null check necessary?
       TargetQId = new ModuleQualifiedId(cloner, original.TargetQId);
 
@@ -21,10 +20,9 @@ protected ImportModuleDecl(Cloner cloner, ImportModuleDecl original, ModuleDefin
     }
   }
 
-  protected ImportModuleDecl(DafnyOptions options, RangeToken rangeToken, ModuleQualifiedId path, Name name, 
-    ModuleDefinition parent, bool opened, bool isRefining, Guid cloneId) 
-    : base(options, rangeToken, name, parent, opened, isRefining, cloneId)
-  {
+  protected ImportModuleDecl(DafnyOptions options, RangeToken rangeToken, ModuleQualifiedId path, Name name,
+    ModuleDefinition parent, bool opened, bool isRefining, Guid cloneId)
+    : base(options, rangeToken, name, parent, opened, isRefining, cloneId) {
     TargetQId = path;
   }
 }
diff --git a/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs b/Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
@@ -13,6 +13,7 @@
 using System.Text.RegularExpressions;
 using DafnyCore;
 using DafnyCore.Options;
+using DAST;
 using JetBrains.Annotations;
 using Tomlyn.Model;
 using static Microsoft.Dafny.ConcreteSyntaxTreeUtils;
@@ -113,10 +114,13 @@ void EmitModuleHeader(ConcreteSyntaxTree wr, ModuleDefinition module) {
       wr.WriteLine("package {0}", ModuleName);
       wr.WriteLine();
       EmitImports(wr, out var importWriter, out var dummyImportWriter);
-      foreach (var alias in module.TopLevelDecls.OfType<ImportModuleDecl>()) {
-        var importedDef = alias.TargetQId.Decl.Signature.ModuleDef;
+
+      var defsToImport = module.TopLevelDecls.OfType<ImportModuleDecl>()
+        .Select(d => d.TargetQId.Decl.Signature.ModuleDef).Concat(
+          module.TopLevelDecls.OfType<LiteralModuleDecl>().Select(l => l.ModuleDef));
+      foreach (var importedDef in defsToImport) {
         var externModule = GetExternalModuleFromModule(importedDef, out var libraryName);
-        var import = CreateImport(importedDef.GetCompileName(Options), false, externModule, libraryName); 
+        var import = CreateImport(importedDef.GetCompileName(Options), false, externModule, libraryName);
         EmitImport(import, importWriter, dummyImportWriter);
       }
       wr.WriteLine();

diff --git a/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs b/Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs
@@ -1580,7 +1580,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
 
       Contract.Assert(enclosingModule == null);
       enclosingModule = module;
-      var wr = CreateModule(module, module.GetCompileName(Options), module.IsDefaultModule, 
+      var wr = CreateModule(module, module.GetCompileName(Options), module.IsDefaultModule,
         externModule, libraryName, module.Attributes, programNode);
       var v = new CheckHasNoAssumes_Visitor(this, wr);
       foreach (TopLevelDecl d in module.TopLevelDecls) {
@@ -1705,8 +1705,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
       enclosingModule = null;
     }
 
-    protected ModuleDefinition GetExternalModuleFromModule(ModuleDefinition module, out string libraryName)
-    {
+    protected ModuleDefinition GetExternalModuleFromModule(ModuleDefinition module, out string libraryName) {
       ModuleDefinition externModule = null;
       libraryName = null;
       if (!Options.DisallowExterns) {