Function application delaboration

Stream: lean4

[Henrik Böving]

As discussed over in the doc-gen4 topic I added the delabConst modifications to my fork here https://github.com/hargonix/lean4/tree/const-delab and it works great for regular function applications like IO Nat. However things like Nat = Nat don't tag the = properly with information, although it does in fact get visited, as evident by a dbg_trace in the delabConst function. @Gabriel Ebner suspected this has to do with the unexpander generated for mixfix notation generated over here https://github.com/hargoniX/lean4/blob/const-delab/src/Lean/Elab/Notation.lean#L46-L66 not carrying the information along so I changed this (according to his suggestions) to:

def mkSimpleDelab (attrKind : Syntax) (vars : Array Syntax) (pat qrhs : Syntax) : OptionT MacroM Syntax := do
  match qrhs with
  | `($c:ident $args*) =>
    let [(c, [])] ← Macro.resolveGlobalName c.getId | failure
    guard <| args.all (Syntax.isIdent ∘ getAntiquotTerm)
    guard <| args.allDiff
    -- replace head constant with (unused) antiquotation so we're not dependent on the exact pretty printing of the head
    `(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident]
      aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun
       | `($$tk:ident $args*) => withRef tk `($pat)
       | _                     => throw ())
  | `($c:ident)        =>
    let [(c, [])] ← Macro.resolveGlobalName c.getId | failure
    `(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident]
      aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun
       | `($$tk:ident) => withRef tk `($pat)
       | _              => throw ())
  | _                  => failure

for me locally and updated stage0, however the Format output still insists that the = is merely an untagged text so the information from delabConst is still going missing like this...so now I don't know where to continue again, would someone happen to have an idea?

[Gabriel Ebner]

Ah, this is because the unexpander monad completely discards syntax references. :-/

-- unexpanders should not need to introduce new names
instance : MonadQuotation UnexpandM where
  getRef              := pure Syntax.missing
  withRef             := fun _ => id
  getCurrMacroScope   := pure 0
  getMainModule       := pure `_fakeMod
  withFreshMacroScope := id

[Gabriel Ebner]

Put an Unhygenic.run do before the withRef and it should work. :smile:

[Henrik Böving]

Hm If I just do it like that (with the corrected typo: Unhygienic.run) and update-stage0 + make Init/Notation.lean complains that unknown constant 'Lean.Unhygienic.run' this is not a known constant, is there some additional macro stuff I have to do when calling things from within the result of a macro? I would've expected that to just work automagically.

[Gabriel Ebner]

Arrh, infix is of course used before Unhygienic is defined... We could move Unhygienic to Init.Prelude.

[Gabriel Ebner]

@Sebastian Ullrich Any preferred solution here?

[Sebastian Ullrich]

We should probably just fix UnexpandM getRef/withRef?

[Henrik Böving]

Sebastian Ullrich said:

We should probably just fix UnexpandM getRef/withRef?

So basically I just turn it into a ReaderT Syntax Id....or rather since the Id Monad isn't defined here yet into a EStateM Syntax Syntax (or alternatively pull Id into Prelude as well?) and adapt the ref funcitons accordingly?

[Sebastian Ullrich]

No, it should be EStateM Unit Syntax

[Henrik Böving]

Alright, I made the changes I think are required over here https://github.com/hargoniX/lean4/commit/e123ea251b7e6d393980141805d0a8282007a466 but I can still not see the = being tagged properly in my Format output :/

[Gabriel Ebner]

withRef             := fun ref m => bind m (fun val _ => EStateM.Result.ok val ref)

withRef is supposed to be a monad combinator. withRef stx k sets the reference to stx while k is running, and then reverts to the original afterwards. This implementation sets the reference to stx after k has already been executed.

[Henrik Böving]

Alright, I changed it over to...more or less literally what you said now https://github.com/hargoniX/lean4/commit/1214d5eff07e42a344e5fcf2f40c626477a68896#diff-52ef0c67eea613acf6c0b6284063fd7112cdd40750de38365c214abaef246db4R2266-R2271 but there was still no change in sight so either I mistinterpreted you quite a lot or something else is still missing.

I also tried to dbg_trace inside the delaborators to get a better grasp what's going on but as before since this is in the Init files dbg_trace does not work here either :(

[Gabriel Ebner]

Your branch works for me:

import Lean open Lean Meta Elab in
#eval show TermElabM _ from do
  let f := mkNumeral (mkConst ``Nat)
  let (stx, infos) ← Lean.PrettyPrinter.delabCore `foo [] (← mkEq (← f 8) (← f 42))
  (stx, infos.toList.map (·.1)) -- adds synthetic position 64 to =, and info is available

[Henrik Böving]

Oh it does indeed show up in the delabCore Syntax output for me as well, but if I look at the format part:

#eval show TermElabM _ from do
  let f := mkNumeral (mkConst ``Nat)
  let (stx, infos) ← Lean.PrettyPrinter.delabCore `foo [] (← mkEq (← f 8) (← f 42))
  let fmt ← PrettyPrinter.formatTerm stx
  (stx, fmt, infos.toList.map (·.1))

fmt will still mark the = as just a regular Std.format.text without a tag regarding the info so apparently formatTerm is still missing out on what's happening?

[Wojciech Nawrocki]

In the stx object I am seeing:

Lean.Syntax.node
   (Lean.SourceInfo.synthetic 1 1)
   `«term_=_»
   #[Lean.Syntax.node (Lean.SourceInfo.synthetic 17 17) `numLit #[Lean.Syntax.atom (Lean.SourceInfo.none) "8"],
     Lean.Syntax.atom (Lean.SourceInfo.none) " = ",
     Lean.Syntax.node (Lean.SourceInfo.synthetic 5 5) `numLit #[Lean.Syntax.atom (Lean.SourceInfo.none) "42"]]

It doesn't seem like there's a synthetic position on the =.

[Henrik Böving]

(Lean.Syntax.node
   (Lean.SourceInfo.synthetic 1 1)
   `«term_=_»
   #[Lean.Syntax.node (Lean.SourceInfo.synthetic 17 17) `numLit #[Lean.Syntax.atom (Lean.SourceInfo.none) "8"],
     Lean.Syntax.atom (Lean.SourceInfo.synthetic 64 64) " = ",
     Lean.Syntax.node (Lean.SourceInfo.synthetic 5 5) `numLit #[Lean.Syntax.atom (Lean.SourceInfo.none) "42"]],

This is the one I'm seeing

[Henrik Böving]

Note that this stx object is being generated with my compiler fork from above.

[Wojciech Nawrocki]

Yep I know, but maybe I do need the stage0 update! On your fork you're still not seeing the tag in the fmt?

[Henrik Böving]

Exactly, this:

#eval show TermElabM _ from do
  let f := mkNumeral (mkConst ``Nat)
  let (stx, infos) ← Lean.PrettyPrinter.delabCore `foo [] (← mkEq (← f 8) (← f 42))
  let fmt ← PrettyPrinter.formatTerm stx
  (stx, fmt, infos.toList.map (·.1)) -- adds synthetic position 64 to =, and info is available

Outputs:

(Lean.Syntax.node
   (Lean.SourceInfo.synthetic 1 1)
   `«term_=_»
   #[Lean.Syntax.node (Lean.SourceInfo.synthetic 17 17) `numLit #[Lean.Syntax.atom (Lean.SourceInfo.none) "8"],
     Lean.Syntax.atom (Lean.SourceInfo.synthetic 64 64) " = ",
     Lean.Syntax.node (Lean.SourceInfo.synthetic 5 5) `numLit #[Lean.Syntax.atom (Lean.SourceInfo.none) "42"]],
 Std.Format.group
   (Std.Format.group
     (Std.Format.nest
       2
       (Std.Format.tag
         1
         (Std.Format.append
           (Std.Format.group
             (Std.Format.nest 2 (Std.Format.tag 17 (Std.Format.text "8")))
             (Std.Format.FlattenBehavior.fill))
           (Std.Format.append
             (Std.Format.text " =")
             (Std.Format.append
               (Std.Format.line)
               (Std.Format.group
                 (Std.Format.nest 2 (Std.Format.tag 5 (Std.Format.text "42")))
                 (Std.Format.FlattenBehavior.fill)))))))
     (Std.Format.FlattenBehavior.fill))
   (Std.Format.FlattenBehavior.fill),
 [1, 5, 17, 64])

[Wojciech Nawrocki]

Ah, it's because it's an atom and we only add tags in the formatter for nodes.

[Henrik Böving]

What change would make sense in this context then? Changing the delaborator so it produces a node here or changing the formatter so it acts on atoms as well? (Or something completely different)

[Gabriel Ebner]

Ah, it's because it's an atom and we only add tags in the formatter for nodes.

That's not the whole story. We only add tags for category parsers. That is, term gets a tag, but ident or " = " don't.

[Wojciech Nawrocki]

idents do, actually -- formatterForKindUnsafe is called! It seems it's just atoms that don't.

[Gabriel Ebner]

That's only true if the ident is parsed through term. For idents that directly occur, the tag is not emitted. For example the binder x in ∀ x, x = x gets a (very wrong!) synthetic position in the syntax tree, but not a tag in the format object:

import Lean open Lean Elab Term Meta

deriving instance Repr for Std.Format.FlattenBehavior
deriving instance Repr for Std.Format

#eval show TermElabM _ from do
  let e ← withLocalDeclD `x (mkConst ``Nat) fun x => do
    mkForallFVars #[x] (← mkEq x x)
  let (stx, infos) ← Lean.PrettyPrinter.delabCore `foo [] e
  let fmt ← PrettyPrinter.formatTerm stx
  (stx, fmt, infos.toList.map (·.1))

[Wojciech Nawrocki]

Oh dear, so that synthetic position is a bug in the delaborator, and then there's still the issue with the formatter missing tags.

[Wojciech Nawrocki]

So @Henrik Böving you could make the formatter add the missing tags by using withMaybeTag here, for example to make sure they are added for symbols (so e.g. = ), the following might do:

  | ParserDescr.symbol tk                           => return do
      let stx ← Syntax.MonadTraverser.getCur
      withMaybeTag (getExprPos? stx) <| symbol.formatter tk

However I am not sure that we do want these tags. In source code hovers 8 = 42 is highlighted as a whole Prop, and the numerals are also hoverable, but the equality sign itself is not. It seems weird to add that, so we may not want to have it in the delaborator either.

In particular when we do add it, it is no longer possible to hover over the top-level expression since now every subspan is tagged: 8, = , and 42.

[Wojciech Nawrocki]

Point in support: mathlib docs make symbols clickable. Point against: when viewed interactively the top-level expression will expand to, for example, Eq.{1} a b and then one can click on Eq.{1}, so no information is lost.

[Henrik Böving]

For doc-gen4 this is exactly what I actually want it to be like so I can linkify the type of a constant (In the environment sense) properly and e..g likn to Eq if you click the =. The alternative would be to link the entire span (which is basically what I'm doing rn) but that also links stuff such as variables etc. that should just not be linked to at all.

If I understood him correctly, the original idea of Gabriel was to just filter the stuff I add now out in the LSP related parts later on so both things could coexist (which I am not 100% sure how to do either since after all they just look like normal tags right?).

[Henrik Böving]

Wojciech Nawrocki said:

Point in support: mathlib docs make symbols clickable. Point against: when viewed interactively the top-level expression will expand to, for example, Eq.{1} a b and then one can click on Eq.{1}, so no information is lost.

Yes this top level expression is exactly what im observing in doc-gen4 right now, however for example for stuff such as custom mixfix notation I have no way of really knowing which parts of the syntax inside of the tagged span actually is from the mixfix notation and which parts are not right? So how would I know what to highlight there? I could of course just put the expression there like for example for the syntax: Γ ⊢ e : τ I could (in the web UI) instead show Typing Γ e τ with Typing linking to the function etc. but that way I have to throw the syntax away. And the alternative I had in mind was that the compiler tags both the turnstyle and the colon here as syntax that points to the Typing function so I could link it that way.

[Henrik Böving]

Maybe we could also have an option/switch that enables/disables these specific tags and is default set to false? So doc-gen just calls format with this enabled and the rest stays as is?

[Gabriel Ebner]

So Henrik Böving you could make the formatter add the missing tags by using withMaybeTag here, for example to make sure they are added for symbols (so e.g. = ), the following might do:

  | ParserDescr.symbol tk                           => return do
      let stx ← Syntax.MonadTraverser.getCur
      withMaybeTag (getExprPos? stx) <| symbol.formatter tk

The withMaybeTag is the right direction, but it needs to be added at symbolNoAntiquot.formatter, then it will also work for non-ParserDescr parsers.

[Wojciech Nawrocki]

Henrik Böving said:

Maybe we could also have an option/switch that enables/disables these specific tags and is default set to false? So doc-gen just calls format with this enabled and the rest stays as is?

This sounds exactly like what I was just going to propose :) So you raise a good point that there are some conflicting requirements. Namely, we wish to use the pretty-printer infrastructure for doc-gen and for widgets because it would be extremely complicated to maintain separate systems, but we sometimes want different information present depending on the target. I think the formatter should ideally be deterministic (i.e.e always tag all the taggable nodes), but we can control the delaborator with pp options. So there could be something like pp.tagSymbols which tells the delaborator to add the info when producing symbol Syntax, or not.

[Henrik Böving]

That definitely does sound reasonable, everyone okay with this variant?

[Henrik Böving]

PR is here: https://github.com/leanprover/lean4/pull/911, tested against both the examples in the chat as well as with my doc-gen4 prototype.

[Henrik Böving]

Aaand test failure :/ let's see, fixed \o/