src/SortedRun.bend
mylsm-lsm-store@0.6.0.0 · 419 lines · 0 definitions
1import Base
2import mylsm-lsm-store@0.6.0.0/src/Keys.bend as Keys
3import mylsm-lsm-store@0.6.0.0/src/MemTable.bend as MemTable
4
5# Pure reference semantics and stable sorted-run merging. This module stays
6# independent of Sstable so table construction can depend on it later.
7
8# Evaluate not for the sorted-run operations.
9def bool_not(rhs: Bool) -> Bool:
10 match rhs:
11 case False{}:
12 True{}
13 case True{}:
14 False{}
15
16# Evaluate and for the sorted-run operations.
17def bool_and(lhs: Bool, rhs: Bool) -> Bool:
18 match lhs:
19 case False{}:
20 False{}
21 case True{}:
22 rhs
23
24# Evaluate or for the sorted-run operations.
25def bool_or(lhs: Bool, rhs: Bool) -> Bool:
26 match lhs:
27 case False{}:
28 rhs
29 case True{}:
30 True{}
31
32# Handle the entry cmp for the sorted-run operations.
33def entry_cmp(e1: MemTable.Entry, e2: MemTable.Entry) -> Cmp:
34 match e1:
35 case MemTable.Entry{k1, v1}:
36 match e2:
37 case MemTable.Entry{k2, v2}:
38 Keys.cmp(k1, k2)
39
40# Handle the entry key eq for the sorted-run operations.
41def entry_key_eq(entry: MemTable.Entry, +key: String) -> Bool:
42 match entry:
43 case MemTable.Entry{k, v}:
44 Keys.eq(k, key)
45
46# --- Reference predicates and observable model ---
47
48# Check membership for whether key holds for the sorted-run operations.
49def contains_key(+entry: MemTable.Entry, entries: List<&2, MemTable.Entry>) -> Bool:
50 match entry:
51 case MemTable.Entry{+key, val}:
52 match entries:
53 case Nil{}:
54 False{}
55 case Con{h, t}:
56 bool_or(entry_key_eq(h, key), contains_key(MemTable.Entry{key, val}, t))
57
58# Check whether unique holds for the sorted-run operations.
59def is_unique(entries: List<&2, MemTable.Entry>) -> Bool:
60 match entries:
61 case Nil{}:
62 True{}
63 case Con{+h, +t}:
64 bool_and(bool_not(contains_key(h, t)), is_unique(t))
65
66# Check whether strict holds for the sorted-run operations.
67def is_strict(entries: List<&2, MemTable.Entry>) -> Bool:
68 match entries:
69 case Nil{}:
70 True{}
71 case Con{h, Nil{}}:
72 True{}
73 case Con{+h, Con{+next, +rest}}:
74 bool_and(Keys.cmp_is_lt(entry_cmp(h, next)), is_strict(Con{next, rest}))
75
76# Resolve step for the sorted-run operations.
77def resolve_step(
78 done: Bool,
79 hit: Bool,
80 val: Maybe<&2, String>,
81 ans: Maybe<&2, Maybe<&2, String>>
82) -> Bool & Maybe<&2, Maybe<&2, String>>:
83 match done:
84 case True{}:
85 (True{}, ans)
86 case False{}:
87 match hit:
88 case True{}:
89 (True{}, Some{val})
90 case False{}:
91 (False{}, ans)
92
93# Resolve state for the sorted-run operations.
94def resolve_state(
95 entries: List<&2, MemTable.Entry>,
96 +key: String,
97 state: Bool & Maybe<&2, Maybe<&2, String>>
98) -> Bool & Maybe<&2, Maybe<&2, String>>:
99 match entries:
100 case Nil{}:
101 state
102 case Con{MemTable.Entry{k, val}, t}:
103 (done, ans) = state
104 resolve_state(t, key, resolve_step(done, Keys.eq(k, key), val, ans))
105
106# Resolve answer for the sorted-run operations.
107def resolve_answer(state: Bool & Maybe<&2, Maybe<&2, String>>) -> Maybe<&2, Maybe<&2, String>>:
108 match state:
109 case (done, ans):
110 ans
111
112# Handle resolve in the sorted-run operations.
113def resolve(entries: List<&2, MemTable.Entry>, key: String) -> Maybe<&2, Maybe<&2, String>>:
114 resolve_answer(resolve_state(entries, key, (False{}, None{})))
115
116# Resolve newest go for the sorted-run operations.
117def resolve_newest_go(
118 runs: List<&2, List<&2, MemTable.Entry>>,
119 +key: String,
120 state: Bool & Maybe<&2, Maybe<&2, String>>
121) -> Bool & Maybe<&2, Maybe<&2, String>>:
122 match runs:
123 case Nil{}:
124 state
125 case Con{run, rest}:
126 resolve_newest_go(rest, key, resolve_state(run, key, state))
127
128# Resolve newest for the sorted-run operations.
129def resolve_newest(runs: List<&2, List<&2, MemTable.Entry>>, key: String) -> Maybe<&2, Maybe<&2, String>>:
130 resolve_answer(resolve_newest_go(runs, key, (False{}, None{})))
131
132
133# Run s well formed for the sorted-run operations.
134def runs_well_formed(runs: List<&2, List<&2, MemTable.Entry>>) -> Bool:
135 match runs:
136 case Nil{}:
137 True{}
138 case Con{+run, rest}:
139 bool_and(bool_and(is_strict(run), is_unique(run)), runs_well_formed(rest))
140
141# L1 helpers operate on entry runs to avoid a SortedRun <-> Sstable cycle.
142def first_key(entries: List<&2, MemTable.Entry>) -> Maybe<&2, String>:
143 match entries:
144 case Nil{}:
145 None{}
146 case Con{MemTable.Entry{key, val}, t}:
147 Some{key}
148
149# Return the last key go in the sorted-run operations.
150def last_key_go(entries: List<&2, MemTable.Entry>, last: String) -> Maybe<&2, String>:
151 match entries:
152 case Nil{}:
153 Some{last}
154 case Con{MemTable.Entry{key, val}, t}:
155 last_key_go(t, key)
156
157# Return the last key in the sorted-run operations.
158def last_key(entries: List<&2, MemTable.Entry>) -> Maybe<&2, String>:
159 match entries:
160 case Nil{}:
161 None{}
162 case Con{MemTable.Entry{key, val}, t}:
163 last_key_go(t, key)
164
165# Handle range disjoint bounds in the sorted-run operations.
166def range_disjoint_bounds(
167 af: Maybe<&2, String>,
168 al: Maybe<&2, String>,
169 bf: Maybe<&2, String>,
170 bl: Maybe<&2, String>
171) -> Bool:
172 match af al bf bl:
173 case None{} _ _ _:
174 True{}
175 case _ None{} _ _:
176 True{}
177 case _ _ None{} _:
178 True{}
179 case _ _ _ None{}:
180 True{}
181 case Some{a_first} Some{a_last} Some{b_first} Some{b_last}:
182 bool_or(Keys.lt(a_last, b_first), Keys.lt(b_last, a_first))
183
184# Handle range disjoint in the sorted-run operations.
185def range_disjoint(+xs: List<&2, MemTable.Entry>, +ys: List<&2, MemTable.Entry>) -> Bool:
186 range_disjoint_bounds(first_key(xs), last_key(xs), first_key(ys), last_key(ys))
187
188# Check disjointness of whether with holds for the sorted-run operations.
189def disjoint_with(+run: List<&2, MemTable.Entry>, runs: List<&2, List<&2, MemTable.Entry>>) -> Bool:
190 match runs:
191 case Nil{}:
192 True{}
193 case Con{+h, t}:
194 bool_and(range_disjoint(run, h), disjoint_with(run, t))
195
196# Handle pairwise disjoint in the sorted-run operations.
197def pairwise_disjoint(runs: List<&2, List<&2, MemTable.Entry>>) -> Bool:
198 match runs:
199 case Nil{}:
200 True{}
201 case Con{+h, +t}:
202 bool_and(disjoint_with(h, t), pairwise_disjoint(t))
203
204# --- Fuel-bounded stable two-run linear merge ---
205
206# Merge step for the sorted-run operations.
207def merge_step(
208 order: Cmp,
209 +newer_head: MemTable.Entry,
210 newer_tail: List<&2, MemTable.Entry>,
211 +older_head: MemTable.Entry,
212 older_tail: List<&2, MemTable.Entry>,
213 acc: List<&2, MemTable.Entry>
214) -> List<&2, MemTable.Entry> & List<&2, MemTable.Entry> & List<&2, MemTable.Entry>:
215 match order:
216 case LT{}:
217 (Con{newer_head, acc}, newer_tail, Con{older_head, older_tail})
218 case EQ{}:
219 (Con{newer_head, acc}, newer_tail, older_tail)
220 case GT{}:
221 (Con{older_head, acc}, Con{newer_head, newer_tail}, older_tail)
222
223# Merge go for the sorted-run operations.
224def merge_go(
225 fuel: Nat,
226 state: List<&2, MemTable.Entry> & List<&2, MemTable.Entry> & List<&2, MemTable.Entry>
227) -> List<&2, MemTable.Entry>:
228 match fuel:
229 case 0n:
230 (acc, newer, older) = state
231 List.reverse.go(&2, MemTable.Entry, acc, List.append(&2, MemTable.Entry, newer, older))
232 case 1n+f:
233 (acc, newer, older) = state
234 match newer older:
235 case Nil{} Nil{}:
236 List.reverse(&2, MemTable.Entry, acc)
237 case Nil{} rest:
238 List.reverse.go(&2, MemTable.Entry, acc, rest)
239 case rest Nil{}:
240 List.reverse.go(&2, MemTable.Entry, acc, rest)
241 case Con{+nh, nt} Con{+oh, ot}:
242 merge_go(f, merge_step(entry_cmp(nh, oh), nh, nt, oh, ot, acc))
243
244# Merge newer for the sorted-run operations.
245def merge_newer(+newer: List<&2, MemTable.Entry>, +older: List<&2, MemTable.Entry>) -> List<&2, MemTable.Entry>:
246 fuel = Nat.add(Nat.add(List.length(&2, MemTable.Entry, newer), List.length(&2, MemTable.Entry, older)), 1n)
247 merge_go(fuel, (Nil{}, newer, older))
248
249# --- Precedence-preserving balanced multi-run merge ---
250
251# Represent RunGroup data used by the sorted-run operations.
252type RunGroup is Data:
253 RunGroup{
254 newest_rank: Nat,
255 oldest_rank: Nat,
256 entries: List<&2, MemTable.Entry>
257 }
258
259# Rank runs for the sorted-run operations.
260def rank_runs(runs: List<&2, List<&2, MemTable.Entry>>, +rank: Nat) -> List<&2, RunGroup>:
261 match runs:
262 case Nil{}:
263 Nil{}
264 case Con{entries, rest}:
265 Con{RunGroup{rank, rank, entries}, rank_runs(rest, 1n+rank)}
266
267# Merge groups for the sorted-run operations.
268def merge_groups(newer: RunGroup, older: RunGroup) -> RunGroup:
269 match newer:
270 case RunGroup{newest_rank, oldest_rank, newer_entries}:
271 match older:
272 case RunGroup{older_newest, older_oldest, older_entries}:
273 RunGroup{newest_rank, older_oldest, merge_newer(newer_entries, older_entries)}
274
275# Merge round for the sorted-run operations.
276def merge_round(groups: List<&2, RunGroup>) -> List<&2, RunGroup>:
277 match groups:
278 case Nil{}:
279 Nil{}
280 case Con{group, Nil{}}:
281 Con{group, Nil{}}
282 case Con{newer, Con{older, rest}}:
283 merged tail = merge_groups(newer, older) merge_round(rest)
284 Con{merged, tail}
285
286# Group entries for the sorted-run operations.
287def group_entries(groups: List<&2, RunGroup>) -> List<&2, MemTable.Entry>:
288 match groups:
289 case Nil{}:
290 Nil{}
291 case Con{RunGroup{newest_rank, oldest_rank, entries}, rest}:
292 entries
293
294# Merge many go for the sorted-run operations.
295def merge_many_go(fuel: Nat, groups: List<&2, RunGroup>) -> List<&2, MemTable.Entry>:
296 match fuel:
297 case 0n:
298 group_entries(groups)
299 case 1n+f:
300 merge_many_go(f, merge_round(groups))
301
302# Merge many newest for the sorted-run operations.
303def merge_many_newest(+runs: List<&2, List<&2, MemTable.Entry>>) -> List<&2, MemTable.Entry>:
304 fuel = Nat.add(List.length(&2, List<&2, MemTable.Entry>, runs), 1n)
305 merge_many_go(fuel, rank_runs(runs, 0n))
306
307# Canonicalize raw newest-first entries in O(N log N): each entry starts as one
308# already-sorted run, and stable EQ selection preserves the earlier/newer entry.
309def singleton_runs(entries: List<&2, MemTable.Entry>) -> List<&2, List<&2, MemTable.Entry>>:
310 match entries:
311 case Nil{}:
312 Nil{}
313 case Con{entry, rest}:
314 Con{Con{entry, Nil{}}, singleton_runs(rest)}
315
316# Sort newest for the sorted-run operations.
317def sort_newest(entries: List<&2, MemTable.Entry>) -> List<&2, MemTable.Entry>:
318 merge_many_newest(singleton_runs(entries))
319
320# --- Pure bounded output partitioning ---
321
322# A zero target cannot bound a non-empty partition, so the public partitioning
323# API and its bound predicate consistently interpret it as the smallest safe
324# target: one entry per chunk.
325def partition_target(target: Nat) -> Nat:
326 match target:
327 case 0n:
328 1n
329 case 1n+n:
330 1n+n
331
332# Partition finish for the sorted-run operations.
333def partition_finish(
334 current_rev: List<&2, MemTable.Entry>,
335 chunks_rev: List<&2, List<&2, MemTable.Entry>>
336) -> List<&2, List<&2, MemTable.Entry>>:
337 match current_rev:
338 case Nil{}:
339 List.reverse(&2, List<&2, MemTable.Entry>, chunks_rev)
340 case Con{entry, rest}:
341 chunk = List.reverse(&2, MemTable.Entry, Con{entry, rest})
342 List.reverse(&2, List<&2, MemTable.Entry>, Con{chunk, chunks_rev})
343
344# Represent PartitionState data used by the sorted-run operations.
345type PartitionState is Data:
346 PartitionState{
347 room: Nat,
348 entries: List<&2, MemTable.Entry>,
349 current_rev: List<&2, MemTable.Entry>,
350 chunks_rev: List<&2, List<&2, MemTable.Entry>>
351 }
352
353# Partition step for the sorted-run operations.
354def partition_step(
355 full: Bool,
356 target: Nat,
357 room_after: Nat,
358 entry: MemTable.Entry,
359 rest: List<&2, MemTable.Entry>,
360 current_rev: List<&2, MemTable.Entry>,
361 chunks_rev: List<&2, List<&2, MemTable.Entry>>
362) -> PartitionState:
363 match full:
364 case False{}:
365 PartitionState{room_after, rest, Con{entry, current_rev}, chunks_rev}
366 case True{}:
367 chunk = List.reverse(&2, MemTable.Entry, Con{entry, current_rev})
368 PartitionState{target, rest, Nil{}, Con{chunk, chunks_rev}}
369
370# Partition go for the sorted-run operations.
371def partition_go(
372 fuel: Nat,
373 +target: Nat,
374 state: PartitionState
375) -> List<&2, List<&2, MemTable.Entry>>:
376 match fuel state:
377 case 0n PartitionState{room, entries, current_rev, chunks_rev}:
378 partition_finish(current_rev, chunks_rev)
379 case 1n+f PartitionState{0n, entries, current_rev, chunks_rev}:
380 partition_finish(current_rev, chunks_rev)
381 case 1n+f PartitionState{1n+r, Nil{}, current_rev, chunks_rev}:
382 partition_finish(current_rev, chunks_rev)
383 case 1n+f PartitionState{1n++r, Con{entry, rest}, current_rev, chunks_rev}:
384 partition_go(f, target, partition_step(Nat.is_eq(r, 0n), target, r, entry, rest, current_rev, chunks_rev))
385
386# Handle partition in the sorted-run operations.
387def partition(+target: Nat, +entries: List<&2, MemTable.Entry>) -> List<&2, List<&2, MemTable.Entry>>:
388 +size = partition_target(target)
389 partition_go(List.length(&2, MemTable.Entry, entries), size, PartitionState{size, entries, Nil{}, Nil{}})
390
391# Concatenate chunks for the sorted-run operations.
392def concat_chunks(chunks: List<&2, List<&2, MemTable.Entry>>) -> List<&2, MemTable.Entry>:
393 match chunks:
394 case Nil{}:
395 Nil{}
396 case Con{chunk, rest}:
397 List.append(&2, MemTable.Entry, chunk, concat_chunks(rest))
398
399# Handle the chunk s bounded go for the sorted-run operations.
400def chunks_bounded_go(+target: Nat, chunks: List<&2, List<&2, MemTable.Entry>>) -> Bool:
401 match chunks:
402 case Nil{}:
403 True{}
404 case Con{chunk, rest}:
405 bool_and(
406 Nat.is_le(List.length(&2, MemTable.Entry, chunk), target),
407 chunks_bounded_go(target, rest))
408
409# Handle the chunk s bounded for the sorted-run operations.
410def chunks_bounded(target: Nat, chunks: List<&2, List<&2, MemTable.Entry>>) -> Bool:
411 chunks_bounded_go(partition_target(target), chunks)
412
413# Handle the chunk s strict unique for the sorted-run operations.
414def chunks_strict_unique(chunks: List<&2, List<&2, MemTable.Entry>>) -> Bool:
415 runs_well_formed(chunks)
416
417# Handle the chunk s pairwise disjoint for the sorted-run operations.
418def chunks_pairwise_disjoint(chunks: List<&2, List<&2, MemTable.Entry>>) -> Bool:
419 pairwise_disjoint(chunks)