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

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

added adts for sets, tables and priority sets in order to make life easier when working on the interference graph code

File size: 2.2 KB
Line 
1include "basics/types.ma".
2include "basics/bool.ma".
3include "basics/list.ma".
4
5include "arithmetics/nat.ma".
6
7include "utilities/adt/ordering.ma".
8include "utilities/adt/equal.ma".
9
10include "ASM/Util.ma".
11
12record table_adt
13  (key_type: Type[0]) (rng_type: Type[0]) (order: ordered key_type): Type[1] ≝
14{
15  table  : Type[0] → Type[0] → Type[0];
16 
17  tbl_empty  : table key_type rng_type;
18  tbl_size   : table key_type rng_type → nat;
19 
20  tbl_to_list: table key_type rng_type → list (key_type × rng_type);
21 
22  tbl_insert : key_type → rng_type → table key_type rng_type → table key_type rng_type;
23  tbl_remove : key_type → table key_type rng_type → table key_type rng_type;
24 
25  tbl_find   : key_type → table key_type rng_type → option rng_type;
26 
27  tbl_forall : (rng_type → bool) → table key_type rng_type → bool;
28  tbl_exists : (rng_type → bool) → table key_type rng_type → bool;
29  tbl_filter : (rng_type → bool) → table key_type rng_type → table key_type rng_type;
30 
31  tbl_equal  : equal rng_type → table key_type rng_type
32             → table key_type rng_type → bool;
33 
34  tbl_mapi   : ∀a: Type[0]. (key_type → rng_type → a)
35             → table key_type rng_type → table key_type a;
36  tbl_map    : ∀a: Type[0]. (rng_type → a) → table key_type rng_type
37             → table key_type a;
38  tbl_fold   : ∀a: Type[0]. (key_type → a → a) → table key_type rng_type → a → a
39}.
40
41definition tbl_is_empty ≝
42  λkey_type : Type[0].
43  λrng_type : Type[0].
44  λorder    : ordered key_type.
45  λtable_adt: table_adt key_type rng_type order.
46  λtable    : table … table_adt key_type rng_type.
47    tbl_size … table = 0.
48
49definition tbl_singleton ≝
50  λkey_type : Type[0].
51  λrng_type : Type[0].
52  λorder    : ordered key_type.
53  λtable_adt: table_adt key_type rng_type order.
54  λkey      : key_type.
55  λrng      : rng_type.
56    tbl_insert … table_adt key rng (tbl_empty …).
57
58definition tbl_from_list ≝
59  λkey_type : Type[0].
60  λrng_type : Type[0].
61  λorder    : ordered key_type.
62  λtable_adt: table_adt key_type rng_type order.
63  λthe_list : list (key_type × rng_type).
64    foldr … (λkey_rng.
65      let 〈key, rng〉 ≝ key_rng in
66        tbl_insert … table_adt key rng) (tbl_empty …) the_list.
67
Note: See TracBrowser for help on using the repository browser.