points by dunham 2 days ago | 0 comments
The table-driven aspect is nice when you have user defined operators. I've used it inside a combinator based parser for a language with mixfix operators (e.g. _≡⟨_⟩_ ).
Lean4 takes this to an extreme and has "syntax categories" (e.g. expression), each of which has something like a pratt parser. Ambiguity is broken by taking the option that makes the most progress, and it is made efficient by memoization. You can add syntax at compile time, down to the lexing level. There is an example that adds HTML-like syntax and uses it later in the same file.
https://github.com/leanprover/lean4/blob/0f2eaa6e776255083f9...
(I'm not saying changing the language on the fly is a good idea, but it's interesting that they pulled it off.)
Aún no hay comentarios.