-
Notifications
You must be signed in to change notification settings - Fork 34
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
Namespacer and ID Refresher #1104
Namespacer and ID Refresher #1104
Conversation
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.
LGTM
@@ -504,6 +285,7 @@ function resolveNamesOrThrow(currentTable: LookupTable, sourceMap: Map<bigint, L | |||
// This should not happen, as the flattening should not introduce any | |||
// errors, since parsePhase3 analysis of the original modules has already | |||
// assured all names are correct. | |||
console.log(moduleToString(module)) |
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.
Is this left-over debugging output, or intended?
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.
A bit of both, I used it for debugging and, since this should never happen (unless I'm modifying the code and break something while doing it), I left it there for my future self.
However, this code is going away when the new flattener comes, so I don't think it is going to be useful again 😅
quint/src/ir/idRefresher.ts
Outdated
* provided IdGenerator. Returns a new QuintDef with the updated IDs. Also | ||
* updates the provided source map and analysis output with copies of the values | ||
* from the old ids to the new ids |
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 don't understand the "copies of the values" part here – what does "values" refer to?
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.
On the source map, the value is the location; on the types map, the value is the type; etc. So if we had a type map like this in the input (inside the analysisOutput
parameter):
{
1n: 'int',
2n: 'foo',
}
and then generated new ids where the component with id 1n
has now id 3n
, the refresher should update the type map so we end up with:
{
1n: 'int',
2n: 'foo',
3n: 'int',
}
That is, the new id 3n
receives a copy of the value in 1n
. This should also happen for the source map, the effects map and the modes map.
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.
Ah, I see! I'd propose to change the last sentence to something like
"Also extends the provided source map and analysis output, such that they contain the respective entries under both their old and new IDs."
quint/src/ir/namespacer.ts
Outdated
* --------------------------------------------------------------------------------- */ | ||
|
||
/** | ||
* Recursive addition of namespaces into all names in IR components. |
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.
Maybe add a sentence here on where/how this is used?
Co-authored-by: Thomas Pani <[email protected]>
…pdate-procedure-extraction
Some tests are breaking because, I realize now, the current flattener expects some weird specific behavior in the namespacer that won't be necessary once the new flattener lands. I'm making a one-line change to fix it for now (along with a comment explaining) and we can roll back when I implement the new flattener. |
Hello
This PR extracts the procedures to add namespaces to definitions and generate new ids for IR components from the flattener. They are also refactored into IR transformers.
I've also moved IR-related files into an
ir
folder, since adding two more files to thesrc
dir didn't seem great, and this is the grouping that made most sense to me. It's safe to ignore the paths in imports and file renaming, and focus on the newly added files.Closes #1098
CHANGELOG.md
for any new functionalityREADME.md
updated for any listed functionality