Lean.PrettyPrinter

source

def Lean.PPContext.runCoreM {α : Type} (ppCtx : Lean.PPContext) (x : Lean.CoreM α) :

IO α

Equations

Lean.PPContext.runCoreM ppCtx x = Prod.fst <$> Lean.Core.CoreM.toIO x { options := ppCtx.opts, currRecDepth := 0, maxRecDepth := 1000, ref := Lean.Syntax.missing, currNamespace := ppCtx.currNamespace, openDecls := ppCtx.openDecls, initHeartbeats := 0, maxHeartbeats := Lean.Core.getMaxHeartbeats ppCtx.opts } { env := ppCtx.env, nextMacroScope := Lean.firstFrontendMacroScope + 1, ngen := { namePrefix := `_pp_uniq, idx := 1 }, traceState := { enabled := true, traces := { 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 } } }

source

def Lean.PPContext.runMetaM {α : Type} (ppCtx : Lean.PPContext) (x : Lean.MetaM α) :

IO α

Equations

Lean.PPContext.runMetaM ppCtx x = Lean.PPContext.runCoreM ppCtx (Lean.Meta.MetaM.run' x { 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 := ppCtx.lctx, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none } { mctx := ppCtx.mctx, 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 } })

source

def Lean.PrettyPrinter.ppTerm (stx : Lean.Syntax) :

Lean.CoreM Lean.Format

Equations

Lean.PrettyPrinter.ppTerm stx = Lean.getOptions >>= fun opts => let stx := StateT.run' (Lean.sanitizeSyntax stx) { options := opts, nameStem2Idx := ∅, userName2Sanitized := ∅ }; Lean.PrettyPrinter.parenthesizeTerm stx >>= Lean.PrettyPrinter.formatTerm

source

def Lean.PrettyPrinter.ppExpr (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (e : Lean.Expr) :

Lean.MetaM Lean.Format

Equations

Lean.PrettyPrinter.ppExpr currNamespace openDecls e = do let lctx ← Lean.getLCtx let opts ← Lean.getOptions let lctx : Id Lean.LocalContext := StateT.run' (Lean.LocalContext.sanitizeNames lctx) { options := opts, nameStem2Idx := ∅, userName2Sanitized := ∅ } Lean.Meta.withLCtx lctx #[] do let stx ← Lean.PrettyPrinter.delab currNamespace openDecls e ∅ liftM (Lean.PrettyPrinter.ppTerm stx)

source

def Lean.PrettyPrinter.ppExprLegacy (env : Lean.Environment) (mctx : Lean.MetavarContext) (lctx : Lean.LocalContext) (opts : Lean.Options) (e : Lean.Expr) :

IO Lean.Format

Equations

Lean.PrettyPrinter.ppExprLegacy env mctx lctx opts e = Prod.fst <$> Lean.Core.CoreM.toIO (Lean.Meta.MetaM.run' (Lean.PrettyPrinter.ppExpr Lean.Name.anonymous [] e) { 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 := lctx, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none } { mctx := mctx, 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 } }) { options := opts, currRecDepth := 0, maxRecDepth := 1000, ref := Lean.Syntax.missing, currNamespace := Lean.Name.anonymous, openDecls := [], initHeartbeats := 0, maxHeartbeats := Lean.Core.getMaxHeartbeats opts } { env := env, nextMacroScope := Lean.firstFrontendMacroScope + 1, ngen := { namePrefix := `_uniq, idx := 1 }, traceState := { enabled := true, traces := { 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 } } }

source

def Lean.PrettyPrinter.ppCommand (stx : Lean.Syntax) :

Lean.CoreM Lean.Format

Equations

Lean.PrettyPrinter.ppCommand stx = Lean.PrettyPrinter.parenthesizeCommand stx >>= Lean.PrettyPrinter.formatCommand

source

def Lean.PrettyPrinter.ppModule (stx : Lean.Syntax) :

Lean.CoreM Lean.Format

Equations

Lean.PrettyPrinter.ppModule stx = Lean.PrettyPrinter.parenthesize Lean.Parser.Module.module.parenthesizer stx >>= Lean.PrettyPrinter.format Lean.Parser.Module.module.formatter

source

unsafe def Lean.PrettyPrinter.registerParserCompilers :

IO Unit

Equations

Lean.PrettyPrinter.registerParserCompilers = do Lean.ParserCompiler.registerParserCompiler { varName := `parenthesizer, categoryAttr := Lean.PrettyPrinter.parenthesizerAttribute, combinatorAttr := Lean.PrettyPrinter.combinatorParenthesizerAttribute } Lean.ParserCompiler.registerParserCompiler { varName := `formatter, categoryAttr := Lean.PrettyPrinter.formatterAttribute, combinatorAttr := Lean.PrettyPrinter.combinatorFormatterAttribute }