def remove_ordered

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

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

173def remove_ordered(~A: Data, +h: H.Heap<Q.Ticket<A>>, +i: Nat, +eh: L.ordered(A, h)) -> L.ordered(A, Q.remove.heap(~A, h, i)):
174  match h:
175    case H.HLeaf{}:
176      Unit{}
177    case H.HNode{n, t, l, r}:
178      L.Both{L.Both{el, er}, L.Both{ol, or}} = eh
179      +l2 = Q.remove.heap(~A, l, i)
180      +r2 = Q.remove.heap(~A, r, i)
181      +ol2 = remove_ordered(~A, l, i, ol)
182      +or2 = remove_ordered(~A, r, i, or)
183      split(c => L.ordered(A, Q.remove.heap.keep(~A, c, t, l2, r2)), Nat.is_eq(Q.id(A, t), i),
184        e => merge_ordered.full(~A, l2, r2, ol2, or2),
185        e => L.Both{L.Both{remove_all(~A, L.bound.ticket(A, t), l, i, el), remove_all(~A, L.bound.ticket(A, t), r, i, er)}, L.Both{ol2, or2}})