Interface for caching results.
@[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
- Lean.checkCache a f = do let a ← Lean.MonadCache.findCached? a match a with | some b => pure b | none => do let b ← f () Lean.MonadCache.cache a b pure b
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 }
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) }
class
Lean.MonadHashMapCacheAdapter
(α : Type)
(β : Type)
(m : Type → Type)
[inst : BEq α]
[inst : Hashable α]
:
Type
- getCache : m (Std.HashMap α β)
- modifyCache : (Std.HashMap α β → Std.HashMap α β) → m Unit
Adapter for implementing MonadCache interface using HashMaps.
We just have to specify how to extract/modify the HashMap.
@[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 (Std.HashMap.find? c a)
@[inline]
def
Lean.MonadHashMapCacheAdapter.cache
{α : Type}
{β : Type}
{m : Type → Type}
[inst : BEq α]
[inst : Hashable α]
[inst : Lean.MonadHashMapCacheAdapter α β m]
(a : α)
(b : β)
:
m Unit
Equations
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 }
def
Lean.MonadCacheT
{ω : Type}
(α : Type)
(β : Type)
(m : Type → Type)
[inst : STWorld ω m]
[inst : BEq α]
[inst : Hashable α]
(α : Type)
:
Type
Equations
- Lean.MonadCacheT α β m = StateRefT' ω (Std.HashMap α β) m
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)
@[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 Std.mkHashMap
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' ω (Std.HashMap α β) m))
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' ω (Std.HashMap α β) m))
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
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' ω (Std.HashMap α β) m))
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' ω (Std.HashMap α β) m))
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' ω (Std.HashMap α β) m))
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' ω (Std.HashMap α β) m))
def
Lean.MonadStateCacheT
(α : Type)
(β : Type)
(m : Type → Type)
[inst : BEq α]
[inst : Hashable α]
(α : Type)
:
Type
Equations
- Lean.MonadStateCacheT α β m = StateT (Std.HashMap α β) m
instance
Lean.MonadStateCacheT.instMonadHashMapCacheAdapterMonadStateCacheT
{α : Type}
{β : Type}
{m : Type → Type}
[inst : BEq α]
[inst : Hashable α]
[inst : Monad m]
:
Lean.MonadHashMapCacheAdapter α β (Lean.MonadStateCacheT α β m)
@[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 Std.mkHashMap
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 (Std.HashMap α β) m))
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 (Std.HashMap α β) m))
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
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 (Std.HashMap α β) m))
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 (Std.HashMap α β) m))
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 (Std.HashMap α β) m))