@[inline]
Equations
@[inline]
Equations
- Lean.Expr.ReplaceImpl.cache i key result = do modify fun x => match x with | { keys := keys, results := results } => { keys := Array.uset keys i key (_ : USize.toNat i < Array.size keys), results := Array.uset results i result (_ : USize.toNat i < Array.size results) } pure result
unsafe def
Lean.Expr.ReplaceImpl.replaceUnsafeM
(f? : Lean.Expr → Option Lean.Expr)
(size : USize)
(e : Lean.Expr)
:
Equations
- Lean.Expr.ReplaceImpl.replaceUnsafeM f? size e = (fun visit => visit e) (Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? size)
unsafe def
Lean.Expr.ReplaceImpl.replaceUnsafeM.visit
(f? : Lean.Expr → Option Lean.Expr)
(size : USize)
(e : Lean.Expr)
:
Equations
- Lean.Expr.ReplaceImpl.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 f? e with | some eNew => Lean.Expr.ReplaceImpl.cache i e eNew | none => match e with | Lean.Expr.forallE x d b x_1 => do let a ← Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? size d let a_1 ← Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? size b Lean.Expr.ReplaceImpl.cache i e (Lean.Expr.updateForallE! e a a_1) | Lean.Expr.lam x d b x_1 => do let a ← Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? size d let a_1 ← Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? size b Lean.Expr.ReplaceImpl.cache i e (Lean.Expr.updateLambdaE! e a a_1) | Lean.Expr.mdata x b x_1 => do let a ← Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? size b Lean.Expr.ReplaceImpl.cache i e (Lean.Expr.updateMData! e a) | Lean.Expr.letE x t v b x_1 => do let a ← Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? size t let a_1 ← Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? size v let a_2 ← Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? size b Lean.Expr.ReplaceImpl.cache i e (Lean.Expr.updateLet! e a a_1 a_2) | Lean.Expr.app f a x => do let a_1 ← Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? size f let a ← Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? size a Lean.Expr.ReplaceImpl.cache i e (Lean.Expr.updateApp! e a_1 a) | Lean.Expr.proj x x_1 b x_2 => do let a ← Lean.Expr.ReplaceImpl.replaceUnsafeM.visit f? size b Lean.Expr.ReplaceImpl.cache i e (Lean.Expr.updateProj! e a) | e => pure e
Equations
- Lean.Expr.ReplaceImpl.initCache = { keys := mkArray (USize.toNat Lean.Expr.ReplaceImpl.cacheSize) (cast Lean.Expr.ReplaceImpl.initCache.proof_1 ()), results := mkArray (USize.toNat Lean.Expr.ReplaceImpl.cacheSize) default }
unsafe def
Lean.Expr.ReplaceImpl.replaceUnsafe
(f? : Lean.Expr → Option Lean.Expr)
(e : Lean.Expr)
: