# Subexpr utilities for delaborator. #

This file defines utilities for `MetaM` computations to traverse subexpressions of an expression in sync with the `Nat` "position" values that refer to them.

source
@[reducible, inline]
abbrev Lean.PrettyPrinter.Delaborator.OptionsPerPos :
Type
Equations

- Lean.PrettyPrinter.Delaborator.OptionsPerPos = Std.TreeMap Lean.SubExpr.Pos Lean.Options compare

Instances For

source
def Lean.PrettyPrinter.Delaborator.OptionsPerPos.insertAt (optionsPerPos : OptionsPerPos) (pos : SubExpr.Pos) (name : Name) (value : DataValue) :
OptionsPerPos
Equations

- optionsPerPos.insertAt pos name value = Std.TreeMap.insert optionsPerPos pos (Lean.KVMap.insert ((Std.TreeMap.get? optionsPerPos pos).getD { }) name value)

Instances For

source
def Lean.PrettyPrinter.Delaborator.OptionsPerPos.merge :
OptionsPerPos → OptionsPerPos → OptionsPerPos

Merges two collections of options, where the second overrides the first.

Equations

- Lean.PrettyPrinter.Delaborator.OptionsPerPos.merge = Std.TreeMap.mergeWith fun (x : Lean.SubExpr.Pos) => Lean.KVMap.mergeBy fun (x : Lean.Name) (x_1 dv : Lean.DataValue) => dv

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.getExpr {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] :
m Expr
Equations

- Lean.PrettyPrinter.Delaborator.SubExpr.getExpr = do let __do_lift ← readThe Lean.SubExpr pure __do_lift.expr

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.getPos {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] :
m SubExpr.Pos
Equations

- Lean.PrettyPrinter.Delaborator.SubExpr.getPos = do let __do_lift ← readThe Lean.SubExpr pure __do_lift.pos

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.descend {α : Type} {m : Type → Type} [MonadWithReaderOf SubExpr m] (child : Expr) (childIdx : Nat) (x : m α) :
m α
Equations

- Lean.PrettyPrinter.Delaborator.SubExpr.descend child childIdx x = withTheReader Lean.SubExpr (fun (cfg : Lean.SubExpr) => { expr := child, pos := cfg.pos.push childIdx }) x

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] (x : m α) :
m α
Equations

- Lean.PrettyPrinter.Delaborator.SubExpr.withAppFn x = do let __do_lift ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr Lean.PrettyPrinter.Delaborator.SubExpr.descend __do_lift.appFn! 0 x

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] (x : m α) :
m α
Equations

- Lean.PrettyPrinter.Delaborator.SubExpr.withAppArg x = do let __do_lift ← Lean.PrettyPrinter.Delaborator.SubExpr.getExpr Lean.PrettyPrinter.Delaborator.SubExpr.descend __do_lift.appArg! 1 x

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withType {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] [MonadLiftT MetaM m] (x : m α) :
m α
Equations

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

Instances For

source
partial def Lean.PrettyPrinter.Delaborator.SubExpr.withAppFnArgs {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] (xf : m α) (xa : α → m α) :
m α

Uses `xa` to compute the fold across the arguments of an application, where `xf` provides the initial value and is evaluated in the context of the head of the application.

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withBoundedAppFnArgs {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] (maxArgs : Nat) (xf : m α) (xa : α → m α) :
m α

Uses `xa` to compute the fold across up to `maxArgs` outermost arguments of an application, where `xf` provides the initial value and is evaluated in the context of the application minus the arguments being folded across.

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withBoundedAppFn {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] (maxArgs : Nat) (xf : m α) :
m α

Runs `xf` in the context of `Lean.Expr.getBoundedAppFn maxArgs`. This is equivalent to `withBoundedAppFnArgs maxArgs xf pure`.

Equations

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

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withBindingDomain {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] (x : m α) :
m α
Equations

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

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody' {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] [MonadControlT MetaM m] {β : Type} (n : Name) (v : Expr → m β) (x : β → m α) :
m α

Assumes the `SubExpr` is a lambda or forall.

1. Creates a local declaration for this binder using the name `n`.
2. Evaluates `v` using the fvar for the local declaration.
3. Enters the binding body, and evaluates `x` using this result.

Equations

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

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] [MonadControlT MetaM m] (n : Name) (x : m α) :
m α

Assumes the `SubExpr` is a lambda or forall. Creates a local declaration for this binder using the name `n`, enters the binding body, and evaluates `x`.

Equations

- Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody n x = Lean.PrettyPrinter.Delaborator.SubExpr.withBindingBody' n (fun (x : Lean.Expr) => pure ()) fun (x_1 : Unit) => x

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withProj {α : Type} [Inhabited α] {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] (x : m α) :
m α
Equations

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

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withMDataExpr {α : Type} [Inhabited α] {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] (x : m α) :
m α
Equations

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

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withLetVarType {α : Type} [Inhabited α] {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] (x : m α) :
m α
Equations

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

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withLetValue {α : Type} [Inhabited α] {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] (x : m α) :
m α
Equations

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

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withLetBody {α : Type} [Inhabited α] {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] [MonadControlT MetaM m] (x : m α) :
m α
Equations

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

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withNaryFn {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] (x : m α) :
m α
Equations

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

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.withNaryArg {α : Type} {m : Type → Type} [Monad m] [MonadReaderOf SubExpr m] [MonadWithReaderOf SubExpr m] (argIdx : Nat) (x : m α) :
m α
Equations

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

Instances For

source
structure Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator :
Type

- curr : Nat
- top : Nat

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.instInhabitedHoleIterator.default :
HoleIterator
Equations

- Lean.PrettyPrinter.Delaborator.SubExpr.instInhabitedHoleIterator.default = { curr := default, top := default }

Instances For

source
instance Lean.PrettyPrinter.Delaborator.SubExpr.instInhabitedHoleIterator :
Inhabited HoleIterator
Equations

- Lean.PrettyPrinter.Delaborator.SubExpr.instInhabitedHoleIterator = { default := Lean.PrettyPrinter.Delaborator.SubExpr.instInhabitedHoleIterator.default }

source
def Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.toPos (iter : HoleIterator) :
SubExpr.Pos
Equations

- iter.toPos = iter.curr

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator.next (iter : HoleIterator) :
HoleIterator
Equations

- iter.next = if (iter.curr + 1 == iter.top) = true then { curr := 2 * iter.top, top := Lean.SubExpr.Pos.maxChildren * iter.top } else { curr := iter.curr + 1, top := iter.top }

Instances For

source
def Lean.PrettyPrinter.Delaborator.SubExpr.nextExtraPos {m : Type → Type} [Monad m] [MonadStateOf HoleIterator m] :
m SubExpr.Pos

The positioning scheme guarantees that there will be an infinite number of extra positions which are never used by `Expr`s. The `HoleIterator` always points at the next such "hole". We use these to attach additional `Elab.Info`.

Note: these positions are incompatible with `Lean.SubExpr.Pos.push` since the iterator will eventually yield every child of every returned position.

Equations

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

Instances For