bend-collections

Search uses release 1.0.0.0 · 4,483 definitions

Releases (1)

1.0.0.0 indexed

Definitions (4,483)

src/containers/doubly_linked_list.bend

def run

src/containers/dynamic_array.bend

type DynArray
def max_depth
def pow22^d (structural doubling; Base Nat.pow is avoided, see docs/VALIDATION.md).
def empty_slots
def new
def clamp_limitDepth limit min(k, 31).
def with_limitSame as new, with capacity bounded by 2^min(k, 31).
def length
def capacity
def slot_result
def get_found
def get_checked
def get
def set_checked
def set
def grownDoubling: the old tree becomes the left half of a tree one level deeper.
def push_room
def push
def pop_found
def pop_len
def pop
def grow_if
def grow_step
def grow_untilDoubles until n fits; `fuel` = limit - depth bounds the number of doublings.
def reserve_roomThe feasibility test (n <= 2^limit) is only reached when the cached capacity does not already suffice: computing 2^limit is O(limit) and reserve is otherwise O(1).
def reserve_checked
def reserveEnsures capacity >= n (new capacity: least 2^k >= n with k >= depth).
def clearKeeps the capacity; all slots become None.
def cons_someto_list walks the occupied slots BY INDEX, newest first, and conses them: the walk gives the array back, so nothing is cloned, and a `Base.Array` is never matched structurally (that destroys the flat representation, see docs/VALIDATION.md).
def dec1
def tl_gok slots are still to be read, the last of them first: the pair `r` is slot k - 1, already read.
def tl_done
def tl_start
def to_list
def obs_nat
def obs_item
def obs_unit
def obs_list
def step
def record
def step_acc
def run_accRuns ops left to right; observations are accumulated newest-first.
def finish
def runFinal state and the observation of every operation, in order.
def empty_slots_at
def new_at
def with_limit_at
def get_found_atKeep the element type specialized through the returned payload.
def get_checked_at
def get_at
def set_checked_at
def set_at
def grown_at
def push_room_at
def push_at
def pop_len_at
def pop_at
def grow_if_at
def grow_step_at
def grow_until_at
def reserve_room_atThe feasibility test (n <= 2^limit) is only reached when the cached capacity does not already suffice: computing 2^limit is O(limit) and reserve is otherwise O(1).
def reserve_checked_at
def reserve_at
def clear_go_atThe executable clear resets the occupied slots [0, length) to None, top down, and keeps the block: O(length), no allocation.
def clear_at
def tl_go_atThe executable to_list is the same indexed walk, compiled at a closed element type; proofs/dynamic_array/closed.bend proves the two agree.
def tl_start_at
def to_list_at
def step_at
def step_acc_at
def run_acc_at
def run_at
def empty_ownedStock Array.new requires Data.
def new_owned
def with_limit_owned
def length_owned
def capacity_owned
def grown_owned
def push_room_owned
def push_owned
def owned_result
def pop_found_owned
def pop_len_owned
def pop_owned
def swap_found_ownedThe result on success is the previous value.
def swap_checked_owned
def swap_owned
def set_done_owned
def set_ownedReplace and release the previous element.
def update_put_ownedScoped ownership: f receives the element and must return a replacement.
def update_found_owned
def update_checked_owned
def update_owned
def grow_if_owned
def grow_step_owned
def grow_until_owned
def reserve_room_owned
def reserve_checked_owned
def reserve_owned