1 import Base 2 3 # Bend 2.0.32 rewrote Base's Map descents (get, has, put, pop, seek, ins) as 4 # one-level `Map.X.go` functions over the whole node. The lemmas in this 5 # library were written against 2.0.28's shape, where Map.X on a node branched 6 # through a `.bit` helper (`.deep`/`.if` for ins) that recursed with Map.X on 7 # the chosen child. Mutual recursion is no longer allowed, so those helpers 8 # are defined here non-recursively, each calling Base's current Map.X on the 9 # child, and each comes with a bridge law: Map.X on a node equals the helper. 10 # Every bridge holds by unfolding both sides (no induction). 11 12 # ---- the routed key: Map.bit keeps the key (from native_map.bend) ---- 13 14 def routed_key(r: String & Bool) -> String: 15 (key, bit) = r 16 key 17 18 law recursive_bit_key: 19 for c: Char 20 for r: String & Bool 21 {routed_key(Map.bit.go.rec(c, r)) == SCon{c, routed_key(r)} : String} 22 def recursive_bit_key(c, r): 23 match r: 24 case Tuple{key, bit}: 25 {==} 26 27 law bit_go_preserves_key: 28 for key: String 29 for +character: Nat 30 for +offset: Nat 31 {routed_key(Map.bit.go(key, character, offset)) == key : String} 32 def bit_go_preserves_key(key, character, offset): 33 match key character offset: 34 case SNil{} ci off: 35 {==} 36 case SCon{Chr{x}, tail} 0n 0n: 37 {==} 38 case SCon{Chr{x}, tail} 0n 1n+off: 39 {==} 40 case SCon{Chr{x}, +tail} 1n+ci off: 41 +c = {Chr{x} : Char} 42 Equal.trans(String, routed_key(Map.bit.go.rec(c, Map.bit.go(tail, ci, off))), 43 SCon{c, routed_key(Map.bit.go(tail, ci, off))}, SCon{c, tail}, 44 recursive_bit_key(c, Map.bit.go(tail, ci, off)), 45 Equal.cong(String, String, t => SCon{c, t}, routed_key(Map.bit.go(tail, ci, off)), tail, bit_go_preserves_key(tail, ci, off))) 46 47 law bit_at_preserves_key: 48 for key: String 49 for coordinates: Nat & Nat 50 {routed_key(Map.bit.at(key, coordinates)) == key : String} 51 def bit_at_preserves_key(key, coordinates): 52 match coordinates: 53 case Tuple{ci, off}: 54 bit_go_preserves_key(key, ci, off) 55 56 law bit_preserves_key: 57 for key: String 58 for position: Nat 59 {routed_key(Map.bit(key, position)) == key : String} 60 def bit_preserves_key(key, position): 61 bit_at_preserves_key(key, Nat.divmod(position, 33n)) 62 63 # ---- one-step helpers (2.0.28's `.bit` shape over Base's current Map) ---- 64 65 def get_bit(-V: Data, d: V, lo: Map<&2, V>, hi: Map<&2, V>, p2: Nat, kb: String & Bool) -> Map<&2, V> & V: 66 (key2, b) = kb 67 match b: 68 case False{}: 69 Map.lo(&2, V, V, p2, hi, Map.get(V, d, lo, key2)) 70 case True{}: 71 Map.hi(&2, V, V, p2, lo, Map.get(V, d, hi, key2)) 72 73 def has_bit(-a: Quant, -V: Kind(a), lo: Map, hi: Map, p2: Nat, kb: String & Bool) -> Map & Bool: 74 (key2, b) = kb 75 match b: 76 case False{}: 77 Map.lo(a, V, Bool, p2, hi, Map.has(a, V, lo, key2)) 78 case True{}: 79 Map.hi(a, V, Bool, p2, lo, Map.has(a, V, hi, key2)) 80 81 def put_bit(-a: Quant, -V: Kind(a), x: V, p2: Nat, lo: Map, hi: Map, kb: String & Bool) -> Map: 82 (key2, b) = kb 83 match b: 84 case False{}: 85 MNode{p2, Map.put(a, V, lo, key2, x), hi} 86 case True{}: 87 MNode{p2, lo, Map.put(a, V, hi, key2, x)} 88 89 def pop_bit(-a: Quant, -V: Kind(a), lo: Map, hi: Map, p2: Nat, kb: String & Bool) -> Map & Maybe: 90 (key2, b) = kb 91 match b: 92 case False{}: 93 Map.pop.lo(a, V, p2, hi, Map.pop(a, V, lo, key2)) 94 case True{}: 95 Map.pop.hi(a, V, p2, lo, Map.pop(a, V, hi, key2)) 96 97 def seek_bit(-a: Quant, -V: Kind(a), lo: Map, hi: Map, p2: Nat, kb: String & Bool) -> Map & String & Maybe<&2, String>: 98 (key2, b) = kb 99 match b: 100 case False{}: 101 Map.lo(a, V, String & Maybe<&2, String>, p2, hi, Map.seek(a, V, lo, key2)) 102 case True{}: 103 Map.hi(a, V, String & Maybe<&2, String>, p2, lo, Map.seek(a, V, hi, key2)) 104 105 def ins_deep(-a: Quant, -V: Kind(a), x: V, lo: Map, hi: Map, pb: Nat, qb: Nat, kb: String & Bool) -> Map: 106 (key2, b) = kb 107 match b: 108 case False{}: 109 MNode{qb, Map.ins(a, V, lo, key2, x, pb), hi} 110 case True{}: 111 MNode{qb, lo, Map.ins(a, V, hi, key2, x, pb)} 112 113 def ins_if(-a: Quant, -V: Kind(a), key: String, x: V, lo: Map, hi: Map, +p2: Nat, pb: Nat, t: Bool) -> Map: 114 match t: 115 case False{}: 116 Map.ins.splice(a, V, pb, key, x, MNode{p2, lo, hi}) 117 case True{}: 118 ins_deep(a, V, x, lo, hi, pb, p2, Map.bit(key, p2)) 119 120 # ---- bridges: Base Map.X on a node is the one-step helper ---- 121 122 law get_go_bridge: 123 for -V: Data 124 for d: V 125 for +p: Nat 126 for lo: Map<&2, V> 127 for hi: Map<&2, V> 128 for kb: String & Bool 129 {Map.get.go(V, MNode{p, lo, hi}, d, kb) == get_bit(V, d, lo, hi, p, kb) : Map<&2, V> & V} 130 def get_go_bridge(V, d, p, lo, hi, kb): 131 match lo hi kb: 132 case MTip{} _ Tuple{key2, False{}}: 133 {==} 134 case MLeaf{k, v} _ Tuple{key2, False{}}: 135 {==} 136 case MNode{q, c, e} _ Tuple{key2, False{}}: 137 {==} 138 case _ MTip{} Tuple{key2, True{}}: 139 {==} 140 case _ MLeaf{k, v} Tuple{key2, True{}}: 141 {==} 142 case _ MNode{q, c, e} Tuple{key2, True{}}: 143 {==} 144 145 law get_node: 146 for -V: Data 147 for d: V 148 for +p: Nat 149 for lo: Map<&2, V> 150 for hi: Map<&2, V> 151 for key: String 152 {Map.get(V, d, MNode{p, lo, hi}, key) == get_bit(V, d, lo, hi, p, Map.bit(key, p)) : Map<&2, V> & V} 153 def get_node(V, d, p, lo, hi, key): 154 get_go_bridge(V, d, p, lo, hi, Map.bit(key, p)) 155 156 law has_go_bridge: 157 for -a: Quant 158 for -V: Kind(a) 159 for +p: Nat 160 for lo: Map 161 for hi: Map 162 for kb: String & Bool 163 {Map.has.go(a, V, MNode{p, lo, hi}, kb) == has_bit(a, V, lo, hi, p, kb) : Map & Bool} 164 def has_go_bridge(a, V, p, lo, hi, kb): 165 match lo hi kb: 166 case MTip{} _ Tuple{key2, False{}}: 167 {==} 168 case MLeaf{k, v} _ Tuple{key2, False{}}: 169 {==} 170 case MNode{q, c, e} _ Tuple{key2, False{}}: 171 {==} 172 case _ MTip{} Tuple{key2, True{}}: 173 {==} 174 case _ MLeaf{k, v} Tuple{key2, True{}}: 175 {==} 176 case _ MNode{q, c, e} Tuple{key2, True{}}: 177 {==} 178 179 law has_node: 180 for -a: Quant 181 for -V: Kind(a) 182 for +p: Nat 183 for lo: Map 184 for hi: Map 185 for key: String 186 {Map.has(a, V, MNode{p, lo, hi}, key) == has_bit(a, V, lo, hi, p, Map.bit(key, p)) : Map & Bool} 187 def has_node(a, V, p, lo, hi, key): 188 has_go_bridge(a, V, p, lo, hi, Map.bit(key, p)) 189 190 law put_go_bridge: 191 for -a: Quant 192 for -V: Kind(a) 193 for x: V 194 for +p: Nat 195 for lo: Map 196 for hi: Map 197 for kb: String & Bool 198 {Map.put.go(a, V, MNode{p, lo, hi}, x, kb) == put_bit(a, V, x, p, lo, hi, kb) : Map} 199 def put_go_bridge(a, V, x, p, lo, hi, kb): 200 match lo hi kb: 201 case MTip{} _ Tuple{key2, False{}}: 202 {==} 203 case MLeaf{k, v} _ Tuple{key2, False{}}: 204 {==} 205 case MNode{q, c, e} _ Tuple{key2, False{}}: 206 {==} 207 case _ MTip{} Tuple{key2, True{}}: 208 {==} 209 case _ MLeaf{k, v} Tuple{key2, True{}}: 210 {==} 211 case _ MNode{q, c, e} Tuple{key2, True{}}: 212 {==} 213 214 law put_node: 215 for -a: Quant 216 for -V: Kind(a) 217 for x: V 218 for +p: Nat 219 for lo: Map 220 for hi: Map 221 for key: String 222 {Map.put(a, V, MNode{p, lo, hi}, key, x) == put_bit(a, V, x, p, lo, hi, Map.bit(key, p)) : Map} 223 def put_node(a, V, x, p, lo, hi, key): 224 put_go_bridge(a, V, x, p, lo, hi, Map.bit(key, p)) 225 226 law pop_go_bridge: 227 for -a: Quant 228 for -V: Kind(a) 229 for +p: Nat 230 for lo: Map 231 for hi: Map 232 for kb: String & Bool 233 {Map.pop.go(a, V, MNode{p, lo, hi}, kb) == pop_bit(a, V, lo, hi, p, kb) : Map & Maybe} 234 def pop_go_bridge(a, V, p, lo, hi, kb): 235 match lo hi kb: 236 case MTip{} _ Tuple{key2, False{}}: 237 {==} 238 case MLeaf{k, v} _ Tuple{key2, False{}}: 239 {==} 240 case MNode{q, c, e} _ Tuple{key2, False{}}: 241 {==} 242 case _ MTip{} Tuple{key2, True{}}: 243 {==} 244 case _ MLeaf{k, v} Tuple{key2, True{}}: 245 {==} 246 case _ MNode{q, c, e} Tuple{key2, True{}}: 247 {==} 248 249 law pop_node: 250 for -a: Quant 251 for -V: Kind(a) 252 for +p: Nat 253 for lo: Map 254 for hi: Map 255 for key: String 256 {Map.pop(a, V, MNode{p, lo, hi}, key) == pop_bit(a, V, lo, hi, p, Map.bit(key, p)) : Map & Maybe} 257 def pop_node(a, V, p, lo, hi, key): 258 pop_go_bridge(a, V, p, lo, hi, Map.bit(key, p)) 259 260 law seek_go_bridge: 261 for -a: Quant 262 for -V: Kind(a) 263 for +p: Nat 264 for lo: Map 265 for hi: Map 266 for kb: String & Bool 267 {Map.seek.go(a, V, MNode{p, lo, hi}, kb) == seek_bit(a, V, lo, hi, p, kb) : Map & String & Maybe<&2, String>} 268 def seek_go_bridge(a, V, p, lo, hi, kb): 269 match lo hi kb: 270 case MTip{} _ Tuple{key2, False{}}: 271 {==} 272 case MLeaf{k, v} _ Tuple{key2, False{}}: 273 {==} 274 case MNode{q, c, e} _ Tuple{key2, False{}}: 275 {==} 276 case _ MTip{} Tuple{key2, True{}}: 277 {==} 278 case _ MLeaf{k, v} Tuple{key2, True{}}: 279 {==} 280 case _ MNode{q, c, e} Tuple{key2, True{}}: 281 {==} 282 283 law seek_node: 284 for -a: Quant 285 for -V: Kind(a) 286 for +p: Nat 287 for lo: Map 288 for hi: Map 289 for key: String 290 {Map.seek(a, V, MNode{p, lo, hi}, key) == seek_bit(a, V, lo, hi, p, Map.bit(key, p)) : Map & String & Maybe<&2, String>} 291 def seek_node(a, V, p, lo, hi, key): 292 seek_go_bridge(a, V, p, lo, hi, Map.bit(key, p)) 293 294 law ins_splice_bridge: 295 for -a: Quant 296 for -V: Kind(a) 297 for +q: Nat 298 for lo: Map 299 for hi: Map 300 for x: V 301 for +p: Nat 302 for key: String 303 for kb: String & Bool 304 for hk: {routed_key(kb) == key : String} 305 {Map.ins.go(a, V, MNode{q, lo, hi}, x, p, kb, False{}) == Map.ins.splice(a, V, p, key, x, MNode{q, lo, hi}) : Map} 306 def ins_splice_bridge(a, V, q, lo, hi, x, p, key, kb, hk): 307 match lo hi kb: 308 case MTip{} MTip{} Tuple{k2, False{}}: 309 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MTip{}}) : Map} 310 {==} 311 case MTip{} MTip{} Tuple{k2, True{}}: 312 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MTip{}}) : Map} 313 {==} 314 case MTip{} MLeaf{k3, v3} Tuple{k2, False{}}: 315 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MLeaf{k3, v3}}) : Map} 316 {==} 317 case MTip{} MLeaf{k3, v3} Tuple{k2, True{}}: 318 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MLeaf{k3, v3}}) : Map} 319 {==} 320 case MTip{} MNode{r3, c3, e3} Tuple{k2, False{}}: 321 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MNode{r3, c3, e3}}) : Map} 322 {==} 323 case MTip{} MNode{r3, c3, e3} Tuple{k2, True{}}: 324 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MTip{}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MTip{}, MNode{r3, c3, e3}}) : Map} 325 {==} 326 case MLeaf{k1, v1} MTip{} Tuple{k2, False{}}: 327 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MTip{}}) : Map} 328 {==} 329 case MLeaf{k1, v1} MTip{} Tuple{k2, True{}}: 330 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MTip{}}) : Map} 331 {==} 332 case MLeaf{k1, v1} MLeaf{k3, v3} Tuple{k2, False{}}: 333 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MLeaf{k3, v3}}) : Map} 334 {==} 335 case MLeaf{k1, v1} MLeaf{k3, v3} Tuple{k2, True{}}: 336 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MLeaf{k3, v3}}) : Map} 337 {==} 338 case MLeaf{k1, v1} MNode{r3, c3, e3} Tuple{k2, False{}}: 339 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MNode{r3, c3, e3}}) : Map} 340 {==} 341 case MLeaf{k1, v1} MNode{r3, c3, e3} Tuple{k2, True{}}: 342 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MLeaf{k1, v1}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MLeaf{k1, v1}, MNode{r3, c3, e3}}) : Map} 343 {==} 344 case MNode{r1, c1, e1} MTip{} Tuple{k2, False{}}: 345 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MTip{}}) : Map} 346 {==} 347 case MNode{r1, c1, e1} MTip{} Tuple{k2, True{}}: 348 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MTip{}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MTip{}}) : Map} 349 {==} 350 case MNode{r1, c1, e1} MLeaf{k3, v3} Tuple{k2, False{}}: 351 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MLeaf{k3, v3}}) : Map} 352 {==} 353 case MNode{r1, c1, e1} MLeaf{k3, v3} Tuple{k2, True{}}: 354 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MLeaf{k3, v3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MLeaf{k3, v3}}) : Map} 355 {==} 356 case MNode{r1, c1, e1} MNode{r3, c3, e3} Tuple{k2, False{}}: 357 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MNode{r3, c3, e3}}) : Map} 358 {==} 359 case MNode{r1, c1, e1} MNode{r3, c3, e3} Tuple{k2, True{}}: 360 %Equal.sym(String, k2, key, hk) : {Map.ins.splice(a, V, p, _, x, MNode{q, MNode{r1, c1, e1}, MNode{r3, c3, e3}}) == Map.ins.splice(a, V, p, key, x, MNode{q, MNode{r1, c1, e1}, MNode{r3, c3, e3}}) : Map} 361 {==} 362 363 law ins_deep_bridge: 364 for -a: Quant 365 for -V: Kind(a) 366 for +q: Nat 367 for lo: Map 368 for hi: Map 369 for x: V 370 for +p: Nat 371 for kb: String & Bool 372 {Map.ins.go(a, V, MNode{q, lo, hi}, x, p, kb, True{}) == ins_deep(a, V, x, lo, hi, p, q, kb) : Map} 373 def ins_deep_bridge(a, V, q, lo, hi, x, p, kb): 374 match lo hi kb: 375 case MTip{} _ Tuple{key2, False{}}: 376 {==} 377 case MLeaf{k, v} _ Tuple{key2, False{}}: 378 {==} 379 case MNode{r, c, e} _ Tuple{key2, False{}}: 380 {==} 381 case _ MTip{} Tuple{key2, True{}}: 382 {==} 383 case _ MLeaf{k, v} Tuple{key2, True{}}: 384 {==} 385 case _ MNode{r, c, e} Tuple{key2, True{}}: 386 {==} 387 388 law ins_t: 389 for -a: Quant 390 for -V: Kind(a) 391 for +pos: Nat 392 for lo: Map 393 for hi: Map 394 for +key: String 395 for x: V 396 for +p: Nat 397 for t: Bool 398 {Map.ins.go(a, V, MNode{pos, lo, hi}, x, p, Map.bit(key, pos), t) == ins_if(a, V, key, x, lo, hi, pos, p, t) : Map} 399 def ins_t(a, V, pos, lo, hi, key, x, p, t): 400 match t: 401 case False{}: 402 ins_splice_bridge(a, V, pos, lo, hi, x, p, key, Map.bit(key, pos), bit_preserves_key(key, pos)) 403 case True{}: 404 ins_deep_bridge(a, V, pos, lo, hi, x, p, Map.bit(key, pos)) 405 406 law ins_node: 407 for -a: Quant 408 for -V: Kind(a) 409 for +pos: Nat 410 for lo: Map 411 for hi: Map 412 for +key: String 413 for x: V 414 for +p: Nat 415 {Map.ins(a, V, MNode{pos, lo, hi}, key, x, p) == ins_if(a, V, key, x, lo, hi, pos, p, Nat.is_lt(pos, p)) : Map} 416 def ins_node(a, V, pos, lo, hi, key, x, p): 417 ins_t(a, V, pos, lo, hi, key, x, p, Nat.is_lt(pos, p))