What to pass to `categoryParserFn` for it to work?

Stream: lean4

[nrs]

I'm digging around Lean.Parser and trying to get individual parsers to work. Some of these work with empty contexts and environments, but not categoryParserFn. What do I need to initialize to, e.g., have ParserFn.run (categoryParserFn ``command) parse def mynat : Nat := 2?

[Mario Carneiro]

you need to run the initializer for Lean

[Mario Carneiro]

this populates the global tables used by the parser

[Mario Carneiro]

the way you run the initializer depends on how you got yourself in a situation where they haven't been run yet

[nrs]

Mario Carneiro said:

the way you run the initializer depends on how you got yourself in a situation where they haven't been run yet

I see thanks a lot for the answer! what parts of source should I look at to learn how the initializer is ran or how it works? (the easy way out is to use the fact that the initializer has in fact been ran and that I have a working environment I'm importing Lean.Parser in, but I want to understand the internals better)

[Mario Carneiro]

The parser table is not stored in the environment, so once you have run the initializer it will work even in the empty environment

[Mario Carneiro]

this is important, because otherwise lean would not be able to parse Prelude.lean, the first lean file

[Mario Carneiro]

Because these are "builtin parsers", they are run as part of the function initialize_Lean which runs all the initializers. The way these function calls ended up in this function is a bit convoluted, but goes via the @[builtin_init] attribute and a bootstrap stage

[Mario Carneiro]

but the starting point is the use of @[builtin_command_parser] e.g. here

[nrs]

Mario Carneiro said:

The parser table is not stored in the environment, so once you have run the initializer it will work even in the empty environment

hm, I am however getting a kernel panic from the following (crude I know) code. Other parsers that do not depend on something else than the context's input, such as strLitFnAux, do successfully parse when called in this way

import Lean.Parser
import Lean.Data
open Lean.Parser Lean

def mkInputContext' (str : String) : InputContext := .mk str "" (.mk "" #[])

def tempmain : IO Unit := do
  let emptyenv : Environment := (<- mkEmptyEnvironment)
  let emptyParserModuleContext : ParserModuleContext := .mk emptyenv (.mk []) .anonymous []
  let emptyTrie : Lean.Data.Trie Token := Lean.Data.Trie.empty
  let emptyTokenCacheEntry : TokenCacheEntry := .mk 0 0 .missing
  let emptyParserCache : ParserCache := .mk emptyTokenCacheEntry .empty
  let emptyParserState : ParserState := .mk .empty 0 0 emptyParserCache .none #[]

  let result := ParserFn.run (categoryParserFn `command) (mkInputContext' "def mynat : Nat := 2") emptyParserModuleContext emptyTrie emptyParserState
  dbg_trace result.stxStack.toSubarray

#eval tempmain

[nrs]

Using the current env instead (from /tests):

def withCurrentEnv : CoreM Unit := do
  let stx <- ofExcept <| Parser.runParserCategory (<- getEnv) `command "def mynat : Nat := 2"
  dbg_trace stx

[nrs]

I will be removing each piece of the environment until I figure out the critical objects for this to work, will report back (but do let me know if I should be focusing on something!)

[nrs]

The following works and seems to be the minimal initialization necessary to make categoryParserFn work

def tempmain : IO Unit := do
  let env : Environment := (<- makeEmptyEnvironment)
  let emptyParserModuleContext : ParserModuleContext := .mk env (.mk []) .anonymous []
  let pcache : ParserCache := initCacheForInput ""
  let emptyParserState : ParserState := .mk .empty 0 0 pcache .none #[]
  let result := ParserFn.run (categoryParserFn `command) (Parser.mkInputContext "def mynat : Nat := 2" "") emptyParserModuleContext (getTokenTable env) emptyParserState
  dbg_trace result.stxStack.toSubarray

[Mario Carneiro]

oh yes, the initial token table comes from the global state I mentioned, but the parser itself carries (non-global) state so it can handle files that change the parser in the middle of the file