Chaining commands defined as macros

Stream: lean4

[Adam Topaz]

Is there a way to "compose" commands defined using macro? Silly mwe:

macro "c0" s:ident : command => `(def $s:ident : Nat := 0)
macro "c1" s:ident : command => `(def $s:ident : Nat := 1)

macro "c01" s:ident t:ident : command => do
  `(c0 $s)
  `(c1 $t)

The last macro gives an error because `(c0 $s) would have had to be of type MacroM Punit

[Leonardo de Moura]

macro "c0" s:ident : command => `(def $s:ident : Nat := 0)
macro "c1" s:ident : command => `(def $s:ident : Nat := 1)

macro "c01" s:ident t:ident : command => do
  `(c0 $s c1 $t)

c01 x y
#print x
#print y

[Adam Topaz]

Thanks! Just for my own understanding, I would still like to know whether there is a way to do this without putting both c0 and c1 in a single quotation.

[Sebastian Ullrich]

A macro is a transformation from syntax tree to syntax tree, so in the end you do have to produce exactly one tree. In an elaborator however you can "execute" intermediate commands using elabCommand, which does produce Unit

[Adam Topaz]

yes I understand that. But there must be a way to run a macro in an elab command?

[Sebastian Ullrich]

Yes, by feeding the macro's output into elabCommand

[Adam Topaz]

Ah okay I think I understand

[Adam Topaz]

For the sake of completeness, I suppose

import Lean
open Lean Elab Command

macro "c0" s:ident : command => `(def $s:ident : Nat := 0)
macro "c1" s:ident : command => `(def $s:ident : Nat := 1)

elab "c01" s:ident t:ident : command => do
  elabCommand (← `(c0 $s))
  elabCommand (← `(c1 $t))

c01 x y
#print x
#print y

illustrates what @Sebastian Ullrich was saying?

[Adam Topaz]

Anyway, this works! Thanks to both of you!

[Marcus Rossel]

@Adam Topaz, you might also be interested in mkNullNode for chaining instances of Command on a syntactic level: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Antiquot.20Splice/near/297761901