Documentation

Lean.Util.MonadCache

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

Interface for caching results.

  • findCached? : αm (Option β)
  • cache : αβm Unit
Instances
    @[inline]
    def Lean.checkCache {α : Type} {β : Type} {m : TypeType} [Lean.MonadCache α β m] [Monad m] (a : α) (f : Unitm β) :
    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
    Instances For
      instance Lean.instMonadCacheReaderT {α : Type} {β : Type} {ρ : Type} {m : TypeType} [Lean.MonadCache α β m] :
      Equations
      @[always_inline]
      instance Lean.instMonadCacheExceptTOfMonad {α : Type} {β : Type} {ε : Type} {m : TypeType} [Lean.MonadCache α β m] [Monad m] :
      Equations
      class Lean.MonadHashMapCacheAdapter (α : Type) (β : Type) (m : TypeType) [BEq α] [Hashable α] :

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

      Instances
        @[inline]
        def Lean.MonadHashMapCacheAdapter.findCached? {α : Type} {β : Type} {m : TypeType} [BEq α] [Hashable α] [Monad m] [Lean.MonadHashMapCacheAdapter α β m] (a : α) :
        m (Option β)
        Equations
        Instances For
          @[inline]
          def Lean.MonadHashMapCacheAdapter.cache {α : Type} {β : Type} {m : TypeType} [BEq α] [Hashable α] [Lean.MonadHashMapCacheAdapter α β m] (a : α) (b : β) :
          Equations
          Instances For
            Equations
            • Lean.MonadHashMapCacheAdapter.instMonadCacheOfMonad = { findCached? := Lean.MonadHashMapCacheAdapter.findCached?, cache := Lean.MonadHashMapCacheAdapter.cache }
            def Lean.MonadCacheT {ω : Type} (α : Type) (β : Type) (m : TypeType) [STWorld ω m] [BEq α✝] [Hashable α✝] (α : Type) :
            Equations
            Instances For
              instance Lean.MonadCacheT.instMonadHashMapCacheAdapter {ω : Type} {α : Type} {β : Type} {m : TypeType} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] :
              Equations
              • Lean.MonadCacheT.instMonadHashMapCacheAdapter = { getCache := get, modifyCache := fun (f : Std.HashMap α βStd.HashMap α β) => modify f }
              @[inline]
              def Lean.MonadCacheT.run {ω : Type} {α : Type} {β : Type} {m : TypeType} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m] {σ : Type} (x : Lean.MonadCacheT α β m σ) :
              m σ
              Equations
              Instances For
                instance Lean.MonadCacheT.instMonad {ω : Type} {α : Type} {β : Type} {m : TypeType} [STWorld ω m] [BEq α] [Hashable α] [Monad m] :
                Equations
                instance Lean.MonadCacheT.instMonadLift {ω : Type} {α : Type} {β : Type} {m : TypeType} [STWorld ω m] [BEq α] [Hashable α] :
                Equations
                instance Lean.MonadCacheT.instMonadControl {ω : Type} {α : Type} {β : Type} {m : TypeType} [STWorld ω m] [BEq α] [Hashable α] :
                Equations
                instance Lean.MonadCacheT.instMonadFinally {ω : Type} {α : Type} {β : Type} {m : TypeType} [STWorld ω m] [BEq α] [Hashable α] [MonadFinally m] :
                Equations
                instance Lean.MonadCacheT.instMonadRef {ω : Type} {α : Type} {β : Type} {m : TypeType} [STWorld ω m] [BEq α] [Hashable α] [Lean.MonadRef m] :
                Equations
                instance Lean.MonadCacheT.instAlternative {ω : Type} {α : Type} {β : Type} {m : TypeType} [STWorld ω m] [BEq α] [Hashable α] [Monad m] [Alternative m] :
                Equations
                def Lean.MonadStateCacheT (α : Type) (β : Type) (m : TypeType) [BEq α✝] [Hashable α✝] (α : Type) :
                Equations
                Instances For
                  Equations
                  • Lean.MonadStateCacheT.instMonadHashMapCacheAdapter = { getCache := get, modifyCache := fun (f : Std.HashMap α βStd.HashMap α β) => modify f }
                  @[inline]
                  def Lean.MonadStateCacheT.run {α : Type} {β : Type} {m : TypeType} [BEq α] [Hashable α] [Monad m] {σ : Type} (x : Lean.MonadStateCacheT α β m σ) :
                  m σ
                  Equations
                  Instances For
                    instance Lean.MonadStateCacheT.instMonad {α : Type} {β : Type} {m : TypeType} [BEq α] [Hashable α] [Monad m] :
                    Equations
                    instance Lean.MonadStateCacheT.instMonadLift {α : Type} {β : Type} {m : TypeType} [BEq α] [Hashable α] [Monad m] :
                    Equations
                    instance Lean.MonadStateCacheT.instMonadControl {α : Type} {β : Type} {m : TypeType} [BEq α] [Hashable α] [Monad m] :
                    Equations
                    Equations
                    Equations