def h.sz_del_hit

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

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

3601def h.sz_del_hit(
3602  ~K: Data, ~V: Data, ~eq: K -> K -> Bool, n: Nat, +mask: U32, m: M.HMap<K, V>, +hk: U32, +k: K, -w: V,
3603  hit: {h.G(~K, ~V, ~eq, n, mask, m, hk, k) == Some{w} : Maybe<&2, V>}
3604) -> {1n+h.Sz(K, V, h.D(~K, ~V, ~eq, n, mask, m, hk, k)) == h.Sz(K, V, m) : Nat}:
3605  match n:
3606    case 0n:
3607      match m:
3608        case M.HNil{}:
3609          h.none_some({1n == 0n : Nat}, V, w, hit)
3610        case M.HLeaf{+o, +es}:
3611          %h.size_leaf(K, V, o, M.HMap.entries.del(~K, ~V, ~eq, es, k)) : {1n+_ == h.len(K, V, es) : Nat}
3612          h.elen_del_hit(~K, ~V, ~eq, es, k, w, hit)
3613        case M.HBranch{+lo, +hi}:
3614          h.none_some({1n+h.Sz(K, V, M.HBranch{lo, hi}) == h.Sz(K, V, M.HBranch{lo, hi}) : Nat}, V, w, hit)
3615    case 1n+(+p):
3616      match m:
3617        case M.HNil{}:
3618          h.none_some({1n == 0n : Nat}, V, w, hit)
3619        case M.HLeaf{+o, +es}:
3620          h.sz_del_hit.lf(~K, ~V, ~eq, o, es, hk, k, w, U32.is_eq(o, hk), {==}, hit)
3621        case M.HBranch{+lo, +hi}:
3622          h.sz_del_hit.br(~K, ~V, ~eq, p, mask, lo, hi, hk, k, w, U32.is_eq((hk .&. mask : U32), 0), {==}, hit,
3623            e => h.sz_del_hit(~K, ~V, ~eq, p, (mask << 1n : U32), lo, hk, k, w, e),
3624            e => h.sz_del_hit(~K, ~V, ~eq, p, (mask << 1n : U32), hi, hk, k, w, e))