def select_selected_absent

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

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

315def select_selected_absent(~A: Data, now: Nat, +i: Nat, +s: Q.State<A>, eh: L.absent.heap(A, Q.pending(A, s), i)) -> selected_absent(A, i, L.selected(A, Q.select(~A, now, s))):
316  match s:
317    case Q.State{n, H.HLeaf{}, r}:
318      Unit{}
319    case Q.State{n, H.HNode{size, t, l, q}, r}:
320      L.Both{et, L.Both{el, eq}} = eh
321      split(c => selected_absent(A, i, L.selected(A, Q.select.due(~A, c, n, H.HNode{size, t, l, q}, r, t, l, q))), Nat.is_le(Q.deadline(A, t), now),
322        e => et,
323        e => Unit{})