using syntax parsers at runtime

Stream: lean4

[Joachim Breitner]

Can I use lean’s syntax declaration to define parsers that I want to use at _runtime_ of my program?

syntax test := "some" ident

unsafe def main : IO Unit := do
  let input := "some test"
  let parsed_input : Lean.Syntax := _ -- what do I put here to apply `test` to `input`

[Mac Malone]

@Joachim Breitner This was the motivating use case behind my package, Partax.

import Partax
open scoped Partax

syntax test := "some" ident

namespace Parser
compile_parser test
end Parser

def main : IO Unit := do
  let input := "some test"
  let parsedInput ← IO.ofExcept <| Parser.test.run' input
  -- ...
  IO.println parsedInput

#eval main -- (test "some" `test)

[Joachim Breitner]

Great, will try that tomorrow! I'm a bit relieved that there isn't a simple way that I failed to figure out :-)

[Joachim Breitner]

Kyle Miller said:

Could you say a little bit about why find_patterns is a syntax category in the PR? I don't really understand "so that it can be used by external tools".

(moving this question to a separate topic)

This was the only way so far I managed to access this parser at runtime, which I need in the loogle tool, using this code:
https://github.com/nomeata/loogle/blob/ac0b5ff07276449df091bd2f30ef31a589547391/Loogle.lean#L31
I was mostly guessing and cargo-culting, and am happy to learn of better ways.

I did not yet investigate Partax, it seems then I wouldn’t need a syntax category. Let me do that right away. (Although I wish lean would just allow me to use parsers at runtime without extra tools…)

[Kyle Miller]

@Joachim Breitner I've never tried this before and I might be doing it wrong, but here's a runParser function that takes a declaration name for the syntax.

import Lean

/-- The turnstyle for conclusion patterns, unicode or ascii allowed -/
syntax turnstyle := patternIgnore(" ⊢ " <|> " |- ")

/-- `#find` patterns -/
syntax find_patterns := term,* (turnstyle term)?

open Lean Parser

def runParser (env : Environment) (declName : Name) (input : String) (fileName := "<input>") : Except String Syntax :=
  let p := andthenFn whitespace (evalParserConst declName)
  let ictx := mkInputContext input fileName
  let s := p.run ictx { env, options := {} } (getTokenTable env) (mkParserState input)
  if s.hasError then
    Except.error (s.toErrorMsg ictx)
  else if input.atEnd s.pos then
    Except.ok s.stxStack.back
  else
    Except.error ((s.mkError "end of input").toErrorMsg ictx)

#eval do
  let env ← (getEnv : Elab.TermElabM _)
  match runParser env ``find_patterns "1 + 1 ⊢ x" with
  | .ok s => logInfo m!"ok: {s}"
  | .error e => logError m!"error: {e}"

[Kyle Miller]

(The particular syntax declarations are just for testing, and I don't mean to suggest anything about how #find should work.)

[Joachim Breitner]

Hmm, using partax to compile the term parsers certainly adds noticably friction to the development process. It seems cleaner if loogle doesn't use the environment of the loaded .olean, but not sure if the extra build time is worth it. Hmm.

[Joachim Breitner]

Thanks, Kyle, that code seems to work. Using it now in loogle and removed the syntax category from the #find PR

[Mac Malone]

Joachim Breitner said:

Hmm, using partax to compile the term parsers certainly adds noticably friction to the development process.

Yeah, compiling the whole Lean grammar is unfortunately currently slow in Partax.