Agda-2.8.0.1: src/full/Agda/Utils/HashTable.hs
{-# OPTIONS_GHC -Wunused-imports #-}
------------------------------------------------------------------------
-- | Hash tables.
------------------------------------------------------------------------
module Agda.Utils.HashTable
( HashTable
, empty
, insert
, lookup
, toList
, keySet
) where
import Prelude hiding (lookup)
import Data.Hashable
import qualified Data.Vector.Hashtables as H
import qualified Data.Vector.Mutable as VM
import qualified Data.Vector as V
import Data.Set (Set)
import qualified Data.Set as Set
-- | 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).
newtype HashTable k v =
HashTable (H.Dictionary (H.PrimState IO) VM.MVector k VM.MVector v)
-- | An empty hash table.
empty :: IO (HashTable k v)
empty = HashTable <$> H.initialize 0
-- | Inserts the key and the corresponding value into the hash table.
insert :: (Eq k, Hashable k) => HashTable k v -> k -> v -> IO ()
insert (HashTable h) = H.insert h
{-# INLINABLE insert #-}
-- | Tries to find a value corresponding to the key in the hash table.
lookup :: (Eq k, Hashable k) => HashTable k v -> k -> IO (Maybe v)
lookup (HashTable h) = H.lookup h
{-# INLINABLE lookup #-}
-- | Converts the hash table to a list.
--
-- The order of the elements in the list is unspecified.
toList :: (Eq k, Hashable k) => HashTable k v -> IO [(k, v)]
toList (HashTable h) = H.toList h
{-# INLINABLE toList #-}
keySet :: forall k v. Ord k => HashTable k v -> IO (Set k)
keySet (HashTable h) = do
(ks :: V.Vector k) <- H.keys h
pure $! V.foldl' (flip Set.insert) mempty ks
{-# INLINABLE keySet #-}