1	import Base
2	import ../types/model.bend as T
3	import ./cache.bend as C
4	import ./time.bend as Time
5	
6	# Shared entry operations used by the callback-free public machine.
7	# The historical phase protocol forwards here to retain its checked proofs.
8	# This module does not depend on that protocol or its aggregate/eviction phases.
9	
10	def finish_miss(-K: Data, -V: Data, c: C.Cache<K, V>, tracked: Bool) -> C.Cache<K, V>:
11	  C.State{cap, table, order, life, counts, cb} = c
12	  C.State{cap, table, order, life, C.hit_counts(counts, tracked, False{}), cb}
13	
14	def keys_of(-K: Data, -V: Data, xs: List<&2, T.Entry<K, V>>) -> List<&2, K>:
15	  match xs:
16	    case Nil{}:
17	      Nil{}
18	    case Con{T.Item{k, v, d}, rest}:
19	      Con{k, keys_of(K, V, rest)}
20	
21	def values_of(-K: Data, -V: Data, xs: List<&2, T.Entry<K, V>>) -> List<&2, V>:
22	  match xs:
23	    case Nil{}:
24	      Nil{}
25	    case Con{T.Item{k, v, d}, rest}:
26	      Con{v, values_of(K, V, rest)}
27	
28	def refresh_prepare_found(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, found: Maybe<&2, T.Entry<K, V>>) -> C.Step<K, V>:
29	  match found:
30	    case None{}:
31	      C.Out{finish_miss(K, V, c, True{}), None{}, False{}, Nil{}}
32	    case Some{entry}:
33	      C.read_live(K, V, c, code, entry, True{})
34	
35	def refresh_prepare(-K: Data, -V: Data, +c: C.Cache<K, V>, +code: String) -> C.Step<K, V>:
36	  refresh_prepare_found(K, V, c, code, C.lookup(K, V, c, code))
37	
38	def refresh_at(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, entry: T.Entry<K, V>, lifetime: T.Int64, now: T.Int64) -> C.Cache<K, V>:
39	  C.State{cap, table, order, life, counts, cb} = c
40	  T.Item{k, v, old} = entry
41	  C.State{cap, Map.set(&2, Maybe<&2, T.Entry<K, V>>, table, code, Some{T.Item{k, v, Time.deadline(now, lifetime)}}), order, life, counts, cb}