Parser generator

Stream: Is there code for X?

[Jiahua Chen]

(unsure if this is the right stream to put this, this is more metaprogramming related)

I'm trying to implement a DSL in Lean (specifically, generating Lean statements from a logical specification language). Part of that involves implementing custom syntax in Lean, I've been following metaprogramming in Lean as a guide.

A lot of my code related to syntax has followed the following pattern: creating (mutual) inductive types for the different types of syntax, creating syntax categories, defining elaborators that translates from custom syntax to our syntax type. A lot of which is really mechanical.

Is there anything that might resemble a parser generator for Lean? I'm thinking something like Menhir that allows one to define the grammar in a file and generate the custom syntax for it. It might be useful for more general metaprogramming, especially using Lean to interact with other languages. If not, is this something that might be desirable? (I don't mind taking a hack at it).

[Scott Morrison]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Parsec.20parser.20for.20decoding.20Uri.20escapes/near/397698455 for some useful links.

[Jiahua Chen]

Thanks! I'll have a look through. These seem promising.