Documentation

Lean.ParserCompiler

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

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

Type

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

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

Equations

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

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

Equations

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

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

Lean.MetaM (Option Lean.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 α) :

Precondition: α must match ctx.tyName.

Equations

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