
  0 | module Data.HashMap
  1 | 
  2 | import Data.HashMap.Internal
  3 | import public Data.Hashable
  4 | 
  5 | export
  6 | data HashMap : (key : Type) -> (val : Type) -> Type where
  7 |     Empty : Hashable key => Eq key => HashMap key val
  8 |     Trie : Hashable key => Eq key => HAMT key (const val) -> HashMap key val
  9 | 
 10 | %name HashMap hm
 11 | 
 12 | export
 13 | empty : Hashable key => Eq key => HashMap key val
 14 | empty = Empty
 15 | 
 16 | export
 17 | lookup : key -> HashMap key val -> Maybe val
 18 | lookup key Empty = Nothing
 19 | lookup key (Trie hamt) = map snd $ lookup (==) key hamt
 20 | 
 21 | export
 22 | insert : key -> val -> HashMap key val -> HashMap key val
 23 | insert key val Empty = Trie $ singleton key val
 24 | insert key val (Trie hamt) = Trie $ insert (==) key val hamt
 25 | 
 26 | export
 27 | delete : key -> HashMap key val -> HashMap key val
 28 | delete key Empty = Empty
 29 | delete key (Trie hamt) = case delete (==) key hamt of
 30 |     Just hamt' => Trie hamt'
 31 |     Nothing => Empty
 32 | 
 33 | export
 34 | foldWithKey : (f : k -> v -> acc -> acc) -> acc -> HashMap k v -> acc
 35 | foldWithKey f z Empty = z
 36 | foldWithKey f z (Trie hamt) = foldWithKey f z hamt
 37 | 
 38 | export
 39 | toList : HashMap k v -> List (k, v)
 40 | toList hm = foldWithKey (\key, val, acc => (key, val) :: acc) [] hm
 41 | 
 42 | export
 43 | keys : HashMap k v -> List k
 44 | keys hm = foldWithKey (\key, val, acc => key :: acc) [] hm
 45 | 
 46 | export
 47 | fromList : Hashable k => Eq k => List (k, v) -> HashMap k v
 48 | fromList lst = foldr (\(k, v) => insert k v) empty lst
 49 | 
 50 | export
 51 | Functor (HashMap key) where
 52 |     map f Empty = Empty
 53 |     map f (Trie hamt) = Trie $ trieMap f hamt
 54 | 
 55 | export
 56 | Show key => Show val => Show (HashMap key val) where
 57 |     show hm = "fromList \{show $ HashMap.toList hm}"
 58 |