macro expander

Stream: lean4

[Yasu Watanabe]

Is there Common LIsp's macroexpand or macroexpand-1 equivalent in Lean 4? I'm reading "Beyond Notations" paper and try to understand how macros are expanded into non meta language.

[Henrik Böving]

Basically its done like this: (from here https://github.com/leanprover/lean4/blob/master/doc/metaprogramming-arith.md)
you declare a bunch of syntax rules:

declare_syntax_cat arith
syntax num : arith -- int for Arith.int
syntax str : arith -- strings for Arith.symbol
syntax:60  arith:60 "+" arith:61 : arith -- Arith.add
syntax:70 arith:70 "*" arith:71 : arith -- Arith.mul
syntax "(" arith ")" : arith -- bracketed expressions
syntax "`[Arith| " arith "]" : term

you declare a bunch of macro rules:

macro_rules
  | `(`[Arith| $s:strLit ]) => `(Arith.symbol $s)
  | `(`[Arith| $num:numLit ]) => `(Arith.int $num)
  | `(`[Arith| $x:arith + $y:arith ]) => `(Arith.add `[Arith| $x] `[Arith| $y])
  | `(`[Arith| $x:arith * $y:arith ]) => `(Arith.mul `[Arith| $x] `[Arith| $y])
  | `(`[Arith| ($x:arith) ]) => `(`[Arith| $x ])

you can instead of declaring macro rules also declare MacroM functions and mark them as elaborators of certain syntax declarations
now whenever lean sees the corresponding syntax, this is for example how its done here: https://github.com/leanprover/doc-gen4/blob/main/DocGen4/IncludeStr.lean#L28-L50, note that this is a term elaborator which is a special case of a macro that (surprise) is used in place of a term.

Now whenever lean sees the corresponding syntax it will execute the macro code and put whatever expression it returned in place of it. There is also a more special case of this which is the tactic world where you also have metavariables and the proof context etc but the basic idea is this.

[Sebastian Ullrich]

@Yasu Watanabe I think you are looking for expandMacro? (which ultimately uses epxandMacroImpl?). See also the paper supplement for a standalone implementation of an expander.