1 (* This module is used by the [hashtable] module, but could also be useful 2 per se. It offers mutable lists of key-value pairs. *) 3 4 (* -------------------------------------------------------------------------- *) 5 6 (* A bucket is a mutable list of entries. Each entry holds a key and a value. *) 7 8 mutable data bucket k a = 9 | BNil 10 | BCons { key: k; value: a; tail: bucket k a } 11 12 (* -------------------------------------------------------------------------- *) 13 14 (* Search. *) 15 16 val mem : [k, a] ( 17 equal: (k, k) -> bool, 18 x: k, 19 b: bucket k a 20 ) -> bool 21 22 val assoc: [k, a, p : perm] duplicable a => ( 23 equal: (k, k | p) -> bool, 24 x: k, 25 b: bucket k a 26 | p 27 ) -> option a 28 29 val assoc_all: [k, a, p : perm] duplicable a => ( 30 equal: (k, k | p) -> bool, 31 x: k, 32 b: bucket k a 33 | p 34 ) -> list::list a 35 36 (* -------------------------------------------------------------------------- *) 37 38 (* Removal and update. *) 39 40 (* [remove (b, ok)] looks for the first cell whose key satisfies the predicate 41 [ok] and (if it finds one) removes it. It returns a pair of the new list 42 head and the value that was found, if one was found. *) 43 44 val remove : [k, a, p : perm] ( 45 consumes b: bucket k a, 46 ok: (k | p) -> bool 47 | p 48 ) -> (bucket k a, option a) 49 50 (* [update (equal, b, x, f)] looks for an entry whose key is [equal] to [x] 51 in the bucket [b]. It calls the user-supplied function [f] exactly once, 52 and passes it either the value [v] that is associated with the key [x], 53 or nothing, if the key [x] does not appear in the bucket. The function 54 [f] returns either a new value, or nothing. In the former case, the new 55 value replaces the value [v]. In the latter case, the key [x] is removed 56 (if it was there at all). An updated bucket is returned. *) 57 58 val update : [k, a, pre : perm, post : perm] ( 59 equal: (k, k) -> bool, 60 consumes b: bucket k a, 61 consumes x: k, 62 f: (consumes (option a | pre)) -> (option a | post) 63 | consumes pre 64 ) -> (bucket k a | post) 65 66 (* -------------------------------------------------------------------------- *) 67 68 (* Iteration. *) 69 70 (* Non-destructive iteration over the elements of a bucket. *) 71 72 val fold : [k, a, b] ( 73 bucket k a, 74 consumes b, 75 f: (k, a, consumes b) -> b 76 ) -> b 77 78 (* Destructive iteration over the cells of a bucket. Each cell is presented in 79 turn to the function [f]. Note that the cells that are presented to [f] are 80 detached, i.e., their [tail] field is garbage. *) 81 82 val iter_bucket_down : [k, a, p : perm] ( 83 consumes b: bucket k a, 84 f: (consumes b: BCons { key: k; value: a; tail: unknown } | p) -> () 85 | p 86 ) -> () 87 88 (* -------------------------------------------------------------------------- *) 89 90 (* Length. *) 91 92 val length: [k, a] bucket k a -> int 93