heap.bend checks

raw source on the hub · import bend-kit-collections@0.1.1.0/heap.bend as Heap

Heap: a priority queue, as a skew heap ordered by a le you pass in.

The smallest element (by le) sits at the top. push and pop are amortized O(log n) over a heap used once (sharing one with + and popping both copies can cost more), peek and size are O(1), and sort is heapsort. le is a template, as in List.sort: Heap.push(~U32, ~U32.is_le, 7, h).

The laws at the bottom are checked every time this file is imported.

1 import

import Base

Laws

law Heap.pop.push_new provedsource · line 110 · raw

@-x:U32 -> {Heap.pop(U32, U32.is_le, Heap.push(U32, U32.is_le, x, Heap.new(U32))) == Some{(x, Heap.new(U32))} : Maybe<&1, Pair(U32, Heap<U32>)>}

LAW: popping what was pushed onto an empty heap gives it back

law Heap.size.push provedsource · line 119 · raw

@-x:U32 -> @h:Heap<U32> -> {Heap.size(U32, Heap.push(U32, U32.is_le, x, h)) == 1n+Heap.size(U32, h) : Nat}

LAW: a push adds one to the size

Types

type Heap source · line 12 · raw

@-A:Data -> Data

HLeaf
```
@-A:Data -> Heap<A>
```

HNode

@-A:Data -> @size:Nat -> @top:A -> @left:Heap<A> -> @right:Heap<A> -> Heap<A>

Definitions

def Heap.new source · line 16 · raw

@-A:Data -> Heap<A>

def Heap.size source · line 19 · raw

@-A:Data -> @h:Heap<A> -> Nat

def Heap.peek source · line 26 · raw

@-A:Data -> @h:Heap<A> -> Maybe<&2, A>

Templates

template Heap.merge.go source · line 37 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @fuel:Nat -> @a:Heap<A> -> @b:Heap<A> -> Heap<A>

The smaller root wins: its right child merges with the other heap and becomes the left, and its old left becomes the right (a skew heap's swap, which keeps merges short on average). The fuel is the size of both heaps: every step takes a root out, so it never runs short.

template Heap.merge source · line 60 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+a:Heap<A> -> @+b:Heap<A> -> Heap<A>

template Heap.push source · line 65 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @x:A -> @h:Heap<A> -> Heap<A>

template Heap.pop source · line 69 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @h:Heap<A> -> Maybe<&1, Pair(A, Heap<A>)>

the top, and the heap without it; None on an empty heap

template Heap.from_list source · line 78 · raw

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

template Heap.to_list.go source · line 85 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @fuel:Nat -> @h:Heap<A> -> List<&2, A>

template Heap.to_list source · line 99 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+h:Heap<A> -> List<&2, A>

the elements, smallest first

template Heap.sort source · line 103 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @xs:List<&2, A> -> List<&2, A>

heapsort