- varName : Lean.Name
- categoryAttr : Lean.KeyedDeclsAttribute α
- combinatorAttr : Lean.ParserCompiler.CombinatorAttribute
Equations
- Lean.ParserCompiler.Context.tyName ctx = ctx.categoryAttr.defn.valueTypeName
def
Lean.ParserCompiler.replaceParserTy
{α : Type}
(ctx : Lean.ParserCompiler.Context α)
(e : Lean.Expr)
:
Equations
- Lean.ParserCompiler.replaceParserTy ctx e = Lean.Expr.replace (fun e => let e := if Lean.Expr.isOptParam e = true then Lean.Expr.appArg! (Lean.Expr.appFn! e) else e; if Lean.Expr.isConstOf e `Lean.Parser.Parser = true then some (Lean.mkConst (Lean.ParserCompiler.Context.tyName ctx)) else none) e
partial def
Lean.ParserCompiler.compileParserExpr
{α : Type}
(ctx : Lean.ParserCompiler.Context α)
(builtin : Bool)
(force : Bool)
(e : Lean.Expr)
:
def
Lean.ParserCompiler.compileEmbeddedParsers
{α : Type}
(ctx : Lean.ParserCompiler.Context α)
(builtin : Bool)
:
Equations
- Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.const x_1) = pure ()
- Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.unary x_1 d) = Lean.ParserCompiler.compileEmbeddedParsers ctx builtin d
- Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.binary x_1 d₁ d₂) = SeqRight.seqRight (Lean.ParserCompiler.compileEmbeddedParsers ctx builtin d₁) fun x => 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 x_1 x_2 d) = Lean.ParserCompiler.compileEmbeddedParsers ctx builtin d
- Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.nodeWithAntiquot x_1 x_2 d) = Lean.ParserCompiler.compileEmbeddedParsers ctx builtin d
- Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.sepBy p x_1 psep x_2) = SeqRight.seqRight (Lean.ParserCompiler.compileEmbeddedParsers ctx builtin p) fun x => Lean.ParserCompiler.compileEmbeddedParsers ctx builtin psep
- Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.sepBy1 p x_1 psep x_2) = SeqRight.seqRight (Lean.ParserCompiler.compileEmbeddedParsers ctx builtin p) fun x => Lean.ParserCompiler.compileEmbeddedParsers ctx builtin psep
- Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.trailingNode x_1 x_2 x_3 d) = Lean.ParserCompiler.compileEmbeddedParsers ctx builtin d
- Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.symbol x_1) = pure ()
- Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.nonReservedSymbol x_1 x_2) = pure ()
- Lean.ParserCompiler.compileEmbeddedParsers ctx builtin (Lean.ParserDescr.cat x_1 x_2) = pure ()
unsafe def
Lean.ParserCompiler.registerParserCompiler
{α : Type}
(ctx : Lean.ParserCompiler.Context α)
:
Equations
- Lean.ParserCompiler.registerParserCompiler ctx = Lean.Parser.registerParserAttributeHook { postAdd := fun catName constName builtin => do let info ← Lean.getConstInfo constName if (Lean.Expr.isConstOf (Lean.ConstantInfo.type info) `Lean.ParserDescr || Lean.Expr.isConstOf (Lean.ConstantInfo.type info) `Lean.TrailingParserDescr) = true then do let d ← HOrElse.hOrElse (Lean.evalConstCheck Lean.ParserDescr `Lean.ParserDescr constName) fun x => Lean.evalConstCheck Lean.TrailingParserDescr `Lean.TrailingParserDescr constName Lean.Meta.MetaM.run' (Lean.ParserCompiler.compileEmbeddedParsers ctx builtin d) { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, transparency := Lean.Meta.TransparencyMode.default, zetaNonDep := true, trackZeta := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, ignoreLevelMVarDepth := true, offsetCnstrs := true, etaStruct := true }, lctx := { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none } { mctx := { depth := 0, mvarCounter := 0, lDepth := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, cache := { inferType := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEqDefault := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEqAll := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := ∅, postponed := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } } else let force := Lean.Name.isAnonymous catName; discard (Lean.Meta.MetaM.run' (Lean.ParserCompiler.compileParserExpr ctx builtin force (Lean.mkConst constName)) { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, transparency := Lean.Meta.TransparencyMode.default, zetaNonDep := true, trackZeta := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, ignoreLevelMVarDepth := true, offsetCnstrs := true, etaStruct := true }, lctx := { fvarIdToDecl := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none } { mctx := { depth := 0, mvarCounter := 0, lDepth := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, cache := { inferType := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEqDefault := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEqAll := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := ∅, postponed := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }) }