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

Interface for caching results.

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

@[inline]

def Lean.checkCache {α β : Type} {m : Type → Type} [MonadCache α β m] [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.

@[instance_reducible]

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

@[instance_reducible, always_inline]

instance Lean.instMonadCacheExceptTOfMonad {α β ε : Type} {m : Type → Type} [MonadCache α β m] [Monad m] : MonadCache α β (ExceptT ε m)

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

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

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

@[inline]

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

@[inline]

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

@[instance_reducible]

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

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

@[instance_reducible]

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

@[inline]

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

@[instance_reducible]

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

@[instance_reducible]

instance Lean.MonadCacheT.instMonadLift {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] : MonadLift m (MonadCacheT α β m)

@[instance_reducible]

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

@[instance_reducible]

instance Lean.MonadCacheT.instMonadControl {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] : MonadControl m (MonadCacheT α β m)

@[instance_reducible]

instance Lean.MonadCacheT.instMonadFinally {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadFinally m] : MonadFinally (MonadCacheT α β m)

@[instance_reducible]

instance Lean.MonadCacheT.instMonadRef {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadRef m] : MonadRef (MonadCacheT α β m)

@[instance_reducible]

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

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

Similar to MonadCacheT, but using StateT instead of StateRefT

@[instance_reducible]

instance Lean.MonadStateCacheT.instMonadHashMapCacheAdapter {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] : MonadHashMapCacheAdapter α β (MonadStateCacheT α β m)

@[inline]

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

@[instance_reducible]

instance Lean.MonadStateCacheT.instMonad {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] : Monad (MonadStateCacheT α β m)

@[instance_reducible]

instance Lean.MonadStateCacheT.instMonadLift {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] : MonadLift m (MonadStateCacheT α β m)

@[instance_reducible]

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

@[instance_reducible]

instance Lean.MonadStateCacheT.instMonadControl {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] : MonadControl m (MonadStateCacheT α β m)

@[instance_reducible]

instance Lean.MonadStateCacheT.instMonadFinally {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadFinally m] : MonadFinally (MonadStateCacheT α β m)

@[instance_reducible]

instance Lean.MonadStateCacheT.instMonadRef {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadRef m] : MonadRef (MonadStateCacheT α β m)