source: src/utilities/HMap.ma @ 1049

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

more stuff added

File size: 21.9 KB
Line 
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".
7include "common/Order.ma".
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
172definition map_single_r ≝
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  match left with
180  [ map_nil ⇒ None ?
181  | map_fork l_sz l_key l_elt l_l l_r ⇒
182      Some ? (map_binsert ? ? l_key l_elt l_l (map_binsert ? ? key elt l_r right))
183  ].
184
185definition map_double_r ≝
186  λkey_type.
187  λelt_type.
188  λkey: key_type.
189  λelt: elt_type.
190  λleft: map key_type elt_type.
191  λright: map key_type elt_type.
192  match left with
193  [ map_nil ⇒ None ?
194  | map_fork l_sz l_key l_elt l_l l_r ⇒
195    match l_r with
196    [ map_nil ⇒ None ?
197    | map_fork lr_sz lr_key lr_elt lr_l lr_r ⇒
198      Some ? (map_binsert … lr_key lr_elt (map_binsert … l_key l_elt l_l lr_l) (map_binsert … key elt lr_r right))
199    ]
200  ].
201
202definition map_double_l ≝
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  match right with
210  [ map_nil ⇒ None …
211  | map_fork r_sz r_key r_elt r_l r_r ⇒
212    match r_l with
213    [ map_nil ⇒ None …
214    | map_fork rl_sz rl_key rl_elt rl_l rl_r ⇒
215      Some ? (map_binsert … rl_key rl_elt (map_binsert … key elt left rl_l) (map_binsert … r_key r_elt rl_r r_r))
216    ]
217  ].
218
219definition map_rotate_r ≝
220  λkey_type.
221  λelt_type.
222  λkey: key_type.
223  λelt: elt_type.
224  λleft: map key_type elt_type.
225  λright: map key_type elt_type.
226  match left with
227  [ map_nil ⇒ None ?
228  | map_fork l_sz l_key l_elt l_l l_r ⇒
229    if ltb (map_size ? ? l_r) (map_ratio * map_size ? ? l_l) then
230      map_single_r ? ? key elt left right
231    else
232      map_double_r ? ? key elt left right
233  ].
234
235(* fails only when right = nil *)
236definition map_rotate_l ≝
237  λkey_type.
238  λelt_type.
239  λkey: key_type.
240  λelt: elt_type.
241  λleft: map key_type elt_type.
242  λright: map key_type elt_type.
243  match right with
244  [ map_nil ⇒ None ?
245  | map_fork r_sz r_key r_elt r_l r_r ⇒
246      if ltb (map_size ? ? r_l) (map_ratio * map_size ? ? r_r) then
247        map_single_l ? ? key elt left right
248      else
249        map_double_l ? ? key elt left right
250  ].
251 
252definition map_balance ≝
253  λkey_type.
254  λelt_type.
255  λkey: key_type.
256  λelt: elt_type.
257  λleft: map key_type elt_type.
258  λright: map key_type elt_type.
259  let size_l ≝ map_size ? ? left in
260  let size_r ≝ map_size ? ? right in
261  let size_x ≝ 1 + size_l + size_r in
262    if leb (size_l + size_r) 1 then
263      Some ? (map_fork ? ? size_x key elt left right)
264    else if geb size_r (map_delta * size_l) then
265      map_rotate_l ? ? key elt left right
266    else if geb size_l (map_delta * size_r) then
267      map_rotate_r ? ? key elt left right
268    else
269      Some ? (map_fork ? ? size_x key elt left right).
270
271let rec map_delete_find_min
272  (key_type: Type[0]) (elt_type: Type[0]) (the_map: map key_type elt_type) on the_map ≝
273  match the_map with
274  [ map_nil ⇒ None ?
275  | map_fork sz key elt l r ⇒
276    match l with
277    [ map_nil ⇒ Some ? 〈〈key, elt〉, r〉
278    | _ ⇒
279      match map_delete_find_min key_type elt_type l with
280      [ None ⇒ None ?
281      | Some kmn ⇒
282        let 〈km, new〉 ≝ kmn in
283        match map_balance key_type elt_type key elt new r with
284        [ None ⇒ None ?
285        | Some balanced ⇒ Some ? 〈km, balanced〉
286        ]
287      ]
288    ]
289  ].
290
291let rec map_delete_find_max
292  (key_type: Type[0]) (elt_type: Type[0]) (the_map: map key_type elt_type) on the_map ≝
293  match the_map with
294  [ map_nil ⇒ None ?
295  | map_fork sz key elt l r ⇒
296    match r with
297    [ map_nil ⇒ Some ? 〈〈key, elt〉, l〉
298    | _ ⇒
299      match map_delete_find_max key_type elt_type r with
300      [ None ⇒ None ?
301      | Some kmn ⇒
302        let 〈km, new〉 ≝ kmn in
303        match map_balance key_type elt_type key elt l new with
304        [ None ⇒ None ?
305        | Some balanced ⇒ Some ? 〈km, balanced〉
306        ]
307      ]
308    ]
309  ].
310
311definition map_glue ≝
312  λkey_type.
313  λelt_type.
314  λleft: map key_type elt_type.
315  λright: map key_type elt_type.
316  match left with
317  [ map_nil ⇒ Some ? right
318  | map_fork l_sz l_key l_elt l_l l_r ⇒
319    match right with
320    [ map_nil ⇒ Some ? left
321    | map_fork r_sz r_key r_elt r_l r_r ⇒
322      if gtb l_sz r_sz then
323        match map_delete_find_max key_type elt_type left with
324        [ None ⇒ None ?
325        | Some kmml' ⇒
326          let 〈kmm, l'〉 ≝ kmml' in
327          let 〈km, m〉 ≝ kmm in
328            map_balance key_type elt_type km m l' right
329        ]
330      else
331        match map_delete_find_min key_type elt_type right with
332        [ None ⇒ None ?
333        | Some kmmr' ⇒
334          let 〈kmm, r'〉 ≝ kmmr' in
335          let 〈km, m〉 ≝ kmm in
336            map_balance key_type elt_type km m left r'
337        ]
338    ]
339  ].
340
341(* -------------------------------------------------------------------------- *)
342(* Inserting elements.                                                        *)
343(* -------------------------------------------------------------------------- *)
344
345let rec map_insert
346  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order)
347  (key: key_type) (elt: elt_type) (the_map: map key_type elt_type) on the_map: option (map key_type elt_type) ≝
348  match the_map with
349  [ map_nil ⇒ Some ? (map_singleton … key elt)
350  | map_fork m_sz m_key m_elt m_l m_r ⇒
351    match ord m_key key with
352    [ order_lt ⇒
353      match map_insert … ord key elt m_l with
354      [ None ⇒ None ?
355      | Some new_l ⇒ map_balance … m_key m_elt new_l m_r
356      ]
357    | order_eq ⇒ Some ? (map_fork key_type elt_type m_sz key elt m_l m_r)
358    | order_gt ⇒
359      match map_insert key_type elt_type ord key elt m_r with
360      [ None ⇒ None ?
361      | Some new_r ⇒ map_balance key_type elt_type m_key m_elt m_l new_r
362      ]
363    ]
364  ].
365
366(* -------------------------------------------------------------------------- *)
367(* Deleting elements.                                                         *)
368(* -------------------------------------------------------------------------- *)
369
370let rec map_delete
371  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order)
372  (the_key: key_type) (the_map: map key_type elt_type) on the_map ≝
373  match the_map with
374  [ map_nil ⇒ Some ? (map_nil key_type elt_type)
375  | map_fork sz key elt l r ⇒
376    match ord the_key key with
377    [ order_lt ⇒
378      match map_delete key_type elt_type ord the_key l with
379      [ None ⇒ None ?
380      | Some new_l ⇒ map_balance key_type elt_type key elt new_l r
381      ]
382    | order_eq ⇒ map_glue key_type elt_type l r
383    | order_gt ⇒
384      match map_delete key_type elt_type ord the_key r with
385      [ None ⇒ None ?
386      | Some new_r ⇒ map_balance key_type elt_type key elt l new_r
387      ]
388    ]
389  ].
390 
391(* -------------------------------------------------------------------------- *)
392(* Folds.                                                                     *)
393(* -------------------------------------------------------------------------- *)
394
395let rec map_foldr_with_key
396  (key_type: Type[0]) (dom_type: Type[0]) (rng_type: Type[0])
397  (f: key_type → dom_type → rng_type → rng_type) (e: rng_type)
398  (the_map: map key_type dom_type) on the_map ≝
399  match the_map with
400  [ map_nil ⇒ e
401  | map_fork m_sz m_key m_elt m_l m_r ⇒
402    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
403  ].
404
405let rec map_foldl_with_key
406  (key_type: Type[0]) (dom_type: Type[0]) (rng_type: Type[0])
407  (f: rng_type → key_type → dom_type → rng_type) (e: rng_type)
408  (the_map: map key_type dom_type) on the_map ≝
409  match the_map with
410  [ map_nil ⇒ e
411  | map_fork m_sz m_key m_elt m_l m_r ⇒
412      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
413  ].
414
415definition map_fold ≝
416  λkey_type.
417  λdom_type.
418  λrng_type.
419  λf: dom_type → rng_type → rng_type.
420    map_foldr_with_key key_type dom_type rng_type (λi. λx'. λz'. f x' z').
421
422(* -------------------------------------------------------------------------- *)
423(* Maps.                                                                      *)
424(* -------------------------------------------------------------------------- *)
425   
426let rec map_map_with_key
427  (key_type: Type[0]) (dom_type: Type[0]) (rng_type: Type[0])
428  (f: key_type → dom_type → rng_type) (the_map: map key_type dom_type) on the_map ≝
429  match the_map with
430  [ map_nil ⇒ map_nil key_type rng_type
431  | map_fork m_sz m_key m_elt m_l m_r ⇒
432    map_fork key_type rng_type m_sz m_key (f m_key m_elt)
433      (map_map_with_key key_type dom_type rng_type f m_l)
434      (map_map_with_key key_type dom_type rng_type f m_r)
435  ].
436
437definition map_map ≝
438  λkey_type.
439  λdom_type.
440  λrng_type.
441  λf: dom_type → rng_type.
442  λthe_map: map key_type dom_type.
443    map_map_with_key key_type dom_type rng_type (λk. f) the_map.
444
445(* -------------------------------------------------------------------------- *)
446(* Unions.                                                                    *)
447(* -------------------------------------------------------------------------- *)
448
449let rec map_insert_max
450  (key_type: Type[0]) (elt_type: Type[0]) (key: key_type) (elt: elt_type)
451  (the_map: map key_type elt_type) on the_map ≝
452  match the_map with
453  [ map_nil ⇒ Some ? (map_singleton key_type elt_type key elt)
454  | map_fork m_sz m_key m_elt m_l m_r ⇒
455    match map_insert_max key_type elt_type key elt m_r with
456    [ None ⇒ None ?
457    | Some new_r ⇒ map_balance key_type elt_type m_key m_elt m_l new_r
458    ]
459  ].
460
461let rec map_insert_min
462  (key_type: Type[0]) (elt_type: Type[0]) (key: key_type) (elt: elt_type)
463  (the_map: map key_type elt_type) on the_map ≝
464  match the_map with
465  [ map_nil ⇒ Some ? (map_singleton key_type elt_type key elt)
466  | map_fork m_sz m_key m_elt m_l m_r ⇒
467    match map_insert_min key_type elt_type key elt m_l with
468    [ None ⇒ None ?
469    | Some new_l ⇒ map_balance key_type elt_type m_key m_elt new_l m_r
470    ]
471  ].
472
473definition map_join_prf' ≝
474  λkey_type.
475  λelt_type.
476  λmeasure: nat × nat.
477  λleft: map key_type elt_type.
478  λright: map key_type elt_type.
479  \fst measure = O → left = map_nil key_type elt_type →
480  \snd measure = O → left = map_nil key_type elt_type →
481  ∀n. ∀l_sz. ∀l_key. ∀l_elt. ∀l_l. ∀l_r.
482    \fst measure = S n → left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r →
483  ∀n. ∀r_sz. ∀r_key. ∀r_elt. ∀r_l. ∀r_r.
484    \snd measure = S n → left = map_fork key_type elt_type r_sz r_key r_elt r_l r_r.
485
486axiom map_join':
487  ∀key_type.
488  ∀elt_type.
489  ∀key: key_type.
490  ∀elt: elt_type.
491  ∀left: map key_type elt_type.
492  ∀right: map key_type elt_type.
493  ∀measure: nat × nat.
494  ∀prf: map_join_prf' key_type elt_type measure left right.
495    option (map key_type elt_type).
496
497(*
498let rec map_join'
499  (key_type: Type[0]) (elt_type: Type[0]) (key: key_type) (elt: elt_type)
500  (left: map key_type elt_type) (right: map key_type elt_type)
501  (measure: nat × nat)
502  (prf: map_join_prf' key_type elt_type measure left right)
503  on measure: option (map key_type elt_type) ≝
504  let size_l ≝ \fst measure in
505  let size_r ≝ \snd measure in
506  match size_l return λx. map_join_prf' key_type elt_type 〈x, size_r〉 left right → option (map key_type elt_type) with
507  [ O ⇒
508    λprf_left_nil: map_join_prf' key_type elt_type 〈0, size_r〉 left right.
509      map_insert_min key_type elt_type key elt right
510  | S size_l' ⇒
511    match left with
512    [ map_nil ⇒
513      λprf_left_nil_abs: map_join_prf' key_type elt_type 〈S size_l', size_r〉 left right. ?
514    | map_fork l_sz l_key l_elt l_l l_r ⇒
515      λprf_left_fork: map_join_prf' key_type elt_type 〈size_l', size_r〉 l_l l_r.
516      match size_r return λy. map_join_prf' key_type elt_type 〈size_l', y〉 left right → option (map key_type elt_type) with
517      [ O ⇒
518        λprf_right_nil: map_join_prf' key_type elt_type 〈size_l', 0〉 left right.
519          map_insert_max key_type elt_type key elt left
520      | S size_r' ⇒
521        match right with
522        [ map_nil ⇒
523          λprf_right_nil_abs: map_join_prf' key_type elt_type 〈S size_l', S size_r'〉 left right. ?
524        | map_fork r_sz r_key r_elt r_l r_r ⇒
525          λprf_right_fork: map_join_prf' key_type elt_type 〈size_l', size_r'〉 r_l r_r.
526            if ltb (map_delta * l_sz) r_sz then
527              match map_join' key_type elt_type key elt left r_l 〈S size_l', S size_r'〉 ? with
528              [ None ⇒ None ?
529              | Some joined ⇒
530                  map_balance key_type elt_type r_key r_elt joined r_r
531              ]
532            else if ltb (map_delta * r_sz) l_sz then
533              match map_join' key_type elt_type key elt l_r right 〈S size_l', S size_r'〉 ? with
534              [ None ⇒ None ?
535              | Some joined ⇒
536                  map_balance key_type elt_type l_key l_elt l_l joined
537              ]
538            else
539              Some ? (map_binsert key_type elt_type key elt left right)
540         ]
541       ] ?
542     ]
543   ] ?.
544   [ 3: @prf_right_fork
545   | 4: @prf_left_fork
546*)
547
548(* requires some crazy trick to convince termination checker *)
549axiom map_join:
550  ∀key_type.
551  ∀elt_type.
552  ∀key: key_type.
553  ∀elt: elt_type.
554  ∀left: map key_type elt_type.
555  ∀right: map key_type elt_type.
556    option (map key_type elt_type).
557
558let rec map_filter_gt
559  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → order)
560  (the_map: map key_type elt_type) on the_map ≝
561  match the_map with
562  [ map_nil ⇒ Some ? (map_nil key_type elt_type)
563  | map_fork m_sz m_key m_elt m_l m_r ⇒
564    match ord m_key with
565    [ order_eq ⇒ Some ? m_r
566    | order_lt ⇒
567      match map_filter_gt key_type elt_type ord m_l with
568      [ None ⇒ None ?
569      | Some filtered ⇒
570          map_join key_type elt_type m_key m_elt filtered m_r
571      ]
572    | order_gt ⇒ map_filter_gt key_type elt_type ord m_r
573    ]
574  ].
575
576let rec map_filter_lt
577  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → order)
578  (the_map: map key_type elt_type) on the_map ≝
579  match the_map with
580  [ map_nil ⇒ Some ? (map_nil key_type elt_type)
581  | map_fork m_sz m_key m_elt m_l m_r ⇒
582    match ord m_key with
583    [ order_eq ⇒ Some ? m_l
584    | order_lt ⇒ map_filter_lt key_type elt_type ord m_l
585    | order_gt ⇒
586      match map_filter_lt key_type elt_type ord m_r with
587      [ None ⇒ None ?
588      | Some filtered ⇒ map_join key_type elt_type m_key m_elt m_l filtered
589      ]
590    ]
591  ].
592
593let rec map_trim
594  (key_type: Type[0]) (elt_type: Type[0]) (lord: key_type → order)
595  (hord: key_type → order) (the_map: map key_type elt_type) on the_map ≝
596  match the_map with
597  [ map_nil ⇒ map_nil key_type elt_type
598  | map_fork m_sz m_key m_elt m_l m_r ⇒
599    match lord m_key with
600    [ order_lt ⇒
601      match hord m_key with
602      [ order_gt ⇒ the_map
603      | _ ⇒ map_trim key_type elt_type lord hord m_l
604      ]
605    | _ ⇒ map_trim key_type elt_type lord hord m_r
606    ]
607  ].
608 
609axiom map_hedge_union:
610  ∀key_type: Type[0].
611  ∀elt_type: Type[0].
612  ∀ord: key_type → key_type → order.
613  ∀lord: key_type → order.
614  ∀hord: key_type → order.
615  ∀left: map key_type elt_type.
616  ∀right: map key_type elt_type.
617    option (map key_type elt_type).
618
619(*
620(* left biased hedge union *)
621let rec map_hedge_union
622  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order)
623  (lord: key_type → order) (hord: key_type → order)
624(*  (prod: (map key_type elt_type) × (map key_type elt_type)) on prod ≝ *)
625  (left: map key_type elt_type) (right: map key_type elt_type) on right ≝
626  let 〈left, right〉 ≝ prod in
627  match right with
628  [ map_nil ⇒ Some ? left
629  | map_fork r_sz r_key r_elt r_l r_r ⇒
630    match left with
631    [ map_nil ⇒
632      match map_filter_gt key_type elt_type lord r_l with
633      [ None ⇒ None ?
634      | Some filtered_gt ⇒
635        match map_filter_lt key_type elt_type hord r_r with
636        [ None ⇒ None ?
637        | Some filtered_lt ⇒ map_join key_type elt_type r_key r_elt filtered_gt filtered_lt
638        ]
639      ]
640    | map_fork l_sz l_key l_elt l_l l_r ⇒
641      let xord ≝ λk: key_type. ord l_key k in
642      let trimmed_l ≝ map_trim key_type elt_type lord xord right in
643      let trimmed_r ≝ map_trim key_type elt_type xord hord right in
644      match map_hedge_union key_type elt_type ord lord xord 〈l_l, trimmed_l〉 with
645      [ None ⇒ None ?
646      | Some hedged_l ⇒
647        match map_hedge_union key_type elt_type ord xord hord 〈l_r, trimmed_r〉 with
648        [ None ⇒ None ?
649        | Some hedged_r ⇒ map_join key_type elt_type l_key l_elt hedged_l hedged_r
650        ]
651      ]
652    ]
653  ].
654*)
655
656definition map_union ≝
657  λkey_type.
658  λelt_type.
659  λord: key_type → key_type → order.
660  λleft: map key_type elt_type.
661  λright: map key_type elt_type.
662  match left with
663  [ map_nil ⇒ Some ? right
664  | _ ⇒
665    match right with
666    [ map_nil ⇒ Some ? left
667    | _ ⇒ map_hedge_union key_type elt_type ord (λx. order_lt) (λx. order_gt) left right
668    ]
669  ].
Note: See TracBrowser for help on using the repository browser.