Understanding syntax extension

Stream: general

[Graham Leach-Krouse]

I'm trying to understand Lean's syntax extension mechanisms a little better. Is it possible to add a new Parser that will be recognized by the syntax command without modifying lean's core?

[Graham Leach-Krouse]

So far, I've noticed that @[term_parser] can be used to designate a Parseras eligible for use with syntax. I'm a bit unclear, though, on how to define parser combinators like withPosition - it might have something to do with @[combinator_parenthesizer ..]?

[Graham Leach-Krouse]

OK, it appears that the trick is to either:

1. Apply @[run_parser_attribute_hooks] to myparser
2. Or, use both @[combinator_formatter myparser] and @[combinator_parenthesizer myparser] to declare a Parenthesizer and a Formattermore carefully

and then use initialize register_parser_alias myparser. The new parser appears to only be recognized in files that import the file where it is registered, not in the registering file. (This restriction appears not to apply to @[term_parser] for some reason.)

I wonder, is this written down anywhere? A paper, a blog post?

[Kyle Miller]

Maybe this is helpful? #general > How can I parse custom tokens with the Lean Parser? @ 💬

[Graham Leach-Krouse]

Thanks! I saw that - the example from verso is helpful.

Another example I found was:

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Util/Superscript.lean

Both of them, I think, suggest that the approach above (@[run_parser_attribute_hooks] or @[combinator_*] plus register_parser_alias) is not completely an abuse of something that's intended to be an internal interface. It would be nice to be able to understand this a little bit more though!