Introducing Partax, the Parser Compiler

Stream: lean4

[Mac Malone]

Hello everyone! I have been working on a little library I would like to showcase: Partax. It is inspired by an old PoC I discussed with with @Siddharth Bhat and @Andrés Goens in 2022 that I have since turned into a full library.

Partax compiles Lean syntax and parser definitions into something else. The "something else" is configurable, but the motivating example is a monadic parser (LParse) that does not require a Lean Environment. Thus, with Partax, grammars written in Lean can be compiled down into more elementary parsers for use in projects that do not wish to depend on Lean symbols or metaprogramming code. Currently, Partax can compile all Lean parsers and syntax declarations, but compiling large categories (e.g., term, tactic, or command) can take some time (e.g., a few minutes). Partax's parser can parse everything except for antiquotations and a few unsupported special parsers (e.g., parserOfStack). It is also missing some optimizations (e.g., syntax caching). In practice, this means that it can parse any Lean file that does not use antiquotations or add and then use new syntax.

Here is an example use of Partax from the README:

import Lean
import Partax

open scoped Partax

compile_parser Lean.Parser.Term.attributes => attrs
#eval attrs.run' "@[instance high, inline]" -- TSyntax `Lean.Parser.Term.attributes

compile_parser_category prio
#eval prio.run' "default + default" -- TSyntax `prio

open Lean Elab Command in -- 2000
#eval liftMacroM (m := CommandElabM) do
  match prio.run' "default + default" with
  | .ok stx => evalPrio stx
  | .error e => Macro.throwError e

If this looks interesting, give it a try! I happily welcome any bug reports, feature requests, or contributions. Also, the documentation is somewhat sparse, so please feel free to ask for explanations or clarifications.