src/scan/ByteBlockBuilder.bend

mylsm-lsm-store@0.6.0.0 · 89 lines · 0 definitions

1import Base
2
3# Selects appending, rollover, or rejection for an exact byte-record size.
4type Decision is Data:
5  Append{used_bytes: Nat}
6  StartNextBlock{record_bytes: Nat}
7  RecordTooLarge{}
8
9def nat.clone.pair(+value: Nat) -> Nat & Nat:
10  (Nat.mul(1n, value), Nat.mul(1n, value))
11
12def decide.rollover(record_bytes: Nat, current_empty: Bool) -> Decision:
13  match current_empty:
14    case True{}: RecordTooLarge{}
15    case False{}: StartNextBlock{record_bytes}
16
17# Chooses whether a record fits the current block without exceeding its cap.
18def decide.current(
19  used_bytes: Nat,
20  record_bytes: Nat,
21  fits_current: Bool
22) -> Decision:
23  match fits_current:
24    case True{}: Append{Nat.add(used_bytes, record_bytes)}
25    case False{}:
26      decide.rollover(record_bytes, Nat.is_eq(used_bytes, 0n))
27
28def decide.sized.limits(
29  +used_bytes: Nat,
30  +record_bytes: Nat,
31  limits: Nat & Nat,
32  record_fits: Bool
33) -> Decision:
34  match limits:
35    case (current_cap, comparison_cap):
36      match record_fits:
37        case False{}: RecordTooLarge{}
38        case True{}:
39          decide.current(used_bytes, record_bytes,
40            Nat.is_le(Nat.add(used_bytes, record_bytes), comparison_cap))
41
42# Rejects a record above the block cap before considering current occupancy.
43def decide.sized(
44  used_bytes: Nat,
45  record_bytes: Nat,
46  max_bytes: Nat,
47  record_fits: Bool
48) -> Decision:
49  decide.sized.limits(used_bytes, record_bytes, nat.clone.pair(max_bytes), record_fits)
50
51def decide.with.max(
52  used_bytes: Nat,
53  +record_bytes: Nat,
54  limits: Nat & Nat
55) -> Decision:
56  match limits:
57    case (record_cap, block_cap):
58      decide.sized(used_bytes, record_bytes, block_cap,
59        Nat.is_le(record_bytes, record_cap))
60
61# Admits, rolls over, or rejects one record using byte-exact limits.
62def decide(used_bytes: Nat, record_bytes: Nat, max_bytes: Nat) -> Decision:
63  decide.with.max(used_bytes, record_bytes, nat.clone.pair(max_bytes))
64
65def decide.target.placed(+used_bytes: Nat, +record_bytes: Nat, append: Bool) -> Decision:
66  match append:
67    case True{}: Append{Nat.add(used_bytes, record_bytes)}
68    case False{}: StartNextBlock{record_bytes}
69
70# Rejects a record above the hard cap, otherwise appends or starts the next block.
71def decide.target.sized(
72  +used_bytes: Nat,
73  +record_bytes: Nat,
74  record_fits: Bool,
75  append: Bool
76) -> Decision:
77  match record_fits:
78    case False{}: RecordTooLarge{}
79    case True{}: decide.target.placed(used_bytes, record_bytes, append)
80
81# Fills blocks up to a target size while admitting any record within the hard cap.
82def decide.target(
83  +used_bytes: Nat,
84  +record_bytes: Nat,
85  target_bytes: Nat,
86  max_bytes: Nat
87) -> Decision:
88  decide.target.sized(used_bytes, record_bytes, Nat.is_le(record_bytes, max_bytes),
89    Nat.is_eq(used_bytes, 0n) || Nat.is_le(Nat.add(used_bytes, record_bytes), target_bytes))