pretty printer bug

Stream: lean4

[Jovan Gerbscheid]

I noticed that when hovering over the + in then following example, it displays the information about f instead of +. This seems to be a general problem when using a binop%.

import Mathlib

variable (f g : Nat → Nat)
#check (f + g) 4

[Kevin Buzzard]

I think this is the same as https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/infoview.20inspects.20term.20for.20only.20one.20frame/near/417649451

[Jovan Gerbscheid]

When there is a coercion involved, then the bug doesn't appear:

variable (f g : Poly Int)
#check (f + g) 4

[Kevin Buzzard]

You might want to continue the discussion at the other thread? Not sure. At the very least someone should check to see if there's already an issue, and then file one and link to the previous thread.

[Kyle Miller]

The fact that a coercion inhibits the bug makes sense.

I'm pretty sure it has to do with the unexpander that the notation/infixl/infixr/... generates for the over-applied case. It doesn't have anything to do with binop% -- instead if you're testing only binary operators they all incidentally have a binop% macro. You can verify this by adding macro_rules | `($x + $y) => `(HAdd.hAdd $x $y) to turn off the binop% elaborator.

I think there are two solutions:
1) Get to the bottom of why the refs for the syntax generated by the unexpander aren't right, and/or
2) Make the app delaborator responsible for overapplication, though that might be at the cost of a bit of quadratic runtime in the unexpanders. (The app delaborator can run app unexpanders with fewer and fewer arguments, if there is an unexpander for that head constant.)

[Jovan Gerbscheid]

I've taken a closer look at the syntax generated by notation, and it turns out that this minimal example is what's going wrong:

import Mathlib.Data.Pi.Algebra
@[app_unexpander HAdd.hAdd]
def unexpand : Lean.PrettyPrinter.Unexpander := fun
  | `(HAdd.hAdd $a $b $c) => do
    let x ← `($a - $b)
    `($x $c)
  | _   => throw ()

variable (f g : Nat → Nat)
#check HAdd.hAdd f g 4

And we can fix it by placing brackets around the x:

import Mathlib.Data.Pi.Algebra
@[app_unexpander HAdd.hAdd]
def unexpand : Lean.PrettyPrinter.Unexpander := fun
  | `(HAdd.hAdd $a $b $c) => do
    let x ← `($a - $b)
    `(($x) $c)
  | _   => throw ()

variable (f g : Nat → Nat)
#check HAdd.hAdd f g 4

[Jovan Gerbscheid]

Note this comment in the definition of the Syntax.node constructor

  (Remark: the `node` constructor did not have an `info` field in previous
  versions. This caused a bug in the interactive widgets, where the popup for
  `a + b` was the same as for `a`. The delaborator used to associate
  subexpressions with pretty-printed syntax by setting the (string) position
  of the first atom/identifier to the (expression) position of the
  subexpression. For example, both `a` and `a + b` have the same first
  identifier, and so their infos got mixed up.) -/
  | node   (info : SourceInfo) (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax

[Jovan Gerbscheid]

I think it would be a natural feature that hovering over the + in (f + g) 4 gives you the information about f + g, so not the full application with the 4 at the end. However, this is impossible using an unexpander, and instead would require a delaborator. This is because the default delaborator will not compute the information for the partially applied f + g, and so the unexpander also doesn't have access to this.

[Jovan Gerbscheid]

In the case of the ⁻¹ notation, if it is overapplied, the hovering works fine, and there are no needed brackets for the over-application. So what I could imagine is that there is a bug in the code that adds brackets to insufficiently bracketed syntax. The bug being that it tries to find hover information for the newly bracketed syntax, even when no such information is available. However I don't know where the code is that adds these brackets.

[Jovan Gerbscheid]

I noticed that in

#check (1 ≤ 2) = True

There is hover information on both 1 ≤ 2 and (1 ≤ 2), which I find a bit weird.
So the problem seems to lie in automatically generated brackets getting too many annotations.
Does anyone have a pointer as to which code is responsible for this?

[Kyle Miller]

By the way, for your original report for (f + g) 4, I have a PR in the works to fix the issue. lean4#3375

[Kyle Miller]

For the term parenthesizer, take a look at docs#Lean.PrettyPrinter.Parenthesizer.term.parenthesizer

[Kyle Miller]

I touched that last. The way it used to work is that the parentheses didn't get any annotation at all, so when you hovered over them it would highlight the expression outside the parentheses.

[Kyle Miller]

Now, you can hover over the parentheses, at the cost of a mild amount of duplication. Maybe if there's some nice way to strip off and transfer position information it might be nicer still.

[Kyle Miller]

Notice that the way it works at the moment is that it copies the position information from the syntax to the parenthesized syntax, without touching the inner syntax.

[Kyle Miller]

Or, rather than touching the parenthesizer, perhaps the Infoview widget code can detect this case and highlight the parentheses too when you hover over the inside since they have the same expr position?

[Jovan Gerbscheid]

When shift-clicking this already sort of happens. Shift-clicking on either the 1 ≤ 2 or (1 ≤ 2) makes the parentheses highlight, but with more transparency than the inner part.