diff --git a/Source/DafnyCore/AST/Grammar/ProgramParser.cs b/Source/DafnyCore/AST/Grammar/ProgramParser.cs index 9f8505659ae..ddd97af636f 100644 --- a/Source/DafnyCore/AST/Grammar/ProgramParser.cs +++ b/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 TryParseIncludes( IReadOnlyList files, IEnumerable roots, diff --git a/Source/DafnyCore/AST/Modules/DefaultModuleDefinition.cs b/Source/DafnyCore/AST/Modules/DefaultModuleDefinition.cs index deee99268ea..5069e5ef3a6 100644 --- a/Source/DafnyCore/AST/Modules/DefaultModuleDefinition.cs +++ b/Source/DafnyCore/AST/Modules/DefaultModuleDefinition.cs @@ -14,12 +14,14 @@ public DefaultModuleDefinition(Cloner cloner, DefaultModuleDefinition original) public DefaultModuleDefinition(IList rootSourceUris) : base(RangeToken.NoToken, new Name("_module"), new List(), 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 Children => Includes.Concat(base.Children); public override IEnumerable PreResolveChildren => Includes.Concat(base.PreResolveChildren); public new DefaultModuleDefinition Clone(Cloner cloner) { diff --git a/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs b/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs index 00c29a9a915..374d1102420 100644 --- a/Source/DafnyCore/AST/Modules/FileModuleDefinition.cs +++ b/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(), - false, false, null, null, null, true) { + false, false, null, null, null) { { } } diff --git a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs b/Source/DafnyCore/AST/Modules/ModuleDefinition.cs index ec51039c152..e5ab45f5425 100644 --- a/Source/DafnyCore/AST/Modules/ModuleDefinition.cs +++ b/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 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 prefixIds, bool this.RefinementQId = refinementQId; this.IsAbstract = isAbstract; this.IsFacade = isFacade; - this.IsBuiltinName = isBuiltinName; if (Name != "_System") { DefaultClass = new DefaultClassDecl(this, new List()); @@ -180,8 +176,15 @@ public ModuleDefinition(RangeToken tok, Name name, List 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(), 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. diff --git a/Source/DafnyCore/AST/SystemModuleManager.cs b/Source/DafnyCore/AST/SystemModuleManager.cs index 737b5efa0c2..cf2632e41c0 100644 --- a/Source/DafnyCore/AST/SystemModuleManager.cs +++ b/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(), - false, false, null, null, null, true); + false, false, null, null, null); internal readonly Dictionary arrayTypeDecls = new(); public readonly Dictionary ArrowTypeDecls = new(); public readonly Dictionary PartialArrowTypeDecls = new(); // same keys as arrowTypeDecl diff --git a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs b/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs index 23919f5ce38..d810ad08b5e 100644 --- a/Source/DafnyCore/AST/TypeDeclarations/TopLevelDecl.cs +++ b/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)); } diff --git a/Source/DafnyCore/AST/Types/UserDefinedType.cs b/Source/DafnyCore/AST/Types/UserDefinedType.cs index 0b198febe58..aeac33a8b8b 100644 --- a/Source/DafnyCore/AST/Types/UserDefinedType.cs +++ b/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); } diff --git a/Source/DafnyCore/Auditor/AuditReport.cs b/Source/DafnyCore/Auditor/AuditReport.cs index 07d1f48985c..046dba58775 100644 --- a/Source/DafnyCore/Auditor/AuditReport.cs +++ b/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}`"); diff --git a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs b/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs index 4d61a1c4446..8b0f18cc80d 100644 --- a/Source/DafnyCore/Compilers/CSharp/Compiler-Csharp.cs +++ b/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() != 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); diff --git a/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs b/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs index 547029299e8..23fd88722f8 100644 --- a/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs +++ b/Source/DafnyCore/Compilers/CSharp/CsharpBackend.cs @@ -4,8 +4,6 @@ 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; @@ -13,6 +11,7 @@ namespace Microsoft.Dafny.Compilers; public class CsharpBackend : ExecutableBackend { + protected override SinglePassCompiler CreateCompiler() { return new CsharpCompiler(Options, Reporter); } diff --git a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs index 7ea11be54b1..1a434c12b7e 100644 --- a/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs +++ b/Source/DafnyCore/Compilers/Cplusplus/Compiler-cpp.cs @@ -85,8 +85,9 @@ public CppCompiler(DafnyOptions options, ErrorReporter reporter, ReadOnlyCollect const string DafnySeqClass = "DafnySequence"; const string DafnyMapClass = "DafnyMap"; - protected override string ModuleSeparator => "::"; - protected override string ClassAccessor => "->"; + public override string ModuleSeparator => "::"; + protected override string StaticClassAccessor => "::"; + protected override string InstanceClassAccessor => "->"; protected override void EmitHeader(Program program, ConcreteSyntaxTree wr) { // This seems to be a good place to check for unsupported options diff --git a/Source/DafnyCore/Compilers/ExecutableBackend.cs b/Source/DafnyCore/Compilers/ExecutableBackend.cs index 4bfda9bc82e..f17cd73b39b 100644 --- a/Source/DafnyCore/Compilers/ExecutableBackend.cs +++ b/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 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(), 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 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 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) { diff --git a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs index 24492bacaab..7ecd76663a2 100644 --- a/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs +++ b/Source/DafnyCore/Compilers/GoLang/Compiler-go.cs @@ -30,6 +30,8 @@ public GoCompiler(DafnyOptions options, ErrorReporter reporter) : base(options, Feature.AllUnderscoreExternalModuleNames }; + public override string ModuleSeparator => "_"; + string FormatDefaultTypeParameterValue(TopLevelDecl tp) { Contract.Requires(tp is TypeParameter || tp is AbstractTypeDecl); return $"_default_{tp.GetCompileName(Options)}"; @@ -876,7 +878,7 @@ string StructOfCtor(DatatypeCtor ctor) { w.WriteLine("case nil: return \"null\""); foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) { var wCase = w.NewNamedBlock("case {0}:", StructOfCtor(ctor)); - var nm = (dt.EnclosingModuleDefinition.IsDefaultModule ? "" : dt.EnclosingModuleDefinition.Name + ".") + dt.Name + "." + ctor.Name; + var nm = (dt.EnclosingModuleDefinition.TryToAvoidName ? "" : dt.EnclosingModuleDefinition.Name + ".") + dt.Name + "." + ctor.Name; if (dt is CoDatatypeDecl) { wCase.WriteLine("return \"{0}\"", nm); } else { @@ -2512,7 +2514,7 @@ private string UserDefinedTypeName(TopLevelDecl cl, bool full, MemberDecl/*?*/ m // Don't use IdName since that'll capitalize, which is unhelpful for // built-in types return qual + (qual == "" ? "" : ".") + cl.GetCompileName(Options); - } else if (!full || cl.EnclosingModuleDefinition.IsDefaultModule || this.ModuleName == cl.EnclosingModuleDefinition.GetCompileName(Options)) { + } else if (!full || cl.EnclosingModuleDefinition.TryToAvoidName || this.ModuleName == cl.EnclosingModuleDefinition.GetCompileName(Options)) { return IdName(cl); } else { return cl.EnclosingModuleDefinition.GetCompileName(Options) + "." + IdName(cl); diff --git a/Source/DafnyCore/Compilers/Java/Compiler-java.cs b/Source/DafnyCore/Compilers/Java/Compiler-java.cs index 00992b1ec40..033147a9d98 100644 --- a/Source/DafnyCore/Compilers/Java/Compiler-java.cs +++ b/Source/DafnyCore/Compilers/Java/Compiler-java.cs @@ -815,7 +815,7 @@ protected string FullTypeName(UserDefinedType udt, MemberDecl member, bool useCo return DafnyTupleClass(tupleDecl.NonGhostDims); } else if (cl is TraitDecl && useCompanionName) { return IdProtect(udt.GetFullCompanionCompileName(Options)); - } else if (cl.EnclosingModuleDefinition.GetCompileName(Options) == ModuleName || cl.EnclosingModuleDefinition.IsDefaultModule) { + } else if (cl.EnclosingModuleDefinition.GetCompileName(Options) == ModuleName || cl.EnclosingModuleDefinition.TryToAvoidName) { return IdProtect(cl.GetCompileName(Options)); } else { return IdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdProtect(cl.GetCompileName(Options)); @@ -2159,7 +2159,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; } if (dt is TupleTypeDecl && ctor.Formals.Count == 0) { // here we want parentheses and no name diff --git a/Source/DafnyCore/Compilers/Java/JavaBackend.cs b/Source/DafnyCore/Compilers/Java/JavaBackend.cs index 68d620e15ad..e067fb442d6 100644 --- a/Source/DafnyCore/Compilers/Java/JavaBackend.cs +++ b/Source/DafnyCore/Compilers/Java/JavaBackend.cs @@ -1,6 +1,7 @@ using System; using System.Collections.Generic; using System.Collections.ObjectModel; +using System.CommandLine; using System.Diagnostics.Contracts; using System.IO; using System.Linq; diff --git a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs b/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs index 2a8205adfa3..0640b60d819 100644 --- a/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs +++ b/Source/DafnyCore/Compilers/JavaScript/Compiler-js.cs @@ -29,6 +29,8 @@ public JavaScriptCompiler(DafnyOptions options, ErrorReporter reporter) : base(o Feature.SeparateCompilation }; + public override string ModuleSeparator => "_"; + const string DafnySetClass = "_dafny.Set"; const string DafnyMultiSetClass = "_dafny.MultiSet"; const string DafnySeqClass = "_dafny.Seq"; @@ -440,7 +442,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete i = 0; foreach (var ctor in dt.Ctors) { var thn = EmitIf(string.Format("this.$tag === {0}", i), true, w); - var nm = (dt.EnclosingModuleDefinition.IsDefaultModule ? "" : dt.EnclosingModuleDefinition.Name + ".") + + var nm = (dt.EnclosingModuleDefinition.TryToAvoidName ? "" : dt.EnclosingModuleDefinition.Name + ".") + dt.Name + "." + ctor.Name; thn.WriteLine("return \"{0}\";", nm); i++; @@ -454,7 +456,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete i = 0; foreach (var ctor in dt.Ctors) { var cw = EmitIf(string.Format("this.$tag === {0}", i), true, w); - var nm = (dt.EnclosingModuleDefinition.IsDefaultModule ? "" : dt.EnclosingModuleDefinition.Name + ".") + + var nm = (dt.EnclosingModuleDefinition.TryToAvoidName ? "" : dt.EnclosingModuleDefinition.Name + ".") + dt.Name + "." + ctor.Name; cw.Write("return \"{0}\"", nm); var sep = " + \"(\" + "; @@ -1565,7 +1567,7 @@ protected override string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ memb } else if (cl is DefaultClassDecl && Attributes.Contains(cl.EnclosingModuleDefinition.Attributes, "extern") && member != null && Attributes.Contains(member.Attributes, "extern")) { // omit the default class name ("_default") in extern modules, when the class is used to qualify an extern member - Contract.Assert(!cl.EnclosingModuleDefinition.IsDefaultModule); // default module is not marked ":extern" + Contract.Assert(!cl.EnclosingModuleDefinition.TryToAvoidName); // default module is not marked ":extern" return IdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options)); } else { return IdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdProtect(cl.GetCompileName(Options)); diff --git a/Source/DafnyCore/Compilers/Python/Compiler-python.cs b/Source/DafnyCore/Compilers/Python/Compiler-python.cs index fd1d360b340..9f628e4a96f 100644 --- a/Source/DafnyCore/Compilers/Python/Compiler-python.cs +++ b/Source/DafnyCore/Compilers/Python/Compiler-python.cs @@ -37,6 +37,8 @@ public PythonCompiler(DafnyOptions options, ErrorReporter reporter) : base(optio Feature.MethodSynthesis }; + public override string ModuleSeparator => "_"; + private const string DafnyRuntimeModule = "_dafny"; private const string DafnyDefaultModule = "module_"; const string DafnySetClass = $"{DafnyRuntimeModule}.Set"; @@ -88,8 +90,7 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, bool isExtern, string libraryName, ConcreteSyntaxTree wr) { moduleName = IdProtect(moduleName); - var modulePath = moduleName.Replace('.', Path.DirectorySeparatorChar); - var file = wr.NewFile($"{modulePath}.py"); + var file = wr.NewFile($"{moduleName}.py"); EmitImports(moduleName, file); return file; } @@ -351,7 +352,7 @@ private void DatatypeFieldsAndConstructor(DatatypeCtor ctor, ConcreteSyntaxTree var dt = ctor.EnclosingDatatype; // Dt.Ctor - var fString = (dt.EnclosingModuleDefinition.IsDefaultModule ? "" : dt.EnclosingModuleDefinition.Name + ".") + + var fString = (dt.EnclosingModuleDefinition.TryToAvoidName ? "" : dt.EnclosingModuleDefinition.Name + ".") + dt.Name + "." + ctor.Name; // {self.Dtor0}, {self.Dtor1}, ..., {self.DtorN} diff --git a/Source/DafnyCore/Compilers/SinglePassCompiler.cs b/Source/DafnyCore/Compilers/SinglePassCompiler.cs index 76236977d09..1bd727a445e 100644 --- a/Source/DafnyCore/Compilers/SinglePassCompiler.cs +++ b/Source/DafnyCore/Compilers/SinglePassCompiler.cs @@ -44,8 +44,9 @@ public abstract class SinglePassCompiler { public virtual bool SupportsDatatypeWrapperErasure => true; public static string DefaultNameMain = "Main"; - protected virtual string ModuleSeparator { get => "."; } - protected virtual string ClassAccessor { get => "."; } + public virtual string ModuleSeparator => "."; + protected virtual string StaticClassAccessor => "."; + protected virtual string InstanceClassAccessor => "."; protected ErrorReporter Reporter; @@ -1386,168 +1387,196 @@ public void Compile(Program program, ConcreteSyntaxTree wrx) { var temp = new List(); OrganizeModules(program, out temp); foreach (var m in temp) { - if (m.IsAbstract) { - // the purpose of an abstract module is to skip compilation - continue; - } + EmitModule(program, wrx, m); + } + EmitFooter(program, wrx); + } - DetectAndMarkCapitalizationConflicts(m); + private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleDefinition module) { + if (module.IsAbstract) { + // the purpose of an abstract module is to skip compilation + return; + } - var moduleIsExtern = false; - string libraryName = null; - if (!Options.DisallowExterns) { - var args = Attributes.FindExpressions(m.Attributes, "extern"); - if (args != null) { - if (args.Count == 2) { - libraryName = (string)(args[1] as StringLiteralExpr)?.Value; - } - moduleIsExtern = true; + DetectAndMarkCapitalizationConflicts(module); + + var moduleIsExtern = false; + 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; } + + moduleIsExtern = true; } - if (!m.ShouldCompile(program.Compilation)) { - DependOnModule(m.GetCompileName(Options), m.IsDefaultModule, moduleIsExtern, libraryName); + } + + if (!module.ShouldCompile(program.Compilation)) { + DependOnModule(module.GetCompileName(Options), module.IsDefaultModule, moduleIsExtern, libraryName); + return; + } + + var wr = CreateModule(module.GetCompileName(Options), module.IsDefaultModule, moduleIsExtern, libraryName, programNode); + var v = new CheckHasNoAssumes_Visitor(this, wr); + Contract.Assert(enclosingModule == null); + enclosingModule = module; + foreach (TopLevelDecl d in module.TopLevelDecls) { + bool compileIt = true; + if (Attributes.ContainsBool(d.Attributes, "compile", ref compileIt) && !compileIt) { continue; } - var wr = CreateModule(m.GetCompileName(Options), m.IsDefaultModule, moduleIsExtern, libraryName, wrx); - var v = new CheckHasNoAssumes_Visitor(this, wr); - Contract.Assert(enclosingModule == null); - enclosingModule = m; - foreach (TopLevelDecl d in m.TopLevelDecls) { - bool compileIt = true; - if (Attributes.ContainsBool(d.Attributes, "compile", ref compileIt) && !compileIt) { - continue; - } - var newLineWriter = wr.Fork(); - if (d is AbstractTypeDecl) { - var at = (AbstractTypeDecl)d; - bool externP = Attributes.Contains(at.Attributes, "extern"); - if (externP) { - var exprs = Attributes.FindExpressions(at.Attributes, "extern"); - Contract.Assert(exprs != null); // because externP is true - if (exprs.Count == 1) { - DeclareExternType(at, exprs[0], wr); - } else { - Error(ErrorId.c_abstract_type_needs_hint, d.tok, "Abstract type ('{0}') with extern attribute requires a compile hint. Expected {{:extern compile_type_hint}}", wr, at.FullName); - } - v.Visit(exprs); - } else { - Error(ErrorId.c_abstract_type_cannot_be_compiled, d.tok, "Abstract type ('{0}') cannot be compiled; perhaps make it a type synonym or use :extern.", wr, at.FullName); - } - } else if (d is TypeSynonymDecl) { - var sst = d as SubsetTypeDecl; - if (sst != null) { - DeclareSubsetType(sst, wr); - v.Visit(sst); - } else { - continue; - } - } else if (d is NewtypeDecl) { - var nt = (NewtypeDecl)d; - var w = DeclareNewtype(nt, wr); - v.Visit(nt); - CompileClassMembers(program, nt, w); - w.Finish(); - } else if ((d as TupleTypeDecl)?.NonGhostDims == 1 && SupportsDatatypeWrapperErasure && Options.Get(CommonOptionBag.OptimizeErasableDatatypeWrapper)) { - // ignore this type declaration - } else if (d is DatatypeDecl) { - var dt = (DatatypeDecl)d; - if (!DeclaredDatatypes.Add((m, dt.GetCompileName(Options)))) { - continue; - } - var w = DeclareDatatype(dt, wr); - if (w != null) { - CompileClassMembers(program, dt, w); - w.Finish(); - } else if (DatatypeDeclarationAndMemberCompilationAreSeparate) { - continue; - } - } else if (d is IteratorDecl) { - var iter = (IteratorDecl)d; - if (Options.ForbidNondeterminism && iter.Outs.Count > 0) { - Error(ErrorId.c_iterators_are_not_deterministic, iter.tok, "since yield parameters are initialized arbitrarily, iterators are forbidden by the --enforce-determinism option", wr); - } - - var wIter = CreateIterator(iter, wr); - if (iter.Body == null) { - Error(ErrorId.c_iterator_has_no_body, iter.tok, "iterator {0} has no body", wIter, iter.FullName); + var newLineWriter = wr.Fork(); + if (d is AbstractTypeDecl) { + var at = (AbstractTypeDecl)d; + bool externP = Attributes.Contains(at.Attributes, "extern"); + if (externP) { + var exprs = Attributes.FindExpressions(at.Attributes, "extern"); + Contract.Assert(exprs != null); // because externP is true + if (exprs.Count == 1) { + DeclareExternType(at, exprs[0], wr); } else { - TrStmtList(iter.Body.Body, wIter); + Error(ErrorId.c_abstract_type_needs_hint, d.tok, + "Abstract type ('{0}') with extern attribute requires a compile hint. Expected {{:extern compile_type_hint}}", + wr, at.FullName); } - } else if (d is TraitDecl trait) { - // writing the trait - var w = CreateTrait(trait.GetCompileName(Options), trait.IsExtern(Options, out _, out _), trait.TypeArgs, trait, trait.ParentTypeInformation.UniqueParentTraits(), trait.tok, wr); - CompileClassMembers(program, trait, w); + v.Visit(exprs); + } else { + Error(ErrorId.c_abstract_type_cannot_be_compiled, d.tok, + "Abstract type ('{0}') cannot be compiled; perhaps make it a type synonym or use :extern.", wr, + at.FullName); + } + } else if (d is TypeSynonymDecl) { + var sst = d as SubsetTypeDecl; + if (sst != null) { + DeclareSubsetType(sst, wr); + v.Visit(sst); + } else { + continue; + } + } else if (d is NewtypeDecl) { + var nt = (NewtypeDecl)d; + var w = DeclareNewtype(nt, wr); + v.Visit(nt); + CompileClassMembers(program, nt, w); + w.Finish(); + } else if ((d as TupleTypeDecl)?.NonGhostDims == 1 && SupportsDatatypeWrapperErasure && + Options.Get(CommonOptionBag.OptimizeErasableDatatypeWrapper)) { + // ignore this type declaration + } else if (d is DatatypeDecl) { + var dt = (DatatypeDecl)d; + + if (!DeclaredDatatypes.Add((module, dt.GetCompileName(Options)))) { + continue; + } + + var w = DeclareDatatype(dt, wr); + if (w != null) { + CompileClassMembers(program, dt, w); w.Finish(); - } else if (d is DefaultClassDecl defaultClassDecl) { - Contract.Assert(defaultClassDecl.InheritedMembers.Count == 0); - Predicate compilationMaterial = x => - !x.IsGhost && (Options.DisallowExterns || !Attributes.Contains(x.Attributes, "extern")); - var include = defaultClassDecl.Members.Exists(compilationMaterial); - var classIsExtern = false; - if (include) { - classIsExtern = - (!Options.DisallowExterns && Attributes.Contains(defaultClassDecl.Attributes, "extern")) || - Attributes.Contains(defaultClassDecl.EnclosingModuleDefinition.Attributes, "extern"); - if (classIsExtern && defaultClassDecl.Members.TrueForAll(member => member.IsGhost || Attributes.Contains(member.Attributes, "extern"))) { - include = false; - } - } - if (include) { - var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), IdName(defaultClassDecl), - classIsExtern, defaultClassDecl.FullName, - defaultClassDecl.TypeArgs, defaultClassDecl, defaultClassDecl.ParentTypeInformation.UniqueParentTraits(), defaultClassDecl.tok, wr); - CompileClassMembers(program, defaultClassDecl, cw); - cw.Finish(); - } else { - // still check that given members satisfy compilation rules - var abyss = new NullClassWriter(); - CompileClassMembers(program, defaultClassDecl, abyss); - } + } else if (DatatypeDeclarationAndMemberCompilationAreSeparate) { + continue; + } + } else if (d is IteratorDecl) { + var iter = (IteratorDecl)d; + if (Options.ForbidNondeterminism && iter.Outs.Count > 0) { + Error(ErrorId.c_iterators_are_not_deterministic, iter.tok, + "since yield parameters are initialized arbitrarily, iterators are forbidden by the --enforce-determinism option", + wr); + } - } else if (d is ClassLikeDecl cl) { - var include = true; - var classIsExtern = false; - if (include) { - classIsExtern = !Options.DisallowExterns && Attributes.Contains(cl.Attributes, "extern"); - if (classIsExtern && cl.Members.TrueForAll(member => member.IsGhost || Attributes.Contains(member.Attributes, "extern"))) { - include = false; - } - } - if (Options.ForbidNondeterminism && - !classIsExtern && - !cl.Members.Exists(member => member is Constructor) && - cl.Members.Exists(member => member is Field && !(member is ConstantField { Rhs: not null }))) { - Error(ErrorId.c_constructorless_class_forbidden, cl.tok, "since fields are initialized arbitrarily, constructor-less classes are forbidden by the --enforce-determinism option", wr); + var wIter = CreateIterator(iter, wr); + if (iter.Body == null) { + Error(ErrorId.c_iterator_has_no_body, iter.tok, "iterator {0} has no body", wIter, iter.FullName); + } else { + TrStmtList(iter.Body.Body, wIter); + } + } else if (d is TraitDecl trait) { + // writing the trait + var w = CreateTrait(trait.GetCompileName(Options), trait.IsExtern(Options, out _, out _), trait.TypeArgs, + trait, trait.ParentTypeInformation.UniqueParentTraits(), trait.tok, wr); + CompileClassMembers(program, trait, w); + w.Finish(); + } else if (d is DefaultClassDecl defaultClassDecl) { + Contract.Assert(defaultClassDecl.InheritedMembers.Count == 0); + Predicate compilationMaterial = x => + !x.IsGhost && (Options.DisallowExterns || !Attributes.Contains(x.Attributes, "extern")); + var include = defaultClassDecl.Members.Exists(compilationMaterial); + var classIsExtern = false; + if (include) { + classIsExtern = + (!Options.DisallowExterns && Attributes.Contains(defaultClassDecl.Attributes, "extern")) || + Attributes.Contains(defaultClassDecl.EnclosingModuleDefinition.Attributes, "extern"); + if (classIsExtern && defaultClassDecl.Members.TrueForAll(member => + member.IsGhost || Attributes.Contains(member.Attributes, "extern"))) { + include = false; } - if (include) { - var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), IdName(cl), classIsExtern, cl.FullName, - cl.TypeArgs, cl, cl.ParentTypeInformation.UniqueParentTraits(), cl.tok, wr); - CompileClassMembers(program, cl, cw); - cw.Finish(); - } else { - // still check that given members satisfy compilation rules - var abyss = new NullClassWriter(); - CompileClassMembers(program, cl, abyss); + } + + if (include) { + var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), + IdName(defaultClassDecl), + classIsExtern, defaultClassDecl.FullName, + defaultClassDecl.TypeArgs, defaultClassDecl, + defaultClassDecl.ParentTypeInformation.UniqueParentTraits(), defaultClassDecl.tok, wr); + CompileClassMembers(program, defaultClassDecl, cw); + cw.Finish(); + } else { + // still check that given members satisfy compilation rules + var abyss = new NullClassWriter(); + CompileClassMembers(program, defaultClassDecl, abyss); + } + } else if (d is ClassLikeDecl cl) { + var include = true; + var classIsExtern = false; + if (include) { + classIsExtern = !Options.DisallowExterns && Attributes.Contains(cl.Attributes, "extern"); + if (classIsExtern && cl.Members.TrueForAll(member => + member.IsGhost || Attributes.Contains(member.Attributes, "extern"))) { + include = false; } - } else if (d is ValuetypeDecl) { - // nop - continue; - } else if (d is ModuleDecl) { - // nop - continue; - } else { Contract.Assert(false); } + } - newLineWriter.WriteLine(); - } + if (Options.ForbidNondeterminism && + !classIsExtern && + !cl.Members.Exists(member => member is Constructor) && + cl.Members.Exists(member => member is Field && !(member is ConstantField { Rhs: not null }))) { + Error(ErrorId.c_constructorless_class_forbidden, cl.tok, + "since fields are initialized arbitrarily, constructor-less classes are forbidden by the --enforce-determinism option", + wr); + } - FinishModule(); + if (include) { + var cw = CreateClass(IdProtect(d.EnclosingModuleDefinition.GetCompileName(Options)), IdName(cl), + classIsExtern, cl.FullName, + cl.TypeArgs, cl, cl.ParentTypeInformation.UniqueParentTraits(), cl.tok, wr); + CompileClassMembers(program, cl, cw); + cw.Finish(); + } else { + // still check that given members satisfy compilation rules + var abyss = new NullClassWriter(); + CompileClassMembers(program, cl, abyss); + } + } else if (d is ValuetypeDecl) { + // nop + continue; + } else if (d is ModuleDecl) { + // nop + continue; + } else { + Contract.Assert(false); + } - Contract.Assert(enclosingModule == m); - enclosingModule = null; + newLineWriter.WriteLine(); } - EmitFooter(program, wrx); + + FinishModule(); + + Contract.Assert(enclosingModule == module); + enclosingModule = null; } private void DetectAndMarkCapitalizationConflicts(ModuleDefinition module) { @@ -2219,7 +2248,7 @@ protected void EmitCallToInheritedConstRHS(ConstantField f, ConcreteSyntaxTree w wr = EmitCoercionIfNecessary(f.Type, fOriginal.Type, f.tok, wr); var calleeReceiverType = UserDefinedType.FromTopLevelDecl(f.tok, f.EnclosingClass).Subst(thisContext.ParentFormalTypeParametersToActuals); - wr.Write("{0}{1}", TypeName_Companion(calleeReceiverType, wr, f.tok, f), ModuleSeparator); + wr.Write("{0}{1}", TypeName_Companion(calleeReceiverType, wr, f.tok, f), StaticClassAccessor); var typeArgs = CombineAllTypeArguments(f, thisContext); EmitNameAndActualTypeArgs(IdName(f), TypeArgumentInstantiation.ToActuals(ForTypeParameters(typeArgs, f, true)), f.tok, wr); wr.Write("("); @@ -2260,7 +2289,7 @@ protected void EmitCallToInheritedFunction(Function f, [CanBeNull] TopLevelDeclW var companionName = CompanionMemberIdName(f); var calleeReceiverType = UserDefinedType.FromTopLevelDecl(f.tok, f.EnclosingClass).Subst(thisContext.ParentFormalTypeParametersToActuals); - wr.Write("{0}{1}", TypeName_Companion(calleeReceiverType, wr, f.tok, f), ModuleSeparator); + wr.Write("{0}{1}", TypeName_Companion(calleeReceiverType, wr, f.tok, f), StaticClassAccessor); var typeArgs = CombineAllTypeArguments(f, thisContext); EmitNameAndActualTypeArgs(companionName, TypeArgumentInstantiation.ToActuals(ForTypeParameters(typeArgs, f, true)), f.tok, wr); wr.Write("("); @@ -2344,7 +2373,7 @@ protected virtual void EmitCallToInheritedMethod(Method method, [CanBeNull] TopL var companionName = CompanionMemberIdName(method); var calleeReceiverType = UserDefinedType.FromTopLevelDecl(method.tok, method.EnclosingClass).Subst(thisContext.ParentFormalTypeParametersToActuals); EmitTypeName_Companion(calleeReceiverType, wr, wr, method.tok, method); - wr.Write(ClassAccessor); + wr.Write(StaticClassAccessor); var typeArgs = CombineAllTypeArguments(method, thisContext); EmitNameAndActualTypeArgs(companionName, TypeArgumentInstantiation.ToActuals(ForTypeParameters(typeArgs, method, true)), method.tok, wr); @@ -4714,10 +4743,10 @@ protected virtual void TrCallStmt(CallStmt s, string receiverReplacement, Concre var protectedName = receiverReplacement == null && customReceiver ? CompanionMemberIdName(s.Method) : IdName(s.Method); if (receiverReplacement != null) { EmitIdentifier(IdProtect(receiverReplacement), wr); - wr.Write(ClassAccessor); + wr.Write(InstanceClassAccessor); } else if (customReceiver) { EmitTypeName_Companion(s.Receiver.Type, wr, wr, s.Tok, s.Method); - wr.Write(ClassAccessor); + wr.Write(StaticClassAccessor); } else if (!s.Method.IsStatic) { wr.Write("("); var wReceiver = wr; @@ -4725,13 +4754,13 @@ protected virtual void TrCallStmt(CallStmt s, string receiverReplacement, Concre wReceiver = EmitCoercionIfNecessary(s.Receiver.Type, UserDefinedType.UpcastToMemberEnclosingType(s.Receiver.Type, s.Method), s.Tok, wr); } EmitExpr(s.Receiver, false, wReceiver, wStmts); - wr.Write($"){ClassAccessor}"); + wr.Write($"){InstanceClassAccessor}"); } else if (s.Method.IsExtern(Options, out var qual, out var compileName) && qual != null) { - wr.Write("{0}{1}", qual, ModuleSeparator); + wr.Write("{0}{1}", qual, StaticClassAccessor); protectedName = compileName; } else { EmitTypeName_Companion(s.Receiver.Type, wr, wr, s.Tok, s.Method); - wr.Write(ModuleSeparator); + wr.Write(StaticClassAccessor); } var typeArgs = CombineAllTypeArguments(s.Method, s.MethodSelect.TypeApplication_AtEnclosingClass, s.MethodSelect.TypeApplication_JustMember); EmitNameAndActualTypeArgs(protectedName, TypeArgumentInstantiation.ToActuals(ForTypeParameters(typeArgs, s.Method, false)), s.Tok, wr); @@ -5840,7 +5869,7 @@ protected virtual void CompileFunctionCallExpr(FunctionCallExpr e, ConcreteSynta if (f.IsExtern(Options, out qual, out compileName) && qual != null) { wr.Write("{0}{1}", qual, ModuleSeparator); } else if (f.IsStatic || customReceiver) { - wr.Write("{0}{1}", TypeName_Companion(e.Receiver.Type, wr, e.tok, f), ModuleSeparator); + wr.Write("{0}{1}", TypeName_Companion(e.Receiver.Type, wr, e.tok, f), StaticClassAccessor); compileName = customReceiver ? CompanionMemberIdName(f) : IdName(f); } else { wr.Write("("); @@ -5849,7 +5878,7 @@ protected virtual void CompileFunctionCallExpr(FunctionCallExpr e, ConcreteSynta wReceiver = EmitCoercionIfNecessary(e.Receiver.Type, UserDefinedType.UpcastToMemberEnclosingType(e.Receiver.Type, f), e.tok, wr); } tr(e.Receiver, wReceiver, inLetExprBody, wStmts); - wr.Write($"){ClassAccessor}"); + wr.Write($"){InstanceClassAccessor}"); compileName = IdName(f); } var typeArgs = CombineAllTypeArguments(f, e.TypeApplication_AtEnclosingClass, e.TypeApplication_JustFunction); diff --git a/Source/DafnyCore/Dafny.atg b/Source/DafnyCore/Dafny.atg index e25883c00bd..5ad19f49b2d 100644 --- a/Source/DafnyCore/Dafny.atg +++ b/Source/DafnyCore/Dafny.atg @@ -1051,8 +1051,7 @@ ModuleDefinition (. SemErr(ErrorId.p_bad_module_decl, t, $"expected either a '{{' or a 'refines' keyword here, found {iderr.val}"); .) ] (. module = new ModuleDefinition(RangeToken.NoToken, name, prefixIds, isAbstract, false, - idRefined == null ? null : new ModuleQualifiedId(idRefined), parent, attrs, - false); + idRefined == null ? null : new ModuleQualifiedId(idRefined), parent, attrs); .) SYNC (. tokenWithTrailingDocString = t; .) "{" (. module.BodyStartTok = t; .) diff --git a/Source/DafnyCore/Options/CommonOptionBag.cs b/Source/DafnyCore/Options/CommonOptionBag.cs index b8a108c0e9c..ccd03594ed0 100644 --- a/Source/DafnyCore/Options/CommonOptionBag.cs +++ b/Source/DafnyCore/Options/CommonOptionBag.cs @@ -3,6 +3,7 @@ using System.IO; using System.Linq; using DafnyCore; +using Microsoft.Dafny.Compilers; namespace Microsoft.Dafny; diff --git a/Source/DafnyCore/Options/DafnyCommands.cs b/Source/DafnyCore/Options/DafnyCommands.cs index e338b6e3edd..9775aa6eeec 100644 --- a/Source/DafnyCore/Options/DafnyCommands.cs +++ b/Source/DafnyCore/Options/DafnyCommands.cs @@ -52,7 +52,7 @@ static DafnyCommands() { CommonOptionBag.OptimizeErasableDatatypeWrapper, CommonOptionBag.TestAssumptions, DeveloperOptionBag.Bootstrapping, - CommonOptionBag.AddCompileSuffix, + CommonOptionBag.AddCompileSuffix }.Concat(VerificationOptions).ToList(); public static IReadOnlyList