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

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

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

Instances For

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

- ctx.tyName = ctx.categoryAttr.defn.valueTypeName

Instances For

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

Replace all references of `Parser` with `tyName`

Equations

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

Instances For

source
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.

source
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.

source
def Lean.ParserCompiler.compileEmbeddedParsers {α : Type} (ctx : Context α) (builtin : Bool) :
ParserDescr → 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.unicodeSymbol val asciiVal preserveForPP) = pure ()
- Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.cat catName rbp) = pure ()

Instances For

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

Precondition: `α` must match `ctx.tyName`.

Equations

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

Instances For