def rhs.wb

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

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

1343# Rotations toward hi, after lo grew or hi shrank by one.
1344def rhs.wb(
1345  -K: Data, -V: Data, +k: K, +v: V, +lk: K, +lv: V, +ll: O.OMap<K, V>,
1346  +lh: O.OMap<K, V>, +hi: O.OMap<K, V>,
1347  +wbl: {WB(K, V, O.OBin{0, lk, lv, ll, lh}) == True{} : Bool},
1348  wbh: {WB(K, V, hi) == True{} : Bool},
1349  +heavy: Ord.LE(1n+Nat.mul(3n, W(K, V, hi)), Nat.add(W(K, V, ll), W(K, V, lh))),
1350  +alm: Ord.LE(Nat.add(W(K, V, ll), W(K, V, lh)), Nat.add(3n, Nat.mul(3n, W(K, V, hi)))),
1351  +hs: Ord.LE(1n+W(K, V, lh), Nat.mul(2n, W(K, V, ll)))
1352) -> {WB(K, V, O.OMap.bin(K, V, lk, lv, ll, O.OMap.bin(K, V, k, v, lh, hi))) == True{} : Bool}:
1353  +l = W(K, V, hi)
1354  +a = W(K, V, lh)
1355  +b = W(K, V, ll)
1356  +okl = wb.ok(K, V, lk, lv, ll, lh, wbl)
1357  +h1 = Ord.wok_l(b, a, okl)
1358  +h2 = Ord.wok_r(b, a, okl)
1359  +pl = w_pos(K, V, hi)
1360  +pa = w_pos(K, V, lh)
1361  +pb = w_pos(K, V, ll)
1362  wb.i(K, V, lk, lv, ll, O.OMap.bin(K, V, k, v, lh, hi),
1363    Ord.rhs.w0(l, a, b, h1, h2, heavy, alm, hs, pl, pa, pb),
1364    wb.l(K, V, lk, lv, ll, lh, wbl),
1365    wb.i(K, V, k, v, lh, hi, Ord.rhs.w1(l, a, b, h1, h2, heavy, alm, hs, pl, pa, pb),
1366      wb.h(K, V, lk, lv, ll, lh, wbl), wbh))