Lean.Util.FindExpr

source

@[inline]

abbrev Lean.Expr.FindImpl.cacheSize :

USize

Equations

Lean.Expr.FindImpl.cacheSize = 8192

source

structure Lean.Expr.FindImpl.State :

Type

keys : Array Lean.Expr

source

@[inline]

abbrev Lean.Expr.FindImpl.FindM (α : Type) :

Type

Equations

Lean.Expr.FindImpl.FindM = StateT Lean.Expr.FindImpl.State Id

source

unsafe def Lean.Expr.FindImpl.visited (e : Lean.Expr) (size : USize) :

Lean.Expr.FindImpl.FindM Bool

Equations

Lean.Expr.FindImpl.visited e size = do let s ← get let h : USize := ptrAddrUnsafe e let i : USize := h % size let k : Lean.Expr := Array.uget s.keys i (_ : USize.toNat (ptrAddrUnsafe e % size) < Array.size s.keys) if (ptrAddrUnsafe k == h) = true then pure true else do modify fun s => { keys := Array.uset s.keys i e (_ : USize.toNat (ptrAddrUnsafe e % size) < Array.size s.keys) } pure false

source

unsafe def Lean.Expr.FindImpl.findM? (p : Lean.Expr → Bool) (size : USize) (e : Lean.Expr) :

OptionT Lean.Expr.FindImpl.FindM Lean.Expr

Equations

Lean.Expr.FindImpl.findM? p size e = (fun visit => visit e) (Lean.Expr.FindImpl.findM?.visit p size)

source

unsafe def Lean.Expr.FindImpl.findM?.visit (p : Lean.Expr → Bool) (size : USize) (e : Lean.Expr) :

OptionT Lean.Expr.FindImpl.FindM Lean.Expr

Equations

Lean.Expr.FindImpl.findM?.visit p size e = do let a ← liftM (Lean.Expr.FindImpl.visited e size) if a = true then failure else if p e = true then pure e else match e with | Lean.Expr.forallE x d b x_1 => HOrElse.hOrElse (Lean.Expr.FindImpl.findM?.visit p size d) fun x => Lean.Expr.FindImpl.findM?.visit p size b | Lean.Expr.lam x d b x_1 => HOrElse.hOrElse (Lean.Expr.FindImpl.findM?.visit p size d) fun x => Lean.Expr.FindImpl.findM?.visit p size b | Lean.Expr.mdata x b x_1 => Lean.Expr.FindImpl.findM?.visit p size b | Lean.Expr.letE x t v b x_1 => HOrElse.hOrElse (Lean.Expr.FindImpl.findM?.visit p size t) fun x => HOrElse.hOrElse (Lean.Expr.FindImpl.findM?.visit p size v) fun x => Lean.Expr.FindImpl.findM?.visit p size b | Lean.Expr.app f a x => HOrElse.hOrElse (Lean.Expr.FindImpl.findM?.visit p size f) fun x => Lean.Expr.FindImpl.findM?.visit p size a | Lean.Expr.proj x x_1 b x_2 => Lean.Expr.FindImpl.findM?.visit p size b | e => failure

source

unsafe def Lean.Expr.FindImpl.initCache :

Lean.Expr.FindImpl.State

Equations

Lean.Expr.FindImpl.initCache = { keys := mkArray (USize.toNat Lean.Expr.FindImpl.cacheSize) (cast Lean.Expr.FindImpl.initCache.proof_1 ()) }

source

unsafe def Lean.Expr.FindImpl.findUnsafe? (p : Lean.Expr → Bool) (e : Lean.Expr) :

Option Lean.Expr

Equations

Lean.Expr.FindImpl.findUnsafe? p e = Id.run (StateT.run' (Lean.Expr.FindImpl.findM? p Lean.Expr.FindImpl.cacheSize e) Lean.Expr.FindImpl.initCache)

source

@[implementedBy Lean.Expr.FindImpl.findUnsafe?]

partial def Lean.Expr.find? (p : Lean.Expr → Bool) (e : Lean.Expr) :

Option Lean.Expr

source

def Lean.Expr.occurs (e : Lean.Expr) (t : Lean.Expr) :

Bool

Equations

Lean.Expr.occurs e t = Option.isSome (Lean.Expr.find? (fun s => s == e) t)