feat: push down lets #1111
Closed
feat: push down lets #1111
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
This is in preparation for rethinking how we evaluate let bindings. Signed-off-by: Ben Price <[email protected]>
we do this because we are changing eval a lot shortly, and want to be able to see changes. is also easier to update when bounds are broken!
…ith next commit! This can be seen as an explicit-substitution style operational semantics. This change in approach means that our evaluation rules are much more local, and will enable some future simplifications. In particular we will avoid using the `Accum` machinery, simplify the eval `Cxt` and not have to have a separate eval mode for substitutions. We temporarily disable EvalFull.unit_8. It does pass (note that the step count is bumped), but takes a long time (almost 10 minutes on my machine!). This will be massively improved shortly, by being more aggressive in eliding pointless `let`s. Signed-off-by: Ben Price <[email protected]> pushMulti opt
Signed-off-by: Ben Price <[email protected]>
bump limit on unit_prim_partial_map because... it turns out that on this workload the aggressive elision optimisation actually takes more step. However, the trees are somewhat smaller. this is because the optimisation makes no difference on terms like let x1=_ in ... let xn=_ in xi as `xi` is a leaf. This workload has many such subterms which get created when pushing lets down. Aggressive elision will remove some of the lets early, when they are (for example) let x1=_ in ... let xn=_ in C xi xj but this takes an extra step This phenomenon is also seen in unit_type_preservation_BETA_regression
Since we are eliding aggressively, we may as well not create the pointless lets in the first place. (Note that we may still create pointless lets when renaming binders.) This again noticably speeds up unit_8 and unit_9. Signed-off-by: Ben Price <[email protected]>
This fixes unit_redexes_lettype_capture, where we want to not consider a burried binder renamable. Signed-off-by: Ben Price <[email protected]>
Now we are pushing down lets, we do not need so much information about bindings. In particular, we do not need to record the original binding location, or the original binding's context, since we do not do long-range substitution where care is needed to avoid capture. Signed-off-by: Ben Price <[email protected]>
This fixes a rare issue that if one has two adjacent lets with the same name, we would only record one of them in the `Cxt`, and thus miscalculate whether a binder they immediately contain needs to be renamed before we can push the lets under. Signed-off-by: Ben Price <[email protected]>
This is because we "push down lets", rather than doing long-range substitutions. Signed-off-by: Ben Price <[email protected]>
brprice
force-pushed
the
brprice/explicit-subst
branch
3 times, most recently
from
025ceb9
to
ac6aea5
Compare
|
Ah, I have worked out how to re-open the old PR. Closing this one. Sorry for the noise. FTR, the problem & timeline was
|
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.
This addresses #44
This supersedes #736, which was accidentally closed.