def rls.wb

bend-kit-collections@0.1.4.1 · PROOF.bend:1252

import Base
import bend-kit-collections@0.1.4.1/omap.bend as O
import bend-kit-collections@0.1.4.1/nat_order.bend as Ord

1252# Rotations toward lo, after hi grew or lo shrank by one.
1253def rls.wb(
1254  -K: Data, -V: Data, +k: K, +v: V, +lo: O.OMap<K, V>, +hk: K, +hv: V,
1255  +hl: O.OMap<K, V>, +hh: O.OMap<K, V>,
1256  wbl: {WB(K, V, lo) == True{} : Bool},
1257  +wbh: {WB(K, V, O.OBin{0, hk, hv, hl, hh}) == True{} : Bool},
1258  +heavy: Ord.LE(1n+Nat.mul(3n, W(K, V, lo)), Nat.add(W(K, V, hl), W(K, V, hh))),
1259  +alm: Ord.LE(Nat.add(W(K, V, hl), W(K, V, hh)), Nat.add(3n, Nat.mul(3n, W(K, V, lo)))),
1260  +hs: Ord.LE(1n+W(K, V, hl), Nat.mul(2n, W(K, V, hh)))
1261) -> {WB(K, V, O.OMap.bin(K, V, hk, hv, O.OMap.bin(K, V, k, v, lo, hl), hh)) == True{} : Bool}:
1262  +l = W(K, V, lo)
1263  +a = W(K, V, hl)
1264  +b = W(K, V, hh)
1265  +okh = wb.ok(K, V, hk, hv, hl, hh, wbh)
1266  +h1 = Ord.wok_r(a, b, okh)
1267  +h2 = Ord.wok_l(a, b, okh)
1268  +pl = w_pos(K, V, lo)
1269  +pa = w_pos(K, V, hl)
1270  +pb = w_pos(K, V, hh)
1271  wb.i(K, V, hk, hv, O.OMap.bin(K, V, k, v, lo, hl), hh,
1272    Ord.rls.w1(l, a, b, h1, h2, heavy, alm, hs, pl, pa, pb),
1273    wb.i(K, V, k, v, lo, hl, Ord.rls.w0(l, a, b, h1, h2, heavy, alm, hs, pl, pa, pb), wbl,
1274      wb.l(K, V, hk, hv, hl, hh, wbh)),
1275    wb.h(K, V, hk, hv, hl, hh, wbh))