Documentation

Lean.Util.ReplaceLevel

partial def Lean.Level.replace (f? : Lean.Level → Option Lean.Level) (u : Lean.Level) :

@[inline]

abbrev Lean.Expr.ReplaceLevelImpl.cacheSize :

Equations

Lean.Expr.ReplaceLevelImpl.cacheSize = 8192

structure Lean.Expr.ReplaceLevelImpl.State :

Type

keys : Array Lean.Expr
results : Array Lean.Expr

@[inline]

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

Type

Equations

Lean.Expr.ReplaceLevelImpl.ReplaceM = StateM Lean.Expr.ReplaceLevelImpl.State

unsafe def Lean.Expr.ReplaceLevelImpl.cache (i : USize) (key : Lean.Expr) (result : Lean.Expr) :

Lean.Expr.ReplaceLevelImpl.ReplaceM Lean.Expr

Equations

Lean.Expr.ReplaceLevelImpl.cache i key result = do modify fun s => { keys := Array.uset s.keys i key (_ : USize.toNat i < Array.size s.keys), results := Array.uset s.results i result (_ : USize.toNat i < Array.size s.results) } pure result

unsafe def Lean.Expr.ReplaceLevelImpl.replaceUnsafeM (f? : Lean.Level → Option Lean.Level) (size : USize) (e : Lean.Expr) :

Lean.Expr.ReplaceLevelImpl.ReplaceM Lean.Expr

Equations

Lean.Expr.ReplaceLevelImpl.replaceUnsafeM f? size e = (fun visit => visit e) (Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit f? size)

unsafe def Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit (f? : Lean.Level → Option Lean.Level) (size : USize) (e : Lean.Expr) :

Lean.Expr.ReplaceLevelImpl.ReplaceM Lean.Expr

Equations

Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit f? size e = do let c ← get let h : USize := ptrAddrUnsafe e let i : USize := h % size if (ptrAddrUnsafe (Array.uget c.keys i (_ : USize.toNat i < Array.size c.keys)) == h) = true then pure (Array.uget c.results i (_ : USize.toNat i < Array.size c.results)) else match e with | Lean.Expr.forallE x d b x_1 => do let a ← Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit f? size d let a_1 ← Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit f? size b Lean.Expr.ReplaceLevelImpl.cache i e (Lean.Expr.updateForallE! e a a_1) | Lean.Expr.lam x d b x_1 => do let a ← Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit f? size d let a_1 ← Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit f? size b Lean.Expr.ReplaceLevelImpl.cache i e (Lean.Expr.updateLambdaE! e a a_1) | Lean.Expr.mdata x b x_1 => do let a ← Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit f? size b Lean.Expr.ReplaceLevelImpl.cache i e (Lean.Expr.updateMData! e a) | Lean.Expr.letE x t v b x_1 => do let a ← Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit f? size t let a_1 ← Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit f? size v let a_2 ← Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit f? size b Lean.Expr.ReplaceLevelImpl.cache i e (Lean.Expr.updateLet! e a a_1 a_2) | Lean.Expr.app f a x => do let a_1 ← Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit f? size f let a ← Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit f? size a Lean.Expr.ReplaceLevelImpl.cache i e (Lean.Expr.updateApp! e a_1 a) | Lean.Expr.proj x x_1 b x_2 => do let a ← Lean.Expr.ReplaceLevelImpl.replaceUnsafeM.visit f? size b Lean.Expr.ReplaceLevelImpl.cache i e (Lean.Expr.updateProj! e a) | Lean.Expr.sort u x => Lean.Expr.ReplaceLevelImpl.cache i e (Lean.Expr.updateSort! e (Lean.Level.replace f? u)) | Lean.Expr.const n us x => Lean.Expr.ReplaceLevelImpl.cache i e (Lean.Expr.updateConst! e (List.map (Lean.Level.replace f?) us)) | e => pure e

unsafe def Lean.Expr.ReplaceLevelImpl.initCache :

Lean.Expr.ReplaceLevelImpl.State

Equations

Lean.Expr.ReplaceLevelImpl.initCache = { keys := mkArray (USize.toNat Lean.Expr.ReplaceLevelImpl.cacheSize) (cast Lean.Expr.ReplaceLevelImpl.initCache.proof_1 ()), results := mkArray (USize.toNat Lean.Expr.ReplaceLevelImpl.cacheSize) default }

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

Equations

Lean.Expr.ReplaceLevelImpl.replaceUnsafe f? e = StateT.run' (Lean.Expr.ReplaceLevelImpl.replaceUnsafeM f? Lean.Expr.ReplaceLevelImpl.cacheSize e) Lean.Expr.ReplaceLevelImpl.initCache

@[implementedBy Lean.Expr.ReplaceLevelImpl.replaceUnsafe]

partial def Lean.Expr.replaceLevel (f? : Lean.Level → Option Lean.Level) :

Lean.Expr → Lean.Expr