src/containers/dynamic_array.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/src/containers/dynamic_array.bend as Dynamic_array

3 imports

import Base
import ../math/pow2.bend as P2
import ./types/dynamic_array.bend as E

Types

type DynArray source · line 29 · raw

@-a:Quant -> @-T:Kind(a) -> Type

DA

@-a:Quant -> @-T:Kind(a) -> @limit:Nat -> @depth:Nat -> @cap:Nat -> @length:Nat -> @slots:Array<Maybe<a, T>> -> DynArray<a, T>

Definitions

def max_depth source · line 32 · raw

Nat

def pow2 source · line 36 · raw

@d:Nat -> Nat

2^d (structural doubling; Base Nat.pow is avoided, see docs/VALIDATION.md).

def empty_slots source · line 43 · raw

@-T:Data -> @+depth:Nat -> Array<Maybe<&2, T>>

def new source · line 46 · raw

@-T:Data -> DynArray<&2, T>

def clamp_limit source · line 51 · raw

@k:Nat -> @small:Bool -> Nat

Depth limit min(k, 31). (Written with an explicit match: Base Nat.min is a Bool.pick over shared arguments, which miscompiled at runtime; docs/VALIDATION.md.)

def with_limit source · line 59 · raw

@-T:Data -> @+k:Nat -> DynArray<&2, T>

Same as new, with capacity bounded by 2^min(k, 31).

def length source · line 62 · raw

@-T:Data -> @da:DynArray<&2, T> -> Pair(DynArray<&2, T>, Nat)

def capacity source · line 66 · raw

@-T:Data -> @da:DynArray<&2, T> -> Pair(DynArray<&2, T>, Nat)

def slot_result source · line 70 · raw

@-T:Data -> @slot:Maybe<&2, T> -> Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>

def get_found source · line 79 · raw

@-T:Data -> @limit:Nat -> @depth:Nat -> @+cap:Nat -> @len:Nat -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

def get_checked source · line 83 · raw

@-T:Data -> @limit:Nat -> @depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> @i:Nat -> @ok:Bool -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

def get source · line 90 · raw

@-T:Data -> @da:DynArray<&2, T> -> @+i:Nat -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

def set_checked source · line 96 · raw

@-T:Data -> @limit:Nat -> @depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> @i:Nat -> @v:T -> @ok:Bool -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

def set source · line 103 · raw

@-T:Data -> @da:DynArray<&2, T> -> @+i:Nat -> @v:T -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

def grown source · line 110 · raw

@-T:Data -> @+depth:Nat -> @arr:Array<Maybe<&2, T>> -> Array<Maybe<&2, T>>

Doubling: the old tree becomes the left half of a tree one level deeper.

def push_room source · line 113 · raw

@-T:Data -> @limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+len:Nat -> @arr:Array<Maybe<&2, T>> -> @v:T -> @room:Bool -> @grow:Bool -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

def push source · line 122 · raw

@-T:Data -> @da:DynArray<&2, T> -> @v:T -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

def pop_found source · line 128 · raw

@-T:Data -> @limit:Nat -> @depth:Nat -> @+cap:Nat -> @m:Nat -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

def pop_len source · line 132 · raw

@-T:Data -> @limit:Nat -> @depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

def pop source · line 139 · raw

@-T:Data -> @da:DynArray<&2, T> -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

def grow_if source · line 145 · raw

@-T:Data -> @limit:Nat -> @+depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> @fits:Bool -> DynArray<&2, T>

def grow_step source · line 152 · raw

@-T:Data -> @+n:Nat -> @st:DynArray<&2, T> -> DynArray<&2, T>

def grow_until source · line 157 · raw

@-T:Data -> @fuel:Nat -> @+n:Nat -> @st:DynArray<&2, T> -> DynArray<&2, T>

Doubles until n fits; fuel = limit - depth bounds the number of doublings.

def reserve_room source · line 167 · raw

@-T:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> @+n:Nat -> @feasible:Bool -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

The 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 source · line 174 · raw

@-T:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> @+n:Nat -> @fits:Bool -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

def reserve source · line 182 · raw

@-T:Data -> @da:DynArray<&2, T> -> @+n:Nat -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

Ensures capacity >= n (new capacity: least 2^k >= n with k >= depth).

def clear source · line 189 · raw

@-T:Data -> @da:DynArray<&2, T> -> DynArray<&2, T>

Keeps the capacity; all slots become None.

def cons_some source · line 197 · raw

@-T:Data -> @x:Maybe<&2, T> -> @acc:List<&2, T> -> List<&2, T>

to_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 source · line 204 · raw

@n:Nat -> Nat

def tl_go source · line 213 · raw

@k:Nat -> @-T:Data -> @acc:List<&2, T> -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Pair(Array<Maybe<&2, T>>, List<&2, T>)

k slots are still to be read, the last of them first: the pair r is slot k - 1, already read.

def tl_done source · line 220 · raw

@-T:Data -> @limit:Nat -> @depth:Nat -> @+cap:Nat -> @+len:Nat -> @r:Pair(Array<Maybe<&2, T>>, List<&2, T>) -> Pair(DynArray<&2, T>, List<&2, T>)

def tl_start source · line 224 · raw

@-T:Data -> @limit:Nat -> @depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> Pair(DynArray<&2, T>, List<&2, T>)

def to_list source · line 231 · raw

@-T:Data -> @da:DynArray<&2, T> -> Pair(DynArray<&2, T>, List<&2, T>)

def obs_nat source · line 237 · raw

@-T:Data -> @r:Pair(DynArray<&2, T>, Nat) -> Pair(DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)

def obs_item source · line 241 · raw

@-T:Data -> @r:Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>) -> Pair(DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)

def obs_unit source · line 245 · raw

@-T:Data -> @r:Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>) -> Pair(DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)

def obs_list source · line 249 · raw

@-T:Data -> @r:Pair(DynArray<&2, T>, List<&2, T>) -> Pair(DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)

def step source · line 253 · raw

@-T:Data -> @da:DynArray<&2, T> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> Pair(DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)

def record source · line 274 · raw

@-T:Data -> @acc:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>> -> @r:Pair(DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>) -> Pair(DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)

def step_acc source · line 278 · raw

@-T:Data -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> @st:Pair(DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>) -> Pair(DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)

def run_acc source · line 283 · raw

@-T:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> @st:Pair(DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>) -> Pair(DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)

Runs ops left to right; observations are accumulated newest-first.

def finish source · line 290 · raw

@-T:Data -> @st:Pair(DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>) -> Pair(DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)

def run source · line 295 · raw

@-T:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> @da:DynArray<&2, T> -> Pair(DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)

Final state and the observation of every operation, in order.

Templates

template empty_slots_at source · line 317 · raw

@-T:Data -> @+depth:Nat -> Array<Maybe<&2, T>>

template new_at source · line 320 · raw

@-T:Data -> DynArray<&2, T>

template with_limit_at source · line 323 · raw

@-T:Data -> @+k:Nat -> DynArray<&2, T>

template get_found_at source · line 328 · raw

@-T:Data -> @limit:Nat -> @depth:Nat -> @cap:Nat -> @len:Nat -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

Keep the element type specialized through the returned payload. Calling the erased generic get_found here boxes composite Data on every indexed read.

template get_checked_at source · line 335 · raw

@-T:Data -> @limit:Nat -> @depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> @i:Nat -> @ok:Bool -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

template get_at source · line 342 · raw

@-T:Data -> @da:DynArray<&2, T> -> @+i:Nat -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

template set_checked_at source · line 346 · raw

@-T:Data -> @limit:Nat -> @depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> @i:Nat -> @v:T -> @ok:Bool -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

template set_at source · line 353 · raw

@-T:Data -> @da:DynArray<&2, T> -> @+i:Nat -> @v:T -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

template grown_at source · line 357 · raw

@-T:Data -> @+depth:Nat -> @arr:Array<Maybe<&2, T>> -> Array<Maybe<&2, T>>

template push_room_at source · line 360 · raw

@-T:Data -> @limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+len:Nat -> @arr:Array<Maybe<&2, T>> -> @v:T -> @room:Bool -> @grow:Bool -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

template push_at source · line 369 · raw

@-T:Data -> @da:DynArray<&2, T> -> @v:T -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

template pop_len_at source · line 373 · raw

@-T:Data -> @limit:Nat -> @depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

template pop_at source · line 380 · raw

@-T:Data -> @da:DynArray<&2, T> -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

template grow_if_at source · line 384 · raw

@-T:Data -> @limit:Nat -> @+depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> @fits:Bool -> DynArray<&2, T>

template grow_step_at source · line 391 · raw

@-T:Data -> @+n:Nat -> @st:DynArray<&2, T> -> DynArray<&2, T>

template grow_until_at source · line 395 · raw

@-T:Data -> @fuel:Nat -> @+n:Nat -> @st:DynArray<&2, T> -> DynArray<&2, T>

template reserve_room_at source · line 405 · raw

@-T:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> @+n:Nat -> @feasible:Bool -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

The 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).

template reserve_checked_at source · line 412 · raw

@-T:Data -> @+limit:Nat -> @+depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> @+n:Nat -> @fits:Bool -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

template reserve_at source · line 419 · raw

@-T:Data -> @da:DynArray<&2, T> -> @+n:Nat -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

template clear_go_at source · line 429 · raw

@-T:Data -> @k:Nat -> @arr:Array<Maybe<&2, T>> -> Array<Maybe<&2, T>>

The executable clear resets the occupied slots [0, length) to None, top down, and keeps the block: O(length), no allocation. Dropping the old block and allocating a fresh one (what the parametric clear describes) walks every one of the 2^depth slots twice in the runtime. Every slot at or past the length already holds None, so the result is the same all-None block; proofs/containers/dynamic_array/clear.bend proves it on every good state.

template clear_at source · line 436 · raw

@-T:Data -> @da:DynArray<&2, T> -> DynArray<&2, T>

template tl_go_at source · line 442 · raw

@-T:Data -> @k:Nat -> @acc:List<&2, T> -> @r:Pair(Array<Maybe<&2, T>>, Maybe<&2, T>) -> Pair(Array<Maybe<&2, T>>, List<&2, T>)

The executable to_list is the same indexed walk, compiled at a closed element type; proofs/dynamic_array/closed.bend proves the two agree.

template tl_start_at source · line 449 · raw

@-T:Data -> @limit:Nat -> @depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> Pair(DynArray<&2, T>, List<&2, T>)

template to_list_at source · line 456 · raw

@-T:Data -> @da:DynArray<&2, T> -> Pair(DynArray<&2, T>, List<&2, T>)

template step_at source · line 460 · raw

@-T:Data -> @da:DynArray<&2, T> -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> Pair(DynArray<&2, T>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>)

template step_acc_at source · line 481 · raw

@-T:Data -> @op:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T> -> @st:Pair(DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>) -> Pair(DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)

template run_acc_at source · line 485 · raw

@-T:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> @st:Pair(DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>) -> Pair(DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)

template run_at source · line 492 · raw

@-T:Data -> @ops:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Op<T>> -> @da:DynArray<&2, T> -> Pair(DynArray<&2, T>, List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Obs<T>>)

template empty_owned source · line 503 · raw

@-T:Type -> @depth:Nat -> Array<Maybe<&1, T>>

Stock Array.new requires Data. This fresh-empty initializer is O(c log c) in the native backend because ANode merges blocks; see ownership docs.

template new_owned source · line 510 · raw

@-T:Type -> DynArray<&1, T>

template with_limit_owned source · line 513 · raw

@-T:Type -> @+k:Nat -> DynArray<&1, T>

template length_owned source · line 516 · raw

@-T:Type -> @da:DynArray<&1, T> -> Pair(DynArray<&1, T>, Nat)

template capacity_owned source · line 520 · raw

@-T:Type -> @da:DynArray<&1, T> -> Pair(DynArray<&1, T>, Nat)

template grown_owned source · line 524 · raw

@-T:Type -> @+depth:Nat -> @arr:Array<Maybe<&1, T>> -> Array<Maybe<&1, T>>

template push_room_owned source · line 527 · raw

@-T:Type -> @limit:Nat -> @+depth:Nat -> @+cap:Nat -> @+len:Nat -> @arr:Array<Maybe<&1, T>> -> @v:T -> @room:Bool -> @grow:Bool -> Pair(DynArray<&1, T>, Result<&1, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<T>, Unit>)

template push_owned source · line 536 · raw

@-T:Type -> @da:DynArray<&1, T> -> @v:T -> Pair(DynArray<&1, T>, Result<&1, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<T>, Unit>)

template owned_result source · line 540 · raw

@-T:Type -> @slot:Maybe<&1, T> -> Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>

template pop_found_owned source · line 547 · raw

@-T:Type -> @limit:Nat -> @depth:Nat -> @cap:Nat -> @n:Nat -> @r:Pair(Array<Maybe<&1, T>>, Maybe<&1, T>) -> Pair(DynArray<&1, T>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

template pop_len_owned source · line 551 · raw

@-T:Type -> @limit:Nat -> @depth:Nat -> @cap:Nat -> @len:Nat -> @arr:Array<Maybe<&1, T>> -> Pair(DynArray<&1, T>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

template pop_owned source · line 558 · raw

@-T:Type -> @da:DynArray<&1, T> -> Pair(DynArray<&1, T>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

template swap_found_owned source · line 564 · raw

@-T:Type -> @limit:Nat -> @depth:Nat -> @cap:Nat -> @len:Nat -> @r:Pair(Array<Maybe<&1, T>>, Maybe<&1, T>) -> Pair(DynArray<&1, T>, Result<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<T>, Maybe<&1, T>>)

The result on success is the previous value. Invalid indices return v. None can occur only in an invalid externally constructed DA representation.

template swap_checked_owned source · line 568 · raw

@-T:Type -> @limit:Nat -> @depth:Nat -> @cap:Nat -> @len:Nat -> @arr:Array<Maybe<&1, T>> -> @i:Nat -> @v:T -> @ok:Bool -> Pair(DynArray<&1, T>, Result<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<T>, Maybe<&1, T>>)

template swap_owned source · line 575 · raw

@-T:Type -> @da:DynArray<&1, T> -> @+i:Nat -> @v:T -> Pair(DynArray<&1, T>, Result<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<T>, Maybe<&1, T>>)

template set_done_owned source · line 579 · raw

@-T:Type -> @r:Pair(DynArray<&1, T>, Result<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<T>, Maybe<&1, T>>) -> Pair(DynArray<&1, T>, Result<&1, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<T>, Unit>)

template set_owned source · line 587 · raw

@-T:Type -> @da:DynArray<&1, T> -> @i:Nat -> @value:T -> Pair(DynArray<&1, T>, Result<&1, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<T>, Unit>)

Replace and release the previous element. Use swap_owned to retain it.

template update_put_owned source · line 592 · raw

@-T:Type -> @-R:Type -> @limit:Nat -> @depth:Nat -> @cap:Nat -> @len:Nat -> @arr:Array<Maybe<&1, T>> -> @i:Nat -> @r:Pair(T, R) -> Pair(DynArray<&1, T>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, R>)

Scoped ownership: f receives the element and must return a replacement. No placeholder escapes the call. f is not called for an invalid index.

template update_found_owned source · line 596 · raw

@-T:Type -> @-R:Type -> @limit:Nat -> @depth:Nat -> @cap:Nat -> @len:Nat -> @i:Nat -> @f:(@_:T -> Pair(T, R)) -> @r:Pair(Array<Maybe<&1, T>>, Maybe<&1, T>) -> Pair(DynArray<&1, T>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, R>)

template update_checked_owned source · line 603 · raw

@-T:Type -> @-R:Type -> @limit:Nat -> @depth:Nat -> @cap:Nat -> @len:Nat -> @arr:Array<Maybe<&1, T>> -> @+i:Nat -> @f:(@_:T -> Pair(T, R)) -> @ok:Bool -> Pair(DynArray<&1, T>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, R>)

template update_owned source · line 610 · raw

@-T:Type -> @-R:Type -> @da:DynArray<&1, T> -> @+i:Nat -> @f:(@_:T -> Pair(T, R)) -> Pair(DynArray<&1, T>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, R>)

template grow_if_owned source · line 614 · raw

@-T:Type -> @limit:Nat -> @+depth:Nat -> @+cap:Nat -> @len:Nat -> @arr:Array<Maybe<&1, T>> -> @fits:Bool -> DynArray<&1, T>

template grow_step_owned source · line 621 · raw

@-T:Type -> @+n:Nat -> @st:DynArray<&1, T> -> DynArray<&1, T>

template grow_until_owned source · line 625 · raw

@-T:Type -> @fuel:Nat -> @+n:Nat -> @st:DynArray<&1, T> -> DynArray<&1, T>

template reserve_room_owned source · line 632 · raw

@-T:Type -> @+limit:Nat -> @+depth:Nat -> @cap:Nat -> @len:Nat -> @arr:Array<Maybe<&1, T>> -> @+n:Nat -> @feasible:Bool -> Pair(DynArray<&1, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

template reserve_checked_owned source · line 639 · raw

@-T:Type -> @+limit:Nat -> @depth:Nat -> @cap:Nat -> @len:Nat -> @arr:Array<Maybe<&1, T>> -> @+n:Nat -> @fits:Bool -> Pair(DynArray<&1, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

template reserve_owned source · line 646 · raw

@-T:Type -> @da:DynArray<&1, T> -> @+n:Nat -> Pair(DynArray<&1, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Unit>)

template clear_owned source · line 650 · raw

@-T:Type -> @da:DynArray<&1, T> -> DynArray<&1, T>

template cons_owned source · line 654 · raw

@-T:Type -> @x:Maybe<&1, T> -> @acc:List<&1, T> -> List<&1, T>

template drain_go_owned source · line 661 · raw

@-T:Type -> @k:Nat -> @acc:List<&1, T> -> @r:Pair(Array<Maybe<&1, T>>, Maybe<&1, T>) -> List<&1, T>

template drain_len_owned source · line 668 · raw

@-T:Type -> @len:Nat -> @arr:Array<Maybe<&1, T>> -> List<&1, T>

template into_list_owned source · line 676 · raw

@-T:Type -> @da:DynArray<&1, T> -> List<&1, T>

Consumes the container; values move into the returned list, in order.

template swap_checked_at source · line 683 · raw

@-T:Data -> @limit:Nat -> @depth:Nat -> @cap:Nat -> @len:Nat -> @arr:Array<Maybe<&2, T>> -> @i:Nat -> @v:T -> @ok:Bool -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)

Copyable-element exchange, used by indexed collection storage. The previous value is returned and all other slots remain unchanged. Like set_at, an invalid index leaves the array unchanged and reports IndexOutOfRange.

template swap_at source · line 690 · raw

@-T:Data -> @da:DynArray<&2, T> -> @+i:Nat -> @v:T -> Pair(DynArray<&2, T>, Result<&2, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)