Skip to content

Commit

Permalink
Fix alternative module reference case
Browse files Browse the repository at this point in the history
  • Loading branch information
keyboardDrummer committed Oct 14, 2024
1 parent 3f4037b commit d913874
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
5 changes: 2 additions & 3 deletions Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs
Original file line number Diff line number Diff line change
Expand Up @@ -1854,10 +1854,10 @@ protected override string TypeName_Companion(Type type, ConcreteSyntaxTree wr, I
// XXX This duplicates some of the logic in UserDefinedTypeName, but if we
// don't do it here, we end up passing the name of the module to
// FormatCompanionName, which doesn't help anyone
if (type is UserDefinedType udt && udt.ResolvedClass != null && IsExternMemberOfExternModule(member, udt.ResolvedClass)) {
if (type is UserDefinedType { ResolvedClass: not null } udt && IsExternMemberOfExternModule(member, udt.ResolvedClass)) {
// omit the default class name ("_default") in extern modules, when the class is used to qualify an extern member
Contract.Assert(!udt.ResolvedClass.EnclosingModuleDefinition.IsDefaultModule); // default module is not marked ":extern"
return IdProtect(udt.ResolvedClass.EnclosingModuleDefinition.GetCompileName(Options));
return IdProtect(ModuleImports[udt.ResolvedClass.EnclosingModuleDefinition].Name);
}
return TypeName_Related(FormatCompanionName, type, wr, tok, member);
}
Expand Down Expand Up @@ -2729,7 +2729,6 @@ 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.TryToAvoidName || this.ModuleName == enclosingModuleDefinitionId) {
return IdName(cl);
} else {
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@
using System.IO;
using System.Diagnostics.Contracts;
using DafnyCore;
using DafnyCore.Options;
using JetBrains.Annotations;
using Microsoft.BaseTypes;
using static Microsoft.Dafny.GeneratorErrors;
Expand Down

0 comments on commit d913874

Please sign in to comment.