feat(rengine): add KnownApplications resugaring
#1656
Closed
Conversation
This file contains hidden or 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
W95Psp
force-pushed
the
rengine-add-known-apps-resugaring
branch
4 times, most recently
from
dfd1e10 to
87cfd73
Compare
W95Psp
force-pushed
the
rengine-add-known-apps-resugaring
branch
from
87cfd73 to
594348c
Compare
W95Psp
force-pushed
the
rengine-add-known-apps-resugaring
branch
from
6dad272 to
6ba5f6a
Compare
W95Psp
requested review from
clementblaudeau,
keks and
a team
and removed request for
a team
W95Psp
force-pushed
the
rengine-global-id-names
branch
from
a0f860c to
9ddecbe
Compare
W95Psp
force-pushed
the
rengine-add-known-apps-resugaring
branch
from
e3ea02f to
fe7f7a4
Compare
keks
requested changes
Sep 8, 2025
W95Psp
force-pushed
the
rengine-add-known-apps-resugaring
branch
from
dd13dab to
119cd10
Compare
|
Putting this back to draft. |
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 PR introduces a new
KnownApplicationsresugaring.It transforms every
ExprKind::Appnode (representing function applications) into the new variantResugaredExprKind::FunApp.FunAppserves as an enum capturing a list of known function and operator names (e.g., addition, dereference, multiplication, etc.), along with an array of arguments. The arity of each function is encoded in the type system.This resugaring is especially useful for printers.
It also generalizes and replaces the existing
BinOpresugaring. As such, this PR removesBinOpand updates its usage in the Lean backend accordingly.