src/SortedRun.bend

mylsm-lsm-store@0.6.0.1 · 419 lines · 45 definitions

1import Base
2import mylsm-lsm-store@0.6.0.1/src/Keys.bend as Keys
3import mylsm-lsm-store@0.6.0.1/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)