bend-osdev-algo

Releases (1)

• 0.1.0.0 indexed

Definitions (367)

algo.bend

• def bitw.testbit k (False at or past the width)
• def bitw.popcount.step
• def bitw.popcount
• def bitw.ffs.stepk is ffs of the bits above the lowest one
• def bitw.ffs
• def bitw.fls.stepk is fls of the bits above the lowest one
• def bitw.fls
• def bitw.ctz.step
• def bitw.ctz
• def bitw.clz
• def bitw.indexa 1-based position (ffs, fls) as a 0-based index
• def bitw.to_listthe bits of w, least significant first, in front of rest
• def bits32.word
• def bits32.testbit k of x (False for k >= 32)
• def bits32.popcount
• def bits32.ffs
• def bits32.fls
• def bits32.first_set
• def bits32.last_set
• def bits32.ctz
• def bits32.clz
• def bits64.word
• def bits64.testbit k of a (False for k >= 64)
• def bits64.popcount
• def bits64.ffs
• def bits64.fls
• def bits64.first_set
• def bits64.last_set
• def bits64.ctz
• def bits64.clz

bitmap.bend

• def bitseq.atbit i (False past the end)
• def bitseq.nextthe least i with start <= i < size whose bit is want, or size if there is none (bits past the end of bs are clear)
• def bitmap.bitsthe bits of the words, bit 0 of the first word first
• def bitmap.testbit i of the bitmap (False past its end)
• def bitmap.next_setthe first set bit at or after start and below size, or size
• def bitmap.next_clearthe first clear bit at or after start and below size, or size
• def bitmap.first_set
• def bitmap.first_clear

bsearch.bend

• def bsearch.sorted.pairSorted: each element is at most the next
• def bsearch.sorted
• def bsearch.below.step
• def bsearch.lower_boundthe number of leading elements below key: on a sorted list, the index of the first element not below key (the length if there is none)
• def bsearch.find.hit
• def bsearch.find.check
• def bsearch.findan index of a sorted list that holds key (the first), or None
• def bsearch.array.fin
• def bsearch.array.val
• type BsearchStatethe search state: the array, and the range [lo, hi) still in question
• def bsearch.array.pickone halving of [lo, hi): the element at mid decides which half stays
• def bsearch.array.step
• def bsearch.array.advance
• def bsearch.array.result
• def bsearch.array.gofuel bounds the halvings: 33 is enough for any [lo, hi) of U32; once the range is empty the remaining steps change nothing
• def bsearch.array_lower_boundthe index of the first of the first n elements not below key (n if none)
• def bsearch.array.found
• def bsearch.array.find
• def bsearch.array_findan index of the first n elements of a sorted array that holds key, or None

check.bend

• def show_maybe
• def fill
• def show_val
• def show_opt
• def sorted
• def main

proof_bsearch.bend

• def bq.ol
• def bq.mid
• def bq.xthe element the search reads between lo and hi
• def bq.prethe searched prefix, its lower bound, and the range's size and middle as Nats
• def bq.lb
• def bq.s
• def bq.m
• def bq.lo_b
• def bq.hi_b
• def bq.nlo.a
• def bq.nhi.a
• def bq.nlo
• def bq.nhi
• def bq.runf halvings, then lo
• def bq.pick_eq
• def bq.step_eq
• def bq.go
• def bq.bt
• def bq.ft
• def bq.tf
• def bq.nt
• def bq.sz
• def bq.le_zero
• def bq.le_refl
• def bq.le_succ_r
• def bq.lt_le
• def bq.le_trans
• def bq.lt_le_trans
• def bq.le_antisym
• def bq.not_lt
• def bq.lt_one
• def bq.lt_succ_le
• def bq.lt_rw
• def bq.le_rw
• def bq.lt_cancel
• def bq.pw_pos
• def bq.sub_zero