def LeanRedis.Inflight : Type

Equations

• LeanRedis.Inflight = IO.Promise (Except IO.Error String)

structure LeanRedis.Cache (τ : Type) : Type

Cache Aside pattern with a Redis backend. When a cache miss occurs, we fetch from the source callback and store it in Redis. Cache Stampete prevention with inflight request detection.

• redis : Client τ
• inflight : Std.Mutex (Std.HashMap String Inflight)

inductive LeanRedis.CacheInflightStatus : Type

Simple Inflight Status of a key

• hit: The value is cached
• missInflight: The value is not cached, but a request to retrieve it is pending
• miss: The value is not cached, we need to create a request to retrieve it

• hit (value : String) : CacheInflightStatus
• missInflight (consume : Inflight) : CacheInflightStatus
• miss (produce : Inflight) : CacheInflightStatus

structure LeanRedis.CacheSWROptions : Type

Options for CacheSWR operations.

• staleTtl: seconds after which a cached value is considered stale
• ttl: optional overall Redis key TTL for eviction (default: staleTtl * 2)

• staleTtl : UInt64
• ttl : Option UInt64

@[implicit_reducible]

instance LeanRedis.instInhabitedCacheSWROptions : Inhabited CacheSWROptions

Equations

• LeanRedis.instInhabitedCacheSWROptions = { default := LeanRedis.instInhabitedCacheSWROptions.default }

@[implicit_reducible]

instance LeanRedis.instBEqCacheSWROptions : BEq CacheSWROptions

Equations

• LeanRedis.instBEqCacheSWROptions = { beq := LeanRedis.instBEqCacheSWROptions.beq }

def LeanRedis.instBEqCacheSWROptions.beq : CacheSWROptions → CacheSWROptions → Bool

Equations

• LeanRedis.instBEqCacheSWROptions.beq { staleTtl := a, ttl := a_1 } { staleTtl := b, ttl := b_1 } = (a == b && a_1 == b_1)
• LeanRedis.instBEqCacheSWROptions.beq x✝¹ x✝ = false

def LeanRedis.instReprCacheSWROptions.repr : CacheSWROptions → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance LeanRedis.instReprCacheSWROptions : Repr CacheSWROptions

Equations

• LeanRedis.instReprCacheSWROptions = { reprPrec := LeanRedis.instReprCacheSWROptions.repr }

structure LeanRedis.CacheSWR (τ : Type) : Type

Cache Aside pattern with a Redis backend with stale while revalidate. When a cache stale occurs, we return the stale value and fetch from the source callback in the background. When a cache miss occurs, we fetch from the source callback and store it in Redis. Cache Stampete prevention with inflight request detection.

• redis : Client τ
• inflight : Std.Mutex (Std.HashMap String Inflight)

inductive LeanRedis.CacheSWRStatus : Type

Advanced Status for stale while revalidate pattern.

• hit: The value is cached and fresh
• stale: The value is cached but stale, we need to refresh it with the given promise
• staleInflight: The value is cached but stale, and a refresh is already in flight
• missInflight: The value is not cached, but a request to retrieve it is pending
• miss: The value is not cached, we need to create a request to retrieve it

• hit (value : String) : CacheSWRStatus
• staleInflight (value : String) : CacheSWRStatus
• stale (value : String) (produce : Inflight) : CacheSWRStatus
• missInflight (consume : Inflight) : CacheSWRStatus
• miss (produce : Inflight) : CacheSWRStatus