feat: Legacy module names option (#5679)

### Description
Similar to the previously added `--legacy-data-constructors` option,
`--legacy-module-names` outputs module names in the scheme `A_mB_mC`, as
previous versions of Dafny did, instead of `A.B.C`, in the name of
backwards compatibility with other Dafny-generated consumers.

### How has this been tested?
Updated
`comp/separate-compilation/usesTimesTwo-oldDafnyCompatibility.dfy` to
use a nested library module name, and therefore test both
`--legacy-data-constructors` and `--legacy-module-names`.

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -1,8 +1,11 @@
 using System;
 using System.Collections.Generic;
 using System.Collections.Immutable;
+using System.CommandLine;
 using System.Diagnostics.Contracts;
 using System.Linq;
+using DafnyCore;
+using DafnyCore.Options;
 using Microsoft.Dafny.Auditor;
 using Microsoft.Dafny.Compilers;
 using OmniSharp.Extensions.LanguageServer.Protocol.Models;
@@ -25,6 +28,18 @@ public enum ImplementationKind {
 public record Implements(ImplementationKind Kind, ModuleQualifiedId Target);
 
 public class ModuleDefinition : RangeNode, IAttributeBearingDeclaration, ICloneable<ModuleDefinition>, IHasSymbolChildren {
+
+  public static readonly Option<bool> LegacyModuleNames = new("--legacy-module-names",
+    @"
+Generate module names in the older A_mB_mC style instead of the current A.B.C scheme".TrimStart()) {
+    IsHidden = true
+  };
+
+  static ModuleDefinition() {
+    DafnyOptions.RegisterLegacyUi(LegacyModuleNames, DafnyOptions.ParseBoolean, "Compilation options", legacyName: "legacyModuleNames", defaultValue: false);
+    OptionRegistry.RegisterOption(LegacyModuleNames, OptionScope.Translation);
+  }
+
   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
@@ -215,11 +230,15 @@ public string GetCompileName(DafnyOptions options) {
       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);
+        if (options.Get(LegacyModuleNames)) {
+          compileName = SanitizedName;
+        } else {
+          // 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);
       }

Source/DafnyCore/Options/DafnyCommands.cs

@@ -58,6 +58,7 @@ static DafnyCommands() {
     CommonOptionBag.AddCompileSuffix,
     CommonOptionBag.SystemModule,
     IExecutableBackend.TranslationRecords,
+    ModuleDefinition.LegacyModuleNames
   }.Concat(VerificationOptions).ToList();
 
   public static readonly IReadOnlyList<Option> ExecutionOptions = new Option[] {

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/Inputs/producer/timesTwo.dfy

@@ -1,18 +1,25 @@
-module {:options "--function-syntax:4"} LibraryModule {
+module {:options "--function-syntax:4"} CoolLibraryName {
 
-  function TimesTwo(x: nat): nat
-  {
-    x * 2
-  }
+  // Ensuring this module is not empty,
+  // or else it will be omitted from the translation record.
+  const FOO := 42
+
+  module LibraryModule {
 
-  datatype Result<+T, +E> = Success(value: T) | Failure(error: E)
+    function TimesTwo(x: nat): nat
+    {
+      x * 2
+    }
 
-  // Record type
-  datatype Pair<+T, +U> = Pair(first: T, second: U)
+    datatype Result<+T, +E> = Success(value: T) | Failure(error: E)
 
-  datatype NestedTypeConstructorRecord<+T> = First(value: Pair<T, T>)
-  datatype NestedTypeConstructorClass<+T> = First2(value: Pair<T, T>) | Second2(value: Pair<T, T>)
+    // Record type
+    datatype Pair<+T, +U> = Pair(first: T, second: U)
 
-  datatype NoTypeArgs = Success2 | Failure2
+    datatype NestedTypeConstructorRecord<+T> = First(value: Pair<T, T>)
+    datatype NestedTypeConstructorClass<+T> = First2(value: Pair<T, T>) | Second2(value: Pair<T, T>)
 
+    datatype NoTypeArgs = Success2 | Failure2
+
+  }
 }

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/fromDafny42/usesTimesTwo-java/ConsumerModule/__default.java

@@ -12,7 +12,7 @@ public static void Main(dafny.DafnySequence<? extends dafny.DafnySequence<? exte
     java.math.BigInteger _0_n = java.math.BigInteger.ZERO;
     _0_n = java.math.BigInteger.valueOf(21L);
     java.math.BigInteger _1_TwoN = java.math.BigInteger.ZERO;
-    _1_TwoN = LibraryModule.__default.TimesTwo(_0_n);
+    _1_TwoN = CoolLibraryName_mLibraryModule.__default.TimesTwo(_0_n);
     System.out.print((dafny.DafnySequence.asUnicodeString("Two times ")).verbatimString());
     System.out.print(java.lang.String.valueOf(_0_n));
     System.out.print((dafny.DafnySequence.asUnicodeString(" is ")).verbatimString());
@@ -46,13 +46,13 @@ public static <__T> __T PickSomething(dafny.TypeDescriptor<__T> _td___T)
   }
   public static void MakeAResult()
   {
-    LibraryModule.Result<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>> _3_r;
-    _3_r = LibraryModule.Result.<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>>create_Success(java.math.BigInteger.valueOf(42L));
+    CoolLibraryName_mLibraryModule.Result<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>> _3_r;
+    _3_r = CoolLibraryName_mLibraryModule.Result.<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>>create_Success(java.math.BigInteger.valueOf(42L));
   }
   public static void MakeAPair()
   {
-    LibraryModule.Pair<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>> _4_p;
-    _4_p = LibraryModule.Pair.<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>>create(java.math.BigInteger.ONE, dafny.DafnySequence.asUnicodeString("partridge in a pair tree"));
+    CoolLibraryName_mLibraryModule.Pair<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>> _4_p;
+    _4_p = CoolLibraryName_mLibraryModule.Pair.<java.math.BigInteger, dafny.DafnySequence<? extends dafny.CodePoint>>create(java.math.BigInteger.ONE, dafny.DafnySequence.asUnicodeString("partridge in a pair tree"));
   }
   @Override
   public java.lang.String toString() {

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo-oldDafnyCompatability.dfy

@@ -5,7 +5,7 @@
 
 // Java
 
-// RUN: %baredafny translate java --output=%S/Inputs/producer/timesTwo %S/Inputs/producer/timesTwo.dfy --legacy-data-constructors
+// RUN: %baredafny translate java --output=%S/Inputs/producer/timesTwo %S/Inputs/producer/timesTwo.dfy --legacy-data-constructors --legacy-module-names
 // RUN: javac -cp %binaryDir/DafnyRuntime.jar%{pathsep}%S/Inputs/producer/timesTwo-java %S/Inputs/producer/timesTwo-java/**/*.java
 
 // Already run using Dafny 4.2: %baredafny translate java --output=%S/fromDafny42/usesTimesTwo --allow-warnings --library=%S/Inputs/producer/timesTwo.dfy %S/usesTimesTwo.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/separate-compilation/usesTimesTwo.dfy

@@ -49,7 +49,7 @@ include "Inputs/producer/timesTwo.dfy"
 
 module ConsumerModule {
 
-  import opened LibraryModule
+  import opened CoolLibraryName.LibraryModule
 
   method Main() {
     var n := 21;