Dimming implicit arguments in `#check`

Stream: general

[Mirek Olšák]

I just thought that it could improve user experience if I could quickly see the explicit arguments of a library function, so for example when typing

#check AffineSubspace

Seeing highlighted output instead of the monotone current state. What do you think? Would it be easy to implement? Would it be generally appreciated?
check-AffineSubspace-hl.png
check-AffineSubspace.png.

[Ruben Van de Velde]

I have the impression that this was discussed recently and it was hard, but would certainly be nice

[Ruben Van de Velde]

Also on hover

[Markus Himmel]

Here is the recent discussion. It was about the signature help, not about #check. #lean4 > rfc: show arity of current function

[Mirek Olšák]

Hm, it should not be that hard at least in terms of generating HTML... Only that it would miss the hover feature, so it cannot be the default.

[Aaron Liu]

apparently we can do diagrams in the docstrings and it shows up in the infoview #mathlib4 > readable commutative diagrams in docstrings @ 💬

[Aaron Liu]

so the infoview is pretty powerful

[Mirek Olšák]

In a sense, clickable grayed-out terms are possible

import ProofWidgets
import Qq

open ProofWidgets Jsx

open Qq in
def makeWidget : Lean.Meta.MetaM Html := do
  let term : Q(Nat) := q(2 + 2)
  return <span «class»="goal-inaccessible">
    <InteractiveCode fmt={← Lean.Widget.ppExprTagged term} /> </span>

#html makeWidget

[Mirek Olšák]

(only it is also italic)

[Michael Rothgang]

My personal preference would be to add a version of #check that only shows explicit arguments. (Probably, adding a configuration option to #check would be the way, i.e. this needs core modifications.)

[Michael Rothgang]

Here is how to write this as a separate command, today:

import Mathlib

open Lean Elab Command PrettyPrinter Delaborator in
elab tk:"#check' " name:ident : command => runTermElabM fun _ => do
  for c in (← realizeGlobalConstWithInfos name) do
    addCompletionInfo <| .id name name.getId (danglingDot := false) {} none
    let info ← getConstInfo c
    let delab : Delab := do
      delabForallParamsWithSignature fun binders type => do
        let binders := binders.filter fun binder => binder.raw.isOfKind ``Parser.Term.explicitBinder
        return ⟨← `(declSigWithId| $(mkIdent c) $binders* : $type)⟩
    logInfoAt tk <| .ofFormatWithInfosM (PrettyPrinter.ppExprWithInfos (delab := delab) info.type)

/--
info: mfderiv_comp (x : M) (hg : MDifferentiableAt I' I'' g (f x)) (hf : MDifferentiableAt I I' f x) :
  mfderiv I I'' (g ∘ f) x = (mfderiv I' I'' g (f x)).comp (mfderiv I I' f x)
-/
#guard_msgs in
#check' mfderiv_comp

[Michael Rothgang]

Note that #check' mfderiv_comp does not show any of the ~dozen implicit or typeclass arguments.

[Mirek Olšák]

Thanks for the first outline, although I would prefer the implicit arguments dimmed, not missing...

[Mirek Olšák]

That probably means doing custom elementary argument decomposition side, to produce a Html instead of MessageData, so we would need to reimplement things like

• printing different kinds of parentheses around arguments
• skipping [anonymous] : for arguments without names
• grouping together arguments with identical types

Besides that, it suffices to group all the Html parts into <span class="font-code">, and dimmed arguments into <span class="goal-inaccessible">. Do I understand it correctly?

[Michael Rothgang]

(Note: making a #check' tactic is not difficult either, I have that on a branch. Let me open a PR in any case.)

[Mirek Olšák]

Here we go!

import Mathlib

open Lean ProofWidgets Jsx in
def checkH (name : Lean.Name) (showAlt : Bool) : MetaM Unit := do
  let constVal ← getConstVal name
  Meta.forallTelescope constVal.type <| fun args outType => do
    let mut msg : MessageData := toString name
    if !constVal.levelParams.isEmpty then
      let univStr : String := ",".intercalate (constVal.levelParams.map toString)
      let univStr := ".{" ++ univStr ++ "}"
      let alt := if showAlt then univStr else ""
      msg := msg ++ (←MessageData.ofHtml <span «class»="o-50">{
        .text <| univStr
      }</span> alt)
    let decls ← args.mapM Meta.getFVarLocalDecl
    let groups := decls.toList.splitBy
      (fun d1 d2 => declCore d1 == declCore d2)
    for group in groups do
      let decl : LocalDecl := group.head!
      let (p1,p2) : String × String := match decl.binderInfo with
      | .default => ("(",")")
      | .implicit => ("{","}")
      | .instImplicit => ("[","]")
      | .strictImplicit => ("⦃","⦄")
      let mut paramParts : Array (String ⊕ Expr) := #[.inl " "]
      paramParts := paramParts.push (.inl p1)
      if group.length > 1 ∨ ¬decl.binderInfo.isInstImplicit then
        for arg in group do
          let e : Expr := .fvar arg.fvarId
          paramParts := paramParts.push (.inr e)
          paramParts := paramParts.push (.inl " ")
        paramParts := paramParts.push (.inl ": ")
      paramParts := paramParts.push (.inr decl.type)
      paramParts := paramParts.push (.inl p2)
      let paramMsg : MessageData ←
        if decl.binderInfo.isExplicit then
          pure <| paramParts.foldl (fun m part =>
            m ++ match part with
            | .inl s => toMessageData s
            | .inr e => toMessageData e
          ) m!""
        else
          let htmls ← paramParts.mapM (fun part => match part with
          | .inl s => pure (.text s)
          | .inr e => do
            let widget ← Lean.Widget.ppExprTagged e
            pure <InteractiveCode fmt={widget} />
          )
          let mut alt := ""
          if showAlt then
            let strs : Array String ← paramParts.mapM (fun part => match part with
            | .inl s => pure s
            | .inr e => toString <$> Meta.ppExpr e
            )
            alt := "".intercalate strs.toList
          pure <| ←MessageData.ofHtml
            (.element "span" #[("class", "o-50")] htmls) alt
      msg := msg ++ paramMsg
    msg := msg ++ " : "
    msg := msg ++ outType
    logInfo msg
where
  declCore (decl : Lean.LocalDecl) :=
    (decl.type, decl.binderInfo, decl.kind)

elab "#checkh " name:ident : command =>
  Lean.Elab.Command.runTermElabM fun _ => do
    for fullName in (← Lean.Elab.realizeGlobalConstWithInfos name) do
      checkH fullName false
elab "#checkh' " name:ident : command =>
  Lean.Elab.Command.runTermElabM fun _ => do
    for fullName in (← Lean.Elab.realizeGlobalConstWithInfos name) do
      checkH fullName true

#checkh AffineSubspace
#checkh mul_assoc

It might not be as sophisticated as the real delaboration but looks usable.

[Mirek Olšák]

Update: Now it only passes the dimmed parts through Html, so Error Lens show the same as check'. Now I am quite happy with it. Where could this belong? ProofWidgets?
Update2: o-50 looks like better dimmer than goal-inaccessible. I update the code above.

[Mirek Olšák]

screenshot.png
error-lens.png

[Eric Wieser]

I wonder if this should be built into the term MessageData formatter, so that this also happens in error messages about mismatching types?

[Mirek Olšák]

Unfortunatelly, I don't think it is a desirable feature in general that the export from MessageData to String hides some parts of the output. Only here, I didn't have much better option because I needed to insert an HTML tag into it, which breaks the path to string.

[Mirek Olšák]

Actually, I could have used the alt-text, so it is possible to export string correctly... Hard to decide. I still think for user experience the shortened Error Lens is great, but I cannot expect this to be the default, when you also see the shortened string on terminal output upon calling lean from command line.

[Mirek Olšák]

If the question was about dimming implicit arguments in other MessageData, then sure, I think it would be helpful & principled (without the detour through ProofWidgets).

[Mirek Olšák]

I made it a PR to ProofWidgets: https://github.com/leanprover-community/ProofWidgets4/pull/142
I understand it would be better to have it more general, and in Core but let's start somewhere...