From d38be4429a5866cd8a77de9be52a217c5d919df6 Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 12 Aug 2024 12:35:39 -0700 Subject: [PATCH] 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`. --- .../DafnyCore/AST/Modules/ModuleDefinition.cs | 29 +++++++++++++++---- Source/DafnyCore/Options/DafnyCommands.cs | 1 + .../Inputs/producer/timesTwo.dfy | 29 ++++++++++++------- .../ConsumerModule/__default.java | 10 +++---- .../usesTimesTwo-oldDafnyCompatability.dfy | 2 +- .../separate-compilation/usesTimesTwo.dfy | 2 +- 6 files changed, 50 insertions(+), 23 deletions(-) diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index f165d89b5f..c7b1b971f8 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/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, IHasSymbolChildren { + + public static readonly Option 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); } diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs index 74acb94d98..d3d3eadbe7 100644 --- a/Source/DafnyCore/Options/DafnyCommands.cs +++ b/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