~/bend-docscommunity

src/containers/binary_heap.bend checks

raw source on the hub · import 0xe4067e0d858024083f36a7abe7281e89/src/containers/binary_heap.bend as Binary_heap

2 imports
import Base
import ./types/binary_heap.bend as E

Types

type Heap source · line 42 · raw

@-A:Data -> Type

type Up source · line 88 · raw

@-A:Data -> Type

type Down source · line 142 · raw

@-A:Data -> Type

type Drain source · line 309 · raw

@-A:Data -> Type

Definitions

def max_depth source · line 45 · raw

Nat

def parent source · line 93 · raw

@+i:U32 -> U32

The parent index of i (i > 0). For i = 0 the probe never reads it.

def run_u32 source · line 438 · raw

@ops:List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Op<U32>> -> @h:Heap<U32> -> Pair(Heap<U32>, List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<U32>>)

def run_string source · line 441 · raw

@ops:List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Op<String>> -> @h:Heap<String> -> Pair(Heap<String>, List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<String>>)

Templates

template le source · line 48 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @x:A -> @y:A -> Bool

template empty_slots source · line 51 · raw

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

template new source · line 54 · raw

@-A:Data -> Heap<A>

template length source · line 57 · raw

@-A:Data -> @h:Heap<A> -> Pair(Heap<A>, Nat)

template slot_or source · line 65 · raw

@-A:Data -> @d:A -> @m:Maybe<&2, A> -> A

The slot value, with a default that a well-formed heap never needs (every index a sift loop reads is inside [0, size), where the slot is Some).

template item_of source · line 72 · raw

@-A:Data -> @m:Maybe<&2, A> -> Result<&2, &2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Error, A>

template up_dec source · line 96 · raw

@-A:Data -> @arr:Array<Maybe<&2, A>> -> @i:U32 -> @pv:A -> @p:U32 -> @ok:Bool -> Up<A>

template up_mb source · line 103 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @arr:Array<Maybe<&2, A>> -> @i:U32 -> @+x:A -> @p:U32 -> @m:Maybe<&2, A> -> Up<A>

template up_slot source · line 110 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @i:U32 -> @x:A -> @p:U32 -> @r:Pair(Array<Maybe<&2, A>>, Maybe<&2, A>) -> Up<A>

template up_root source · line 114 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+i:U32 -> @x:A -> @arr:Array<Maybe<&2, A>> -> @root:Bool -> Up<A>

template up_probe source · line 122 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+i:U32 -> @+x:A -> @arr:Array<Maybe<&2, A>> -> Up<A>

Where the value x, currently destined for slot i, must go next.

template up_go source · line 125 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @fuel:Nat -> @+x:A -> @st:Up<A> -> Array<Maybe<&2, A>>

template sift_up source · line 137 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @fuel:Nat -> @i:U32 -> @+x:A -> @arr:Array<Maybe<&2, A>> -> Array<Maybe<&2, A>>

Place x at slot i and restore heap order upwards (fuel bounds the climb).

template down_dec source · line 146 · raw

@-A:Data -> @arr:Array<Maybe<&2, A>> -> @i:U32 -> @cv:A -> @ci:U32 -> @ok:Bool -> Down<A>

template down_two source · line 153 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @arr:Array<Maybe<&2, A>> -> @i:U32 -> @+x:A -> @l:U32 -> @+lv:A -> @r:U32 -> @+rv:A -> @left:Bool -> Down<A>

template down_rmb source · line 160 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @arr:Array<Maybe<&2, A>> -> @i:U32 -> @+x:A -> @l:U32 -> @+lv:A -> @r:U32 -> @m:Maybe<&2, A> -> Down<A>

template down_rslot source · line 167 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @i:U32 -> @x:A -> @l:U32 -> @+lv:A -> @r:U32 -> @rr:Pair(Array<Maybe<&2, A>>, Maybe<&2, A>) -> Down<A>

template down_lmb source · line 171 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @arr:Array<Maybe<&2, A>> -> @i:U32 -> @+x:A -> @+l:U32 -> @two:Bool -> @m:Maybe<&2, A> -> Down<A>

template down_lslot source · line 180 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @i:U32 -> @+x:A -> @+l:U32 -> @two:Bool -> @r:Pair(Array<Maybe<&2, A>>, Maybe<&2, A>) -> Down<A>

template down_has source · line 184 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+size:U32 -> @i:U32 -> @x:A -> @arr:Array<Maybe<&2, A>> -> @+l:U32 -> @has_left:Bool -> Down<A>

template down_probe source · line 193 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+size:U32 -> @+i:U32 -> @x:A -> @arr:Array<Maybe<&2, A>> -> Down<A>

Where the value x, currently destined for slot i of a heap of size elements, must go next.

template down_go source · line 196 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @fuel:Nat -> @+size:U32 -> @+x:A -> @st:Down<A> -> Array<Maybe<&2, A>>

template sift_down source · line 208 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @fuel:Nat -> @+size:U32 -> @i:U32 -> @+x:A -> @arr:Array<Maybe<&2, A>> -> Array<Maybe<&2, A>>

Place x at slot i of a heap of size elements and restore heap order down.

template grown source · line 215 · raw

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

Doubling: the old block becomes the lower half of a block one level deeper, so every element keeps its index.

template push_room source · line 218 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @size:Nat -> @+n:U32 -> @+depth:Nat -> @+cap:U32 -> @arr:Array<Maybe<&2, A>> -> @x:A -> @room:Bool -> Heap<A>

template push source · line 225 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @h:Heap<A> -> @x:A -> Heap<A>

template peek_found source · line 231 · raw

@-A:Data -> @size:Nat -> @n:U32 -> @depth:Nat -> @cap:U32 -> @r:Pair(Array<Maybe<&2, A>>, Maybe<&2, A>) -> Pair(Heap<A>, Result<&2, &2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Error, A>)

template peek_go source · line 235 · raw

@-A:Data -> @size:Nat -> @+n:U32 -> @depth:Nat -> @cap:U32 -> @arr:Array<Maybe<&2, A>> -> @empty:Bool -> Pair(Heap<A>, Result<&2, &2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Error, A>)

template peek source · line 242 · raw

@-A:Data -> @h:Heap<A> -> Pair(Heap<A>, Result<&2, &2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Error, A>)

template pop_move source · line 250 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @size:Nat -> @+m:U32 -> @+depth:Nat -> @cap:U32 -> @root:A -> @last:A -> @arr:Array<Maybe<&2, A>> -> @empty:Bool -> Pair(Heap<A>, Result<&2, &2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Error, A>)

The last element has been taken out of slot m = n - 1; put it at the root and sift it down over the remaining m elements.

template pop_last source · line 257 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @size:Nat -> @+m:U32 -> @depth:Nat -> @cap:U32 -> @+root:A -> @rl:Pair(Array<Maybe<&2, A>>, Maybe<&2, A>) -> Pair(Heap<A>, Result<&2, &2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Error, A>)

template pop_with source · line 267 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @size:Nat -> @+n:U32 -> @depth:Nat -> @cap:U32 -> @arr:Array<Maybe<&2, A>> -> @mr:Maybe<&2, A> -> Pair(Heap<A>, Result<&2, &2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Error, A>)

The last element is READ, not cleared: the invariant says nothing about the slots above the size, so clearing it would be one array write per pop that the algorithm does not need (the C reference does not do it either).

The root slot of a nonempty heap is Some; the None case cannot be reached from a well-formed heap and returns the state unchanged.

template pop_root source · line 274 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @size:Nat -> @+n:U32 -> @depth:Nat -> @cap:U32 -> @rr:Pair(Array<Maybe<&2, A>>, Maybe<&2, A>) -> Pair(Heap<A>, Result<&2, &2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Error, A>)

template pop_go source · line 278 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @size:Nat -> @+n:U32 -> @depth:Nat -> @cap:U32 -> @arr:Array<Maybe<&2, A>> -> @empty:Bool -> Pair(Heap<A>, Result<&2, &2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Error, A>)

template pop source · line 285 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @h:Heap<A> -> Pair(Heap<A>, Result<&2, &2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Error, A>)

template from_list_go source · line 291 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @xs:List<&2, A> -> @h:Heap<A> -> Heap<A>

template from_list source · line 298 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @xs:List<&2, A> -> Heap<A>

template burn source · line 315 · raw

@-A:Data -> @arr:Array<Maybe<&2, A>> -> List<&2, A>

Dropping the (linear) block is O(1): the runtime erases it.

template burn_cons source · line 318 · raw

@-A:Data -> @root:A -> @arr:Array<Maybe<&2, A>> -> List<&2, A>

template drain_mb source · line 321 · raw

@-A:Data -> @arr:Array<Maybe<&2, A>> -> @root:A -> @+m:U32 -> @ml:Maybe<&2, A> -> @empty:Bool -> Drain<A>

template drain_last source · line 330 · raw

@-A:Data -> @root:A -> @+m:U32 -> @empty:Bool -> @rl:Pair(Array<Maybe<&2, A>>, Maybe<&2, A>) -> Drain<A>

template drain_root source · line 334 · raw

@-A:Data -> @arr:Array<Maybe<&2, A>> -> @+m:U32 -> @mr:Maybe<&2, A> -> Drain<A>

template drain_take source · line 341 · raw

@-A:Data -> @+m:U32 -> @r:Pair(Array<Maybe<&2, A>>, Maybe<&2, A>) -> Drain<A>

template drain_take_go source · line 348 · raw

@-A:Data -> @+n:U32 -> @arr:Array<Maybe<&2, A>> -> @empty:Bool -> Drain<A>

Take the root out of a copy holding n elements. Emptiness is decided by the count, not by reading slot 0: the drain must stop at n = 0 whatever the slots above the heap hold (and it saves one array read per element).

template drain_probe source · line 355 · raw

@-A:Data -> @+n:U32 -> @arr:Array<Maybe<&2, A>> -> Drain<A>

template drain_go source · line 358 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @fuel:Nat -> @+depth:Nat -> @st:Drain<A> -> List<&2, A>

template sorted_of source · line 369 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @+size:Nat -> @+n:U32 -> @+depth:Nat -> @cap:U32 -> @c:Pair(Array<Maybe<&2, A>>, Array<Maybe<&2, A>>) -> Pair(Heap<A>, List<&2, A>)

template to_sorted_list source · line 373 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @h:Heap<A> -> Pair(Heap<A>, List<&2, A>)

template obs_nat source · line 379 · raw

@-A:Data -> @r:Pair(Heap<A>, Nat) -> Pair(Heap<A>, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>)

template obs_item source · line 383 · raw

@-A:Data -> @r:Pair(Heap<A>, Result<&2, &2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Error, A>) -> Pair(Heap<A>, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>)

template obs_list source · line 387 · raw

@-A:Data -> @r:Pair(Heap<A>, List<&2, A>) -> Pair(Heap<A>, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>)

template drop_heap source · line 391 · raw

@-A:Data -> @h:Heap<A> -> @v:Pair(Heap<A>, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>) -> Pair(Heap<A>, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>)

template replace source · line 395 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @h:Heap<A> -> @xs:List<&2, A> -> Pair(Heap<A>, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>)

FromList replaces the heap: the old block is dropped (O(1) erasure).

template step source · line 399 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @h:Heap<A> -> @op:0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Op<A> -> Pair(Heap<A>, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>)

template record source · line 414 · raw

@-A:Data -> @acc:List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>> -> @r:Pair(Heap<A>, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>) -> Pair(Heap<A>, List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>>)

template step_acc source · line 418 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @op:0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Op<A> -> @st:Pair(Heap<A>, List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>>) -> Pair(Heap<A>, List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>>)

template run_acc source · line 422 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @ops:List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Op<A>> -> @st:Pair(Heap<A>, List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>>) -> Pair(Heap<A>, List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>>)

template finish source · line 429 · raw

@-A:Data -> @st:Pair(Heap<A>, List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>>) -> Pair(Heap<A>, List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>>)

template run source · line 433 · raw

@-A:Data -> @-cmp:(@_:A -> @_:A -> Cmp) -> @ops:List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Op<A>> -> @h:Heap<A> -> Pair(Heap<A>, List<&2, 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.Obs<A>>)