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

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

getting rid of typeclass-like records in favour of file-level axioms. much too heavyweight to use effectively

File size: 2.4 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
12axiom table: Type[0] → Type[0] → Type[0].
13 
14axiom tbl_empty  : ∀key_type, rng_type. table key_type rng_type.
15axiom tbl_size   : ∀key_type, rng_type. table key_type rng_type → nat.
16 
17axiom tbl_to_list: ∀key_type, rng_type. table key_type rng_type → list (key_type × rng_type).
18 
19axiom tbl_insert : ∀key_type, rng_type. key_type → rng_type → table key_type rng_type → table key_type rng_type.
20axiom tbl_remove : ∀key_type, rng_type. key_type → table key_type rng_type → table key_type rng_type.
21 
22axiom tbl_find   : ∀key_type, rng_type. key_type → table key_type rng_type → option rng_type.
23axiom tbl_update : ∀key_type, rng_type. key_type → (rng_type → rng_type) → table key_type rng_type →
24                    table key_type rng_type.
25 
26axiom tbl_forall : ∀key_type, rng_type. (rng_type → bool) → table key_type rng_type → bool.
27axiom tbl_exists : ∀key_type, rng_type. (rng_type → bool) → table key_type rng_type → bool.
28axiom tbl_filter : ∀key_type, rng_type. (rng_type → bool) → table key_type rng_type → table key_type rng_type.
29 
30axiom tbl_equal  : ∀key_type, rng_type. table key_type rng_type
31                    → table key_type rng_type → bool.
32 
33axiom tbl_mapi   : ∀key_type, rng_type. ∀a: Type[0]. (key_type → rng_type → a)
34                   → table key_type rng_type → table key_type a.
35axiom tbl_map    : ∀key_type, rng_type. ∀a: Type[0]. (rng_type → a) → table key_type rng_type
36                   → table key_type a.
37axiom tbl_fold   : ∀key_type, rng_type. ∀a: Type[0]. (key_type → a → a) → table key_type rng_type → a → a.
38
39definition tbl_is_empty ≝
40  λkey_type : Type[0].
41  λrng_type : Type[0].
42  λtable    : table key_type rng_type.
43    tbl_size … table = 0.
44
45definition tbl_singleton ≝
46  λkey_type : Type[0].
47  λrng_type : Type[0].
48  λkey      : key_type.
49  λrng      : rng_type.
50    tbl_insert … key rng (tbl_empty …).
51
52definition tbl_from_list ≝
53  λkey_type : Type[0].
54  λrng_type : Type[0].
55  λthe_list : list (key_type × rng_type).
56    foldr … (λkey_rng.
57      let 〈key, rng〉 ≝ key_rng in
58        tbl_insert … key rng) (tbl_empty …) the_list.
59
Note: See TracBrowser for help on using the repository browser.