1	import Base
2	import ../types/model.bend as T
3	import ./cache.bend as C
4	import ./time.bend as Time
5	import ./entry_ops.bend as Entry
6	
7	# Historical phase API retained for checked lemmas. The public runtime imports
8	# entry_ops directly; do not build new public behavior on this legacy protocol.
9	
10	# At this explicit removal boundary the key is absent and Len is decremented,
11	# but Removals/Evictions/Misses/Inserts have NOT yet changed.
12	def detach_present(-K: Data, -V: Data, c: C.Cache<K, V>, +code: String, +entry: T.Entry<K, V>) -> C.Step<K, V>:
13	  C.State{cap, table, order, life, counts, +cb} = c
14	  C.Out{C.State{cap, Map.del(&2, Maybe<&2, T.Entry<K, V>>, table, code), C.without(order, code), life, counts, cb}, Some{entry}, True{}, C.events(K, V, cb, entry)}
15	
16	def detach_found(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, found: Maybe<&2, T.Entry<K, V>>) -> C.Step<K, V>:
17	  match found:
18	    case None{}:
19	      C.Out{c, None{}, False{}, Nil{}}
20	    case Some{entry}:
21	      detach_present(K, V, c, code, entry)
22	
23	def detach(-K: Data, -V: Data, +c: C.Cache<K, V>, +code: String) -> C.Step<K, V>:
24	  detach_found(K, V, c, code, C.lookup(K, V, c, code))
25	
26	def detach_first(-K: Data, -V: Data, c: C.Cache<K, V>, order: List<&2, String>) -> C.Step<K, V>:
27	  match order:
28	    case Nil{}:
29	      C.Out{c, None{}, False{}, Nil{}}
30	    case Con{code, rest}:
31	      detach(K, V, c, code)
32	
33	def detach_oldest(-K: Data, -V: Data, +c: C.Cache<K, V>) -> C.Step<K, V>:
34	  C.State{cap, table, order, life, counts, cb} = c
35	  detach_first(K, V, c, order)
36	
37	def finish_removal(-K: Data, -V: Data, c: C.Cache<K, V>, evict: Bool) -> C.Cache<K, V>:
38	  C.State{cap, table, order, life, counts, cb} = c
39	  C.State{cap, table, order, life, C.removal_counts(counts, evict), cb}
40	
41	def finish_miss(-K: Data, -V: Data, c: C.Cache<K, V>, tracked: Bool) -> C.Cache<K, V>:
42	  Entry.finish_miss(K, V, c, tracked)
43	
44	def prepare_room(-K: Data, -V: Data, c: C.Cache<K, V>, full: Bool) -> C.Step<K, V>:
45	  match full:
46	    case False{}:
47	      C.Out{c, None{}, False{}, Nil{}}
48	    case True{}:
49	      detach_oldest(K, V, c)
50	
51	def prepare_found(-K: Data, -V: Data, +c: C.Cache<K, V>, found: Maybe<&2, T.Entry<K, V>>) -> C.Step<K, V>:
52	  match found:
53	    case Some{entry}:
54	      C.Out{c, None{}, False{}, Nil{}}
55	    case None{}:
56	      prepare_room(K, V, c, Nat.is_eq(C.len(K, V, c), C.capacity(K, V, c)))
57	
58	def prepare_add(-K: Data, -V: Data, +c: C.Cache<K, V>, code: String) -> C.Step<K, V>:
59	  prepare_found(K, V, c, C.lookup(K, V, c, code))
60	
61	type Read<-K: Data, -V: Data> is Data:
62	  Reading{step: C.Step<K, V>, removed: Bool}
63	
64	def expired_read(-K: Data, -V: Data, step: C.Step<K, V>) -> Read<K, V>:
65	  C.Out{c, item, flag, events} = step
66	  Reading{C.Out{c, item, False{}, events}, True{}}
67	
68	def decide_read(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, entry: T.Entry<K, V>, tracked: Bool, expired: Bool) -> Read<K, V>:
69	  match expired:
70	    case False{}:
71	      Reading{C.read_live(K, V, c, code, entry, tracked), False{}}
72	    case True{}:
73	      expired_read(K, V, detach(K, V, c, code))
74	
75	def read_found(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, now: T.Int64, tracked: Bool, found: Maybe<&2, T.Entry<K, V>>) -> Read<K, V>:
76	  match found:
77	    case None{}:
78	      Reading{C.Out{finish_miss(K, V, c, tracked), None{}, False{}, Nil{}}, False{}}
79	    case Some{T.Item{k, v, +d}}:
80	      decide_read(K, V, c, code, T.Item{k, v, d}, tracked, Time.expired(d, now))
81	
82	def read(-K: Data, -V: Data, +c: C.Cache<K, V>, +code: String, now: T.Int64, tracked: Bool) -> Read<K, V>:
83	  read_found(K, V, c, code, now, tracked, C.lookup(K, V, c, code))
84	
85	type Mode is Data:
86	  All{}
87	  Expired{}
88	  KeyList{}
89	  ValueList{}
90	
91	# Closed aggregate mode prevents invalid numeric mode values.
92	# These are internal removal and clock requests. No user code runs at removal.
93	type Aggregate<-K: Data, -V: Data> is Data:
94	  Complete{cache: C.Cache<K, V>, keys: List<&2, K>, values: List<&2, V>}
95	  NeedClock{cache: C.Cache<K, V>, remaining: Nat, kind: Mode}
96	  RemovalReady{step: C.Step<K, V>, remaining: Nat, kind: Mode}
97	
98	def keys_of(-K: Data, -V: Data, xs: List<&2, T.Entry<K, V>>) -> List<&2, K>:
99	  Entry.keys_of(K, V, xs)
100	
101	def values_of(-K: Data, -V: Data, xs: List<&2, T.Entry<K, V>>) -> List<&2, V>:
102	  Entry.values_of(K, V, xs)
103	
104	def complete(-K: Data, -V: Data, +c: C.Cache<K, V>, kind: Mode) -> Aggregate<K, V>:
105	  match kind:
106	    case All{}:
107	      Complete{C.clear_metrics(K, V, c), Nil{}, Nil{}}
108	    case KeyList{}:
109	      Complete{c, keys_of(K, V, C.entries(K, V, c)), Nil{}}
110	    case ValueList{}:
111	      Complete{c, Nil{}, values_of(K, V, C.entries(K, V, c))}
112	    case Expired{}:
113	      Complete{c, Nil{}, Nil{}}
114	
115	def need_clock(-K: Data, -V: Data, c: C.Cache<K, V>, remaining: Nat, kind: Mode, finite: Bool) -> Aggregate<K, V>:
116	  match finite:
117	    case False{}:
118	      complete(K, V, c, kind)
119	    case True{}:
120	      NeedClock{c, remaining, kind}
121	
122	def aggregate_next(-K: Data, -V: Data, remaining: Nat, +c: C.Cache<K, V>, kind: Mode) -> Aggregate<K, V>:
123	  match remaining kind:
124	    case 0n k:
125	      complete(K, V, c, k)
126	    case 1n+p All{}:
127	      RemovalReady{detach_oldest(K, V, c), p, All{}}
128	    case 1n+p k:
129	      need_clock(K, V, c, p, k, C.purge_needs_clock(K, V, c))
130	
131	def after_removal(-K: Data, -V: Data, remaining: Nat, c: C.Cache<K, V>, kind: Mode) -> Aggregate<K, V>:
132	  aggregate_next(K, V, remaining, finish_removal(K, V, c, False{}), kind)
133	
134	def clock_decide(-K: Data, -V: Data, c: C.Cache<K, V>, remaining: Nat, kind: Mode, expired: Bool) -> Aggregate<K, V>:
135	  match expired:
136	    case False{}:
137	      complete(K, V, c, kind)
138	    case True{}:
139	      RemovalReady{detach_oldest(K, V, c), remaining, kind}
140	
141	def clock_entry(-K: Data, -V: Data, c: C.Cache<K, V>, remaining: Nat, kind: Mode, now: T.Int64, entry: Maybe<&2, T.Entry<K, V>>) -> Aggregate<K, V>:
142	  match entry:
143	    case None{}:
144	      complete(K, V, c, kind)
145	    case Some{T.Item{k, v, d}}:
146	      clock_decide(K, V, c, remaining, kind, Time.expired(d, now))
147	
148	def after_clock(-K: Data, -V: Data, +c: C.Cache<K, V>, remaining: Nat, kind: Mode, now: T.Int64) -> Aggregate<K, V>:
149	  clock_entry(K, V, c, remaining, kind, now, C.oldest_entry(K, V, c))
150	
151	def purge(-K: Data, -V: Data, +c: C.Cache<K, V>) -> Aggregate<K, V>:
152	  aggregate_next(K, V, C.len(K, V, c), c, All{})
153	
154	def purge_expired(-K: Data, -V: Data, +c: C.Cache<K, V>) -> Aggregate<K, V>:
155	  aggregate_next(K, V, C.len(K, V, c), c, Expired{})
156	
157	def keys(-K: Data, -V: Data, +c: C.Cache<K, V>) -> Aggregate<K, V>:
158	  aggregate_next(K, V, C.len(K, V, c), c, KeyList{})
159	
160	def values(-K: Data, -V: Data, +c: C.Cache<K, V>) -> Aggregate<K, V>:
161	  aggregate_next(K, V, C.len(K, V, c), c, ValueList{})
162	
163	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>:
164	  Entry.refresh_prepare_found(K, V, c, code, found)
165	
166	def refresh_prepare(-K: Data, -V: Data, +c: C.Cache<K, V>, +code: String) -> C.Step<K, V>:
167	  Entry.refresh_prepare(K, V, c, code)
168	
169	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>:
170	  Entry.refresh_at(K, V, c, code, entry, lifetime, now)
171	
172	# Pure fold of detach and count-update phases. The callback-free host performs
173	# these internal phases without invoking user code.
174	def finish_detached(-K: Data, -V: Data, step: C.Step<K, V>, evict: Bool) -> C.Step<K, V>:
175	  C.Out{c, item, flag, events} = step
176	  match flag:
177	    case False{}:
178	      C.Out{c, item, False{}, events}
179	    case True{}:
180	      C.Out{finish_removal(K, V, c, evict), item, True{}, events}