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

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

changes

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