Lean.Util.MonadCache

class Lean.MonadCache (α : Type) (β : Type) (m : Type → Type) :

findCached? : α → m (Option β)
cache : α → β → m Unit

Interface for caching results.

Instances

@[inline]

def Lean.checkCache {α : Type} {β : Type} {m : Type → Type} [inst : Lean.MonadCache α β m] [inst : Monad m] (a : α) (f : Unit → m β) :

m β

If entry a := b is already in the cache, then return b. Otherwise, execute b ← f (), store a := b in the cache and return b.

Equations

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

source

instance Lean.instMonadCacheReaderT {α : Type} {β : Type} {ρ : Type} {m : Type → Type} [inst : Lean.MonadCache α β m] :

Lean.MonadCache α β (ReaderT ρ m)

Equations

Lean.instMonadCacheReaderT = { findCached? := fun a x => Lean.MonadCache.findCached? a, cache := fun a b x => Lean.MonadCache.cache a b }

source

@[always_inline]

instance Lean.instMonadCacheExceptT {α : Type} {β : Type} {ε : Type} {m : Type → Type} [inst : Lean.MonadCache α β m] [inst : Monad m] :

Lean.MonadCache α β (ExceptT ε m)

Equations

Lean.instMonadCacheExceptT = { findCached? := fun a => ExceptT.lift (Lean.MonadCache.findCached? a), cache := fun a b => ExceptT.lift (Lean.MonadCache.cache a b) }

source

class Lean.MonadHashMapCacheAdapter (α : Type) (β : Type) (m : Type → Type) [inst : BEq α] [inst : Hashable α] :

Type

getCache : m (Lean.HashMap α β)
modifyCache : (Lean.HashMap α β → Lean.HashMap α β) → m Unit

Adapter for implementing MonadCache interface using HashMaps. We just have to specify how to extract/modify the HashMap.

Instances

source

@[inline]

def Lean.MonadHashMapCacheAdapter.findCached? {α : Type} {β : Type} {m : Type → Type} [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : Lean.MonadHashMapCacheAdapter α β m] (a : α) :

m (Option β)

Equations

Lean.MonadHashMapCacheAdapter.findCached? a = do let c ← Lean.MonadHashMapCacheAdapter.getCache pure (Lean.HashMap.find? c a)

source

@[inline]

def Lean.MonadHashMapCacheAdapter.cache {α : Type} {β : Type} {m : Type → Type} [inst : BEq α] [inst : Hashable α] [inst : Lean.MonadHashMapCacheAdapter α β m] (a : α) (b : β) :

m Unit

Equations

Lean.MonadHashMapCacheAdapter.cache a b = Lean.MonadHashMapCacheAdapter.modifyCache fun s => Lean.HashMap.insert s a b

source

instance Lean.MonadHashMapCacheAdapter.instMonadCache {α : Type} {β : Type} {m : Type → Type} [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : Lean.MonadHashMapCacheAdapter α β m] :

Lean.MonadCache α β m

Equations

Lean.MonadHashMapCacheAdapter.instMonadCache = { findCached? := Lean.MonadHashMapCacheAdapter.findCached?, cache := Lean.MonadHashMapCacheAdapter.cache }

source

def Lean.MonadCacheT {ω : Type} (α : Type) (β : Type) (m : Type → Type) [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] (α : Type) :

Type

Equations

Lean.MonadCacheT α β m = StateRefT' ω (Lean.HashMap α β) m

source

instance Lean.MonadCacheT.instMonadHashMapCacheAdapterMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] [inst : MonadLiftT (ST ω) m] [inst : Monad m] :

Lean.MonadHashMapCacheAdapter α β (Lean.MonadCacheT α β m)

Equations

Lean.MonadCacheT.instMonadHashMapCacheAdapterMonadCacheT = { getCache := get, modifyCache := fun f => modify f }

source

@[inline]

def Lean.MonadCacheT.run {ω : Type} {α : Type} {β : Type} {m : Type → Type} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] [inst : MonadLiftT (ST ω) m] [inst : Monad m] {σ : Type} (x : Lean.MonadCacheT α β m σ) :

m σ

Equations

Lean.MonadCacheT.run x = StateRefT'.run' x Lean.mkHashMap

source

instance Lean.MonadCacheT.instMonadMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] [inst : Monad m] :

Monad (Lean.MonadCacheT α β m)

Equations

Lean.MonadCacheT.instMonadMonadCacheT = inferInstanceAs (Monad (StateRefT' ω (Lean.HashMap α β) m))

source

instance Lean.MonadCacheT.instMonadLiftMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] :

MonadLift m (Lean.MonadCacheT α β m)

Equations

Lean.MonadCacheT.instMonadLiftMonadCacheT = inferInstanceAs (MonadLift m (StateRefT' ω (Lean.HashMap α β) m))

source

instance Lean.MonadCacheT.instMonadExceptOfMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] (ε : Type u_1) [inst : MonadExceptOf ε m] :

MonadExceptOf ε (Lean.MonadCacheT α β m)

Equations

Lean.MonadCacheT.instMonadExceptOfMonadCacheT ε = inferInstanceAs (MonadExceptOf ε (StateRefT' ω (Lean.HashMap α β) m))

source

instance Lean.MonadCacheT.instMonadControlMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] :

MonadControl m (Lean.MonadCacheT α β m)

Equations

Lean.MonadCacheT.instMonadControlMonadCacheT = inferInstanceAs (MonadControl m (StateRefT' ω (Lean.HashMap α β) m))

source

instance Lean.MonadCacheT.instMonadFinallyMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : MonadFinally m] :

MonadFinally (Lean.MonadCacheT α β m)

Equations

Lean.MonadCacheT.instMonadFinallyMonadCacheT = inferInstanceAs (MonadFinally (StateRefT' ω (Lean.HashMap α β) m))

source

instance Lean.MonadCacheT.instMonadRefMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : Lean.MonadRef m] :

Lean.MonadRef (Lean.MonadCacheT α β m)

Equations

Lean.MonadCacheT.instMonadRefMonadCacheT = inferInstanceAs (Lean.MonadRef (StateRefT' ω (Lean.HashMap α β) m))

source

instance Lean.MonadCacheT.instAlternativeMonadCacheT {ω : Type} {α : Type} {β : Type} {m : Type → Type} [inst : STWorld ω m] [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : Alternative m] :

Alternative (Lean.MonadCacheT α β m)

Equations

Lean.MonadCacheT.instAlternativeMonadCacheT = inferInstanceAs (Alternative (StateRefT' ω (Lean.HashMap α β) m))

source

def Lean.MonadStateCacheT (α : Type) (β : Type) (m : Type → Type) [inst : BEq α] [inst : Hashable α] (α : Type) :

Type

Equations

Lean.MonadStateCacheT α β m = StateT (Lean.HashMap α β) m

source

instance Lean.MonadStateCacheT.instMonadHashMapCacheAdapterMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [inst : BEq α] [inst : Hashable α] [inst : Monad m] :

Lean.MonadHashMapCacheAdapter α β (Lean.MonadStateCacheT α β m)

Equations

Lean.MonadStateCacheT.instMonadHashMapCacheAdapterMonadStateCacheT = { getCache := get, modifyCache := fun f => modify f }

source

@[inline]

def Lean.MonadStateCacheT.run {α : Type} {β : Type} {m : Type → Type} [inst : BEq α] [inst : Hashable α] [inst : Monad m] {σ : Type} (x : Lean.MonadStateCacheT α β m σ) :

m σ

Equations

Lean.MonadStateCacheT.run x = StateT.run' x Lean.mkHashMap

source

instance Lean.MonadStateCacheT.instMonadMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [inst : BEq α] [inst : Hashable α] [inst : Monad m] :

Monad (Lean.MonadStateCacheT α β m)

Equations

Lean.MonadStateCacheT.instMonadMonadStateCacheT = inferInstanceAs (Monad (StateT (Lean.HashMap α β) m))

source

instance Lean.MonadStateCacheT.instMonadLiftMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [inst : BEq α] [inst : Hashable α] [inst : Monad m] :

MonadLift m (Lean.MonadStateCacheT α β m)

Equations

Lean.MonadStateCacheT.instMonadLiftMonadStateCacheT = inferInstanceAs (MonadLift m (StateT (Lean.HashMap α β) m))

source

instance Lean.MonadStateCacheT.instMonadExceptOfMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [inst : BEq α] [inst : Hashable α] [inst : Monad m] (ε : Type u_1) [inst : MonadExceptOf ε m] :

MonadExceptOf ε (Lean.MonadStateCacheT α β m)

Equations

Lean.MonadStateCacheT.instMonadExceptOfMonadStateCacheT ε = inferInstanceAs (MonadExceptOf ε (StateT (Lean.HashMap α β) m))

source

instance Lean.MonadStateCacheT.instMonadControlMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [inst : BEq α] [inst : Hashable α] [inst : Monad m] :

MonadControl m (Lean.MonadStateCacheT α β m)

Equations

Lean.MonadStateCacheT.instMonadControlMonadStateCacheT = inferInstanceAs (MonadControl m (StateT (Lean.HashMap α β) m))

source

instance Lean.MonadStateCacheT.instMonadFinallyMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : MonadFinally m] :

MonadFinally (Lean.MonadStateCacheT α β m)

Equations

Lean.MonadStateCacheT.instMonadFinallyMonadStateCacheT = inferInstanceAs (MonadFinally (StateT (Lean.HashMap α β) m))

source

instance Lean.MonadStateCacheT.instMonadRefMonadStateCacheT {α : Type} {β : Type} {m : Type → Type} [inst : BEq α] [inst : Hashable α] [inst : Monad m] [inst : Lean.MonadRef m] :

Lean.MonadRef (Lean.MonadStateCacheT α β m)

Equations

Lean.MonadStateCacheT.instMonadRefMonadStateCacheT = inferInstanceAs (Lean.MonadRef (StateT (Lean.HashMap α β) m))