def remove_all

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

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

159def remove_all(~A: Data, -P: Q.Ticket<A> -> Data, +h: H.Heap<Q.Ticket<A>>, +i: Nat, +eh: L.all.heap(A, P, h)) -> L.all.heap(A, P, Q.remove.heap(~A, h, i)):
160  match h:
161    case H.HLeaf{}:
162      Unit{}
163    case H.HNode{n, t, l, r}:
164      L.Both{et, L.Both{el, er}} = eh
165      +l2 = Q.remove.heap(~A, l, i)
166      +r2 = Q.remove.heap(~A, r, i)
167      +el2 = remove_all(~A, P, l, i, el)
168      +er2 = remove_all(~A, P, r, i, er)
169      split(c => L.all.heap(A, P, Q.remove.heap.keep(~A, c, t, l2, r2)), Nat.is_eq(Q.id(A, t), i),
170        e => merge_all.full(~A, P, l2, r2, el2, er2),
171        e => L.Both{et, L.Both{el2, er2}})