Pretty-print mvars without `.1234`?

Stream: mathlib4

[Thomas Murrills]

I'm writing some tests in which I want to ensure that the "don't know how to synthesize implicit argument ..." error gets printed via #guard_msgs, but these inevitably involve anonymous mvars (like ?m.1234), and so would potentially be rather fragile.

Is there an option somewhere for pretty-printing these mvars without the trailing fragile number? (Or should #guard_msgs strip these numbers by default, like the lean core test output checker does?)

[Kyle Miller]

I've been thinking about making #guard_msgs have some sort of way to specify holes in the text, like maybe with #guard_msgs (hole := "XXX") in ... then you can put XXX in the text, and these match one or more characters.

[Kyle Miller]

You should be able to make a mvar pretty printer that strips the number off. You could copy Lean.PrettyPrinter.Delaborator.delabMVar and then adjust n afterwards, replacing a .num component with .str ... "NNN" or something like that.

[Thomas Murrills]

Kyle Miller said:

I've been thinking about making #guard_msgs have some sort of way to specify holes in the text, like maybe with #guard_msgs (hole := "XXX") in ... then you can put XXX in the text, and these match one or more characters.

That sounds neat! I wonder if it would also be worth having an "automatic" version which just renumbered the holes inside #guard_msgs, so that the first-encountered?m.NNN became ?m.1 wherever it occurred, the next became ?m.2, etc.

[Thomas Murrills]

Btw, I found I also needed to override the delaborator for Expr.sort to handle level mvars there. Unfortunately handling level mvars in constants would (I think) require a lot of copypasta, since it relies on delabConst, which isn't actually a delaborator for .const. (Luckily this typically doesn't matter and isn't printed.)

[Thomas Murrills]

For anyone that might find this useful in the future, here's the (first draft of the) code:

code

import Lean

namespace Lean.Level

namespace PP

def toResultNoSuffix : Level → Result
  | .zero       => Result.num 0
  | .succ l     => Result.succ (toResult l)
  | .max l₁ l₂  => Result.max (toResult l₁) (toResult l₂)
  | .imax l₁ l₂ => Result.imax (toResult l₁) (toResult l₂)
  | .param n    => Result.leaf n
  | .mvar _     => Result.leaf (Name.mkSimple "?u")

end PP

def quoteNoSuffix (u : Level) (prec : Nat := 0) : Syntax.Level :=
  (PP.toResultNoSuffix u).quote prec

end Lean.Level

namespace Lean.PrettyPrinter.Delaborator

open SubExpr

@[delab sort]
def delabSortNoLevelSuffix : Delab := do
  let Expr.sort l ← getExpr | unreachable!
  match l with
  | Level.zero => `(Prop)
  | Level.succ .zero => `(Type)
  | _ => match l.dec with
    | some l' => `(Type $(Level.quoteNoSuffix l' max_prec))
    | none    => `(Sort $(Level.quoteNoSuffix l max_prec))

@[delab mvar]
def delabMVarNoSuffix : Delab := do
  let Expr.mvar n ← getExpr | unreachable!
  let mvarDecl ← n.getDecl
  let n := eraseSuffix mvarDecl.userName
  `(?$(mkIdent n))
where
  eraseSuffix : Name → Name
  | Name.anonymous => `m
  | .num n _ => eraseSuffix n
  | n => n

(I might put this—or a scoped version?—in some Mathlib.Util file (?) in an upcoming PR that could use it for those tests.)

[Mario Carneiro]

Thomas Murrills said:

That sounds neat! I wonder if it would also be worth having an "automatic" version which just renumbered the holes inside #guard_msgs, so that the first-encountered?m.NNN became ?m.1 wherever it occurred, the next became ?m.2, etc.

I've been wanting to just have the pretty printer do that all the time. This is how lean 3 worked and it is infinitely easier to read than all those big (and changing) numbers

[Mario Carneiro]

In mm0 I did that but with "alphabetic numbering" i.e. ?a, ?b, ..., ?z, ?aa, ... which I think is a bit more mnemonic, but possibly this would be confusing in the presence of named metavariables since it would imply that you can refer to ?b using case b => ... etc

[Thomas Murrills]

My final draft of the code above (now in #8364) appended ✝ at the end to avoid that confusion (e.g. ?m✝), so maybe that's a potential solution for alphabetic numbering, since the user knows ✝ terms are inaccessible!