source: src/utilities/HMap.ma @ 1133

Last change on this file since 1133 was 1052, checked in by mulligan, 9 years ago

removed offsets after reading cerco mailing list

File size: 25.0 KB
RevLine 
[1048]1(* -------------------------------------------------------------------------- *)
2(* Generic associative map data structure, using balanced binary trees, based *)
3(* on Data.Map from the Haskell standard library.                             *)
4(* -------------------------------------------------------------------------- *)
5
6include "arithmetics/nat.ma".
[1049]7include "common/Order.ma".
[1048]8
9(* for eq_rect_Type0_r *)
10include "ASM/Util.ma".
11
12inductive 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
20definition 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
29definition 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   
38definition 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
47definition 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(* -------------------------------------------------------------------------- *)
58definition 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(* -------------------------------------------------------------------------- *)
70let 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
83definition 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
94definition 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
106definition 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
117definition 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(* -------------------------------------------------------------------------- *)
131definition map_empty ≝
132  λkey_type.
133  λelt_type.
134    map_nil key_type elt_type.
135
136definition 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(* -------------------------------------------------------------------------- *)
146definition map_delta ≝ 4.
147definition map_ratio ≝ 2.
148
149definition 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. *)
159definition 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]172definition 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
187qed.
188
[1048]189definition 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]202definition 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
217qed.
218
219definition 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]232lemma 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  ]
261qed.
262
263lemma 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  ]
301qed.
302
[1048]303definition 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
320definition 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
337definition 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 *)
354definition 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 
370definition 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
389let 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
409let 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
429definition 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
463let 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
488let 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
513let 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
523let 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
533definition 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   
544let 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
555definition 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
567let 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
579let 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
591definition 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
604axiom 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(*
616let 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 *)
667axiom 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
676let 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
694let 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
711let 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 
727axiom 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 *)
739let 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
774definition 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  ].
Note: See TracBrowser for help on using the repository browser.