Creating a wrapper for a Term quotiation

Stream: general

[Codegoblin]

Hello Lean Community,

I am trying to add comments to all of my syntax declarations via wrappers to both syntax declarations and the matching of said syntax.

I have already created a wrapper for syntax creation, which adds a syntax parser (for comments) between every element of the syntax defined by the user.

Syntax with comment

declare_syntax_cat syntax_with_comments_element

  syntax str : syntax_with_comments_element

  syntax ident : syntax_with_comments_element

  /--

  A call to syntax_with_comments is like a call to syntax, except

  between every element of the syntax the comment syntax_category is added

  -/

  syntax

    (name := syntax_with_comments_stx)

    ("#")? "syntax_with_comments" (syntax_with_comments_element)* ":" ident : command

  private def evaluate_syntax_creation

  (elements :TSyntaxArray `syntax_with_comments_element)

  (stx_cat : Ident)

  : Command

  := Unhygienic.run do

  let comment_stx ← `(stx | ($(mkIdent `comment):ident)?)

  let mut elements_as_stx : Array (TSyntax `stx) := #[comment_stx]

  for element in elements do

    match element with

      | `(syntax_with_comments_element | $str_element:str) =>

        let str_element_stx ← `(stx | $(str_element):str)

        elements_as_stx := elements_as_stx.push str_element_stx

        elements_as_stx := elements_as_stx.push comment_stx

      | `(syntax_with_comments_element | $ident_element:ident) =>

        let ident_element_stx ← `(stx | $(ident_element):ident)

        elements_as_stx := elements_as_stx.push ident_element_stx

        elements_as_stx := elements_as_stx.push comment_stx

      | _ => unreachable!

  return ← `(command | syntax $[$elements_as_stx]* : $stx_cat)

  @[command_elab syntax_with_comments_stx]

  private def syntax_with_comments_implementation : CommandElab := fun stx => do

    try

      match stx with

        | `(

            # syntax_with_comments

            $elements:syntax_with_comments_element*

            : $stx_cat:ident

          ) =>

          let s := (evaluate_syntax_creation elements stx_cat)

          logInfo s

          elabCommand s

        | `(

            syntax_with_comments

            $elements:syntax_with_comments_element*

            : $stx_cat:ident

          ) =>

          let s := (evaluate_syntax_creation elements stx_cat)

          elabCommand s

        | _ => return

    catch | x => throwError x.toMessageData

This transforms the following syntax

declare_syntax_cat example_stx_cat
#syntax_with_comments  "example_stx"  : example_stx_cat

to a syntax declaration of

syntax (comment)? "example_stx" (comment)? : example_stx_cat

Now I want to 'ignore' the comments in all matches, for this purpose I would like to wrap quotations to add an optional match like

$[$_:comment]?

between every element.

E.g. I would like to create the following function

def canMatch (i : TSyntax `example_stx_cat) : Bool :=
  match i with
    | `(example_stx_cat | $[$_:comment]? example_stx $[$_:comment]?) => true
    | _ => false

more like this

def canMatch (i : TSyntax `example_stx_cat) : Bool :=
  match i with
    | syntax_match_with_comments `(example_stx_cat |  example_stx ) => true
    | _ => false

Now I do not know how I can add the comment matches to the quotation. So far I have the following:

quote match

syntax

  (name := syntax_match_with_comments_stx)

  ("#")? "syntax_match_with_comments"

  Parser.Term.dynamicQuot : term

@[term_elab syntax_match_with_comments_stx]

private def syntax_match_with_comments_implementation

: TermElab := fun stx expectedType? => do

    match stx with

      | `(

          # syntax_match_with_comments

          $syntax_match_quote:dynamicQuot

        ) =>

        logInfo syntax_match_quote

        elabTerm

          syntax_match_quote

          expectedType?

      | `(

            syntax_match_with_comments

            $syntax_match_quote:dynamicQuot

        ) =>

        elabTerm

          syntax_match_quote

          expectedType?

      | syntx =>

        throwError s!"Could not create Syntax match for syntax '{syntx}'"

But if I try to deconstruct the dynamic quote or construct one like

match syntax_match_quote with
          | `(Parser.Term.dynamicQuot | `($id:ident | $s:stx)) => ...

I get the error

failed to determine parser using syntax stack, the specified element on the stack is not an identifier

Is this because I try to de/construct a quotation with a quotation? Is there a way to add the empty match ($[$_:comment]?) to the syntax of a quotation?