Accessing splices and joining quoted syntax in macros

Stream: lean4

[Codegoblin]

Hello,
I would like to bundle multiple commands together as a new command.

However, I have problems to compute the splices as identifiers in the attached example. (I get Error : unexpected token '*'; expected ':=', 'where' or '|')

Additionally, I would like to join x and y, so that both are executed when you call the command. Is this even possible?

open Lean
syntax "create" ident "{"
  (ident ":" ident),*
"}" : command

set_option hygiene false in
macro_rules
| `(create $name {}) => `(variable ($name : R))
| `(create $name {
      $[$relation : $name2],*
    }
  )
  => show MacroM Command from do
    let x : MacroM (TSyntax `command) :=
    `(
      variable ($name : R)
      variable ($name2* : R)
      -- rel def ?
      def $relation* : Prop := true -- how to access relation as identifier
    )
    let y : MacroM (TSyntax `command) := `(variable (xx : Nat))
    x -- join x and y

create A {
  B : C
}
#check A
#check B
#check C

[Marcus Rossel]

What is create A { B : C } supposed to do?

[Codegoblin]

@Marcus Rossel

create A { B : C }

It is supposed to execute the commands in the Macro.
Meaning to create the Variables A and C. This and the matching work already.

Then I would also like it to create the definition (or theorem) with name B. However, here I can't (or don't know how to) access the ident "relation".

Since I want the possibility to add more than one in the {}-brackets, I used the *-Operator.

Another possibility would be to use a for loop over relation and name2, but then I would have to join multiple of the Expressions in the `()-Quotation together (which I also do not know how to do).

Maybe there is also an easier way to accomplish my goal?

[Jon Eugster]

Is it that you just need to give your definition a name? adding def xy $relation* : Prop := True seems to compile at first glance. I think I actually don't understand what you try to do, sorry. If B is a list of names then I think you should create one definition per name. If B includes hypotheses, then I think you need separate name & declSign as in the link below.

[Jon Eugster]

(note that I have no clue, but for reference here I create some theorems on the fly, maybe that helps for comparison?)

[Eric Wieser]

You can't access relation as an identifier, because relation is an Array. Did you want to loop over that array?

[Codegoblin]

@Eric Wieser Indeed, that's what I want. I want that the def is created as many times as there is something in the array.
@Jon Eugster I think my description was unclear. I want to create the possibility to add *-many entrys in the {}. For example

create A{
B : C
D : E
F : G
H : J
}

should also be possible. (And can already be parsed). I would like to access relation in a manner that the def is done *-times like in the variable creation (
variable ($name2* : R)

E: So the output of the Example above would be.

variable (A:R)
variable (C:R)
variable (E:R)
variable (G:R)
variable (J:R)

def B : Prop := true
def D : Prop := true
def F : Prop := true
def H : Prop := true

[Codegoblin]

Here is a minimalistic example of what I'm trying to archive.

While cmd1 works, in cmd2 I get an Error.

If there is another way to achieve this goal (maybe without macro?), I will also gladly hear it.

open Lean
syntax "cmd1" ident,* : command

macro_rules
| `(cmd1 $[$n],*) => do
    `(variable ($n* : Prop))  -- Error in this line

cmd1 A, B, C

#check A
#check B
#check C


syntax "cmd2" ident,* : command

set_option hygiene false in
macro_rules
| `(cmd2 $[$n],*) => do
    `(def $n* : Prop := True)

cmd2 A, B, C

#check A
#check B
#check C

[Marcus Rossel]

I'm not sure where R comes from, but this implements the example you gave:

import Lean
open Lean

declare_syntax_cat entry
syntax ident " : " ident : entry

private def splitEntries (entries : Array (TSyntax `entry)) : (Array Ident) × (Array Ident) :=
  entries.foldl (init := (#[], #[])) fun (ls, rs) => fun
    | `(entry|$l:ident : $r) => (ls.push l, rs.push r)
    | _                      => unreachable!

macro "create" a:ident "{" entries:entry* "}" : command => do
  let (ls, rs) := splitEntries entries
  let rIdent := mkIdent `R
  let vars ← (#[a] ++ rs).mapM fun r => `(variable ($r : $rIdent))
  let defs ← ls.mapM fun l => `(def $l : Prop := true)
  let cmds := vars ++ defs
  return ⟨mkNullNode cmds⟩

create A {
  B : C
  D : E
  F : G
}

#check A -- A : R
#check B -- B : Prop

(For an explanation of the mkNullNode, see https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Antiquot.20Splice/near/297760730)

[Codegoblin]

@Marcus Rossel Thank you VERY much. Not only did you show me the entry "trick", you also showed how to join multiple Command outputs. I could apply it perfectly to my Problem. :smiley: