src/SortedRun.bend checks

raw source on the hub · import mylsm-lsm-store@0.5.0.0/src/SortedRun.bend as SortedRun

3 imports

import Base
import ./Keys.bend as Keys
import ./MemTable.bend as MemTable

Types

type RunGroup source · line 275 · raw

Data

Represent RunGroup data used by the sorted-run operations.

RunGroup

@newest_rank:Nat -> @oldest_rank:Nat -> @entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> RunGroup

type PartitionState source · line 381 · raw

Data

Represent PartitionState data used by the sorted-run operations.

PartitionState

@room:Nat -> @entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @current_rev:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @chunks_rev:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> PartitionState

Definitions

def bool_not source · line 9 · raw

@rhs:Bool -> Bool

Evaluate not for the sorted-run operations.

def bool_and source · line 17 · raw

@lhs:Bool -> @rhs:Bool -> Bool

Evaluate and for the sorted-run operations.

def bool_or source · line 25 · raw

@lhs:Bool -> @rhs:Bool -> Bool

Evaluate or for the sorted-run operations.

def entry_cmp source · line 33 · raw

@e1:0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry -> @e2:0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry -> Cmp

Handle the entry cmp for the sorted-run operations.

def entry_key_eq source · line 41 · raw

@entry:0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry -> @+key:String -> Bool

Handle the entry key eq for the sorted-run operations.

def contains_key source · line 49 · raw

@+entry:0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry -> @entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> Bool

Check membership for whether key holds for the sorted-run operations.

def is_unique source · line 59 · raw

@entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> Bool

Check whether unique holds for the sorted-run operations.

def is_strict source · line 67 · raw

@entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> Bool

Check whether strict holds for the sorted-run operations.

def resolve_step source · line 77 · raw

@done:Bool -> @hit:Bool -> @val:Maybe<&2, String> -> @ans:Maybe<&2, Maybe<&2, String>> -> Pair(Bool, Maybe<&2, Maybe<&2, String>>)

Resolve step for the sorted-run operations.

def resolve_state source · line 94 · raw

@entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @+key:String -> @state:Pair(Bool, Maybe<&2, Maybe<&2, String>>) -> Pair(Bool, Maybe<&2, Maybe<&2, String>>)

Resolve state for the sorted-run operations.

def resolve_answer source · line 107 · raw

@state:Pair(Bool, Maybe<&2, Maybe<&2, String>>) -> Maybe<&2, Maybe<&2, String>>

Resolve answer for the sorted-run operations.

def resolve source · line 113 · raw

@entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @key:String -> Maybe<&2, Maybe<&2, String>>

Handle resolve in the sorted-run operations.

def resolve_newest_go source · line 117 · raw

@runs:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> @+key:String -> @state:Pair(Bool, Maybe<&2, Maybe<&2, String>>) -> Pair(Bool, Maybe<&2, Maybe<&2, String>>)

Resolve newest go for the sorted-run operations.

def resolve_newest source · line 129 · raw

@runs:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> @key:String -> Maybe<&2, Maybe<&2, String>>

Resolve newest for the sorted-run operations.

def runs_well_formed source · line 134 · raw

@runs:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> Bool

Run s well formed for the sorted-run operations.

def first_key source · line 142 · raw

@entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> Maybe<&2, String>

L1 helpers operate on entry runs to avoid a SortedRun <-> Sstable cycle.

def last_key_go source · line 150 · raw

@entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @last:String -> Maybe<&2, String>

Return the last key go in the sorted-run operations.

def last_key source · line 158 · raw

@entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> Maybe<&2, String>

Return the last key in the sorted-run operations.

def range_disjoint_bounds source · line 166 · raw

@af:Maybe<&2, String> -> @al:Maybe<&2, String> -> @bf:Maybe<&2, String> -> @bl:Maybe<&2, String> -> Bool

Handle range disjoint bounds in the sorted-run operations.

def range_disjoint source · line 185 · raw

@+xs:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @+ys:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> Bool

Handle range disjoint in the sorted-run operations.

def disjoint_with source · line 189 · raw

@+run:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @runs:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> Bool

Check disjointness of whether with holds for the sorted-run operations.

def pairwise_disjoint source · line 197 · raw

@runs:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> Bool

Handle pairwise disjoint in the sorted-run operations.

def level_disjoint source · line 205 · raw

@+runs:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> Bool

Return the level disjoint for the sorted-run operations.

def levels_well_formed source · line 209 · raw

@levels:List<&2, List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>>> -> Bool

Return the level s well formed for the sorted-run operations.

def lower_levels_well_formed source · line 218 · raw

@levels:List<&2, List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/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 230 · raw

@order:Cmp -> @+newer_head:0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry -> @newer_tail:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @+older_head:0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry -> @older_tail:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @acc:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> Pair(List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>, Pair(List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>))

Merge step for the sorted-run operations.

def merge_go source · line 247 · raw

@fuel:Nat -> @state:Pair(List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>, Pair(List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>)) -> List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>

Merge go for the sorted-run operations.

def merge_newer source · line 268 · raw

@+newer:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @+older:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>

Merge newer for the sorted-run operations.

def rank_runs source · line 283 · raw

@runs:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> @+rank:Nat -> List<&2, RunGroup>

Rank runs for the sorted-run operations.

def merge_groups source · line 291 · raw

@newer:RunGroup -> @older:RunGroup -> RunGroup

Merge groups for the sorted-run operations.

def merge_round source · line 299 · raw

@groups:List<&2, RunGroup> -> List<&2, RunGroup>

Merge round for the sorted-run operations.

def group_entries source · line 310 · raw

@groups:List<&2, RunGroup> -> List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>

Group entries for the sorted-run operations.

def merge_many_go source · line 318 · raw

@fuel:Nat -> @groups:List<&2, RunGroup> -> List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>

Merge many go for the sorted-run operations.

def merge_many_newest source · line 326 · raw

@+runs:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>

Merge many newest for the sorted-run operations.

def singleton_runs source · line 332 · raw

@entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/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 340 · raw

@entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>

Sort newest for the sorted-run operations.

def merge_disjoint_dec source · line 344 · raw

@ok:Bool -> @runs:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> Maybe<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>>

Merge disjoint dec for the sorted-run operations.

def merge_many_disjoint source · line 353 · raw

@+runs:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> Maybe<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/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 361 · 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 369 · raw

@current_rev:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @chunks_rev:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>>

Partition finish for the sorted-run operations.

def partition_step source · line 390 · raw

@full:Bool -> @target:Nat -> @room_after:Nat -> @entry:0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry -> @rest:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @current_rev:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> @chunks_rev:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> PartitionState

Partition step for the sorted-run operations.

def partition_go source · line 407 · raw

@fuel:Nat -> @+target:Nat -> @state:PartitionState -> List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>>

Partition go for the sorted-run operations.

def partition source · line 423 · raw

@+target:Nat -> @+entries:List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry> -> List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>>

Handle partition in the sorted-run operations.

def concat_chunks source · line 428 · raw

@chunks:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>

Concatenate chunks for the sorted-run operations.

def chunks_bounded_go source · line 436 · raw

@+target:Nat -> @chunks:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> Bool

Handle the chunk s bounded go for the sorted-run operations.

def chunks_bounded source · line 446 · raw

@target:Nat -> @chunks:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> Bool

Handle the chunk s bounded for the sorted-run operations.

def chunks_strict_unique source · line 450 · raw

@chunks:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> Bool

Handle the chunk s strict unique for the sorted-run operations.

def chunks_pairwise_disjoint source · line 454 · raw

@chunks:List<&2, List<&2, 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.Entry>> -> Bool

Handle the chunk s pairwise disjoint for the sorted-run operations.