src/containers/binary_heap.bend
bend-collections-laws-containers@1.0.0.0 · 442 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/src/containers/types/binary_heap.bend as E
3
4# Min-heap in a PACKED native array: the elements live in slots [0, size) of a
5# `Base.Array` of 2^depth slots, element i having children 2i+1 and 2i+2 and
6# parent (i-1)/2. No node is allocated per element and no link is stored: the
7# heap shape is the index arithmetic (docs/ARCHITECTURE.md).
8#
9# push writes the element at slot `size` and SIFTS IT UP while its parent
10# is larger (early exit: the loop stops at the first parent that is
11# not larger, which is what makes a random push O(1) on average),
12# pop takes slot 0, moves the last element to the root and SIFTS IT DOWN
13# through the smaller child,
14# peek reads slot 0, length is the cached size,
15# to_sorted_list clones the array and drains the clone (the heap itself is
16# returned unchanged),
17# from_list is repeated push.
18#
19# Index arithmetic uses `U32.shl` (doubling), `U32.inc` (+1) and `U32.shr`
20# (halving) rather than `U32.add`, because those are exactly the operations
21# whose Nat meaning the proofs can bridge without ever naming 2^32 -- a
22# literal the checker would have to expand as a unary Nat
23# (proofs/binary_heap/u32idx.bend).
24#
25# The record caches what would otherwise be recomputed per operation: `n` is
26# the size as a U32 (the index the next push writes), `cap` = 2^depth as a
27# U32, and `depth` bounds every sift loop. Indices are U32 throughout, so no
28# index arithmetic walks a unary Nat; `size` stays a Nat because that is what
29# the specification's `length` is.
30#
31# The order is a static comparator ~cmp : A -> A -> Cmp (a template
32# parameter); its total-order laws are proof obligations of each instance
33# (proofs/lib/order.bend: U32 and String). Elements equal under cmp are
34# identical under the laws, so multiplicities are exact.
35#
36# Cost (n = size): push O(log n) worst case and O(1) expected, pop O(log n),
37# peek/length O(1), from_list O(n log n), to_sorted_list O(n log n) plus one
38# O(n) array clone. Capacity doubles when a push finds the block full; depth
39# is bounded by 31, so every slot index is a representable U32.
40# Errors: peek/pop on an empty heap -> Fail{EmptyHeap}, heap unchanged.
41
42type Heap<-A: Data> is Type:
43 BH{size: Nat, n: U32, depth: Nat, cap: U32, slots: Array<Maybe<&2, A>>}
44
45def max_depth() -> Nat:
46 31n
47
48def le(~A: Data, ~cmp: A -> A -> Cmp, x: A, y: A) -> Bool:
49 Cmp.is_le(cmp(x, y))
50
51def empty_slots(~A: Data, +depth: Nat) -> Array<Maybe<&2, A>>:
52 Array.new(Maybe<&2, A>, depth, None{})
53
54def new(~A: Data) -> Heap<A>:
55 BH{0n, 0, 0n, 1, empty_slots(~A, 0n)}
56
57def length(~A: Data, h: Heap<A>) -> Heap<A> & Nat:
58 BH{+size, n, depth, cap, arr} = h
59 (BH{size, n, depth, cap, arr}, size)
60
61# ---- reading a slot ----
62
63# The slot value, with a default that a well-formed heap never needs (every
64# index a sift loop reads is inside [0, size), where the slot is Some).
65def slot_or(~A: Data, d: A, m: Maybe<&2, A>) -> A:
66 match m:
67 case None{}:
68 d
69 case Some{v}:
70 v
71
72def item_of(~A: Data, m: Maybe<&2, A>) -> Result<&2, &2, E.Error, A>:
73 match m:
74 case None{}:
75 Fail{E.EmptyHeap{}}
76 case Some{v}:
77 Done{v}
78
79# ---- sift up ----
80#
81# A sift loop cannot be written as one recursive function with an early exit
82# in Bend: `match` only scrutinises a parameter, and definitions may not be
83# mutually recursive. The loop therefore carries its decision in a state that
84# an earlier (non-recursive) probe builds: `UStop{arr, i}` means the sifted
85# value belongs at slot i, `UMove{arr, i, pv, p}` means the parent value pv
86# moves down into slot i and the sift goes on at p.
87
88type Up<-A: Data> is Type:
89 UStop{arr: Array<Maybe<&2, A>>, i: U32}
90 UMove{arr: Array<Maybe<&2, A>>, i: U32, pv: A, p: U32}
91
92# The parent index of i (i > 0). For i = 0 the probe never reads it.
93def parent(+i: U32) -> U32:
94 U32.shr(U32.sub(i, 1))
95
96def up_dec(~A: Data, arr: Array<Maybe<&2, A>>, i: U32, pv: A, p: U32, ok: Bool) -> Up<A>:
97 match ok:
98 case True{}:
99 UStop{arr, i}
100 case False{}:
101 UMove{arr, i, pv, p}
102
103def up_mb(~A: Data, ~cmp: A -> A -> Cmp, arr: Array<Maybe<&2, A>>, i: U32, +x: A, p: U32, m: Maybe<&2, A>) -> Up<A>:
104 match m:
105 case None{}:
106 UStop{arr, i}
107 case Some{+pv}:
108 up_dec(~A, arr, i, pv, p, le(~A, ~cmp, pv, x))
109
110def up_slot(~A: Data, ~cmp: A -> A -> Cmp, i: U32, x: A, p: U32, r: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Up<A>:
111 (arr, m) = r
112 up_mb(~A, ~cmp, arr, i, x, p, m)
113
114def up_root(~A: Data, ~cmp: A -> A -> Cmp, +i: U32, x: A, arr: Array<Maybe<&2, A>>, root: Bool) -> Up<A>:
115 match root:
116 case True{}:
117 UStop{arr, i}
118 case False{}:
119 up_slot(~A, ~cmp, i, x, parent(i), Array.get(Maybe<&2, A>, arr, parent(i)))
120
121# Where the value x, currently destined for slot i, must go next.
122def up_probe(~A: Data, ~cmp: A -> A -> Cmp, +i: U32, +x: A, arr: Array<Maybe<&2, A>>) -> Up<A>:
123 up_root(~A, ~cmp, i, x, arr, U32.is_eq(i, 0))
124
125def up_go(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, +x: A, st: Up<A>) -> Array<Maybe<&2, A>>:
126 match fuel st:
127 case 0n UStop{arr, i}:
128 Array.set(Maybe<&2, A>, arr, i, Some{x})
129 case 0n UMove{arr, i, pv, p}:
130 Array.set(Maybe<&2, A>, arr, i, Some{x})
131 case 1n+f UStop{arr, i}:
132 Array.set(Maybe<&2, A>, arr, i, Some{x})
133 case 1n+f UMove{arr, i, +pv, +p}:
134 up_go(~A, ~cmp, f, x, up_probe(~A, ~cmp, p, x, Array.set(Maybe<&2, A>, arr, i, Some{pv})))
135
136# Place x at slot i and restore heap order upwards (fuel bounds the climb).
137def sift_up(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, i: U32, +x: A, arr: Array<Maybe<&2, A>>) -> Array<Maybe<&2, A>>:
138 up_go(~A, ~cmp, fuel, x, up_probe(~A, ~cmp, i, x, arr))
139
140# ---- sift down ----
141
142type Down<-A: Data> is Type:
143 DStop{arr: Array<Maybe<&2, A>>, i: U32}
144 DMove{arr: Array<Maybe<&2, A>>, i: U32, cv: A, ci: U32}
145
146def down_dec(~A: Data, arr: Array<Maybe<&2, A>>, i: U32, cv: A, ci: U32, ok: Bool) -> Down<A>:
147 match ok:
148 case True{}:
149 DStop{arr, i}
150 case False{}:
151 DMove{arr, i, cv, ci}
152
153def down_two(~A: Data, ~cmp: A -> A -> Cmp, arr: Array<Maybe<&2, A>>, i: U32, +x: A, l: U32, +lv: A, r: U32, +rv: A, left: Bool) -> Down<A>:
154 match left:
155 case True{}:
156 down_dec(~A, arr, i, lv, l, le(~A, ~cmp, x, lv))
157 case False{}:
158 down_dec(~A, arr, i, rv, r, le(~A, ~cmp, x, rv))
159
160def down_rmb(~A: Data, ~cmp: A -> A -> Cmp, arr: Array<Maybe<&2, A>>, i: U32, +x: A, l: U32, +lv: A, r: U32, m: Maybe<&2, A>) -> Down<A>:
161 match m:
162 case None{}:
163 down_dec(~A, arr, i, lv, l, le(~A, ~cmp, x, lv))
164 case Some{+rv}:
165 down_two(~A, ~cmp, arr, i, x, l, lv, r, rv, le(~A, ~cmp, lv, rv))
166
167def down_rslot(~A: Data, ~cmp: A -> A -> Cmp, i: U32, x: A, l: U32, +lv: A, r: U32, rr: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Down<A>:
168 (arr, m) = rr
169 down_rmb(~A, ~cmp, arr, i, x, l, lv, r, m)
170
171def down_lmb(~A: Data, ~cmp: A -> A -> Cmp, arr: Array<Maybe<&2, A>>, i: U32, +x: A, +l: U32, two: Bool, m: Maybe<&2, A>) -> Down<A>:
172 match two m:
173 case _ None{}:
174 DStop{arr, i}
175 case True{} Some{+lv}:
176 down_rslot(~A, ~cmp, i, x, l, lv, U32.inc(l), Array.get(Maybe<&2, A>, arr, U32.inc(l)))
177 case False{} Some{+lv}:
178 down_dec(~A, arr, i, lv, l, le(~A, ~cmp, x, lv))
179
180def down_lslot(~A: Data, ~cmp: A -> A -> Cmp, i: U32, +x: A, +l: U32, two: Bool, r: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Down<A>:
181 (arr, m) = r
182 down_lmb(~A, ~cmp, arr, i, x, l, two, m)
183
184def down_has(~A: Data, ~cmp: A -> A -> Cmp, +size: U32, i: U32, x: A, arr: Array<Maybe<&2, A>>, +l: U32, has_left: Bool) -> Down<A>:
185 match has_left:
186 case True{}:
187 down_lslot(~A, ~cmp, i, x, l, U32.is_lt(l, U32.sub(size, 1)), Array.get(Maybe<&2, A>, arr, l))
188 case False{}:
189 DStop{arr, i}
190
191# Where the value x, currently destined for slot i of a heap of `size`
192# elements, must go next.
193def down_probe(~A: Data, ~cmp: A -> A -> Cmp, +size: U32, +i: U32, x: A, arr: Array<Maybe<&2, A>>) -> Down<A>:
194 down_has(~A, ~cmp, size, i, x, arr, U32.inc(U32.shl(i)), U32.is_lt(U32.inc(U32.shl(i)), size))
195
196def down_go(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, +size: U32, +x: A, st: Down<A>) -> Array<Maybe<&2, A>>:
197 match fuel st:
198 case 0n DStop{arr, i}:
199 Array.set(Maybe<&2, A>, arr, i, Some{x})
200 case 0n DMove{arr, i, cv, ci}:
201 Array.set(Maybe<&2, A>, arr, i, Some{x})
202 case 1n+f DStop{arr, i}:
203 Array.set(Maybe<&2, A>, arr, i, Some{x})
204 case 1n+f DMove{arr, i, +cv, +ci}:
205 down_go(~A, ~cmp, f, size, x, down_probe(~A, ~cmp, size, ci, x, Array.set(Maybe<&2, A>, arr, i, Some{cv})))
206
207# Place x at slot i of a heap of `size` elements and restore heap order down.
208def sift_down(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, +size: U32, i: U32, +x: A, arr: Array<Maybe<&2, A>>) -> Array<Maybe<&2, A>>:
209 down_go(~A, ~cmp, fuel, size, x, down_probe(~A, ~cmp, size, i, x, arr))
210
211# ---- push ----
212
213# Doubling: the old block becomes the lower half of a block one level deeper,
214# so every element keeps its index.
215def grown(~A: Data, +depth: Nat, arr: Array<Maybe<&2, A>>) -> Array<Maybe<&2, A>>:
216 ANode{arr, empty_slots(~A, depth)}
217
218def push_room(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +n: U32, +depth: Nat, +cap: U32, arr: Array<Maybe<&2, A>>, x: A, room: Bool) -> Heap<A>:
219 match room:
220 case True{}:
221 BH{1n+size, U32.inc(n), depth, cap, sift_up(~A, ~cmp, depth, n, x, arr)}
222 case False{}:
223 BH{1n+size, U32.inc(n), 1n+depth, U32.shl(cap), sift_up(~A, ~cmp, 1n+depth, n, x, grown(~A, depth, arr))}
224
225def push(~A: Data, ~cmp: A -> A -> Cmp, h: Heap<A>, x: A) -> Heap<A>:
226 BH{size, +n, +depth, +cap, arr} = h
227 push_room(~A, ~cmp, size, n, depth, cap, arr, x, U32.is_lt(n, cap))
228
229# ---- peek ----
230
231def peek_found(~A: Data, size: Nat, n: U32, depth: Nat, cap: U32, r: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Heap<A> & Result<&2, &2, E.Error, A>:
232 (arr, m) = r
233 (BH{size, n, depth, cap, arr}, item_of(~A, m))
234
235def peek_go(~A: Data, size: Nat, +n: U32, depth: Nat, cap: U32, arr: Array<Maybe<&2, A>>, empty: Bool) -> Heap<A> & Result<&2, &2, E.Error, A>:
236 match empty:
237 case True{}:
238 (BH{size, n, depth, cap, arr}, Fail{E.EmptyHeap{}})
239 case False{}:
240 peek_found(~A, size, n, depth, cap, Array.get(Maybe<&2, A>, arr, 0))
241
242def peek(~A: Data, h: Heap<A>) -> Heap<A> & Result<&2, &2, E.Error, A>:
243 BH{size, +n, depth, cap, arr} = h
244 peek_go(~A, size, n, depth, cap, arr, U32.is_eq(n, 0))
245
246# ---- pop ----
247
248# The last element has been taken out of slot m = n - 1; put it at the root
249# and sift it down over the remaining m elements.
250def pop_move(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +m: U32, +depth: Nat, cap: U32, root: A, last: A, arr: Array<Maybe<&2, A>>, empty: Bool) -> Heap<A> & Result<&2, &2, E.Error, A>:
251 match empty:
252 case True{}:
253 (BH{size, m, depth, cap, arr}, Done{root})
254 case False{}:
255 (BH{size, m, depth, cap, sift_down(~A, ~cmp, depth, m, 0, last, arr)}, Done{root})
256
257def pop_last(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +m: U32, depth: Nat, cap: U32, +root: A, rl: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Heap<A> & Result<&2, &2, E.Error, A>:
258 (arr, ml) = rl
259 pop_move(~A, ~cmp, size, m, depth, cap, root, slot_or(~A, root, ml), arr, U32.is_eq(m, 0))
260
261# The last element is READ, not cleared: the invariant says nothing about the
262# slots above the size, so clearing it would be one array write per pop that
263# the algorithm does not need (the C reference does not do it either).
264#
265# The root slot of a nonempty heap is Some; the None case cannot be reached
266# from a well-formed heap and returns the state unchanged.
267def pop_with(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +n: U32, depth: Nat, cap: U32, arr: Array<Maybe<&2, A>>, mr: Maybe<&2, A>) -> Heap<A> & Result<&2, &2, E.Error, A>:
268 match mr:
269 case None{}:
270 (BH{size, n, depth, cap, arr}, Fail{E.EmptyHeap{}})
271 case Some{+root}:
272 pop_last(~A, ~cmp, Nat.sub(size, 1n), U32.sub(n, 1), depth, cap, root, Array.get(Maybe<&2, A>, arr, U32.sub(n, 1)))
273
274def pop_root(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +n: U32, depth: Nat, cap: U32, rr: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Heap<A> & Result<&2, &2, E.Error, A>:
275 (arr, mr) = rr
276 pop_with(~A, ~cmp, size, n, depth, cap, arr, mr)
277
278def pop_go(~A: Data, ~cmp: A -> A -> Cmp, size: Nat, +n: U32, depth: Nat, cap: U32, arr: Array<Maybe<&2, A>>, empty: Bool) -> Heap<A> & Result<&2, &2, E.Error, A>:
279 match empty:
280 case True{}:
281 (BH{size, n, depth, cap, arr}, Fail{E.EmptyHeap{}})
282 case False{}:
283 pop_root(~A, ~cmp, size, n, depth, cap, Array.get(Maybe<&2, A>, arr, 0))
284
285def pop(~A: Data, ~cmp: A -> A -> Cmp, h: Heap<A>) -> Heap<A> & Result<&2, &2, E.Error, A>:
286 BH{size, +n, depth, cap, arr} = h
287 pop_go(~A, ~cmp, size, n, depth, cap, arr, U32.is_eq(n, 0))
288
289# ---- from_list ----
290
291def from_list_go(~A: Data, ~cmp: A -> A -> Cmp, xs: List<&2, A>, h: Heap<A>) -> Heap<A>:
292 match xs:
293 case Nil{}:
294 h
295 case Con{x, rest}:
296 from_list_go(~A, ~cmp, rest, push(~A, ~cmp, h, x))
297
298def from_list(~A: Data, ~cmp: A -> A -> Cmp, xs: List<&2, A>) -> Heap<A>:
299 from_list_go(~A, ~cmp, xs, new(~A))
300
301# ---- to_sorted_list ----
302
303# Repeated root removal on a COPY of the block: the heap itself is unchanged.
304# The loop carries its state for the same reason the sift loops do.
305# DrDone the copy is exhausted
306# DrLast the root was the last element
307# DrMore the root is out, `m` elements remain and `last` has to sift down
308
309type Drain<-A: Data> is Type:
310 DrDone{arr: Array<Maybe<&2, A>>}
311 DrLast{arr: Array<Maybe<&2, A>>, root: A}
312 DrMore{arr: Array<Maybe<&2, A>>, root: A, m: U32, last: A}
313
314# Dropping the (linear) block is O(1): the runtime erases it.
315def burn(~A: Data, arr: Array<Maybe<&2, A>>) -> List<&2, A>:
316 Nil{}
317
318def burn_cons(~A: Data, root: A, arr: Array<Maybe<&2, A>>) -> List<&2, A>:
319 Con{root, Nil{}}
320
321def drain_mb(~A: Data, arr: Array<Maybe<&2, A>>, root: A, +m: U32, ml: Maybe<&2, A>, empty: Bool) -> Drain<A>:
322 match ml empty:
323 case None{} _:
324 DrLast{arr, root}
325 case Some{last} True{}:
326 DrLast{arr, root}
327 case Some{last} False{}:
328 DrMore{arr, root, m, last}
329
330def drain_last(~A: Data, root: A, +m: U32, empty: Bool, rl: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Drain<A>:
331 (arr, ml) = rl
332 drain_mb(~A, arr, root, m, ml, empty)
333
334def drain_root(~A: Data, arr: Array<Maybe<&2, A>>, +m: U32, mr: Maybe<&2, A>) -> Drain<A>:
335 match mr:
336 case None{}:
337 DrDone{arr}
338 case Some{root}:
339 drain_last(~A, root, m, U32.is_eq(m, 0), Array.get(Maybe<&2, A>, arr, m))
340
341def drain_take(~A: Data, +m: U32, r: Array<Maybe<&2, A>> & Maybe<&2, A>) -> Drain<A>:
342 (arr, mr) = r
343 drain_root(~A, arr, m, mr)
344
345# Take the root out of a copy holding `n` elements. Emptiness is decided by
346# the count, not by reading slot 0: the drain must stop at `n = 0` whatever
347# the slots above the heap hold (and it saves one array read per element).
348def drain_take_go(~A: Data, +n: U32, arr: Array<Maybe<&2, A>>, empty: Bool) -> Drain<A>:
349 match empty:
350 case True{}:
351 DrDone{arr}
352 case False{}:
353 drain_take(~A, U32.sub(n, 1), Array.get(Maybe<&2, A>, arr, 0))
354
355def drain_probe(~A: Data, +n: U32, arr: Array<Maybe<&2, A>>) -> Drain<A>:
356 drain_take_go(~A, n, arr, U32.is_eq(n, 0))
357
358def drain_go(~A: Data, ~cmp: A -> A -> Cmp, fuel: Nat, +depth: Nat, st: Drain<A>) -> List<&2, A>:
359 match fuel st:
360 case _ DrDone{arr}:
361 burn(~A, arr)
362 case _ DrLast{arr, root}:
363 burn_cons(~A, root, arr)
364 case 0n DrMore{arr, root, m, last}:
365 burn_cons(~A, root, arr)
366 case 1n+f DrMore{arr, root, +m, last}:
367 Con{root, drain_go(~A, ~cmp, f, depth, drain_probe(~A, m, sift_down(~A, ~cmp, depth, m, 0, last, arr)))}
368
369def sorted_of(~A: Data, ~cmp: A -> A -> Cmp, +size: Nat, +n: U32, +depth: Nat, cap: U32, c: Array<Maybe<&2, A>> & Array<Maybe<&2, A>>) -> Heap<A> & List<&2, A>:
370 (arr, copy) = c
371 (BH{size, n, depth, cap, arr}, drain_go(~A, ~cmp, size, depth, drain_probe(~A, n, copy)))
372
373def to_sorted_list(~A: Data, ~cmp: A -> A -> Cmp, h: Heap<A>) -> Heap<A> & List<&2, A>:
374 BH{+size, +n, +depth, +cap, arr} = h
375 sorted_of(~A, ~cmp, size, n, depth, cap, Array.clone(Maybe<&2, A>, arr))
376
377# ---- operation traces ----
378
379def obs_nat(~A: Data, r: Heap<A> & Nat) -> Heap<A> & E.Obs<A>:
380 (h, n) = r
381 (h, E.ONat{n})
382
383def obs_item(~A: Data, r: Heap<A> & Result<&2, &2, E.Error, A>) -> Heap<A> & E.Obs<A>:
384 (h, x) = r
385 (h, E.OItem{x})
386
387def obs_list(~A: Data, r: Heap<A> & List<&2, A>) -> Heap<A> & E.Obs<A>:
388 (h, xs) = r
389 (h, E.OList{xs})
390
391def drop_heap(~A: Data, h: Heap<A>, v: Heap<A> & E.Obs<A>) -> Heap<A> & E.Obs<A>:
392 v
393
394# FromList replaces the heap: the old block is dropped (O(1) erasure).
395def replace(~A: Data, ~cmp: A -> A -> Cmp, h: Heap<A>, xs: List<&2, A>) -> Heap<A> & E.Obs<A>:
396 BH{size, n, depth, cap, arr} = h
397 (from_list(~A, ~cmp, xs), E.OUnit{})
398
399def step(~A: Data, ~cmp: A -> A -> Cmp, h: Heap<A>, op: E.Op<A>) -> Heap<A> & E.Obs<A>:
400 match op:
401 case E.Length{}:
402 obs_nat(~A, length(~A, h))
403 case E.Push{x}:
404 (push(~A, ~cmp, h, x), E.OUnit{})
405 case E.Peek{}:
406 obs_item(~A, peek(~A, h))
407 case E.Pop{}:
408 obs_item(~A, pop(~A, ~cmp, h))
409 case E.FromList{xs}:
410 replace(~A, ~cmp, h, xs)
411 case E.ToSortedList{}:
412 obs_list(~A, to_sorted_list(~A, ~cmp, h))
413
414def record(~A: Data, acc: List<&2, E.Obs<A>>, r: Heap<A> & E.Obs<A>) -> Heap<A> & List<&2, E.Obs<A>>:
415 (h, o) = r
416 (h, Con{o, acc})
417
418def step_acc(~A: Data, ~cmp: A -> A -> Cmp, op: E.Op<A>, st: Heap<A> & List<&2, E.Obs<A>>) -> Heap<A> & List<&2, E.Obs<A>>:
419 (h, acc) = st
420 record(~A, acc, step(~A, ~cmp, h, op))
421
422def run_acc(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op<A>>, st: Heap<A> & List<&2, E.Obs<A>>) -> Heap<A> & List<&2, E.Obs<A>>:
423 match ops:
424 case Nil{}:
425 st
426 case Con{op, rest}:
427 run_acc(~A, ~cmp, rest, step_acc(~A, ~cmp, op, st))
428
429def finish(~A: Data, st: Heap<A> & List<&2, E.Obs<A>>) -> Heap<A> & List<&2, E.Obs<A>>:
430 (h, acc) = st
431 (h, List.reverse(&2, E.Obs<A>, acc))
432
433def run(~A: Data, ~cmp: A -> A -> Cmp, ops: List<&2, E.Op<A>>, h: Heap<A>) -> Heap<A> & List<&2, E.Obs<A>>:
434 finish(~A, run_acc(~A, ~cmp, ops, (h, Nil{})))
435
436# ---- checked instances (proofs/binary_heap.bend) ----
437
438def run_u32(ops: List<&2, E.Op<U32>>, h: Heap<U32>) -> Heap<U32> & List<&2, E.Obs<U32>>:
439 run(~U32, ~U32.cmp, ops, h)
440
441def run_string(ops: List<&2, E.Op<String>>, h: Heap<String>) -> Heap<String> & List<&2, E.Obs<String>>:
442 run(~String, ~String.order, ops, h)