Fix GoLang issue when module and datatype names collide

Source/DafnyCore/AST/Cloner.cs

@@ -626,28 +626,24 @@ class DeepModuleSignatureCloner : Cloner {
     public DeepModuleSignatureCloner(bool cloneResolvedFields = false) : base(false, cloneResolvedFields) {
     }
 
-    public override TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition newParent) {
-      var dd = base.CloneDeclaration(d, newParent);
-      if (d is ModuleDecl) {
-        ((ModuleDecl)dd).Signature = ((ModuleDecl)d).Signature;
-        if (d is AbstractModuleDecl) {
-          var sourcefacade = (AbstractModuleDecl)d;
-
-          ((AbstractModuleDecl)dd).OriginalSignature = sourcefacade.OriginalSignature;
-          if (sourcefacade.QId.Root != null) {
-            ((AbstractModuleDecl)dd).QId.Root = (ModuleDecl)CloneDeclaration(sourcefacade.QId.Root, newParent);
-          }
-        } else if (d is AliasModuleDecl) {
-          var sourcealias = (AliasModuleDecl)d;
+    public override TopLevelDecl CloneDeclaration(TopLevelDecl original, ModuleDefinition newParent) {
+      var result = base.CloneDeclaration(original, newParent);
+      if (original is not ModuleDecl moduleDecl) {
+        return result;
+      }
 
-          if (sourcealias.TargetQId.Root != null) {
-            ((AliasModuleDecl)dd).TargetQId.Root =
-              (ModuleDecl)CloneDeclaration(sourcealias.TargetQId.Root, newParent);
-          }
+      ((ModuleDecl)result).Signature = moduleDecl.Signature;
+      if (moduleDecl is ImportModuleDecl importModuleDecl) {
+        if (importModuleDecl.TargetQId.Root != null) {
+          ((AliasModuleDecl)result).TargetQId.Root =
+            (ModuleDecl)CloneDeclaration(importModuleDecl.TargetQId.Root, newParent);
         }
       }
+      if (moduleDecl is AbstractModuleDecl abstractModuleDecl) {
+        ((AbstractModuleDecl)result).OriginalSignature = abstractModuleDecl.OriginalSignature;
+      }
 
-      return dd;
+      return result;
     }
   }
 

Source/DafnyCore/AST/Grammar/Printer/Printer.cs

@@ -429,7 +429,7 @@ public void PrintTopLevelDecls(CompilationData compilation, IEnumerable<TopLevel
               wr.Write(" opened");
             }
             wr.Write(" {0} ", dd.Name);
-            wr.Write(": {0}", dd.QId.ToString());
+            wr.Write(": {0}", dd.TargetQId.ToString());
             if (dd.Exports.Count > 0) {
               wr.Write("`{{{0}}}", Util.Comma(dd.Exports, id => id.val));
             }

Source/DafnyCore/AST/Modules/AbstractModuleDecl.cs

@@ -8,25 +8,22 @@ namespace Microsoft.Dafny;
 /// Represents "module name as path [ = compilePath];", where name is a identifier and path is a possibly qualified name.
 /// Used to be called ModuleFacadeDecl -- renamed to be like LiteralModuleDecl, AliasModuleDecl
 /// </summary>
-public class AbstractModuleDecl : ModuleDecl, ICanFormat {
-  public readonly ModuleQualifiedId QId;
+public class AbstractModuleDecl : ImportModuleDecl, ICanFormat {
   public readonly List<IToken> Exports; // list of exports sets
   public ModuleDecl CompileRoot;
   public ModuleSignature OriginalSignature;
 
   public AbstractModuleDecl(Cloner cloner, AbstractModuleDecl original, ModuleDefinition parent)
     : base(cloner, original, parent) {
     Exports = original.Exports;
-    QId = new ModuleQualifiedId(cloner, original.QId);
   }
 
   public AbstractModuleDecl(DafnyOptions options, RangeToken rangeToken, ModuleQualifiedId qid, Name name,
     ModuleDefinition parent, bool opened, List<IToken> exports, Guid cloneId)
-    : base(options, rangeToken, name, parent, opened, false, cloneId) {
+    : base(options, rangeToken, qid, name, parent, opened, false, cloneId) {
     Contract.Requires(qid != null && qid.Path.Count > 0);
     Contract.Requires(exports != null);
 
-    QId = qid;
     Exports = exports;
   }
 

Source/DafnyCore/AST/Modules/AliasModuleDecl.cs

@@ -10,34 +10,21 @@ namespace Microsoft.Dafny;
 /// <summary>
 /// Represents "module name = path;", where name is an identifier and path is a possibly qualified name.
 /// </summary>
-public class AliasModuleDecl : ModuleDecl, ICanFormat {
-  public readonly ModuleQualifiedId TargetQId; // generated by the parser, this is looked up
+public class AliasModuleDecl : ImportModuleDecl, ICanFormat {
   public readonly List<IToken> Exports; // list of exports sets
   [FilledInDuringResolution] public bool ShadowsLiteralModule;  // initialized early during Resolution (and used not long after that); true for "import opened A = A" where "A" is a literal module in the same scope
 
   public AliasModuleDecl(Cloner cloner, AliasModuleDecl original, ModuleDefinition parent)
     : base(cloner, original, parent) {
-    if (original.TargetQId != null) { // TODO is this null check necessary?
-      TargetQId = new ModuleQualifiedId(cloner, original.TargetQId);
-
-      /*
-       * Refinement cloning happens in PreResolver, which is after the ModuleQualifiedId.Root fields are set,
-       * so this field must be copied as part of refinement cloning.
-       * However, letting refinement cloning set CloneResolvedFields==true causes exceptions for an uninvestigated reason,
-       * so we will clone this field even when !CloneResolvedFields.
-       */
-      TargetQId.Root = original.TargetQId.Root;
-    }
     Exports = original.Exports;
   }
 
   public AliasModuleDecl(DafnyOptions options, RangeToken rangeToken, ModuleQualifiedId path, Name name,
     ModuleDefinition parent, bool opened, List<IToken> exports, Guid cloneId)
-    : base(options, rangeToken, name, parent, opened, false, cloneId) {
+    : base(options, rangeToken, path, name, parent, opened, false, cloneId) {
     Contract.Requires(path != null && path.Path.Count > 0);
     Contract.Requires(exports != null);
     Contract.Requires(exports.Count == 0 || path.Path.Count == 1);
-    TargetQId = path;
     Exports = exports;
   }
 

Source/DafnyCore/AST/Modules/ImportModuleDecl.cs

@@ -0,0 +1,28 @@
+using System;
+
+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) {
+    if (original.TargetQId != null) { // TODO is this null check necessary?
+      TargetQId = new ModuleQualifiedId(cloner, original.TargetQId);
+
+      /*
+       * Refinement cloning happens in PreResolver, which is after the ModuleQualifiedId.Root fields are set,
+       * so this field must be copied as part of refinement cloning.
+       * However, letting refinement cloning set CloneResolvedFields==true causes exceptions for an uninvestigated reason,
+       * so we will clone this field even when !CloneResolvedFields.
+       */
+      TargetQId.Root = original.TargetQId.Root;
+    }
+  }
+
+  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;
+  }
+}

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -163,7 +163,7 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
         wr.WriteLine("#if ISDAFNYRUNTIMELIB");
       }
 
-      var dafnyNamespace = CreateModule("Dafny", false, null, null, null, wr);
+      var dafnyNamespace = CreateModule(null, "Dafny", false, null, null, null, wr);
       EmitInitNewArrays(systemModuleManager, dafnyNamespace);
       if (Synthesize) {
         CsharpSynthesizer.EmitMultiMatcher(dafnyNamespace);
@@ -274,7 +274,8 @@ string IdProtectModule(string moduleName) {
       return string.Join(".", moduleName.Split(".").Select(IdProtect));
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       moduleName = IdProtectModule(moduleName);
       return wr.NewBlock($"namespace {moduleName}", " // end of " + $"namespace {moduleName}");

Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs

@@ -159,7 +159,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
       return wr.NewBlock($"int main(DafnySequence<DafnySequence<char>> {argsParameterName})");
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       var s = $"namespace {IdProtect(moduleName)} ";
       string footer = "// end of " + s + " declarations";

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -124,7 +124,8 @@ private bool NeedsExternalImport(MemberDecl memberDecl) {
              memberDecl is Function { Body: null } or Method { Body: null };
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       if (currentBuilder is ModuleContainer moduleBuilder) {
         var attributes = (Sequence<DAST.Attribute>)ParseAttributes(moduleAttributes);

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;
@@ -54,6 +55,7 @@ string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
     }
 
     private readonly List<Import> Imports = new(StandardImports);
+    private readonly List<Import> ExtendedImports = new();
     private string ModuleName;
     private ConcreteSyntaxTree RootImportWriter;
     private ConcreteSyntaxTree RootImportDummyWriter;
@@ -105,14 +107,22 @@ private bool IsDafnySequence(TopLevelDecl d) =>
 
     private string DafnySequenceCompanion => $"{HelperModulePrefix}Companion_Sequence_";
 
-    void EmitModuleHeader(ConcreteSyntaxTree wr) {
+    void EmitModuleHeader(ConcreteSyntaxTree wr, ModuleDefinition module) {
       wr.WriteLine("// Package {0}", ModuleName);
       wr.WriteLine("// Dafny module {0} compiled into Go", ModuleName);
       wr.WriteLine();
       wr.WriteLine("package {0}", ModuleName);
       wr.WriteLine();
-      // This is a non-main module; it only imports things declared before it, so we don't need these writers
-      EmitImports(wr, out _, out _);
+      EmitImports(wr, out var importWriter, out var dummyImportWriter);
+
+      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);
+        EmitImport(import, importWriter, dummyImportWriter);
+      }
       wr.WriteLine();
       wr.WriteLine("type {0} struct{{}}", DummyTypeName);
       wr.WriteLine();
@@ -192,7 +202,7 @@ protected override bool ShouldCompileModule(Program program, ModuleDefinition mo
       return true;
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
       ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       if (isDefault) {
@@ -212,7 +222,7 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef
       var import = CreateImport(ModuleName, isDefault, externModule, libraryName);
       var filename = string.Format("{0}/{0}.go", import.Path);
       var w = wr.NewFile(filename);
-      EmitModuleHeader(w);
+      EmitModuleHeader(w, module);
 
       import.Path = goModuleName + import.Path;
       AddImport(import);
@@ -267,7 +277,7 @@ private void AddImport(Import import) {
       // Import in root module
       EmitImport(import, RootImportWriter, RootImportDummyWriter);
       // Import in all subsequent modules
-      Imports.Add(import);
+      ExtendedImports.Add(import);
     }
 
     private void EmitImport(Import import, ConcreteSyntaxTree importWriter, ConcreteSyntaxTree importDummyWriter) {

Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs

@@ -379,7 +379,8 @@ string IdProtectModule(string moduleName) {
       return string.Join(".", moduleName.Split(".").Select(IdProtect));
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       moduleName = IdProtectModule(moduleName);
       if (isDefault) {

Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs

@@ -63,7 +63,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
       return wr.NewBlock($"static Main({argsParameterName})");
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       moduleName = IdProtect(moduleName);
       if (externModule == null || libraryName != null) {

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

@@ -98,7 +98,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
       return mw.NewBlockPy($"def StaticMain({argsParameterName}):");
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       var pythonModuleName = PythonModuleMode ? PythonModuleName + "." : "";
 

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

@@ -187,7 +187,8 @@ protected virtual bool ShouldCompileModule(Program program, ModuleDefinition mod
       return module.ShouldCompile(program.Compilation);
     }
 
-    protected abstract ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected abstract ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr);
     /// <summary>
     /// Indicates the current program depends on the given module without creating it.
@@ -1570,18 +1571,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
 
       DetectAndMarkCapitalizationConflicts(module);
 
-      ModuleDefinition externModule = null;
-      string libraryName = null;
-      if (!Options.DisallowExterns) {
-        var args = Attributes.FindExpressions(module.Attributes, "extern");
-        if (args != null) {
-          if (args.Count == 2) {
-            libraryName = (string)(args[1] as StringLiteralExpr)?.Value;
-          }
-
-          externModule = module;
-        }
-      }
+      var externModule = GetExternalModuleFromModule(module, out var libraryName);
 
       if (!ShouldCompileModule(program, module)) {
         DependOnModule(program, module, externModule, libraryName);
@@ -1590,7 +1580,8 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
 
       Contract.Assert(enclosingModule == null);
       enclosingModule = module;
-      var wr = CreateModule(module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName, module.Attributes, programNode);
+      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) {
         if (!ProgramResolver.ShouldCompile(d)) {
@@ -1714,6 +1705,23 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
       enclosingModule = null;
     }
 
+    protected ModuleDefinition GetExternalModuleFromModule(ModuleDefinition module, out string libraryName) {
+      ModuleDefinition externModule = null;
+      libraryName = null;
+      if (!Options.DisallowExterns) {
+        var args = Attributes.FindExpressions(module.Attributes, "extern");
+        if (args != null) {
+          if (args.Count == 2) {
+            libraryName = (string)(args[1] as StringLiteralExpr)?.Value;
+          }
+
+          externModule = module;
+        }
+      }
+
+      return externModule;
+    }
+
     private void DetectAndMarkCapitalizationConflicts(ModuleDefinition module) {
       foreach (TopLevelDecl d in module.TopLevelDecls) {
         if (d is DatatypeDecl datatypeDecl) {

Source/DafnyCore/Resolver/ModuleResolver.cs

@@ -190,7 +190,7 @@ public ModuleResolutionResult ResolveModuleDeclaration(CompilationData compilati
           alias.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature
         }
       } else if (decl is AbstractModuleDecl abs) {
-        if (ResolveExport(abs, abs.EnclosingModuleDefinition, abs.QId, abs.Exports, out var originalSignature, reporter)) {
+        if (ResolveExport(abs, abs.EnclosingModuleDefinition, abs.TargetQId, abs.Exports, out var originalSignature, reporter)) {
           abs.OriginalSignature = originalSignature;
           abs.Signature = MakeAbstractSignature(originalSignature, abs.FullSanitizedName, abs.Height, signatures);
         } else {
@@ -868,7 +868,7 @@ TopLevelDecl CloneDeclarationForAbstractSignature(VisibilityScope scope, TopLeve
 
       if (d is AbstractModuleDecl abstractDecl) {
         var sig = MakeAbstractSignature(abstractDecl.OriginalSignature, name + "." + abstractDecl.Name, abstractDecl.Height, mods);
-        var result = new AbstractModuleDecl(abstractDecl.Options, abstractDecl.RangeToken, abstractDecl.QId, abstractDecl.NameNode,
+        var result = new AbstractModuleDecl(abstractDecl.Options, abstractDecl.RangeToken, abstractDecl.TargetQId, abstractDecl.NameNode,
           newParent, abstractDecl.Opened, abstractDecl.Exports, Guid.NewGuid()) {
           Signature = sig,
           OriginalSignature = abstractDecl.OriginalSignature