Two fixes for Paxos simulation

[bugarela]

Hello

This includes 2 changes that make test for Paxos get a ✅ (even though it has no tests, we had failures before):

1. Problem: type aliases no being found in the flattener. Solution: update IRTransformer to transform the types inside the sum type fields. There was also a related problem with printing that was fixed, and tests were updated accordingly.
2. Problem: nested definitions inside assume were not being flattened correctly, because the way we track definitionDepth was not considering assume (or instance overrides, which could also introduce the same issue). Solution: definitionDepth now is also incremented inside top level declarations. It is a bit tricky, and this is used in 4 different visitors, so instead of adding complexity to all of them, I moved handling of definitionDepth to the IRVisitor interface and its walk* functions.

This has the potential to help @shonfeder's work on making sumtypes work in Apalache, since the problem there seems to be related to (1).

• Tests added for any new code
• Documentation added for any new functionality
• Entries added to the respective CHANGELOG.md for any new functionality
• Feature table on README.md updated for any listed functionality

[konnov]

I feel like incrementing and decrementing the depth counter across multiple classes is a bit a fragile solution. Would not it make sense to introduce higher-level methods like init(), enterDef, exitDef?

[konnov]

I think I am a bit lost in the difference between top-level and inner definitions. Would not that code get triggered on both?

[bugarela]

Top-level definitions are declarations, while inner definitions are NOT declarations. This is inside walkDeclaration, so the code would only be called right before walking top level definitions.

[shonfeder]

This fixes the problem on the Apalache side, according to a test I just ran locally. 💃.

[shonfeder]

What does it mean if definitionDepth is undefined here?

[bugarela]

It means that the class (the concrete visitor) doesn't care about definitionDepth (it doesn't define or use it).

[bugarela]

I can't think of a better way to implement the definitionDepth counter, but here are some more drastic changes to consider:

1. Add the depth attribute to QuintDef in the IR and set this while parsing. I know @konnov is, in general, against adding stuff to the IR.
2. Lookup the def in the lookup table whenever we need to know its depth. This might affect performance, and we'd also have to add maps from the definition id to "itself" (the entries in the lookup table include additional metadata such as depth) to the lookup table, in order to effectively .get() it.
3. Include an additional argument to the enter/exitDef and enter/exitExpr which yields the depth - or to all enter/exit functions. This would mean that even the visitors that don't care about the depth would need to be updated with that extra argument on the enter/exit functions it declares.

Do you think any of this two approaches are worth implementing? Or perhaps have a better idea to abstract this?

[shonfeder]

I suggest going with your approach to fix the bugs, as I don't see it adding more complexity. It is just correcting the implementation and if it makes complexity more apparent it is only the complexity that is already required by our approach.

The other approaches you suggest seem worth considering, but we can address those in a followup issue, exploring the trade offs there.

WDYT?

[konnov]

1. Add the depth attribute to QuintDef in the IR and set this while parsing. I know @konnov is, in general, against adding stuff to the IR.

I would like to avoid this one especially. It would be much harder to compose definitions, if we have to keep track of their depth.

[konnov]

2. Lookup the def in the lookup table whenever we need to know its depth. This might affect performance, and we'd also have to add maps from the definition id to "itself" (the entries in the lookup table include additional metadata such as depth) to the lookup table, in order to effectively .get() it.

This is probably the cleanest solution. After all, this is exactly what we need lookup tables for: To get all additional data without computing it ever again.