Why does the fvar delab pretty-print bvars?

Stream: lean4

[Eric Rodriguez]

Here's a MWE:

import Qq
import Lean

namespace Lean.PrettyPrinter.Delaborator
open Meta
open Parser.Term
open SubExpr
open TSyntax.Compat

@[delab fvar]
def delabFVar' : Delab := do
let Expr.fvar fvarId ← getExpr | unreachable!
-- Use internal name - when pp.showFVarIDs is true or when the variable is loose.
maybeAddBlockImplicit <| mkIdent fvarId.name

#check ∀ x : Nat, x = x
--open Qq
-- #eval q(∀ x : Nat, x = x)

delabFVar' is adapted from just the normal delabFVar; it prints the fvarid at all times instead. However, it prints ∀ (x : Nat), _pp_uniq.1 = _pp_uniq.1 : Prop for this forall - even though this x is not an fvar, but a bvar. Is this configurable? I guess it's expected, sadly...

[Kyle Miller]

Yes, that's expected. The forall delab function creates an fvar and instantiates the bvar as it enters its body, in the usual way.

[Eric Rodriguez]

Is the correct way to get around this just to match against _pp_uniq?

[Kyle Miller]

What are you trying to get around?

[Eric Rodriguez]

I want to pretty-print fvars with the _uniq names, but bvars as their actual "proper" name

[Kyle Miller]

Could you help me understand why you're wanting to do this?

[Eric Rodriguez]

I want to output a state with unique names, but this leaves (for example) for alls as forall a, P _pp_uniq... and these clearly don't match up.

[Kyle Miller]

I think I haven't understood your question. Is it that if you override the fvar delaborator, the x in ∀ x doesn't change with it?

[Kyle Miller]

What do you expect the output to be?

[Eric Rodriguez]

Any of ∀ _pp_uniq1, P _pp.uniq1 _uniq.234... or ∀ a, P a _uniq.234... work, with _uniq.234 some actual fvar. Or well, some other name that won't get messed up by shadowing. I can see how to hack to get the second output, but not sure how I'd get that first output.

[Kyle Miller]

Eric Rodriguez said:

but bvars as their actual "proper" name

And what are you calling the proper name of a bvar?

[Eric Rodriguez]

Well, I mean whatever it pretty prints as. I'm not too fussed as long as I can have a consistent name for bvars throughout the expression

[Kyle Miller]

I'm wanting to clarify this because loose bvars are never supposed to appear in what's being pretty printed, and if they do show up, they print as #0, #1, etc. The idea of locally nameless representations is that bvars themselves don't have names at all, other than this de Bruijn index.

The a in ∀ a is not a bvar to be clear.

[Kyle Miller]

This whole time I thought you were wanting bvars in the body to print as #0, #1, etc.

[Kyle Miller]

The default name for a binder is stored inside the forallE and lam expressions. You can transform your Expr to replace all the binders with unique names and then pass that to the pretty printer, if your end goal is having every binder being alpha renamed to be unique.

[Eric Rodriguez]

Oh right, that's the forallE! Makes sense. I'm not super worried about loose bvars - I see the confusion. Thanks, I'll try that solution.