source: src/utilities/HMap.ma @ 1050

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

adding dependent types to map datastructure to remove all option types. some changes to rtlabs to rtl translation pass.

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