1 import Base 2 import bend-mathlib@0.7.4.0/nat.bend as MNat 3 import bend-mathlib@0.7.4.0/bool.bend as MBool 4 import ./LAWS.bend as Laws 5 import ./omap.bend as O 6 import ./hmap.bend as M 7 import ./nat_order.bend as Ord 8 import ./order.bend as Order 9 import bend-kit-lemmas@0.1.1.0/lemmas.bend as Lemmas 10 11 def Laws.omap_keys_ascending_puts(): 12 {==} 13 14 def Laws.omap_size_del(): 15 {==} 16 17 def Laws.omap_get_after_rotations(): 18 {==} 19 20 def Laws.omap_keys_del_root(): 21 {==} 22 23 def Laws.omap_get_put(): 24 {==} 25 26 def Laws.omap_get_put_replace(): 27 {==} 28 29 def Laws.omap_get_put_other(): 30 {==} 31 32 def Laws.omap_get_missing(): 33 {==} 34 35 def Laws.omap_keys_sorted(): 36 {==} 37 38 def Laws.omap_size_replace(): 39 {==} 40 41 def Laws.omap_get_del(): 42 {==} 43 44 def Laws.omap_get_del_other(): 45 {==} 46 47 def Laws.omap_keys_del(): 48 {==} 49 50 def Laws.omap_string_keys(): 51 {==} 52 53 def Laws.oset_to_list(): 54 {==} 55 56 def Laws.oset_has_del(): 57 {==} 58 59 def Laws.vec_from_list(): 60 {==} 61 62 def Laws.vec_get(): 63 {==} 64 65 def Laws.vec_get_past_len(): 66 {==} 67 68 def Laws.vec_set(): 69 {==} 70 71 def Laws.vec_pop(): 72 {==} 73 74 def Laws.vec_pop_empty(): 75 {==} 76 77 def Laws.vec_pop_to_list(): 78 {==} 79 80 def Laws.deque_ends(): 81 {==} 82 83 def Laws.heap_sort(): 84 {==} 85 86 def c4.a( 87 +a: Bool, +b: Bool, +c: Bool, +d: Bool, 88 e: {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool} 89 ) -> {a == True{} : Bool}: 90 MBool.eq_true_of_and_left(a, b, MBool.eq_true_of_and_left(Bool.and(a, b), c, MBool.eq_true_of_and_left(Bool.and(Bool.and(a, b), c), d, e))) 91 92 def c4.b( 93 +a: Bool, +b: Bool, +c: Bool, +d: Bool, 94 e: {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool} 95 ) -> {b == True{} : Bool}: 96 MBool.eq_true_of_and_right(a, b, MBool.eq_true_of_and_left(Bool.and(a, b), c, MBool.eq_true_of_and_left(Bool.and(Bool.and(a, b), c), d, e))) 97 98 def c4.c( 99 +a: Bool, +b: Bool, +c: Bool, +d: Bool, 100 e: {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool} 101 ) -> {c == True{} : Bool}: 102 MBool.eq_true_of_and_right(Bool.and(a, b), c, MBool.eq_true_of_and_left(Bool.and(Bool.and(a, b), c), d, e)) 103 104 def c4.d( 105 +a: Bool, +b: Bool, +c: Bool, +d: Bool, 106 e: {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool} 107 ) -> {d == True{} : Bool}: 108 MBool.eq_true_of_and_right(Bool.and(Bool.and(a, b), c), d, e) 109 110 def c4.i( 111 +a: Bool, +b: Bool, +c: Bool, +d: Bool, ea: {a == True{} : Bool}, 112 eb: {b == True{} : Bool}, ec: {c == True{} : Bool}, ed: {d == True{} : Bool} 113 ) -> {Bool.and(Bool.and(Bool.and(a, b), c), d) == True{} : Bool}: 114 MBool.and_eq_true(Bool.and(Bool.and(a, b), c), d, MBool.and_eq_true(Bool.and(a, b), c, MBool.and_eq_true(a, b, ea, eb), ec), ed) 115 116 117 def c3.a(+a: Bool, +b: Bool, +c: Bool, e: {Bool.and(Bool.and(a, b), c) == True{} : Bool}) -> {a == True{} : Bool}: 118 MBool.eq_true_of_and_left(a, b, MBool.eq_true_of_and_left(Bool.and(a, b), c, e)) 119 120 def c3.b(+a: Bool, +b: Bool, +c: Bool, e: {Bool.and(Bool.and(a, b), c) == True{} : Bool}) -> {b == True{} : Bool}: 121 MBool.eq_true_of_and_right(a, b, MBool.eq_true_of_and_left(Bool.and(a, b), c, e)) 122 123 def c3.c(+a: Bool, +b: Bool, +c: Bool, e: {Bool.and(Bool.and(a, b), c) == True{} : Bool}) -> {c == True{} : Bool}: 124 MBool.eq_true_of_and_right(Bool.and(a, b), c, e) 125 126 def c3.i(+a: Bool, +b: Bool, +c: Bool, ea: {a == True{} : Bool}, eb: {b == True{} : Bool}, ec: {c == True{} : Bool}) 127 -> {Bool.and(Bool.and(a, b), c) == True{} : Bool}: 128 MBool.and_eq_true(Bool.and(a, b), c, MBool.and_eq_true(a, b, ea, eb), ec) 129 130 def Laws.omap_new_searchtree(K, V, cmp): 131 {==} 132 133 def head(-K: Data, xs: List<&2, K>) -> Maybe<&2, K>: 134 match xs: 135 case Nil{}: 136 None{} 137 case Con{h, t}: 138 Some{h} 139 140 # The list is sorted and its first element lies above lb. 141 def sfrom(~K: Data, ~cmp: K -> K -> Cmp, lb: Maybe<&2, K>, xs: List<&2, K>) -> Bool: 142 match lb: 143 case None{}: 144 Laws.sorted(~K, ~cmp, xs) 145 case Some{b}: 146 Laws.sorted.go(~K, ~cmp, xs, b) 147 148 # lb lies below ub, when both exist. 149 def lt_m(~K: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, ub: Maybe<&2, K>) -> Bool: 150 match ub: 151 case None{}: 152 True{} 153 case Some{u}: 154 Laws.above(~K, ~cmp, lb, u) 155 156 def lt_m.some( 157 ~K: Data, ~cmp: K -> K -> Cmp, ub: Maybe<&2, K>, +k: K, 158 e: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool} 159 ) -> {lt_m(~K, ~cmp, Some{k}, ub) == True{} : Bool}: 160 match ub: 161 case None{}: 162 {==} 163 case Some{u}: 164 e 165 166 def sfrom.base( 167 ~K: Data, ~cmp: K -> K -> Cmp, lb: Maybe<&2, K>, acc: List<&2, K>, 168 lt: {lt_m(~K, ~cmp, lb, head(K, acc)) == True{} : Bool}, 169 sa: {Laws.sorted(~K, ~cmp, acc) == True{} : Bool} 170 ) -> {sfrom(~K, ~cmp, lb, acc) == True{} : Bool}: 171 match lb acc: 172 case None{} _: 173 sa 174 case Some{b} Nil{}: 175 {==} 176 case Some{+b} Con{+h, t}: 177 MBool.and_eq_true(Cmp.is_lt(cmp(b, h)), Laws.sorted.go(~K, ~cmp, t, h), lt, sa) 178 179 def keys_sorted.go( 180 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, t: O.OMap, +lb: Maybe<&2, K>, 181 +acc: List<&2, K>, 182 +bt: {Laws.bounded(~K, ~V, ~cmp, t, lb, head(K, acc)) == True{} : Bool}, 183 lt: {lt_m(~K, ~cmp, lb, head(K, acc)) == True{} : Bool}, 184 sa: {Laws.sorted(~K, ~cmp, acc) == True{} : Bool} 185 ) -> {sfrom(~K, ~cmp, lb, O.OMap.keys.go(K, V, t, acc)) == True{} : Bool}: 186 match t: 187 case O.OTip{}: 188 sfrom.base(~K, ~cmp, lb, acc, lt, sa) 189 case O.OBin{s, +k, v, +lo, +hi}: 190 +A = Laws.above(~K, ~cmp, lb, k) 191 +B = Laws.below(~K, ~cmp, head(K, acc), k) 192 +L = Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) 193 +H = Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, head(K, acc)) 194 ih = keys_sorted.go(~K, ~V, ~cmp, hi, Some{k}, acc, c4.d(A, B, L, H, bt), 195 lt_m.some(~K, ~cmp, head(K, acc), k, c4.b(A, B, L, H, bt)), sa) 196 keys_sorted.go(~K, ~V, ~cmp, lo, lb, k <> O.OMap.keys.go(K, V, hi, acc), 197 c4.c(A, B, L, H, bt), c4.a(A, B, L, H, bt), ih) 198 199 def Laws.omap_searchtree_keys_sorted(K, V, cmp, m, tree): 200 keys_sorted.go(~K, ~V, ~cmp, m, None{}, Nil{}, tree, {==}, {==}) 201 202 def Trans(~K: Data, ~cmp: K -> K -> Cmp) -> Type: 203 @x: K -> @y: K -> @z: K -> {cmp(x, y) == LT{} : Cmp} -> {cmp(y, z) == LT{} : Cmp} -> {cmp(x, z) == LT{} : Cmp} 204 205 def Flip(~K: Data, ~cmp: K -> K -> Cmp) -> Type: 206 @x: K -> @y: K -> {cmp(y, x) == Laws.flip(cmp(x, y)) : Cmp} 207 208 def Refl(~K: Data, ~cmp: K -> K -> Cmp) -> Type: 209 @x: K -> {cmp(x, x) == EQ{} : Cmp} 210 211 def Eq(~K: Data, ~cmp: K -> K -> Cmp) -> Type: 212 @x: K -> @y: K -> {cmp(x, y) == EQ{} : Cmp} -> {x == y : K} 213 214 def lt_of(c: Cmp, e: {Cmp.is_lt(c) == True{} : Bool}) -> {c == LT{} : Cmp}: 215 match c: 216 case LT{}: 217 {==} 218 case EQ{}: 219 Empty.absurd({EQ{} == LT{} : Cmp}, MBool.false_ne_true()(e)) 220 case GT{}: 221 Empty.absurd({GT{} == LT{} : Cmp}, MBool.false_ne_true()(e)) 222 223 def lt_true(-c: Cmp, e: {c == LT{} : Cmp}) -> {Cmp.is_lt(c) == True{} : Bool}: 224 Equal.cong(Cmp, Bool, x => Cmp.is_lt(x), c, LT{}, e) 225 226 def gt_flip( 227 ~K: Data, ~cmp: K -> K -> Cmp, ~flip: Flip(~K, ~cmp), +x: K, +y: K, 228 e: {cmp(x, y) == GT{} : Cmp} 229 ) -> {cmp(y, x) == LT{} : Cmp}: 230 Equal.trans(Cmp, cmp(y, x), Laws.flip(cmp(x, y)), LT{}, flip(x, y), 231 Equal.cong(Cmp, Cmp, c => Laws.flip(c), cmp(x, y), GT{}, e)) 232 233 def lt_trans( 234 ~K: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), +x: K, +y: K, +z: K, 235 e1: {Cmp.is_lt(cmp(x, y)) == True{} : Bool}, 236 e2: {Cmp.is_lt(cmp(y, z)) == True{} : Bool} 237 ) -> {Cmp.is_lt(cmp(x, z)) == True{} : Bool}: 238 lt_true(cmp(x, z), trans(x, y, z, lt_of(cmp(x, y), e1), lt_of(cmp(y, z), e2))) 239 240 def above_trans( 241 ~K: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), lb: Maybe<&2, K>, 242 +k: K, +hk: K, ea: {Laws.above(~K, ~cmp, lb, k) == True{} : Bool}, 243 e: {Cmp.is_lt(cmp(k, hk)) == True{} : Bool} 244 ) -> {Laws.above(~K, ~cmp, lb, hk) == True{} : Bool}: 245 match lb: 246 case None{}: 247 {==} 248 case Some{+b}: 249 lt_trans(~K, ~cmp, ~trans, b, k, hk, ea, e) 250 251 def below_trans( 252 ~K: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), ub: Maybe<&2, K>, 253 +k: K, +hk: K, e: {Cmp.is_lt(cmp(k, hk)) == True{} : Bool}, 254 eb: {Laws.below(~K, ~cmp, ub, hk) == True{} : Bool} 255 ) -> {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}: 256 match ub: 257 case None{}: 258 {==} 259 case Some{+u}: 260 lt_trans(~K, ~cmp, ~trans, k, hk, u, e, eb) 261 262 # Projections and introduction for bounded on one node. 263 def bn.a( 264 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, 265 +k: K, -v: V, +lo: O.OMap, +hi: O.OMap, 266 e: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, lb, ub) == True{} : Bool} 267 ) -> {Laws.above(~K, ~cmp, lb, k) == True{} : Bool}: 268 c4.a(Laws.above(~K, ~cmp, lb, k), Laws.below(~K, ~cmp, ub, k), 269 Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}), 270 Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub), e) 271 272 def bn.b( 273 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, 274 +k: K, -v: V, +lo: O.OMap, +hi: O.OMap, 275 e: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, lb, ub) == True{} : Bool} 276 ) -> {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}: 277 c4.b(Laws.above(~K, ~cmp, lb, k), Laws.below(~K, ~cmp, ub, k), 278 Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}), 279 Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub), e) 280 281 def bn.l( 282 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, 283 +k: K, -v: V, +lo: O.OMap, +hi: O.OMap, 284 e: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, lb, ub) == True{} : Bool} 285 ) -> {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) == True{} : Bool}: 286 c4.c(Laws.above(~K, ~cmp, lb, k), Laws.below(~K, ~cmp, ub, k), 287 Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}), 288 Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub), e) 289 290 def bn.h( 291 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, 292 +k: K, -v: V, +lo: O.OMap, +hi: O.OMap, 293 e: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, lb, ub) == True{} : Bool} 294 ) -> {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool}: 295 c4.d(Laws.above(~K, ~cmp, lb, k), Laws.below(~K, ~cmp, ub, k), 296 Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}), 297 Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub), e) 298 299 def bn.i( 300 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, 301 +k: K, -v: V, +lo: O.OMap, +hi: O.OMap, 302 ea: {Laws.above(~K, ~cmp, lb, k) == True{} : Bool}, 303 eb: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}, 304 el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) == True{} : Bool}, 305 eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool} 306 ) -> {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, lb, ub) == True{} : Bool}: 307 c4.i(Laws.above(~K, ~cmp, lb, k), Laws.below(~K, ~cmp, ub, k), 308 Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}), 309 Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub), ea, eb, el, eh) 310 311 def rot_lo.single.bnd( 312 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 313 +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, +v: V, +lo: O.OMap, 314 +hk: K, +hv: V, +hl: O.OMap, +hh: O.OMap, 315 +ea: {Laws.above(~K, ~cmp, lb, k) == True{} : Bool}, 316 el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) == True{} : Bool}, 317 +eh: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, hk, hv, hl, hh}, Some{k}, ub) == True{} : Bool} 318 ) -> {Laws.bounded(~K, ~V, ~cmp, 319 O.OMap.bin(K, V, hk, hv, O.OMap.bin(K, V, k, v, lo, hl), hh), lb, ub) == True{} : Bool}: 320 +h_a = bn.a(~K, ~V, ~cmp, Some{k}, ub, hk, hv, hl, hh, eh) 321 bn.i(~K, ~V, ~cmp, lb, ub, hk, hv, O.OMap.bin(K, V, k, v, lo, hl), hh, 322 above_trans(~K, ~cmp, ~trans, lb, k, hk, ea, h_a), 323 bn.b(~K, ~V, ~cmp, Some{k}, ub, hk, hv, hl, hh, eh), 324 bn.i(~K, ~V, ~cmp, lb, Some{hk}, k, v, lo, hl, ea, h_a, el, 325 bn.l(~K, ~V, ~cmp, Some{k}, ub, hk, hv, hl, hh, eh)), 326 bn.h(~K, ~V, ~cmp, Some{k}, ub, hk, hv, hl, hh, eh)) 327 328 def rot_lo.double.bnd( 329 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 330 hl: O.OMap, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, +v: V, 331 +lo: O.OMap, +hk: K, +hv: V, +hh: O.OMap, 332 +ea: {Laws.above(~K, ~cmp, lb, k) == True{} : Bool}, 333 el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) == True{} : Bool}, 334 +eh: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, hk, hv, hl, hh}, Some{k}, ub) == True{} : Bool} 335 ) -> {Laws.bounded(~K, ~V, ~cmp, 336 O.OMap.rot_lo.double(K, V, k, v, lo, hk, hv, hl, hh), lb, ub) == True{} : Bool}: 337 match hl: 338 case O.OTip{}: 339 rot_lo.single.bnd(~K, ~V, ~cmp, ~trans, lb, ub, k, v, lo, hk, hv, O.OTip{}, hh, 340 ea, el, eh) 341 case O.OBin{s, +mk, +mv, +ml, +mh}: 342 +hl = {O.OBin{0, mk, mv, ml, mh} : O.OMap} 343 +h_b = bn.b(~K, ~V, ~cmp, Some{k}, ub, hk, hv, hl, hh, eh) 344 +h_l = bn.l(~K, ~V, ~cmp, Some{k}, ub, hk, hv, hl, hh, eh) 345 +m_a = bn.a(~K, ~V, ~cmp, Some{k}, Some{hk}, mk, mv, ml, mh, h_l) 346 +m_b = bn.b(~K, ~V, ~cmp, Some{k}, Some{hk}, mk, mv, ml, mh, h_l) 347 bn.i(~K, ~V, ~cmp, lb, ub, mk, mv, O.OMap.bin(K, V, k, v, lo, ml), 348 O.OMap.bin(K, V, hk, hv, mh, hh), 349 above_trans(~K, ~cmp, ~trans, lb, k, mk, ea, m_a), 350 below_trans(~K, ~cmp, ~trans, ub, mk, hk, m_b, h_b), 351 bn.i(~K, ~V, ~cmp, lb, Some{mk}, k, v, lo, ml, ea, m_a, el, 352 bn.l(~K, ~V, ~cmp, Some{k}, Some{hk}, mk, mv, ml, mh, h_l)), 353 bn.i(~K, ~V, ~cmp, Some{mk}, ub, hk, hv, mh, hh, m_b, h_b, 354 bn.h(~K, ~V, ~cmp, Some{k}, Some{hk}, mk, mv, ml, mh, h_l), 355 bn.h(~K, ~V, ~cmp, Some{k}, ub, hk, hv, hl, hh, eh))) 356 357 def rot_lo.pick.bnd( 358 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 359 single: Bool, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, +v: V, 360 +lo: O.OMap, +hk: K, +hv: V, +hl: O.OMap, +hh: O.OMap, 361 +ea: {Laws.above(~K, ~cmp, lb, k) == True{} : Bool}, 362 el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) == True{} : Bool}, 363 +eh: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, hk, hv, hl, hh}, Some{k}, ub) == True{} : Bool} 364 ) -> {Laws.bounded(~K, ~V, ~cmp, 365 O.OMap.rot_lo.pick(K, V, single, k, v, lo, hk, hv, hl, hh), lb, ub) == True{} : Bool}: 366 match single: 367 case True{}: 368 rot_lo.single.bnd(~K, ~V, ~cmp, ~trans, lb, ub, k, v, lo, hk, hv, hl, hh, ea, el, eh) 369 case False{}: 370 rot_lo.double.bnd(~K, ~V, ~cmp, ~trans, hl, lb, ub, k, v, lo, hk, hv, hh, ea, el, eh) 371 372 def rot_lo.bnd( 373 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 374 hi: O.OMap, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, +v: V, 375 +lo: O.OMap, 376 +ea: {Laws.above(~K, ~cmp, lb, k) == True{} : Bool}, 377 eb: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}, 378 el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) == True{} : Bool}, 379 +eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool} 380 ) -> {Laws.bounded(~K, ~V, ~cmp, O.OMap.rot_lo(K, V, k, v, lo, hi), lb, ub) == True{} : Bool}: 381 match hi: 382 case O.OTip{}: 383 bn.i(~K, ~V, ~cmp, lb, ub, k, v, lo, O.OTip{}, ea, eb, el, eh) 384 case O.OBin{s, +hk, +hv, +hl, +hh}: 385 rot_lo.pick.bnd(~K, ~V, ~cmp, ~trans, 386 U32.is_lt((O.OMap.size(K, V, hl) + 1 : U32), 387 (2 * (O.OMap.size(K, V, hh) + 1) : U32)), 388 lb, ub, k, v, lo, hk, hv, hl, hh, ea, el, eh) 389 390 def rot_hi.single.bnd( 391 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 392 +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, +v: V, +lk: K, +lv: V, 393 +ll: O.OMap, +lh: O.OMap, +hi: O.OMap, 394 +eb: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}, 395 +el: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, lk, lv, ll, lh}, lb, Some{k}) == True{} : Bool}, 396 eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool} 397 ) -> {Laws.bounded(~K, ~V, ~cmp, 398 O.OMap.bin(K, V, lk, lv, ll, O.OMap.bin(K, V, k, v, lh, hi)), lb, ub) == True{} : Bool}: 399 +l_b = bn.b(~K, ~V, ~cmp, lb, Some{k}, lk, lv, ll, lh, el) 400 bn.i(~K, ~V, ~cmp, lb, ub, lk, lv, ll, O.OMap.bin(K, V, k, v, lh, hi), 401 bn.a(~K, ~V, ~cmp, lb, Some{k}, lk, lv, ll, lh, el), 402 below_trans(~K, ~cmp, ~trans, ub, lk, k, l_b, eb), 403 bn.l(~K, ~V, ~cmp, lb, Some{k}, lk, lv, ll, lh, el), 404 bn.i(~K, ~V, ~cmp, Some{lk}, ub, k, v, lh, hi, l_b, eb, 405 bn.h(~K, ~V, ~cmp, lb, Some{k}, lk, lv, ll, lh, el), eh)) 406 407 def rot_hi.double.bnd( 408 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 409 lh: O.OMap, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, +v: V, 410 +lk: K, +lv: V, +ll: O.OMap, +hi: O.OMap, 411 +eb: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}, 412 +el: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, lk, lv, ll, lh}, lb, Some{k}) == True{} : Bool}, 413 eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool} 414 ) -> {Laws.bounded(~K, ~V, ~cmp, 415 O.OMap.rot_hi.double(K, V, k, v, lk, lv, ll, lh, hi), lb, ub) == True{} : Bool}: 416 match lh: 417 case O.OTip{}: 418 rot_hi.single.bnd(~K, ~V, ~cmp, ~trans, lb, ub, k, v, lk, lv, ll, O.OTip{}, hi, 419 eb, el, eh) 420 case O.OBin{s, +mk, +mv, +ml, +mh}: 421 +lh = {O.OBin{0, mk, mv, ml, mh} : O.OMap} 422 +l_a = bn.a(~K, ~V, ~cmp, lb, Some{k}, lk, lv, ll, lh, el) 423 +l_h = bn.h(~K, ~V, ~cmp, lb, Some{k}, lk, lv, ll, lh, el) 424 +m_a = bn.a(~K, ~V, ~cmp, Some{lk}, Some{k}, mk, mv, ml, mh, l_h) 425 +m_b = bn.b(~K, ~V, ~cmp, Some{lk}, Some{k}, mk, mv, ml, mh, l_h) 426 bn.i(~K, ~V, ~cmp, lb, ub, mk, mv, O.OMap.bin(K, V, lk, lv, ll, ml), 427 O.OMap.bin(K, V, k, v, mh, hi), 428 above_trans(~K, ~cmp, ~trans, lb, lk, mk, l_a, m_a), 429 below_trans(~K, ~cmp, ~trans, ub, mk, k, m_b, eb), 430 bn.i(~K, ~V, ~cmp, lb, Some{mk}, lk, lv, ll, ml, l_a, m_a, 431 bn.l(~K, ~V, ~cmp, lb, Some{k}, lk, lv, ll, lh, el), 432 bn.l(~K, ~V, ~cmp, Some{lk}, Some{k}, mk, mv, ml, mh, l_h)), 433 bn.i(~K, ~V, ~cmp, Some{mk}, ub, k, v, mh, hi, m_b, eb, 434 bn.h(~K, ~V, ~cmp, Some{lk}, Some{k}, mk, mv, ml, mh, l_h), eh)) 435 436 def rot_hi.pick.bnd( 437 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 438 single: Bool, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, +v: V, 439 +lk: K, +lv: V, +ll: O.OMap, +lh: O.OMap, +hi: O.OMap, 440 +eb: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}, 441 +el: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, lk, lv, ll, lh}, lb, Some{k}) == True{} : Bool}, 442 eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool} 443 ) -> {Laws.bounded(~K, ~V, ~cmp, 444 O.OMap.rot_hi.pick(K, V, single, k, v, lk, lv, ll, lh, hi), lb, ub) == True{} : Bool}: 445 match single: 446 case True{}: 447 rot_hi.single.bnd(~K, ~V, ~cmp, ~trans, lb, ub, k, v, lk, lv, ll, lh, hi, eb, el, eh) 448 case False{}: 449 rot_hi.double.bnd(~K, ~V, ~cmp, ~trans, lh, lb, ub, k, v, lk, lv, ll, hi, eb, el, eh) 450 451 def rot_hi.bnd( 452 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 453 lo: O.OMap, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, +v: V, 454 +hi: O.OMap, 455 ea: {Laws.above(~K, ~cmp, lb, k) == True{} : Bool}, 456 +eb: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}, 457 +el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) == True{} : Bool}, 458 eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool} 459 ) -> {Laws.bounded(~K, ~V, ~cmp, O.OMap.rot_hi(K, V, k, v, lo, hi), lb, ub) == True{} : Bool}: 460 match lo: 461 case O.OTip{}: 462 bn.i(~K, ~V, ~cmp, lb, ub, k, v, O.OTip{}, hi, ea, eb, el, eh) 463 case O.OBin{s, +lk, +lv, +ll, +lh}: 464 rot_hi.pick.bnd(~K, ~V, ~cmp, ~trans, 465 U32.is_lt((O.OMap.size(K, V, lh) + 1 : U32), 466 (2 * (O.OMap.size(K, V, ll) + 1) : U32)), 467 lb, ub, k, v, lk, lv, ll, lh, hi, eb, el, eh) 468 469 def balance.if.bnd( 470 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 471 heavy_hi: Bool, heavy_lo: Bool, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, 472 +v: V, +lo: O.OMap, +hi: O.OMap, 473 +ea: {Laws.above(~K, ~cmp, lb, k) == True{} : Bool}, 474 +eb: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}, 475 +el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) == True{} : Bool}, 476 +eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool} 477 ) -> {Laws.bounded(~K, ~V, ~cmp, 478 O.OMap.balance.if(K, V, heavy_hi, heavy_lo, k, v, lo, hi), lb, ub) == True{} : Bool}: 479 match heavy_hi heavy_lo: 480 case True{} _: 481 rot_lo.bnd(~K, ~V, ~cmp, ~trans, hi, lb, ub, k, v, lo, ea, eb, el, eh) 482 case False{} True{}: 483 rot_hi.bnd(~K, ~V, ~cmp, ~trans, lo, lb, ub, k, v, hi, ea, eb, el, eh) 484 case False{} False{}: 485 bn.i(~K, ~V, ~cmp, lb, ub, k, v, lo, hi, ea, eb, el, eh) 486 487 def balance.bnd( 488 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 489 +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, +v: V, +lo: O.OMap, 490 +hi: O.OMap, 491 ea: {Laws.above(~K, ~cmp, lb, k) == True{} : Bool}, 492 eb: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}, 493 el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) == True{} : Bool}, 494 eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool} 495 ) -> {Laws.bounded(~K, ~V, ~cmp, O.OMap.balance(K, V, k, v, lo, hi), lb, ub) == True{} : Bool}: 496 +wl = (O.OMap.size(K, V, lo) + 1 : U32) 497 +wh = (O.OMap.size(K, V, hi) + 1 : U32) 498 balance.if.bnd(~K, ~V, ~cmp, ~trans, U32.is_gt(wh, (3 * wl : U32)), 499 U32.is_gt(wl, (3 * wh : U32)), lb, ub, k, v, lo, hi, ea, eb, el, eh) 500 501 # Proves a goal about O.Cmp.case by one case per comparison result. 502 def cmp.split( 503 -A: Type, -B: Type, -F: A -> B, -G: B, c: Cmp, -f1: Unit -> A, 504 -f2: Unit -> A, -f3: Unit -> A, 505 hl: {c == LT{} : Cmp} -> {F(f1(Unit{})) == G : B}, 506 he: {c == EQ{} : Cmp} -> {F(f2(Unit{})) == G : B}, 507 hg: {c == GT{} : Cmp} -> {F(f3(Unit{})) == G : B} 508 ) -> {F(O.Cmp.case(A, c, f1, f2, f3)) == G : B}: 509 match c: 510 case LT{}: 511 hl({==}) 512 case EQ{}: 513 he({==}) 514 case GT{}: 515 hg({==}) 516 517 def put.bnd( 518 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~flip: Flip(~K, ~cmp), 519 ~trans: Trans(~K, ~cmp), t: O.OMap, +lb: Maybe<&2, K>, 520 +ub: Maybe<&2, K>, +k: K, +v: V, 521 +bt: {Laws.bounded(~K, ~V, ~cmp, t, lb, ub) == True{} : Bool}, 522 +ea: {Laws.above(~K, ~cmp, lb, k) == True{} : Bool}, 523 +eb: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool} 524 ) -> {Laws.bounded(~K, ~V, ~cmp, O.OMap.put(~K, ~V, ~cmp, t, k, v), lb, ub) == True{} : Bool}: 525 match t: 526 case O.OTip{}: 527 bn.i(~K, ~V, ~cmp, lb, ub, k, v, O.OTip{}, O.OTip{}, ea, eb, {==}, {==}) 528 case O.OBin{+s, +key, +val, +lo, +hi}: 529 +b_a = bn.a(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) 530 +b_b = bn.b(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) 531 +b_l = bn.l(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) 532 +b_h = bn.h(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) 533 cmp.split(O.OMap, Bool, x => Laws.bounded(~K, ~V, ~cmp, x, lb, ub), True{}, 534 cmp(k, key), 535 u => O.OMap.balance(K, V, key, val, O.OMap.put(~K, ~V, ~cmp, lo, k, v), hi), 536 u => O.OBin{s, key, v, lo, hi}, 537 u => O.OMap.balance(K, V, key, val, lo, O.OMap.put(~K, ~V, ~cmp, hi, k, v)), 538 e => balance.bnd(~K, ~V, ~cmp, ~trans, lb, ub, key, val, 539 O.OMap.put(~K, ~V, ~cmp, lo, k, v), hi, b_a, b_b, 540 put.bnd(~K, ~V, ~cmp, ~flip, ~trans, lo, lb, Some{key}, k, v, b_l, ea, 541 lt_true(cmp(k, key), e)), 542 b_h), 543 e => bt, 544 e => balance.bnd(~K, ~V, ~cmp, ~trans, lb, ub, key, val, lo, 545 O.OMap.put(~K, ~V, ~cmp, hi, k, v), b_a, b_b, b_l, 546 put.bnd(~K, ~V, ~cmp, ~flip, ~trans, hi, Some{key}, ub, k, v, b_h, 547 lt_true(cmp(key, k), gt_flip(~K, ~cmp, ~flip, k, key, e)), eb))) 548 549 def Laws.omap_put_searchtree(K, V, cmp, refl, eq, flip, trans, m, tree, k, v): 550 put.bnd(~K, ~V, ~cmp, ~flip, ~trans, m, None{}, None{}, k, v, tree, {==}, {==}) 551 552 def rw(-A: Type, -P: A -> Type, -a: A, -b: A, e: {a == b : A}, p: P(b)) -> P(a): 553 %Equal.sym(A, a, b, e) : P(_) 554 p 555 556 def split( 557 -P: Cmp -> Type, c: Cmp, hl: {c == LT{} : Cmp} -> P(LT{}), 558 he: {c == EQ{} : Cmp} -> P(EQ{}), hg: {c == GT{} : Cmp} -> P(GT{}) 559 ) -> P(c): 560 match c: 561 case LT{}: 562 hl({==}) 563 case EQ{}: 564 he({==}) 565 case GT{}: 566 hg({==}) 567 568 def gt_of_lt( 569 ~K: Data, ~cmp: K -> K -> Cmp, ~flip: Flip(~K, ~cmp), +x: K, +y: K, 570 e: {cmp(x, y) == LT{} : Cmp} 571 ) -> {cmp(y, x) == GT{} : Cmp}: 572 Equal.trans(Cmp, cmp(y, x), Laws.flip(cmp(x, y)), GT{}, flip(x, y), 573 Equal.cong(Cmp, Cmp, c => Laws.flip(c), cmp(x, y), LT{}, e)) 574 575 # get on one node, with the comparison result as a parameter. 576 def getc( 577 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, c: Cmp, +x: K, +val: V, 578 lo: O.OMap, hi: O.OMap 579 ) -> Maybe<&2, V>: 580 O.Cmp.case(Maybe<&2, V>, c, 581 u => O.OMap.get(~K, ~V, ~cmp, lo, x), 582 u => Some{val}, 583 u => O.OMap.get(~K, ~V, ~cmp, hi, x)) 584 585 # get finds key k itself in a node keyed by k. 586 def get.here( 587 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), +k: K, +v: V, 588 +lo: O.OMap, +hi: O.OMap 589 ) -> {O.OMap.get(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, k) == Some{v} : Maybe<&2, V>}: 590 rw(Cmp, c => {getc(~K, ~V, ~cmp, c, k, v, lo, hi) == Some{v} : Maybe<&2, V>}, 591 cmp(k, k), EQ{}, refl(k), {==}) 592 593 # get on a node goes to lo when the comparison is LT. 594 def get.lt( 595 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: K, +k: K, +v: V, 596 +lo: O.OMap, +hi: O.OMap, e: {cmp(x, k) == LT{} : Cmp} 597 ) -> {O.OMap.get(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, x) 598 == O.OMap.get(~K, ~V, ~cmp, lo, x) : Maybe<&2, V>}: 599 rw(Cmp, c => {getc(~K, ~V, ~cmp, c, x, v, lo, hi) 600 == O.OMap.get(~K, ~V, ~cmp, lo, x) : Maybe<&2, V>}, 601 cmp(x, k), LT{}, e, {==}) 602 603 # get on a node goes to hi when the comparison is GT. 604 def get.gt( 605 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +x: K, +k: K, +v: V, 606 +lo: O.OMap, +hi: O.OMap, e: {cmp(x, k) == GT{} : Cmp} 607 ) -> {O.OMap.get(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, x) 608 == O.OMap.get(~K, ~V, ~cmp, hi, x) : Maybe<&2, V>}: 609 rw(Cmp, c => {getc(~K, ~V, ~cmp, c, x, v, lo, hi) 610 == O.OMap.get(~K, ~V, ~cmp, hi, x) : Maybe<&2, V>}, 611 cmp(x, k), GT{}, e, {==}) 612 613 def rot_lo.single.get( 614 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 615 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 616 +x: K, +k: K, +v: V, +lo: O.OMap, +hk: K, 617 +hv: V, +hl: O.OMap, +hh: O.OMap, +khk: {cmp(k, hk) == LT{} : Cmp} 618 ) -> {O.OMap.get(~K, ~V, ~cmp, 619 O.OMap.bin(K, V, hk, hv, O.OMap.bin(K, V, k, v, lo, hl), hh), x) 620 == O.OMap.get(~K, ~V, ~cmp, O.OBin{0, k, v, lo, O.OBin{0, hk, hv, hl, hh}}, x) 621 : Maybe<&2, V>}: 622 +inner = {O.OBin{0, k, v, lo, hl} : O.OMap} 623 +lhs = {O.OBin{0, hk, hv, inner, hh} : O.OMap} 624 split(c => {O.OMap.get(~K, ~V, ~cmp, lhs, x) 625 == getc(~K, ~V, ~cmp, c, x, v, lo, O.OBin{0, hk, hv, hl, hh}) : Maybe<&2, V>}, 626 cmp(x, k), 627 +e => Equal.trans(Maybe<&2, V>, O.OMap.get(~K, ~V, ~cmp, lhs, x), 628 O.OMap.get(~K, ~V, ~cmp, inner, x), O.OMap.get(~K, ~V, ~cmp, lo, x), 629 get.lt(~K, ~V, ~cmp, x, hk, hv, inner, hh, trans(x, k, hk, e, khk)), 630 get.lt(~K, ~V, ~cmp, x, k, v, lo, hl, e)), 631 e => rw(K, y => {O.OMap.get(~K, ~V, ~cmp, lhs, y) == Some{v} : Maybe<&2, V>}, 632 x, k, eq(x, k, e), 633 Equal.trans(Maybe<&2, V>, O.OMap.get(~K, ~V, ~cmp, lhs, k), 634 O.OMap.get(~K, ~V, ~cmp, inner, k), Some{v}, 635 get.lt(~K, ~V, ~cmp, k, hk, hv, inner, hh, khk), 636 get.here(~K, ~V, ~cmp, ~refl, k, v, lo, hl))), 637 e => split(c => {getc(~K, ~V, ~cmp, c, x, hv, inner, hh) 638 == getc(~K, ~V, ~cmp, c, x, hv, hl, hh) : Maybe<&2, V>}, 639 cmp(x, hk), 640 e2 => get.gt(~K, ~V, ~cmp, x, k, v, lo, hl, e), 641 e2 => {==}, 642 e2 => {==})) 643 644 def g(~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, t: O.OMap, +x: K) -> Maybe<&2, V>: 645 O.OMap.get(~K, ~V, ~cmp, t, x) 646 647 def mtr( 648 -V: Data, -a: Maybe<&2, V>, -b: Maybe<&2, V>, -c: Maybe<&2, V>, 649 e1: {a == b : Maybe<&2, V>}, e2: {b == c : Maybe<&2, V>} 650 ) -> {a == c : Maybe<&2, V>}: 651 Equal.trans(Maybe<&2, V>, a, b, c, e1, e2) 652 653 def rot_lo.double.get2( 654 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 655 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 656 +x: K, +k: K, +v: V, +lo: O.OMap, +hk: K, +hv: V, +mk: K, +mv: V, 657 +ml: O.OMap, +mh: O.OMap, +hh: O.OMap, 658 +khm: {cmp(k, mk) == LT{} : Cmp}, +mhk: {cmp(mk, hk) == LT{} : Cmp} 659 ) -> {g(~K, ~V, ~cmp, O.OMap.bin(K, V, mk, mv, O.OMap.bin(K, V, k, v, lo, ml), 660 O.OMap.bin(K, V, hk, hv, mh, hh)), x) 661 == g(~K, ~V, ~cmp, O.OBin{0, k, v, lo, O.OBin{0, hk, hv, O.OBin{0, mk, mv, ml, mh}, hh}}, x) 662 : Maybe<&2, V>}: 663 +a = {O.OBin{0, k, v, lo, ml} : O.OMap} 664 +b = {O.OBin{0, hk, hv, mh, hh} : O.OMap} 665 +l = {O.OBin{0, mk, mv, a, b} : O.OMap} 666 +m = {O.OBin{0, mk, mv, ml, mh} : O.OMap} 667 +r1 = {O.OBin{0, hk, hv, m, hh} : O.OMap} 668 split(c => {g(~K, ~V, ~cmp, l, x) == getc(~K, ~V, ~cmp, c, x, v, lo, r1) : Maybe<&2, V>}, 669 cmp(x, k), 670 +e => mtr(V, g(~K, ~V, ~cmp, l, x), g(~K, ~V, ~cmp, a, x), g(~K, ~V, ~cmp, lo, x), 671 get.lt(~K, ~V, ~cmp, x, mk, mv, a, b, trans(x, k, mk, e, khm)), 672 get.lt(~K, ~V, ~cmp, x, k, v, lo, ml, e)), 673 e => rw(K, y => {g(~K, ~V, ~cmp, l, y) == Some{v} : Maybe<&2, V>}, x, k, eq(x, k, e), 674 mtr(V, g(~K, ~V, ~cmp, l, k), g(~K, ~V, ~cmp, a, k), Some{v}, 675 get.lt(~K, ~V, ~cmp, k, mk, mv, a, b, khm), 676 get.here(~K, ~V, ~cmp, ~refl, k, v, lo, ml))), 677 +e => split(c => {g(~K, ~V, ~cmp, l, x) == getc(~K, ~V, ~cmp, c, x, hv, m, hh) : Maybe<&2, V>}, 678 cmp(x, hk), 679 +e2 => split(c => {getc(~K, ~V, ~cmp, c, x, mv, a, b) 680 == getc(~K, ~V, ~cmp, c, x, mv, ml, mh) : Maybe<&2, V>}, 681 cmp(x, mk), 682 e3 => get.gt(~K, ~V, ~cmp, x, k, v, lo, ml, e), 683 e3 => {==}, 684 e3 => get.lt(~K, ~V, ~cmp, x, hk, hv, mh, hh, e2)), 685 e2 => rw(K, y => {g(~K, ~V, ~cmp, l, y) == Some{hv} : Maybe<&2, V>}, x, hk, eq(x, hk, e2), 686 mtr(V, g(~K, ~V, ~cmp, l, hk), g(~K, ~V, ~cmp, b, hk), Some{hv}, 687 get.gt(~K, ~V, ~cmp, hk, mk, mv, a, b, gt_of_lt(~K, ~cmp, ~flip, mk, hk, mhk)), 688 get.here(~K, ~V, ~cmp, ~refl, hk, hv, mh, hh))), 689 +e2 => mtr(V, g(~K, ~V, ~cmp, l, x), g(~K, ~V, ~cmp, b, x), g(~K, ~V, ~cmp, hh, x), 690 get.gt(~K, ~V, ~cmp, x, mk, mv, a, b, 691 gt_of_lt(~K, ~cmp, ~flip, mk, x, 692 trans(mk, hk, x, mhk, gt_flip(~K, ~cmp, ~flip, x, hk, e2)))), 693 get.gt(~K, ~V, ~cmp, x, hk, hv, mh, hh, e2)))) 694 695 def rot_lo.double.get( 696 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 697 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 698 hl: O.OMap, +x: K, +k: K, +v: V, +lo: O.OMap, +hk: K, +hv: V, 699 +hh: O.OMap, +khk: {cmp(k, hk) == LT{} : Cmp}, 700 +h_l: {Laws.bounded(~K, ~V, ~cmp, hl, Some{k}, Some{hk}) == True{} : Bool} 701 ) -> {g(~K, ~V, ~cmp, O.OMap.rot_lo.double(K, V, k, v, lo, hk, hv, hl, hh), x) 702 == g(~K, ~V, ~cmp, O.OBin{0, k, v, lo, O.OBin{0, hk, hv, hl, hh}}, x) : Maybe<&2, V>}: 703 match hl: 704 case O.OTip{}: 705 rot_lo.single.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, x, k, v, lo, hk, hv, 706 O.OTip{}, hh, khk) 707 case O.OBin{s, +mk, +mv, +ml, +mh}: 708 rot_lo.double.get2(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, x, k, v, lo, hk, hv, 709 mk, mv, ml, mh, hh, 710 lt_of(cmp(k, mk), bn.a(~K, ~V, ~cmp, Some{k}, Some{hk}, mk, mv, ml, mh, h_l)), 711 lt_of(cmp(mk, hk), bn.b(~K, ~V, ~cmp, Some{k}, Some{hk}, mk, mv, ml, mh, h_l))) 712 713 def rot_lo.pick.get( 714 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 715 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 716 single: Bool, +x: K, +k: K, +v: V, +lo: O.OMap, +hk: K, +hv: V, 717 +hl: O.OMap, +hh: O.OMap, +khk: {cmp(k, hk) == LT{} : Cmp}, 718 +h_l: {Laws.bounded(~K, ~V, ~cmp, hl, Some{k}, Some{hk}) == True{} : Bool} 719 ) -> {g(~K, ~V, ~cmp, O.OMap.rot_lo.pick(K, V, single, k, v, lo, hk, hv, hl, hh), x) 720 == g(~K, ~V, ~cmp, O.OBin{0, k, v, lo, O.OBin{0, hk, hv, hl, hh}}, x) : Maybe<&2, V>}: 721 match single: 722 case True{}: 723 rot_lo.single.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, x, k, v, lo, hk, hv, 724 hl, hh, khk) 725 case False{}: 726 rot_lo.double.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, hl, x, k, v, lo, hk, hv, 727 hh, khk, h_l) 728 729 def rot_lo.get( 730 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 731 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 732 hi: O.OMap, +ub: Maybe<&2, K>, +x: K, +k: K, +v: V, +lo: O.OMap, 733 +eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool} 734 ) -> {g(~K, ~V, ~cmp, O.OMap.rot_lo(K, V, k, v, lo, hi), x) 735 == g(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, x) : Maybe<&2, V>}: 736 match hi: 737 case O.OTip{}: 738 {==} 739 case O.OBin{s, +hk, +hv, +hl, +hh}: 740 rot_lo.pick.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, 741 U32.is_lt((O.OMap.size(K, V, hl) + 1 : U32), 742 (2 * (O.OMap.size(K, V, hh) + 1) : U32)), 743 x, k, v, lo, hk, hv, hl, hh, 744 lt_of(cmp(k, hk), bn.a(~K, ~V, ~cmp, Some{k}, ub, hk, hv, hl, hh, eh)), 745 bn.l(~K, ~V, ~cmp, Some{k}, ub, hk, hv, hl, hh, eh)) 746 747 def rot_hi.single.get( 748 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 749 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 750 +x: K, +k: K, +v: V, +lk: K, +lv: V, +ll: O.OMap, +lh: O.OMap, 751 +hi: O.OMap, +lkk: {cmp(lk, k) == LT{} : Cmp} 752 ) -> {g(~K, ~V, ~cmp, O.OMap.bin(K, V, lk, lv, ll, O.OMap.bin(K, V, k, v, lh, hi)), x) 753 == g(~K, ~V, ~cmp, O.OBin{0, k, v, O.OBin{0, lk, lv, ll, lh}, hi}, x) : Maybe<&2, V>}: 754 +b = {O.OBin{0, k, v, lh, hi} : O.OMap} 755 +l = {O.OBin{0, lk, lv, ll, b} : O.OMap} 756 +ln = {O.OBin{0, lk, lv, ll, lh} : O.OMap} 757 split(c => {g(~K, ~V, ~cmp, l, x) == getc(~K, ~V, ~cmp, c, x, v, ln, hi) : Maybe<&2, V>}, 758 cmp(x, k), 759 e => split(c => {getc(~K, ~V, ~cmp, c, x, lv, ll, b) 760 == getc(~K, ~V, ~cmp, c, x, lv, ll, lh) : Maybe<&2, V>}, 761 cmp(x, lk), 762 e2 => {==}, 763 e2 => {==}, 764 e2 => get.lt(~K, ~V, ~cmp, x, k, v, lh, hi, e)), 765 e => rw(K, y => {g(~K, ~V, ~cmp, l, y) == Some{v} : Maybe<&2, V>}, x, k, eq(x, k, e), 766 mtr(V, g(~K, ~V, ~cmp, l, k), g(~K, ~V, ~cmp, b, k), Some{v}, 767 get.gt(~K, ~V, ~cmp, k, lk, lv, ll, b, gt_of_lt(~K, ~cmp, ~flip, lk, k, lkk)), 768 get.here(~K, ~V, ~cmp, ~refl, k, v, lh, hi))), 769 +e => mtr(V, g(~K, ~V, ~cmp, l, x), g(~K, ~V, ~cmp, b, x), g(~K, ~V, ~cmp, hi, x), 770 get.gt(~K, ~V, ~cmp, x, lk, lv, ll, b, 771 gt_of_lt(~K, ~cmp, ~flip, lk, x, 772 trans(lk, k, x, lkk, gt_flip(~K, ~cmp, ~flip, x, k, e)))), 773 get.gt(~K, ~V, ~cmp, x, k, v, lh, hi, e))) 774 775 def rot_hi.double.get2( 776 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 777 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 778 +x: K, +k: K, +v: V, +lk: K, +lv: V, +ll: O.OMap, +mk: K, +mv: V, 779 +ml: O.OMap, +mh: O.OMap, +hi: O.OMap, 780 +lkm: {cmp(lk, mk) == LT{} : Cmp}, +mkk: {cmp(mk, k) == LT{} : Cmp} 781 ) -> {g(~K, ~V, ~cmp, O.OMap.bin(K, V, mk, mv, O.OMap.bin(K, V, lk, lv, ll, ml), 782 O.OMap.bin(K, V, k, v, mh, hi)), x) 783 == g(~K, ~V, ~cmp, O.OBin{0, k, v, O.OBin{0, lk, lv, ll, O.OBin{0, mk, mv, ml, mh}}, hi}, x) 784 : Maybe<&2, V>}: 785 +a = {O.OBin{0, lk, lv, ll, ml} : O.OMap} 786 +b = {O.OBin{0, k, v, mh, hi} : O.OMap} 787 +l = {O.OBin{0, mk, mv, a, b} : O.OMap} 788 +m = {O.OBin{0, mk, mv, ml, mh} : O.OMap} 789 +ln = {O.OBin{0, lk, lv, ll, m} : O.OMap} 790 split(c => {g(~K, ~V, ~cmp, l, x) == getc(~K, ~V, ~cmp, c, x, v, ln, hi) : Maybe<&2, V>}, 791 cmp(x, k), 792 +e => split(c => {g(~K, ~V, ~cmp, l, x) == getc(~K, ~V, ~cmp, c, x, lv, ll, m) : Maybe<&2, V>}, 793 cmp(x, lk), 794 +e2 => mtr(V, g(~K, ~V, ~cmp, l, x), g(~K, ~V, ~cmp, a, x), g(~K, ~V, ~cmp, ll, x), 795 get.lt(~K, ~V, ~cmp, x, mk, mv, a, b, trans(x, lk, mk, e2, lkm)), 796 get.lt(~K, ~V, ~cmp, x, lk, lv, ll, ml, e2)), 797 e2 => rw(K, y => {g(~K, ~V, ~cmp, l, y) == Some{lv} : Maybe<&2, V>}, x, lk, eq(x, lk, e2), 798 mtr(V, g(~K, ~V, ~cmp, l, lk), g(~K, ~V, ~cmp, a, lk), Some{lv}, 799 get.lt(~K, ~V, ~cmp, lk, mk, mv, a, b, lkm), 800 get.here(~K, ~V, ~cmp, ~refl, lk, lv, ll, ml))), 801 +e2 => split(c => {getc(~K, ~V, ~cmp, c, x, mv, a, b) 802 == getc(~K, ~V, ~cmp, c, x, mv, ml, mh) : Maybe<&2, V>}, 803 cmp(x, mk), 804 e3 => get.gt(~K, ~V, ~cmp, x, lk, lv, ll, ml, e2), 805 e3 => {==}, 806 e3 => get.lt(~K, ~V, ~cmp, x, k, v, mh, hi, e))), 807 e => rw(K, y => {g(~K, ~V, ~cmp, l, y) == Some{v} : Maybe<&2, V>}, x, k, eq(x, k, e), 808 mtr(V, g(~K, ~V, ~cmp, l, k), g(~K, ~V, ~cmp, b, k), Some{v}, 809 get.gt(~K, ~V, ~cmp, k, mk, mv, a, b, gt_of_lt(~K, ~cmp, ~flip, mk, k, mkk)), 810 get.here(~K, ~V, ~cmp, ~refl, k, v, mh, hi))), 811 +e => mtr(V, g(~K, ~V, ~cmp, l, x), g(~K, ~V, ~cmp, b, x), g(~K, ~V, ~cmp, hi, x), 812 get.gt(~K, ~V, ~cmp, x, mk, mv, a, b, 813 gt_of_lt(~K, ~cmp, ~flip, mk, x, 814 trans(mk, k, x, mkk, gt_flip(~K, ~cmp, ~flip, x, k, e)))), 815 get.gt(~K, ~V, ~cmp, x, k, v, mh, hi, e))) 816 817 def rot_hi.double.get( 818 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 819 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 820 lh: O.OMap, +x: K, +k: K, +v: V, +lk: K, +lv: V, +ll: O.OMap, 821 +hi: O.OMap, +lkk: {cmp(lk, k) == LT{} : Cmp}, 822 +l_h: {Laws.bounded(~K, ~V, ~cmp, lh, Some{lk}, Some{k}) == True{} : Bool} 823 ) -> {g(~K, ~V, ~cmp, O.OMap.rot_hi.double(K, V, k, v, lk, lv, ll, lh, hi), x) 824 == g(~K, ~V, ~cmp, O.OBin{0, k, v, O.OBin{0, lk, lv, ll, lh}, hi}, x) : Maybe<&2, V>}: 825 match lh: 826 case O.OTip{}: 827 rot_hi.single.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, x, k, v, lk, lv, ll, 828 O.OTip{}, hi, lkk) 829 case O.OBin{s, +mk, +mv, +ml, +mh}: 830 rot_hi.double.get2(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, x, k, v, lk, lv, ll, 831 mk, mv, ml, mh, hi, 832 lt_of(cmp(lk, mk), bn.a(~K, ~V, ~cmp, Some{lk}, Some{k}, mk, mv, ml, mh, l_h)), 833 lt_of(cmp(mk, k), bn.b(~K, ~V, ~cmp, Some{lk}, Some{k}, mk, mv, ml, mh, l_h))) 834 835 def rot_hi.pick.get( 836 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 837 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 838 single: Bool, +x: K, +k: K, +v: V, +lk: K, +lv: V, +ll: O.OMap, 839 +lh: O.OMap, +hi: O.OMap, +lkk: {cmp(lk, k) == LT{} : Cmp}, 840 +l_h: {Laws.bounded(~K, ~V, ~cmp, lh, Some{lk}, Some{k}) == True{} : Bool} 841 ) -> {g(~K, ~V, ~cmp, O.OMap.rot_hi.pick(K, V, single, k, v, lk, lv, ll, lh, hi), x) 842 == g(~K, ~V, ~cmp, O.OBin{0, k, v, O.OBin{0, lk, lv, ll, lh}, hi}, x) : Maybe<&2, V>}: 843 match single: 844 case True{}: 845 rot_hi.single.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, x, k, v, lk, lv, ll, 846 lh, hi, lkk) 847 case False{}: 848 rot_hi.double.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lh, x, k, v, lk, lv, 849 ll, hi, lkk, l_h) 850 851 def rot_hi.get( 852 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 853 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 854 lo: O.OMap, +lb: Maybe<&2, K>, +x: K, +k: K, +v: V, +hi: O.OMap, 855 +el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) == True{} : Bool} 856 ) -> {g(~K, ~V, ~cmp, O.OMap.rot_hi(K, V, k, v, lo, hi), x) 857 == g(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, x) : Maybe<&2, V>}: 858 match lo: 859 case O.OTip{}: 860 {==} 861 case O.OBin{s, +lk, +lv, +ll, +lh}: 862 rot_hi.pick.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, 863 U32.is_lt((O.OMap.size(K, V, lh) + 1 : U32), 864 (2 * (O.OMap.size(K, V, ll) + 1) : U32)), 865 x, k, v, lk, lv, ll, lh, hi, 866 lt_of(cmp(lk, k), bn.b(~K, ~V, ~cmp, lb, Some{k}, lk, lv, ll, lh, el)), 867 bn.h(~K, ~V, ~cmp, lb, Some{k}, lk, lv, ll, lh, el)) 868 869 def balance.if.get( 870 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 871 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 872 heavy_hi: Bool, heavy_lo: Bool, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +x: K, 873 +k: K, +v: V, +lo: O.OMap, +hi: O.OMap, 874 el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) == True{} : Bool}, 875 eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool} 876 ) -> {g(~K, ~V, ~cmp, O.OMap.balance.if(K, V, heavy_hi, heavy_lo, k, v, lo, hi), x) 877 == g(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, x) : Maybe<&2, V>}: 878 match heavy_hi heavy_lo: 879 case True{} _: 880 rot_lo.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, hi, ub, x, k, v, lo, eh) 881 case False{} True{}: 882 rot_hi.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lo, lb, x, k, v, hi, el) 883 case False{} False{}: 884 {==} 885 886 def balance.get( 887 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 888 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 889 +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +x: K, +k: K, +v: V, +lo: O.OMap, 890 +hi: O.OMap, 891 el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{k}) == True{} : Bool}, 892 eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool} 893 ) -> {g(~K, ~V, ~cmp, O.OMap.balance(K, V, k, v, lo, hi), x) 894 == g(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, x) : Maybe<&2, V>}: 895 +wl = (O.OMap.size(K, V, lo) + 1 : U32) 896 +wh = (O.OMap.size(K, V, hi) + 1 : U32) 897 balance.if.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, U32.is_gt(wh, (3 * wl : U32)), 898 U32.is_gt(wl, (3 * wh : U32)), lb, ub, x, k, v, lo, hi, el, eh) 899 900 def get_put_same( 901 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 902 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 903 t: O.OMap, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, +v: V, 904 +bt: {Laws.bounded(~K, ~V, ~cmp, t, lb, ub) == True{} : Bool}, 905 +ea: {Laws.above(~K, ~cmp, lb, k) == True{} : Bool}, 906 +eb: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool} 907 ) -> {g(~K, ~V, ~cmp, O.OMap.put(~K, ~V, ~cmp, t, k, v), k) == Some{v} : Maybe<&2, V>}: 908 match t: 909 case O.OTip{}: 910 get.here(~K, ~V, ~cmp, ~refl, k, v, O.OTip{}, O.OTip{}) 911 case O.OBin{+s, +key, +val, +lo, +hi}: 912 +b_l = bn.l(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) 913 +b_h = bn.h(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) 914 +plo = O.OMap.put(~K, ~V, ~cmp, lo, k, v) 915 +phi = O.OMap.put(~K, ~V, ~cmp, hi, k, v) 916 cmp.split(O.OMap, Maybe<&2, V>, y => g(~K, ~V, ~cmp, y, k), Some{v}, 917 cmp(k, key), 918 u => O.OMap.balance(K, V, key, val, O.OMap.put(~K, ~V, ~cmp, lo, k, v), hi), 919 u => O.OBin{s, key, v, lo, hi}, 920 u => O.OMap.balance(K, V, key, val, lo, O.OMap.put(~K, ~V, ~cmp, hi, k, v)), 921 +e => mtr(V, g(~K, ~V, ~cmp, O.OMap.balance(K, V, key, val, plo, hi), k), 922 g(~K, ~V, ~cmp, O.OBin{0, key, val, plo, hi}, k), Some{v}, 923 balance.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lb, ub, k, key, val, plo, hi, 924 put.bnd(~K, ~V, ~cmp, ~flip, ~trans, lo, lb, Some{key}, k, v, b_l, ea, 925 lt_true(cmp(k, key), e)), 926 b_h), 927 mtr(V, g(~K, ~V, ~cmp, O.OBin{0, key, val, plo, hi}, k), g(~K, ~V, ~cmp, plo, k), 928 Some{v}, 929 get.lt(~K, ~V, ~cmp, k, key, val, plo, hi, e), 930 get_put_same(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lo, lb, Some{key}, k, v, 931 b_l, ea, lt_true(cmp(k, key), e)))), 932 e => rw(Cmp, c => {getc(~K, ~V, ~cmp, c, k, v, lo, hi) == Some{v} : Maybe<&2, V>}, 933 cmp(k, key), EQ{}, e, {==}), 934 +e => mtr(V, g(~K, ~V, ~cmp, O.OMap.balance(K, V, key, val, lo, phi), k), 935 g(~K, ~V, ~cmp, O.OBin{0, key, val, lo, phi}, k), Some{v}, 936 balance.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lb, ub, k, key, val, lo, phi, 937 b_l, 938 put.bnd(~K, ~V, ~cmp, ~flip, ~trans, hi, Some{key}, ub, k, v, b_h, 939 lt_true(cmp(key, k), gt_flip(~K, ~cmp, ~flip, k, key, e)), eb)), 940 mtr(V, g(~K, ~V, ~cmp, O.OBin{0, key, val, lo, phi}, k), g(~K, ~V, ~cmp, phi, k), 941 Some{v}, 942 get.gt(~K, ~V, ~cmp, k, key, val, lo, phi, e), 943 get_put_same(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, hi, Some{key}, ub, k, v, 944 b_h, lt_true(cmp(key, k), gt_flip(~K, ~cmp, ~flip, k, key, e)), eb)))) 945 946 def Laws.omap_get_put_same(K, V, cmp, refl, eq, flip, trans, m, tree, k, v): 947 get_put_same(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, m, None{}, None{}, k, v, tree, 948 {==}, {==}) 949 950 def neq_false(c: Cmp, ne: {c != EQ{} : Cmp}) -> {Cmp.is_eq(c) == False{} : Bool}: 951 match c: 952 case LT{}: 953 {==} 954 case EQ{}: 955 Empty.absurd({Cmp.is_eq(EQ{}) == False{} : Bool}, ne({==})) 956 case GT{}: 957 {==} 958 959 def ne_absurd( 960 -A: Type, -c: Cmp, nef: {Cmp.is_eq(c) == False{} : Bool}, e: {c == EQ{} : Cmp} 961 ) -> A: 962 +tf = Equal.trans(Bool, True{}, Cmp.is_eq(c), False{}, 963 Equal.sym(Bool, Cmp.is_eq(c), True{}, Equal.cong(Cmp, Bool, x => Cmp.is_eq(x), c, EQ{}, e)), 964 nef) 965 Empty.absurd(A, MBool.false_ne_true()(Equal.sym(Bool, True{}, False{}, tf))) 966 967 def eq_flip( 968 ~K: Data, ~cmp: K -> K -> Cmp, ~flip: Flip(~K, ~cmp), +x: K, +y: K, 969 e: {cmp(x, y) == EQ{} : Cmp} 970 ) -> {cmp(y, x) == EQ{} : Cmp}: 971 Equal.trans(Cmp, cmp(y, x), Laws.flip(cmp(x, y)), EQ{}, flip(x, y), 972 Equal.cong(Cmp, Cmp, c => Laws.flip(c), cmp(x, y), EQ{}, e)) 973 974 def get_put_other( 975 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~refl: Refl(~K, ~cmp), ~eq: Eq(~K, ~cmp), 976 ~flip: Flip(~K, ~cmp), ~trans: Trans(~K, ~cmp), 977 t: O.OMap, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k2: K, +k: K, +v: V, 978 +bt: {Laws.bounded(~K, ~V, ~cmp, t, lb, ub) == True{} : Bool}, 979 +ea: {Laws.above(~K, ~cmp, lb, k2) == True{} : Bool}, 980 +eb: {Laws.below(~K, ~cmp, ub, k2) == True{} : Bool}, 981 +nef: {Cmp.is_eq(cmp(k2, k)) == False{} : Bool} 982 ) -> {g(~K, ~V, ~cmp, O.OMap.put(~K, ~V, ~cmp, t, k2, v), k) 983 == g(~K, ~V, ~cmp, t, k) : Maybe<&2, V>}: 984 match t: 985 case O.OTip{}: 986 split(c => {getc(~K, ~V, ~cmp, c, k, v, O.OTip{}, O.OTip{}) == None{} : Maybe<&2, V>}, 987 cmp(k, k2), 988 e => {==}, 989 e => ne_absurd({Some{v} == None{} : Maybe<&2, V>}, cmp(k2, k), nef, 990 eq_flip(~K, ~cmp, ~flip, k, k2, e)), 991 e => {==}) 992 case O.OBin{+s, +key, +val, +lo, +hi}: 993 +b_l = bn.l(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) 994 +b_h = bn.h(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) 995 +plo = O.OMap.put(~K, ~V, ~cmp, lo, k2, v) 996 +phi = O.OMap.put(~K, ~V, ~cmp, hi, k2, v) 997 +old = {O.OBin{s, key, val, lo, hi} : O.OMap} 998 cmp.split(O.OMap, Maybe<&2, V>, y => g(~K, ~V, ~cmp, y, k), 999 g(~K, ~V, ~cmp, old, k), cmp(k2, key), 1000 u => O.OMap.balance(K, V, key, val, O.OMap.put(~K, ~V, ~cmp, lo, k2, v), hi), 1001 u => O.OBin{s, key, v, lo, hi}, 1002 u => O.OMap.balance(K, V, key, val, lo, O.OMap.put(~K, ~V, ~cmp, hi, k2, v)), 1003 +e => mtr(V, g(~K, ~V, ~cmp, O.OMap.balance(K, V, key, val, plo, hi), k), 1004 g(~K, ~V, ~cmp, O.OBin{0, key, val, plo, hi}, k), g(~K, ~V, ~cmp, old, k), 1005 balance.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lb, ub, k, key, val, plo, hi, 1006 put.bnd(~K, ~V, ~cmp, ~flip, ~trans, lo, lb, Some{key}, k2, v, b_l, ea, 1007 lt_true(cmp(k2, key), e)), 1008 b_h), 1009 split(c => {getc(~K, ~V, ~cmp, c, k, val, plo, hi) 1010 == getc(~K, ~V, ~cmp, c, k, val, lo, hi) : Maybe<&2, V>}, 1011 cmp(k, key), 1012 e2 => get_put_other(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lo, lb, Some{key}, 1013 k2, k, v, b_l, ea, lt_true(cmp(k2, key), e), nef), 1014 e2 => {==}, 1015 e2 => {==})), 1016 +e => split(c => {getc(~K, ~V, ~cmp, c, k, v, lo, hi) 1017 == getc(~K, ~V, ~cmp, c, k, val, lo, hi) : Maybe<&2, V>}, 1018 cmp(k, key), 1019 e2 => {==}, 1020 e2 => ne_absurd({Some{v} == Some{val} : Maybe<&2, V>}, cmp(k2, k), nef, 1021 rw(K, y => {cmp(y, k) == EQ{} : Cmp}, k2, key, eq(k2, key, e), 1022 eq_flip(~K, ~cmp, ~flip, k, key, e2))), 1023 e2 => {==}), 1024 +e => mtr(V, g(~K, ~V, ~cmp, O.OMap.balance(K, V, key, val, lo, phi), k), 1025 g(~K, ~V, ~cmp, O.OBin{0, key, val, lo, phi}, k), g(~K, ~V, ~cmp, old, k), 1026 balance.get(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, lb, ub, k, key, val, lo, phi, 1027 b_l, 1028 put.bnd(~K, ~V, ~cmp, ~flip, ~trans, hi, Some{key}, ub, k2, v, b_h, 1029 lt_true(cmp(key, k2), gt_flip(~K, ~cmp, ~flip, k2, key, e)), eb)), 1030 split(c => {getc(~K, ~V, ~cmp, c, k, val, lo, phi) 1031 == getc(~K, ~V, ~cmp, c, k, val, lo, hi) : Maybe<&2, V>}, 1032 cmp(k, key), 1033 e2 => {==}, 1034 e2 => {==}, 1035 e2 => get_put_other(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, hi, Some{key}, ub, 1036 k2, k, v, b_h, lt_true(cmp(key, k2), gt_flip(~K, ~cmp, ~flip, k2, key, e)), 1037 eb, nef)))) 1038 1039 def Laws.omap_get_put_other_key(K, V, cmp, refl, eq, flip, trans, m, tree, k2, k, ne, v): 1040 get_put_other(~K, ~V, ~cmp, ~refl, ~eq, ~flip, ~trans, m, None{}, None{}, k2, k, v, tree, 1041 {==}, {==}, neq_false(cmp(k2, k), ne)) 1042 1043 # A tree bounded above by a is bounded above by anything above a. 1044 def weaken_hi( 1045 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 1046 t: O.OMap, +lb: Maybe<&2, K>, +a: K, +ub: Maybe<&2, K>, 1047 +e: {Laws.bounded(~K, ~V, ~cmp, t, lb, Some{a}) == True{} : Bool}, 1048 +eab: {Laws.below(~K, ~cmp, ub, a) == True{} : Bool} 1049 ) -> {Laws.bounded(~K, ~V, ~cmp, t, lb, ub) == True{} : Bool}: 1050 match t: 1051 case O.OTip{}: 1052 {==} 1053 case O.OBin{s, +k, +v, +lo, +hi}: 1054 bn.i(~K, ~V, ~cmp, lb, ub, k, v, lo, hi, 1055 bn.a(~K, ~V, ~cmp, lb, Some{a}, k, v, lo, hi, e), 1056 below_trans(~K, ~cmp, ~trans, ub, k, a, 1057 bn.b(~K, ~V, ~cmp, lb, Some{a}, k, v, lo, hi, e), eab), 1058 bn.l(~K, ~V, ~cmp, lb, Some{a}, k, v, lo, hi, e), 1059 weaken_hi(~K, ~V, ~cmp, ~trans, hi, Some{k}, a, ub, 1060 bn.h(~K, ~V, ~cmp, lb, Some{a}, k, v, lo, hi, e), eab)) 1061 1062 # What pop_min answers: its key lies between the bounds, and the rest lies above it. 1063 def PM( 1064 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, 1065 r: K & V & O.OMap 1066 ) -> Bool: 1067 (+mk, mv, t) = r 1068 Bool.and(Bool.and(Laws.above(~K, ~cmp, lb, mk), Laws.below(~K, ~cmp, ub, mk)), 1069 Laws.bounded(~K, ~V, ~cmp, t, Some{mk}, ub)) 1070 1071 def pm.fin.bnd.go( 1072 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 1073 +mk: K, +mv: V, +t: O.OMap, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, 1074 +v: V, +hi: O.OMap, 1075 +ih: {PM(~K, ~V, ~cmp, lb, Some{k}, {(mk, mv, t) : K & V & O.OMap}) == True{} : Bool}, 1076 +eb: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}, 1077 eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool} 1078 ) -> {PM(~K, ~V, ~cmp, lb, ub, 1079 O.OMap.pop_min.fin(K, V, k, v, hi, {(mk, mv, t) : K & V & O.OMap})) == True{} : Bool}: 1080 +ab = Bool.and(Laws.above(~K, ~cmp, lb, mk), Laws.below(~K, ~cmp, Some{k}, mk)) 1081 +c = Laws.bounded(~K, ~V, ~cmp, t, Some{mk}, Some{k}) 1082 +eab = MBool.eq_true_of_and_left(ab, c, ih) 1083 +mkk = MBool.eq_true_of_and_right(Laws.above(~K, ~cmp, lb, mk), Laws.below(~K, ~cmp, Some{k}, mk), eab) 1084 MBool.and_eq_true(Bool.and(Laws.above(~K, ~cmp, lb, mk), Laws.below(~K, ~cmp, ub, mk)), Laws.bounded(~K, ~V, ~cmp, O.OMap.balance(K, V, k, v, t, hi), Some{mk}, ub), MBool.and_eq_true(Laws.above(~K, ~cmp, lb, mk), Laws.below(~K, ~cmp, ub, mk), MBool.eq_true_of_and_left(Laws.above(~K, ~cmp, lb, mk), Laws.below(~K, ~cmp, Some{k}, mk), eab), below_trans(~K, ~cmp, ~trans, ub, mk, k, mkk, eb)), balance.bnd(~K, ~V, ~cmp, ~trans, Some{mk}, ub, k, v, t, hi, mkk, eb, 1085 MBool.eq_true_of_and_right(ab, c, ih), eh)) 1086 1087 # Workaround for https://github.com/bendlang/bend/issues/1077: bind the tuple without +. 1088 def pm.fin.bnd( 1089 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 1090 r: K & V & O.OMap, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, +v: V, 1091 +hi: O.OMap, 1092 ih: {PM(~K, ~V, ~cmp, lb, Some{k}, r) == True{} : Bool}, 1093 eb: {Laws.below(~K, ~cmp, ub, k) == True{} : Bool}, 1094 eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub) == True{} : Bool} 1095 ) -> {PM(~K, ~V, ~cmp, lb, ub, O.OMap.pop_min.fin(K, V, k, v, hi, r)) == True{} : Bool}: 1096 (mk, rest) = r 1097 (mv, t) = rest 1098 pm.fin.bnd.go(~K, ~V, ~cmp, ~trans, mk, mv, t, lb, ub, k, v, hi, ih, eb, eh) 1099 1100 def pm.bnd( 1101 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 1102 lo: O.OMap, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, +v: V, 1103 +hi: O.OMap, 1104 +e: {Laws.bounded(~K, ~V, ~cmp, O.OBin{0, k, v, lo, hi}, lb, ub) == True{} : Bool} 1105 ) -> {PM(~K, ~V, ~cmp, lb, ub, O.OMap.pop_min(K, V, lo, k, v, hi)) == True{} : Bool}: 1106 match lo: 1107 case O.OTip{}: 1108 MBool.and_eq_true(Bool.and(Laws.above(~K, ~cmp, lb, k), Laws.below(~K, ~cmp, ub, k)), Laws.bounded(~K, ~V, ~cmp, hi, Some{k}, ub), MBool.and_eq_true(Laws.above(~K, ~cmp, lb, k), Laws.below(~K, ~cmp, ub, k), bn.a(~K, ~V, ~cmp, lb, ub, k, v, O.OTip{}, hi, e), bn.b(~K, ~V, ~cmp, lb, ub, k, v, O.OTip{}, hi, e)), bn.h(~K, ~V, ~cmp, lb, ub, k, v, O.OTip{}, hi, e)) 1109 case O.OBin{s, +lk, +lv, +ll, +lh}: 1110 +lo = {O.OBin{0, lk, lv, ll, lh} : O.OMap} 1111 pm.fin.bnd(~K, ~V, ~cmp, ~trans, O.OMap.pop_min(K, V, ll, lk, lv, lh), lb, ub, k, v, hi, 1112 pm.bnd(~K, ~V, ~cmp, ~trans, ll, lb, Some{k}, lk, lv, lh, 1113 bn.l(~K, ~V, ~cmp, lb, ub, k, v, lo, hi, e)), 1114 bn.b(~K, ~V, ~cmp, lb, ub, k, v, lo, hi, e), 1115 bn.h(~K, ~V, ~cmp, lb, ub, k, v, lo, hi, e)) 1116 1117 def glue.fin.bnd.go( 1118 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 1119 +mk: K, +mv: V, +t: O.OMap, +lo: O.OMap, +lb: Maybe<&2, K>, 1120 +ub: Maybe<&2, K>, +key: K, 1121 eka: {Laws.above(~K, ~cmp, lb, key) == True{} : Bool}, 1122 el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{key}) == True{} : Bool}, 1123 +pmr: {PM(~K, ~V, ~cmp, Some{key}, ub, {(mk, mv, t) : K & V & O.OMap}) == True{} : Bool} 1124 ) -> {Laws.bounded(~K, ~V, ~cmp, 1125 O.OMap.glue.fin(K, V, lo, {(mk, mv, t) : K & V & O.OMap}), lb, ub) == True{} : Bool}: 1126 +ab = Bool.and(Laws.above(~K, ~cmp, Some{key}, mk), Laws.below(~K, ~cmp, ub, mk)) 1127 +c = Laws.bounded(~K, ~V, ~cmp, t, Some{mk}, ub) 1128 +eab = MBool.eq_true_of_and_left(ab, c, pmr) 1129 +km = MBool.eq_true_of_and_left(Laws.above(~K, ~cmp, Some{key}, mk), Laws.below(~K, ~cmp, ub, mk), eab) 1130 balance.bnd(~K, ~V, ~cmp, ~trans, lb, ub, mk, mv, lo, t, 1131 above_trans(~K, ~cmp, ~trans, lb, key, mk, eka, km), 1132 MBool.eq_true_of_and_right(Laws.above(~K, ~cmp, Some{key}, mk), Laws.below(~K, ~cmp, ub, mk), eab), 1133 weaken_hi(~K, ~V, ~cmp, ~trans, lo, lb, key, Some{mk}, el, km), 1134 MBool.eq_true_of_and_right(ab, c, pmr)) 1135 1136 # Workaround for https://github.com/bendlang/bend/issues/1077: bind the tuple without +. 1137 def glue.fin.bnd( 1138 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 1139 r: K & V & O.OMap, +lo: O.OMap, +lb: Maybe<&2, K>, 1140 +ub: Maybe<&2, K>, +key: K, 1141 eka: {Laws.above(~K, ~cmp, lb, key) == True{} : Bool}, 1142 el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{key}) == True{} : Bool}, 1143 pmr: {PM(~K, ~V, ~cmp, Some{key}, ub, r) == True{} : Bool} 1144 ) -> {Laws.bounded(~K, ~V, ~cmp, O.OMap.glue.fin(K, V, lo, r), lb, ub) == True{} : Bool}: 1145 (mk, rest) = r 1146 (mv, t) = rest 1147 glue.fin.bnd.go(~K, ~V, ~cmp, ~trans, mk, mv, t, lo, lb, ub, key, eka, el, pmr) 1148 1149 def glue.bnd( 1150 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 1151 hi: O.OMap, +lo: O.OMap, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, 1152 +key: K, 1153 eka: {Laws.above(~K, ~cmp, lb, key) == True{} : Bool}, 1154 ekb: {Laws.below(~K, ~cmp, ub, key) == True{} : Bool}, 1155 el: {Laws.bounded(~K, ~V, ~cmp, lo, lb, Some{key}) == True{} : Bool}, 1156 eh: {Laws.bounded(~K, ~V, ~cmp, hi, Some{key}, ub) == True{} : Bool} 1157 ) -> {Laws.bounded(~K, ~V, ~cmp, O.OMap.glue(K, V, lo, hi), lb, ub) == True{} : Bool}: 1158 match hi: 1159 case O.OTip{}: 1160 weaken_hi(~K, ~V, ~cmp, ~trans, lo, lb, key, ub, el, ekb) 1161 case O.OBin{s, +k, +v, +hl, +hh}: 1162 glue.fin.bnd(~K, ~V, ~cmp, ~trans, O.OMap.pop_min(K, V, hl, k, v, hh), lo, lb, ub, key, 1163 eka, el, pm.bnd(~K, ~V, ~cmp, ~trans, hl, Some{key}, ub, k, v, hh, eh)) 1164 1165 def del.bnd( 1166 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, ~trans: Trans(~K, ~cmp), 1167 t: O.OMap, +lb: Maybe<&2, K>, +ub: Maybe<&2, K>, +k: K, 1168 +bt: {Laws.bounded(~K, ~V, ~cmp, t, lb, ub) == True{} : Bool} 1169 ) -> {Laws.bounded(~K, ~V, ~cmp, O.OMap.del(~K, ~V, ~cmp, t, k), lb, ub) == True{} : Bool}: 1170 match t: 1171 case O.OTip{}: 1172 {==} 1173 case O.OBin{+s, +key, +val, +lo, +hi}: 1174 +b_a = bn.a(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) 1175 +b_b = bn.b(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) 1176 +b_l = bn.l(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) 1177 +b_h = bn.h(~K, ~V, ~cmp, lb, ub, key, val, lo, hi, bt) 1178 cmp.split(O.OMap, Bool, y => Laws.bounded(~K, ~V, ~cmp, y, lb, ub), True{}, 1179 cmp(k, key), 1180 u => O.OMap.balance(K, V, key, val, O.OMap.del(~K, ~V, ~cmp, lo, k), hi), 1181 u => O.OMap.glue(K, V, lo, hi), 1182 u => O.OMap.balance(K, V, key, val, lo, O.OMap.del(~K, ~V, ~cmp, hi, k)), 1183 e => balance.bnd(~K, ~V, ~cmp, ~trans, lb, ub, key, val, 1184 O.OMap.del(~K, ~V, ~cmp, lo, k), hi, b_a, b_b, 1185 del.bnd(~K, ~V, ~cmp, ~trans, lo, lb, Some{key}, k, b_l), b_h), 1186 e => glue.bnd(~K, ~V, ~cmp, ~trans, hi, lo, lb, ub, key, b_a, b_b, b_l, b_h), 1187 e => balance.bnd(~K, ~V, ~cmp, ~trans, lb, ub, key, val, lo, 1188 O.OMap.del(~K, ~V, ~cmp, hi, k), b_a, b_b, b_l, 1189 del.bnd(~K, ~V, ~cmp, ~trans, hi, Some{key}, ub, k, b_h))) 1190 1191 def Laws.omap_del_searchtree(K, V, cmp, refl, eq, flip, trans, m, tree, k): 1192 del.bnd(~K, ~V, ~cmp, ~trans, m, None{}, None{}, k, tree) 1193 1194 def Laws.omap_new_weight_balanced(K, V): 1195 {==} 1196 1197 # --- weight balance ------------------------------------------------------------- 1198 1199 def W(-K: Data, -V: Data, t: O.OMap) -> Nat: 1200 Laws.omap_weight(K, V, t) 1201 1202 def WB(-K: Data, -V: Data, t: O.OMap) -> Bool: 1203 Laws.weight_balanced(K, V, t) 1204 1205 # t is balanced and its weight is within one of n. 1206 def PW(-K: Data, -V: Data, +n: Nat, +t: O.OMap) -> Bool: 1207 Bool.and(WB(K, V, t), Ord.near(n, W(K, V, t))) 1208 1209 def PMW(-K: Data, -V: Data, +n: Nat, r: K & V & O.OMap) -> Bool: 1210 (mk, mv, t) = r 1211 PW(K, V, n, t) 1212 1213 def pos_add(a: Nat, +b: Nat, e: Ord.LE(1n, a)) -> Ord.LE(1n, Nat.add(a, b)): 1214 match a: 1215 case 0n: 1216 Empty.absurd(Ord.LE(1n, b), MBool.false_ne_true()(e)) 1217 case 1n+p: 1218 MNat.zero_le(Nat.add(p, b)) 1219 1220 def w_pos(-K: Data, -V: Data, t: O.OMap) -> Ord.LE(1n, W(K, V, t)): 1221 match t: 1222 case O.OTip{}: 1223 {==} 1224 case O.OBin{s, k, v, +lo, +hi}: 1225 pos_add(W(K, V, lo), W(K, V, hi), w_pos(K, V, lo)) 1226 1227 def wb.ok( 1228 -K: Data, -V: Data, -k: K, -v: V, +lo: O.OMap, +hi: O.OMap, 1229 e: {WB(K, V, O.OBin{0, k, v, lo, hi}) == True{} : Bool} 1230 ) -> {Laws.weight_ok(W(K, V, lo), W(K, V, hi)) == True{} : Bool}: 1231 c3.a(Laws.weight_ok(W(K, V, lo), W(K, V, hi)), WB(K, V, lo), WB(K, V, hi), e) 1232 1233 def wb.l( 1234 -K: Data, -V: Data, -k: K, -v: V, +lo: O.OMap, +hi: O.OMap, 1235 e: {WB(K, V, O.OBin{0, k, v, lo, hi}) == True{} : Bool} 1236 ) -> {WB(K, V, lo) == True{} : Bool}: 1237 c3.b(Laws.weight_ok(W(K, V, lo), W(K, V, hi)), WB(K, V, lo), WB(K, V, hi), e) 1238 1239 def wb.h( 1240 -K: Data, -V: Data, -k: K, -v: V, +lo: O.OMap, +hi: O.OMap, 1241 e: {WB(K, V, O.OBin{0, k, v, lo, hi}) == True{} : Bool} 1242 ) -> {WB(K, V, hi) == True{} : Bool}: 1243 c3.c(Laws.weight_ok(W(K, V, lo), W(K, V, hi)), WB(K, V, lo), WB(K, V, hi), e) 1244 1245 def wb.i( 1246 -K: Data, -V: Data, -k: K, -v: V, +lo: O.OMap, +hi: O.OMap, 1247 eo: {Laws.weight_ok(W(K, V, lo), W(K, V, hi)) == True{} : Bool}, 1248 el: {WB(K, V, lo) == True{} : Bool}, eh: {WB(K, V, hi) == True{} : Bool} 1249 ) -> {WB(K, V, O.OBin{0, k, v, lo, hi}) == True{} : Bool}: 1250 c3.i(Laws.weight_ok(W(K, V, lo), W(K, V, hi)), WB(K, V, lo), WB(K, V, hi), eo, el, eh) 1251 1252 # Rotations toward lo, after hi grew or lo shrank by one. 1253 def rls.wb( 1254 -K: Data, -V: Data, +k: K, +v: V, +lo: O.OMap, +hk: K, +hv: V, 1255 +hl: O.OMap, +hh: O.OMap, 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)) 1276 1277 def rld.wb( 1278 -K: Data, -V: Data, hl: O.OMap, +k: K, +v: V, +lo: O.OMap, +hk: K, +hv: V, 1279 +hh: O.OMap, 1280 wbl: {WB(K, V, lo) == True{} : Bool}, 1281 +wbh: {WB(K, V, O.OBin{0, hk, hv, hl, hh}) == True{} : Bool}, 1282 +heavy: Ord.LE(1n+Nat.mul(3n, W(K, V, lo)), Nat.add(W(K, V, hl), W(K, V, hh))), 1283 +alm: Ord.LE(Nat.add(W(K, V, hl), W(K, V, hh)), Nat.add(3n, Nat.mul(3n, W(K, V, lo)))), 1284 +hd: Ord.LE(Nat.mul(2n, W(K, V, hh)), W(K, V, hl)) 1285 ) -> {WB(K, V, O.OMap.rot_lo.double(K, V, k, v, lo, hk, hv, hl, hh)) == True{} : Bool}: 1286 match hl: 1287 case O.OTip{}: 1288 Empty.absurd({WB(K, V, O.OMap.rot_lo.double(K, V, k, v, lo, hk, hv, O.OTip{}, hh)) == True{} : Bool}, Ord.dtip(W(K, V, hh), hd, w_pos(K, V, hh))) 1289 case O.OBin{s, +mk, +mv, +ml, +mh}: 1290 +hl = {O.OBin{0, mk, mv, ml, mh} : O.OMap} 1291 +l = W(K, V, lo) 1292 +x = W(K, V, ml) 1293 +y = W(K, V, mh) 1294 +b = W(K, V, hh) 1295 +okh = wb.ok(K, V, hk, hv, hl, hh, wbh) 1296 +h1 = Ord.wok_r(Nat.add(x, y), b, okh) 1297 +h2 = Ord.wok_l(Nat.add(x, y), b, okh) 1298 +wbm = wb.l(K, V, hk, hv, hl, hh, wbh) 1299 +okm = wb.ok(K, V, mk, mv, ml, mh, wbm) 1300 +h5 = Ord.wok_r(x, y, okm) 1301 +h6 = Ord.wok_l(x, y, okm) 1302 +pl = w_pos(K, V, lo) 1303 +px = w_pos(K, V, ml) 1304 +py = w_pos(K, V, mh) 1305 +pb = w_pos(K, V, hh) 1306 wb.i(K, V, mk, mv, O.OMap.bin(K, V, k, v, lo, ml), O.OMap.bin(K, V, hk, hv, mh, hh), 1307 Ord.rld.w0(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb), 1308 wb.i(K, V, k, v, lo, ml, Ord.rld.w1(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb), 1309 wbl, wb.l(K, V, mk, mv, ml, mh, wbm)), 1310 wb.i(K, V, hk, hv, mh, hh, Ord.rld.w2(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb), 1311 wb.h(K, V, mk, mv, ml, mh, wbm), wb.h(K, V, hk, hv, hl, hh, wbh))) 1312 1313 def rlp.wb( 1314 -K: Data, -V: Data, single: Bool, +k: K, +v: V, +lo: O.OMap, +hk: K, +hv: V, 1315 +hl: O.OMap, +hh: O.OMap, 1316 es: {Nat.is_lt(W(K, V, hl), Nat.mul(2n, W(K, V, hh))) == single : Bool}, 1317 wbl: {WB(K, V, lo) == True{} : Bool}, 1318 wbh: {WB(K, V, O.OBin{0, hk, hv, hl, hh}) == True{} : Bool}, 1319 heavy: Ord.LE(1n+Nat.mul(3n, W(K, V, lo)), Nat.add(W(K, V, hl), W(K, V, hh))), 1320 alm: Ord.LE(Nat.add(W(K, V, hl), W(K, V, hh)), Nat.add(3n, Nat.mul(3n, W(K, V, lo)))) 1321 ) -> {WB(K, V, O.OMap.rot_lo.pick(K, V, single, k, v, lo, hk, hv, hl, hh)) == True{} : Bool}: 1322 match single: 1323 case True{}: 1324 rls.wb(K, V, k, v, lo, hk, hv, hl, hh, wbl, wbh, heavy, alm, 1325 MNat.succ_le_of_lt(W(K, V, hl), Nat.mul(2n, W(K, V, hh)), es)) 1326 case False{}: 1327 rld.wb(K, V, hl, k, v, lo, hk, hv, hh, wbl, wbh, heavy, alm, 1328 MNat.le_of_not_lt(W(K, V, hl), Nat.mul(2n, W(K, V, hh)), es)) 1329 1330 def rl.wb( 1331 -K: Data, -V: Data, hi: O.OMap, +k: K, +v: V, +lo: O.OMap, 1332 wbl: {WB(K, V, lo) == True{} : Bool}, +wbh: {WB(K, V, hi) == True{} : Bool}, 1333 heavy: Ord.LE(1n+Nat.mul(3n, W(K, V, lo)), W(K, V, hi)), 1334 alm: Ord.LE(W(K, V, hi), Nat.add(3n, Nat.mul(3n, W(K, V, lo)))) 1335 ) -> {WB(K, V, Laws.g_rot_lo(K, V, k, v, lo, hi)) == True{} : Bool}: 1336 match hi: 1337 case O.OTip{}: 1338 Empty.absurd({WB(K, V, Laws.g_rot_lo(K, V, k, v, lo, O.OTip{})) == True{} : Bool}, Ord.tiph(W(K, V, lo), heavy, w_pos(K, V, lo))) 1339 case O.OBin{s, +hk, +hv, +hl, +hh}: 1340 rlp.wb(K, V, Nat.is_lt(W(K, V, hl), Nat.mul(2n, W(K, V, hh))), k, v, lo, hk, hv, hl, hh, 1341 {==}, wbl, wbh, heavy, alm) 1342 1343 # Rotations toward hi, after lo grew or hi shrank by one. 1344 def rhs.wb( 1345 -K: Data, -V: Data, +k: K, +v: V, +lk: K, +lv: V, +ll: O.OMap, 1346 +lh: O.OMap, +hi: O.OMap, 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)) 1367 1368 def rhd.wb( 1369 -K: Data, -V: Data, lh: O.OMap, +k: K, +v: V, +lk: K, +lv: V, 1370 +ll: O.OMap, +hi: O.OMap, 1371 +wbl: {WB(K, V, O.OBin{0, lk, lv, ll, lh}) == True{} : Bool}, 1372 wbh: {WB(K, V, hi) == True{} : Bool}, 1373 +heavy: Ord.LE(1n+Nat.mul(3n, W(K, V, hi)), Nat.add(W(K, V, ll), W(K, V, lh))), 1374 +alm: Ord.LE(Nat.add(W(K, V, ll), W(K, V, lh)), Nat.add(3n, Nat.mul(3n, W(K, V, hi)))), 1375 +hd: Ord.LE(Nat.mul(2n, W(K, V, ll)), W(K, V, lh)) 1376 ) -> {WB(K, V, O.OMap.rot_hi.double(K, V, k, v, lk, lv, ll, lh, hi)) == True{} : Bool}: 1377 match lh: 1378 case O.OTip{}: 1379 Empty.absurd({WB(K, V, O.OMap.rot_hi.double(K, V, k, v, lk, lv, ll, O.OTip{}, hi)) == True{} : Bool}, Ord.dtip(W(K, V, ll), hd, w_pos(K, V, ll))) 1380 case O.OBin{s, +mk, +mv, +ml, +mh}: 1381 +lh = {O.OBin{0, mk, mv, ml, mh} : O.OMap} 1382 +l = W(K, V, hi) 1383 +x = W(K, V, mh) 1384 +y = W(K, V, ml) 1385 +b = W(K, V, ll) 1386 +okl = wb.ok(K, V, lk, lv, ll, lh, wbl) 1387 +h1 = Ord.wok_l(b, Nat.add(y, x), okl) 1388 +h2 = Ord.wok_r(b, Nat.add(y, x), okl) 1389 +wbm = wb.h(K, V, lk, lv, ll, lh, wbl) 1390 +okm = wb.ok(K, V, mk, mv, ml, mh, wbm) 1391 +h5 = Ord.wok_l(y, x, okm) 1392 +h6 = Ord.wok_r(y, x, okm) 1393 +pl = w_pos(K, V, hi) 1394 +px = w_pos(K, V, mh) 1395 +py = w_pos(K, V, ml) 1396 +pb = w_pos(K, V, ll) 1397 wb.i(K, V, mk, mv, O.OMap.bin(K, V, lk, lv, ll, ml), O.OMap.bin(K, V, k, v, mh, hi), 1398 Ord.rhd.w0(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb), 1399 wb.i(K, V, lk, lv, ll, ml, Ord.rhd.w1(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb), 1400 wb.l(K, V, lk, lv, ll, lh, wbl), wb.l(K, V, mk, mv, ml, mh, wbm)), 1401 wb.i(K, V, k, v, mh, hi, Ord.rhd.w2(l, x, y, b, h1, h2, heavy, alm, hd, h5, h6, pl, px, py, pb), 1402 wb.h(K, V, mk, mv, ml, mh, wbm), wbh)) 1403 1404 def rhp.wb( 1405 -K: Data, -V: Data, single: Bool, +k: K, +v: V, +lk: K, +lv: V, +ll: O.OMap, 1406 +lh: O.OMap, +hi: O.OMap, 1407 es: {Nat.is_lt(W(K, V, lh), Nat.mul(2n, W(K, V, ll))) == single : Bool}, 1408 wbl: {WB(K, V, O.OBin{0, lk, lv, ll, lh}) == True{} : Bool}, 1409 wbh: {WB(K, V, hi) == True{} : Bool}, 1410 heavy: Ord.LE(1n+Nat.mul(3n, W(K, V, hi)), Nat.add(W(K, V, ll), W(K, V, lh))), 1411 alm: Ord.LE(Nat.add(W(K, V, ll), W(K, V, lh)), Nat.add(3n, Nat.mul(3n, W(K, V, hi)))) 1412 ) -> {WB(K, V, O.OMap.rot_hi.pick(K, V, single, k, v, lk, lv, ll, lh, hi)) == True{} : Bool}: 1413 match single: 1414 case True{}: 1415 rhs.wb(K, V, k, v, lk, lv, ll, lh, hi, wbl, wbh, heavy, alm, 1416 MNat.succ_le_of_lt(W(K, V, lh), Nat.mul(2n, W(K, V, ll)), es)) 1417 case False{}: 1418 rhd.wb(K, V, lh, k, v, lk, lv, ll, hi, wbl, wbh, heavy, alm, 1419 MNat.le_of_not_lt(W(K, V, lh), Nat.mul(2n, W(K, V, ll)), es)) 1420 1421 def rh.wb( 1422 -K: Data, -V: Data, lo: O.OMap, +k: K, +v: V, +hi: O.OMap, 1423 +wbl: {WB(K, V, lo) == True{} : Bool}, wbh: {WB(K, V, hi) == True{} : Bool}, 1424 heavy: Ord.LE(1n+Nat.mul(3n, W(K, V, hi)), W(K, V, lo)), 1425 alm: Ord.LE(W(K, V, lo), Nat.add(3n, Nat.mul(3n, W(K, V, hi)))) 1426 ) -> {WB(K, V, Laws.g_rot_hi(K, V, k, v, lo, hi)) == True{} : Bool}: 1427 match lo: 1428 case O.OTip{}: 1429 Empty.absurd({WB(K, V, Laws.g_rot_hi(K, V, k, v, O.OTip{}, hi)) == True{} : Bool}, Ord.tiph(W(K, V, hi), heavy, w_pos(K, V, hi))) 1430 case O.OBin{s, +lk, +lv, +ll, +lh}: 1431 rhp.wb(K, V, Nat.is_lt(W(K, V, lh), Nat.mul(2n, W(K, V, ll))), k, v, lk, lv, ll, lh, hi, 1432 {==}, wbl, wbh, heavy, alm) 1433 1434 def bif.wb( 1435 -K: Data, -V: Data, heavy_hi: Bool, heavy_lo: Bool, +k: K, +v: V, 1436 +lo: O.OMap, +hi: O.OMap, 1437 eh: {Laws.g_heavy_hi(K, V, lo, hi) == heavy_hi : Bool}, 1438 el: {Laws.g_heavy_lo(K, V, lo, hi) == heavy_lo : Bool}, 1439 wbl: {WB(K, V, lo) == True{} : Bool}, wbh: {WB(K, V, hi) == True{} : Bool}, 1440 +alm: {Ord.alm(W(K, V, lo), W(K, V, hi)) == True{} : Bool} 1441 ) -> {WB(K, V, Laws.g_balance.if(K, V, heavy_hi, heavy_lo, k, v, lo, hi)) == True{} : Bool}: 1442 match heavy_hi heavy_lo: 1443 case True{} _: 1444 rl.wb(K, V, hi, k, v, lo, wbl, wbh, 1445 Ord.gt_le(W(K, V, hi), Nat.mul(3n, W(K, V, lo)), eh), MBool.eq_true_of_and_left(Nat.is_le(W(K, V, hi), Nat.add(3n, Nat.mul(3n, W(K, V, lo)))), Nat.is_le(W(K, V, lo), Nat.add(3n, Nat.mul(3n, W(K, V, hi)))), alm)) 1446 case False{} True{}: 1447 rh.wb(K, V, lo, k, v, hi, wbl, wbh, 1448 Ord.gt_le(W(K, V, lo), Nat.mul(3n, W(K, V, hi)), el), MBool.eq_true_of_and_right(Nat.is_le(W(K, V, hi), Nat.add(3n, Nat.mul(3n, W(K, V, lo)))), Nat.is_le(W(K, V, lo), Nat.add(3n, Nat.mul(3n, W(K, V, hi)))), alm)) 1449 case False{} False{}: 1450 wb.i(K, V, k, v, lo, hi, 1451 MBool.and_eq_true(Nat.is_le(W(K, V, hi), Nat.mul(3n, W(K, V, lo))), Nat.is_le(W(K, V, lo), Nat.mul(3n, W(K, V, hi))), Ord.ngt_le(W(K, V, hi), Nat.mul(3n, W(K, V, lo)), eh), Ord.ngt_le(W(K, V, lo), Nat.mul(3n, W(K, V, hi)), el)), 1452 wbl, wbh) 1453 1454 def bal.wb( 1455 -K: Data, -V: Data, +k: K, +v: V, +lo: O.OMap, +hi: O.OMap, 1456 wbl: {WB(K, V, lo) == True{} : Bool}, wbh: {WB(K, V, hi) == True{} : Bool}, 1457 alm: {Ord.alm(W(K, V, lo), W(K, V, hi)) == True{} : Bool} 1458 ) -> {WB(K, V, Laws.g_balance(K, V, k, v, lo, hi)) == True{} : Bool}: 1459 bif.wb(K, V, Laws.g_heavy_hi(K, V, lo, hi), Laws.g_heavy_lo(K, V, lo, hi), k, v, lo, hi, 1460 {==}, {==}, wbl, wbh, alm) 1461 1462 # Balancing keeps the weight. 1463 def rlp.w( 1464 -K: Data, -V: Data, single: Bool, -k: K, -v: V, +lo: O.OMap, -hk: K, -hv: V, 1465 hl: O.OMap, +hh: O.OMap 1466 ) -> {Nat.add(W(K, V, lo), Nat.add(W(K, V, hl), W(K, V, hh))) 1467 == W(K, V, O.OMap.rot_lo.pick(K, V, single, k, v, lo, hk, hv, hl, hh)) : Nat}: 1468 match single hl: 1469 case True{} +hl: 1470 Ord.sy(Nat.add(Nat.add(W(K, V, lo), W(K, V, hl)), W(K, V, hh)), 1471 Nat.add(W(K, V, lo), Nat.add(W(K, V, hl), W(K, V, hh))), 1472 MNat.add_assoc(W(K, V, lo), W(K, V, hl), W(K, V, hh))) 1473 case False{} O.OTip{}: 1474 Ord.sy(Nat.add(Nat.add(W(K, V, lo), 1n), W(K, V, hh)), Nat.add(W(K, V, lo), Nat.add(1n, W(K, V, hh))), 1475 MNat.add_assoc(W(K, V, lo), 1n, W(K, V, hh))) 1476 case False{} O.OBin{s, mk, mv, +ml, +mh}: 1477 +l = W(K, V, lo) 1478 +x = W(K, V, ml) 1479 +y = W(K, V, mh) 1480 +b = W(K, V, hh) 1481 Ord.tr(Nat.add(l, Nat.add(Nat.add(x, y), b)), Nat.add(l, Nat.add(x, Nat.add(y, b))), 1482 Nat.add(Nat.add(l, x), Nat.add(y, b)), 1483 Ord.cong_add(l, l, Nat.add(Nat.add(x, y), b), Nat.add(x, Nat.add(y, b)), {==}, MNat.add_assoc(x, y, b)), 1484 Ord.sy(Nat.add(Nat.add(l, x), Nat.add(y, b)), Nat.add(l, Nat.add(x, Nat.add(y, b))), 1485 MNat.add_assoc(l, x, Nat.add(y, b)))) 1486 1487 def rhp.w( 1488 -K: Data, -V: Data, single: Bool, -k: K, -v: V, -lk: K, -lv: V, +ll: O.OMap, 1489 lh: O.OMap, +hi: O.OMap 1490 ) -> {Nat.add(Nat.add(W(K, V, ll), W(K, V, lh)), W(K, V, hi)) 1491 == W(K, V, O.OMap.rot_hi.pick(K, V, single, k, v, lk, lv, ll, lh, hi)) : Nat}: 1492 match single lh: 1493 case True{} +lh: 1494 MNat.add_assoc(W(K, V, ll), W(K, V, lh), W(K, V, hi)) 1495 case False{} O.OTip{}: 1496 MNat.add_assoc(W(K, V, ll), 1n, W(K, V, hi)) 1497 case False{} O.OBin{s, mk, mv, +ml, +mh}: 1498 +l = W(K, V, hi) 1499 +x = W(K, V, mh) 1500 +y = W(K, V, ml) 1501 +b = W(K, V, ll) 1502 Ord.tr(Nat.add(Nat.add(b, Nat.add(y, x)), l), Nat.add(Nat.add(Nat.add(b, y), x), l), 1503 Nat.add(Nat.add(b, y), Nat.add(x, l)), 1504 Ord.cong_add(Nat.add(b, Nat.add(y, x)), Nat.add(Nat.add(b, y), x), l, l, 1505 Ord.sy(Nat.add(Nat.add(b, y), x), Nat.add(b, Nat.add(y, x)), MNat.add_assoc(b, y, x)), {==}), 1506 MNat.add_assoc(Nat.add(b, y), x, l)) 1507 1508 def rl.w(-K: Data, -V: Data, hi: O.OMap, -k: K, -v: V, +lo: O.OMap) 1509 -> {Nat.add(W(K, V, lo), W(K, V, hi)) == W(K, V, Laws.g_rot_lo(K, V, k, v, lo, hi)) : Nat}: 1510 match hi: 1511 case O.OTip{}: 1512 {==} 1513 case O.OBin{s, hk, hv, +hl, +hh}: 1514 rlp.w(K, V, Nat.is_lt(W(K, V, hl), Nat.mul(2n, W(K, V, hh))), k, v, lo, hk, hv, hl, hh) 1515 1516 def rh.w(-K: Data, -V: Data, lo: O.OMap, -k: K, -v: V, +hi: O.OMap) 1517 -> {Nat.add(W(K, V, lo), W(K, V, hi)) == W(K, V, Laws.g_rot_hi(K, V, k, v, lo, hi)) : Nat}: 1518 match lo: 1519 case O.OTip{}: 1520 {==} 1521 case O.OBin{s, lk, lv, +ll, +lh}: 1522 rhp.w(K, V, Nat.is_lt(W(K, V, lh), Nat.mul(2n, W(K, V, ll))), k, v, lk, lv, ll, lh, hi) 1523 1524 def bif.w( 1525 -K: Data, -V: Data, heavy_hi: Bool, heavy_lo: Bool, -k: K, -v: V, 1526 +lo: O.OMap, +hi: O.OMap 1527 ) -> {Nat.add(W(K, V, lo), W(K, V, hi)) 1528 == W(K, V, Laws.g_balance.if(K, V, heavy_hi, heavy_lo, k, v, lo, hi)) : Nat}: 1529 match heavy_hi heavy_lo: 1530 case True{} _: 1531 rl.w(K, V, hi, k, v, lo) 1532 case False{} True{}: 1533 rh.w(K, V, lo, k, v, hi) 1534 case False{} False{}: 1535 {==} 1536 1537 def bal.w(-K: Data, -V: Data, -k: K, -v: V, +lo: O.OMap, +hi: O.OMap) 1538 -> {Nat.add(W(K, V, lo), W(K, V, hi)) == W(K, V, Laws.g_balance(K, V, k, v, lo, hi)) : Nat}: 1539 bif.w(K, V, Laws.g_heavy_hi(K, V, lo, hi), Laws.g_heavy_lo(K, V, lo, hi), k, v, lo, hi) 1540 1541 def bal.lo.near( 1542 -K: Data, -V: Data, -k: K, -v: V, +lo: O.OMap, +lo2: O.OMap, +hi: O.OMap, 1543 n1: Ord.LE(W(K, V, lo), 1n+W(K, V, lo2)), n2: Ord.LE(W(K, V, lo2), 1n+W(K, V, lo)) 1544 ) -> {Ord.near(Nat.add(W(K, V, lo), W(K, V, hi)), W(K, V, Laws.g_balance(K, V, k, v, lo2, hi))) == True{} : Bool}: 1545 %bal.w(K, V, k, v, lo2, hi) : {Ord.near(Nat.add(W(K, V, lo), W(K, V, hi)), _) == True{} : Bool} 1546 Ord.nearlo.w0(W(K, V, lo), W(K, V, lo2), W(K, V, hi), n1, n2) 1547 1548 def bal.hi.near( 1549 -K: Data, -V: Data, -k: K, -v: V, +lo: O.OMap, +hi: O.OMap, +hi2: O.OMap, 1550 n1: Ord.LE(W(K, V, hi), 1n+W(K, V, hi2)), n2: Ord.LE(W(K, V, hi2), 1n+W(K, V, hi)) 1551 ) -> {Ord.near(Nat.add(W(K, V, lo), W(K, V, hi)), W(K, V, Laws.g_balance(K, V, k, v, lo, hi2))) == True{} : Bool}: 1552 %bal.w(K, V, k, v, lo, hi2) : {Ord.near(Nat.add(W(K, V, lo), W(K, V, hi)), _) == True{} : Bool} 1553 Ord.nearhi.w0(W(K, V, lo), W(K, V, hi), W(K, V, hi2), n1, n2) 1554 1555 # lo became lo2, one lighter or heavier at most: rebalance the node. 1556 def bal.lo( 1557 -K: Data, -V: Data, +k: K, +v: V, +lo: O.OMap, +lo2: O.OMap, +hi: O.OMap, 1558 +ok: {Laws.weight_ok(W(K, V, lo), W(K, V, hi)) == True{} : Bool}, 1559 wbh: {WB(K, V, hi) == True{} : Bool}, 1560 +pw: {PW(K, V, W(K, V, lo), lo2) == True{} : Bool} 1561 ) -> {PW(K, V, Nat.add(W(K, V, lo), W(K, V, hi)), Laws.g_balance(K, V, k, v, lo2, hi)) == True{} : Bool}: 1562 +a = W(K, V, lo) 1563 +a2 = W(K, V, lo2) 1564 +c = W(K, V, hi) 1565 +nr = MBool.eq_true_of_and_right(WB(K, V, lo2), Ord.near(a, a2), pw) 1566 +n1 = MBool.eq_true_of_and_left(Nat.is_le(a, 1n+a2), Nat.is_le(a2, 1n+a), nr) 1567 +n2 = MBool.eq_true_of_and_right(Nat.is_le(a, 1n+a2), Nat.is_le(a2, 1n+a), nr) 1568 MBool.and_eq_true(WB(K, V, Laws.g_balance(K, V, k, v, lo2, hi)), Ord.near(Nat.add(a, c), W(K, V, Laws.g_balance(K, V, k, v, lo2, hi))), bal.wb(K, V, k, v, lo2, hi, MBool.eq_true_of_and_left(WB(K, V, lo2), Ord.near(a, a2), pw), wbh, 1569 Ord.almlo.w0(a, c, a2, Ord.wok_l(a, c, ok), Ord.wok_r(a, c, ok), n1, n2)), bal.lo.near(K, V, k, v, lo, lo2, hi, n1, n2)) 1570 1571 def bal.hi( 1572 -K: Data, -V: Data, +k: K, +v: V, +lo: O.OMap, +hi: O.OMap, +hi2: O.OMap, 1573 +ok: {Laws.weight_ok(W(K, V, lo), W(K, V, hi)) == True{} : Bool}, 1574 wbl: {WB(K, V, lo) == True{} : Bool}, 1575 +pw: {PW(K, V, W(K, V, hi), hi2) == True{} : Bool} 1576 ) -> {PW(K, V, Nat.add(W(K, V, lo), W(K, V, hi)), Laws.g_balance(K, V, k, v, lo, hi2)) == True{} : Bool}: 1577 +a = W(K, V, lo) 1578 +c = W(K, V, hi) 1579 +c2 = W(K, V, hi2) 1580 +nr = MBool.eq_true_of_and_right(WB(K, V, hi2), Ord.near(c, c2), pw) 1581 +n1 = MBool.eq_true_of_and_left(Nat.is_le(c, 1n+c2), Nat.is_le(c2, 1n+c), nr) 1582 +n2 = MBool.eq_true_of_and_right(Nat.is_le(c, 1n+c2), Nat.is_le(c2, 1n+c), nr) 1583 MBool.and_eq_true(WB(K, V, Laws.g_balance(K, V, k, v, lo, hi2)), Ord.near(Nat.add(a, c), W(K, V, Laws.g_balance(K, V, k, v, lo, hi2))), bal.wb(K, V, k, v, lo, hi2, wbl, MBool.eq_true_of_and_left(WB(K, V, hi2), Ord.near(c, c2), pw), 1584 Ord.almhi.w0(a, c, c2, Ord.wok_l(a, c, ok), Ord.wok_r(a, c, ok), n1, n2)), bal.hi.near(K, V, k, v, lo, hi, hi2, n1, n2)) 1585 1586 def put.wb( 1587 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, t: O.OMap, +k: K, +v: V, 1588 +wb: {WB(K, V, t) == True{} : Bool} 1589 ) -> {PW(K, V, W(K, V, t), Laws.g_put(~K, ~V, ~cmp, t, k, v)) == True{} : Bool}: 1590 match t: 1591 case O.OTip{}: 1592 {==} 1593 case O.OBin{+s, +key, +val, +lo, +hi}: 1594 +ok = wb.ok(K, V, key, val, lo, hi, wb) 1595 +wbl = wb.l(K, V, key, val, lo, hi, wb) 1596 +wbh = wb.h(K, V, key, val, lo, hi, wb) 1597 +n = Nat.add(W(K, V, lo), W(K, V, hi)) 1598 cmp.split(O.OMap, Bool, x => PW(K, V, n, x), True{}, cmp(k, key), 1599 u => Laws.g_balance(K, V, key, val, Laws.g_put(~K, ~V, ~cmp, lo, k, v), hi), 1600 u => O.OBin{s, key, v, lo, hi}, 1601 u => Laws.g_balance(K, V, key, val, lo, Laws.g_put(~K, ~V, ~cmp, hi, k, v)), 1602 e => bal.lo(K, V, key, val, lo, Laws.g_put(~K, ~V, ~cmp, lo, k, v), hi, ok, wbh, 1603 put.wb(~K, ~V, ~cmp, lo, k, v, wbl)), 1604 e => MBool.and_eq_true(WB(K, V, O.OBin{s, key, v, lo, hi}), Ord.near(n, n), wb, Ord.nearrf.w0(n)), 1605 e => bal.hi(K, V, key, val, lo, hi, Laws.g_put(~K, ~V, ~cmp, hi, k, v), ok, wbl, 1606 put.wb(~K, ~V, ~cmp, hi, k, v, wbh))) 1607 1608 def Laws.omap_put_weight_balanced(K, V, cmp, m, wb, k, v): 1609 MBool.eq_true_of_and_left(WB(K, V, Laws.g_put(~K, ~V, ~cmp, m, k, v)), Ord.near(W(K, V, m), W(K, V, Laws.g_put(~K, ~V, ~cmp, m, k, v))), put.wb(~K, ~V, ~cmp, m, k, v, wb)) 1610 1611 def pm.fin.wb.go( 1612 -K: Data, -V: Data, +mk: K, +mv: V, +t: O.OMap, +k: K, +v: V, 1613 +lo: O.OMap, +hi: O.OMap, 1614 ok: {Laws.weight_ok(W(K, V, lo), W(K, V, hi)) == True{} : Bool}, 1615 wbh: {WB(K, V, hi) == True{} : Bool}, 1616 ih: {PMW(K, V, W(K, V, lo), {(mk, mv, t) : K & V & O.OMap}) == True{} : Bool} 1617 ) -> {PMW(K, V, Nat.add(W(K, V, lo), W(K, V, hi)), 1618 Laws.g_pop_min.fin(K, V, k, v, hi, {(mk, mv, t) : K & V & O.OMap})) == True{} : Bool}: 1619 bal.lo(K, V, k, v, lo, t, hi, ok, wbh, ih) 1620 1621 # Workaround for https://github.com/bendlang/bend/issues/1077: bind the tuple without +. 1622 def pm.fin.wb( 1623 -K: Data, -V: Data, r: K & V & O.OMap, +k: K, +v: V, 1624 +lo: O.OMap, +hi: O.OMap, 1625 ok: {Laws.weight_ok(W(K, V, lo), W(K, V, hi)) == True{} : Bool}, 1626 wbh: {WB(K, V, hi) == True{} : Bool}, 1627 ih: {PMW(K, V, W(K, V, lo), r) == True{} : Bool} 1628 ) -> {PMW(K, V, Nat.add(W(K, V, lo), W(K, V, hi)), Laws.g_pop_min.fin(K, V, k, v, hi, r)) == True{} : Bool}: 1629 (mk, rest) = r 1630 (mv, t) = rest 1631 pm.fin.wb.go(K, V, mk, mv, t, k, v, lo, hi, ok, wbh, ih) 1632 1633 def pm.wb( 1634 -K: Data, -V: Data, lo: O.OMap, +k: K, +v: V, +hi: O.OMap, 1635 +e: {WB(K, V, O.OBin{0, k, v, lo, hi}) == True{} : Bool} 1636 ) -> {PMW(K, V, Nat.add(W(K, V, lo), W(K, V, hi)), Laws.g_pop_min(K, V, lo, k, v, hi)) == True{} : Bool}: 1637 match lo: 1638 case O.OTip{}: 1639 MBool.and_eq_true(WB(K, V, hi), Ord.near(1n+W(K, V, hi), W(K, V, hi)), wb.h(K, V, k, v, O.OTip{}, hi, e), Ord.nearpm.w0(W(K, V, hi))) 1640 case O.OBin{s, +lk, +lv, +ll, +lh}: 1641 +lo = {O.OBin{0, lk, lv, ll, lh} : O.OMap} 1642 pm.fin.wb(K, V, Laws.g_pop_min(K, V, ll, lk, lv, lh), k, v, lo, hi, 1643 wb.ok(K, V, k, v, lo, hi, e), wb.h(K, V, k, v, lo, hi, e), 1644 pm.wb(K, V, ll, lk, lv, lh, wb.l(K, V, k, v, lo, hi, e))) 1645 1646 def glue.fin.wb.go( 1647 -K: Data, -V: Data, +mk: K, +mv: V, +t: O.OMap, +lo: O.OMap, +hi: O.OMap, 1648 ok: {Laws.weight_ok(W(K, V, lo), W(K, V, hi)) == True{} : Bool}, 1649 wbl: {WB(K, V, lo) == True{} : Bool}, 1650 pmr: {PMW(K, V, W(K, V, hi), {(mk, mv, t) : K & V & O.OMap}) == True{} : Bool} 1651 ) -> {PW(K, V, Nat.add(W(K, V, lo), W(K, V, hi)), 1652 Laws.g_glue.fin(K, V, lo, {(mk, mv, t) : K & V & O.OMap})) == True{} : Bool}: 1653 bal.hi(K, V, mk, mv, lo, hi, t, ok, wbl, pmr) 1654 1655 # Workaround for https://github.com/bendlang/bend/issues/1077: bind the tuple without +. 1656 def glue.fin.wb( 1657 -K: Data, -V: Data, r: K & V & O.OMap, +lo: O.OMap, +hi: O.OMap, 1658 ok: {Laws.weight_ok(W(K, V, lo), W(K, V, hi)) == True{} : Bool}, 1659 wbl: {WB(K, V, lo) == True{} : Bool}, 1660 pmr: {PMW(K, V, W(K, V, hi), r) == True{} : Bool} 1661 ) -> {PW(K, V, Nat.add(W(K, V, lo), W(K, V, hi)), Laws.g_glue.fin(K, V, lo, r)) == True{} : Bool}: 1662 (mk, rest) = r 1663 (mv, t) = rest 1664 glue.fin.wb.go(K, V, mk, mv, t, lo, hi, ok, wbl, pmr) 1665 1666 def glue.wb( 1667 -K: Data, -V: Data, hi: O.OMap, +lo: O.OMap, -key: K, -val: V, 1668 +e: {WB(K, V, O.OBin{0, key, val, lo, hi}) == True{} : Bool} 1669 ) -> {PW(K, V, Nat.add(W(K, V, lo), W(K, V, hi)), Laws.g_glue(K, V, lo, hi)) == True{} : Bool}: 1670 match hi: 1671 case O.OTip{}: 1672 MBool.and_eq_true(WB(K, V, lo), Ord.near(Nat.add(W(K, V, lo), 1n), W(K, V, lo)), wb.l(K, V, key, val, lo, O.OTip{}, e), Ord.neargt.w0(W(K, V, lo))) 1673 case O.OBin{s, +k, +v, +hl, +hh}: 1674 +hi = {O.OBin{0, k, v, hl, hh} : O.OMap} 1675 glue.fin.wb(K, V, Laws.g_pop_min(K, V, hl, k, v, hh), lo, hi, 1676 wb.ok(K, V, key, val, lo, hi, e), wb.l(K, V, key, val, lo, hi, e), 1677 pm.wb(K, V, hl, k, v, hh, wb.h(K, V, key, val, lo, hi, e))) 1678 1679 def del.wb( 1680 ~K: Data, ~V: Data, ~cmp: K -> K -> Cmp, t: O.OMap, +k: K, 1681 +wb: {WB(K, V, t) == True{} : Bool} 1682 ) -> {PW(K, V, W(K, V, t), Laws.g_del(~K, ~V, ~cmp, t, k)) == True{} : Bool}: 1683 match t: 1684 case O.OTip{}: 1685 {==} 1686 case O.OBin{+s, +key, +val, +lo, +hi}: 1687 +ok = wb.ok(K, V, key, val, lo, hi, wb) 1688 +wbl = wb.l(K, V, key, val, lo, hi, wb) 1689 +wbh = wb.h(K, V, key, val, lo, hi, wb) 1690 +n = Nat.add(W(K, V, lo), W(K, V, hi)) 1691 cmp.split(O.OMap, Bool, x => PW(K, V, n, x), True{}, cmp(k, key), 1692 u => Laws.g_balance(K, V, key, val, Laws.g_del(~K, ~V, ~cmp, lo, k), hi), 1693 u => Laws.g_glue(K, V, lo, hi), 1694 u => Laws.g_balance(K, V, key, val, lo, Laws.g_del(~K, ~V, ~cmp, hi, k)), 1695 e => bal.lo(K, V, key, val, lo, Laws.g_del(~K, ~V, ~cmp, lo, k), hi, ok, wbh, 1696 del.wb(~K, ~V, ~cmp, lo, k, wbl)), 1697 e => glue.wb(K, V, hi, lo, key, val, wb), 1698 e => bal.hi(K, V, key, val, lo, hi, Laws.g_del(~K, ~V, ~cmp, hi, k), ok, wbl, 1699 del.wb(~K, ~V, ~cmp, hi, k, wbh))) 1700 1701 def Laws.omap_del_weight_balanced(K, V, cmp, m, wb, k): 1702 MBool.eq_true_of_and_left(WB(K, V, Laws.g_del(~K, ~V, ~cmp, m, k)), Ord.near(W(K, V, m), W(K, V, Laws.g_del(~K, ~V, ~cmp, m, k))), del.wb(~K, ~V, ~cmp, m, k, wb)) 1703 1704 def Laws.omap_g_put_matches(): 1705 {==} 1706 1707 def Laws.omap_g_del_matches(): 1708 {==} 1709 1710 def Laws.hmap_get_put(): 1711 {==} 1712 1713 def Laws.hmap_get_put_other(): 1714 {==} 1715 1716 def Laws.hmap_collision(): 1717 {==} 1718 1719 def Laws.hmap_replace_collision(): 1720 {==} 1721 1722 def Laws.hmap_high_bit(): 1723 {==} 1724 1725 def Laws.hmap_missing_collision(): 1726 {==} 1727 1728 # --- hmap ------------------------------------------------------------------------ 1729 1730 def h.sb(-a: Bool, -b: Bool, e: {a == b : Bool}) -> {b == a : Bool}: 1731 Equal.sym(Bool, a, b, e) 1732 1733 def h.tf(-A: Type, -b: Bool, et: {b == True{} : Bool}, ef: {b == False{} : Bool}) -> A: 1734 Empty.absurd(A, MBool.false_ne_true()(Equal.trans(Bool, False{}, b, True{}, Equal.sym(Bool, b, False{}, ef), et))) 1735 1736 def h.isS(-V: Data, m: Maybe<&2, V>) -> Type: 1737 match m: 1738 case None{}: 1739 Empty 1740 case Some{x}: 1741 Unit 1742 1743 def h.some_none.e(-V: Data, -x: V, e: {Some{x} == None{} : Maybe<&2, V>}) -> Empty: 1744 %e : h.isS(V, _) 1745 Unit{} 1746 1747 def h.some_none(-A: Type, -V: Data, -x: V, e: {Some{x} == None{} : Maybe<&2, V>}) -> A: 1748 Empty.absurd(A, h.some_none.e(V, x, e)) 1749 1750 def h.none_some(-A: Type, -V: Data, -x: V, e: {None{} == Some{x} : Maybe<&2, V>}) -> A: 1751 Empty.absurd(A, h.some_none.e(V, x, Equal.sym(Maybe<&2, V>, None{}, Some{x}, e))) 1752 1753 # U32 equality is Word equality, so is_eq is reflexive and sound. 1754 def h.wcmp_refl(n: Nat, w: Word(n)) -> {Word.cmp(n, w, w) == EQ{} : Cmp}: 1755 match n: 1756 case 0n: 1757 {==} 1758 case 1n+p: 1759 match w: 1760 case WCon{+b, +t}: 1761 %Equal.sym(Cmp, Word.cmp(p, t, t), EQ{}, h.wcmp_refl(p, t)) : {Word.cmp.fin(b, b, _) == EQ{} : Cmp} 1762 MBool.cmp_refl(b) 1763 1764 def h.u_refl(x: U32) -> {U32.is_eq(x, x) == True{} : Bool}: 1765 match x: 1766 case U32{+w}: 1767 %Equal.sym(Cmp, Word.cmp(32n, w, w), EQ{}, h.wcmp_refl(32n, w)) : {Cmp.is_eq(_) == True{} : Bool} 1768 {==} 1769 1770 def h.fin_eq(t: Cmp, -x: Bool, -y: Bool, e: {Cmp.is_eq(Word.cmp.fin(x, y, t)) == True{} : Bool}) 1771 -> {Cmp.is_eq(t) == True{} : Bool}: 1772 match t: 1773 case LT{}: 1774 Empty.absurd({Cmp.is_eq(LT{}) == True{} : Bool}, MBool.false_ne_true()(e)) 1775 case EQ{}: 1776 {==} 1777 case GT{}: 1778 Empty.absurd({Cmp.is_eq(GT{}) == True{} : Bool}, MBool.false_ne_true()(e)) 1779 1780 def h.fin_hd(t: Cmp, x: Bool, y: Bool, e: {Cmp.is_eq(Word.cmp.fin(x, y, t)) == True{} : Bool}) 1781 -> {x == y : Bool}: 1782 match t: 1783 case LT{}: 1784 Empty.absurd({x == y : Bool}, MBool.false_ne_true()(e)) 1785 case EQ{}: 1786 match x y: 1787 case False{} False{}: 1788 {==} 1789 case False{} True{}: 1790 Empty.absurd({False{} == True{} : Bool}, MBool.false_ne_true()(e)) 1791 case True{} False{}: 1792 Empty.absurd({True{} == False{} : Bool}, MBool.false_ne_true()(e)) 1793 case True{} True{}: 1794 {==} 1795 case GT{}: 1796 Empty.absurd({x == y : Bool}, MBool.false_ne_true()(e)) 1797 1798 def h.wcmp_sound(+n: Nat, a: Word(n), b: Word(n), +e: {Cmp.is_eq(Word.cmp(n, a, b)) == True{} : Bool}) 1799 -> {a == b : Word(n)}: 1800 match n: 1801 case 0n: 1802 match a b: 1803 case WNil{} WNil{}: 1804 {==} 1805 case 1n+p: 1806 match a b: 1807 case WCon{+x, +at} WCon{+y, +bt}: 1808 +e1 = h.fin_hd(Word.cmp(p, at, bt), x, y, e) 1809 +e2 = h.wcmp_sound(p, at, bt, h.fin_eq(Word.cmp(p, at, bt), x, y, e)) 1810 %e1 : {WCon{x, at} == WCon{_, bt} : Word(1n+p)} 1811 %e2 : {WCon{x, at} == WCon{x, _} : Word(1n+p)} 1812 {==} 1813 1814 def h.u_sound(a: U32, b: U32, e: {U32.is_eq(a, b) == True{} : Bool}) -> {a == b : U32}: 1815 match a b: 1816 case U32{+x} U32{+y}: 1817 %h.wcmp_sound(32n, x, y, e) : {U32{x} == U32{_} : U32} 1818 {==} 1819 1820 # A mask with at most one set bit routes every hash to one of two sides. 1821 def h.isz(n: Nat, w: Word(n)) -> Bool: 1822 match n: 1823 case 0n: 1824 True{} 1825 case 1n+p: 1826 match w: 1827 case WCon{b, t}: 1828 Bool.not(b) && h.isz(p, t) 1829 1830 def h.at1(n: Nat, w: Word(n)) -> Bool: 1831 match n: 1832 case 0n: 1833 True{} 1834 case 1n+p: 1835 match w: 1836 case WCon{b, t}: 1837 match b: 1838 case True{}: 1839 h.isz(p, t) 1840 case False{}: 1841 h.at1(p, t) 1842 1843 def h.onebit(m: U32) -> Bool: 1844 match m: 1845 case U32{w}: 1846 h.at1(32n, w) 1847 1848 def h.and_z(+n: Nat, x: Word(n), m: Word(n), e: {h.isz(n, m) == True{} : Bool}) 1849 -> {Word.and(n, x, m) == Word.zero(n) : Word(n)}: 1850 match n: 1851 case 0n: 1852 match x m: 1853 case WNil{} WNil{}: 1854 {==} 1855 case 1n+p: 1856 match x m: 1857 case WCon{+a, +xt} WCon{True{}, +mt}: 1858 Empty.absurd({Word.and(1n+p, WCon{a, xt}, WCon{True{}, mt}) == Word.zero(1n+p) : Word(1n+p)}, MBool.false_ne_true()(e)) 1859 case WCon{True{}, +xt} WCon{False{}, +mt}: 1860 Equal.cong(Word(p), Word(1n+p), w => WCon{False{}, w}, Word.and(p, xt, mt), Word.zero(p), 1861 h.and_z(p, xt, mt, e)) 1862 case WCon{False{}, +xt} WCon{False{}, +mt}: 1863 Equal.cong(Word(p), Word(1n+p), w => WCon{False{}, w}, Word.and(p, xt, mt), Word.zero(p), 1864 h.and_z(p, xt, mt, e)) 1865 1866 def h.zc(+n: Nat, +x: Word(n), +m: Word(n), +e: {h.isz(n, m) == True{} : Bool}) 1867 -> {Word.cmp(n, Word.and(n, x, m), Word.zero(n)) == EQ{} : Cmp}: 1868 %Equal.sym(Word(n), Word.and(n, x, m), Word.zero(n), h.and_z(n, x, m, e)) : {Word.cmp(n, _, Word.zero(n)) == EQ{} : Cmp} 1869 h.wcmp_refl(n, Word.zero(n)) 1870 1871 def h.zc2(+n: Nat, +x: Word(n), +y: Word(n), +m: Word(n), +e: {h.isz(n, m) == True{} : Bool}) 1872 -> {Word.cmp(n, Word.and(n, x, m), Word.and(n, y, m)) == EQ{} : Cmp}: 1873 %Equal.sym(Word(n), Word.and(n, x, m), Word.zero(n), h.and_z(n, x, m, e)) : {Word.cmp(n, _, Word.and(n, y, m)) == EQ{} : Cmp} 1874 %Equal.sym(Word(n), Word.and(n, y, m), Word.zero(n), h.and_z(n, y, m, e)) : {Word.cmp(n, Word.zero(n), _) == EQ{} : Cmp} 1875 h.wcmp_refl(n, Word.zero(n)) 1876 1877 # A head bit under a set mask bit, with the rest masked to zero, is set when the word is not zero. 1878 def h.hd_true( 1879 a: Bool, +p: Nat, +xt: Word(p), +mt: Word(p), +em: {h.isz(p, mt) == True{} : Bool}, 1880 ex: {Cmp.is_eq(Word.cmp.fin(Bool.and(a, True{}), False{}, Word.cmp(p, Word.and(p, xt, mt), Word.zero(p)))) == False{} : Bool} 1881 ) -> {a == True{} : Bool}: 1882 match a: 1883 case True{}: 1884 {==} 1885 case False{}: 1886 Equal.sym(Bool, True{}, False{}, 1887 rw(Cmp, t => {Cmp.is_eq(Word.cmp.fin(False{}, False{}, t)) == False{} : Bool}, 1888 EQ{}, Word.cmp(p, Word.and(p, xt, mt), Word.zero(p)), 1889 Equal.sym(Cmp, Word.cmp(p, Word.and(p, xt, mt), Word.zero(p)), EQ{}, h.zc(p, xt, mt, em)), ex)) 1890 1891 def h.low(a: Bool, t: Cmp, e: {Cmp.is_eq(Word.cmp.fin(Bool.and(a, False{}), False{}, t)) == False{} : Bool}) 1892 -> {Cmp.is_eq(t) == False{} : Bool}: 1893 match a: 1894 case True{}: 1895 match t: 1896 case LT{}: 1897 e 1898 case EQ{}: 1899 e 1900 case GT{}: 1901 e 1902 case False{}: 1903 match t: 1904 case LT{}: 1905 e 1906 case EQ{}: 1907 e 1908 case GT{}: 1909 e 1910 1911 def h.lift0(t: Cmp, ih: {Cmp.is_eq(t) == True{} : Bool}) 1912 -> {Cmp.is_eq(Word.cmp.fin(False{}, False{}, t)) == True{} : Bool}: 1913 match t: 1914 case LT{}: 1915 ih 1916 case EQ{}: 1917 {==} 1918 case GT{}: 1919 ih 1920 1921 def h.lift(a: Bool, c: Bool, t: Cmp, ih: {Cmp.is_eq(t) == True{} : Bool}) 1922 -> {Cmp.is_eq(Word.cmp.fin(Bool.and(a, False{}), Bool.and(c, False{}), t)) == True{} : Bool}: 1923 match a c: 1924 case True{} True{}: 1925 h.lift0(t, ih) 1926 case True{} False{}: 1927 h.lift0(t, ih) 1928 case False{} True{}: 1929 h.lift0(t, ih) 1930 case False{} False{}: 1931 h.lift0(t, ih) 1932 1933 def h.route_t( 1934 +a: Bool, +c: Bool, +p: Nat, +xt: Word(p), +yt: Word(p), +mt: Word(p), 1935 +em: {h.isz(p, mt) == True{} : Bool}, 1936 ex: {Cmp.is_eq(Word.cmp.fin(Bool.and(a, True{}), False{}, Word.cmp(p, Word.and(p, xt, mt), Word.zero(p)))) == False{} : Bool}, 1937 ey: {Cmp.is_eq(Word.cmp.fin(Bool.and(c, True{}), False{}, Word.cmp(p, Word.and(p, yt, mt), Word.zero(p)))) == False{} : Bool} 1938 ) -> {Cmp.is_eq(Word.cmp.fin(Bool.and(a, True{}), Bool.and(c, True{}), 1939 Word.cmp(p, Word.and(p, xt, mt), Word.and(p, yt, mt)))) == True{} : Bool}: 1940 %Equal.sym(Bool, a, True{}, h.hd_true(a, p, xt, mt, em, ex)) 1941 : {Cmp.is_eq(Word.cmp.fin(Bool.and(_, True{}), Bool.and(c, True{}), Word.cmp(p, Word.and(p, xt, mt), Word.and(p, yt, mt)))) == True{} : Bool} 1942 %Equal.sym(Bool, c, True{}, h.hd_true(c, p, yt, mt, em, ey)) 1943 : {Cmp.is_eq(Word.cmp.fin(True{}, Bool.and(_, True{}), Word.cmp(p, Word.and(p, xt, mt), Word.and(p, yt, mt)))) == True{} : Bool} 1944 %Equal.sym(Cmp, Word.cmp(p, Word.and(p, xt, mt), Word.and(p, yt, mt)), EQ{}, h.zc2(p, xt, yt, mt, em)) 1945 : {Cmp.is_eq(Word.cmp.fin(True{}, True{}, _)) == True{} : Bool} 1946 {==} 1947 1948 def h.route_w( 1949 +n: Nat, x: Word(n), y: Word(n), m: Word(n), 1950 em: {h.at1(n, m) == True{} : Bool}, 1951 ex: {Cmp.is_eq(Word.cmp(n, Word.and(n, x, m), Word.zero(n))) == False{} : Bool}, 1952 ey: {Cmp.is_eq(Word.cmp(n, Word.and(n, y, m), Word.zero(n))) == False{} : Bool} 1953 ) -> {Cmp.is_eq(Word.cmp(n, Word.and(n, x, m), Word.and(n, y, m))) == True{} : Bool}: 1954 match n: 1955 case 0n: 1956 {==} 1957 case 1n+p: 1958 match x y m: 1959 case WCon{+a, +xt} WCon{+c, +yt} WCon{True{}, +mt}: 1960 h.route_t(a, c, p, xt, yt, mt, em, ex, ey) 1961 case WCon{+a, +xt} WCon{+c, +yt} WCon{False{}, +mt}: 1962 h.lift(a, c, Word.cmp(p, Word.and(p, xt, mt), Word.and(p, yt, mt)), 1963 h.route_w(p, xt, yt, mt, em, 1964 h.low(a, Word.cmp(p, Word.and(p, xt, mt), Word.zero(p)), ex), 1965 h.low(c, Word.cmp(p, Word.and(p, yt, mt), Word.zero(p)), ey))) 1966 1967 def h.route( 1968 x: U32, y: U32, m: U32, em: {h.onebit(m) == True{} : Bool}, 1969 ex: {U32.is_eq((x .&. m : U32), 0) == False{} : Bool}, 1970 ey: {U32.is_eq((y .&. m : U32), 0) == False{} : Bool} 1971 ) -> {U32.is_eq((x .&. m : U32), (y .&. m : U32)) == True{} : Bool}: 1972 match x y m: 1973 case U32{xw} U32{yw} U32{+mw}: 1974 h.route_w(32n, xw, yw, mw, em, ex, ey) 1975 1976 def h.isz_put(n: Nat, t: Word(n), e: {h.isz(n, t) == True{} : Bool}) 1977 -> {h.isz(n, Word.shl.put(n, False{}, t)) == True{} : Bool}: 1978 match n: 1979 case 0n: 1980 {==} 1981 case 1n+p: 1982 match t: 1983 case WCon{True{}, t2}: 1984 Empty.absurd({h.isz(1n+p, Word.shl.put(1n+p, False{}, WCon{True{}, t2})) == True{} : Bool}, MBool.false_ne_true()(e)) 1985 case WCon{False{}, t2}: 1986 h.isz_put(p, t2, e) 1987 1988 def h.at1_put.t(q: Nat, b: Bool, t2: Word(q), e: {h.isz(1n+q, WCon{b, t2}) == True{} : Bool}) 1989 -> {h.isz(q, Word.shl.put(q, b, t2)) == True{} : Bool}: 1990 match b: 1991 case True{}: 1992 Empty.absurd({h.isz(q, Word.shl.put(q, True{}, t2)) == True{} : Bool}, MBool.false_ne_true()(e)) 1993 case False{}: 1994 h.isz_put(q, t2, e) 1995 1996 def h.at1_put(p: Nat, t: Word(p), c: Bool, e: {h.at1(1n+p, WCon{c, t}) == True{} : Bool}) 1997 -> {h.at1(p, Word.shl.put(p, c, t)) == True{} : Bool}: 1998 match p: 1999 case 0n: 2000 {==} Lines 1-2000 of 4125. More: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=2001