Show expanded macros

Stream: lean4

[Marcus Rossel]

Is there a way of viewing the code generated by a macro?
For example, for something like:

macro "my_cmd" thing:ident : command => `(
  inductive $(mkIdent <| thing.getId ++ `One) | a | b | c
  inductive $(mkIdent <| thing.getId ++ `Two) | d | e | f
)

my_cmd Test

... is there a way of having Lean show me?:

inductive Test.One | a | b | c
inductive Test.Two | d | e | f

Or does this question not make sense, as Lean can't know which macros I want it to expand and which should remain untouched?

[Henrik Böving]

You can recover the Syntax object itself:

import Lean
open Lean

macro "my_cmd" thing:ident : command => do
  let stx ← `(
    inductive $(mkIdent <| thing.getId ++ `One) | a | b | c
    inductive $(mkIdent <| thing.getId ++ `Two) | d | e | f
  )
  dbg_trace stx
  return stx

my_cmd Test

but doing it in a readable way would require you to use the pretty printer which afaik cannot work because it operates in the meta stack (CoreM, MetaM) while MacroM is only a weak:

abbrev MacroM := ReaderT Macro.Context (EStateM Macro.Exception Macro.State)

[Marcus Rossel]

@Henrik Böving I don't understand the last part about the pretty printer. Are you saying that there is way to pretty print any given Syntax object, but it requires using CoreM/MetaM? If so, let's say I have a Syntax object, then how would I use CoreM/MetaM to pretty print it?

[Henrik Böving]

In your case for example with docs4#Lean.PrettyPrinter.ppCommand, the pretty printer is how all of the info view works, otherwise we'd only see Exprs

Also i dug a little more you can get a sort of pretty print (more of a toString) this way:

import Lean
open Lean

macro "my_cmd" thing:ident : command => do
  let stx ← `(
    inductive $(mkIdent <| thing.getId ++ `One) | a | b | c
    inductive $(mkIdent <| thing.getId ++ `Two) | d | e | f
  )
  dbg_trace Syntax.prettyPrint stx
  return stx

my_cmd test

[Sebastian Ullrich]

set_option trace.Elab.command true; see https://leanprover.github.io/lean4/doc/dev/debugging.html#tracing