feat: extract delabAppCore, define withOverApp, and make over-applied projections pretty print
#3083
Conversation
github-actions
bot
added
the
toolchain-available
leanprover-community-mathlib4-bot
added
the
breaks-mathlib
|
leanprover-community-mathlib4-bot
added
builds-mathlib
| @@ -919,6 +919,14 @@ private def getAppNumArgsAux : Expr → Nat → Nat | |||
| def getAppNumArgs (e : Expr) : Nat := | |||
| getAppNumArgsAux e 0 | |||
|
|
|||
| /-- | |||
| If the given expression is a sequence of function applications `f a₁ .. aₙ`, | |||
| returns `f a₁ .. aₖ` where `k` is minimal such that `n - k ≤ maxArgs`. | |||
There was a problem hiding this comment.
Should it be maxRemainingArgs here for clarity?
There was a problem hiding this comment.
I find my comment to be confusing. I want getBoundedAppFn m e to pop off at most m arguments, and I want it to be "dual" to getBoundedAppArgs in the sense that mkAppN (e.getBoundedAppFn m) (e.getBoundedAppArgs m) = e.
Really, the use case is extracting a function of a particular arity, but I found it easier to think about these functions in their current form, where it is up to the caller to decide how many arguments to pop off.
There was a problem hiding this comment.
I tried to clarify the docstring.
| The remaining arguments are processed depending on whether heuristics indicate that the application | ||
| should be delaborated using `@`. | ||
| -/ | ||
| def delabAppCore (maxArgs : Nat) (delabHead : Delab) : Delab := do |
There was a problem hiding this comment.
Are there any delabs in core that should already be using delabAppCore with a specific maxArgs?
There was a problem hiding this comment.
Yeah, many builtin delaborators could use it. One example is delabProjectionApp, which could use it to handle over-application.
My plan was to use delabAppCore to upstream a more general version of Lean.PrettyPrinter.Delaborator.withOverApp and then use this combinator to improve builtins.
There was a problem hiding this comment.
I went ahead and upstreamed the combinator and improved the builtins that could be improved.
By the way, I found a bug in getParamKinds where the default values can refer to temporary fvars rather than be specialized to the supplied arguments. I rewrote the function to be more efficient while fixing this -- I can split those changes into. a separate PR if you want.
Co-authored-by: Sebastian Ullrich <[email protected]>
kmill
force-pushed
the
refactor_delabApp
branch
from
6c851fd to
0573ac1
Compare
kmill
changed the title
delabAppCore for use in delaboratorsdelabAppCore, defines withOverApp, and makes over-applied projections pretty print
Kha
changed the title
delabAppCore, defines withOverApp, and makes over-applied projections pretty printdelabAppCore, define withOverApp, and make over-applied projections pretty print
To handle delaborating notations that are functions that can be applied to arguments, extracts the core function application delaborator as a separate function that accepts the number of arguments to process and a delaborator to apply to the "head" of the expression.
Defines
withOverApp, which has the same interface as the combinator of the same name from std4, but it uses this core function application delaborator.Uses
withOverAppto improve a number of application delaborators, notably projections. This means Mathlib can stop usingpp_dotfor structure fields that have function types.Incidentally fixes
getParamKindsto specialize default values to use supplied arguments, which impacts how default arguments are delaborated.