max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: make binders in #check be hoverable (#7074)

Browse source 
This PR modifies the signature pretty printer to add hover information
for parameters in binders. This makes the binders be consistent with the
hovers in pi types.

Suggested by @david-christiansen
This commit is contained in:
Kyle Miller 2025-02-14 09:28:54 -08:00 • committed by GitHub
parent dd1a4188a0
commit 1babe9fc67
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 24 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/Lean/PrettyPrinter/Delaborator/Builtins.lean
View file

@ -1386,25 +1386,38 @@ where
let e@(.forallE n d e' i) ← getExpr | unreachable!
let n ← if bindingNames.contains n then withFreshMacroScope <| MonadQuotation.addMacroScope n else pure n
let bindingNames := bindingNames.insert n
let stxN := mkIdent n
let curIds := curIds.push ⟨stxN⟩
if shouldGroupWithNext bindingNames e e' then
withBindingBody n <| delabParamsAux bindingNames idStx groups curIds
withBindingBody' n (mkAnnotatedIdent n) fun stxN =>
delabParamsAux bindingNames idStx groups (curIds.push stxN)
else
let group ← withBindingDomain do
/-
`mkGroup` constructs binder syntax for the binder names `curIds : Array Ident`, which all have the same type and binder info.
This being a function is solving the following issue:
- To get the last binder name, we need to be under `withBindingBody'`, which lets us annotate the binder with its fvar.
- However, we should delaborate the binder type from outside `withBindingBody'`.
- Thus, we need to partially construct the binder syntax, waiting on the final value of `curIds`.
-/
let mkGroup : Array Ident → DelabM Syntax ← withBindingDomain do
match i with
| .implicit => `(bracketedBinderF|{$curIds* : $(← delabTy)})
| .strictImplicit => `(bracketedBinderF|⦃$curIds* : $(← delabTy)⦄)
| .instImplicit => `(bracketedBinderF|[$stxN : $(← delabTy)])
| .implicit => let ty ← delabTy; pure fun curIds => `(bracketedBinderF|{$curIds* : $ty})
| .strictImplicit => let ty ← delabTy; pure fun curIds => `(bracketedBinderF|⦃$curIds* : $ty⦄)
| .instImplicit => let ty ← delabTy; pure fun curIds => `(bracketedBinderF|[$(curIds[0]!) : $ty])
| _ =>
if d.isOptParam then
`(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := $(← withAppArg delabTy)))
let ty ← withAppFn <| withAppArg delabTy
let val ← withAppArg delabTy
pure fun curIds => `(bracketedBinderF|($curIds* : $ty := $val))
else if let some (.const tacticDecl _) := d.getAutoParamTactic? then
let ty ← withAppFn <| withAppArg delabTy
let tacticSyntax ← ofExcept <| evalSyntaxConstant (← getEnv) (← getOptions) tacticDecl
`(bracketedBinderF|($curIds* : $(← withAppFn <| withAppArg delabTy) := by $tacticSyntax))
pure fun curIds => `(bracketedBinderF|($curIds* : $ty := by $tacticSyntax))
else
`(bracketedBinderF|($curIds* : $(← delabTy)))
withBindingBody n <| delabParams bindingNames idStx (groups.push group)
let ty ← delabTy
pure fun curIds => `(bracketedBinderF|($curIds* : $ty))
withBindingBody' n (mkAnnotatedIdent n) fun stxN => do
let curIds := curIds.push stxN
let group ← mkGroup curIds
delabParams bindingNames idStx (groups.push group)
/-
Given the forall `e` with body `e'`, determines if the binder from `e'` (if it is a forall) should be grouped with `e`'s binder.
-/