macro for multiple commands

Stream: general

[Jeremy Avigad]

Is it possible to write a macro that expands to a sequence of Lean commands? For example #silly foo expands to

def foo_1 := 1
def foo_2 := 2
def foo_3 := 3

and #silly bar expands to

def bar_1 = 1
def bar_2 = 2
def bar_3 = 3

If macros are not the way to go, what is the easiest way to write such a command?

[Alex J. Best]

I couldn't find a way when I tried recently and instead came up with something only slightly more verbose in this thread
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Type.20synonym.20boilerplate

[Adam Topaz]

You can just put them all into an quotation

[Adam Topaz]

macro "foo!!" : command =>
`(def foo1 := 1
def foo2 := 2
def foo3 := 3)

This works, but there is something that needs to be done with the actual names foo1 etc. that I forget at the moment.

[Adam Topaz]

Oh wait I misunderstood. But it's still possible, you just need to pass a nm:ident as a parameter (for foo resp. bar)

[Tomas Skrivan]

Here is how you can chain it in a for loop.

elab "#empty" : command => pure ()
macro "#silly" id:ident : command => do

  let mut command : TSyntax `command ← `(command| #empty)
  for i in [0:3] do
    let idn := mkIdent (id.getId.appendAfter s!"_{i}")
    let n := Syntax.mkNumLit (toString i)
    command ←
      `($command
        def $idn := $n)
  pure command

#silly foo
#print foo_1

#silly bar
#print bar_2

The command #empty is just a dummy command doing nothing and is used to initialize the value of command. There has to be a better way to do this.

[Adam Topaz]

Aha! mkIdent is what I was missing in my first message :)

[Alex J. Best]

And you don't really need to build them all as one syntax if you use an elab instead and just elab the defs one at a time in a loop instead of building one big syntax for the block

[Kyle Miller]

One pattern you find in things like the derive handlers is that functions return an Array (TSyntax `command), these are all concatenated, and then there's a main loop that elabs the combined results.

[Kyle Miller]

Another pattern is in the irreducible_def module. It (locally) defines a syntax for a sequence of commands, where when it elaborates them it stops at the first error: https://github.com/leanprover-community/mathlib4/blob/7d308680dc444730e84a86c72357ad9a7aea9c4b/Mathlib/Tactic/IrreducibleDef.lean#L58

[Mac Malone]

The easiest way to expand/elaborate (an Array of) multiple commands at once is via mkNullNode (which the command elaborator has special support for):

macro "#silly " id:ident : command =>
  let cmds := -- [0:3].map ...
  {raw := mkNullNode cmds}

(Sorry that I cannot write a proper mwe. I am on my phone away from the computer).

[Jeremy Avigad]

Thank you! All the information and examples are helpful.