structure Lean.Expr.ReplaceImpl.Cache : Type

• size : USize
• keysResults : Array NonScalar

unsafe def Lean.Expr.ReplaceImpl.Cache.new (e : Lean.Expr) : Lean.Expr.ReplaceImpl.Cache

Equations

• Lean.Expr.ReplaceImpl.Cache.new e = let size := 1 <<< min (max e.approxDepth.toUSize 1) 13 - 1; { size := size, keysResults := mkArray (2 * size).toNat (unsafeCast ()) }

@[inline]

unsafe def Lean.Expr.ReplaceImpl.Cache.keyIdx (c : Lean.Expr.ReplaceImpl.Cache) (key : Lean.Expr) : USize

Equations

• c.keyIdx key = ptrAddrUnsafe key % c.size

@[inline]

unsafe def Lean.Expr.ReplaceImpl.Cache.resultIdx (c : Lean.Expr.ReplaceImpl.Cache) (key : Lean.Expr) : USize

Equations

• c.resultIdx key = c.keyIdx key + c.size

@[inline]

unsafe def Lean.Expr.ReplaceImpl.Cache.hasResultFor (c : Lean.Expr.ReplaceImpl.Cache) (key : Lean.Expr) : Bool

Equations

• c.hasResultFor key = let_fun this := ⋯; ptrEq (unsafeCast key) c.keysResults[c.keyIdx key]

@[inline]

unsafe def Lean.Expr.ReplaceImpl.Cache.getResultFor (c : Lean.Expr.ReplaceImpl.Cache) (key : Lean.Expr) : Lean.Expr

Equations

• c.getResultFor key = let_fun this := ⋯; unsafeCast c.keysResults[c.resultIdx key]

unsafe def Lean.Expr.ReplaceImpl.Cache.store (c : Lean.Expr.ReplaceImpl.Cache) (key : Lean.Expr) (result : Lean.Expr) : Lean.Expr.ReplaceImpl.Cache

Equations

• c.store key result = { size := c.size, keysResults := (c.keysResults.uset (c.keyIdx key) (unsafeCast key) ⋯).uset (c.resultIdx key) (unsafeCast result) ⋯ }

@[reducible, inline]

abbrev Lean.Expr.ReplaceImpl.ReplaceM (α : Type) : Type

Equations

• Lean.Expr.ReplaceImpl.ReplaceM = StateM Lean.Expr.ReplaceImpl.Cache

@[inline]

unsafe def Lean.Expr.ReplaceImpl.cache (key : Lean.Expr) (result : Lean.Expr) : Lean.Expr.ReplaceImpl.ReplaceM Lean.Expr

Equations

• Lean.Expr.ReplaceImpl.cache key result = do modify fun (x : Lean.Expr.ReplaceImpl.Cache) => x.store key result pure result

@[specialize #[]]

unsafe def Lean.Expr.ReplaceImpl.replaceUnsafeM (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) : Lean.Expr.ReplaceImpl.ReplaceM Lean.Expr

Equations

• Lean.Expr.ReplaceImpl.replaceUnsafeM f? e = Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? e

@[specialize #[]]

unsafe def Lean.Expr.ReplaceImpl.replaceUnsafeM.visit (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) : Lean.Expr.ReplaceImpl.ReplaceM Lean.Expr

Equations

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

@[inline]

unsafe def Lean.Expr.ReplaceImpl.replaceUnsafe (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) : Lean.Expr

Equations

• Lean.Expr.ReplaceImpl.replaceUnsafe f? e = StateT.run' (Lean.Expr.ReplaceImpl.replaceUnsafeM f? e) (Lean.Expr.ReplaceImpl.Cache.new e)

@[specialize #[]]

def Lean.Expr.replaceNoCache (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) : Lean.Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Expr.replaceNoCache f? e = match f? e with | some eNew => eNew | none => e

@[implemented_by Lean.Expr.ReplaceImpl.replaceUnsafe]

def Lean.Expr.replace (f? : Lean.Expr → Option Lean.Expr) (e : Lean.Expr) : Lean.Expr

Equations

• Lean.Expr.replace f? e = Lean.Expr.replaceNoCache f? e