1 abstract table k +a
 2 fact exclusive (table k a)
 3 
 4 (* -------------------------------------------------------------------------- *)
 5 
 6 (* Creation. *)
 7 
 8 val create : [k, a] (
 9   capacity: int,
10   hash: k -> int,
11   equal: (k, k) -> bool
12 ) -> table k a
13 
14 (* -------------------------------------------------------------------------- *)
15 
16 (* Clearing. *)
17 
18 val clear : [k, a] table k a -> ()
19 val reset : [k, a] (table k a, capacity: int) -> ()
20 
21 (* -------------------------------------------------------------------------- *)
22 
23 (* Insertion. *)
24 
25 val add : [k, a] (consumes k, consumes a, table k a) -> ()
26 
27 (* -------------------------------------------------------------------------- *)
28 
29 (* Merging. *)
30 
31 (* [merge (t1, t2)] does not require the two tables to use the same notions
32    of equality of hashing. It is equivalent to successively inserting each
33    element of [t1] into [t2]. *)
34 
35 val merge: [k, a] (consumes table k a, table k a) -> ()
36 
37 (* -------------------------------------------------------------------------- *)
38 
39 (* Removal. *)
40 
41 val remove : [k, a] (x: k, t: table k a) -> option a
42 
43 (* -------------------------------------------------------------------------- *)
44 
45 (* Lookup. *)
46 
47 val mem : [k, a] (x: k, t: table k a) -> bool
48 
49 val find     : [k, a] duplicable a => (x: k, t: table k a) -> option a
50 val find_all : [k, a] duplicable a => (x: k, t: table k a) -> list::list a
51 
52 (* -------------------------------------------------------------------------- *)
53 
54 (* Update. *)
55 
56 (* [update (t, x, f)] looks for the key [x] in the table [t]. It calls the
57    user-supplied function [f] exactly once, and passes it either the value [v]
58    that is associated with the key [x], or nothing, if the key [x] does not
59    appear in the table. The function [f] returns either a new value, or
60    nothing. In the former case, the new value replaces the value [v]. In the
61    latter case, the key [x] is removed (if it was there at all). *)
62 
63 val update : [k, a, pre : perm, post : perm] (
64   t: table k a,
65   consumes x: k,
66   f: (consumes (option a | pre)) -> (option a | post)
67   | consumes pre
68 ) -> (| post)
69 
70 (* -------------------------------------------------------------------------- *)
71 
72 (* Iteration. *)
73 
74 val fold : [k, a, b] (
75   t: table k a,
76   consumes seed: b,
77   f: (k, a, consumes b) -> b
78 ) -> b
79 
80 val iter : [k, a, p : perm] (
81   t: table k a,
82   f: (k, a | p) -> ()
83   | p
84 ) -> ()
85 
86 (* -------------------------------------------------------------------------- *)
87 
88 (* Statistics. *)
89 
90 val cardinal : [k, a] (t: table k a) -> int
91 
92 data statistics = Statistics {
93   num_bindings: int;
94   num_buckets: int;
95   max_bucket_length: int;
96   bucket_histogram: array int
97 }
98 
99 val stats : [k, a] (t: table k a) -> statistics