1	import Base
2	import ../types/model.bend as T
3	import ./time.bend as Time
4	
5	# The list is oldest first; it contains only encoded keys, never values.
6	type Cache<-K: Data, -V: Data> is Data:
7	  State{capacity: Nat, table: Map<&2, Maybe<&2, T.Entry<K, V>>>, order: List<&2, String>, lifetime: T.Int64, counts: T.Metrics, callback: Bool}
8	
9	type Step<-K: Data, -V: Data> is Data:
10	  Out{cache: Cache<K, V>, item: Maybe<&2, T.Entry<K, V>>, flag: Bool, events: List<&2, T.LruEvent<K, V>>}
11	
12	def init(-K: Data, -V: Data, capacity: Nat) -> Cache<K, V>:
13	  State{capacity, Map.new(&2, Maybe<&2, T.Entry<K, V>>), Nil{}, T.I64{Word.zero(64n)}, T.zero_metrics(), False{}}
14	
15	def new_checked(-K: Data, -V: Data, capacity: Nat, valid: Bool) -> Result<&2, &2, String, Cache<K, V>>:
16	  match valid:
17	    case False{}:
18	      Fail{"invalid capacity or size"}
19	    case True{}:
20	      Done{init(K, V, capacity)}
21	
22	def construct(-K: Data, -V: Data, capacity: U32, size: U32, zero: Bool, reserved: Bool, small: Bool) -> Result<&2, &2, String, Cache<K, V>>:
23	  match zero reserved small:
24	    case True{} a b:
25	      Fail{"capacity must be positive"}
26	    case False{} True{} b:
27	      Fail{"size must not be 0XFFFFFFFF"}
28	    case False{} False{} True{}:
29	      Fail{"size (" ++ U32.show(size) ++ ") is smaller than capacity (" ++ U32.show(capacity) ++ ")"}
30	    case False{} False{} False{}:
31	      Done{init(K, V, U32.to_nat(capacity))}
32	
33	def new_with_size(-K: Data, -V: Data, +capacity: U32, +size: U32) -> Result<&2, &2, String, Cache<K, V>>:
34	  construct(K, V, capacity, size, U32.is_eq(capacity, 0), U32.is_eq(size, 4294967295), U32.is_lt(size, capacity))
35	
36	def new(-K: Data, -V: Data, +capacity: U32) -> Result<&2, &2, String, Cache<K, V>>:
37	  new_with_size(K, V, capacity, capacity)
38	
39	def len(-K: Data, -V: Data, +c: Cache<K, V>) -> Nat:
40	  State{cap, m, order, life, counts, cb} = c
41	  List.length(&2, String, order)
42	
43	law without:
44	  for xs: List<&2, String>
45	  for +key: String
46	  List<&2, String>
47	
48	def without_keep(h: String, tail: List<&2, String>, eq: Bool) -> List<&2, String>:
49	  match eq:
50	    case True{}:
51	      tail
52	    case False{}:
53	      Con{h, tail}
54	
55	def without(xs, key):
56	  match xs:
57	    case Nil{}:
58	      Nil{}
59	    case Con{+h, tail}:
60	      without_keep(h, without(tail, key), String.eq(h, key))
61	
62	def events(-K: Data, -V: Data, cb: Bool, e: T.Entry<K, V>) -> List<&2, T.LruEvent<K, V>>:
63	  match cb:
64	    case False{}:
65	      Nil{}
66	    case True{}:
67	      T.Item{k, v, d} = e
68	      Con{T.Evicted{k, v}, Nil{}}
69	
70	def removal_counts(m: T.Metrics, capacity_eviction: Bool) -> T.Metrics:
71	  T.Counts{i, e, r, h, s} = m
72	  match capacity_eviction:
73	    case True{}:
74	      T.Counts{i, Word.inc(64n, e), r, h, s}
75	    case False{}:
76	      T.Counts{i, e, Word.inc(64n, r), h, s}
77	
78	def lookup_result(-K: Data, -V: Data, result: Map<&2, Maybe<&2, T.Entry<K, V>>> & Maybe<&2, T.Entry<K, V>>) -> Maybe<&2, T.Entry<K, V>>:
79	  (m, found) = result
80	  found
81	
82	def lookup(-K: Data, -V: Data, c: Cache<K, V>, code: String) -> Maybe<&2, T.Entry<K, V>>:
83	  State{cap, m, order, life, counts, cb} = c
84	  lookup_result(K, V, Map.get(Maybe<&2, T.Entry<K, V>>, None{}, m, code))
85	
86	def remove_present(-K: Data, -V: Data, c: Cache<K, V>, +key: String, evict: Bool, +entry: T.Entry<K, V>) -> Step<K, V>:
87	  State{cap, m, order, life, counts, +cb} = c
88	  Out{State{cap, Map.del(&2, Maybe<&2, T.Entry<K, V>>, m, key), without(order, key), life, removal_counts(counts, evict), cb}, Some{entry}, True{}, events(K, V, cb, entry)}
89	
90	def remove_found(-K: Data, -V: Data, c: Cache<K, V>, key: String, evict: Bool, found: Maybe<&2, T.Entry<K, V>>) -> Step<K, V>:
91	  match found:
92	    case None{}:
93	      Out{c, None{}, False{}, Nil{}}
94	    case Some{entry}:
95	      remove_present(K, V, c, key, evict, entry)
96	
97	def remove_encoded(-K: Data, -V: Data, +c: Cache<K, V>, +key: String, evict: Bool) -> Step<K, V>:
98	  remove_found(K, V, c, key, evict, lookup(K, V, c, key))
99	
100	def remove(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K) -> Step<K, V>:
101	  remove_encoded(K, V, c, encode(key), False{})
102	
103	def oldest_remove(-K: Data, -V: Data, +c: Cache<K, V>, order: List<&2, String>, evict: Bool) -> Step<K, V>:
104	  match order:
105	    case Nil{}:
106	      Out{c, None{}, False{}, Nil{}}
107	    case Con{k, rest}:
108	      remove_encoded(K, V, c, k, evict)
109	
110	def remove_oldest(-K: Data, -V: Data, +c: Cache<K, V>, evict: Bool) -> Step<K, V>:
111	  State{cap, m, order, life, counts, cb} = c
112	  oldest_remove(K, V, c, order, evict)
113	
114	def store(-K: Data, -V: Data, +c: Cache<K, V>, +code: String, key: K, value: V, deadline: T.Int64, flag: Bool, evs: List<&2, T.LruEvent<K, V>>) -> Step<K, V>:
115	  State{cap, m, order, life, counts, cb} = c
116	  T.Counts{i, e, r, h, s} = counts
117	  Out{State{cap, Map.set(&2, Maybe<&2, T.Entry<K, V>>, m, code, Some{T.Item{key, value, deadline}}), List.append(&2, String, without(order, code), Con{code, Nil{}}), life, T.Counts{Word.inc(64n, i), e, r, h, s}, cb}, None{}, flag, evs}
118	
119	def store_after_evict(-K: Data, -V: Data, code: String, key: K, value: V, deadline: T.Int64, step: Step<K, V>) -> Step<K, V>:
120	  Out{c, item, flag, evs} = step
121	  store(K, V, c, code, key, value, deadline, flag, evs)
122	
123	def add_room(-K: Data, -V: Data, +c: Cache<K, V>, code: String, key: K, value: V, deadline: T.Int64, full: Bool) -> Step<K, V>:
124	  match full:
125	    case False{}:
126	      store(K, V, c, code, key, value, deadline, False{}, Nil{})
127	    case True{}:
128	      store_after_evict(K, V, code, key, value, deadline, remove_oldest(K, V, c, True{}))
129	
130	def capacity(-K: Data, -V: Data, c: Cache<K, V>) -> Nat:
131	  State{cap, m, order, life, counts, cb} = c
132	  cap
133	
134	def add_found(-K: Data, -V: Data, +c: Cache<K, V>, code: String, key: K, value: V, deadline: T.Int64, found: Maybe<&2, T.Entry<K, V>>) -> Step<K, V>:
135	  match found:
136	    case None{}:
137	      add_room(K, V, c, code, key, value, deadline, Nat.is_ge(len(K, V, c), capacity(K, V, c)))
138	    case Some{T.Item{original, old, expiry}}:
139	      store(K, V, c, code, original, value, deadline, False{}, Nil{})
140	
141	def add_with_lifetime(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, +key: K, value: V, ns: T.Int64, now: T.Int64) -> Step<K, V>:
142	  +code = encode(key)
143	  add_found(K, V, c, code, key, value, Time.deadline(now, ns), lookup(K, V, c, code))
144	
145	def add(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K, value: V, now: T.Int64) -> Step<K, V>:
146	  State{cap, m, order, life, counts, cb} = c
147	  add_with_lifetime(K, V, encode, c, key, value, life, now)
148	
149	def hit_counts(m: T.Metrics, +tracked: Bool, hit: Bool) -> T.Metrics:
150	  T.Counts{i, e, r, h, s} = m
151	  match tracked hit:
152	    case False{} unused:
153	      T.Counts{i, e, r, h, s}
154	    case True{} True{}:
155	      T.Counts{i, e, r, Word.inc(64n, h), s}
156	    case True{} False{}:
157	      T.Counts{i, e, r, h, Word.inc(64n, s)}
158	
159	def counted(-K: Data, -V: Data, step: Step<K, V>, +tracked: Bool, hit: Bool) -> Step<K, V>:
160	  Out{State{cap, m, order, life, counts, cb}, item, flag, evs} = step
161	  Out{State{cap, m, order, life, hit_counts(counts, tracked, hit), cb}, item, flag, evs}
162	
163	def miss_after_remove(-K: Data, -V: Data, step: Step<K, V>, +tracked: Bool) -> Step<K, V>:
164	  Out{c, item, flag, evs} = step
165	  counted(K, V, Out{c, item, False{}, evs}, tracked, False{})
166	
167	def touch_order(order: List<&2, String>, +code: String, touch: Bool) -> List<&2, String>:
168	  match touch:
169	    case False{}:
170	      order
171	    case True{}:
172	      List.append(&2, String, without(order, code), Con{code, Nil{}})
173	
174	def read_live(-K: Data, -V: Data, +c: Cache<K, V>, code: String, +entry: T.Entry<K, V>, +tracked: Bool) -> Step<K, V>:
175	  State{cap, m, order, life, counts, cb} = c
176	  Out{State{cap, m, touch_order(order, code, tracked), life, hit_counts(counts, tracked, True{}), cb}, Some{entry}, True{}, Nil{}}
177	
178	def read_expiry(-K: Data, -V: Data, +c: Cache<K, V>, code: String, entry: T.Entry<K, V>, +tracked: Bool, expired: Bool) -> Step<K, V>:
179	  match expired:
180	    case False{}:
181	      read_live(K, V, c, code, entry, tracked)
182	    case True{}:
183	      miss_after_remove(K, V, remove_encoded(K, V, c, code, False{}), tracked)
184	
185	def read_found(-K: Data, -V: Data, +c: Cache<K, V>, code: String, now: T.Int64, +tracked: Bool, found: Maybe<&2, T.Entry<K, V>>) -> Step<K, V>:
186	  match found:
187	    case None{}:
188	      counted(K, V, Out{c, None{}, False{}, Nil{}}, tracked, False{})
189	    case Some{T.Item{k, v, +d}}:
190	      read_expiry(K, V, c, code, T.Item{k, v, d}, tracked, Time.expired(d, now))
191	
192	def read_encoded(-K: Data, -V: Data, +c: Cache<K, V>, +code: String, now: T.Int64, +tracked: Bool) -> Step<K, V>:
193	  read_found(K, V, c, code, now, tracked, lookup(K, V, c, code))
194	
195	def get(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K, now: T.Int64) -> Step<K, V>:
196	  read_encoded(K, V, c, encode(key), now, True{})
197	
198	def peek(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K, now: T.Int64) -> Step<K, V>:
199	  read_encoded(K, V, c, encode(key), now, False{})
200	
201	def refresh_present(-K: Data, -V: Data, c: Cache<K, V>, +code: String, +entry: T.Entry<K, V>) -> Step<K, V>:
202	  State{cap, m, order, life, counts, cb} = c
203	  read_live(K, V, State{cap, Map.set(&2, Maybe<&2, T.Entry<K, V>>, m, code, Some{entry}), order, life, counts, cb}, code, entry, True{})
204	
205	def refresh_found(-K: Data, -V: Data, +c: Cache<K, V>, +code: String, deadline: T.Int64, found: Maybe<&2, T.Entry<K, V>>) -> Step<K, V>:
206	  match found:
207	    case None{}:
208	      counted(K, V, Out{c, None{}, False{}, Nil{}}, True{}, False{})
209	    case Some{T.Item{k, v, old}}:
210	      +entry = {T.Item{k, v, deadline} : T.Entry<K, V>}
211	      refresh_present(K, V, c, code, entry)
212	
213	def get_and_refresh(-K: Data, -V: Data, encode: K -> String, +c: Cache<K, V>, key: K, ns: T.Int64, now: T.Int64) -> Step<K, V>:
214	  +code = encode(key)
215	  refresh_found(K, V, c, code, Time.deadline(now, ns), lookup(K, V, c, code))
216	
217	def set_lifetime(-K: Data, -V: Data, +c: Cache<K, V>, ns: T.Int64) -> Cache<K, V>:
218	  State{cap, m, order, life, counts, cb} = c
219	  State{cap, m, order, ns, counts, cb}
220	
221	def metrics(-K: Data, -V: Data, +c: Cache<K, V>) -> T.Metrics:
222	  State{cap, m, order, life, counts, cb} = c
223	  counts
224	
225	def reset_metrics(-K: Data, -V: Data, +c: Cache<K, V>) -> Cache<K, V> & T.Metrics:
226	  State{cap, m, order, life, counts, cb} = c
227	  (State{cap, m, order, life, T.zero_metrics(), cb}, counts)
228	
229	def oldest_read(-K: Data, -V: Data, +c: Cache<K, V>, order: List<&2, String>, now: T.Int64) -> Step<K, V>:
230	  match order:
231	    case Nil{}:
232	      Out{c, None{}, False{}, Nil{}}
233	    case Con{k, rest}:
234	      read_encoded(K, V, c, k, now, False{})
235	
236	def get_oldest(-K: Data, -V: Data, +c: Cache<K, V>, now: T.Int64) -> Step<K, V>:
237	  State{cap, m, order, life, counts, cb} = c
238	  oldest_read(K, V, c, order, now)
239	
240	def step_cache(-K: Data, -V: Data, s: Step<K, V>) -> Cache<K, V>:
241	  Out{c, item, flag, evs} = s
242	  c
243	
244	def step_events(-K: Data, -V: Data, s: Step<K, V>) -> List<&2, T.LruEvent<K, V>>:
245	  Out{c, item, flag, evs} = s
246	  evs
247	
248	def clear_metrics(-K: Data, -V: Data, c: Cache<K, V>) -> Cache<K, V>:
249	  State{cap, m, order, life, counts, cb} = c
250	  State{cap, m, order, life, T.zero_metrics(), cb}
251	
252	# No accumulated event log is stored in the cache itself.
253	def 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))}
261	
262	def purge(-K: Data, -V: Data, +c: Cache<K, V>) -> Step<K, V>:
263	  purge_loop(K, V, len(K, V, c), c)
264	
265	def first_entry(-K: Data, -V: Data, c: Cache<K, V>, order: List<&2, String>) -> Maybe<&2, T.Entry<K, V>>:
266	  match order:
267	    case Nil{}:
268	      None{}
269	    case Con{k, rest}:
270	      lookup(K, V, c, k)
271	
272	def oldest_entry(-K: Data, -V: Data, +c: Cache<K, V>) -> Maybe<&2, T.Entry<K, V>>:
273	  State{cap, m, order, life, counts, cb} = c
274	  first_entry(K, V, c, order)
275	
276	def finite_entry(-K: Data, -V: Data, e: Maybe<&2, T.Entry<K, V>>) -> Bool:
277	  match e:
278	    case None{}:
279	      False{}
280	    case Some{T.Item{k, v, d}}:
281	      Bool.not(Time.is_zero(d))
282	
283	# One oldest inspection. Immortal or empty means stop and consumes no clock read.
284	def purge_needs_clock(-K: Data, -V: Data, c: Cache<K, V>) -> Bool:
285	  finite_entry(K, V, oldest_entry(K, V, c))
286	
287	def collect_entry(-K: Data, -V: Data, entry: Maybe<&2, T.Entry<K, V>>, rest: List<&2, T.Entry<K, V>>) -> List<&2, T.Entry<K, V>>:
288	  match entry:
289	    case None{}:
290	      rest
291	    case Some{e}:
292	      Con{e, rest}
293	
294	def entries_go(-K: Data, -V: Data, order: List<&2, String>, +table: Map<&2, Maybe<&2, T.Entry<K, V>>>) -> List<&2, T.Entry<K, V>>:
295	  match order:
296	    case Nil{}:
297	      Nil{}
298	    case Con{k, rest}:
299	      collect_entry(K, V, lookup_result(K, V, Map.get(Maybe<&2, T.Entry<K, V>>, None{}, table, k)), entries_go(K, V, rest, table))
300	
301	# Raw enumeration. Public protocol Keys/Values first finish the oldest-only purge.
302	def entries(-K: Data, -V: Data, c: Cache<K, V>) -> List<&2, T.Entry<K, V>>:
303	  State{cap, table, order, life, counts, cb} = c
304	  entries_go(K, V, order, table)
305	
306	def map_size(-K: Data, -V: Data, c: Cache<K, V>) -> Nat:
307	  State{cap, m, order, life, counts, cb} = c
308	  Map.size(&2, Maybe<&2, T.Entry<K, V>>, m)