1	import Base
2	import ../types/model.bend as T
3	import ./cache.bend as S
4	import ./operations.bend as O
5	import ./clock.bend as Clock
6	import ./effectful_operations.bend as E
7	import ./effectful_aggregate.bend as A
8	
9	# Public callback-free observations. Metrics' storage-dependent Collisions field
10	# is always the documented zero/not-applicable adaptation. Diagnostics describe
11	# the abstract bound-entry count; refinement establishes the native leaf count.
12	type Reply<-K: Data, -V: Data> is Data:
13	  NoReply{}
14	  Boolean{value: Bool}
15	  Value{value: V, found: Bool}
16	  Oldest{key: K, value: V, found: Bool}
17	  KeyList{keys: List<&2, K>}
18	  ValueList{values: List<&2, V>}
19	  Length{length: Nat}
20	  Counters{metrics: T.Metrics}
21	  Storage{leaves: Nat, recency: Nat, capacity: Nat, metrics: T.Metrics}
22	
23	type CmdResult<-K: Data, -V: Data> is Data:
24	  Returned{state: S.Model<K, V>, reply: Reply<K, V>, remaining: List<&2, Clock.ClockEvent>, requests: Nat}
25	  Failed{state: S.Model<K, V>, error: Clock.Error, remaining: List<&2, Clock.ClockEvent>, requests: Nat}
26	
27	type Projection<-K: Data> is Data:
28	  Flag{}
29	  ValueOnly{}
30	  RemovedOldest{}
31	  CapturedOldest{key: K}
32	  Nothing{}
33	  Keys{}
34	  Values{}
35	
36	def value(-K: Data, -V: Data, zero: V, item: Maybe<&2, T.Entry<K, V>>, present: Bool) -> V:
37	  match item present:
38	    case Some{T.Item{k, v, d}} True{}: v
39	    case x y: zero
40	
41	def key(-K: Data, -V: Data, zero: K, item: Maybe<&2, T.Entry<K, V>>, present: Bool) -> K:
42	  match item present:
43	    case Some{T.Item{k, v, d}} True{}: k
44	    case x y: zero
45	
46	def project(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, zero_key: K, zero_value: V, +item: Maybe<&2, T.Entry<K, V>>, +present: Bool, kind: Projection<K>) -> Reply<K, V>:
47	  match kind:
48	    case Flag{}: Boolean{present}
49	    case ValueOnly{}: Value{value(K, V, zero_value, item, present), present}
50	    case RemovedOldest{}: Oldest{key(K, V, zero_key, item, present), value(K, V, zero_value, item, present), present}
51	    case CapturedOldest{captured}: Oldest{captured, value(K, V, zero_value, item, present), present}
52	    case Nothing{}: NoReply{}
53	    case Keys{}: KeyList{O.entry_keys(K, V, O.all_entries(~K, ~same, V, s))}
54	    case Values{}: ValueList{O.entry_values(K, V, O.all_entries(~K, ~same, V, s))}
55	
56	def observation(~K: Data, ~same: K -> K -> Bool, -V: Data, zero_key: K, zero_value: V, kind: Projection<K>, observed: S.Observation<K, V>, events: List<&2, Clock.ClockEvent>, requests: Nat) -> CmdResult<K, V>:
57	  S.Observed{+s, item, present, ignored} = observed
58	  Returned{s, project(~K, ~same, V, s, zero_key, zero_value, item, present, kind), events, requests}
59	
60	def effect(~K: Data, ~same: K -> K -> Bool, -V: Data, zero_key: K, zero_value: V, kind: Projection<K>, outcome: E.Outcome<K, V>) -> CmdResult<K, V>:
61	  match outcome:
62	    case E.Failed{s, error, events, requests}: Failed{s, error, events, requests}
63	    case E.Returned{observed, events, requests}: observation(~K, ~same, V, zero_key, zero_value, kind, observed, events, requests)
64	
65	def oldest_binding(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, zero_key: K, zero_value: V, events: List<&2, Clock.ClockEvent>, found: Maybe<&2, T.Entry<K, V>>) -> CmdResult<K, V>:
66	  match found:
67	    case None{}: Returned{s, Oldest{zero_key, zero_value, False{}}, events, 0n}
68	    case Some{T.Item{+original, v, d}}: effect(~K, ~same, V, zero_key, zero_value, CapturedOldest{original}, E.read(~K, ~same, V, s, original, False{}, events))
69	
70	def oldest_order(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, bindings: List<&2, T.Entry<K, V>>, order: List<&2, K>, zero_key: K, zero_value: V, events: List<&2, Clock.ClockEvent>) -> CmdResult<K, V>:
71	  match order:
72	    case Nil{}: Returned{s, Oldest{zero_key, zero_value, False{}}, events, 0n}
73	    case Con{first, tail}: oldest_binding(~K, ~same, V, s, zero_key, zero_value, events, S.find(~K, ~same, V, bindings, first))
74	
75	def oldest(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, zero_key: K, zero_value: V, events: List<&2, Clock.ClockEvent>) -> CmdResult<K, V>:
76	  S.Abstract{cap, bindings, order, life, counts, cb} = s
77	  oldest_order(~K, ~same, V, s, bindings, order, zero_key, zero_value, events)
78	
79	def metrics(-K: Data, -V: Data, +s: S.Model<K, V>, events: List<&2, Clock.ClockEvent>) -> CmdResult<K, V>:
80	  S.Abstract{cap, bindings, order, life, counts, cb} = s
81	  Returned{s, Counters{counts}, events, 0n}
82	
83	def reset(-K: Data, -V: Data, s: S.Model<K, V>, events: List<&2, Clock.ClockEvent>) -> CmdResult<K, V>:
84	  S.Abstract{cap, bindings, order, life, counts, cb} = s
85	  Returned{S.Abstract{cap, bindings, order, life, T.zero_metrics(), cb}, Counters{counts}, events, 0n}
86	
87	# Leaves counts the bound keys of the abstract finite map (the entries reachable
88	# through the recency list); it is independent of binding-list storage order.
89	def diagnostics(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, events: List<&2, Clock.ClockEvent>) -> CmdResult<K, V>:
90	  S.Abstract{cap, bindings, order, life, counts, cb} = s
91	  Returned{s, Storage{List.length(&2, T.Entry<K, V>, O.all_entries(~K, ~same, V, s)), List.length(&2, K, order), cap, counts}, events, 0n}
92	
93	# All typed commands have explicit independent semantics. Invalid transport and
94	# rejected host arguments need a separate marshalling relation; they are not
95	# silently coerced into one of these legal typed commands.
96	def execute(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, zero_key: K, zero_value: V, events: List<&2, Clock.ClockEvent>, command: S.Command<K, V>) -> CmdResult<K, V>:
97	  match command:
98	    case S.Add{k, v}: effect(~K, ~same, V, zero_key, zero_value, Flag{}, E.add(~K, ~same, V, s, k, v, events))
99	    case S.AddWithLifetime{k, v, ns}: effect(~K, ~same, V, zero_key, zero_value, Flag{}, E.add_with_lifetime(~K, ~same, V, s, k, v, ns, events))
100	    case S.Get{k}: effect(~K, ~same, V, zero_key, zero_value, ValueOnly{}, E.read(~K, ~same, V, s, k, True{}, events))
101	    case S.GetAndRefresh{k, ns}: effect(~K, ~same, V, zero_key, zero_value, ValueOnly{}, E.refresh(~K, ~same, V, s, k, ns, events))
102	    case S.Peek{k}: effect(~K, ~same, V, zero_key, zero_value, ValueOnly{}, E.read(~K, ~same, V, s, k, False{}, events))
103	    case S.Contains{k}: effect(~K, ~same, V, zero_key, zero_value, Flag{}, E.read(~K, ~same, V, s, k, False{}, events))
104	    case S.Remove{k}: observation(~K, ~same, V, zero_key, zero_value, Flag{}, S.remove(~K, ~same, V, s, k), events, 0n)
105	    case S.RemoveOldest{}: observation(~K, ~same, V, zero_key, zero_value, RemovedOldest{}, O.remove_oldest(~K, ~same, V, s), events, 0n)
106	    case S.GetOldest{}: oldest(~K, ~same, V, s, zero_key, zero_value, events)
107	    case S.Keys{}: effect(~K, ~same, V, zero_key, zero_value, Keys{}, A.purge_expired(~K, ~same, V, s, events))
108	    case S.Values{}: effect(~K, ~same, V, zero_key, zero_value, Values{}, A.purge_expired(~K, ~same, V, s, events))
109	    case S.PurgeExpired{}: effect(~K, ~same, V, zero_key, zero_value, Nothing{}, A.purge_expired(~K, ~same, V, s, events))
110	    case S.Purge{}: Returned{S.purged(K, V, s), NoReply{}, events, 0n}
111	    case S.Len{}: Returned{s, Length{S.length(K, V, s)}, events, 0n}
112	    case S.SetLifetime{ns}: Returned{S.set_lifetime(K, V, s, ns), NoReply{}, events, 0n}
113	    case S.Metrics{}: metrics(K, V, s, events)
114	    case S.ResetMetrics{}: reset(K, V, s, events)
115	    case S.Diagnostics{}: diagnostics(~K, ~same, V, s, events)