src/containers/binary_heap.bend source

src/containers/binary_heap.bend on the hub · documented module

import Baseimport ./types/binary_heap.bend as E# Min-heap in a PACKED native array: the elements live in slots [0, size) of a# `Base.Array` of 2^depth slots, element i having children 2i+1 and 2i+2 and# parent (i-1)/2. No node is allocated per element and no link is stored: the# heap shape is the index arithmetic (docs/ARCHITECTURE.md).##   push   writes the element at slot `size` and SIFTS IT UP while its parent#          is larger (early exit: the loop stops at the first parent that is#          not larger, which is what makes a random push O(1) on average),#   pop    takes slot 0, moves the last element to the root and SIFTS IT DOWN#          through the smaller child,#   peek   reads slot 0, length is the cached size,#   to_sorted_list clones the array and drains the clone (the heap itself is#          returned unchanged),#   from_list is repeated push.## Index arithmetic uses `U32.shl` (doubling), `U32.inc` (+1) and `U32.shr`# (halving) rather than `U32.add`, because those are exactly the operations# whose Nat meaning the proofs can bridge without ever naming 2^32 -- a# literal the checker would have to expand as a unary Nat# (proofs/binary_heap/u32idx.bend).## The record caches what would otherwise be recomputed per operation: `n` is# the size as a U32 (the index the next push writes), `cap` = 2^depth as a# U32, and `depth` bounds every sift loop. Indices are U32 throughout, so no# index arithmetic walks a unary Nat; `size` stays a Nat because that is what# the specification's `length` is.## The order is a static comparator ~cmp : A -> A -> Cmp (a template# parameter); its total-order laws are proof obligations of each instance# (proofs/lib/order.bend: U32 and String). Elements equal under cmp are# identical under the laws, so multiplicities are exact.## Cost (n = size): push O(log n) worst case and O(1) expected, pop O(log n),# peek/length O(1), from_list O(n log n), to_sorted_list O(n log n) plus one# O(n) array clone. Capacity doubles when a push finds the block full; depth# is bounded by 31, so every slot index is a representable U32.# Errors: peek/pop on an empty heap -> Fail{EmptyHeap}, heap unchanged.type Heap<-A: Data> is Type:  BH{size: Nat, n: U32, depth: Nat, cap: U32, slots: Array<Maybe<&2, A>>}def max_depth() -> Nat:  31ndef le(~A: Data, ~cmp: A -> A -> Cmp, x: A, y: A) -> Bool:  Cmp.is_le(cmp(x, y))def empty_slots(~A: Data, +depth: Nat) -> Array<Maybe<&2, A>>:  Array.new(Maybe<&2, A>, depth, None{})def new(~A: Data) -> Heap<A>:  BH{0n, 0, 0n, 1, empty_slots(~A, 0n)}def length(~A: Data, h: Heap<A>) -> Heap<A> & Nat:  BH{+size, n, depth, cap, arr} = h  (BH{size, n, depth, cap, arr}, size)# ---- reading a slot ----# 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).def slot_or(~A: Data, d: A, m: Maybe<&2, A>) -> A:  match m:    case None{}:      d    case Some{v}:      vdef item_of(~A: Data, m: Maybe<&2, A>) -> Result<&2, &2, E.Error, A>:  match m:    case None{}:      Fail{E.EmptyHeap{}}    case Some{v}:      Done{v}# ---- sift up ----## A sift loop cannot be written as one recursive function with an early exit# in Bend: `match` only scrutinises a parameter, and definitions may not be# mutually recursive. The loop therefore carries its decision in a state that# an earlier (non-recursive) probe builds: `UStop{arr, i}` means the sifted# value belongs at slot i, `UMove{arr, i, pv, p}` means the parent value pv# moves down into slot i and the sift goes on at p.type Up<-A: Data> is Type:  UStop{arr: Array<Maybe<&2, A>>, i: U32}  UMove{arr: Array<Maybe<&2, A>>, i: U32, pv: A, p: U32}# The parent index of i (i > 0). For i = 0 the probe never reads it.def parent(+i: U32) -> U32:  U32.shr(U32.sub(i, 1))def up_dec(~A: Data, arr: Array<Maybe<&2, A>>, i: U32, pv: A, p: U32, ok: Bool) -> Up<A>:  match ok:    case True{}:      UStop{arr, i}    case False{}:      UMove{arr, i, pv, p}def up_mb(~A: Data, ~cmp: A -> A -> Cmp, arr: Array<Maybe<&2, A>>, i: U32, +x: A, p: U32, m: Maybe<&2, A>) -> Up<A>:  match m:    case None{}:      UStop{arr, i}    case Some{+pv}:      up_dec(~A, arr, i, pv, p, le(~A, ~cmp, pv, x))def up_slot(~A: Data, ~cmp: A -> A -> Cmp, i: U32, x: A, p: U32, r: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Up<A>:  (arr, m) = r  up_mb(~A, ~cmp, arr, i, x, p, m)def up_root(~A: Data, ~cmp: A -> A -> Cmp, +i: U32, x: A, arr: Array<Maybe<&2, A>>, root: Bool) -> Up<A>:  match root:    case True{}:      UStop{arr, i}    case False{}:      up_slot(~A, ~cmp, i, x, parent(i), Array.get(Maybe<&2, A>, arr, parent(i)))# Where the value x, currently destined for slot i, must go next.def up_probe(~A: Data, ~cmp: A -> A -> Cmp, +i: U32, +x: A, arr: Array<Maybe<&2, A>>) -> Up<A>:  up_root(~A, ~cmp, i, x, arr, U32.is_eq(i, 0))def up_go(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, +x: A, st: Up<A>) -> Array<Maybe<&2, A>>:  match fuel st:    case 0n UStop{arr, i}:      Array.set(Maybe<&2, A>, arr, i, Some{x})    case 0n UMove{arr, i, pv, p}:      Array.set(Maybe<&2, A>, arr, i, Some{x})    case 1n+f UStop{arr, i}:      Array.set(Maybe<&2, A>, arr, i, Some{x})    case 1n+f UMove{arr, i, +pv, +p}:      up_go(~A, ~cmp, f, x, up_probe(~A, ~cmp, p, x, Array.set(Maybe<&2, A>, arr, i, Some{pv})))# Place x at slot i and restore heap order upwards (fuel bounds the climb).def sift_up(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, i: U32, +x: A, arr: Array<Maybe<&2, A>>) -> Array<Maybe<&2, A>>:  up_go(~A, ~cmp, fuel, x, up_probe(~A, ~cmp, i, x, arr))# ---- sift down ----type Down<-A: Data> is Type:  DStop{arr: Array<Maybe<&2, A>>, i: U32}  DMove{arr: Array<Maybe<&2, A>>, i: U32, cv: A, ci: U32}def down_dec(~A: Data, arr: Array<Maybe<&2, A>>, i: U32, cv: A, ci: U32, ok: Bool) -> Down<A>:  match ok:    case True{}:      DStop{arr, i}    case False{}:      DMove{arr, i, cv, ci}def down_two(~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>:  match left:    case True{}:      down_dec(~A, arr, i, lv, l, le(~A, ~cmp, x, lv))    case False{}:      down_dec(~A, arr, i, rv, r, le(~A, ~cmp, x, rv))def down_rmb(~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>:  match m:    case None{}:      down_dec(~A, arr, i, lv, l, le(~A, ~cmp, x, lv))    case Some{+rv}:      down_two(~A, ~cmp, arr, i, x, l, lv, r, rv, le(~A, ~cmp, lv, rv))def down_rslot(~A: Data, ~cmp: A -> A -> Cmp, i: U32, x: A, l: U32, +lv: A, r: U32, rr: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Down<A>:  (arr, m) = rr  down_rmb(~A, ~cmp, arr, i, x, l, lv, r, m)def down_lmb(~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>:  match two m:    case _ None{}:      DStop{arr, i}    case True{} Some{+lv}:      down_rslot(~A, ~cmp, i, x, l, lv, U32.inc(l), Array.get(Maybe<&2, A>, arr, U32.inc(l)))    case False{} Some{+lv}:      down_dec(~A, arr, i, lv, l, le(~A, ~cmp, x, lv))def down_lslot(~A: Data, ~cmp: A -> A -> Cmp, i: U32, +x: A, +l: U32, two: Bool, r: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Down<A>:  (arr, m) = r  down_lmb(~A, ~cmp, arr, i, x, l, two, m)def down_has(~A: Data, ~cmp: A -> A -> Cmp, +size: U32, i: U32, x: A, arr: Array<Maybe<&2, A>>, +l: U32, has_left: Bool) -> Down<A>:  match has_left:    case True{}:      down_lslot(~A, ~cmp, i, x, l, U32.is_lt(l, U32.sub(size, 1)), Array.get(Maybe<&2, A>, arr, l))    case False{}:      DStop{arr, i}# Where the value x, currently destined for slot i of a heap of `size`# elements, must go next.def down_probe(~A: Data, ~cmp: A -> A -> Cmp, +size: U32, +i: U32, x: A, arr: Array<Maybe<&2, A>>) -> Down<A>:  down_has(~A, ~cmp, size, i, x, arr, U32.inc(U32.shl(i)), U32.is_lt(U32.inc(U32.shl(i)), size))def down_go(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, +size: U32, +x: A, st: Down<A>) -> Array<Maybe<&2, A>>:  match fuel st:    case 0n DStop{arr, i}:      Array.set(Maybe<&2, A>, arr, i, Some{x})    case 0n DMove{arr, i, cv, ci}:      Array.set(Maybe<&2, A>, arr, i, Some{x})    case 1n+f DStop{arr, i}:      Array.set(Maybe<&2, A>, arr, i, Some{x})    case 1n+f DMove{arr, i, +cv, +ci}:      down_go(~A, ~cmp, f, size, x, down_probe(~A, ~cmp, size, ci, x, Array.set(Maybe<&2, A>, arr, i, Some{cv})))# Place x at slot i of a heap of `size` elements and restore heap order down.def sift_down(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, +size: U32, i: U32, +x: A, arr: Array<Maybe<&2, A>>) -> Array<Maybe<&2, A>>:  down_go(~A, ~cmp, fuel, size, x, down_probe(~A, ~cmp, size, i, x, arr))# ---- push ----# Doubling: the old block becomes the lower half of a block one level deeper,# so every element keeps its index.def grown(~A: Data, +depth: Nat, arr: Array<Maybe<&2, A>>) -> Array<Maybe<&2, A>>:  ANode{arr, empty_slots(~A, depth)}def push_room(~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>:  match room:    case True{}:      BH{1n+size, U32.inc(n), depth, cap, sift_up(~A, ~cmp, depth, n, x, arr)}    case False{}:      BH{1n+size, U32.inc(n), 1n+depth, U32.shl(cap), sift_up(~A, ~cmp, 1n+depth, n, x, grown(~A, depth, arr))}def push(~A: Data, ~cmp: A -> A -> Cmp, h: Heap<A>, x: A) -> Heap<A>:  BH{size, +n, +depth, +cap, arr} = h  push_room(~A, ~cmp, size, n, depth, cap, arr, x, U32.is_lt(n, cap))# ---- peek ----def peek_found(~A: Data, size: Nat, n: U32, depth: Nat, cap: U32, r: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Heap<A> & Result<&2, &2, E.Error, A>:  (arr, m) = r  (BH{size, n, depth, cap, arr}, item_of(~A, m))def peek_go(~A: Data, size: Nat, +n: U32, depth: Nat, cap: U32, arr: Array<Maybe<&2, A>>, empty: Bool) -> Heap<A> & Result<&2, &2, E.Error, A>:  match empty:    case True{}:      (BH{size, n, depth, cap, arr}, Fail{E.EmptyHeap{}})    case False{}:      peek_found(~A, size, n, depth, cap, Array.get(Maybe<&2, A>, arr, 0))def peek(~A: Data, h: Heap<A>) -> Heap<A> & Result<&2, &2, E.Error, A>:  BH{size, +n, depth, cap, arr} = h  peek_go(~A, size, n, depth, cap, arr, U32.is_eq(n, 0))# ---- pop ----# 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.def pop_move(~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) -> Heap<A> & Result<&2, &2, E.Error, A>:  match empty:    case True{}:      (BH{size, m, depth, cap, arr}, Done{root})    case False{}:      (BH{size, m, depth, cap, sift_down(~A, ~cmp, depth, m, 0, last, arr)}, Done{root})def pop_last(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +m: U32, depth: Nat, cap: U32, +root: A, rl: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Heap<A> & Result<&2, &2, E.Error, A>:  (arr, ml) = rl  pop_move(~A, ~cmp, size, m, depth, cap, root, slot_or(~A, root, ml), arr, U32.is_eq(m, 0))# 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.def pop_with(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +n: U32, depth: Nat, cap: U32, arr: Array<Maybe<&2, A>>, mr: Maybe<&2, A>) -> Heap<A> & Result<&2, &2, E.Error, A>:  match mr:    case None{}:      (BH{size, n, depth, cap, arr}, Fail{E.EmptyHeap{}})    case Some{+root}:      pop_last(~A, ~cmp, Nat.sub(size, 1n), U32.sub(n, 1), depth, cap, root, Array.get(Maybe<&2, A>, arr, U32.sub(n, 1)))def pop_root(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +n: U32, depth: Nat, cap: U32, rr: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Heap<A> & Result<&2, &2, E.Error, A>:  (arr, mr) = rr  pop_with(~A, ~cmp, size, n, depth, cap, arr, mr)def pop_go(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +n: U32, depth: Nat, cap: U32, arr: Array<Maybe<&2, A>>, empty: Bool) -> Heap<A> & Result<&2, &2, E.Error, A>:  match empty:    case True{}:      (BH{size, n, depth, cap, arr}, Fail{E.EmptyHeap{}})    case False{}:      pop_root(~A, ~cmp, size, n, depth, cap, Array.get(Maybe<&2, A>, arr, 0))def pop(~A: Data, ~cmp: A -> A -> Cmp, h: Heap<A>) -> Heap<A> & Result<&2, &2, E.Error, A>:  BH{size, +n, depth, cap, arr} = h  pop_go(~A, ~cmp, size, n, depth, cap, arr, U32.is_eq(n, 0))# ---- from_list ----def from_list_go(~A: Data, ~cmp: A -> A -> Cmp, xs: List<&2, A>, h: Heap<A>) -> Heap<A>:  match xs:    case Nil{}:      h    case Con{x, rest}:      from_list_go(~A, ~cmp, rest, push(~A, ~cmp, h, x))def from_list(~A: Data, ~cmp: A -> A -> Cmp, xs: List<&2, A>) -> Heap<A>:  from_list_go(~A, ~cmp, xs, new(~A))# ---- to_sorted_list ----# Repeated root removal on a COPY of the block: the heap itself is unchanged.# The loop carries its state for the same reason the sift loops do.#   DrDone   the copy is exhausted#   DrLast   the root was the last element#   DrMore   the root is out, `m` elements remain and `last` has to sift downtype Drain<-A: Data> is Type:  DrDone{arr: Array<Maybe<&2, A>>}  DrLast{arr: Array<Maybe<&2, A>>, root: A}  DrMore{arr: Array<Maybe<&2, A>>, root: A, m: U32, last: A}# Dropping the (linear) block is O(1): the runtime erases it.def burn(~A: Data, arr: Array<Maybe<&2, A>>) -> List<&2, A>:  Nil{}def burn_cons(~A: Data, root: A, arr: Array<Maybe<&2, A>>) -> List<&2, A>:  Con{root, Nil{}}def drain_mb(~A: Data, arr: Array<Maybe<&2, A>>, root: A, +m: U32, ml: Maybe<&2, A>, empty: Bool) -> Drain<A>:  match ml empty:    case None{} _:      DrLast{arr, root}    case Some{last} True{}:      DrLast{arr, root}    case Some{last} False{}:      DrMore{arr, root, m, last}def drain_last(~A: Data, root: A, +m: U32, empty: Bool, rl: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Drain<A>:  (arr, ml) = rl  drain_mb(~A, arr, root, m, ml, empty)def drain_root(~A: Data, arr: Array<Maybe<&2, A>>, +m: U32, mr: Maybe<&2, A>) -> Drain<A>:  match mr:    case None{}:      DrDone{arr}    case Some{root}:      drain_last(~A, root, m, U32.is_eq(m, 0), Array.get(Maybe<&2, A>, arr, m))def drain_take(~A: Data, +m: U32, r: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Drain<A>:  (arr, mr) = r  drain_root(~A, arr, m, mr)# 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).def drain_take_go(~A: Data, +n: U32, arr: Array<Maybe<&2, A>>, empty: Bool) -> Drain<A>:  match empty:    case True{}:      DrDone{arr}    case False{}:      drain_take(~A, U32.sub(n, 1), Array.get(Maybe<&2, A>, arr, 0))def drain_probe(~A: Data, +n: U32, arr: Array<Maybe<&2, A>>) -> Drain<A>:  drain_take_go(~A, n, arr, U32.is_eq(n, 0))def drain_go(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, +depth: Nat, st: Drain<A>) -> List<&2, A>:  match fuel st:    case _ DrDone{arr}:      burn(~A, arr)    case _ DrLast{arr, root}:      burn_cons(~A, root, arr)    case 0n DrMore{arr, root, m, last}:      burn_cons(~A, root, arr)    case 1n+f DrMore{arr, root, +m, last}:      Con{root, drain_go(~A, ~cmp, f, depth, drain_probe(~A, m, sift_down(~A, ~cmp, depth, m, 0, last, arr)))}def sorted_of(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +n: U32, +depth: Nat, cap: U32, c: Array<Maybe<&2, A>> & Array<Maybe<&2, A>>) -> Heap<A> & List<&2, A>:  (arr, copy) = c  (BH{size, n, depth, cap, arr}, drain_go(~A, ~cmp, size, depth, drain_probe(~A, n, copy)))def to_sorted_list(~A: Data, ~cmp: A -> A -> Cmp, h: Heap<A>) -> Heap<A> & List<&2, A>:  BH{+size, +n, +depth, +cap, arr} = h  sorted_of(~A, ~cmp, size, n, depth, cap, Array.clone(Maybe<&2, A>, arr))# ---- operation traces ----def obs_nat(~A: Data, r: Heap<A> & Nat) -> Heap<A> & E.Obs<A>:  (h, n) = r  (h, E.ONat{n})def obs_item(~A: Data, r: Heap<A> & Result<&2, &2, E.Error, A>) -> Heap<A> & E.Obs<A>:  (h, x) = r  (h, E.OItem{x})def obs_list(~A: Data, r: Heap<A> & List<&2, A>) -> Heap<A> & E.Obs<A>:  (h, xs) = r  (h, E.OList{xs})def drop_heap(~A: Data, h: Heap<A>, v: Heap<A> & E.Obs<A>) -> Heap<A> & E.Obs<A>:  v# FromList replaces the heap: the old block is dropped (O(1) erasure).def replace(~A: Data, ~cmp: A -> A -> Cmp, h: Heap<A>, xs: List<&2, A>) -> Heap<A> & E.Obs<A>:  BH{size, n, depth, cap, arr} = h  (from_list(~A, ~cmp, xs), E.OUnit{})def step(~A: Data, ~cmp: A -> A -> Cmp, h: Heap<A>, op: E.Op<A>) -> Heap<A> & E.Obs<A>:  match op:    case E.Length{}:      obs_nat(~A, length(~A, h))    case E.Push{x}:      (push(~A, ~cmp, h, x), E.OUnit{})    case E.Peek{}:      obs_item(~A, peek(~A, h))    case E.Pop{}:      obs_item(~A, pop(~A, ~cmp, h))    case E.FromList{xs}:      replace(~A, ~cmp, h, xs)    case E.ToSortedList{}:      obs_list(~A, to_sorted_list(~A, ~cmp, h))def record(~A: Data, acc: List<&2, E.Obs<A>>, r: Heap<A> & E.Obs<A>) -> Heap<A> & List<&2, E.Obs<A>>:  (h, o) = r  (h, Con{o, acc})def step_acc(~A: Data, ~cmp: A -> A -> Cmp, op: E.Op<A>, st: Heap<A> & List<&2, E.Obs<A>>) -> Heap<A> & List<&2, E.Obs<A>>:  (h, acc) = st  record(~A, acc, step(~A, ~cmp, h, op))def run_acc(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op<A>>, st: Heap<A> & List<&2, E.Obs<A>>) -> Heap<A> & List<&2, E.Obs<A>>:  match ops:    case Nil{}:      st    case Con{op, rest}:      run_acc(~A, ~cmp, rest, step_acc(~A, ~cmp, op, st))def finish(~A: Data, st: Heap<A> & List<&2, E.Obs<A>>) -> Heap<A> & List<&2, E.Obs<A>>:  (h, acc) = st  (h, List.reverse(&2, E.Obs<A>, acc))def run(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op<A>>, h: Heap<A>) -> Heap<A> & List<&2, E.Obs<A>>:  finish(~A, run_acc(~A, ~cmp, ops, (h, Nil{})))# ---- checked instances (proofs/binary_heap.bend) ----def run_u32(ops: List<&2, E.Op<U32>>, h: Heap<U32>) -> Heap<U32> & List<&2, E.Obs<U32>>:  run(~U32, ~U32.cmp, ops, h)def run_string(ops: List<&2, E.Op<String>>, h: Heap<String>) -> Heap<String> & List<&2, E.Obs<String>>:  run(~String, ~String.order, ops, h)