generating inductive syntax

Stream: lean4

[James Gallicchio]

Still largely unfamiliar with metaprogramming, so I'm sure I am missing something obvious, but how do I generate the TSyntax `Lean.Parser.Command.ctor necessary for this metaprogram to work?

def keywordsRaw := #[
    "struct"
  , "typedef"
  , "if"
  , "..." ]

open Lean Macro in
scoped macro "genKeywordType!" : command => do
  `(inductive $(mkIdent `Keyword) : Type where
    $[ $(
      keywordsRaw.map (fun kw => sorry)
    ) ]*
  )

I've tried lots of different quotations to try to fill in the sorry, but haven't found the right one. I see from the parser for ctor that it should look something like `(| $kw) but that does not work. I also can't find any documentation in the metaprogramming book or on zulip about how to generate inductive decl syntax D:

Should I just be building an elab command instead of a macro for this?

[Mario Carneiro]

I think you probably don't want to generate the ctor yourself; it looks like you just want to make an identifier

[Mario Carneiro]

in which case you can do something like

scoped macro "genKeywordType!" : command => do
  `(inductive $(mkIdent `Keyword) : Type where
    $[ | $(keywordsRaw):ident ]*
  )

[James Gallicchio]

aha!

scoped macro "genKeywordType!" : command => do
  `(inductive $(mkIdent `Keyword) : Type where
    $[ | $(keywordsRaw.map mkIdent):ident ]*
  )

[James Gallicchio]

what does the :ident do there? if i remove it Lean complains about a syntax error at the $[! :joy:

[Mario Carneiro]

A general antiquotation could be standing in for a variety of syntax categories, so it is somewhat ambiguous for the parser

[James Gallicchio]

Got it. So when I have weird parse errors I should annotate my antiquotations.

[Mario Carneiro]

it can't use type information because it is happening at parse time