1 import Base
2 import bend-mathlib@0.7.4.0/nat.bend as MNat
3 import bend-mathlib@0.7.4.0/bool.bend as MBool
4 import bend-kit-collections@0.1.4.1/heap.bend as H
5 import ./queue.bend as Q
6 import ./queue_laws.bend as L
7
8 def split(-P: Bool -> Type, b: Bool, yes: {b == True{} : Bool} -> P(True{}), no: {b == False{} : Bool} -> P(False{})) -> P(b):
9 match b:
10 case True{}:
11 yes({==})
12 case False{}:
13 no({==})
14
15 def take_equivalent.step(-A: Data, b: Bool, t: Q.Ticket, rest: List<&2, Q.Ticket>, found: Maybe<&2, Q.Ticket>) -> {Q.take.keep(A, b, t, Q.Taken{rest, found}) == Q.Taken{Q.remove.list.keep(A, b, t, rest), Q.find.list.choose(A, b, t, found)} : Q.Taken}:
16 match b:
17 case True{}:
18 {==}
19 case False{}:
20 {==}
21
22 def L.take_equivalent(A, xs, i):
23 match xs:
24 case Nil{}:
25 {==}
26 case Con{t, rest}:
27 %Equal.sym(Q.Taken, Q.take.list(A, rest, i), Q.Taken{Q.remove.list(A, rest, i), Q.find.list(A, rest, i)}, L.take_equivalent(A, rest, i)) : {Q.take.keep(A, Nat.is_eq(Q.id(A, t), i), t, _) == Q.Taken{Q.remove.list(A, t <> rest, i), Q.find.list(A, t <> rest, i)} : Q.Taken}
28 take_equivalent.step(A, Nat.is_eq(Q.id(A, t), i), t, Q.remove.list(A, rest, i), Q.find.list(A, rest, i))
29
30 def L.complete_equivalent(A, i, s):
31 match s:
32 case Q.State{n, h, r}:
33 %Equal.sym(Q.Taken, Q.take.list(A, r, i), Q.Taken{Q.remove.list(A, r, i), Q.find.list(A, r, i)}, L.take_equivalent(A, r, i)) : {Q.complete.taken(A, _, n, h) == L.complete.reference(A, i, Q.State{n, h, r}) : Q.State & Maybe<&2, Q.Ticket>}
34 {==}
35
36 def L.requeue_equivalent(A, i, d, s):
37 %Equal.sym(Q.State & Maybe<&2, Q.Ticket>, Q.complete(A, i, s), L.complete.reference(A, i, s), L.complete_equivalent(A, i, s)) : {Q.requeue.completed(~A, _, d) == L.requeue.reference(~A, i, d, s) : Q.State & Bool}
38 {==}
39
40 def key_refl(+d: Nat, +i: Nat) -> {Q.le.same(Nat.is_eq(d, d), i, i, d, d) == True{} : Bool}:
41 %Equal.sym(Bool, Nat.is_eq(d, d), True{}, MNat.is_eq_refl(d)) : {Q.le.same(_, i, i, d, d) == True{} : Bool}
42 MNat.le_refl(i)
43
44 def key_succ(b: Bool, i: Nat, j: Nat, d: Nat, e: Nat) -> {Q.le.same(b, i, j, 1n+d, 1n+e) == Q.le.same(b, i, j, d, e) : Bool}:
45 match b:
46 case True{}:
47 {==}
48 case False{}:
49 {==}
50
51 def key_succ.premise(+d: Nat, +e: Nat, +i: Nat, +j: Nat, +b: Bool, p: {Q.le.same(Nat.is_eq(d, e), i, j, 1n+d, 1n+e) == b : Bool}) -> {Q.le.same(Nat.is_eq(d, e), i, j, d, e) == b : Bool}:
52 Equal.trans(Bool, Q.le.same(Nat.is_eq(d, e), i, j, d, e), Q.le.same(Nat.is_eq(d, e), i, j, 1n+d, 1n+e), b, Equal.sym(Bool, Q.le.same(Nat.is_eq(d, e), i, j, 1n+d, 1n+e), Q.le.same(Nat.is_eq(d, e), i, j, d, e), key_succ(Nat.is_eq(d, e), i, j, d, e)), p)
53
54 def key_succ.conclusion(+d: Nat, +e: Nat, +i: Nat, +j: Nat, p: {Q.le.same(Nat.is_eq(d, e), i, j, d, e) == True{} : Bool}) -> {Q.le.same(Nat.is_eq(d, e), i, j, 1n+d, 1n+e) == True{} : Bool}:
55 Equal.trans(Bool, Q.le.same(Nat.is_eq(d, e), i, j, 1n+d, 1n+e), Q.le.same(Nat.is_eq(d, e), i, j, d, e), True{}, key_succ(Nat.is_eq(d, e), i, j, d, e), p)
56
57 def key_flip(+d: Nat, +e: Nat, +i: Nat, +j: Nat, p: {Q.le.same(Nat.is_eq(d, e), i, j, d, e) == False{} : Bool}) -> {Q.le.same(Nat.is_eq(e, d), j, i, e, d) == True{} : Bool}:
58 match d e:
59 case 0n 0n:
60 MNat.le_of_lt(j, i, MNat.lt_of_not_le(i, j, p))
61 case 0n 1n+q:
62 Empty.absurd({False{} == True{} : Bool}, MBool.true_ne_false()(p))
63 case 1n+r 0n:
64 {==}
65 case 1n+r 1n+q:
66 key_succ.conclusion(q, r, j, i, key_flip(r, q, i, j, key_succ.premise(r, q, i, j, False{}, p)))
67
68 def key_trans(+d: Nat, +e: Nat, +f: Nat, +i: Nat, +j: Nat, +k: Nat, p: {Q.le.same(Nat.is_eq(d, e), i, j, d, e) == True{} : Bool}, q: {Q.le.same(Nat.is_eq(e, f), j, k, e, f) == True{} : Bool}) -> {Q.le.same(Nat.is_eq(d, f), i, k, d, f) == True{} : Bool}:
69 match d e f:
70 case 0n 0n 0n:
71 MNat.le_trans(i, j, k, p, q)
72 case 0n 0n 1n+r:
73 {==}
74 case 0n 1n+s 0n:
75 Empty.absurd({Nat.is_le(i, k) == True{} : Bool}, MBool.false_ne_true()(q))
76 case 0n 1n+s 1n+r:
77 {==}
78 case 1n+r 0n 0n:
79 Empty.absurd({False{} == True{} : Bool}, MBool.false_ne_true()(p))
80 case 1n+r 0n 1n+t:
81 Empty.absurd({Q.le.same(Nat.is_eq(1n+r, 1n+t), i, k, 1n+r, 1n+t) == True{} : Bool}, MBool.false_ne_true()(p))
82 case 1n+r 1n+s 0n:
83 Empty.absurd({False{} == True{} : Bool}, MBool.false_ne_true()(q))
84 case 1n+r 1n+s 1n+t:
85 key_succ.conclusion(r, t, i, k, key_trans(r, s, t, i, j, k, key_succ.premise(r, s, i, j, True{}, p), key_succ.premise(s, t, j, k, True{}, q)))
86
87 def le_refl(-A: Data, t: Q.Ticket) -> {Q.le(A, t, t) == True{} : Bool}:
88 match t:
89 case Q.Ticket{i, d, x}:
90 key_refl(d, i)
91
92 def le_flip(-A: Data, a: Q.Ticket, b: Q.Ticket, e: {Q.le(A, a, b) == False{} : Bool}) -> {Q.le(A, b, a) == True{} : Bool}:
93 match a b:
94 case Q.Ticket{i, d, x} Q.Ticket{j, f, y}:
95 key_flip(d, f, i, j, e)
96
97 def le_trans(-A: Data, a: Q.Ticket, b: Q.Ticket, c: Q.Ticket, e: {Q.le(A, a, b) == True{} : Bool}, f: {Q.le(A, b, c) == True{} : Bool}) -> {Q.le(A, a, c) == True{} : Bool}:
98 match a b c:
99 case Q.Ticket{i, d, x} Q.Ticket{j, g, y} Q.Ticket{k, h, z}:
100 key_trans(d, g, h, i, j, k, e, f)
101
102 # Merging cannot introduce an element that violates any predicate P. Fuel zero
103 # returns the left heap, so this lemma does not trust cached heap sizes.
104 def merge_all(~A: Data, -P: Q.Ticket -> Data, +fuel: Nat, +a: H.Heap>, +b: H.Heap>, +ea: L.all.heap(A, P, a), +eb: L.all.heap(A, P, b)) -> L.all.heap(A, P, H.Heap.merge.go(~Q.Ticket, ~(x => y => Q.le(A, x, y)), fuel, a, b)):
105 match fuel:
106 case 0n:
107 ea
108 case 1n+f:
109 match a b:
110 case H.HLeaf{} H.HLeaf{}:
111 Unit{}
112 case H.HLeaf{} H.HNode{nb, y, bl, br}:
113 eb
114 case H.HNode{na, x, al, ar} H.HLeaf{}:
115 ea
116 case H.HNode{na, x, al, ar} H.HNode{nb, y, bl, br}:
117 L.Both{ex, L.Both{eal, ear}} = ea
118 L.Both{ey, L.Both{ebl, ebr}} = eb
119 split(c => L.all.heap(A, P, H.HNode{Nat.add(na, nb), Bool.pick(Q.Ticket, c, x, y), H.Heap.merge.go(~Q.Ticket, ~(x => y => Q.le(A, x, y)), f, Bool.pick(H.Heap>, c, ar, br), Bool.pick(H.Heap>, c, H.HNode{nb, y, bl, br}, H.HNode{na, x, al, ar})), Bool.pick(H.Heap>, c, al, bl)}), Q.le(A, x, y),
120 e => L.Both{ex, L.Both{merge_all(~A, P, f, ar, H.HNode{nb, y, bl, br}, ear, L.Both{ey, L.Both{ebl, ebr}}), eal}},
121 e => L.Both{ey, L.Both{merge_all(~A, P, f, br, H.HNode{na, x, al, ar}, ebr, L.Both{ex, L.Both{eal, ear}}), ebl}})
122
123 def merge_all.full(~A: Data, -P: Q.Ticket -> Data, +a: H.Heap>, +b: H.Heap>, ea: L.all.heap(A, P, a), eb: L.all.heap(A, P, b)) -> L.all.heap(A, P, H.Heap.merge(~Q.Ticket, ~(x => y => Q.le(A, x, y)), a, b)):
124 merge_all(~A, P, Nat.add(H.Heap.size(Q.Ticket, a), H.Heap.size(Q.Ticket, b)), a, b, ea, eb)
125
126 def below_trans(-A: Data, h: H.Heap>, +a: Q.Ticket, +b: Q.Ticket, e: {Q.le(A, a, b) == True{} : Bool}, eh: L.below(A, h, b)) -> L.below(A, h, a):
127 match h:
128 case H.HLeaf{}:
129 Unit{}
130 case H.HNode{n, t, l, r}:
131 L.Both{et, L.Both{el, er}} = eh
132 +e = e
133 L.Both{le_trans(A, a, b, t, e, et), L.Both{below_trans(A, l, a, b, e, el), below_trans(A, r, a, b, e, er)}}
134
135 def merge_ordered(~A: Data, +fuel: Nat, +a: H.Heap>, +b: H.Heap>, +ea: L.ordered(A, a), +eb: L.ordered(A, b)) -> L.ordered(A, H.Heap.merge.go(~Q.Ticket, ~(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, c, x, y), H.Heap.merge.go(~Q.Ticket, ~(x => y => Q.le(A, x, y)), f, Bool.pick(H.Heap>, c, ar, br), Bool.pick(H.Heap>, c, H.HNode{nb, y, bl, br}, H.HNode{na, x, al, ar})), Bool.pick(H.Heap>, 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}}))
155
156 def merge_ordered.full(~A: Data, +a: H.Heap>, +b: H.Heap>, ea: L.ordered(A, a), eb: L.ordered(A, b)) -> L.ordered(A, H.Heap.merge(~Q.Ticket, ~(x => y => Q.le(A, x, y)), a, b)):
157 merge_ordered(~A, Nat.add(H.Heap.size(Q.Ticket, a), H.Heap.size(Q.Ticket, b)), a, b, ea, eb)
158
159 def remove_all(~A: Data, -P: Q.Ticket -> Data, +h: H.Heap>, +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}})
172
173 def remove_ordered(~A: Data, +h: H.Heap>, +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}})
186
187 def remove_absent.heap(~A: Data, +h: H.Heap>, +i: Nat) -> L.absent.heap(A, Q.remove.heap(~A, h, i), i):
188 match h:
189 case H.HLeaf{}:
190 Unit{}
191 case H.HNode{n, t, l, r}:
192 +l2 = Q.remove.heap(~A, l, i)
193 +r2 = Q.remove.heap(~A, r, i)
194 +el = remove_absent.heap(~A, l, i)
195 +er = remove_absent.heap(~A, r, i)
196 split(c => L.absent.heap(A, Q.remove.heap.keep(~A, c, t, l2, r2), i), Nat.is_eq(Q.id(A, t), i),
197 e => merge_all.full(~A, L.absent.ticket(A, i), l2, r2, el, er),
198 e => L.Both{e, L.Both{el, er}})
199
200 def remove_absent.list(-A: Data, +xs: List<&2, Q.Ticket>, +i: Nat) -> L.absent.list(A, Q.remove.list(A, xs, i), i):
201 match xs:
202 case Nil{}:
203 Unit{}
204 case Con{t, rest}:
205 +r2 = Q.remove.list(A, rest, i)
206 +er = remove_absent.list(A, rest, i)
207 split(c => L.absent.list(A, Q.remove.list.keep(A, c, t, r2), i), Nat.is_eq(Q.id(A, t), i),
208 e => er,
209 e => L.Both{e, er})
210
211 def L.absent_find(A, xs, i, e):
212 match xs:
213 case Nil{}:
214 {==}
215 case Con{t, rest}:
216 L.Both{et, er} = e
217 %Equal.sym(Bool, Nat.is_eq(Q.id(A, t), i), False{}, et) : {Q.find.list.choose(A, _, t, Q.find.list(A, rest, i)) == None{} : Maybe<&2, Q.Ticket>}
218 L.absent_find(A, rest, i, er)
219
220 def L.new_ordered(A):
221 Unit{}
222
223 def L.equal_deadline_fifo(A, i, j, d, x, y):
224 +d = d
225 %Equal.sym(Bool, Nat.is_eq(d, d), True{}, MNat.is_eq_refl(d)) : {Q.le.same(_, i, j, d, d) == Nat.is_le(i, j) : Bool}
226 {==}
227
228 def L.enqueue_id(A, d, x, s):
229 match s:
230 case Q.State{n, h, r}:
231 {==}
232
233 def L.cancel_pending_absent(A, i, s):
234 match s:
235 case Q.State{n, h, r}:
236 remove_absent.heap(~A, h, i)
237
238 def L.cancel_running_absent(A, i, s):
239 match s:
240 case Q.State{n, h, r}:
241 remove_absent.list(A, r, i)
242
243 def L.complete_one_shot(A, i, s):
244 match s:
245 case Q.State{+n, +h, r}:
246 +r = r
247 %Equal.sym(Q.State & Maybe<&2, Q.Ticket>, Q.complete(A, i, Q.State{n, h, r}), L.complete.reference(A, i, Q.State{n, h, r}), L.complete_equivalent(A, i, Q.State{n, h, r})) : {L.selected(A, Q.complete(A, i, L.state(A, _))) == None{} : Maybe<&2, Q.Ticket>}
248 %Equal.sym(Q.State & Maybe<&2, Q.Ticket>, Q.complete(A, i, Q.State{n, h, Q.remove.list(A, r, i)}), L.complete.reference(A, i, Q.State{n, h, Q.remove.list(A, r, i)}), L.complete_equivalent(A, i, Q.State{n, h, Q.remove.list(A, r, i)})) : {L.selected(A, _) == None{} : Maybe<&2, Q.Ticket>}
249 L.absent_find(A, Q.remove.list(A, r, i), i, remove_absent.list(A, r, i))
250
251 def L.cancel_complete(A, i, s):
252 match s:
253 case Q.State{n, h, r}:
254 +r = r
255 %Equal.sym(Q.State & Maybe<&2, Q.Ticket>, Q.complete(A, i, Q.cancel(~A, i, Q.State{n, h, r})), L.complete.reference(A, i, Q.cancel(~A, i, Q.State{n, h, r})), L.complete_equivalent(A, i, Q.cancel(~A, i, Q.State{n, h, r}))) : {L.selected(A, _) == None{} : Maybe<&2, Q.Ticket>}
256 L.absent_find(A, Q.remove.list(A, r, i), i, remove_absent.list(A, r, i))
257
258 def requeue_absent(~A: Data, +i: Nat, d: Nat, +s: Q.State, e: {Q.find.list(A, Q.running(A, s), i) == None{} : Maybe<&2, Q.Ticket>}) -> {L.requeued(A, Q.requeue(~A, i, d, s)) == False{} : Bool}:
259 match s:
260 case Q.State{n, h, r}:
261 %Equal.sym(Q.State & Bool, Q.requeue(~A, i, d, Q.State{n, h, r}), L.requeue.reference(~A, i, d, Q.State{n, h, r}), L.requeue_equivalent(~A, i, d, Q.State{n, h, r})) : {L.requeued(A, _) == False{} : Bool}
262 %Equal.sym(Maybe<&2, Q.Ticket>, Q.find.list(A, r, i), None{}, e) : {L.requeued(A, Q.requeue.completed(~A, (Q.State{n, h, Q.remove.list(A, r, i)}, _), d)) == False{} : Bool}
263 {==}
264
265 def L.cancel_requeue(A, i, d, s):
266 match s:
267 case Q.State{n, h, +r}:
268 requeue_absent(~A, i, d, Q.State{n, Q.remove.heap(~A, h, i), Q.remove.list(A, r, i)}, L.absent_find(A, Q.remove.list(A, r, i), i, remove_absent.list(A, r, i)))
269
270 def L.complete_requeue(A, i, d, s):
271 match s:
272 case Q.State{+n, +h, +r}:
273 %Equal.sym(Q.State & Maybe<&2, Q.Ticket>, Q.complete(A, i, Q.State{n, h, r}), L.complete.reference(A, i, Q.State{n, h, r}), L.complete_equivalent(A, i, Q.State{n, h, r})) : {L.requeued(A, Q.requeue(~A, i, d, L.state(A, _))) == False{} : Bool}
274 requeue_absent(~A, i, d, Q.State{n, h, Q.remove.list(A, r, i)}, L.absent_find(A, Q.remove.list(A, r, i), i, remove_absent.list(A, r, i)))
275
276 def L.select_due(A, now, s):
277 match s:
278 case Q.State{i, H.HLeaf{}, r}:
279 Unit{}
280 case Q.State{i, H.HNode{n, t, l, q}, r}:
281 +t = t
282 +now = now
283 split(c => L.due(A, L.selected(A, Q.select.due(~A, c, i, H.HNode{n, t, l, q}, r, t, l, q)), now), Nat.is_le(Q.deadline(A, t), now),
284 e => e,
285 e => Unit{})
286
287 def L.select_minimum(A, now, s, e):
288 match s:
289 case Q.State{i, H.HLeaf{}, r}:
290 Unit{}
291 case Q.State{i, H.HNode{n, t, l, q}, r}:
292 L.Both{L.Both{el, eq}, L.Both{ol, oq}} = e
293 split(c => L.minimum(A, H.HNode{n, t, l, q}, L.selected(A, Q.select.due(~A, c, i, H.HNode{n, t, l, q}, r, t, l, q))), Nat.is_le(Q.deadline(A, t), now),
294 e => L.Both{le_refl(A, t), L.Both{el, eq}},
295 e => Unit{})
296
297 def L.select_absent(A, now, i, s, eh, er):
298 match s:
299 case Q.State{n, H.HLeaf{}, r}:
300 (Unit{}, er)
301 case Q.State{n, H.HNode{size, t, l, q}, r}:
302 L.Both{+et, L.Both{+el, +eq}} = eh
303 +er = er
304 split(c => L.absent.heap(A, Q.pending(A, L.state(A, Q.select.due(~A, c, n, H.HNode{size, t, l, q}, r, t, l, q))), i) & L.absent.list(A, Q.running(A, L.state(A, Q.select.due(~A, c, n, H.HNode{size, t, l, q}, r, t, l, q))), i), Nat.is_le(Q.deadline(A, t), now),
305 e => (merge_all.full(~A, L.absent.ticket(A, i), l, q, el, eq), L.Both{et, er}),
306 e => (L.Both{et, L.Both{el, eq}}, er))
307
308 def selected_absent(-A: Data, +i: Nat, m: Maybe<&2, Q.Ticket>) -> Data:
309 match m:
310 case None{}:
311 Unit
312 case Some{t}:
313 {Nat.is_eq(Q.id(A, t), i) == False{} : Bool}
314
315 def select_selected_absent(~A: Data, now: Nat, +i: Nat, +s: Q.State, 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{})
324
325 def L.absent_selected(A, now, i, s, eh, t, e):
326 %e : selected_absent(A, i, _)
327 select_selected_absent(~A, now, i, s, eh)
328
329 def push_ordered(~A: Data, t: Q.Ticket, h: H.Heap>, e: L.ordered(A, h)) -> L.ordered(A, H.Heap.push(~Q.Ticket, ~(x => y => Q.le(A, x, y)), t, h)):
330 merge_ordered.full(~A, H.HNode{1n, t, H.HLeaf{}, H.HLeaf{}}, h, L.Both{L.Both{Unit{}, Unit{}}, L.Both{Unit{}, Unit{}}}, e)
331
332 def L.enqueue_ordered(A, d, x, s, e):
333 match s:
334 case Q.State{n, h, r}:
335 push_ordered(~A, Q.Ticket{n, d, x}, h, e)
336
337 def L.select_ordered(A, now, s, e):
338 match s:
339 case Q.State{i, H.HLeaf{}, r}:
340 Unit{}
341 case Q.State{i, H.HNode{n, t, l, q}, r}:
342 L.Both{L.Both{el, eq}, L.Both{+ol, +oq}} = e
343 split(c => L.ordered(A, Q.pending(A, L.state(A, Q.select.due(~A, c, i, H.HNode{n, t, l, q}, r, t, l, q)))), Nat.is_le(Q.deadline(A, t), now),
344 e => merge_ordered.full(~A, l, q, ol, oq),
345 e2 => L.Both{L.Both{el, eq}, L.Both{ol, oq}})
346
347 def L.cancel_ordered(A, i, s, e):
348 match s:
349 case Q.State{n, h, r}:
350 remove_ordered(~A, h, i, e)
351
352 def requeue_ordered.found(~A: Data, found: Maybe<&2, Q.Ticket>, d: Nat, +s: Q.State, e: L.ordered(A, Q.pending(A, s))) -> L.ordered(A, Q.pending(A, L.requeue.state(A, Q.requeue.found(~A, found, d, s)))):
353 match found:
354 case None{}:
355 e
356 case Some{Q.Ticket{i, old, x}}:
357 match s:
358 case Q.State{n, h, r}:
359 push_ordered(~A, Q.Ticket{i, d, x}, h, e)
360
361 def L.requeue_ordered(A, i, d, s, e):
362 match s:
363 case Q.State{n, h, r}:
364 +d = d
365 %Equal.sym(Q.State & Bool, Q.requeue(~A, i, d, Q.State{n, h, r}), L.requeue.reference(~A, i, d, Q.State{n, h, r}), L.requeue_equivalent(~A, i, d, Q.State{n, h, r})) : L.ordered(A, Q.pending(A, L.requeue.state(A, _)))
366 requeue_ordered.found(~A, Q.find.list(A, r, i), d, Q.State{n, h, Q.remove.list(A, r, i)}, e)
367
368 def L.complete_ordered(A, i, s, e):
369 match s:
370 case Q.State{n, h, r}:
371 %Equal.sym(Q.State & Maybe<&2, Q.Ticket>, Q.complete(A, i, Q.State{n, h, r}), L.complete.reference(A, i, Q.State{n, h, r}), L.complete_equivalent(A, i, Q.State{n, h, r})) : L.ordered(A, Q.pending(A, L.state(A, _)))
372 e
373
374 def L.enqueue_assigned_id(A, d, x, s):
375 match s:
376 case Q.State{n, h, r}:
377 {==}
378
379 def L.cancel_keeps_counter(A, i, s):
380 match s:
381 case Q.State{n, h, r}:
382 {==}
383
384 def L.complete_keeps_counter(A, i, s):
385 match s:
386 case Q.State{n, h, r}:
387 %Equal.sym(Q.State & Maybe<&2, Q.Ticket>, Q.complete(A, i, Q.State{n, h, r}), L.complete.reference(A, i, Q.State{n, h, r}), L.complete_equivalent(A, i, Q.State{n, h, r})) : {Q.next_id(A, L.state(A, _)) == n : Nat}
388 {==}
389
390 def L.select_keeps_counter(A, now, s):
391 match s:
392 case Q.State{i, H.HLeaf{}, r}:
393 {==}
394 case Q.State{i, H.HNode{n, t, l, q}, r}:
395 split(c => {Q.next_id(A, L.state(A, Q.select.due(~A, c, i, H.HNode{n, t, l, q}, r, t, l, q))) == i : Nat}, Nat.is_le(Q.deadline(A, t), now),
396 e => {==}, e => {==})
397
398 def requeue_counter.found(~A: Data, found: Maybe<&2, Q.Ticket>, d: Nat, +s: Q.State) -> {Q.next_id(A, L.requeue.state(A, Q.requeue.found(~A, found, d, s))) == Q.next_id(A, s) : Nat}:
399 match found:
400 case None{}:
401 {==}
402 case Some{Q.Ticket{i, old, x}}:
403 match s:
404 case Q.State{n, h, r}:
405 {==}
406
407 def L.requeue_keeps_counter(A, i, d, s):
408 match s:
409 case Q.State{n, h, r}:
410 +i = i
411 +d = d
412 %Equal.sym(Q.State & Bool, Q.requeue(~A, i, d, Q.State{n, h, r}), L.requeue.reference(~A, i, d, Q.State{n, h, r}), L.requeue_equivalent(~A, i, d, Q.State{n, h, r})) : {Q.next_id(A, L.requeue.state(A, _)) == n : Nat}
413 requeue_counter.found(~A, Q.find.list(A, r, i), d, Q.State{n, h, Q.remove.list(A, r, i)})
414
415 def L.requeue_token(A, i, d, old, x, n, h, r):
416 +x = x
417 +n = n
418 +h = h
419 +r = r
420 +d = d
421 %Equal.sym(Q.State & Bool, Q.requeue(~A, i, d, Q.State{n, h, Q.Ticket{i, old, x} <> r}), L.requeue.reference(~A, i, d, Q.State{n, h, Q.Ticket{i, old, x} <> r}), L.requeue_equivalent(~A, i, d, Q.State{n, h, Q.Ticket{i, old, x} <> r})) : {_ == (Q.State{n, H.Heap.push(~Q.Ticket, ~(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 & Bool}
422 %Equal.sym(Bool, Nat.is_eq(i, i), True{}, MNat.is_eq_refl(i)) : {Q.requeue.completed(~A, (Q.State{n, h, Q.remove.list(A, Q.Ticket{i, old, x} <> r, i)}, Q.find.list.choose(A, _, Q.Ticket{i, old, x}, Q.find.list(A, r, i))), d) == (Q.State{n, H.Heap.push(~Q.Ticket, ~(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 & Bool}
423 {==}
424
425 def L.complete_token(A, i, old, x, n, h, r):
426 +x = x
427 +r = r
428 %Equal.sym(Q.State & Maybe<&2, Q.Ticket>, Q.complete(A, i, Q.State{n, h, Q.Ticket{i, old, x} <> r}), L.complete.reference(A, i, Q.State{n, h, Q.Ticket{i, old, x} <> r}), L.complete_equivalent(A, i, Q.State{n, h, Q.Ticket{i, old, x} <> r})) : {L.selected(A, _) == Some{Q.Ticket{i, old, x}} : Maybe<&2, Q.Ticket>}
429 %Equal.sym(Bool, Nat.is_eq(i, i), True{}, MNat.is_eq_refl(i)) : {Q.find.list.choose(A, _, Q.Ticket{i, old, x}, Q.find.list(A, r, i)) == Some{Q.Ticket{i, old, x}} : Maybe<&2, Q.Ticket>}
430 {==}