Combining macros as functions

Stream: lean4

[Andrés Goens]

Say I wanted to combine two macros, e.g. because they represent two different syntax extensions and I want to call them recursively. I tried naming the functions and building one that combines them, but that apparently doesn't work. Here's an MWE:

import Lean

declare_syntax_cat foo
declare_syntax_cat bar
syntax (name := foo1) ident : foo
syntax (name := foo2) num : foo
syntax foo,* : bar

@[macro foo1]
def expandFoo1 : Lean.Macro
  | `(foo| $x:ident) => `($(Lean.quote x.getId.toString))
  | _ => Lean.Macro.throwUnsupported

@[macro foo2]
def expandFoo2 : Lean.Macro
  | `(foo| $x:num) => `($(Lean.quote x.getNat.repr))
  | _ => Lean.Macro.throwUnsupported

def expandFoo : Lean.Macro
  | `(foo| $x:foo) => do
    let x1 <- expandFoo1 x
    expandFoo2 x1

macro_rules
  | `(bar| $[$xs:foo],*) => do
     -- let xs' <- xs.mapM expandFoo1
     -- let xs' <- xs.mapM expandFoo2
     let xs' <- xs.mapM expandFoo
     let xsl : List (Lean.TSyntax `term) := xs'.toList.map λ stx => ⟨stx⟩
     `($(Lean.quote xsl))

syntax "[bar|" bar "]" : term
macro_rules
  | `([bar| $x:bar]) => `(bar| $x)

#check [bar| foo, baz]
#check [bar| 1, 2]
#check [bar| foo, 2]

I imagine I'm missing some housekeeping in MacroM with my improvised do-gluing there (actually based on Haskell's >=>). I imagine there might already even be a function that join macros like these somewhere but I cannot find it, can someone maybe point me to it?

[Andrés Goens]

Another option that kind of works but is pretty unsatisfactory (feels hacky) is just adding both patterns to one function and then marking the syntax by hand by defining another function (as the macro annotations won't combine)

@[macro foo1]
def expandFoo1 : Lean.Macro
  | `(foo| $x:ident) => `($(Lean.quote x.getId.toString))
  | `(foo| $x:num) => `($(Lean.quote x.getNat.repr))
  | _ => Lean.Macro.throwUnsupported

@[macro foo2]
def expandFoo2 : Lean.Macro := expandFoo1

(I'm assuming that I'll also want those macro expansions to work on their own)