Allow specifying an outer namespace when translating

Source/DafnyCore/AST/Grammar/ProgramParser.cs

@@ -3,6 +3,7 @@
 using System.Diagnostics.Contracts;
 using System.IO;
 using System.Linq;
+using System.Reflection;
 using System.Text;
 using System.Threading;
 using Microsoft.Extensions.Logging;
@@ -157,24 +158,10 @@ private static void AddParseResultToProgram(DfyParseResult parseResult, Program
 
     parseResult.ErrorReporter.CopyDiagnostics(program.Reporter);
 
-    foreach (var declToMove in fileModule.DefaultClasses.Concat(fileModule.SourceDecls)) {
-      declToMove.EnclosingModuleDefinition = defaultModule;
-      if (declToMove is LiteralModuleDecl literalModuleDecl) {
-        literalModuleDecl.ModuleDef.EnclosingModule = defaultModule;
-      }
+    ModuleDefinition sourceModule = fileModule;
+    ModuleDefinition targetModule = defaultModule;
 
-      if (declToMove is ClassLikeDecl { NonNullTypeDecl: { } nonNullTypeDecl }) {
-        nonNullTypeDecl.EnclosingModuleDefinition = defaultModule;
-      }
-      if (declToMove is DefaultClassDecl defaultClassDecl) {
-        foreach (var member in defaultClassDecl.Members) {
-          defaultModule.DefaultClass.Members.Add(member);
-          member.EnclosingClass = defaultModule.DefaultClass;
-        }
-      } else {
-        defaultModule.SourceDecls.Add(declToMove);
-      }
-    }
+    MoveModuleContents(sourceModule, targetModule);
 
     foreach (var include in fileModule.Includes) {
       defaultModule.Includes.Add(include);
@@ -187,6 +174,28 @@ private static void AddParseResultToProgram(DfyParseResult parseResult, Program
     defaultModule.DefaultClass.SetMembersBeforeResolution();
   }
 
+  public static void MoveModuleContents(ModuleDefinition sourceModule, ModuleDefinition targetModule) {
+    foreach (var declToMove in sourceModule.DefaultClasses.Concat(sourceModule.SourceDecls)) {
+      declToMove.EnclosingModuleDefinition = targetModule;
+      if (declToMove is LiteralModuleDecl literalModuleDecl) {
+        literalModuleDecl.ModuleDef.EnclosingModule = targetModule;
+      }
+
+      if (declToMove is ClassLikeDecl { NonNullTypeDecl: { } nonNullTypeDecl }) {
+        nonNullTypeDecl.EnclosingModuleDefinition = targetModule;
+      }
+
+      if (declToMove is DefaultClassDecl defaultClassDecl) {
+        foreach (var member in defaultClassDecl.Members) {
+          targetModule.DefaultClass.Members.Add(member);
+          member.EnclosingClass = targetModule.DefaultClass;
+        }
+      } else {
+        targetModule.SourceDecls.Add(declToMove);
+      }
+    }
+  }
+
   public IList<DfyParseResult> TryParseIncludes(
     IReadOnlyList<DafnyFile> files,
     IEnumerable<Include> roots,

Source/DafnyCore/AST/Modules/DefaultModuleDefinition.cs

@@ -14,12 +14,14 @@ public DefaultModuleDefinition(Cloner cloner, DefaultModuleDefinition original)
 
   public DefaultModuleDefinition(IList<Uri> rootSourceUris)
     : base(RangeToken.NoToken, new Name("_module"), new List<IToken>(), false, false,
-      null, null, null, true) {
+      null, null, null) {
     RootSourceUris = rootSourceUris;
   }
 
   public override bool IsDefaultModule => true;
 
+  public override bool TryToAvoidName => Name == "_module";
+
   public override IEnumerable<INode> Children => Includes.Concat(base.Children);
   public override IEnumerable<INode> PreResolveChildren => Includes.Concat(base.PreResolveChildren);
   public new DefaultModuleDefinition Clone(Cloner cloner) {

Source/DafnyCore/AST/Modules/FileModuleDefinition.cs

@@ -14,7 +14,7 @@ public class FileModuleDefinition : ModuleDefinition {
 
   public FileModuleDefinition(IToken token) :
     base(token.ToRange(), new Name("_module"), new List<IToken>(),
-      false, false, null, null, null, true) {
+      false, false, null, null, null) {
     {
     }
   }

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -14,7 +14,7 @@ public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, IClonea
   public IToken BodyStartTok = Token.NoToken;
   public IToken TokenWithTrailingDocString = Token.NoToken;
   public string DafnyName => NameNode.StartToken.val; // The (not-qualified) name as seen in Dafny source code
-  public readonly Name NameNode; // (Last segment of the) module name
+  public Name NameNode; // (Last segment of the) module name
 
   public override IToken Tok => NameNode.StartToken;
 
@@ -31,7 +31,7 @@ public string FullDafnyName {
   }
   public string FullName {
     get {
-      if (EnclosingModule == null || EnclosingModule.IsDefaultModule) {
+      if (EnclosingModule == null || EnclosingModule.TryToAvoidName) {
         return Name;
       } else {
         return EnclosingModule.FullName + "." + Name;
@@ -47,7 +47,7 @@ public string FullName {
   public bool SuccessfullyResolved;  // set to true upon successful resolution; modules that import an unsuccessfully resolved module are not themselves resolved
   public readonly bool IsAbstract;
   public readonly bool IsFacade; // True iff this module represents a module facade (that is, an abstract interface)
-  private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled.
+  private bool IsBuiltinName => Name is "_System" or "_module"; // true if this is something like _System that shouldn't have it's name mangled.
 
   public DefaultClassDecl DefaultClass { get; set; }
 
@@ -119,11 +119,9 @@ void ObjectInvariant() {
 
   public ModuleDefinition(Cloner cloner, ModuleDefinition original, Name name) : this(cloner, original) {
     NameNode = name;
-    IsBuiltinName = true;
   }
 
   public ModuleDefinition(Cloner cloner, ModuleDefinition original) : base(cloner, original) {
-    IsBuiltinName = original.IsBuiltinName;
     NameNode = original.NameNode;
     PrefixIds = original.PrefixIds.Select(cloner.Tok).ToList();
 
@@ -156,8 +154,7 @@ public ModuleDefinition(Cloner cloner, ModuleDefinition original) : base(cloner,
   }
 
   public ModuleDefinition(RangeToken tok, Name name, List<IToken> prefixIds, bool isAbstract, bool isFacade,
-    ModuleQualifiedId refinementQId, ModuleDefinition parent, Attributes attributes,
-    bool isBuiltinName) : base(tok) {
+    ModuleQualifiedId refinementQId, ModuleDefinition parent, Attributes attributes) : base(tok) {
     Contract.Requires(tok != null);
     Contract.Requires(name != null);
     this.NameNode = name;
@@ -167,7 +164,6 @@ public ModuleDefinition(RangeToken tok, Name name, List<IToken> prefixIds, bool
     this.RefinementQId = refinementQId;
     this.IsAbstract = isAbstract;
     this.IsFacade = isFacade;
-    this.IsBuiltinName = isBuiltinName;
 
     if (Name != "_System") {
       DefaultClass = new DefaultClassDecl(this, new List<MemberDecl>());
@@ -180,8 +176,15 @@ public ModuleDefinition(RangeToken tok, Name name, List<IToken> prefixIds, bool
 
   public virtual bool IsDefaultModule => false;
 
+  public virtual bool TryToAvoidName => false;
+
   private string sanitizedName = null;
 
+  public void ClearNameCache() {
+    sanitizedName = null;
+    compileName = null;
+  }
+
   public string SanitizedName {
     get {
       if (sanitizedName == null) {
@@ -212,7 +215,20 @@ public string GetCompileName(DafnyOptions options) {
       } else if (externArgs != null) {
         compileName = Name + nonExternSuffix;
       } else {
-        compileName = SanitizedName + nonExternSuffix;
+
+        if (IsBuiltinName) {
+          compileName = Name;
+        } else if (EnclosingModule is { TryToAvoidName: false }) {
+          // Include all names in the module tree path, to disambiguate when compiling
+          // a flat list of modules.
+          // Use an "underscore-escaped" character as a module name separator, since
+          // underscores are already used as escape characters in SanitizeName()
+          compileName = EnclosingModule.GetCompileName(options) + options.Backend.ModuleSeparator + NonglobalVariable.SanitizeName(Name);
+        } else {
+          compileName = NonglobalVariable.SanitizeName(Name);
+        }
+
+        compileName += nonExternSuffix;
       }
     }
 
@@ -602,7 +618,7 @@ public void ProcessPrefixNamedModules() {
       var prefixNameModule = prefixNamedModules.First();
       var firstPartToken = prefixNameModule.Parts[0];
       var modDef = new ModuleDefinition(RangeToken.NoToken, new Name(firstPartToken.ToRange(), name), new List<IToken>(), false,
-        false, null, this, null, false);
+        false, null, this, null);
       // Add the new module to the top-level declarations of its parent and then bind its names as usual
 
       // Use an empty cloneId because these are empty module declarations.

Source/DafnyCore/AST/SystemModuleManager.cs

@@ -12,7 +12,7 @@ namespace Microsoft.Dafny;
 public class SystemModuleManager {
   public DafnyOptions Options { get; }
   public readonly ModuleDefinition SystemModule = new(RangeToken.NoToken, new Name("_System"), new List<IToken>(),
-    false, false, null, null, null, true);
+    false, false, null, null, null);
   internal readonly Dictionary<int, ClassDecl> arrayTypeDecls = new();
   public readonly Dictionary<int, ArrowTypeDecl> ArrowTypeDecls = new();
   public readonly Dictionary<int, SubsetTypeDecl> PartialArrowTypeDecls = new();  // same keys as arrowTypeDecl

Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs

@@ -74,7 +74,7 @@ public string GetFullCompileName(DafnyOptions options) {
       }
     }
 
-    return options.Backend.GetCompileName(EnclosingModuleDefinition.IsDefaultModule,
+    return options.Backend.GetCompileName(EnclosingModuleDefinition.TryToAvoidName,
       EnclosingModuleDefinition.GetCompileName(options), GetCompileName(options));
   }
 

Source/DafnyCore/AST/Types/UserDefinedType.cs

@@ -22,7 +22,7 @@ void ObjectInvariant() {
 
   public string FullName {
     get {
-      if (ResolvedClass?.EnclosingModuleDefinition?.IsDefaultModule == false) {
+      if (ResolvedClass?.EnclosingModuleDefinition?.TryToAvoidName == false) {
         return ResolvedClass.EnclosingModuleDefinition.Name + "." + Name;
       } else {
         return Name;
@@ -36,7 +36,7 @@ public string FullName {
   public string GetFullCompanionCompileName(DafnyOptions options) {
     Contract.Requires(ResolvedClass is TraitDecl || (ResolvedClass is NonNullTypeDecl nntd && nntd.Class is TraitDecl));
     var m = ResolvedClass.EnclosingModuleDefinition;
-    var s = m.IsDefaultModule ? "" : m.GetCompileName(options) + ".";
+    var s = m.TryToAvoidName ? "" : m.GetCompileName(options) + ".";
     return s + "_Companion_" + ResolvedClass.GetCompileName(options);
   }
 

Source/DafnyCore/Auditor/AuditReport.cs

@@ -122,7 +122,7 @@ public string RenderMarkdownIETF() {
     StringBuilder text = new StringBuilder();
 
     foreach (var module in modulesWithEntries) {
-      if (module.IsDefaultModule) {
+      if (module.TryToAvoidName) {
         text.AppendLine($"# Default module");
       } else {
         text.AppendLine($"# Module `{module.Name}`");

Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs

@@ -1083,7 +1083,7 @@ void DatatypeFieldsAndConstructor(DatatypeCtor ctor, int constructorIndex, Concr
         if (dt is TupleTypeDecl) {
           nm = "";
         } else {
-          nm = (dt.EnclosingModuleDefinition.IsDefaultModule ? "" : dt.EnclosingModuleDefinition.Name + ".") + dt.Name + "." + ctor.Name;
+          nm = (dt.EnclosingModuleDefinition.TryToAvoidName ? "" : dt.EnclosingModuleDefinition.Name + ".") + dt.Name + "." + ctor.Name;
         }
 
         switch (dt) {
@@ -1166,7 +1166,7 @@ string DtCtorName(DatatypeCtor ctor) {
       Contract.Ensures(Contract.Result<string>() != null);
 
       var dt = ctor.EnclosingDatatype;
-      var dtName = dt.EnclosingModuleDefinition.IsDefaultModule ? IdName(dt) : dt.GetFullCompileName(Options);
+      var dtName = dt.EnclosingModuleDefinition.TryToAvoidName ? IdName(dt) : dt.GetFullCompileName(Options);
       return dt.IsRecordType ? dtName : dtName + "_" + ctor.GetCompileName(Options);
     }
 
@@ -2426,10 +2426,10 @@ private string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null,
       if ((cl is DatatypeDecl)
           && !ignoreInterface
           && (member is null || !NeedsCustomReceiver(member))) {
-        return (cl.EnclosingModuleDefinition.IsDefaultModule ? "" : IdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + DtTypeName(cl, false);
+        return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + DtTypeName(cl, false);
       }
 
-      if (cl.EnclosingModuleDefinition.IsDefaultModule) {
+      if (cl.EnclosingModuleDefinition.TryToAvoidName) {
         return IdProtect(cl.GetCompileName(Options));
       }
 
@@ -3381,7 +3381,7 @@ public override void EmitCallToMain(Method mainMethod, string baseName, Concrete
       var companion = TypeName_Companion(UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(mainMethod.EnclosingClass), wr, mainMethod.tok, mainMethod);
       var wClass = wr.NewNamedBlock("class __CallToMain");
       var wBody = wClass.NewNamedBlock("public static void Main(string[] args)");
-      var modName = mainMethod.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options) == "_module" ? "_module." : "";
+      var modName = mainMethod.EnclosingClass.EnclosingModuleDefinition.TryToAvoidName ? "_module." : "";
       companion = modName + companion;
 
       var idName = IssueCreateStaticMain(mainMethod) ? "_StaticMain" : IdName(mainMethod);

Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs

@@ -4,15 +4,14 @@
 using System.IO;
 using System.Linq;
 using System.Reflection;
-using System.Runtime.Loader;
-using System.Text;
 using System.Text.Json;
 using Microsoft.CodeAnalysis;
 using Microsoft.CodeAnalysis.CSharp;
 
 namespace Microsoft.Dafny.Compilers;
 
 public class CsharpBackend : ExecutableBackend {
+
   protected override SinglePassCompiler CreateCompiler() {
     return new CsharpCompiler(Options, Reporter);
   }

Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs

@@ -85,7 +85,7 @@ public CppCompiler(DafnyOptions options, ErrorReporter reporter, ReadOnlyCollect
     const string DafnySeqClass = "DafnySequence";
     const string DafnyMapClass = "DafnyMap";
 
-    protected override string ModuleSeparator => "::";
+    public override string ModuleSeparator => "::";
     protected override string ClassAccessor => "->";
 
     protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) {

Source/DafnyCore/Compilers/ExecutableBackend.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.ObjectModel;
+using System.Data.SqlTypes;
 using System.Diagnostics;
 using System.Diagnostics.Contracts;
 using System.IO;
@@ -17,39 +18,60 @@ public abstract class ExecutableBackend : IExecutableBackend {
   // May be null for backends that don't use the single-pass compiler logic
   protected SinglePassCompiler compiler;
 
-  protected ExecutableBackend(DafnyOptions options) {
-    Options = options;
+  protected ExecutableBackend(DafnyOptions options) : base(options) {
   }
 
-  public DafnyOptions Options { get; }
-
   public override IReadOnlySet<Feature> UnsupportedFeatures => CreateCompiler().UnsupportedFeatures;
 
   public override bool SupportsDatatypeWrapperErasure =>
     CreateCompiler()?.SupportsDatatypeWrapperErasure ?? base.SupportsDatatypeWrapperErasure;
 
+  public override string ModuleSeparator => Compiler.ModuleSeparator;
+
   public override void Compile(Program dafnyProgram, ConcreteSyntaxTree output) {
-    compiler.Compile(dafnyProgram, output);
+    var outerModules = GetOuterModules();
+    ModuleDefinition rootUserModule = null;
+    foreach (var outerModule in outerModules) {
+      var newRoot = new ModuleDefinition(RangeToken.NoToken, new Name(outerModule), new List<IToken>(), false, false,
+        null, null, null);
+      newRoot.EnclosingModule = rootUserModule;
+      rootUserModule = newRoot;
+    }
+
+    if (rootUserModule != null) {
+      dafnyProgram.DefaultModuleDef.NameNode = rootUserModule.NameNode;
+      dafnyProgram.DefaultModuleDef.EnclosingModule = rootUserModule.EnclosingModule;
+    }
+
+    foreach (var module in dafnyProgram.CompileModules) {
+      module.ClearNameCache();
+    }
+    Compiler.Compile(dafnyProgram, output);
   }
 
-  public override void OnPreCompile(ErrorReporter reporter, ReadOnlyCollection<string> otherFileNames) {
-    base.OnPreCompile(reporter, otherFileNames);
-    compiler = CreateCompiler();
+  SinglePassCompiler Compiler {
+    get {
+      if (compiler == null) {
+        compiler = CreateCompiler();
+      }
+
+      return compiler;
+    }
   }
 
   public override void OnPostCompile() {
     base.OnPostCompile();
-    compiler.Coverage.WriteLegendFile();
+    Compiler.Coverage.WriteLegendFile();
   }
 
   protected abstract SinglePassCompiler CreateCompiler();
 
   public override string PublicIdProtect(string name) {
-    return compiler.PublicIdProtect(name);
+    return Compiler.PublicIdProtect(name);
   }
 
   public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree callToMainTree) {
-    compiler.EmitCallToMain(mainMethod, baseName, callToMainTree);
+    Compiler.EmitCallToMain(mainMethod, baseName, callToMainTree);
   }
 
   public ProcessStartInfo PrepareProcessStartInfo(string programName, IEnumerable<string> args = null) {
@@ -140,11 +162,11 @@ public override bool RunTargetProgram(string dafnyProgramName, string targetProg
   }
 
   public override void InstrumentCompiler(CompilerInstrumenter instrumenter, Program dafnyProgram) {
-    if (compiler == null) {
+    if (Compiler == null) {
       return;
     }
 
-    instrumenter.Instrument(this, compiler, dafnyProgram);
+    instrumenter.Instrument(this, Compiler, dafnyProgram);
   }
 
   protected static void WriteFromFile(string inputFilename, TextWriter outputWriter) {