def purge_loop

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/lemmas/src/cache.bend:252

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/types/model.bend as T

252# No accumulated event log is stored in the cache itself.
253def purge_loop(-K: Data, -V: Data, fuel: Nat, c: Cache<K, V>) -> Step<K, V>:
254  match fuel:
255    case 0n:
256      Out{clear_metrics(K, V, c), None{}, False{}, Nil{}}
257    case 1n+p:
258      +step = remove_oldest(K, V, c, False{})
259      +rest = purge_loop(K, V, p, step_cache(K, V, step))
260      Out{step_cache(K, V, rest), None{}, False{}, List.append(&2, T.LruEvent<K, V>, step_events(K, V, step), step_events(K, V, rest))}