elaboration-based wrapper around structure

Stream: metaprogramming / tactics

[Kiran]

I am trying to write a macro that, as part of other things that it does, produces a structure definition. For reasons not included in the simplified example I've given, my macro runs at elaboration time: (I've tried searching for this, but no hits pop up for a kernal message "(kernel) constant has already been declared").

syntax "mystructure " ident " where " Parser.Command.structFields : command

elab_rules : command
| `(command| mystructure $name:ident where $t:structFields) => do
   Command.elabCommand $
     (<- `(command| structure $name:ident where $(TSyntax.mk t.raw)))

mystructure P where
   x: Nat

This fails with the error "(kernel) constant has already been declared".

[Sebastian Ullrich]

What made you try TSyntax.mk t.raw? The expected type at that point is TSyntax `structCtor, that doesn't sound like something we should squeeze structFields into to me

elab_rules : command
| `(command| mystructure $name:ident where $t:structFields) => do
   Command.elabCommand $
     (<- `(command| structure $name:ident where $t:structFields))

[Sebastian Ullrich]

Note that elab_rules vs macro_rules doesn't make any difference here

[Kiran]

Sebastian Ullrich said:
Ah, my bad, sorry, yeah, that fixes it! for whatever reason I coerced it into structCtor earlier.