~/bend-docscommunity

spec/containers/lru.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as Lru

3 imports
import Base
import ../../src/math/u64.bend as W
import ./hash_table.bend as HT

Types

type Ent source · line 21 · raw

@-V:Data -> Data

t = 1: timed, due at dl; t = 0: immortal

type Ctr source · line 24 · raw

Data

type Lru source · line 28 · raw

@-V:Data -> Data

on != 0: entries get a lifetime of life milliseconds

type Made source · line 31 · raw

@-V:Data -> Data

Definitions

def inc_hi source · line 37 · raw

@+lo:U32 -> @+hi:U32 -> @wrap:Bool -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64

def inc64 source · line 45 · raw

@x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64

x + 1, wrapping at 2^64

def zero_ctr source · line 50 · raw

Ctr

def c_ins source · line 53 · raw

@c:Ctr -> Ctr

def c_ev source · line 58 · raw

@c:Ctr -> Ctr

def c_rm source · line 63 · raw

@c:Ctr -> Ctr

def c_hit source · line 68 · raw

@c:Ctr -> Ctr

def c_miss source · line 73 · raw

@c:Ctr -> Ctr

def c_miss_if source · line 78 · raw

@c:Ctr -> @tracked:Bool -> Ctr

def expired source · line 88 · raw

@+d:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> Bool

a zero deadline never expires; otherwise deadline <= now (signed)

Templates

template gone source · line 91 · raw

@-V:Data -> @e:Ent<V> -> @now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> Bool

template mk_c source · line 97 · raw

@-V:Data -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+key:String -> @v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @off:Bool -> Ent<V>

the entry add stores: immortal without a lifetime, else due at now + life

template mk source · line 104 · raw

@-V:Data -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+key:String -> @v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> Ent<V>

template keys_of source · line 109 · raw

@-V:Data -> @es:List<&2, Ent<V>> -> List<&2, String>

template find source · line 116 · raw

@-V:Data -> @es:List<&2, Ent<V>> -> @+key:String -> Maybe<&2, Ent<V>>

template drop source · line 126 · raw

@-V:Data -> @es:List<&2, Ent<V>> -> @+key:String -> List<&2, Ent<V>>

the list without key's entry

template snoc source · line 135 · raw

@-V:Data -> @es:List<&2, Ent<V>> -> @e:Ent<V> -> List<&2, Ent<V>>

template length source · line 142 · raw

@-V:Data -> @es:List<&2, Ent<V>> -> Nat

template tail source · line 149 · raw

@-V:Data -> @es:List<&2, Ent<V>> -> List<&2, Ent<V>>

template val_of source · line 156 · raw

@-V:Data -> @e:Ent<V> -> V

template new_c source · line 163 · raw

@-V:Data -> @+cap:U32 -> @zero:Bool -> @reserved:Bool -> Made<V>

template new source · line 172 · raw

@-V:Data -> @+cap:U32 -> Made<V>

template capacity source · line 175 · raw

@-V:Data -> @l:Lru<V> -> U32

template len source · line 180 · raw

@-V:Data -> @l:Lru<V> -> U32

template counters source · line 185 · raw

@-V:Data -> @l:Lru<V> -> Ctr

template set_lifetime source · line 190 · raw

@-V:Data -> @l:Lru<V> -> @+ns:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> Lru<V>

template drop_oldest source · line 196 · raw

@-V:Data -> @l:Lru<V> -> Lru<V>

drop the oldest entry, counted by f

template add_absent source · line 201 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @es:List<&2, Ent<V>> -> @+c:Ctr -> @e:Ent<V> -> @full:Bool -> Pair(Lru<V>, Bool)

template add_found source · line 208 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @e:Ent<V> -> @m:Maybe<&2, Ent<V>> -> Pair(Lru<V>, Bool)

template add source · line 216 · raw

@-V:Data -> @l:Lru<V> -> @+key:String -> @v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> Pair(Lru<V>, Bool)

insert or replace key; the Bool reports whether an entry was evicted

template read_live source · line 221 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+e:Ent<V> -> @tracked:Bool -> Pair(Lru<V>, Maybe<&2, V>)

template read_found source · line 228 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+tracked:Bool -> @m:Maybe<&2, Ent<V>> -> Pair(Lru<V>, Maybe<&2, V>)

template read source · line 236 · raw

@-V:Data -> @l:Lru<V> -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+tracked:Bool -> Pair(Lru<V>, Maybe<&2, V>)

tracked (get): touch, count a hit or a miss; untracked (peek): neither

template get source · line 241 · raw

@-V:Data -> @l:Lru<V> -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> Pair(Lru<V>, Maybe<&2, V>)

template peek source · line 244 · raw

@-V:Data -> @l:Lru<V> -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> Pair(Lru<V>, Maybe<&2, V>)

template contains_found source · line 247 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @m:Maybe<&2, Ent<V>> -> Pair(Lru<V>, Bool)

template contains source · line 254 · raw

@-V:Data -> @l:Lru<V> -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> Pair(Lru<V>, Bool)

template remove_found source · line 259 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @m:Maybe<&2, Ent<V>> -> Pair(Lru<V>, Maybe<&2, V>)

template remove source · line 266 · raw

@-V:Data -> @l:Lru<V> -> @+key:String -> Pair(Lru<V>, Maybe<&2, V>)

template purge source · line 271 · raw

@-V:Data -> @l:Lru<V> -> Pair(Lru<V>, U32)

template shrink source · line 277 · raw

@-V:Data -> @fuel:Nat -> @l:Lru<V> -> @+ev:U32 -> Pair(Lru<V>, U32)

evict the oldest until the cache fits, counting them

template rs_done source · line 286 · raw

@-V:Data -> @r:Pair(Lru<V>, U32) -> Pair(Lru<V>, Result<&2, &2, String, U32>)

template resize_c source · line 291 · raw

@-V:Data -> @+c0:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+cap:U32 -> @zero:Bool -> Pair(Lru<V>, Result<&2, &2, String, U32>)

template resize source · line 299 · raw

@-V:Data -> @l:Lru<V> -> @+cap:U32 -> Pair(Lru<V>, Result<&2, &2, String, U32>)

capacity 0 fails; otherwise evict the oldest until the cache fits

template expire source · line 305 · raw

@-V:Data -> @fuel:Nat -> @l:Lru<V> -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> Lru<V>

drop the expired oldest prefix, each a removal

template keys_fin source · line 318 · raw

@-V:Data -> @l:Lru<V> -> Pair(Lru<V>, List<&2, String>)

template keys source · line 324 · raw

@-V:Data -> @l:Lru<V> -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> Pair(Lru<V>, List<&2, String>)

the keys oldest first, after the expired oldest prefix is dropped

template last_go source · line 365 · raw

@-V:Data -> @t:List<&2, Ent<V>> -> @h:Ent<V> -> Maybe<&2, Ent<V>>

template last source · line 372 · raw

@-V:Data -> @es:List<&2, Ent<V>> -> Maybe<&2, Ent<V>>

template es_of source · line 379 · raw

@-V:Data -> @l:Lru<V> -> List<&2, Ent<V>>

template Empty_Map.new_empty source · line 385 · raw

@-V:Data -> @+cap:U32 -> @+hz:{U32.is_eq(cap, 0) == False{} : Bool} -> @+hm:{U32.is_eq(cap, 4294967295) == False{} : Bool} -> Type

Empty_Map (103)

template Empty_Map.new_rejects_zero source · line 389 · raw

@-V:Data -> Type

Empty_Map (103)

template Empty_Map.new_rejects_max source · line 393 · raw

@-V:Data -> Type

Empty_Map (103)

template Length.length_value source · line 397 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> Type

Length (117)

template Capacity.capacity_value source · line 401 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> Type

Capacity (400)

template Include.add_present_order source · line 405 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+old:Ent<V> -> @+hf:{find(V, es, key) == Some{old} : Maybe<&2, Ent<V>>} -> Type

Include (729), present key

template Include.add_present_newest source · line 409 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+old:Ent<V> -> @+hf:{find(V, es, key) == Some{old} : Maybe<&2, Ent<V>>} -> Type

Include (729), present key

template Include.add_present_length source · line 413 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+old:Ent<V> -> @+hf:{find(V, es, key) == Some{old} : Maybe<&2, Ent<V>>} -> Type

Include (729), present key

template Include.add_room_order source · line 417 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{find(V, es, key) == None{} : Maybe<&2, Ent<V>>} -> @+hr:{U32.is_le(cap, U32.from_nat(length(V, es))) == False{} : Bool} -> Type

Include / Insert (619), room

template Include.add_room_newest source · line 421 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{find(V, es, key) == None{} : Maybe<&2, Ent<V>>} -> @+hr:{U32.is_le(cap, U32.from_nat(length(V, es))) == False{} : Bool} -> Type

Include / Insert (619), room

template Include.add_room_length source · line 425 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{find(V, es, key) == None{} : Maybe<&2, Ent<V>>} -> @+hr:{U32.is_le(cap, U32.from_nat(length(V, es))) == False{} : Bool} -> Type

Include / Insert (619), room

template Include.add_evict_order source · line 429 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{find(V, es, key) == None{} : Maybe<&2, Ent<V>>} -> @+hfu:{U32.is_le(cap, U32.from_nat(length(V, es))) == True{} : Bool} -> Type

Include, full (LRU eviction)

template Include.add_evict_newest source · line 433 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{find(V, es, key) == None{} : Maybe<&2, Ent<V>>} -> @+hfu:{U32.is_le(cap, U32.from_nat(length(V, es))) == True{} : Bool} -> Type

Include, full (LRU eviction)

template Include.add_evict_length source · line 437 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+h:Ent<V> -> @+t:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+v:V -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{find(V, h <> t, key) == None{} : Maybe<&2, Ent<V>>} -> @+hfu:{U32.is_le(cap, U32.from_nat(length(V, h <> t))) == True{} : Bool} -> Type

Include, full (LRU eviction)

template Element.get_hit source · line 441 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+e:Ent<V> -> @+hf:{find(V, es, key) == Some{e} : Maybe<&2, Ent<V>>} -> @+hg:{gone(V, e, now) == False{} : Bool} -> Type

Element (1039) + touch

template Element.get_hit_newest source · line 445 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+e:Ent<V> -> @+hf:{find(V, es, key) == Some{e} : Maybe<&2, Ent<V>>} -> @+hg:{gone(V, e, now) == False{} : Bool} -> Type

Element (1039) + touch

template Element.get_miss source · line 449 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{find(V, es, key) == None{} : Maybe<&2, Ent<V>>} -> Type

Element (1039) + touch

template Iter_Model.read_expired source · line 453 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+tracked:Bool -> @+e:Ent<V> -> @+hf:{find(V, es, key) == Some{e} : Maybe<&2, Ent<V>>} -> @+hg:{gone(V, e, now) == True{} : Bool} -> Type

Iter_Model (1078)

template Element.peek_hit source · line 457 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+e:Ent<V> -> @+hf:{find(V, es, key) == Some{e} : Maybe<&2, Ent<V>>} -> @+hg:{gone(V, e, now) == False{} : Bool} -> Type

Element (1039), no touch

template Element.peek_miss source · line 461 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{find(V, es, key) == None{} : Maybe<&2, Ent<V>>} -> Type

Element (1039), no touch

template Contains.contains_live source · line 465 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+e:Ent<V> -> @+hf:{find(V, es, key) == Some{e} : Maybe<&2, Ent<V>>} -> @+hg:{gone(V, e, now) == False{} : Bool} -> Type

Contains (1032)

template Contains.contains_expired source · line 469 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+e:Ent<V> -> @+hf:{find(V, es, key) == Some{e} : Maybe<&2, Ent<V>>} -> @+hg:{gone(V, e, now) == True{} : Bool} -> Type

Contains (1032)

template Contains.contains_absent source · line 473 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+now:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+hf:{find(V, es, key) == None{} : Maybe<&2, Ent<V>>} -> Type

Contains (1032)

template Delete.remove_present source · line 477 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+e:Ent<V> -> @+hf:{find(V, es, key) == Some{e} : Maybe<&2, Ent<V>>} -> Type

Delete (891) / Exclude (851)

template Delete.remove_absent source · line 481 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> @+key:String -> @+hf:{find(V, es, key) == None{} : Maybe<&2, Ent<V>>} -> Type

Delete (891) / Exclude (851)

template Clear.purge_value source · line 485 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> Type

Clear (427)

template Iter_Model.keys_fin_value source · line 489 · raw

@-V:Data -> @+cap:U32 -> @+on:U32 -> @+life:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/math/u64.U64 -> @+es:List<&2, Ent<V>> -> @+c:Ctr -> Type

Iter_Model (1078)