Lean.PrettyPrinter.Delaborator.Basic

Lean.PrettyPrinter.Delaborator.instAlternativeDelabM = Alternative.mk (fun {α} => Lean.PrettyPrinter.Delaborator.failure) fun {α} => Lean.PrettyPrinter.Delaborator.orElse

source

instance Lean.PrettyPrinter.Delaborator.instOrElseDelabM {α : Type} :

OrElse (Lean.PrettyPrinter.Delaborator.DelabM α)

Equations

Lean.PrettyPrinter.Delaborator.instOrElseDelabM = { orElse := Lean.PrettyPrinter.Delaborator.orElse }

source

instance Lean.PrettyPrinter.Delaborator.instMonadReaderOfSubExprDelabM :

MonadReaderOf Lean.PrettyPrinter.Delaborator.SubExpr Lean.PrettyPrinter.Delaborator.DelabM

Equations

Lean.PrettyPrinter.Delaborator.instMonadReaderOfSubExprDelabM = { read := Lean.PrettyPrinter.Delaborator.Context.subExpr <$> read }

source

instance Lean.PrettyPrinter.Delaborator.instMonadWithReaderOfSubExprDelabM :

MonadWithReaderOf Lean.PrettyPrinter.Delaborator.SubExpr Lean.PrettyPrinter.Delaborator.DelabM

Equations

Lean.PrettyPrinter.Delaborator.instMonadWithReaderOfSubExprDelabM = { withReader := fun {α} f x ctx => x { defaultOptions := ctx.defaultOptions, optionsPerPos := ctx.optionsPerPos, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls, inPattern := ctx.inPattern, subExpr := f ctx.subExpr } }

source

instance Lean.PrettyPrinter.Delaborator.instMonadStateOfHoleIteratorDelabM :

MonadStateOf Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator Lean.PrettyPrinter.Delaborator.DelabM

Equations

Lean.PrettyPrinter.Delaborator.instMonadStateOfHoleIteratorDelabM = { get := Lean.PrettyPrinter.Delaborator.State.holeIter <$> get, set := fun iter => modify fun x => match x with | { infos := infos, holeIter := x } => { infos := infos, holeIter := iter }, modifyGet := fun {α} f => modifyGet fun x => match x with | { infos := infos, holeIter := iter } => let x := f iter; match x with | (ret, iter') => (ret, { infos := infos, holeIter := iter' }) }

source

instance Lean.PrettyPrinter.Delaborator.instMonadQuotationDelabM :

Lean.MonadQuotation Lean.PrettyPrinter.Delaborator.DelabM

Equations

Lean.PrettyPrinter.Delaborator.instMonadQuotationDelabM = Lean.MonadQuotation.mk (pure default) (pure default) fun {α} x => x

source

unsafe def Lean.PrettyPrinter.Delaborator.mkDelabAttribute :

IO (Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Delaborator.Delab)

Equations

Lean.PrettyPrinter.Delaborator.mkDelabAttribute = Lean.KeyedDeclsAttribute.init { builtinName := `builtinDelab, name := `delab, descr := "Register a delaborator.\n\n [delab k] registers a declaration of type `Lean.PrettyPrinter.Delaborator.Delab` for the `Lean.Expr`\n constructor `k`. Multiple delaborators for a single constructor are tried in turn until\n the first success. If the term to be delaborated is an application of a constant `c`,\n elaborators for `app.c` are tried first; this is also done for `Expr.const`s (\"nullary applications\")\n to reduce special casing. If the term is an `Expr.mdata` with a single key `k`, `mdata.k`\n is tried first.", valueTypeName := `Lean.PrettyPrinter.Delaborator.Delab, evalKey := fun builtin stx => Lean.Attribute.Builtin.getId stx, onAdded := fun builtin declName => pure () } `Lean.PrettyPrinter.Delaborator.delabAttribute

source

constant Lean.PrettyPrinter.Delaborator.delabAttribute :

Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Delaborator.Delab

source

def Lean.PrettyPrinter.Delaborator.getExprKind :

Lean.PrettyPrinter.Delaborator.DelabM Lean.Name

Equations

Lean.PrettyPrinter.Delaborator.getExprKind = do let e ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr pure (match e with | Lean.Expr.bvar x x_1 => `bvar | Lean.Expr.fvar x x_1 => `fvar | Lean.Expr.mvar x x_1 => `mvar | Lean.Expr.sort x x_1 => `sort | Lean.Expr.const c x x_1 => `app ++ c | Lean.Expr.app fn x x_1 => match Lean.Expr.getAppFn fn with | Lean.Expr.const c x x_2 => `app ++ c | x => `app | Lean.Expr.lam x x_1 x_2 x_3 => `lam | Lean.Expr.forallE x x_1 x_2 x_3 => `forallE | Lean.Expr.letE x x_1 x_2 x_3 x_4 => `letE | Lean.Expr.lit x x_1 => `lit | Lean.Expr.mdata m x x_1 => match m.entries with | [(key, x)] => `mdata ++ key | x => `mdata | Lean.Expr.proj x x_1 x_2 x_3 => `proj)

source

def Lean.PrettyPrinter.Delaborator.getOptionsAtCurrPos :

Lean.PrettyPrinter.Delaborator.DelabM Lean.Options

Equations

Lean.PrettyPrinter.Delaborator.getOptionsAtCurrPos = do let ctx ← read let opts : Lean.Options := ctx.defaultOptions let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getPos let a ← pure (Std.RBMap.find? ctx.optionsPerPos a) let _do_jp : Lean.Options → PUnit → Lean.PrettyPrinter.Delaborator.DelabM Lean.Options := fun opts y => pure opts match a with | some opts' => do let r ← forIn opts' opts fun x r => match x with | (k, v) => let opts := r; let opts := Lean.KVMap.insert opts k v; do pure PUnit.unit pure (ForInStep.yield opts) let x : Lean.Options := r let opts : Lean.Options := x let y ← pure PUnit.unit _do_jp opts y | x => do let y ← pure PUnit.unit _do_jp opts y

source

def Lean.PrettyPrinter.Delaborator.getPPOption (opt : Lean.Options → Bool) :

Lean.PrettyPrinter.Delaborator.DelabM Bool

Equations

Lean.PrettyPrinter.Delaborator.getPPOption opt = do let a ← Lean.PrettyPrinter.Delaborator.getOptionsAtCurrPos pure (opt a)

source

def Lean.PrettyPrinter.Delaborator.whenPPOption (opt : Lean.Options → Bool) (d : Lean.PrettyPrinter.Delaborator.Delab) :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.whenPPOption opt d = do let b ← Lean.PrettyPrinter.Delaborator.getPPOption opt if b = true then d else failure

source

def Lean.PrettyPrinter.Delaborator.whenNotPPOption (opt : Lean.Options → Bool) (d : Lean.PrettyPrinter.Delaborator.Delab) :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.whenNotPPOption opt d = do let b ← Lean.PrettyPrinter.Delaborator.getPPOption opt if b = true then failure else d

source

def Lean.PrettyPrinter.Delaborator.annotatePos (pos : Nat) (stx : Lean.Syntax) :

Lean.Syntax

Equations

Lean.PrettyPrinter.Delaborator.annotatePos pos stx = Lean.Syntax.setInfo (Lean.SourceInfo.synthetic pos pos) stx

source

def Lean.PrettyPrinter.Delaborator.annotateCurPos (stx : Lean.Syntax) :

Lean.PrettyPrinter.Delaborator.Delab

Equations

Lean.PrettyPrinter.Delaborator.annotateCurPos stx = do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getPos pure (Lean.PrettyPrinter.Delaborator.annotatePos a stx)

source

def Lean.PrettyPrinter.Delaborator.getUnusedName (suggestion : Lean.Name) (body : Lean.Expr) :

Lean.PrettyPrinter.Delaborator.DelabM Lean.Name

Equations

Lean.PrettyPrinter.Delaborator.getUnusedName suggestion body = (fun bodyUsesSuggestion => let suggestion := if Lean.Name.isAnonymous suggestion = true then `a else suggestion; let suggestion := Lean.Name.eraseMacroScopes suggestion; do let lctx ← Lean.getLCtx if (!Lean.LocalContext.usesUserName lctx suggestion) = true then pure suggestion else do let a ← Lean.PrettyPrinter.Delaborator.getPPOption Lean.getPPSafeShadowing if (a && !bodyUsesSuggestion lctx suggestion) = true then pure suggestion else pure (Lean.LocalContext.getUnusedName lctx suggestion)) (Lean.PrettyPrinter.Delaborator.getUnusedName.bodyUsesSuggestion body)

source

def Lean.PrettyPrinter.Delaborator.getUnusedName.bodyUsesSuggestion (body : Lean.Expr) (lctx : Lean.LocalContext) (suggestion' : Lean.Name) :

Bool

Equations

Lean.PrettyPrinter.Delaborator.getUnusedName.bodyUsesSuggestion body lctx suggestion' = Option.isSome (Lean.Expr.find? (fun x => match x with | Lean.Expr.fvar fvarId x => match Lean.LocalContext.find? lctx fvarId with | none => false | some decl => Lean.LocalDecl.userName decl == suggestion' | x => false) body)

source

def Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName {α : Type} (d : Lean.Syntax → Lean.PrettyPrinter.Delaborator.DelabM α) :

Lean.PrettyPrinter.Delaborator.DelabM α

Equations

Lean.PrettyPrinter.Delaborator.withBindingBodyUnusedName d = do let a ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let a_1 ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr let n ← Lean.PrettyPrinter.Delaborator.getUnusedName (Lean.Expr.bindingName! a) (Lean.Expr.bindingBody! a_1) let stxN ← Lean.PrettyPrinter.Delaborator.annotateCurPos (Lean.mkIdent n) Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody n (d stxN)

source

@[inline]

def Lean.PrettyPrinter.Delaborator.liftMetaM {α : Type} (x : Lean.MetaM α) :

Lean.PrettyPrinter.Delaborator.DelabM α

Equations

Lean.PrettyPrinter.Delaborator.liftMetaM x = liftM x

source

def Lean.PrettyPrinter.Delaborator.addTermInfo (pos : Lean.PrettyPrinter.Delaborator.Pos) (stx : Lean.Syntax) (e : Lean.Expr) (isBinder : optParam Bool false) :

Lean.PrettyPrinter.Delaborator.DelabM Unit

Equations

Lean.PrettyPrinter.Delaborator.addTermInfo pos stx e isBinder = (fun mkTermInfo => do let info ← mkTermInfo stx e isBinder modify fun s => { infos := Std.RBMap.insert s.infos pos info, holeIter := s.holeIter }) Lean.PrettyPrinter.Delaborator.addTermInfo.mkTermInfo

source

def Lean.PrettyPrinter.Delaborator.addTermInfo.mkTermInfo (stx : Lean.Syntax) (e : Lean.Expr) (isBinder : optParam Bool false) :

Lean.PrettyPrinter.Delaborator.DelabM Lean.Elab.Info

Equations

Lean.PrettyPrinter.Delaborator.addTermInfo.mkTermInfo stx e isBinder = do let a ← Lean.getLCtx pure (Lean.Elab.Info.ofTermInfo { toElabInfo := { elaborator := `Delab, stx := stx }, lctx := a, expectedType? := none, expr := e, isBinder := isBinder })

source

def Lean.PrettyPrinter.Delaborator.addFieldInfo (pos : Lean.PrettyPrinter.Delaborator.Pos) (projName : Lean.Name) (fieldName : Lean.Name) (stx : Lean.Syntax) (val : Lean.Expr) :

Lean.PrettyPrinter.Delaborator.DelabM Unit

Equations

Lean.PrettyPrinter.Delaborator.addFieldInfo pos projName fieldName stx val = (fun mkFieldInfo => do let info ← mkFieldInfo projName fieldName stx val modify fun s => { infos := Std.RBMap.insert s.infos pos info, holeIter := s.holeIter }) Lean.PrettyPrinter.Delaborator.addFieldInfo.mkFieldInfo

source

def Lean.PrettyPrinter.Delaborator.addFieldInfo.mkFieldInfo (projName : Lean.Name) (fieldName : Lean.Name) (stx : Lean.Syntax) (val : Lean.Expr) :

Lean.PrettyPrinter.Delaborator.DelabM Lean.Elab.Info

Equations

Lean.PrettyPrinter.Delaborator.addFieldInfo.mkFieldInfo projName fieldName stx val = do let a ← Lean.getLCtx pure (Lean.Elab.Info.ofFieldInfo { projName := projName, fieldName := fieldName, lctx := a, val := val, stx := stx })

source

partial def Lean.PrettyPrinter.Delaborator.delabFor :

Lean.Name → Lean.PrettyPrinter.Delaborator.Delab

source

partial def Lean.PrettyPrinter.Delaborator.delab :

Lean.PrettyPrinter.Delaborator.Delab

source

unsafe def Lean.PrettyPrinter.Delaborator.mkAppUnexpanderAttribute :

IO (Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Unexpander)

Equations

Lean.PrettyPrinter.Delaborator.mkAppUnexpanderAttribute = Lean.KeyedDeclsAttribute.init { builtinName := Lean.Name.anonymous, name := `appUnexpander, descr := "Register an unexpander for applications of a given constant.\n\n[appUnexpander c] registers a `Lean.PrettyPrinter.Unexpander` for applications of the constant `c`. The unexpander is\npassed the result of pre-pretty printing the application *without* implicitly passed arguments. If `pp.explicit` is set\nto true or `pp.notation` is set to false, it will not be called at all.", valueTypeName := `Lean.PrettyPrinter.Unexpander, evalKey := fun x stx => do let a ← Lean.Attribute.Builtin.getId stx Lean.resolveGlobalConstNoOverloadCore a, onAdded := fun builtin declName => pure () } `Lean.PrettyPrinter.Delaborator.appUnexpanderAttribute

source

constant Lean.PrettyPrinter.Delaborator.appUnexpanderAttribute :

Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Unexpander

source

def Lean.PrettyPrinter.delabCore (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (e : Lean.Expr) (optionsPerPos : optParam Lean.PrettyPrinter.Delaborator.OptionsPerPos ∅) :

Lean.MetaM (Lean.Syntax × Std.RBMap Lean.PrettyPrinter.Delaborator.Pos Lean.Elab.Info compare)

Equations

Lean.PrettyPrinter.delabCore currNamespace openDecls e optionsPerPos = let cls := `PrettyPrinter.delab.input; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM (Lean.Syntax × Std.RBMap Lean.PrettyPrinter.Delaborator.Pos Lean.Elab.Info compare) := fun y => do let opts ← Lean.getOptions let _do_jp : Lean.Options → PUnit → Lean.MetaM (Lean.Syntax × Std.RBMap Lean.PrettyPrinter.Delaborator.Pos Lean.Elab.Info compare) := fun opts y => let _do_jp := fun e => let _do_jp := fun optionsPerPos => do let discr ← Lean.catchInternalId Lean.PrettyPrinter.Delaborator.delabFailureId (StateRefT'.run (Lean.PrettyPrinter.Delaborator.delab { defaultOptions := opts, optionsPerPos := optionsPerPos, currNamespace := currNamespace, openDecls := openDecls, inPattern := false, subExpr := Lean.PrettyPrinter.Delaborator.SubExpr.mkRoot e }) { infos := ∅, holeIter := { curr := 2, top := Lean.PrettyPrinter.Delaborator.SubExpr.maxChildren } }) fun x => panicWithPosWithDecl "Lean.PrettyPrinter.Delaborator.Basic" "Lean.PrettyPrinter.delabCore" 283 14 "unreachable code has been reached" let x : Lean.Syntax × Lean.PrettyPrinter.Delaborator.State := discr match x with | (stx, { infos := infos, holeIter := x }) => pure (stx, infos); if (!Lean.getPPAll opts && Lean.getPPAnalyze opts && Std.RBMap.isEmpty optionsPerPos) = true then do let y ← withTheReader Lean.Core.Context (fun ctx => { options := opts, currRecDepth := ctx.currRecDepth, maxRecDepth := ctx.maxRecDepth, ref := ctx.ref, currNamespace := ctx.currNamespace, openDecls := ctx.openDecls, initHeartbeats := ctx.initHeartbeats, maxHeartbeats := ctx.maxHeartbeats }) (Lean.PrettyPrinter.Delaborator.topDownAnalyze e) _do_jp y else do let y ← pure optionsPerPos _do_jp y; if Lean.getPPInstantiateMVars opts = true then do let a ← Lean.Meta.instantiateMVars e let y ← pure a _do_jp y else do let y ← pure e _do_jp y if (Lean.Option.get? opts Lean.pp.proofs == none) = true then do let r ← tryCatch (do let a ← Lean.Meta.isProof e if a = true then let opts := Lean.Option.set opts Lean.pp.proofs true; do let y ← pure PUnit.unit pure { fst := y, snd := opts } else do let y ← pure PUnit.unit pure { fst := y, snd := opts }) fun x => do let y ← pure () pure { fst := y, snd := opts } let x : Lean.Options := r.snd let opts : Lean.Options := x let y ← pure r.fst _do_jp opts y else do let y ← pure PUnit.unit _do_jp opts y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData (Lean.format e) ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.PrettyPrinter.delab (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl) (e : Lean.Expr) (optionsPerPos : optParam Lean.PrettyPrinter.Delaborator.OptionsPerPos ∅) :

Lean.MetaM Lean.Syntax

Equations

Lean.PrettyPrinter.delab currNamespace openDecls e optionsPerPos = do let discr ← Lean.PrettyPrinter.delabCore currNamespace openDecls e optionsPerPos let x : Lean.Syntax × Std.RBMap Lean.PrettyPrinter.Delaborator.Pos Lean.Elab.Info compare := discr match x with | (stx, x) => pure stx