NBE: mantain shape of primops to read them back them properly #3196
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
Fixes FStarLang#3185. In that issue, a primop was encoded to a Lam node with a set of binders of unit type (essentially eta-expanding it), which caused a failure in reading it back. This patch introduces a new shape for an encoded lambda which is a partially applied primop, so reading it back becomes trivial, and does not require an eta.
mtzguido
changed the title
|
Thanks Guido! This resolves the issue for me - I no longer need to eta-expand before running nbe |
|
Thanks for checking! |
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.
Fixes #3185.
In that issue, a primop was encoded to a Lam node with a set of binders
of unit type (essentially eta-expanding it), which caused a failure in
reading it back. This patch introduces a new shape for an encoded lambda
which is a partially applied primop, so reading it back becomes trivial,
and does not require an eta.
cc @amosr , maybe you can give it a spin on the rest of your development?