def pop_with

bend-collections@1.0.0.0 · src/containers/binary_heap.bend:261

import Base
import bend-collections@1.0.0.0/src/containers/types/binary_heap.bend as E

261# The last element is READ, not cleared: the invariant says nothing about the
262# slots above the size, so clearing it would be one array write per pop that
263# the algorithm does not need (the C reference does not do it either).
264#
265# The root slot of a nonempty heap is Some; the None case cannot be reached
266# from a well-formed heap and returns the state unchanged.
267def 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>:
268  match mr:
269    case None{}:
270      (BH{size, n, depth, cap, arr}, Fail{E.EmptyHeap{}})
271    case Some{+root}:
272      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)))