Omit empty modules when translating to Go

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -12,6 +12,7 @@
 using System.Diagnostics.Contracts;
 using System.Text.RegularExpressions;
 using DafnyCore;
+using DafnyCore.Options;
 using JetBrains.Annotations;
 using Tomlyn.Model;
 using static Microsoft.Dafny.ConcreteSyntaxTreeUtils;
@@ -179,6 +180,18 @@ private Import CreateImport(string moduleName, bool isDefault, ModuleDefinition
       return new Import { Name = moduleName, Path = pkgName, ExternModule = externModule };
     }
 
+    protected override bool ShouldCompileModule(Program program, ModuleDefinition module) {
+      if (!base.ShouldCompileModule(program, module)) {
+        return false;
+      }
+
+      if (TranslationRecord.ModuleEmptyForCompilation(module)) {
+        return false;
+      }
+
+      return true;
+    }
+
     protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault,
       ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
@@ -209,6 +222,11 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef
 
     protected override void DependOnModule(Program program, ModuleDefinition module, ModuleDefinition externModule,
       string libraryName) {
+
+      if (externModule == null && TranslationRecord.ModuleEmptyForCompilation(module)) {
+        return;
+      }
+
       var goModuleName = "";
       if (GoModuleMode) {
         // "_System" module has a special handling because although it gets translated from a Dafny module,

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

@@ -182,6 +182,11 @@ protected void CheckSystemModulePopulatedToCommonLimits(SystemModuleManager syst
     /// call to the instance Main method in the enclosing class.
     /// </summary>
     protected abstract ConcreteSyntaxTree CreateStaticMain(IClassWriter wr, string argsParameterName);
+
+    protected virtual bool ShouldCompileModule(Program program, ModuleDefinition module) {
+      return module.ShouldCompile(program.Compilation);
+    }
+
     protected abstract ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr);
     /// <summary>
@@ -1578,7 +1583,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
         }
       }
 
-      if (!module.ShouldCompile(program.Compilation)) {
+      if (!ShouldCompileModule(program, module)) {
         DependOnModule(program, module, externModule, libraryName);
         return;
       }

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/GoEmptyParentModules.dfy

@@ -0,0 +1,10 @@
+// RUN: %baredafny translate go %args %s
+// RUN: %OutputCheck --file-to-check %S/GoEmptyParentModules-go/src/GoEmptyParentModules.go "%s"
+// CHECK-NOT: "A"
+// CHECK-NOT: "A_B"
+
+module A.B.C {
+  method Main() {
+    print "Hi there!\n";
+  }
+}