-
Notifications
You must be signed in to change notification settings - Fork 261
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fix GoLang issue when module and datatype names collide #5824
Fix GoLang issue when module and datatype names collide #5824
Conversation
…rdDrummer/dafny into renameImportsToAvoidNameCollision
@@ -0,0 +1,18 @@ | |||
// NONUNIFORM: this fails on Java |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Interesting, why? Do we need a similar fix in other languages?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I spent a few minutes trying to fix it but couldn't. I already forgot what I noticed but it didn't seem similar.
private readonly List<Import> Imports = new(StandardImports); | ||
private string ModuleName; | ||
private ModuleDefinition CurrentModule; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Never loved the fact that the Go code generator has the extra state of tracking the currently-compiled module, but I won't object to this new state since it's parallel.
But on that note, can ModuleName
just be derived from CurrentModule
so we only have the only field?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
ModuleName
is usually the translated name of a module, but sometimes it's something else:
ModuleName = MainModuleName = program.MainMethod != null ? "main" : TransformToClassName(Path.GetFileNameWithoutExtension(program.Name));
@@ -53,8 +60,10 @@ string FormatDefaultTypeParameterValue(TopLevelDecl tp) { | |||
return $"_default_{tp.GetCompileName(Options)}"; | |||
} | |||
|
|||
private readonly Dictionary<ModuleDefinition, Import> ModuleImports = new(); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we still need Imports
after we have this field?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Renamed it to ImportsNotFromDafnyModules
and updated the behavior accordingly
@@ -1365,6 +1386,9 @@ private ConcreteSyntaxTree CreateSubroutine(string name, List<TypeArgumentInstan | |||
} else if (thisContext != null) { | |||
w = w.NewBlock("", open: BlockStyle.Brace); | |||
for (var i = 0; i < inParams.Count; i++) { | |||
if (inParams[i].IsGhost) { |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This was already fixed in #5815 so you'll probably want to take this out
Description
m_
How has this been tested?
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.