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

Last change on this file since 1274 was 1274, checked in by mulligan, 8 years ago

starting removing axioms from adts and giving them proper implementations

File size: 4.8 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_empty ≝ empty.
17
18definition tbl_size ≝
19  λdom_type : Type[0].
20  λrng_type : Type[0].
21  λthe_table: table dom_type rng_type.
22  match the_table with
23  [ empty ⇒ 0
24  | node sz key val l r ⇒ sz
25  ].
26
27let rec tbl_to_list
28  (dom_type: Type[0]) (rng_type: Type[0]) (the_table: table dom_type rng_type)
29    on the_table: list (dom_type × rng_type) ≝
30  match the_table with
31  [ empty ⇒ [ ]
32  | node sz key val l r ⇒ 〈key, val〉 :: tbl_to_list … l @ tbl_to_list … r
33  ].
34 
35axiom tbl_insert : ∀key_type, rng_type. key_type → rng_type → table key_type rng_type → table key_type rng_type.
36
37axiom tbl_merge:
38  ∀key_type, rng_type.
39    (key_type → key_type → order) → table key_type rng_type → table key_type rng_type → table key_type rng_type.
40
41axiom tbl_remove : ∀key_type, rng_type. key_type → table key_type rng_type → table key_type rng_type.
42 
43let rec tbl_find
44  (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order)
45    (to_find: dom_type) (the_table: table dom_type rng_type)
46      on the_table: option rng_type ≝
47  match the_table with
48  [ empty               ⇒ None …
49  | node sz key val l r ⇒
50    match ord to_find key with
51    [ order_lt ⇒ tbl_find … ord to_find l
52    | order_eq ⇒ Some … val
53    | order_gt ⇒ tbl_find … ord to_find r
54    ]
55  ].
56
57let rec tbl_update
58  (dom_type: Type[0]) (rng_type: Type[0]) (ord: dom_type → dom_type → order)
59    (to_find: dom_type) (update: rng_type → rng_type)
60      (the_table: table dom_type rng_type)
61        on the_table: table dom_type rng_type ≝
62  match the_table with
63  [ empty               ⇒ empty …
64  | node sz key val l r ⇒
65    match ord to_find key with
66    [ order_lt ⇒ tbl_update … ord to_find update l
67    | order_eq ⇒ node … sz key (update val) l r
68    | order_gt ⇒ tbl_update … ord to_find update r
69    ]
70  ].
71
72let rec tbl_forall
73  (dom_type: Type[0]) (rng_type: Type[0]) (f: rng_type → bool)
74    (the_table: table dom_type rng_type)
75      on the_table: bool ≝
76  match the_table with
77  [ empty               ⇒ true
78  | node sz key val l r ⇒ f val ∧ tbl_forall … f l ∧ tbl_forall … f r
79  ].
80 
81let rec tbl_exists
82  (dom_type: Type[0]) (rng_type: Type[0]) (f: rng_type → bool)
83    (the_table: table dom_type rng_type)
84      on the_table: bool ≝
85  match the_table with
86  [ empty               ⇒ false
87  | node sz key val l r ⇒ f val ∨ tbl_exists … f l ∨ tbl_exists … f r
88  ].
89 
90axiom tbl_equal  : ∀key_type, rng_type. table key_type rng_type
91                    → table key_type rng_type → bool.
92
93let rec tbl_mapi
94  (dom_type: Type[0]) (rng_type: Type[0]) (a: Type[0]) (f: dom_type → rng_type → a)
95    (the_table: table dom_type rng_type)
96      on the_table: table dom_type a ≝
97  match the_table with
98  [ empty               ⇒ empty …
99  | node sz key val l r ⇒ node  … sz key (f key val) (tbl_mapi … f l) (tbl_mapi … f r)
100  ].
101
102let rec tbl_map
103  (dom_type: Type[0]) (rng_type: Type[0]) (a: Type[0]) (f: rng_type → a)
104    (the_table: table dom_type rng_type)
105      on the_table: table dom_type a ≝
106  match the_table with
107  [ empty               ⇒ empty …
108  | node sz key val l r ⇒ node  … sz key (f val) (tbl_map … f l) (tbl_map … f r)
109  ].
110
111let rec tbl_fold
112  (dom_type: Type[0]) (a: Type[0]) (b: Type[0]) (f: dom_type → a → b → b)
113    (the_table: table dom_type a) (seed: b)
114      on the_table: b ≝
115  match the_table with
116  [ empty               ⇒ seed
117  | node sz key val l r ⇒ tbl_fold … f r (f key val (tbl_fold … f l seed))
118  ].
119
120definition tbl_is_empty ≝
121  λkey_type : Type[0].
122  λrng_type : Type[0].
123  λtable    : table key_type rng_type.
124    tbl_size … table = 0.
125
126definition tbl_singleton ≝
127  λkey_type : Type[0].
128  λrng_type : Type[0].
129  λkey      : key_type.
130  λrng      : rng_type.
131    tbl_insert … key rng (tbl_empty …).
132
133definition tbl_from_list ≝
134  λkey_type : Type[0].
135  λrng_type : Type[0].
136  λthe_list : list (key_type × rng_type).
137    foldr … (λkey_rng.
138      let 〈key, rng〉 ≝ key_rng in
139        tbl_insert … key rng) (tbl_empty …) the_list.
140
141definition tbl_filter ≝
142  λdom_type : Type[0].
143  λrng_type : Type[0].
144  λf        : rng_type → bool.
145  λthe_table: table dom_type rng_type.
146  let as_list  ≝ tbl_to_list … the_table in
147  let filtered ≝ filter … (λx. f (\snd x)) as_list in
148    tbl_from_list … filtered.
149
Note: See TracBrowser for help on using the repository browser.