A version of check displaying only explicit arguments.

Stream: lean4

[Patrick Massot]

I would be very grateful if some meta-programming guru could write a version of the #check command that shows only explicit argument. This week I’m spending a significant portion of my time staring at things like

MDifferentiableAt.clm_apply_of_inCoordinates.{u_1, u_2, u_3, u_4, u_5, u_6, u_7, u_8, u_9, u_10, u_11, u_12, u_13, u_14}
  {𝕜 : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {B₁ : Type u_4} {B₂ : Type u_5} {M : Type u_6} {E₁ : B₁ → Type u_7}
  {E₂ : B₂ → Type u_8} [NontriviallyNormedField 𝕜] [(x : B₁) → AddCommGroup (E₁ x)] [(x : B₁) → Module 𝕜 (E₁ x)]
  [NormedAddCommGroup F₁] [NormedSpace 𝕜 F₁] [TopologicalSpace (TotalSpace F₁ E₁)] [(x : B₁) → TopologicalSpace (E₁ x)]
  [(x : B₂) → AddCommGroup (E₂ x)] [(x : B₂) → Module 𝕜 (E₂ x)] [NormedAddCommGroup F₂] [NormedSpace 𝕜 F₂]
  [TopologicalSpace (TotalSpace F₂ E₂)] [(x : B₂) → TopologicalSpace (E₂ x)] {EB₁ : Type u_9} [NormedAddCommGroup EB₁]
  [NormedSpace 𝕜 EB₁] {HB₁ : Type u_10} [TopologicalSpace HB₁] {IB₁ : ModelWithCorners 𝕜 EB₁ HB₁} [TopologicalSpace B₁]
  [ChartedSpace HB₁ B₁] {EB₂ : Type u_11} [NormedAddCommGroup EB₂] [NormedSpace 𝕜 EB₂] {HB₂ : Type u_12}
  [TopologicalSpace HB₂] {IB₂ : ModelWithCorners 𝕜 EB₂ HB₂} [TopologicalSpace B₂] [ChartedSpace HB₂ B₂] {EM : Type u_13}
  [NormedAddCommGroup EM] [NormedSpace 𝕜 EM] {HM : Type u_14} [TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  [TopologicalSpace M] [ChartedSpace HM M] [FiberBundle F₁ E₁] [VectorBundle 𝕜 F₁ E₁] [FiberBundle F₂ E₂]
  [VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁} {b₂ : M → B₂} {m₀ : M} {ϕ : (m : M) → E₁ (b₁ m) →L[𝕜] E₂ (b₂ m)}
  {v : (m : M) → E₁ (b₁ m)}
  (hϕ :
    MDifferentiableAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀)
  (hv : MDifferentiableAt IM (IB₁.prod 𝓘(𝕜, F₁)) (fun m ↦ { proj := b₁ m, snd := v m }) m₀)
  (hb₂ : MDifferentiableAt IM IB₂ b₂ m₀) :
  MDifferentiableAt IM (IB₂.prod 𝓘(𝕜, F₂)) (fun m ↦ { proj := b₂ m, snd := (ϕ m) (v m) }) m₀

trying to spot what are the arguments I’m meant to give explicitly. Note that an option to tell #check to remove universes would also be nice. It would be even greater to have an option asking for tooltips to show only explicit arguments, but I’m probably getting too excited here.

[Patrick Massot]

I don’t even understand why

namespace Lean.Elab.Command
open Meta

elab "#check'" x:term : command => do
  withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_check do
    let e ← Term.elabTerm x none
    Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true)
    Meta.check e
    let e ← Term.levelMVarToParam (← instantiateMVars e)
    if e.isSyntheticSorry then
      return
    let type ← inferType e
    logInfo m!"{e} : {type}"

end Lean.Elab.Command

does not reproduce what #check is doing in the above example.

[Aaron Liu]

#check has special support for identifiers

[Joachim Breitner]

You want to see only explicit parameters, right?

[Aaron Liu]

If you do #check (MDifferentiableAt.clm_apply_of_inCoordinates) then it fills in the implicit arguments with metavariables

[Patrick Massot]

I’m not sure what is the difference between arguments and parameters. In the above example I’d like to see

MDifferentiableAt.clm_apply_of_inCoordinates
  (hϕ :   MDifferentiableAt IM 𝓘(𝕜, F₁ →L[𝕜] F₂) (fun m ↦ inCoordinates F₁ E₁ F₂ E₂ (b₁ m₀) (b₁ m) (b₂ m₀) (b₂ m) (ϕ m)) m₀)
  (hv : MDifferentiableAt IM (IB₁.prod 𝓘(𝕜, F₁)) (fun m ↦ { proj := b₁ m, snd := v m }) m₀)
  (hb₂ : MDifferentiableAt IM IB₂ b₂ m₀) :
  MDifferentiableAt IM (IB₂.prod 𝓘(𝕜, F₂)) (fun m ↦ { proj := b₂ m, snd := (ϕ m) (v m) }) m₀

[Aaron Liu]

Do you want it on only identifiers?

[Kyle Miller]

An idea: use the signature delaborator directly and then filter out the implicit binder syntaxes.

Here's a hint for the new interface for that: https://github.com/leanprover/doc-gen4/pull/302/files#diff-2cee00262515d0d1209747d4bb2dbec5423900de5ec0ab9f286446e02eb96090R54

If you use the right kind of messagedata, there's a way to pass along the infos

[Patrick Massot]

Aaron Liu said:

Do you want it on only identifiers?

This would already be very useful. Of course more is better.

[Aaron Liu]

I'm asking because if you try it on a general term then elabTerm will fill them in with metavariables first

[Aaron Liu]

Anyways here's what I came up with

import Mathlib

namespace Lean.Elab.Command
open Meta

elab "#check'" x:term : command => do
  withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_check' do
    let e ← Term.elabTerm x none
    Term.synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true)
    Meta.check e
    let mut e ← Term.levelMVarToParam (← instantiateMVars e)
    if e.isSyntheticSorry then
      return
    let mut type ← instantiateMVars (← inferType e)
    -- for tracking the context, since it seems complicated to do it myself I have a metavariable do it for me
    let mut mvar ← mkFreshExprMVar (some type)
    repeat do
      let .forallE n t b bi := type | break
      if let .default := bi then break
      (type, mvar, e) ← mvar.mvarId!.withContext do withLocalDecl n bi t fun v => do
        let e := .app e v
        let type := b.instantiate1 v
        let mvar ← mkFreshExprMVar (some type)
        return (type, mvar, e)
    mvar.mvarId!.withContext do logInfo m!"{e} : {type}"

end Lean.Elab.Command

#check' @MDifferentiableAt.clm_apply_of_inCoordinates

[Patrick Massot]

Thanks, it’s very encouraging but does not use delaborators, so the output is pretty hard to read.

[Aaron Liu]

What do you mean by that?

[Aaron Liu]

Do you want to use the signature delaborator?

[Kyle Miller]

I'm pretty sure Patrick wants what check does, but skip the implicit binders

[Patrick Massot]

Oh no, this is simply a missing open Manifold, sorry about the noise.

[Patrick Massot]

But it would still be nicer to have the argument names instead of a chain of implications.

[Kyle Miller]

Iirc, MessageData.ofFormatWithInfos is the other piece to the puzzle, given the interface in the linked diff, for how to print the result and get it hoverable. If you copy some of the delabConst and declSigId logic from the core signature delaborator, you can get the constant in there too. (On my phone)

[Eric Wieser]

Could there be a pp option to show all arrows as named binders, if they have a name? That is, show ℕ → ℕ as (n : ℕ) → ℕ etc

[Kyle Miller]

Every arrow has a name though, but presence of macro scopes is a reasonable indication of being intentional.

There's a secret inaccessible pp option for this, used by the signature delaborator to do exactly this after the colon. https://github.com/leanprover/lean4/blob/8424ddbb3edf4c3b440d0c4e1216e3ebf19bdaf4/src/Lean/PrettyPrinter/Delaborator/Builtins.lean#L950

[Aaron Liu]

there are secret pp options?

[Kyle Miller]

import Lean

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)

#check' id
-- id (a : α) : α

[Patrick Massot]

Great, thanks!