def merge_ordered

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

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

135def merge_ordered(~A: Data, +fuel: Nat, +a: H.Heap<Q.Ticket<A>>, +b: H.Heap<Q.Ticket<A>>, +ea: L.ordered(A, a), +eb: L.ordered(A, b)) -> L.ordered(A, H.Heap.merge.go(~Q.Ticket<A>, ~(x => y => Q.le(A, x, y)), fuel, a, b)):
136  match fuel:
137    case 0n:
138      ea
139    case 1n+f:
140      match a b:
141        case H.HLeaf{} H.HLeaf{}:
142          Unit{}
143        case H.HLeaf{} H.HNode{nb, y, bl, br}:
144          eb
145        case H.HNode{na, x, al, ar} H.HLeaf{}:
146          ea
147        case H.HNode{na, x, al, ar} H.HNode{nb, y, bl, br}:
148          L.Both{L.Both{xal, xar}, L.Both{oal, oar}} = ea
149          L.Both{L.Both{ybl, ybr}, L.Both{obl, obr}} = eb
150          split(c => L.ordered(A, H.HNode{Nat.add(na, nb), Bool.pick(Q.Ticket<A>, c, x, y), H.Heap.merge.go(~Q.Ticket<A>, ~(x => y => Q.le(A, x, y)), f, Bool.pick(H.Heap<Q.Ticket<A>>, c, ar, br), Bool.pick(H.Heap<Q.Ticket<A>>, c, H.HNode{nb, y, bl, br}, H.HNode{na, x, al, ar})), Bool.pick(H.Heap<Q.Ticket<A>>, c, al, bl)}), Q.le(A, x, y),
151            +e => L.Both{L.Both{merge_all(~A, L.bound.ticket(A, x), f, ar, H.HNode{nb, y, bl, br}, xar, L.Both{e, L.Both{below_trans(A, bl, x, y, e, ybl), below_trans(A, br, x, y, e, ybr)}}), xal}, L.Both{merge_ordered(~A, f, ar, H.HNode{nb, y, bl, br}, oar, L.Both{L.Both{ybl, ybr}, L.Both{obl, obr}}), oal}},
152            e => (
153              +e = le_flip(A, x, y, e)
154              L.Both{L.Both{merge_all(~A, L.bound.ticket(A, y), f, br, H.HNode{na, x, al, ar}, ybr, L.Both{e, L.Both{below_trans(A, al, y, x, e, xal), below_trans(A, ar, y, x, e, xar)}}), ybl}, L.Both{merge_ordered(~A, f, br, H.HNode{na, x, al, ar}, obr, L.Both{L.Both{xal, xar}, L.Both{oal, oar}}), obl}}))