Gadgets for compiling parser declarations into other programs, such as pretty printers.

structure Lean.ParserCompiler.Context (α : Type) : Type

• varName : Name
• categoryAttr : KeyedDeclsAttribute α
• combinatorAttr : CombinatorAttribute

def Lean.ParserCompiler.Context.tyName {α : Type} (ctx : Context α) : Name

def Lean.ParserCompiler.replaceParserTy {α : Type} (ctx : Context α) (e : Expr) : Expr

Replace all references of Parser with tyName

partial def Lean.ParserCompiler.parserNodeKind? (e : Expr) : MetaM (Option Name)

Takes an expression of type Parser, and determines the syntax kind of the root node it produces.

partial def Lean.ParserCompiler.compileParserExpr {α : Type} (ctx : Context α) (builtin force : Bool) (e : Expr) : MetaM Expr

Translate an expression of type Parser into one of type tyName, tagging intermediary constants with ctx.combinatorAttr. If force is false, refuse to do so for imported constants.

def Lean.ParserCompiler.compileEmbeddedParsers {α : Type} (ctx : Context α) (builtin : Bool) : ParserDescr → MetaM Unit

unsafe def Lean.ParserCompiler.registerParserCompiler {α : Type} (ctx : Context α) : IO Unit

Precondition: α must match ctx.tyName.