def remove_absent.heap

bend-kit-scheduler@0.4.1.0 · queue_proof.bend:187

import Base
import bend-kit-collections@0.1.4.1/heap.bend as H
import bend-kit-scheduler@0.4.1.0/queue.bend as Q
import bend-kit-scheduler@0.4.1.0/queue_laws.bend as L

187def remove_absent.heap(~A: Data, +h: H.Heap<Q.Ticket<A>>, +i: Nat) -> L.absent.heap(A, Q.remove.heap(~A, h, i), i):
188  match h:
189    case H.HLeaf{}:
190      Unit{}
191    case H.HNode{n, t, l, r}:
192      +l2 = Q.remove.heap(~A, l, i)
193      +r2 = Q.remove.heap(~A, r, i)
194      +el = remove_absent.heap(~A, l, i)
195      +er = remove_absent.heap(~A, r, i)
196      split(c => L.absent.heap(A, Q.remove.heap.keep(~A, c, t, l2, r2), i), Nat.is_eq(Q.id(A, t), i),
197        e => merge_all.full(~A, L.absent.ticket(A, i), l2, r2, el, er),
198        e => L.Both{e, L.Both{el, er}})