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

Interface for caching results.

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

Instances

source
@[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`.

Equations

- Lean.checkCache a f = do let __do_lift ← Lean.MonadCache.findCached? a match __do_lift with | some b => pure b | none => do let b ← f () Lean.MonadCache.cache a b pure b

Instances For

source
instance Lean.instMonadCacheReaderT {α β ρ : Type} {m : Type → Type} [MonadCache α β m] :
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.instMonadCacheExceptTOfMonad {α β ε : Type} {m : Type → Type} [MonadCache α β m] [Monad m] :
MonadCache α β (ExceptT ε m)
Equations

- Lean.instMonadCacheExceptTOfMonad = { 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) (m : Type → Type) [BEq α] [Hashable α] :
Type

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

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

Instances

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

- Lean.MonadHashMapCacheAdapter.findCached? a = do let c ← Lean.MonadHashMapCacheAdapter.getCache pure (c.get? a)

Instances For

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

- Lean.MonadHashMapCacheAdapter.cache a b = Lean.MonadHashMapCacheAdapter.modifyCache fun (s : Std.HashMap α β) => s.insert a b

Instances For

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

- Lean.MonadHashMapCacheAdapter.instMonadCacheOfMonad = { findCached? := Lean.MonadHashMapCacheAdapter.findCached?, cache := Lean.MonadHashMapCacheAdapter.cache }

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

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

Instances For

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

- Lean.MonadCacheT.instMonadHashMapCacheAdapter = { getCache := get, modifyCache := fun (f : Std.HashMap α β → Std.HashMap α β) => modify f }

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

- x.run = StateRefT'.run' x ∅

Instances For

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

- Lean.MonadCacheT.instMonad = inferInstanceAs (Monad (StateRefT' ω (Std.HashMap α β) m))

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

- Lean.MonadCacheT.instMonadLift = inferInstanceAs (MonadLift m (StateRefT' ω (Std.HashMap α β) m))

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

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

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

- Lean.MonadCacheT.instMonadControl = inferInstanceAs (MonadControl m (StateRefT' ω (Std.HashMap α β) m))

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

- Lean.MonadCacheT.instMonadFinally = inferInstanceAs (MonadFinally (StateRefT' ω (Std.HashMap α β) m))

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

- Lean.MonadCacheT.instMonadRef = inferInstanceAs (Lean.MonadRef (StateRefT' ω (Std.HashMap α β) m))

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

- Lean.MonadCacheT.instAlternative = inferInstanceAs (Alternative (StateRefT' ω (Std.HashMap α β) m))

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

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

Instances For

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

- Lean.MonadStateCacheT.instMonadHashMapCacheAdapter = { getCache := get, modifyCache := fun (f : Std.HashMap α β → Std.HashMap α β) => modify f }

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

- x.run = StateT.run' x ∅

Instances For

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

- Lean.MonadStateCacheT.instMonad = inferInstanceAs (Monad (StateT (Std.HashMap α β) m))

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

- Lean.MonadStateCacheT.instMonadLift = inferInstanceAs (MonadLift m (StateT (Std.HashMap α β) m))

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

- Lean.MonadStateCacheT.instMonadExceptOf ε = inferInstanceAs (MonadExceptOf ε (StateT (Std.HashMap α β) m))

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

- Lean.MonadStateCacheT.instMonadControl = inferInstanceAs (MonadControl m (StateT (Std.HashMap α β) m))

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

- Lean.MonadStateCacheT.instMonadFinally = inferInstanceAs (MonadFinally (StateT (Std.HashMap α β) m))

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

- Lean.MonadStateCacheT.instMonadRef = inferInstanceAs (Lean.MonadRef (StateT (Std.HashMap α β) m))