Using nested Macro

Stream: lean4

[Codegoblin]

Hello,
is it possible, to nest Macros in the way, that the outer Macro "just" calls the macro rules of the underlying macro?

As Example:

declare_syntax_cat under

syntax "start " under* " end" : command
macro_rules
| `(start $stx* end) => `($stx)  -- How to call the lower Macro Definition?

syntax "eval " ident : under
macro_rules
| `(under| eval $id) => `(#eval $id)

syntax "check" ident : under
macro_rules
| `(under| check $id) => `(#check $id)

variable (x:Nat)

start
eval x
check x
end

I would like to encapsulate my Macros in a scope beginning with "start" and ending with "end", inside I want to be able to call *-many checks or evals (nothing else should be permitted). They should just evaluate to the macro rules already defined for them (e.g. check x becomes #check x)

Maybe there is also an easier or better way to archive this?

[Codegoblin]

I tried to solve my problem with another approach: Instead of using the underlying macro rules, I tried to recapture them in functions. However here I get either typeclass instance problem is stuck, it is often due to metavariables

private def evalMacroSyntax1
  (entries : Array (TSyntax `under)) := do
    let mut cmds := #[]
    for entry in entries do -- error in this line
      let cmd ← match entry with
        | `(under| check $id) => `(#check $id)
        | `(under| eval $id) => `(#eval $id)
        | _ => unreachable!
      cmds := cmds.push cmd
    return cmds

or I get multiple failed to synthesize instance

private def evalMacroSyntax2
  (entries : Array (TSyntax `under)) :=
    return entries.foldl
      (init := (#[]))
        fun (entry) => fun
          | `(under| check $id) => `(#check $id) -- error here
          | `(under| eval $id) => `(#eval $id) -- error here
          | _ => unreachable!

These examples are written into the original example.

How can I resolve these errors? How can I avoid crossing such errors in the future?

[Sebastian Ullrich]

You should annotate the return types of your functions

[Codegoblin]

@Sebastian Ullrich If I give the return type of Array (TSyntax `command) I apparently need to add Id.run, however then I get the error failed to synthesize instance now related to Id.

private def evalMacroSyntax
  (entries : Array (TSyntax `under))
    : Array (TSyntax `command) := Id.run do
      let mut cmds : Array (TSyntax `command) := #[]
      for entry in entries do
        let cmd ← match entry with
          | `(under| check $id) => `(#check $id) -- errors here
          | `(under| eval $id) => `(#eval $id) --errors here
          | _ => unreachable!
        cmds := cmds.push cmd
      return cmds

If this is not possible to solve, it's OK, since I can use MacroM Syntax as return value. However, then I cannot join the result with others (of type MacroM Syntax). Or if it is possible, I don't know how to do it.

With the following version I get another error in the last step saying (kernel) declaration has free variables '_eval'. Is this an Error in my variable declaration?

open Lean

declare_syntax_cat under

syntax "eval " ident : under
syntax "check" ident : under

private def evalMacroSyntax
  (entries : Array (TSyntax `under))
    : MacroM Syntax := do
      let mut cmds : Array (TSyntax `command) := #[]
      for entry in entries do
        let cmd : TSyntax `command ←
          match entry with
            | `(under| check $id) => `(#check $id)
            | `(under| eval $id) => `(#eval $id)
            | _ => unreachable! -- there are only two permitted options
        cmds := cmds.push cmd
      return (mkNullNode cmds)

syntax "start " under+ " end" : command
macro_rules
| `(start $stx* end) => evalMacroSyntax stx

variable (x:Nat)

start -- here i get the error => (kernel) declaration has free variables '_eval'
  eval x
  check x
end

[Sebastian Ullrich]

What do you expect evaluating a free variable to do? You get the same error using #eval x independently of your macro

[Codegoblin]

Oh, indeed. This was a problem in front of the pc. :laughing:

Thanks so far. However, I have one last question: Is it possible to "concatenate" multiple Structures of MacroM Syntax together? Or is the only way here to collect all in an Array and use mkNullNode?