Nesting Macros - possible? worthwhile?

Stream: new members

[Britt Anderson]

My knowledge of metaprogramming is limited to some rudimentary common lisp. In trying a learning exercise for myself I was led into a side question about macros. In my case I wanted to create a "state" type that was essentially just a Fin n. I wanted to be able to create new values for a state type of a particular n without my users (or myself) having to always specify the bound or provide a proof like (by omega) that seemed boiler plate. I just wanted compile time failure for bad values. Trying to work with claude.ai to create a nested structure for my macros we came up with the following. It doesn't work, but may be a clearer way of showing what I was going for.

macro "makeFinMacro" name:ident bound:term : command =>
  `(macro $name n:term : term =>
      `(@Fin.mk $bound $$n (by omega)))

makeFinMacro myFin8 8

#eval myFin8 3   -- Expands to @Fin.mk 8 3 (by omega)

Of course this doesn't actually work. My question is not so much about the specifics here, though I would be happy to see a corrected implementation, but a more general comment on this type of "nesting". Is it thought to be useful? If so, is there a more standard way to implement it, and can I be pointed to something to read? Thank you.

[Robin Arnez]

Possible? Yes:

macro "makeFinMacro" name:ident bound:term : command =>
  `(macro $(Lean.Syntax.mkStrLit name.getId.toString):str n:term : term =>
      `(@Fin.mk $bound $$n (by omega)))

makeFinMacro myFin8 8

#eval myFin8 3   -- Expands to @Fin.mk 8 3 (by omega)

Worthwhile? Definitely sometimes, core also does something similar with declare_simp_like_tactic:

declare_simp_like_tactic simpOnce "simp_once" +singlePass

example (a b : Bool) : a = b := by
  simp_once only [Bool.eq_iff_iff]

[Britt Anderson]

Thank you. Can you explain why we need $(Lean.Syntax.mkStrLit name.getId.toString):str in place of $name. I am not quite sure what to look up to understand this better. I can see the source for mkStrLit, but I don't understand why it is needed here or where to read to better understand that.