def h.gd_same.br

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

import Base
import bend-kit-collections@0.1.4.1/hmap.bend as M

3241def h.gd_same.br(
3242  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, +p: Nat, +mask: U32, +lo: M.HMap<K, V>,
3243  +hi: M.HMap<K, V>, +hk: U32, +k: K, b: Bool, eb: {b == U32.is_eq((hk .&. mask : U32), 0) : Bool},
3244  il: {h.G(~K, ~V, ~eq, p, (mask << 1n : U32), h.D(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k), hk, k) == None{} : Maybe<&2, V>},
3245  ih: {h.G(~K, ~V, ~eq, p, (mask << 1n : U32), h.D(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k), hk, k) == None{} : Maybe<&2, V>}
3246) -> {h.G(~K, ~V, ~eq, 1n+p, mask, h.db(~K, ~V, ~eq, b, p, mask, lo, hi, hk, k), hk, k) == None{} : Maybe<&2, V>}:
3247  match b:
3248    case True{}:
3249      +dlo = h.D(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k)
3250      +dhi = h.D(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)
3251      %h.get_join(~K, ~V, ~eq, p, mask, dlo, hi, hk, k) : {_ == None{} : Maybe<&2, V>}
3252      %h.g_lo(~K, ~V, ~eq, p, mask, dlo, hi, hk, k, h.sb(True{}, U32.is_eq((hk .&. mask : U32), 0), eb))
3253        : {_ == None{} : Maybe<&2, V>}
3254      il
3255    case False{}:
3256      +dlo = h.D(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k)
3257      +dhi = h.D(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k)
3258      %h.get_join(~K, ~V, ~eq, p, mask, lo, dhi, hk, k) : {_ == None{} : Maybe<&2, V>}
3259      %h.g_hi(~K, ~V, ~eq, p, mask, lo, dhi, hk, k, h.sb(False{}, U32.is_eq((hk .&. mask : U32), 0), eb))
3260        : {_ == None{} : Maybe<&2, V>}
3261      ih