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

Last change on this file since 1285 was 1285, checked in by mulligan, 8 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.