def h.split_other.b

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

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

3068def h.split_other.b(
3069  ~K: Data, ~V: Data, ~hash: K -> U32, ~eq: K -> K -> Bool,
3070  ~sound: @x: K -> @y: K -> {eq(x, y) == True{} : Bool} -> {x == y : K},
3071  +p: Nat, +mask: U32, +o: U32, +es: List<&2, M.Entry<K, V>>, +h2: U32, +k2: K, +k: K, +v: V,
3072  +hs: {Laws.hmap_hashed(~K, ~V, ~hash, es, o) == True{} : Bool},
3073  +nk: {eq(k, k2) == False{} : Bool},
3074  b1: Bool, b2: Bool,
3075  e2: {b2 == U32.is_eq((o .&. mask : U32), 0) : Bool},
3076  ih: {h.G(~K, ~V, ~eq, p, (mask << 1n : U32), h.S(~K, ~V, ~eq, p, (mask << 1n : U32), o, es, h2, k2, v), hash(k), k)
3077       == h.R(~K, ~V, ~hash, ~eq, o, es, k) : Maybe<&2, V>}
3078) -> {h.G(~K, ~V, ~eq, 1n+p, mask, h.sp(~K, ~V, ~eq, b1, b2, p, mask, o, es, h2, k2, v), hash(k), k)
3079      == h.R(~K, ~V, ~hash, ~eq, o, es, k) : Maybe<&2, V>}:
3080  match b1 b2:
3081    case True{} True{}:
3082      +mm = (mask << 1n : U32)
3083      +d = U32.is_eq((hash(k) .&. mask : U32), 0)
3084      +sub = h.S(~K, ~V, ~eq, p, mm, o, es, h2, k2, v)
3085      +old = {M.HLeaf{o, es} : M.HMap<K, V>}
3086      +fresh = {M.HLeaf{h2, [M.Entry{k2, v}]} : M.HMap<K, V>}
3087      +r = h.R(~K, ~V, ~hash, ~eq, o, es, k)
3088      h.bsel(Maybe<&2, V>, d, h.G(~K, ~V, ~eq, p, mm, sub, hash(k), k),
3089        h.G(~K, ~V, ~eq, p, mm, M.HNil{}, hash(k), k), r,
3090        ed => ih,
3091        ed => Equal.trans(Maybe<&2, V>, h.G(~K, ~V, ~eq, p, mm, M.HNil{}, hash(k), k), None{}, r,
3092          h.gnil(~K, ~V, ~eq, p, mm, hash(k), k),
3093          h.r_none(~K, ~V, ~hash, ~eq, o, es, k,
3094            h.u_diff(o, hash(k), mask, True{}, h.sb(True{}, U32.is_eq((o .&. mask : U32), 0), e2), ed))))
3095    case True{} False{}:
3096      +mm = (mask << 1n : U32)
3097      +d = U32.is_eq((hash(k) .&. mask : U32), 0)
3098      +sub = h.S(~K, ~V, ~eq, p, mm, o, es, h2, k2, v)
3099      +old = {M.HLeaf{o, es} : M.HMap<K, V>}
3100      +fresh = {M.HLeaf{h2, [M.Entry{k2, v}]} : M.HMap<K, V>}
3101      +r = h.R(~K, ~V, ~hash, ~eq, o, es, k)
3102      h.bsel(Maybe<&2, V>, d, h.G(~K, ~V, ~eq, p, mm, M.HNil{}, hash(k), k),
3103        h.G(~K, ~V, ~eq, p, mm, sub, hash(k), k), r,
3104        ed => Equal.trans(Maybe<&2, V>, h.G(~K, ~V, ~eq, p, mm, M.HNil{}, hash(k), k), None{}, r,
3105          h.gnil(~K, ~V, ~eq, p, mm, hash(k), k),
3106          h.r_none(~K, ~V, ~hash, ~eq, o, es, k,
3107            h.u_diff(o, hash(k), mask, False{}, h.sb(False{}, U32.is_eq((o .&. mask : U32), 0), e2), ed))),
3108        ed => ih)
3109    case False{} True{}:
3110      +mm = (mask << 1n : U32)
3111      +d = U32.is_eq((hash(k) .&. mask : U32), 0)
3112      +sub = h.S(~K, ~V, ~eq, p, mm, o, es, h2, k2, v)
3113      +old = {M.HLeaf{o, es} : M.HMap<K, V>}
3114      +fresh = {M.HLeaf{h2, [M.Entry{k2, v}]} : M.HMap<K, V>}
3115      +r = h.R(~K, ~V, ~hash, ~eq, o, es, k)
3116      h.bsel(Maybe<&2, V>, d, h.G(~K, ~V, ~eq, p, mm, old, hash(k), k),
3117        h.G(~K, ~V, ~eq, p, mm, fresh, hash(k), k), r,
3118        ed => h.g_leaf_r(~K, ~V, ~hash, ~eq, ~sound, p, mm, o, es, k, hs),
3119        ed => Equal.trans(Maybe<&2, V>, h.G(~K, ~V, ~eq, p, mm, fresh, hash(k), k), None{}, r,
3120          h.g_fresh_none(~K, ~V, ~eq, ~sound, p, mm, h2, k2, hash(k), k, v, nk),
3121          h.r_none(~K, ~V, ~hash, ~eq, o, es, k,
3122            h.u_diff(o, hash(k), mask, True{}, h.sb(True{}, U32.is_eq((o .&. mask : U32), 0), e2), ed))))
3123    case False{} False{}:
3124      +mm = (mask << 1n : U32)
3125      +d = U32.is_eq((hash(k) .&. mask : U32), 0)
3126      +sub = h.S(~K, ~V, ~eq, p, mm, o, es, h2, k2, v)
3127      +old = {M.HLeaf{o, es} : M.HMap<K, V>}
3128      +fresh = {M.HLeaf{h2, [M.Entry{k2, v}]} : M.HMap<K, V>}
3129      +r = h.R(~K, ~V, ~hash, ~eq, o, es, k)
3130      h.bsel(Maybe<&2, V>, d, h.G(~K, ~V, ~eq, p, mm, fresh, hash(k), k),
3131        h.G(~K, ~V, ~eq, p, mm, old, hash(k), k), r,
3132        ed => Equal.trans(Maybe<&2, V>, h.G(~K, ~V, ~eq, p, mm, fresh, hash(k), k), None{}, r,
3133          h.g_fresh_none(~K, ~V, ~eq, ~sound, p, mm, h2, k2, hash(k), k, v, nk),
3134          h.r_none(~K, ~V, ~hash, ~eq, o, es, k,
3135            h.u_diff(o, hash(k), mask, False{}, h.sb(False{}, U32.is_eq((o .&. mask : U32), 0), e2), ed))),
3136        ed => h.g_leaf_r(~K, ~V, ~hash, ~eq, ~sound, p, mm, o, es, k, hs))