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 = Lean.RBMap Lean.SubExpr.Pos Lean.Options compare

Instances For

source

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

Lean.PrettyPrinter.Delaborator.OptionsPerPos

Equations

optionsPerPos.insertAt pos name value = Lean.RBMap.insert optionsPerPos pos (Lean.KVMap.insert ((Lean.RBMap.find? optionsPerPos pos).getD { entries := [] }) name value)

Instances For

source

def Lean.PrettyPrinter.Delaborator.OptionsPerPos.merge :

Lean.PrettyPrinter.Delaborator.OptionsPerPos → Lean.PrettyPrinter.Delaborator.OptionsPerPos → Lean.PrettyPrinter.Delaborator.OptionsPerPos

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

Equations

Lean.PrettyPrinter.Delaborator.OptionsPerPos.merge = Lean.RBMap.mergeBy fun (x : Lean.SubExpr.Pos) => Lean.KVMap.mergeBy fun (x : Lean.Name) (x dv : Lean.DataValue) => dv

Instances For

source

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

m Lean.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 Lean.SubExpr m] :

m Lean.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 Lean.SubExpr m] (child : Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] [MonadLiftT Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] [MonadControlT Lean.MetaM m] {β : Type} (n : Lean.Name) (v : Lean.Expr → m β) (x : β → m α) :

m α

Assumes the SubExpr is a lambda or forall.

Creates a local declaration for this binder using the name n.
Evaluates v using the fvar for the local declaration.
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 Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] [MonadControlT Lean.MetaM m] (n : Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.SubExpr m] [MonadControlT Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.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 Lean.SubExpr m] [MonadWithReaderOf Lean.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

instance Lean.PrettyPrinter.Delaborator.SubExpr.instInhabitedHoleIterator :

Inhabited Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator

Equations

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

source

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

Lean.SubExpr.Pos

Equations

iter.toPos = iter.curr

Instances For

source

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

Lean.PrettyPrinter.Delaborator.SubExpr.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 Lean.PrettyPrinter.Delaborator.SubExpr.HoleIterator m] :

m Lean.SubExpr.Pos

The positioning scheme guarantees that there will be an infinite number of extra positions which are never used by Exprs. 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