src/SortedRun.bend fails
raw source on the hub · import 0x05fa0e42448e8e221df592b204de523d/src/SortedRun.bend as SortedRun
3 imports
import Base import ./Keys.bend as Keys import ./MemTable.bend as MemTable
Types
type RunGroup source · line 235 · raw
Data
RunGroup@newest_rank:Nat -> @oldest_rank:Nat -> @entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> RunGroup
type PartitionState source · line 331 · raw
Data
PartitionState@room:Nat -> @entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @current_rev:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @chunks_rev:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> PartitionState
Definitions
def bool_not source · line 8 · raw
@b:Bool -> Bool
def bool_and source · line 15 · raw
@a:Bool -> @b:Bool -> Bool
def bool_or source · line 22 · raw
@a:Bool -> @b:Bool -> Bool
def entry_cmp source · line 29 · raw
@e1:0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry -> @e2:0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry -> Cmp
def entry_key_eq source · line 36 · raw
@e:0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry -> @+key:String -> Bool
def contains_key source · line 43 · raw
@+entry:0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry -> @entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> Bool
def is_unique source · line 52 · raw
@entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> Bool
def is_strict source · line 59 · raw
@entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> Bool
def resolve_step source · line 68 · raw
@done:Bool -> @hit:Bool -> @val:Maybe<&2, String> -> @ans:Maybe<&2, Maybe<&2, String>> -> Pair(Bool, Maybe<&2, Maybe<&2, String>>)
def resolve_state source · line 79 · raw
@entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @+key:String -> @state:Pair(Bool, Maybe<&2, Maybe<&2, String>>) -> Pair(Bool, Maybe<&2, Maybe<&2, String>>)
def resolve_answer source · line 87 · raw
@state:Pair(Bool, Maybe<&2, Maybe<&2, String>>) -> Maybe<&2, Maybe<&2, String>>
def resolve source · line 92 · raw
@entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @key:String -> Maybe<&2, Maybe<&2, String>>
def resolve_newest_go source · line 95 · raw
@runs:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> @+key:String -> @state:Pair(Bool, Maybe<&2, Maybe<&2, String>>) -> Pair(Bool, Maybe<&2, Maybe<&2, String>>)
def resolve_newest source · line 102 · raw
@runs:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> @key:String -> Maybe<&2, Maybe<&2, String>>
def runs_well_formed source · line 106 · raw
@runs:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> Bool
def first_key source · line 114 · raw
@entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> Maybe<&2, String>
L1 helpers operate on entry runs to avoid a SortedRun <-> Sstable cycle.
def last_key_go source · line 121 · raw
@entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @last:String -> Maybe<&2, String>
def last_key source · line 128 · raw
@entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> Maybe<&2, String>
def range_disjoint_bounds source · line 135 · raw
@af:Maybe<&2, String> -> @al:Maybe<&2, String> -> @bf:Maybe<&2, String> -> @bl:Maybe<&2, String> -> Bool
def range_disjoint source · line 153 · raw
@+a:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @+b:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> Bool
def disjoint_with source · line 156 · raw
@+run:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @runs:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> Bool
def pairwise_disjoint source · line 163 · raw
@runs:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> Bool
def level_disjoint source · line 170 · raw
@+runs:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> Bool
def levels_well_formed source · line 173 · raw
@levels:List<&2, List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>>> -> Bool
def lower_levels_well_formed source · line 182 · raw
@levels:List<&2, List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>>> -> @target:Nat -> Bool
Expressible prerequisite for lower-shadow reasoning: every supplied level strictly below target is itself well formed and pairwise range-disjoint.
def merge_step source · line 193 · raw
@order:Cmp -> @+newer_head:0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry -> @newer_tail:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @+older_head:0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry -> @older_tail:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @acc:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> Pair(List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>, Pair(List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>))
def merge_go source · line 209 · raw
@fuel:Nat -> @state:Pair(List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>, Pair(List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>)) -> List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>
def merge_newer source · line 229 · raw
@+newer:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @+older:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>
def rank_runs source · line 242 · raw
@runs:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> @+rank:Nat -> List<&2, RunGroup>
def merge_groups source · line 249 · raw
@newer:RunGroup -> @older:RunGroup -> RunGroup
def merge_round source · line 256 · raw
@groups:List<&2, RunGroup> -> List<&2, RunGroup>
def group_entries source · line 266 · raw
@groups:List<&2, RunGroup> -> List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>
def merge_many_go source · line 273 · raw
@fuel:Nat -> @groups:List<&2, RunGroup> -> List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>
def merge_many_newest source · line 280 · raw
@+runs:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>
def singleton_runs source · line 286 · raw
@entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>>
Canonicalize raw newest-first entries in O(N log N): each entry starts as one already-sorted run, and stable EQ selection preserves the earlier/newer entry.
def sort_newest source · line 293 · raw
@entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>
def merge_disjoint_dec source · line 296 · raw
@ok:Bool -> @runs:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> Maybe<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>>
def merge_many_disjoint source · line 305 · raw
@+runs:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> Maybe<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>>
L1 has no age tie-breaker. Reject malformed overlapping/duplicate ranges; for accepted disjoint runs, balanced merge order is observationally irrelevant.
def partition_target source · line 313 · raw
@target:Nat -> Nat
A zero target cannot bound a non-empty partition, so the public partitioning API and its bound predicate consistently interpret it as the smallest safe target: one entry per chunk.
def partition_finish source · line 320 · raw
@current_rev:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @chunks_rev:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>>
def partition_step source · line 339 · raw
@full:Bool -> @target:Nat -> @room_after:Nat -> @entry:0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry -> @rest:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @current_rev:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> @chunks_rev:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> PartitionState
def partition_go source · line 355 · raw
@fuel:Nat -> @+target:Nat -> @state:PartitionState -> List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>>
def partition source · line 370 · raw
@+target:Nat -> @+entries:List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry> -> List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>>
def concat_chunks source · line 374 · raw
@chunks:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>
def chunks_bounded_go source · line 381 · raw
@+target:Nat -> @chunks:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> Bool
def chunks_bounded source · line 390 · raw
@target:Nat -> @chunks:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> Bool
def chunks_strict_unique source · line 393 · raw
@chunks:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> Bool
def chunks_pairwise_disjoint source · line 396 · raw
@chunks:List<&2, List<&2, 0x05fa0e42448e8e221df592b204de523d/src/MemTable.Entry>> -> Bool