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.

[Eduardo Ochs]

Hi! A beginner question, based on this test from tests/lcompile.lean...

How do we write a command def_from_match_stx that makes the two "#" lines in this example print the same result?

#match_stx term term | 2 + 2 = 4
def_from_match_stx a224 := term term | 2 + 2 = 4
#eval a224

[Eduardo Ochs]

Would this be possible too?

#match_stx term term | 2 + 2 = 4
-- The next two lines should be equivalent:
-- def_from_match_stx a224 := term term | 2 + 2 = 4
   def a224 := from_match_stx term term | 2 + 2 = 4
#eval a224

[Mac Malone]

@Eduardo Ochs I am confused as to what you are trying to do here. What is from_mathc_stx meant to do? The #match_stx command in Partax is a helper command for its unit tests -- it is not really meant for end users.