Creating SyntaxNodeKinds for parsers

Stream: lean4

[Thomas Murrills]

How do you define a term elaborator for a manually-defined parser (via e.g. def myParser : Parser := ...? With syntax, you can use syntax (name := myNodeName) ... and then write @[termElab myNodeName]—but I'm not sure how to attach a SyntaxNodeKind to what's consumed by a manually-defined parser. (I would have expected the SyntaxNodeKind to be myParser, but it doesn't seem to be created automatically.)

[Gabriel Ebner]

Usually the best approach is to use elab_rules:

import Lean
syntax "my_syntax" term : term
elab_rules <= expectedType
  | `(my_syntax $t) => Lean.Elab.Term.elabTerm t expectedType

[Gabriel Ebner]

I would have expected the SyntaxNodeKind to be myParser, but it doesn't seem to be created automatically.

Right, you need to create the node explicitly. We usually do this with the leading_parser macro:

def myParser : Parser := leading_parser ...

This will add a node (with the parser declaration name as the syntax kind), and also a $foo:myParser antiquotation.

[Thomas Murrills]

Hmmm…I am using leading_parser, but it still doesn’t like @[termElab myParser]. #check shows that I do have access to the parser I defined, so it’s not something silly…I’ll investigate a bit! Should I expect that elab will recognize it as a valid SyntaxNodeKind while @[termElab …] won’t?

[Gabriel Ebner]

Please post an #mwe!

[Thomas Murrills]

Ah! Thanks for asking me to—I figured it out while trying to make the #mwe. I hadn't marked the parser with the attribute @[termParser], so termElab didn't know that this parser parsed terms! 🙃