Currently the Lean ecosystem doesn't have a tool for generating parser code from grammar definitions. At work, we have an internal language that is quite large in terms of constructs but syntactically simple. I found BNFC and am considering to use it for having a unified definition as the source for the Lean parser + tree-sitter highlighting + C/C++ backend for blazingly fast™ parsing when it matters.
Would you be open to accept PRs to add a Lean backend? Obviously subject to implementation quality.
Currently the Lean ecosystem doesn't have a tool for generating parser code from grammar definitions. At work, we have an internal language that is quite large in terms of constructs but syntactically simple. I found BNFC and am considering to use it for having a unified definition as the source for the Lean parser + tree-sitter highlighting + C/C++ backend for blazingly fast™ parsing when it matters.
Would you be open to accept PRs to add a Lean backend? Obviously subject to implementation quality.