Get theorem statement as string

Stream: lean4

[Jon Eugster]

How can I extract a String of the form add_zero (n : Nat) : n + 0 = n or just (n : Nat) : n + 0 = n from a defined theorem add_zero? I tried the following:

import Lean

open Lean Meta Elab Command

theorem add_zero (n : Nat) : n + 0 = n := rfl

-- copied from `#check`
def magic (term : Ident) : CommandElabM MessageData := do
  let c := term.getId
  addCompletionInfo <| .id term c (danglingDot := false) {} none
  return (.ofPPFormat { pp := fun
    | some ctx => ctx.runMetaM <| PrettyPrinter.ppSignature c
    | none     => return f!"{c}"  -- should never happen
  })

elab "Test" name:ident : command => do
  logInfoAt name (← magic name)
  logInfoAt name (← (← magic name).toString)

Test add_zero

-- MWE.lean:25:5
--   add_zero (n : Nat) : n + 0 = n  -- `MessageData` looks good in VSCode


-- MWE.lean:25:5
--   add_zero   -- But `.toString` does not do what I want.

The MessageData looks correct, but I can't turn that into a String without loosing the type.

(I want to pack this into a JSON, that's why I think I need String rather than MessageData)

[Kyle Miller]

The main function here is getTypeString

import Lean

open Lean Meta Elab Command

theorem add_zero (n : Nat) : n + 0 = n := rfl

-- Copied somewhat from PrettyPrinter.ppSignature
def getTypeString (name : Name) : MetaM String := do
  let decl ← getConstInfo name
  let e := Expr.const name (decl.levelParams.map mkLevelParam)
  let (stx, _stx) ← PrettyPrinter.delabCore e (delab := PrettyPrinter.Delaborator.delabConstWithSignature)
  let f ← PrettyPrinter.ppTerm ⟨stx⟩ -- HACK: not a term
  return toString f

-- copied from `#check`
def magic (term : Ident) : CommandElabM Unit := do
  try
    for c in (← resolveGlobalConstWithInfos term) do
      addCompletionInfo <| .id term c (danglingDot := false) {} none
      logInfoAt term <| .ofPPFormat { pp := fun
        | some ctx => ctx.runMetaM <| getTypeString c
        | none     => return f!"{c}"  -- should never happen
      }
  catch _ => throwError "failure in magic"


elab "Test" name:ident : command => do
  magic name

Test add_zero
-- add_zero (n : Nat) : n + 0 = n

[Kyle Miller]

Here's a simpler function:

def getTypeString (name : Name) : MetaM String := do
  let decl ← getConstInfo name
  let ty ← ppExpr decl.type
  return toString name ++ " : " ++ toString ty

Rather than the fancy one that puts arguments before the colon, this one gives types like add_zero : ∀ (n : Nat), n + 0 = n

[Jon Eugster]

Thanks Kyle!

[Sebastian Ullrich]

The problem with your original code is that ctx is indeed none, which you can fix by wrapping the message in addMessageContextPartial

[Jon Eugster]

I have to go back on the computer to understand that... where did Kyle's first solution get its ctx back?

[Kyle Miller]

The ctx comes from when the MessageData is finally formatted for the infoview; this .ofPPFormat constructor is for deferring pretty printing until you have such a context. (At least this is my understanding -- I've never really looked at it until now!)

[Kyle Miller]

The problem with the original magic function is that it tries to format the data immediately, so it's not yet in a context with a ctx.

[Jon Eugster]

I understand now what happened, thanks!