Implementing a macro with a sort of "syntax ... in ..."

Stream: lean4

[carson storm]

Hi all, so I am trying to design macro with_binop that would expand something like

with_binop " • " => (comp: α → α → α) in
example (x y : α) : α := x • y

to

section
variable (comp : α → α → α)

local infix:70 " • " => comp

example (x y : α) : α := x • y

end

Right now I am implementing the macro with

open Parser.Command Parser.Term in
syntax "with_binop " Parser.strLit " => " " ( " ident " : " term " ) " " in " command
  : command

open Elab Command in
elab_rules : command
 | `(with_binop $op:str => ($fname:ident : $ftype:term) in $cmd:command) => do

    elabCommand <|<- `(section)
    elabCommand <|<- `(variable ($fname : $ftype))
    elabCommand <|<- `(local infix:70 " • " => $fname)
    elabCommand <| cmd
    elabCommand <|<- `(end)

This isn't working, and I think the main issue that the command after "in" is parsed before the macro is expanded, so it doesn't yet recognize • as a token. Is there a way to defer parsing the command until the macro is expanded? Or is there a better way to achieve similar behavior?

[Alex Keizer]

I'm not sure if it works, but you could try having the with_binop syntax not take the command instead having it expand to

section
 variable ...
 local infix ...
 with_binop_cmd

Where with_binop_cmd is another macro that consumes a single command and puts an end after it.

[carson storm]

So, sort of chaining the macros? Any idea how to write an elaboration rule in this case, since with_binop would be in a sense producing macro instead of a command.

[Alex Keizer]

Hmm, I think it would have to be a macro (i.e., a rewrite rule), I don't think it would work as a command elaborator

[Alex Keizer]

Ok, no, that won't work; the syntax anti-quotation doesn't accept with_binop_cmd as-is, you need to supply it with a command.
One workaround could be to rely on the user to write the sections manually, rather than trying to scope the with_binop to a single command