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

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

• varName : Lake.Name
• categoryAttr : Lean.KeyedDeclsAttribute α
• combinatorAttr : Lean.ParserCompiler.CombinatorAttribute

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

Equations

• Lean.ParserCompiler.Context.tyName ctx = ctx.categoryAttr.defn.valueTypeName

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

Replace all references of Parser with tyName

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.ParserCompiler.parserNodeKind? (e : Lean.Expr) : Lean.MetaM (Option Lake.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 : Lean.ParserCompiler.Context α) (builtin : Bool) (force : Bool) (e : Lean.Expr) : Lean.MetaM Lean.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 : Lean.ParserCompiler.Context α) (builtin : Bool) : Lean.ParserDescr → Lean.MetaM Unit

Equations

• One or more equations did not get rendered due to their size.
• Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.const name) = pure ()
• Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.unary name d) = Lean.ParserCompiler.compileEmbeddedParsers ctx builtin d
• Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.parser constName) = discard (Lean.ParserCompiler.compileParserExpr ctx builtin false (Lean.mkConst constName))
• Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.node kind prec d) = Lean.ParserCompiler.compileEmbeddedParsers ctx builtin d
• Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.nodeWithAntiquot name kind d) = Lean.ParserCompiler.compileEmbeddedParsers ctx builtin d
• Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.trailingNode kind prec lhsPrec d) = Lean.ParserCompiler.compileEmbeddedParsers ctx builtin d
• Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.symbol val) = pure ()
• Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.nonReservedSymbol val includeIdent) = pure ()
• Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.cat catName rbp) = pure ()

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

Precondition: α must match ctx.tyName.

Equations

• One or more equations did not get rendered due to their size.