Documentation

Lean.Util.MonadCache

class Lean.MonadCache (α : Type) (β : Type) (m : TypeType) :
  • findCached? : αm (Option β)
  • cache : αβm Unit

Interface for caching results.

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
    • One or more equations did not get rendered due to their size.
    Instances For
      instance Lean.instMonadCacheReaderT {α : Type} {β : Type} {ρ : Type} {m : TypeType} [Lean.MonadCache α β m] :
      Equations
      @[always_inline]
      instance Lean.instMonadCacheExceptT {α : 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
          Equations
          • Lean.MonadHashMapCacheAdapter.instMonadCache = { findCached? := Lean.MonadHashMapCacheAdapter.findCached?, cache := Lean.MonadHashMapCacheAdapter.cache }
          def Lean.MonadCacheT {ω : Type} (α : Type) (β : Type) (m : TypeType) [STWorld ω m] [BEq α] [Hashable α] (α : Type) :
          Equations
          Instances For
            Equations
            • Lean.MonadCacheT.instMonadHashMapCacheAdapterMonadCacheT = { getCache := get, modifyCache := fun f => 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.instMonadMonadCacheT {ω : Type} {α : Type} {β : Type} {m : TypeType} [STWorld ω m] [BEq α] [Hashable α] [Monad m] :
              Equations
              instance Lean.MonadCacheT.instMonadLiftMonadCacheT {ω : Type} {α : Type} {β : Type} {m : TypeType} [STWorld ω m] [BEq α] [Hashable α] :
              Equations
              instance Lean.MonadCacheT.instMonadControlMonadCacheT {ω : Type} {α : Type} {β : Type} {m : TypeType} [STWorld ω m] [BEq α] [Hashable α] :
              Equations
              instance Lean.MonadCacheT.instMonadFinallyMonadCacheT {ω : Type} {α : Type} {β : Type} {m : TypeType} [STWorld ω m] [BEq α] [Hashable α] [Monad m] [MonadFinally m] :
              Equations
              instance Lean.MonadCacheT.instMonadRefMonadCacheT {ω : Type} {α : Type} {β : Type} {m : TypeType} [STWorld ω m] [BEq α] [Hashable α] [Monad m] [Lean.MonadRef m] :
              Equations
              instance Lean.MonadCacheT.instAlternativeMonadCacheT {ω : 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.instMonadHashMapCacheAdapterMonadStateCacheT = { getCache := get, modifyCache := fun f => modify f }
                @[inline]
                def Lean.MonadStateCacheT.run {α : Type} {β : Type} {m : TypeType} [BEq α] [Hashable α] [Monad m] {σ : Type} (x : Lean.MonadStateCacheT α β m σ) :
                m σ
                Equations
                Instances For
                  Equations
                  Equations
                  Equations
                  Equations
                  Equations