Signature pretty printer

[Kha]

In hover text etc., we should not naively print the signature as a term to the right of the colon : but move parameters to the left of it, ensuring that parameter names are printed and that we can use special syntax for opt/autoParams.

[Kha]

This is even more important after #941. Instead of

@Option.none.{?u.1345} : {α : Type ?u.1345} → Option α

we really should be printing

Option.none.{u} {α : Type u} : Option α

[AdrienChampion]

@Kha I would be interested in giving this a try. As discussed on Zulip, it seems relatively reasonable for my first issue. I'll start looking into it but I'll take any advice on where to start looking, the relevant modules and types etc.

[Kha]

@Vtec234 We probably want to make sure that the output is still usable as an interactive message for widgets, correct? That is, even if the LSP hover is currently non-interactive, if we use the signature pretty printer in e.g. #check, we would expect to be able to inspect any nested terms, in either parameters or the result type. So the output Option.none.{u} {α : Type u} : Option α should be represented by a MessageData values roughly as follows

MessageData.withContext ... <|  -- save environment
  MessageData.ofFormat f!"Option.none.{u} {α : " ++  -- insert more formatting structure here... do we want metadata on `α` as well?
  MessageData.ofExpr `(Type u) ++  -- pretend this is an `Expr` quotation
  MessageData.ofFormat f!"} : " ++
  MessageData.withContext ... <|  -- add `α` to lctx
    MessageData.ofExpr `(Option α)

Additional parameters would introduce additional contexts.

[Vtec234]

That would be one way to do it, but maybe we just want to change the delaborator, perhaps adding a config option to select the current/new behaviour? As long as delabCore here produces the right Syntax and the correct map of Elab.Infos, I think we need not worry about how it gets turned into MessagaData later.

[Kha]

A signature is not a valid term syntax, so this can't be part of the delaborator unconditionally. In theory, we could introduce a purely internal delaborator option for formatting a function type as a signature suffix and then apply that option to the root when build a signature message. But I don't think we can currently embed OptionsPerPos into Message for that.

[Kha]

OTOH, I'm not even sure we want to use the signature printer on #check none since #check takes terms in general, not single idents. So this might be a mostly theoretical issue at this point if we only want to use it in the LSP hover.

[gebner]

A signature is not a valid term syntax

But it can be valid syntax in another (adhoc) category. This is certainly not the only case where we want to embed non-term syntax in messages but which should still be interactive. E.g. tactics, commands, etc. #print could also benefit from better declaration signature printing.

We need to add an extra constructor for MessageData to record the Elab.Info for the syntax tree though.

[Vtec234]

We need to add an extra constructor for MessageData to record the Elab.Info for the syntax tree though.

It's been a while since I looked at this so maybe I am missing something, but it isn't clear to me why we'd want this in the current setup, or the theoretical one in which the delaborator is changed. MessageData is already able to include expressions, goals and syntax objects. Are you proposing some sort of unification of the two types?

[gebner]

It's been a while since I looked at this so maybe I am missing something, but it isn't clear to me why we'd want this in the current setup, or the theoretical one in which the delaborator is changed.

I think I misunderstood you then. Apparently you're proposing a pp.printAsSignature option that prints constants as signatures? This would indeed work for signatures, but it doesn't scale to other syntax categories like tactics (for which we want interactivity and reuse the syntax formatter). It also feels a bit hacky to add non-roundtripping delaborators.

MessageData is already able to include expressions, goals and syntax objects. Are you proposing some sort of unification of the two types?

Not necessarily unification. The separate expression constructor is still useful for performance reasons since it delays delaboration and formatting until display time.

But it would be a useful addition to store the Elab.Info objects in MessageData.ofSyntax to allow for interactive syntax that is not expressions or goals.

But I don't think we can currently embed OptionsPerPos into Message for that.

You can embed them into expressions using the Expr.mdata constructor.

[Kha]

@gebner So if I understood you correctly, you're not necessarily talking about extending the current delaborator (which, as a transformation from Expr to Syntax can't be readily generalized to other categories), but only MessageData for interactivity with arbitrary syntax categories. Then we implement a separate "signature delaborator" (that should not need to be extensible) like delabSignature (decl : Name) (ls: List Level) (type : Expr) : MetaM (Syntax × RBMap Pos Info) and embed this result into a message using the extended ofSyntax constructor.

The separate expression constructor is still useful for performance reasons since it delays delaboration and formatting until display time.

We could add an explicit constructor for laziness. But it looks like this would not let us get rid of ofExpr as it is used in e.g. MessageData.hasSyntheticSorry as well. And there is some special casing of exprs/goals in msgToInteractive where I honestly can't tell if it could be generalized to Syntax × Infos, though I would hope so.

[gebner]

So if I understood you correctly, you're not necessarily talking about extending the current delaborator (which, as a transformation from Expr to Syntax can't be readily generalized to other categories), but only MessageData for interactivity with arbitrary syntax categories. Then we implement a separate "signature delaborator" (that should not need to be extensible) like delabSignature (decl : Name) (ls: List Level) (type : Expr) : MetaM (Syntax × RBMap Pos Info) and embed this result into a message using the extended ofSyntax constructor.

Yes, that was my proposal. Ideally the type would be delabSignature (decl : Name) (ls : List Level) (type : Expr) : BikeshedM Syntax for composability though.

The separate expression constructor is still useful for performance reasons since it delays delaboration and formatting until display time.

We could add an explicit constructor for laziness. But it looks like this would not let us get rid of ofExpr as it is used in e.g. MessageData.hasSyntheticSorry as well.

Wojciech just brought up exactly the same suggestion of adding a lazy constructor. This lazy constructor could have a hasSyntheticSorry field.

And there is some special casing of exprs/goals in msgToInteractive where I honestly can't tell if it could be generalized to Syntax × Infos, though I would hope so.

I think msgToInteractive in its current state generalizes easy. There is a TODO there to use InteractiveGoal for the goals, which would reuse the goal component from the infoview. That would not be covered by ofLazy (ofSyntax).