law requeue_token

bend-kit-scheduler@0.4.1.0 · queue_laws.bend:287

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

287# The running token, not a newly assigned ID, is moved back to pending.
288law requeue_token:
289  for ~A: Data
290  for +i: Nat
291  for d: Nat
292  for old: Nat
293  for x: A
294  for n: Nat
295  for h: H.Heap<Q.Ticket<A>>
296  for r: List<&2, Q.Ticket<A>>
297  {Q.requeue(~A, i, d, Q.State{n, h, Q.Ticket{i, old, x} <> r})
298   == (Q.State{n, H.Heap.push(~Q.Ticket<A>, ~(a => b => Q.le(A, a, b)), Q.Ticket{i, d, x}, h), Q.remove.list(A, Q.Ticket{i, old, x} <> r, i)}, True{}) : Q.State<A> & Bool}