[1048] | 1 | (* -------------------------------------------------------------------------- *) |
---|
| 2 | (* Generic associative map data structure, using balanced binary trees, based *) |
---|
| 3 | (* on Data.Map from the Haskell standard library. *) |
---|
| 4 | (* -------------------------------------------------------------------------- *) |
---|
| 5 | |
---|
| 6 | include "arithmetics/nat.ma". |
---|
[1049] | 7 | include "common/Order.ma". |
---|
[1048] | 8 | |
---|
| 9 | (* for eq_rect_Type0_r *) |
---|
| 10 | include "ASM/Util.ma". |
---|
| 11 | |
---|
| 12 | inductive map (key_type: Type[0]) (elt_type: Type[0]): Type[0] ≝ |
---|
| 13 | | map_nil: map key_type elt_type |
---|
| 14 | | map_fork: nat → key_type → elt_type → map key_type elt_type → map key_type elt_type → map key_type elt_type. |
---|
| 15 | |
---|
| 16 | (* -------------------------------------------------------------------------- *) |
---|
| 17 | (* Discrimination functions for structure of map. *) |
---|
| 18 | (* -------------------------------------------------------------------------- *) |
---|
| 19 | |
---|
| 20 | definition map_nil ≝ |
---|
| 21 | λkey_type. |
---|
| 22 | λelt_type. |
---|
| 23 | λthe_map: map key_type elt_type. |
---|
| 24 | match the_map with |
---|
| 25 | [ map_nil ⇒ true |
---|
| 26 | | _ ⇒ false |
---|
| 27 | ]. |
---|
| 28 | |
---|
| 29 | definition map_not_nil ≝ |
---|
| 30 | λkey_type. |
---|
| 31 | λelt_type. |
---|
| 32 | λthe_map: map key_type elt_type. |
---|
| 33 | match the_map with |
---|
| 34 | [ map_nil ⇒ false |
---|
| 35 | | _ ⇒ true |
---|
| 36 | ]. |
---|
| 37 | |
---|
| 38 | definition map_nil_p ≝ |
---|
| 39 | λkey_type. |
---|
| 40 | λelt_type. |
---|
| 41 | λthe_map: map key_type elt_type. |
---|
| 42 | match the_map with |
---|
| 43 | [ map_nil ⇒ True |
---|
| 44 | | _ ⇒ False |
---|
| 45 | ]. |
---|
| 46 | |
---|
| 47 | definition map_not_nil_p ≝ |
---|
| 48 | λkey_type. |
---|
| 49 | λelt_type. |
---|
| 50 | λthe_map: map key_type elt_type. |
---|
| 51 | match the_map with |
---|
| 52 | [ map_nil ⇒ False |
---|
| 53 | | _ ⇒ True |
---|
| 54 | ]. |
---|
| 55 | (* -------------------------------------------------------------------------- *) |
---|
| 56 | (* Size, depth, etc. *) |
---|
| 57 | (* -------------------------------------------------------------------------- *) |
---|
| 58 | definition map_size ≝ |
---|
| 59 | λkey_type. |
---|
| 60 | λelt_type. |
---|
| 61 | λm: map key_type elt_type. |
---|
| 62 | match m with |
---|
| 63 | [ map_nil ⇒ 0 |
---|
| 64 | | map_fork sz key elt l r ⇒ sz |
---|
| 65 | ]. |
---|
| 66 | |
---|
| 67 | (* -------------------------------------------------------------------------- *) |
---|
| 68 | (* Lookup of elements in map. *) |
---|
| 69 | (* -------------------------------------------------------------------------- *) |
---|
| 70 | let rec map_lookup |
---|
| 71 | (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order) |
---|
| 72 | (to_search: key_type) (the_map: map key_type elt_type) on the_map ≝ |
---|
| 73 | match the_map with |
---|
| 74 | [ map_nil ⇒ None ? |
---|
| 75 | | map_fork sz key elt l r ⇒ |
---|
| 76 | match ord to_search key with |
---|
| 77 | [ order_eq ⇒ Some ? elt |
---|
| 78 | | order_lt ⇒ map_lookup key_type elt_type ord to_search l |
---|
| 79 | | order_gt ⇒ map_lookup key_type elt_type ord to_search r |
---|
| 80 | ] |
---|
| 81 | ]. |
---|
| 82 | |
---|
| 83 | definition map_lookup_assoc ≝ |
---|
| 84 | λkey_type. |
---|
| 85 | λelt_type. |
---|
| 86 | λord: key_type → key_type → order. |
---|
| 87 | λto_search: key_type. |
---|
| 88 | λthe_map: map key_type elt_type. |
---|
| 89 | match map_lookup key_type elt_type ord to_search the_map with |
---|
| 90 | [ None ⇒ None ? |
---|
| 91 | | Some found ⇒ Some ? 〈to_search, found〉 |
---|
| 92 | ]. |
---|
| 93 | |
---|
| 94 | definition map_lookup_default ≝ |
---|
| 95 | λkey_type. |
---|
| 96 | λelt_type. |
---|
| 97 | λord: key_type → key_type → order. |
---|
| 98 | λto_search: key_type. |
---|
| 99 | λdef: elt_type. |
---|
| 100 | λthe_map: map key_type elt_type. |
---|
| 101 | match map_lookup key_type elt_type ord to_search the_map with |
---|
| 102 | [ None ⇒ def |
---|
| 103 | | Some found ⇒ found |
---|
| 104 | ]. |
---|
| 105 | |
---|
| 106 | definition map_member ≝ |
---|
| 107 | λkey_type. |
---|
| 108 | λelt_type. |
---|
| 109 | λord: key_type → key_type → order. |
---|
| 110 | λto_search: key_type. |
---|
| 111 | λthe_map: map key_type elt_type. |
---|
| 112 | match map_lookup key_type elt_type ord to_search the_map with |
---|
| 113 | [ None ⇒ false |
---|
| 114 | | Some found ⇒ true |
---|
| 115 | ]. |
---|
| 116 | |
---|
| 117 | definition map_not_member ≝ |
---|
| 118 | λkey_type. |
---|
| 119 | λelt_type. |
---|
| 120 | λord: key_type → key_type → order. |
---|
| 121 | λto_search: key_type. |
---|
| 122 | λthe_map: map key_type elt_type. |
---|
| 123 | match map_lookup key_type elt_type ord to_search the_map with |
---|
| 124 | [ None ⇒ true |
---|
| 125 | | Some found ⇒ false |
---|
| 126 | ]. |
---|
| 127 | |
---|
| 128 | (* -------------------------------------------------------------------------- *) |
---|
| 129 | (* Creation of maps. *) |
---|
| 130 | (* -------------------------------------------------------------------------- *) |
---|
| 131 | definition map_empty ≝ |
---|
| 132 | λkey_type. |
---|
| 133 | λelt_type. |
---|
| 134 | map_nil key_type elt_type. |
---|
| 135 | |
---|
| 136 | definition map_singleton ≝ |
---|
| 137 | λkey_type. |
---|
| 138 | λelt_type. |
---|
| 139 | λkey: key_type. |
---|
| 140 | λelt: elt_type. |
---|
| 141 | map_fork key_type elt_type 1 key elt (map_nil ? ?) (map_nil ? ?). |
---|
| 142 | |
---|
| 143 | (* -------------------------------------------------------------------------- *) |
---|
| 144 | (* Internal, related to balancing and rotating nodes. *) |
---|
| 145 | (* -------------------------------------------------------------------------- *) |
---|
| 146 | definition map_delta ≝ 4. |
---|
| 147 | definition map_ratio ≝ 2. |
---|
| 148 | |
---|
| 149 | definition map_binsert ≝ |
---|
| 150 | λkey_type. |
---|
| 151 | λelt_type. |
---|
| 152 | λkey: key_type. |
---|
| 153 | λelt: elt_type. |
---|
| 154 | λleft: map key_type elt_type. |
---|
| 155 | λright: map key_type elt_type. |
---|
| 156 | map_fork ? ? (1 + map_size ? ? left + map_size ? ? right) key elt left right. |
---|
| 157 | |
---|
| 158 | (* Single rotations, left and right. *) |
---|
| 159 | definition map_single_l ≝ |
---|
| 160 | λkey_type. |
---|
| 161 | λelt_type. |
---|
| 162 | λkey: key_type. |
---|
| 163 | λelt: elt_type. |
---|
| 164 | λleft: map key_type elt_type. |
---|
| 165 | λright: map key_type elt_type. |
---|
| 166 | match right with |
---|
| 167 | [ map_nil ⇒ None ? |
---|
| 168 | | map_fork r_sz r_key r_elt r_l r_r ⇒ |
---|
| 169 | Some ? (map_binsert ? ? r_key r_elt (map_binsert ? ? key elt left r_l) r_r) |
---|
| 170 | ]. |
---|
| 171 | |
---|
[1050] | 172 | definition map_single_l_safe ≝ |
---|
| 173 | λkey_type. |
---|
| 174 | λelt_type. |
---|
| 175 | λkey: key_type. |
---|
| 176 | λelt: elt_type. |
---|
| 177 | λleft: map key_type elt_type. |
---|
| 178 | λright: map key_type elt_type. |
---|
| 179 | λprf: map_not_nil_p key_type elt_type right. |
---|
| 180 | match right return λx. map_not_nil_p key_type elt_type x → map key_type elt_type with |
---|
| 181 | [ map_nil ⇒ λright_nil_absrd. ? |
---|
| 182 | | map_fork r_sz r_key r_elt r_l r_r ⇒ |
---|
| 183 | λright_fork_prf. map_binsert ? ? r_key r_elt (map_binsert ? ? key elt left r_l) r_r |
---|
| 184 | ] prf. |
---|
| 185 | normalize in right_nil_absrd; |
---|
| 186 | cases right_nil_absrd |
---|
| 187 | qed. |
---|
| 188 | |
---|
[1048] | 189 | definition map_single_r ≝ |
---|
| 190 | λkey_type. |
---|
| 191 | λelt_type. |
---|
| 192 | λkey: key_type. |
---|
| 193 | λelt: elt_type. |
---|
| 194 | λleft: map key_type elt_type. |
---|
| 195 | λright: map key_type elt_type. |
---|
| 196 | match left with |
---|
| 197 | [ map_nil ⇒ None ? |
---|
| 198 | | map_fork l_sz l_key l_elt l_l l_r ⇒ |
---|
| 199 | Some ? (map_binsert ? ? l_key l_elt l_l (map_binsert ? ? key elt l_r right)) |
---|
| 200 | ]. |
---|
| 201 | |
---|
[1050] | 202 | definition map_single_r_safe ≝ |
---|
| 203 | λkey_type. |
---|
| 204 | λelt_type. |
---|
| 205 | λkey: key_type. |
---|
| 206 | λelt: elt_type. |
---|
| 207 | λleft: map key_type elt_type. |
---|
| 208 | λright: map key_type elt_type. |
---|
| 209 | λprf: map_not_nil_p key_type elt_type left. |
---|
| 210 | match left return λx. map_not_nil_p key_type elt_type x → map key_type elt_type with |
---|
| 211 | [ map_nil ⇒ λleft_nil_absrd. ? |
---|
| 212 | | map_fork l_sz l_key l_elt l_l l_r ⇒ |
---|
| 213 | λleft_fork_prf. map_binsert ? ? l_key l_elt l_l (map_binsert ? ? key elt l_r right) |
---|
| 214 | ] prf. |
---|
| 215 | normalize in left_nil_absrd; |
---|
| 216 | cases left_nil_absrd |
---|
| 217 | qed. |
---|
| 218 | |
---|
| 219 | definition map_double_r_property_p ≝ |
---|
| 220 | λkey_type. |
---|
| 221 | λelt_type. |
---|
| 222 | λleft: map key_type elt_type. |
---|
| 223 | match left with |
---|
| 224 | [ map_nil ⇒ False |
---|
| 225 | | map_fork l_sz l_key l_elt l_l l_r ⇒ |
---|
| 226 | match l_r with |
---|
| 227 | [ map_nil ⇒ False |
---|
| 228 | | _ ⇒ True |
---|
| 229 | ] |
---|
| 230 | ]. |
---|
| 231 | |
---|
[1052] | 232 | lemma map_double_r_property_p_exists: |
---|
| 233 | ∀key_type. |
---|
| 234 | ∀elt_type. |
---|
| 235 | ∀left: map key_type elt_type. |
---|
| 236 | map_double_r_property_p key_type elt_type left → |
---|
| 237 | ∃l_sz, l_key, l_elt, l_l, l_r. |
---|
| 238 | left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r. |
---|
| 239 | #KEY_TYPE #ELT_TYPE #LEFT |
---|
| 240 | cases LEFT |
---|
| 241 | [ normalize #HYP cases HYP |
---|
| 242 | | #L_SZ #L_KEY #L_ELT #L_LEFT #L_RIGHT |
---|
| 243 | #HYP |
---|
| 244 | @ex_intro |
---|
| 245 | [1: @L_SZ |
---|
| 246 | |2: @ex_intro |
---|
| 247 | [1: @L_KEY |
---|
| 248 | |2: @ex_intro |
---|
| 249 | [1: @L_ELT |
---|
| 250 | |2: @ex_intro |
---|
| 251 | [1: @L_LEFT |
---|
| 252 | |2: @ex_intro |
---|
| 253 | [1: @L_RIGHT |
---|
| 254 | |2: % |
---|
| 255 | ] |
---|
| 256 | ] |
---|
| 257 | ] |
---|
| 258 | ] |
---|
| 259 | ] |
---|
| 260 | ] |
---|
| 261 | qed. |
---|
| 262 | |
---|
| 263 | lemma map_double_r_property_p_exists_l_r_not_nil_p: |
---|
| 264 | ∀key_type. |
---|
| 265 | ∀elt_type. |
---|
| 266 | ∀left: map key_type elt_type. |
---|
| 267 | map_double_r_property_p key_type elt_type left → |
---|
| 268 | ∃l_sz, l_key, l_elt, l_l, l_r. |
---|
| 269 | (left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r) ∧ |
---|
| 270 | map_not_nil_p key_type elt_type l_r. |
---|
| 271 | #KEY_TYPE #ELT_TYPE #LEFT |
---|
| 272 | cases LEFT |
---|
| 273 | [ normalize #HYP cases HYP |
---|
| 274 | | #L_SZ #L_KEY #L_ELT #L_LEFT #L_RIGHT |
---|
| 275 | #HYP |
---|
| 276 | @ex_intro |
---|
| 277 | [1: @L_SZ |
---|
| 278 | |2: @ex_intro |
---|
| 279 | [1: @L_KEY |
---|
| 280 | |2: @ex_intro |
---|
| 281 | [1: @L_ELT |
---|
| 282 | |2: @ex_intro |
---|
| 283 | [1: @L_LEFT |
---|
| 284 | |2: @ex_intro |
---|
| 285 | [1: @L_RIGHT |
---|
| 286 | |2: @conj |
---|
| 287 | [1: % |
---|
| 288 | |2: generalize in match HYP |
---|
| 289 | cases L_RIGHT |
---|
| 290 | [1: normalize // |
---|
| 291 | |2: #NEW_SZ #NEW_KEY #NEW_ELT #NEW_L #NEW_R |
---|
| 292 | normalize // |
---|
| 293 | ] |
---|
| 294 | ] |
---|
| 295 | ] |
---|
| 296 | ] |
---|
| 297 | ] |
---|
| 298 | ] |
---|
| 299 | ] |
---|
| 300 | ] |
---|
| 301 | qed. |
---|
| 302 | |
---|
[1048] | 303 | definition map_double_r ≝ |
---|
| 304 | λkey_type. |
---|
| 305 | λelt_type. |
---|
| 306 | λkey: key_type. |
---|
| 307 | λelt: elt_type. |
---|
| 308 | λleft: map key_type elt_type. |
---|
| 309 | λright: map key_type elt_type. |
---|
| 310 | match left with |
---|
| 311 | [ map_nil ⇒ None ? |
---|
| 312 | | map_fork l_sz l_key l_elt l_l l_r ⇒ |
---|
| 313 | match l_r with |
---|
| 314 | [ map_nil ⇒ None ? |
---|
| 315 | | map_fork lr_sz lr_key lr_elt lr_l lr_r ⇒ |
---|
| 316 | Some ? (map_binsert … lr_key lr_elt (map_binsert … l_key l_elt l_l lr_l) (map_binsert … key elt lr_r right)) |
---|
| 317 | ] |
---|
| 318 | ]. |
---|
| 319 | |
---|
| 320 | definition map_double_l ≝ |
---|
| 321 | λkey_type. |
---|
| 322 | λelt_type. |
---|
| 323 | λkey: key_type. |
---|
| 324 | λelt: elt_type. |
---|
| 325 | λleft: map key_type elt_type. |
---|
| 326 | λright: map key_type elt_type. |
---|
| 327 | match right with |
---|
| 328 | [ map_nil ⇒ None … |
---|
| 329 | | map_fork r_sz r_key r_elt r_l r_r ⇒ |
---|
| 330 | match r_l with |
---|
| 331 | [ map_nil ⇒ None … |
---|
| 332 | | map_fork rl_sz rl_key rl_elt rl_l rl_r ⇒ |
---|
| 333 | Some ? (map_binsert … rl_key rl_elt (map_binsert … key elt left rl_l) (map_binsert … r_key r_elt rl_r r_r)) |
---|
| 334 | ] |
---|
| 335 | ]. |
---|
| 336 | |
---|
| 337 | definition map_rotate_r ≝ |
---|
| 338 | λkey_type. |
---|
| 339 | λelt_type. |
---|
| 340 | λkey: key_type. |
---|
| 341 | λelt: elt_type. |
---|
| 342 | λleft: map key_type elt_type. |
---|
| 343 | λright: map key_type elt_type. |
---|
| 344 | match left with |
---|
| 345 | [ map_nil ⇒ None ? |
---|
| 346 | | map_fork l_sz l_key l_elt l_l l_r ⇒ |
---|
| 347 | if ltb (map_size ? ? l_r) (map_ratio * map_size ? ? l_l) then |
---|
| 348 | map_single_r ? ? key elt left right |
---|
| 349 | else |
---|
| 350 | map_double_r ? ? key elt left right |
---|
| 351 | ]. |
---|
| 352 | |
---|
| 353 | (* fails only when right = nil *) |
---|
| 354 | definition map_rotate_l ≝ |
---|
| 355 | λkey_type. |
---|
| 356 | λelt_type. |
---|
| 357 | λkey: key_type. |
---|
| 358 | λelt: elt_type. |
---|
| 359 | λleft: map key_type elt_type. |
---|
| 360 | λright: map key_type elt_type. |
---|
| 361 | match right with |
---|
| 362 | [ map_nil ⇒ None ? |
---|
| 363 | | map_fork r_sz r_key r_elt r_l r_r ⇒ |
---|
| 364 | if ltb (map_size ? ? r_l) (map_ratio * map_size ? ? r_r) then |
---|
| 365 | map_single_l ? ? key elt left right |
---|
| 366 | else |
---|
| 367 | map_double_l ? ? key elt left right |
---|
| 368 | ]. |
---|
| 369 | |
---|
| 370 | definition map_balance ≝ |
---|
| 371 | λkey_type. |
---|
| 372 | λelt_type. |
---|
| 373 | λkey: key_type. |
---|
| 374 | λelt: elt_type. |
---|
| 375 | λleft: map key_type elt_type. |
---|
| 376 | λright: map key_type elt_type. |
---|
| 377 | let size_l ≝ map_size ? ? left in |
---|
| 378 | let size_r ≝ map_size ? ? right in |
---|
| 379 | let size_x ≝ 1 + size_l + size_r in |
---|
| 380 | if leb (size_l + size_r) 1 then |
---|
| 381 | Some ? (map_fork ? ? size_x key elt left right) |
---|
| 382 | else if geb size_r (map_delta * size_l) then |
---|
| 383 | map_rotate_l ? ? key elt left right |
---|
| 384 | else if geb size_l (map_delta * size_r) then |
---|
| 385 | map_rotate_r ? ? key elt left right |
---|
| 386 | else |
---|
| 387 | Some ? (map_fork ? ? size_x key elt left right). |
---|
| 388 | |
---|
| 389 | let rec map_delete_find_min |
---|
| 390 | (key_type: Type[0]) (elt_type: Type[0]) (the_map: map key_type elt_type) on the_map ≝ |
---|
| 391 | match the_map with |
---|
| 392 | [ map_nil ⇒ None ? |
---|
| 393 | | map_fork sz key elt l r ⇒ |
---|
| 394 | match l with |
---|
| 395 | [ map_nil ⇒ Some ? 〈〈key, elt〉, r〉 |
---|
| 396 | | _ ⇒ |
---|
| 397 | match map_delete_find_min key_type elt_type l with |
---|
| 398 | [ None ⇒ None ? |
---|
| 399 | | Some kmn ⇒ |
---|
| 400 | let 〈km, new〉 ≝ kmn in |
---|
| 401 | match map_balance key_type elt_type key elt new r with |
---|
| 402 | [ None ⇒ None ? |
---|
| 403 | | Some balanced ⇒ Some ? 〈km, balanced〉 |
---|
| 404 | ] |
---|
| 405 | ] |
---|
| 406 | ] |
---|
| 407 | ]. |
---|
| 408 | |
---|
| 409 | let rec map_delete_find_max |
---|
| 410 | (key_type: Type[0]) (elt_type: Type[0]) (the_map: map key_type elt_type) on the_map ≝ |
---|
| 411 | match the_map with |
---|
| 412 | [ map_nil ⇒ None ? |
---|
| 413 | | map_fork sz key elt l r ⇒ |
---|
| 414 | match r with |
---|
| 415 | [ map_nil ⇒ Some ? 〈〈key, elt〉, l〉 |
---|
| 416 | | _ ⇒ |
---|
| 417 | match map_delete_find_max key_type elt_type r with |
---|
| 418 | [ None ⇒ None ? |
---|
| 419 | | Some kmn ⇒ |
---|
| 420 | let 〈km, new〉 ≝ kmn in |
---|
| 421 | match map_balance key_type elt_type key elt l new with |
---|
| 422 | [ None ⇒ None ? |
---|
| 423 | | Some balanced ⇒ Some ? 〈km, balanced〉 |
---|
| 424 | ] |
---|
| 425 | ] |
---|
| 426 | ] |
---|
| 427 | ]. |
---|
| 428 | |
---|
| 429 | definition map_glue ≝ |
---|
| 430 | λkey_type. |
---|
| 431 | λelt_type. |
---|
| 432 | λleft: map key_type elt_type. |
---|
| 433 | λright: map key_type elt_type. |
---|
| 434 | match left with |
---|
| 435 | [ map_nil ⇒ Some ? right |
---|
| 436 | | map_fork l_sz l_key l_elt l_l l_r ⇒ |
---|
| 437 | match right with |
---|
| 438 | [ map_nil ⇒ Some ? left |
---|
| 439 | | map_fork r_sz r_key r_elt r_l r_r ⇒ |
---|
| 440 | if gtb l_sz r_sz then |
---|
| 441 | match map_delete_find_max key_type elt_type left with |
---|
| 442 | [ None ⇒ None ? |
---|
| 443 | | Some kmml' ⇒ |
---|
| 444 | let 〈kmm, l'〉 ≝ kmml' in |
---|
| 445 | let 〈km, m〉 ≝ kmm in |
---|
| 446 | map_balance key_type elt_type km m l' right |
---|
| 447 | ] |
---|
| 448 | else |
---|
| 449 | match map_delete_find_min key_type elt_type right with |
---|
| 450 | [ None ⇒ None ? |
---|
| 451 | | Some kmmr' ⇒ |
---|
| 452 | let 〈kmm, r'〉 ≝ kmmr' in |
---|
| 453 | let 〈km, m〉 ≝ kmm in |
---|
| 454 | map_balance key_type elt_type km m left r' |
---|
| 455 | ] |
---|
| 456 | ] |
---|
| 457 | ]. |
---|
| 458 | |
---|
| 459 | (* -------------------------------------------------------------------------- *) |
---|
| 460 | (* Inserting elements. *) |
---|
| 461 | (* -------------------------------------------------------------------------- *) |
---|
| 462 | |
---|
| 463 | let rec map_insert |
---|
| 464 | (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order) |
---|
| 465 | (key: key_type) (elt: elt_type) (the_map: map key_type elt_type) on the_map: option (map key_type elt_type) ≝ |
---|
| 466 | match the_map with |
---|
| 467 | [ map_nil ⇒ Some ? (map_singleton … key elt) |
---|
| 468 | | map_fork m_sz m_key m_elt m_l m_r ⇒ |
---|
| 469 | match ord m_key key with |
---|
| 470 | [ order_lt ⇒ |
---|
| 471 | match map_insert … ord key elt m_l with |
---|
| 472 | [ None ⇒ None ? |
---|
| 473 | | Some new_l ⇒ map_balance … m_key m_elt new_l m_r |
---|
| 474 | ] |
---|
| 475 | | order_eq ⇒ Some ? (map_fork key_type elt_type m_sz key elt m_l m_r) |
---|
| 476 | | order_gt ⇒ |
---|
| 477 | match map_insert key_type elt_type ord key elt m_r with |
---|
| 478 | [ None ⇒ None ? |
---|
| 479 | | Some new_r ⇒ map_balance key_type elt_type m_key m_elt m_l new_r |
---|
| 480 | ] |
---|
| 481 | ] |
---|
| 482 | ]. |
---|
| 483 | |
---|
| 484 | (* -------------------------------------------------------------------------- *) |
---|
| 485 | (* Deleting elements. *) |
---|
| 486 | (* -------------------------------------------------------------------------- *) |
---|
| 487 | |
---|
| 488 | let rec map_delete |
---|
| 489 | (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order) |
---|
| 490 | (the_key: key_type) (the_map: map key_type elt_type) on the_map ≝ |
---|
| 491 | match the_map with |
---|
| 492 | [ map_nil ⇒ Some ? (map_nil key_type elt_type) |
---|
| 493 | | map_fork sz key elt l r ⇒ |
---|
| 494 | match ord the_key key with |
---|
| 495 | [ order_lt ⇒ |
---|
| 496 | match map_delete key_type elt_type ord the_key l with |
---|
| 497 | [ None ⇒ None ? |
---|
| 498 | | Some new_l ⇒ map_balance key_type elt_type key elt new_l r |
---|
| 499 | ] |
---|
| 500 | | order_eq ⇒ map_glue key_type elt_type l r |
---|
| 501 | | order_gt ⇒ |
---|
| 502 | match map_delete key_type elt_type ord the_key r with |
---|
| 503 | [ None ⇒ None ? |
---|
| 504 | | Some new_r ⇒ map_balance key_type elt_type key elt l new_r |
---|
| 505 | ] |
---|
| 506 | ] |
---|
| 507 | ]. |
---|
| 508 | |
---|
| 509 | (* -------------------------------------------------------------------------- *) |
---|
| 510 | (* Folds. *) |
---|
| 511 | (* -------------------------------------------------------------------------- *) |
---|
| 512 | |
---|
| 513 | let rec map_foldr_with_key |
---|
| 514 | (key_type: Type[0]) (dom_type: Type[0]) (rng_type: Type[0]) |
---|
| 515 | (f: key_type → dom_type → rng_type → rng_type) (e: rng_type) |
---|
| 516 | (the_map: map key_type dom_type) on the_map ≝ |
---|
| 517 | match the_map with |
---|
| 518 | [ map_nil ⇒ e |
---|
| 519 | | map_fork m_sz m_key m_elt m_l m_r ⇒ |
---|
| 520 | map_foldr_with_key key_type dom_type rng_type f (map_foldr_with_key key_type dom_type rng_type f e m_r) m_l |
---|
| 521 | ]. |
---|
| 522 | |
---|
| 523 | let rec map_foldl_with_key |
---|
| 524 | (key_type: Type[0]) (dom_type: Type[0]) (rng_type: Type[0]) |
---|
| 525 | (f: rng_type → key_type → dom_type → rng_type) (e: rng_type) |
---|
| 526 | (the_map: map key_type dom_type) on the_map ≝ |
---|
| 527 | match the_map with |
---|
| 528 | [ map_nil ⇒ e |
---|
| 529 | | map_fork m_sz m_key m_elt m_l m_r ⇒ |
---|
| 530 | map_foldl_with_key key_type dom_type rng_type f (f (map_foldl_with_key key_type dom_type rng_type f e m_l) m_key m_elt) m_r |
---|
| 531 | ]. |
---|
| 532 | |
---|
| 533 | definition map_fold ≝ |
---|
| 534 | λkey_type. |
---|
| 535 | λdom_type. |
---|
| 536 | λrng_type. |
---|
| 537 | λf: dom_type → rng_type → rng_type. |
---|
| 538 | map_foldr_with_key key_type dom_type rng_type (λi. λx'. λz'. f x' z'). |
---|
| 539 | |
---|
| 540 | (* -------------------------------------------------------------------------- *) |
---|
| 541 | (* Maps. *) |
---|
| 542 | (* -------------------------------------------------------------------------- *) |
---|
| 543 | |
---|
| 544 | let rec map_map_with_key |
---|
| 545 | (key_type: Type[0]) (dom_type: Type[0]) (rng_type: Type[0]) |
---|
| 546 | (f: key_type → dom_type → rng_type) (the_map: map key_type dom_type) on the_map ≝ |
---|
| 547 | match the_map with |
---|
| 548 | [ map_nil ⇒ map_nil key_type rng_type |
---|
| 549 | | map_fork m_sz m_key m_elt m_l m_r ⇒ |
---|
| 550 | map_fork key_type rng_type m_sz m_key (f m_key m_elt) |
---|
| 551 | (map_map_with_key key_type dom_type rng_type f m_l) |
---|
| 552 | (map_map_with_key key_type dom_type rng_type f m_r) |
---|
| 553 | ]. |
---|
| 554 | |
---|
| 555 | definition map_map ≝ |
---|
| 556 | λkey_type. |
---|
| 557 | λdom_type. |
---|
| 558 | λrng_type. |
---|
| 559 | λf: dom_type → rng_type. |
---|
| 560 | λthe_map: map key_type dom_type. |
---|
| 561 | map_map_with_key key_type dom_type rng_type (λk. f) the_map. |
---|
| 562 | |
---|
| 563 | (* -------------------------------------------------------------------------- *) |
---|
| 564 | (* Unions. *) |
---|
| 565 | (* -------------------------------------------------------------------------- *) |
---|
| 566 | |
---|
| 567 | let rec map_insert_max |
---|
| 568 | (key_type: Type[0]) (elt_type: Type[0]) (key: key_type) (elt: elt_type) |
---|
| 569 | (the_map: map key_type elt_type) on the_map ≝ |
---|
| 570 | match the_map with |
---|
| 571 | [ map_nil ⇒ Some ? (map_singleton key_type elt_type key elt) |
---|
| 572 | | map_fork m_sz m_key m_elt m_l m_r ⇒ |
---|
| 573 | match map_insert_max key_type elt_type key elt m_r with |
---|
| 574 | [ None ⇒ None ? |
---|
| 575 | | Some new_r ⇒ map_balance key_type elt_type m_key m_elt m_l new_r |
---|
| 576 | ] |
---|
| 577 | ]. |
---|
| 578 | |
---|
| 579 | let rec map_insert_min |
---|
| 580 | (key_type: Type[0]) (elt_type: Type[0]) (key: key_type) (elt: elt_type) |
---|
| 581 | (the_map: map key_type elt_type) on the_map ≝ |
---|
| 582 | match the_map with |
---|
| 583 | [ map_nil ⇒ Some ? (map_singleton key_type elt_type key elt) |
---|
| 584 | | map_fork m_sz m_key m_elt m_l m_r ⇒ |
---|
| 585 | match map_insert_min key_type elt_type key elt m_l with |
---|
| 586 | [ None ⇒ None ? |
---|
| 587 | | Some new_l ⇒ map_balance key_type elt_type m_key m_elt new_l m_r |
---|
| 588 | ] |
---|
| 589 | ]. |
---|
| 590 | |
---|
| 591 | definition map_join_prf' ≝ |
---|
| 592 | λkey_type. |
---|
| 593 | λelt_type. |
---|
| 594 | λmeasure: nat × nat. |
---|
| 595 | λleft: map key_type elt_type. |
---|
| 596 | λright: map key_type elt_type. |
---|
| 597 | \fst measure = O → left = map_nil key_type elt_type → |
---|
| 598 | \snd measure = O → left = map_nil key_type elt_type → |
---|
| 599 | ∀n. ∀l_sz. ∀l_key. ∀l_elt. ∀l_l. ∀l_r. |
---|
| 600 | \fst measure = S n → left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r → |
---|
| 601 | ∀n. ∀r_sz. ∀r_key. ∀r_elt. ∀r_l. ∀r_r. |
---|
| 602 | \snd measure = S n → left = map_fork key_type elt_type r_sz r_key r_elt r_l r_r. |
---|
| 603 | |
---|
| 604 | axiom map_join': |
---|
| 605 | ∀key_type. |
---|
| 606 | ∀elt_type. |
---|
| 607 | ∀key: key_type. |
---|
| 608 | ∀elt: elt_type. |
---|
| 609 | ∀left: map key_type elt_type. |
---|
| 610 | ∀right: map key_type elt_type. |
---|
| 611 | ∀measure: nat × nat. |
---|
| 612 | ∀prf: map_join_prf' key_type elt_type measure left right. |
---|
| 613 | option (map key_type elt_type). |
---|
| 614 | |
---|
| 615 | (* |
---|
| 616 | let rec map_join' |
---|
| 617 | (key_type: Type[0]) (elt_type: Type[0]) (key: key_type) (elt: elt_type) |
---|
| 618 | (left: map key_type elt_type) (right: map key_type elt_type) |
---|
| 619 | (measure: nat × nat) |
---|
| 620 | (prf: map_join_prf' key_type elt_type measure left right) |
---|
| 621 | on measure: option (map key_type elt_type) ≝ |
---|
| 622 | let size_l ≝ \fst measure in |
---|
| 623 | let size_r ≝ \snd measure in |
---|
| 624 | match size_l return λx. map_join_prf' key_type elt_type 〈x, size_r〉 left right → option (map key_type elt_type) with |
---|
| 625 | [ O ⇒ |
---|
| 626 | λprf_left_nil: map_join_prf' key_type elt_type 〈0, size_r〉 left right. |
---|
| 627 | map_insert_min key_type elt_type key elt right |
---|
| 628 | | S size_l' ⇒ |
---|
| 629 | match left with |
---|
| 630 | [ map_nil ⇒ |
---|
| 631 | λprf_left_nil_abs: map_join_prf' key_type elt_type 〈S size_l', size_r〉 left right. ? |
---|
| 632 | | map_fork l_sz l_key l_elt l_l l_r ⇒ |
---|
| 633 | λprf_left_fork: map_join_prf' key_type elt_type 〈size_l', size_r〉 l_l l_r. |
---|
| 634 | match size_r return λy. map_join_prf' key_type elt_type 〈size_l', y〉 left right → option (map key_type elt_type) with |
---|
| 635 | [ O ⇒ |
---|
| 636 | λprf_right_nil: map_join_prf' key_type elt_type 〈size_l', 0〉 left right. |
---|
| 637 | map_insert_max key_type elt_type key elt left |
---|
| 638 | | S size_r' ⇒ |
---|
| 639 | match right with |
---|
| 640 | [ map_nil ⇒ |
---|
| 641 | λprf_right_nil_abs: map_join_prf' key_type elt_type 〈S size_l', S size_r'〉 left right. ? |
---|
| 642 | | map_fork r_sz r_key r_elt r_l r_r ⇒ |
---|
| 643 | λprf_right_fork: map_join_prf' key_type elt_type 〈size_l', size_r'〉 r_l r_r. |
---|
| 644 | if ltb (map_delta * l_sz) r_sz then |
---|
| 645 | match map_join' key_type elt_type key elt left r_l 〈S size_l', S size_r'〉 ? with |
---|
| 646 | [ None ⇒ None ? |
---|
| 647 | | Some joined ⇒ |
---|
| 648 | map_balance key_type elt_type r_key r_elt joined r_r |
---|
| 649 | ] |
---|
| 650 | else if ltb (map_delta * r_sz) l_sz then |
---|
| 651 | match map_join' key_type elt_type key elt l_r right 〈S size_l', S size_r'〉 ? with |
---|
| 652 | [ None ⇒ None ? |
---|
| 653 | | Some joined ⇒ |
---|
| 654 | map_balance key_type elt_type l_key l_elt l_l joined |
---|
| 655 | ] |
---|
| 656 | else |
---|
| 657 | Some ? (map_binsert key_type elt_type key elt left right) |
---|
| 658 | ] |
---|
| 659 | ] ? |
---|
| 660 | ] |
---|
| 661 | ] ?. |
---|
| 662 | [ 3: @prf_right_fork |
---|
| 663 | | 4: @prf_left_fork |
---|
| 664 | *) |
---|
| 665 | |
---|
| 666 | (* requires some crazy trick to convince termination checker *) |
---|
| 667 | axiom map_join: |
---|
| 668 | ∀key_type. |
---|
| 669 | ∀elt_type. |
---|
| 670 | ∀key: key_type. |
---|
| 671 | ∀elt: elt_type. |
---|
| 672 | ∀left: map key_type elt_type. |
---|
| 673 | ∀right: map key_type elt_type. |
---|
| 674 | option (map key_type elt_type). |
---|
| 675 | |
---|
| 676 | let rec map_filter_gt |
---|
| 677 | (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → order) |
---|
| 678 | (the_map: map key_type elt_type) on the_map ≝ |
---|
| 679 | match the_map with |
---|
| 680 | [ map_nil ⇒ Some ? (map_nil key_type elt_type) |
---|
| 681 | | map_fork m_sz m_key m_elt m_l m_r ⇒ |
---|
| 682 | match ord m_key with |
---|
| 683 | [ order_eq ⇒ Some ? m_r |
---|
| 684 | | order_lt ⇒ |
---|
| 685 | match map_filter_gt key_type elt_type ord m_l with |
---|
| 686 | [ None ⇒ None ? |
---|
| 687 | | Some filtered ⇒ |
---|
| 688 | map_join key_type elt_type m_key m_elt filtered m_r |
---|
| 689 | ] |
---|
| 690 | | order_gt ⇒ map_filter_gt key_type elt_type ord m_r |
---|
| 691 | ] |
---|
| 692 | ]. |
---|
| 693 | |
---|
| 694 | let rec map_filter_lt |
---|
| 695 | (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → order) |
---|
| 696 | (the_map: map key_type elt_type) on the_map ≝ |
---|
| 697 | match the_map with |
---|
| 698 | [ map_nil ⇒ Some ? (map_nil key_type elt_type) |
---|
| 699 | | map_fork m_sz m_key m_elt m_l m_r ⇒ |
---|
| 700 | match ord m_key with |
---|
| 701 | [ order_eq ⇒ Some ? m_l |
---|
| 702 | | order_lt ⇒ map_filter_lt key_type elt_type ord m_l |
---|
| 703 | | order_gt ⇒ |
---|
| 704 | match map_filter_lt key_type elt_type ord m_r with |
---|
| 705 | [ None ⇒ None ? |
---|
| 706 | | Some filtered ⇒ map_join key_type elt_type m_key m_elt m_l filtered |
---|
| 707 | ] |
---|
| 708 | ] |
---|
| 709 | ]. |
---|
| 710 | |
---|
| 711 | let rec map_trim |
---|
| 712 | (key_type: Type[0]) (elt_type: Type[0]) (lord: key_type → order) |
---|
| 713 | (hord: key_type → order) (the_map: map key_type elt_type) on the_map ≝ |
---|
| 714 | match the_map with |
---|
| 715 | [ map_nil ⇒ map_nil key_type elt_type |
---|
| 716 | | map_fork m_sz m_key m_elt m_l m_r ⇒ |
---|
| 717 | match lord m_key with |
---|
| 718 | [ order_lt ⇒ |
---|
| 719 | match hord m_key with |
---|
| 720 | [ order_gt ⇒ the_map |
---|
| 721 | | _ ⇒ map_trim key_type elt_type lord hord m_l |
---|
| 722 | ] |
---|
| 723 | | _ ⇒ map_trim key_type elt_type lord hord m_r |
---|
| 724 | ] |
---|
| 725 | ]. |
---|
| 726 | |
---|
| 727 | axiom map_hedge_union: |
---|
| 728 | ∀key_type: Type[0]. |
---|
| 729 | ∀elt_type: Type[0]. |
---|
| 730 | ∀ord: key_type → key_type → order. |
---|
| 731 | ∀lord: key_type → order. |
---|
| 732 | ∀hord: key_type → order. |
---|
| 733 | ∀left: map key_type elt_type. |
---|
| 734 | ∀right: map key_type elt_type. |
---|
| 735 | option (map key_type elt_type). |
---|
| 736 | |
---|
| 737 | (* |
---|
| 738 | (* left biased hedge union *) |
---|
| 739 | let rec map_hedge_union |
---|
| 740 | (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order) |
---|
| 741 | (lord: key_type → order) (hord: key_type → order) |
---|
| 742 | (* (prod: (map key_type elt_type) × (map key_type elt_type)) on prod ≝ *) |
---|
| 743 | (left: map key_type elt_type) (right: map key_type elt_type) on right ≝ |
---|
| 744 | let 〈left, right〉 ≝ prod in |
---|
| 745 | match right with |
---|
| 746 | [ map_nil ⇒ Some ? left |
---|
| 747 | | map_fork r_sz r_key r_elt r_l r_r ⇒ |
---|
| 748 | match left with |
---|
| 749 | [ map_nil ⇒ |
---|
| 750 | match map_filter_gt key_type elt_type lord r_l with |
---|
| 751 | [ None ⇒ None ? |
---|
| 752 | | Some filtered_gt ⇒ |
---|
| 753 | match map_filter_lt key_type elt_type hord r_r with |
---|
| 754 | [ None ⇒ None ? |
---|
| 755 | | Some filtered_lt ⇒ map_join key_type elt_type r_key r_elt filtered_gt filtered_lt |
---|
| 756 | ] |
---|
| 757 | ] |
---|
| 758 | | map_fork l_sz l_key l_elt l_l l_r ⇒ |
---|
| 759 | let xord ≝ λk: key_type. ord l_key k in |
---|
| 760 | let trimmed_l ≝ map_trim key_type elt_type lord xord right in |
---|
| 761 | let trimmed_r ≝ map_trim key_type elt_type xord hord right in |
---|
| 762 | match map_hedge_union key_type elt_type ord lord xord 〈l_l, trimmed_l〉 with |
---|
| 763 | [ None ⇒ None ? |
---|
| 764 | | Some hedged_l ⇒ |
---|
| 765 | match map_hedge_union key_type elt_type ord xord hord 〈l_r, trimmed_r〉 with |
---|
| 766 | [ None ⇒ None ? |
---|
| 767 | | Some hedged_r ⇒ map_join key_type elt_type l_key l_elt hedged_l hedged_r |
---|
| 768 | ] |
---|
| 769 | ] |
---|
| 770 | ] |
---|
| 771 | ]. |
---|
| 772 | *) |
---|
| 773 | |
---|
| 774 | definition map_union ≝ |
---|
| 775 | λkey_type. |
---|
| 776 | λelt_type. |
---|
| 777 | λord: key_type → key_type → order. |
---|
| 778 | λleft: map key_type elt_type. |
---|
| 779 | λright: map key_type elt_type. |
---|
| 780 | match left with |
---|
| 781 | [ map_nil ⇒ Some ? right |
---|
| 782 | | _ ⇒ |
---|
| 783 | match right with |
---|
| 784 | [ map_nil ⇒ Some ? left |
---|
| 785 | | _ ⇒ map_hedge_union key_type elt_type ord (λx. order_lt) (λx. order_gt) left right |
---|
| 786 | ] |
---|
| 787 | ]. |
---|