source: src/utilities/HMap.ma @ 1048

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

added implementation of haskell associative maps to clean up the mess of a million different ad hoc and incomplete maps used throughout the compiler. uses balanced binary trees. note, api not stable as function types are littered with options which can be cleared up with a judicious use of dependent types.
File size: 22.0 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 "basics/types.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
67inductive order: Type[0] ≝
68  | order_lt: order
69  | order_eq: order
70  | order_gt: order.
71
72(* -------------------------------------------------------------------------- *)
73(* Lookup of elements in map.                                                 *)
74(* -------------------------------------------------------------------------- *)
75let rec map_lookup
76  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order)
77  (to_search: key_type) (the_map: map key_type elt_type) on the_map ≝
78  match the_map with
79  [ map_nil                 ⇒ None ?
80  | map_fork sz key elt l r ⇒
81    match ord to_search key with
82    [ order_eq ⇒ Some ? elt
83    | order_lt ⇒ map_lookup key_type elt_type ord to_search l
84    | order_gt ⇒ map_lookup key_type elt_type ord to_search r
85    ]
86  ].
87
88definition map_lookup_assoc ≝
89  λkey_type.
90  λelt_type.
91  λord: key_type → key_type → order.
92  λto_search: key_type.
93  λthe_map: map key_type elt_type.
94  match map_lookup key_type elt_type ord to_search the_map with
95  [ None ⇒ None ?
96  | Some found ⇒ Some ? 〈to_search, found〉
97  ].
98
99definition map_lookup_default ≝
100  λkey_type.
101  λelt_type.
102  λord: key_type → key_type → order.
103  λto_search: key_type.
104  λdef: elt_type.
105  λthe_map: map key_type elt_type.
106  match map_lookup key_type elt_type ord to_search the_map with
107  [ None ⇒ def
108  | Some found ⇒ found
109  ].
110
111definition map_member ≝
112  λkey_type.
113  λelt_type.
114  λord: key_type → key_type → order.
115  λto_search: key_type.
116  λthe_map: map key_type elt_type.
117  match map_lookup key_type elt_type ord to_search the_map with
118  [ None ⇒ false
119  | Some found ⇒ true
120  ].
121
122definition map_not_member ≝
123  λkey_type.
124  λelt_type.
125  λord: key_type → key_type → order.
126  λto_search: key_type.
127  λthe_map: map key_type elt_type.
128  match map_lookup key_type elt_type ord to_search the_map with
129  [ None ⇒ true
130  | Some found ⇒ false
131  ].
132
133(* -------------------------------------------------------------------------- *)
134(* Creation of maps.                                                          *)
135(* -------------------------------------------------------------------------- *)
136definition map_empty ≝
137  λkey_type.
138  λelt_type.
139    map_nil key_type elt_type.
140
141definition map_singleton ≝
142  λkey_type.
143  λelt_type.
144  λkey: key_type.
145  λelt: elt_type.
146    map_fork key_type elt_type 1 key elt (map_nil ? ?) (map_nil ? ?).
147
148(* -------------------------------------------------------------------------- *)
149(* Internal, related to balancing and rotating nodes.                         *)
150(* -------------------------------------------------------------------------- *)
151definition map_delta ≝ 4.
152definition map_ratio ≝ 2.
153
154definition map_binsert ≝
155  λkey_type.
156  λelt_type.
157  λkey: key_type.
158  λelt: elt_type.
159  λleft: map key_type elt_type.
160  λright: map key_type elt_type.
161    map_fork ? ? (1 + map_size ? ? left + map_size ? ? right) key elt left right.
162
163(* Single rotations, left and right. *)
164definition map_single_l ≝
165  λkey_type.
166  λelt_type.
167  λkey: key_type.
168  λelt: elt_type.
169  λleft: map key_type elt_type.
170  λright: map key_type elt_type.
171  match right with
172  [ map_nil ⇒ None ?
173  | map_fork r_sz r_key r_elt r_l r_r ⇒
174      Some ? (map_binsert ? ? r_key r_elt (map_binsert ? ? key elt left r_l) r_r)
175  ].
176
177definition map_single_r ≝
178  λkey_type.
179  λelt_type.
180  λkey: key_type.
181  λelt: elt_type.
182  λleft: map key_type elt_type.
183  λright: map key_type elt_type.
184  match left with
185  [ map_nil ⇒ None ?
186  | map_fork l_sz l_key l_elt l_l l_r ⇒
187      Some ? (map_binsert ? ? l_key l_elt l_l (map_binsert ? ? key elt l_r right))
188  ].
189
190definition map_double_r ≝
191  λkey_type.
192  λelt_type.
193  λkey: key_type.
194  λelt: elt_type.
195  λleft: map key_type elt_type.
196  λright: map key_type elt_type.
197  match left with
198  [ map_nil ⇒ None ?
199  | map_fork l_sz l_key l_elt l_l l_r ⇒
200    match l_r with
201    [ map_nil ⇒ None ?
202    | map_fork lr_sz lr_key lr_elt lr_l lr_r ⇒
203      Some ? (map_binsert … lr_key lr_elt (map_binsert … l_key l_elt l_l lr_l) (map_binsert … key elt lr_r right))
204    ]
205  ].
206
207definition map_double_l ≝
208  λkey_type.
209  λelt_type.
210  λkey: key_type.
211  λelt: elt_type.
212  λleft: map key_type elt_type.
213  λright: map key_type elt_type.
214  match right with
215  [ map_nil ⇒ None …
216  | map_fork r_sz r_key r_elt r_l r_r ⇒
217    match r_l with
218    [ map_nil ⇒ None …
219    | map_fork rl_sz rl_key rl_elt rl_l rl_r ⇒
220      Some ? (map_binsert … rl_key rl_elt (map_binsert … key elt left rl_l) (map_binsert … r_key r_elt rl_r r_r))
221    ]
222  ].
223
224definition map_rotate_r ≝
225  λkey_type.
226  λelt_type.
227  λkey: key_type.
228  λelt: elt_type.
229  λleft: map key_type elt_type.
230  λright: map key_type elt_type.
231  match left with
232  [ map_nil ⇒ None ?
233  | map_fork l_sz l_key l_elt l_l l_r ⇒
234    if ltb (map_size ? ? l_r) (map_ratio * map_size ? ? l_l) then
235      map_single_r ? ? key elt left right
236    else
237      map_double_r ? ? key elt left right
238  ].
239
240(* fails only when right = nil *)
241definition map_rotate_l ≝
242  λkey_type.
243  λelt_type.
244  λkey: key_type.
245  λelt: elt_type.
246  λleft: map key_type elt_type.
247  λright: map key_type elt_type.
248  match right with
249  [ map_nil ⇒ None ?
250  | map_fork r_sz r_key r_elt r_l r_r ⇒
251      if ltb (map_size ? ? r_l) (map_ratio * map_size ? ? r_r) then
252        map_single_l ? ? key elt left right
253      else
254        map_double_l ? ? key elt left right
255  ].
256 
257definition map_balance ≝
258  λkey_type.
259  λelt_type.
260  λkey: key_type.
261  λelt: elt_type.
262  λleft: map key_type elt_type.
263  λright: map key_type elt_type.
264  let size_l ≝ map_size ? ? left in
265  let size_r ≝ map_size ? ? right in
266  let size_x ≝ 1 + size_l + size_r in
267    if leb (size_l + size_r) 1 then
268      Some ? (map_fork ? ? size_x key elt left right)
269    else if geb size_r (map_delta * size_l) then
270      map_rotate_l ? ? key elt left right
271    else if geb size_l (map_delta * size_r) then
272      map_rotate_r ? ? key elt left right
273    else
274      Some ? (map_fork ? ? size_x key elt left right).
275
276let rec map_delete_find_min
277  (key_type: Type[0]) (elt_type: Type[0]) (the_map: map key_type elt_type) on the_map ≝
278  match the_map with
279  [ map_nil ⇒ None ?
280  | map_fork sz key elt l r ⇒
281    match l with
282    [ map_nil ⇒ Some ? 〈〈key, elt〉, r〉
283    | _ ⇒
284      match map_delete_find_min key_type elt_type l with
285      [ None ⇒ None ?
286      | Some kmn ⇒
287        let 〈km, new〉 ≝ kmn in
288        match map_balance key_type elt_type key elt new r with
289        [ None ⇒ None ?
290        | Some balanced ⇒ Some ? 〈km, balanced〉
291        ]
292      ]
293    ]
294  ].
295
296let rec map_delete_find_max
297  (key_type: Type[0]) (elt_type: Type[0]) (the_map: map key_type elt_type) on the_map ≝
298  match the_map with
299  [ map_nil ⇒ None ?
300  | map_fork sz key elt l r ⇒
301    match r with
302    [ map_nil ⇒ Some ? 〈〈key, elt〉, l〉
303    | _ ⇒
304      match map_delete_find_max key_type elt_type r with
305      [ None ⇒ None ?
306      | Some kmn ⇒
307        let 〈km, new〉 ≝ kmn in
308        match map_balance key_type elt_type key elt l new with
309        [ None ⇒ None ?
310        | Some balanced ⇒ Some ? 〈km, balanced〉
311        ]
312      ]
313    ]
314  ].
315
316definition map_glue ≝
317  λkey_type.
318  λelt_type.
319  λleft: map key_type elt_type.
320  λright: map key_type elt_type.
321  match left with
322  [ map_nil ⇒ Some ? right
323  | map_fork l_sz l_key l_elt l_l l_r ⇒
324    match right with
325    [ map_nil ⇒ Some ? left
326    | map_fork r_sz r_key r_elt r_l r_r ⇒
327      if gtb l_sz r_sz then
328        match map_delete_find_max key_type elt_type left with
329        [ None ⇒ None ?
330        | Some kmml' ⇒
331          let 〈kmm, l'〉 ≝ kmml' in
332          let 〈km, m〉 ≝ kmm in
333            map_balance key_type elt_type km m l' right
334        ]
335      else
336        match map_delete_find_min key_type elt_type right with
337        [ None ⇒ None ?
338        | Some kmmr' ⇒
339          let 〈kmm, r'〉 ≝ kmmr' in
340          let 〈km, m〉 ≝ kmm in
341            map_balance key_type elt_type km m left r'
342        ]
343    ]
344  ].
345
346(* -------------------------------------------------------------------------- *)
347(* Inserting elements.                                                        *)
348(* -------------------------------------------------------------------------- *)
349
350let rec map_insert
351  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order)
352  (key: key_type) (elt: elt_type) (the_map: map key_type elt_type) on the_map: option (map key_type elt_type) ≝
353  match the_map with
354  [ map_nil ⇒ Some ? (map_singleton … key elt)
355  | map_fork m_sz m_key m_elt m_l m_r ⇒
356    match ord m_key key with
357    [ order_lt ⇒
358      match map_insert … ord key elt m_l with
359      [ None ⇒ None ?
360      | Some new_l ⇒ map_balance … m_key m_elt new_l m_r
361      ]
362    | order_eq ⇒ Some ? (map_fork key_type elt_type m_sz key elt m_l m_r)
363    | order_gt ⇒
364      match map_insert key_type elt_type ord key elt m_r with
365      [ None ⇒ None ?
366      | Some new_r ⇒ map_balance key_type elt_type m_key m_elt m_l new_r
367      ]
368    ]
369  ].
370
371(* -------------------------------------------------------------------------- *)
372(* Deleting elements.                                                         *)
373(* -------------------------------------------------------------------------- *)
374
375let rec map_delete
376  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order)
377  (the_key: key_type) (the_map: map key_type elt_type) on the_map ≝
378  match the_map with
379  [ map_nil ⇒ Some ? (map_nil key_type elt_type)
380  | map_fork sz key elt l r ⇒
381    match ord the_key key with
382    [ order_lt ⇒
383      match map_delete key_type elt_type ord the_key l with
384      [ None ⇒ None ?
385      | Some new_l ⇒ map_balance key_type elt_type key elt new_l r
386      ]
387    | order_eq ⇒ map_glue key_type elt_type l r
388    | order_gt ⇒
389      match map_delete key_type elt_type ord the_key r with
390      [ None ⇒ None ?
391      | Some new_r ⇒ map_balance key_type elt_type key elt l new_r
392      ]
393    ]
394  ].
395 
396(* -------------------------------------------------------------------------- *)
397(* Folds.                                                                     *)
398(* -------------------------------------------------------------------------- *)
399
400let rec map_foldr_with_key
401  (key_type: Type[0]) (dom_type: Type[0]) (rng_type: Type[0])
402  (f: key_type → dom_type → rng_type → rng_type) (e: rng_type)
403  (the_map: map key_type dom_type) on the_map ≝
404  match the_map with
405  [ map_nil ⇒ e
406  | map_fork m_sz m_key m_elt m_l m_r ⇒
407    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
408  ].
409
410let rec map_foldl_with_key
411  (key_type: Type[0]) (dom_type: Type[0]) (rng_type: Type[0])
412  (f: rng_type → key_type → dom_type → rng_type) (e: rng_type)
413  (the_map: map key_type dom_type) on the_map ≝
414  match the_map with
415  [ map_nil ⇒ e
416  | map_fork m_sz m_key m_elt m_l m_r ⇒
417      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
418  ].
419
420definition map_fold ≝
421  λkey_type.
422  λdom_type.
423  λrng_type.
424  λf: dom_type → rng_type → rng_type.
425    map_foldr_with_key key_type dom_type rng_type (λi. λx'. λz'. f x' z').
426
427(* -------------------------------------------------------------------------- *)
428(* Maps.                                                                      *)
429(* -------------------------------------------------------------------------- *)
430   
431let rec map_map_with_key
432  (key_type: Type[0]) (dom_type: Type[0]) (rng_type: Type[0])
433  (f: key_type → dom_type → rng_type) (the_map: map key_type dom_type) on the_map ≝
434  match the_map with
435  [ map_nil ⇒ map_nil key_type rng_type
436  | map_fork m_sz m_key m_elt m_l m_r ⇒
437    map_fork key_type rng_type m_sz m_key (f m_key m_elt)
438      (map_map_with_key key_type dom_type rng_type f m_l)
439      (map_map_with_key key_type dom_type rng_type f m_r)
440  ].
441
442definition map_map ≝
443  λkey_type.
444  λdom_type.
445  λrng_type.
446  λf: dom_type → rng_type.
447  λthe_map: map key_type dom_type.
448    map_map_with_key key_type dom_type rng_type (λk. f) the_map.
449
450(* -------------------------------------------------------------------------- *)
451(* Unions.                                                                    *)
452(* -------------------------------------------------------------------------- *)
453
454let rec map_insert_max
455  (key_type: Type[0]) (elt_type: Type[0]) (key: key_type) (elt: elt_type)
456  (the_map: map key_type elt_type) on the_map ≝
457  match the_map with
458  [ map_nil ⇒ Some ? (map_singleton key_type elt_type key elt)
459  | map_fork m_sz m_key m_elt m_l m_r ⇒
460    match map_insert_max key_type elt_type key elt m_r with
461    [ None ⇒ None ?
462    | Some new_r ⇒ map_balance key_type elt_type m_key m_elt m_l new_r
463    ]
464  ].
465
466let rec map_insert_min
467  (key_type: Type[0]) (elt_type: Type[0]) (key: key_type) (elt: elt_type)
468  (the_map: map key_type elt_type) on the_map ≝
469  match the_map with
470  [ map_nil ⇒ Some ? (map_singleton key_type elt_type key elt)
471  | map_fork m_sz m_key m_elt m_l m_r ⇒
472    match map_insert_min key_type elt_type key elt m_l with
473    [ None ⇒ None ?
474    | Some new_l ⇒ map_balance key_type elt_type m_key m_elt new_l m_r
475    ]
476  ].
477
478definition map_join_prf' ≝
479  λkey_type.
480  λelt_type.
481  λmeasure: nat × nat.
482  λleft: map key_type elt_type.
483  λright: map key_type elt_type.
484  \fst measure = O → left = map_nil key_type elt_type →
485  \snd measure = O → left = map_nil key_type elt_type →
486  ∀n. ∀l_sz. ∀l_key. ∀l_elt. ∀l_l. ∀l_r.
487    \fst measure = S n → left = map_fork key_type elt_type l_sz l_key l_elt l_l l_r →
488  ∀n. ∀r_sz. ∀r_key. ∀r_elt. ∀r_l. ∀r_r.
489    \snd measure = S n → left = map_fork key_type elt_type r_sz r_key r_elt r_l r_r.
490
491axiom map_join':
492  ∀key_type.
493  ∀elt_type.
494  ∀key: key_type.
495  ∀elt: elt_type.
496  ∀left: map key_type elt_type.
497  ∀right: map key_type elt_type.
498  ∀measure: nat × nat.
499  ∀prf: map_join_prf' key_type elt_type measure left right.
500    option (map key_type elt_type).
501
502(*
503let rec map_join'
504  (key_type: Type[0]) (elt_type: Type[0]) (key: key_type) (elt: elt_type)
505  (left: map key_type elt_type) (right: map key_type elt_type)
506  (measure: nat × nat)
507  (prf: map_join_prf' key_type elt_type measure left right)
508  on measure: option (map key_type elt_type) ≝
509  let size_l ≝ \fst measure in
510  let size_r ≝ \snd measure in
511  match size_l return λx. map_join_prf' key_type elt_type 〈x, size_r〉 left right → option (map key_type elt_type) with
512  [ O ⇒
513    λprf_left_nil: map_join_prf' key_type elt_type 〈0, size_r〉 left right.
514      map_insert_min key_type elt_type key elt right
515  | S size_l' ⇒
516    match left with
517    [ map_nil ⇒
518      λprf_left_nil_abs: map_join_prf' key_type elt_type 〈S size_l', size_r〉 left right. ?
519    | map_fork l_sz l_key l_elt l_l l_r ⇒
520      λprf_left_fork: map_join_prf' key_type elt_type 〈size_l', size_r〉 l_l l_r.
521      match size_r return λy. map_join_prf' key_type elt_type 〈size_l', y〉 left right → option (map key_type elt_type) with
522      [ O ⇒
523        λprf_right_nil: map_join_prf' key_type elt_type 〈size_l', 0〉 left right.
524          map_insert_max key_type elt_type key elt left
525      | S size_r' ⇒
526        match right with
527        [ map_nil ⇒
528          λprf_right_nil_abs: map_join_prf' key_type elt_type 〈S size_l', S size_r'〉 left right. ?
529        | map_fork r_sz r_key r_elt r_l r_r ⇒
530          λprf_right_fork: map_join_prf' key_type elt_type 〈size_l', size_r'〉 r_l r_r.
531            if ltb (map_delta * l_sz) r_sz then
532              match map_join' key_type elt_type key elt left r_l 〈S size_l', S size_r'〉 ? with
533              [ None ⇒ None ?
534              | Some joined ⇒
535                  map_balance key_type elt_type r_key r_elt joined r_r
536              ]
537            else if ltb (map_delta * r_sz) l_sz then
538              match map_join' key_type elt_type key elt l_r right 〈S size_l', S size_r'〉 ? with
539              [ None ⇒ None ?
540              | Some joined ⇒
541                  map_balance key_type elt_type l_key l_elt l_l joined
542              ]
543            else
544              Some ? (map_binsert key_type elt_type key elt left right)
545         ]
546       ] ?
547     ]
548   ] ?.
549   [ 3: @prf_right_fork
550   | 4: @prf_left_fork
551*)
552
553(* requires some crazy trick to convince termination checker *)
554axiom map_join:
555  ∀key_type.
556  ∀elt_type.
557  ∀key: key_type.
558  ∀elt: elt_type.
559  ∀left: map key_type elt_type.
560  ∀right: map key_type elt_type.
561    option (map key_type elt_type).
562
563let rec map_filter_gt
564  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → order)
565  (the_map: map key_type elt_type) on the_map ≝
566  match the_map with
567  [ map_nil ⇒ Some ? (map_nil key_type elt_type)
568  | map_fork m_sz m_key m_elt m_l m_r ⇒
569    match ord m_key with
570    [ order_eq ⇒ Some ? m_r
571    | order_lt ⇒
572      match map_filter_gt key_type elt_type ord m_l with
573      [ None ⇒ None ?
574      | Some filtered ⇒
575          map_join key_type elt_type m_key m_elt filtered m_r
576      ]
577    | order_gt ⇒ map_filter_gt key_type elt_type ord m_r
578    ]
579  ].
580
581let rec map_filter_lt
582  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → order)
583  (the_map: map key_type elt_type) on the_map ≝
584  match the_map with
585  [ map_nil ⇒ Some ? (map_nil key_type elt_type)
586  | map_fork m_sz m_key m_elt m_l m_r ⇒
587    match ord m_key with
588    [ order_eq ⇒ Some ? m_l
589    | order_lt ⇒ map_filter_lt key_type elt_type ord m_l
590    | order_gt ⇒
591      match map_filter_lt key_type elt_type ord m_r with
592      [ None ⇒ None ?
593      | Some filtered ⇒ map_join key_type elt_type m_key m_elt m_l filtered
594      ]
595    ]
596  ].
597
598let rec map_trim
599  (key_type: Type[0]) (elt_type: Type[0]) (lord: key_type → order)
600  (hord: key_type → order) (the_map: map key_type elt_type) on the_map ≝
601  match the_map with
602  [ map_nil ⇒ map_nil key_type elt_type
603  | map_fork m_sz m_key m_elt m_l m_r ⇒
604    match lord m_key with
605    [ order_lt ⇒
606      match hord m_key with
607      [ order_gt ⇒ the_map
608      | _ ⇒ map_trim key_type elt_type lord hord m_l
609      ]
610    | _ ⇒ map_trim key_type elt_type lord hord m_r
611    ]
612  ].
613 
614axiom map_hedge_union:
615  ∀key_type: Type[0].
616  ∀elt_type: Type[0].
617  ∀ord: key_type → key_type → order.
618  ∀lord: key_type → order.
619  ∀hord: key_type → order.
620  ∀left: map key_type elt_type.
621  ∀right: map key_type elt_type.
622    option (map key_type elt_type).
623
624(*
625(* left biased hedge union *)
626let rec map_hedge_union
627  (key_type: Type[0]) (elt_type: Type[0]) (ord: key_type → key_type → order)
628  (lord: key_type → order) (hord: key_type → order)
629(*  (prod: (map key_type elt_type) × (map key_type elt_type)) on prod ≝ *)
630  (left: map key_type elt_type) (right: map key_type elt_type) on right ≝
631  let 〈left, right〉 ≝ prod in
632  match right with
633  [ map_nil ⇒ Some ? left
634  | map_fork r_sz r_key r_elt r_l r_r ⇒
635    match left with
636    [ map_nil ⇒
637      match map_filter_gt key_type elt_type lord r_l with
638      [ None ⇒ None ?
639      | Some filtered_gt ⇒
640        match map_filter_lt key_type elt_type hord r_r with
641        [ None ⇒ None ?
642        | Some filtered_lt ⇒ map_join key_type elt_type r_key r_elt filtered_gt filtered_lt
643        ]
644      ]
645    | map_fork l_sz l_key l_elt l_l l_r ⇒
646      let xord ≝ λk: key_type. ord l_key k in
647      let trimmed_l ≝ map_trim key_type elt_type lord xord right in
648      let trimmed_r ≝ map_trim key_type elt_type xord hord right in
649      match map_hedge_union key_type elt_type ord lord xord 〈l_l, trimmed_l〉 with
650      [ None ⇒ None ?
651      | Some hedged_l ⇒
652        match map_hedge_union key_type elt_type ord xord hord 〈l_r, trimmed_r〉 with
653        [ None ⇒ None ?
654        | Some hedged_r ⇒ map_join key_type elt_type l_key l_elt hedged_l hedged_r
655        ]
656      ]
657    ]
658  ].
659*)
660
661definition map_union ≝
662  λkey_type.
663  λelt_type.
664  λord: key_type → key_type → order.
665  λleft: map key_type elt_type.
666  λright: map key_type elt_type.
667  match left with
668  [ map_nil ⇒ Some ? right
669  | _ ⇒
670    match right with
671    [ map_nil ⇒ Some ? left
672    | _ ⇒ map_hedge_union key_type elt_type ord (λx. order_lt) (λx. order_gt) left right
673    ]
674  ].
Note: See TracBrowser for help on using the repository browser.