Rewrite applied LET/INs in the builder
#2536
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
added 4 commits
April 14, 2023 16:09
Following #2534, but putting it where it'll help with quint conversion.
Now being delegated to the builder.
This reverts commit 9d5a00a. This can't be useful as is, because any input will choke on the type checker before we ever get to the preprocessing logic. The previous commits move the core logic into the builder, where it fixes the problem hit during conversion.
Codecov Report
@@ Coverage Diff @@
## main #2536 +/- ##
==========================================
- Coverage 78.54% 78.50% -0.05%
==========================================
Files 442 441 -1
Lines 15560 15535 -25
Branches 2518 2507 -11
==========================================
- Hits 12221 12195 -26
- Misses 3339 3340 +1
... and 4 files with indirect coverage changes 📣 We’re building smart automated test selection to slash your CI/CD build times. Learn more |
shonfeder
pushed a commit
to informalsystems/quint
that referenced
this pull request
Apr 14, 2023
This will be passing once informalsystems/apalache#2536 is merged.
Kukovec
reviewed
Apr 17, 2023
Comment on lines
+25
to
+35
| def appOp(Op: TlaEx, args: TlaEx*): TlaEx = { | ||
| Op match { | ||
| // This is a workaround for the fact that that we currently de-lambda, | ||
| // because lambdas are not supported in the Apalache IR. See | ||
| // https://github.com/informalsystems/apalache/issues/2532 | ||
| case LetInEx(nameEx @ NameEx(operName), decl) if operName == decl.name => | ||
| val appliedByName = buildBySignatureLookup(TlaOper.apply, nameEx +: args: _*) | ||
| LetInEx(appliedByName, decl)(appliedByName.typeTag) | ||
| case _ => buildBySignatureLookup(TlaOper.apply, Op +: args: _*) | ||
| } | ||
| } |
There was a problem hiding this comment.
I'm not sure I like us pushing computations, which have nothing to do with building expression trees, but rather compensate for a particular deficiency in our rewriting process, into the Builder itself.
There was a problem hiding this comment.
Thanks for the review and discussion!
To note the upshot of our convo:
- We identified that, in principle, to hold to the logic of TLA, we should not allow returning operator. So, in principle, the
LET/INform used to encode lambdas shouldn't even be allowed. - However, we have inherited a situation in which this otherwise illegal form is used internally to represent lambdas.
- Since we should be able to apply lambdas, it makes sense given our current imperfect state to support this construction in the builder.
- The key caveat is that this should be removed (and replaced with a validation check) once we introduce lambdas via Support
LAMBDAin the Apalache IR #2532.
Kukovec
approved these changes
Apr 17, 2023
shonfeder
pushed a commit
to informalsystems/quint
that referenced
this pull request
Apr 17, 2023
This will be passing once informalsystems/apalache#2536 is merged.
shonfeder
pushed a commit
to informalsystems/quint
that referenced
this pull request
Apr 17, 2023
This will be passing once informalsystems/apalache#2536 is merged.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Closes #2531
Borrows from and reverts #2534. See c59ed3d and
#2534 (comment)
for context.
This provides a workaround for #2532, by rewriting
(LET f = ... IN f)(x)as(LET f = ... IN f(x)).make fmt-fix(or had formatting run automatically on all files edited)./unreleased/for any new functionality