def Heap.merge.go

bend-kit-collections@0.1.4.1 · heap.bend:33

import Base

33# The smaller root wins: its right child merges with the other heap and
34# becomes the left, and its old left becomes the right (a skew heap's
35# swap, which keeps merges short on average). The fuel is the size of both
36# heaps: every step takes a root out, so it never runs short.
37def Heap.merge.go(
38  ~A: Data, ~le: A -> A -> Bool, fuel: Nat, a: Heap<A>, b: Heap<A>
39) -> Heap<A>:
40  match fuel:
41    case 0n:
42      a
43    case 1n+f:
44      match a b:
45        case HLeaf{} HLeaf{}:
46          HLeaf{}
47        case HLeaf{} HNode{nb, y, bl, br}:
48          HNode{nb, y, bl, br}
49        case HNode{na, x, al, ar} HLeaf{}:
50          HNode{na, x, al, ar}
51        case HNode{+na, +x, +al, +ar} HNode{+nb, +y, +bl, +br}:
52          +c = le(x, y)
53          HNode{Nat.add(na, nb), Bool.pick(A, c, x, y),
54            Heap.merge.go(~A, ~le, f,
55              Bool.pick(Heap<A>, c, ar, br),
56              Bool.pick(Heap<A>, c, HNode{nb, y, bl, br},
57                HNode{na, x, al, ar})),
58            Bool.pick(Heap<A>, c, al, bl)}