source: src/utilities/adt/table_adt.ma @ 1285

Last change on this file since 1285 was 1285, checked in by mulligan, 10 years ago

more implementation on maps, final push to get rtl abs to rtl working

File size: 9.7 KB
Line 
1include "basics/types.ma".
2include "basics/bool.ma".
3include "basics/list.ma".
4
5include "arithmetics/nat.ma".
6
7include "utilities/adt/equal.ma".
8include "utilities/adt/ordering.ma".
9
10include "ASM/Util.ma".
11
12inductive table (dom_type: Type[0]) (rng_type: Type[0]): Type[0] ≝
13  | empty: table dom_type rng_type
14  | node : nat → dom_type → rng_type → table dom_type rng_type → table dom_type rng_type → table dom_type rng_type.
15
16definition tbl_height ≝
17  λdom_type : Type[0].
18  λrng_type : Type[0].
19  λthe_table: table dom_type rng_type.
20  match the_table with
21  [ empty ⇒ 0
22  | node sz key val l r ⇒ sz
23  ].
24
25let rec tbl_size
26  (dom_type : Type[0]) (rng_type : Type[0]) (the_table: table dom_type rng_type)
27    on the_table: nat ≝
28  match the_table with
29  [ empty ⇒ 0
30  | node sz key val l r ⇒ S (tbl_size … l) + (tbl_size … r)
31  ].
32 
33definition tbl_empty ≝
34  λdom_type: Type[0].
35  λrng_type: Type[0].
36    empty dom_type rng_type.
37
38definition tbl_is_empty ≝
39  λdom_type: Type[0].
40  λrng_type: Type[0].
41  λthe_table: table dom_type rng_type.
42  match the_table with
43  [ empty ⇒ true
44  | _     ⇒ false
45  ].
46
47definition tbl_is_empty_p ≝
48  λdom_type: Type[0].
49  λrng_type: Type[0].
50  λthe_table: table dom_type rng_type.
51  match the_table with
52  [ empty ⇒ True
53  | _     ⇒ False
54  ].
55
56let rec tbl_to_list
57  (dom_type: Type[0]) (rng_type: Type[0]) (the_table: table dom_type rng_type)
58    on the_table: list (dom_type × rng_type) ≝
59  match the_table with
60  [ empty ⇒ [ ]
61  | node sz key val l r ⇒ 〈key, val〉 :: tbl_to_list … l @ tbl_to_list … r
62  ].
63
64let rec tbl_min_binding
65  (key_type: Type[0]) (rng_type: Type[0]) (the_table: table key_type rng_type)
66    (proof: ¬ (tbl_is_empty_p … the_table))
67      on the_table: key_type × rng_type ≝
68  match the_table return λx. ¬ (tbl_is_empty_p … x) → key_type × rng_type with
69  [ empty               ⇒ λabsurd. ?
70  | node sz key val l r ⇒ λproof.
71    match l return λx. x = l → key_type × rng_type with
72    [ empty ⇒ λproof. 〈key, val〉
73    | _     ⇒ λproof. tbl_min_binding key_type rng_type l ?
74    ] (refl … l)
75  ] proof.
76  [1: normalize in absurd;
77      elim absurd;
78      #ABSURD
79      @⊥ @ABSURD @I
80  |2: <proof
81      normalize
82      /2/
83  ]
84qed.
85
86definition tbl_create ≝
87  λkey_type: Type[0].
88  λrng_type: Type[0].
89  λleft    : table key_type rng_type.
90  λkey     : key_type.
91  λval     : rng_type.
92  λright   : table key_type rng_type.
93  let hl ≝ tbl_height … left in
94  let hr ≝ tbl_height … right in
95  let height ≝ if gtb hl hr then hl + 1 else hr + 1 in
96    node key_type rng_type height key val left right.
97     
98let rec tbl_balance
99  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
100    (left: table key_type rng_type) (key: key_type) (val: rng_type)
101      (right: table key_type rng_type) (left_proof: ¬ (tbl_is_empty_p … left))
102        (right_proof: ¬ (tbl_is_empty_p … right))
103          on left: table key_type rng_type ≝
104  match gtb (tbl_height … left) ((tbl_height … right) + 2) with
105  [ true  ⇒
106    match left return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
107    [ empty              ⇒ λabsurd. ?
108    | node _ lv ld ll lr ⇒ λnon_empty_proof.
109      if gtb (tbl_height … ll) (tbl_height … lr) then
110        tbl_create … ll lv ld (tbl_create … lr key val right)
111      else
112        match lr return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
113        [ empty ⇒ λabsurd. ?
114        | node _ lrv lrd lrl lrr ⇒ λ
115            tbl_create … (tbl_create … ll lv ld lrl) lrv lrd (tbl_create … lrr key val right)
116        ]
117    ] left_proof
118  | false ⇒ ?
119  ].
120  [1: normalize in absurd;
121      elim absurd
122      #ABSURD
123      @⊥ @ABSURD @I
124  |*: cases daemon
125  ]
126qed.
127 
128let rec tbl_remove_min_binding
129  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
130    (the_table: table key_type rng_type) (proof: ¬ (tbl_is_empty_p … the_table))
131      on the_table: table key_type rng_type ≝
132  match the_table return λx. ¬ (tbl_is_empty_p … x) → table key_type rng_type with
133  [ empty               ⇒ λabsurd. ?
134  | node sz key val l r ⇒ λproof.
135    match l return λx. x = l → table key_type rng_type with
136    [ empty ⇒ λproof. r
137    | _     ⇒ λproof. tbl_balance … ord (tbl_remove_min_binding … ord l ?) key val r
138    ] (refl … l)
139  ] proof.
140  [1: normalize in absurd;
141      elim absurd;
142      #ABSURD
143      @⊥ @ABSURD @I
144  |2: <proof
145      normalize
146      @nmk //
147  ]
148qed.
149   
150let rec tbl_insert
151  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
152    (key: key_type) (val: rng_type) (the_table: table key_type rng_type)
153      on the_table: table key_type rng_type ≝
154  match the_table with
155  [ empty                 ⇒ node … 1 key val (empty …) (empty …)
156  | node sz key' val' l r ⇒
157    match ord key key' with
158    [ order_lt ⇒ tbl_balance … ord (tbl_insert … ord key val l) key' val' r
159    | order_eq ⇒ node … sz key val l r
160    | order_gt ⇒ tbl_balance … ord l key' val' (tbl_insert … ord key val r)
161    ]
162  ].
163 
164let rec tbl_merge
165  (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order)
166    (left: table dom_type rng_type) (right: table dom_type rng_type)
167      on left: table dom_type rng_type ≝
168  match left with
169  [ empty ⇒ right
170  | _     ⇒
171    match right return λx. x = right → table dom_type rng_type with
172    [ empty               ⇒ λid_proof. left
173    | node sz key val l r ⇒ λid_proof.
174      let 〈x, d〉 ≝ tbl_min_binding dom_type rng_type right ? in
175        tbl_balance … ord left x d (tbl_remove_min_binding … ord right ?)
176    ] (refl … right)
177  ].
178  <id_proof
179  normalize /2/
180qed.
181
182let rec tbl_remove
183  (key_type: Type[0]) (rng_type: Type[0]) (ord: key_type → key_type → order)
184    (key: key_type) (the_table: table key_type rng_type)
185      on the_table: table key_type rng_type ≝
186  match the_table with
187  [ empty                 ⇒ empty …
188  | node sz key' val' l r ⇒
189    match ord key key' with
190    [ order_lt ⇒ tbl_balance … ord (tbl_remove … ord key l) key' val' r
191    | order_eq ⇒ tbl_merge … ord l r
192    | order_gt ⇒ tbl_balance … ord l key' val' (tbl_remove … ord key r)
193    ]
194  ].
195 
196let rec tbl_find
197  (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order)
198    (to_find: dom_type) (the_table: table dom_type rng_type)
199      on the_table: option rng_type ≝
200  match the_table with
201  [ empty               ⇒ None …
202  | node sz key val l r ⇒
203    match ord to_find key with
204    [ order_lt ⇒ tbl_find … ord to_find l
205    | order_eq ⇒ Some … val
206    | order_gt ⇒ tbl_find … ord to_find r
207    ]
208  ].
209
210let rec tbl_update
211  (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order)
212    (to_find: dom_type) (update: rng_type → rng_type)
213      (the_table: table dom_type rng_type)
214        on the_table: table dom_type rng_type ≝
215  match the_table with
216  [ empty               ⇒ empty …
217  | node sz key val l r ⇒
218    match ord to_find key with
219    [ order_lt ⇒ tbl_update … ord to_find update l
220    | order_eq ⇒ node … sz key (update val) l r
221    | order_gt ⇒ tbl_update … ord to_find update r
222    ]
223  ].
224
225let rec tbl_forall
226  (dom_type: Type[0]) (rng_type: Type[0]) (f: rng_type → bool)
227    (the_table: table dom_type rng_type)
228      on the_table: bool ≝
229  match the_table with
230  [ empty               ⇒ true
231  | node sz key val l r ⇒ f val ∧ tbl_forall … f l ∧ tbl_forall … f r
232  ].
233 
234let rec tbl_exists
235  (dom_type: Type[0]) (rng_type: Type[0]) (f: rng_type → bool)
236    (the_table: table dom_type rng_type)
237      on the_table: bool ≝
238  match the_table with
239  [ empty               ⇒ false
240  | node sz key val l r ⇒ f val ∨ tbl_exists … f l ∨ tbl_exists … f r
241  ].
242     
243axiom tbl_equal:
244  ∀key_type, rng_type.
245    (key_type → key_type → order) → (rng_type → rng_type → order) →
246      table key_type rng_type → table key_type rng_type → bool.
247
248let rec tbl_mapi
249  (dom_type: Type[0]) (rng_type: Type[0]) (a: Type[0]) (f: dom_type → rng_type → a)
250    (the_table: table dom_type rng_type)
251      on the_table: table dom_type a ≝
252  match the_table with
253  [ empty               ⇒ empty …
254  | node sz key val l r ⇒ node  … sz key (f key val) (tbl_mapi … f l) (tbl_mapi … f r)
255  ].
256
257let rec tbl_map
258  (dom_type: Type[0]) (rng_type: Type[0]) (a: Type[0]) (f: rng_type → a)
259    (the_table: table dom_type rng_type)
260      on the_table: table dom_type a ≝
261  match the_table with
262  [ empty               ⇒ empty …
263  | node sz key val l r ⇒ node  … sz key (f val) (tbl_map … f l) (tbl_map … f r)
264  ].
265
266let rec tbl_fold
267  (dom_type: Type[0]) (a: Type[0]) (b: Type[0]) (f: dom_type → a → b → b)
268    (the_table: table dom_type a) (seed: b)
269      on the_table: b ≝
270  match the_table with
271  [ empty               ⇒ seed
272  | node sz key val l r ⇒ tbl_fold … f r (f key val (tbl_fold … f l seed))
273  ].
274
275definition tbl_singleton ≝
276  λkey_type : Type[0].
277  λrng_type : Type[0].
278  λkey      : key_type.
279  λrng      : rng_type.
280    node key_type rng_type 1 key rng (empty …) (empty …).
281
282definition tbl_from_list ≝
283  λkey_type : Type[0].
284  λrng_type : Type[0].
285  λord      : key_type → key_type → order.
286  λthe_list : list (key_type × rng_type).
287    foldr … (λkey_rng.
288      let 〈key, rng〉 ≝ key_rng in
289        tbl_insert … ord key rng) (tbl_empty …) the_list.
290
291definition tbl_filter ≝
292  λdom_type : Type[0].
293  λrng_type : Type[0].
294  λord      : dom_type → dom_type → order.
295  λf        : rng_type → bool.
296  λthe_table: table dom_type rng_type.
297  let as_list  ≝ tbl_to_list … the_table in
298  let filtered ≝ filter … (λx. f (\snd x)) as_list in
299    tbl_from_list … ord filtered.
300
Note: See TracBrowser for help on using the repository browser.