Safe Haskell	None
Language	Haskell2010

Agda.Utils.HashTable

Description

Hash tables.

Synopsis

data HashTable (ks :: Type -> Type -> Type) k (vs :: Type -> Type -> Type) v
type HashTableLU k v = HashTable MVector k MVector v
type HashTableLL k v = HashTable MVector k MVector v
empty :: forall (ks :: Type -> Type -> Type) k (vs :: Type -> Type -> Type) v. (MVector ks k, MVector vs v) => IO (HashTable ks k vs v)
insert :: forall k (vs :: Type -> Type -> Type) v (ks :: Type -> Type -> Type). (Hashable k, MVector vs v, MVector ks k) => HashTable ks k vs v -> k -> v -> IO ()
lookup :: forall k (ks :: Type -> Type -> Type) (vs :: Type -> Type -> Type) v. (Hashable k, MVector ks k, MVector vs v) => HashTable ks k vs v -> k -> IO (Maybe v)
toList :: forall k (ks :: Type -> Type -> Type) (vs :: Type -> Type -> Type) v. (Hashable k, MVector ks k, MVector vs v) => HashTable ks k vs v -> IO [(k, v)]
forAssocs :: forall (ks :: Type -> Type -> Type) k (vs :: Type -> Type -> Type) v. (MVector ks k, MVector vs v) => HashTable ks k vs v -> (k -> v -> IO ()) -> IO ()
size :: forall (ks :: Type -> Type -> Type) k (vs :: Type -> Type -> Type) v. MVector ks k => HashTable ks k vs v -> IO Int
insertingIfAbsent :: forall (ks :: Type -> Type -> Type) k (vs :: Type -> Type -> Type) v a. (Hashable k, MVector ks k, MVector vs v) => HashTable ks k vs v -> k -> (v -> IO a) -> IO v -> (v -> IO a) -> IO a

Documentation

data HashTable (ks :: Type -> Type -> Type) k (vs :: Type -> Type -> Type) v Source #

Hash tables. A very limited amount of (possibly outdated) testing indicates that, for the use in Agda's serialiser/deserialiser, Data.HashTable.IO.CuckooHashTable is somewhat slower than Data.HashTable.IO.BasicHashTable, and that Data.HashTable.IO.LinearHashTable and the hashtables from Data.Hashtable are much slower. However, other (also possibly outdated) testing suggests that Data.HashTable.IO.CuckooHashTable is quite a bit faster than Data.HashTable.IO.BasicHashTable for 64-bit Windows. Some more recent, also limited, testing suggests that the following hash table implementation from Data.Vector.Hashtables is quite a bit faster than Data.HashTable.IO.BasicHashTable (see issue #5966).

type HashTableLU k v = HashTable MVector k MVector v Source #

Hashtable with lifted keys and unboxed values.

type HashTableLL k v = HashTable MVector k MVector v Source #

Hashtable with lifted keys and lifted values.

empty :: forall (ks :: Type -> Type -> Type) k (vs :: Type -> Type -> Type) v. (MVector ks k, MVector vs v) => IO (HashTable ks k vs v) Source #

An empty hash table.

insert :: forall k (vs :: Type -> Type -> Type) v (ks :: Type -> Type -> Type). (Hashable k, MVector vs v, MVector ks k) => HashTable ks k vs v -> k -> v -> IO () Source #

Inserts the key and the corresponding value into the hash table.

lookup :: forall k (ks :: Type -> Type -> Type) (vs :: Type -> Type -> Type) v. (Hashable k, MVector ks k, MVector vs v) => HashTable ks k vs v -> k -> IO (Maybe v) Source #

Tries to find a value corresponding to the key in the hash table.

toList :: forall k (ks :: Type -> Type -> Type) (vs :: Type -> Type -> Type) v. (Hashable k, MVector ks k, MVector vs v) => HashTable ks k vs v -> IO [(k, v)] Source #

Converts the hash table to a list.

The order of the elements in the list is unspecified.

forAssocs :: forall (ks :: Type -> Type -> Type) k (vs :: Type -> Type -> Type) v. (MVector ks k, MVector vs v) => HashTable ks k vs v -> (k -> v -> IO ()) -> IO () Source #

Iterate over key-value pairs in IO.

size :: forall (ks :: Type -> Type -> Type) k (vs :: Type -> Type -> Type) v. MVector ks k => HashTable ks k vs v -> IO Int Source #

insertingIfAbsent :: forall (ks :: Type -> Type -> Type) k (vs :: Type -> Type -> Type) v a. (Hashable k, MVector ks k, MVector vs v) => HashTable ks k vs v -> k -> (v -> IO a) -> IO v -> (v -> IO a) -> IO a Source #

Look up a key in the table. If it's already there, proceed with the first (v -> m a) argument. Otherwise run the (m v) argument, insert the result value in the table and pass it to the second @(v -> m a) argument.