macro_rules not apply

Stream: lean4

[Remy Citerin]

Hello, I tried to use macro_rules to make DSL's but I have the impression that in some cases the macros are not applied, I don't understand

declare_syntax_cat foo
syntax "[bar|" foo "]" : term
syntax num : foo
syntax " ( " foo " ) " : foo

macro_rules
| `(foo| ( $f:foo )) => `(foo| $f)
| `([bar|$n:num]) => `($n)

#eval [bar|0]
#eval  [bar|(0)]

#eval [bar|(0)] return an error, the elaboration function is not implemented according to Lean

[Marcus Rossel]

You're not handling the case for [bar|f]where f is a foo but not a num. This fixes it:

declare_syntax_cat foo
syntax "[bar|" foo "]" : term
syntax num : foo
syntax " ( " foo " ) " : foo

macro_rules
| `(foo| ( $f:foo ))    => `(foo| $f)
| `([bar|$n:num])       => `($n)
| `([bar| ( $f:foo ) ]) => `([bar|$f]) -- add this

#eval [bar|0]
#eval [bar|(0)]

[Remy Citerin]

yes but normally it should just reduce (0) to 0 in [bar|(0)]? And that doesn't solve the problem I want to solve (here is just a minimal example), because in fact I'm not really using $[bar|$f]$ but a custom elaborator that I want to keep simple: for example having a general notation for binary operators like [BINOP| +, $e1, $e2] then have a set of macros to have +, *... with the right associativity...

[Marcus Rossel]

Does this serve your use case better?:

macro_rules
  | `(foo|$n:num)      => `($n)
  | `(foo| ( $f:foo )) => `(foo| $f)
  | `([bar|$f:foo])    => `(foo| $f)

[Remy Citerin]

no it doesn't work, like I said, I actually want to be able to use custom elaborators:

declare_syntax_cat foo
syntax "[bar|" foo "]" : term
syntax num : foo
syntax " ( " foo " ) " : foo

macro_rules
  | `(foo|$n:num)      => `($n)
  | `(foo| ( $f:foo )) => `(foo| $f)
  | `([bar|$f:foo])    => `(foo| $f)
-- my goal: elabFoo does not contain the rule `($f:foo)` because this case is handled by macros
-- so the user of my library can add macros in my DSL
open Qq in
def elabFoo : TSyntax `foo → TermElabM Q(ℕ)
  | `(foo| $n:num) => do
    have n: ℕ := n.getNat
    return q($n)
  | s => throw <| .error s "unsupported syntax"

elab "elab_foo " e:foo : term => elabFoo e
#eval [bar|0]
#eval [bar|(0)]
#eval elab_foo (0) -- error: unsupported syntax

[Mac Malone]

@Remy Citerin You can use docs#Lean.expandMacros to apply any macros to a syntax before match on it. For example:

def elabFoo (foo : TSyntax `foo) : TermElabM Q(ℕ) :=
  let foo <- liftMacroM <| expandMacros foo
  match foo with
  | `(foo| $n:num) => do
    have n: ℕ := n.getNat
    return q($n)
  | s => throw <| .error s "unsupported syntax"

[Sebastian Ullrich]

The first choice in an elaborator should be to recursively elaborate nested syntax and then match on the Expr because that will deal with both macros and elaborators. It depends on the specific use case of course.

[Sebastian Ullrich]

To answer the underlying question:
Remy Citerin said:

yes but normally it should just reduce (0) to 0 in [bar|(0)]?

No, macro expansion works outside-in. This is important for providing the outer macro with as much structure as possible as well as to unify expansion and elaboration.

[Remy Citerin]

using Lean.expandMacros works very well, thanks for the explanation