------------------------------------------------------------------------
-- |
-- Module           : Data.Parameterized.HashTable
-- Description      : a hash table for parameterized keys and values
-- Copyright        : (c) Galois, Inc 2014-2019
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
--
-- This module provides a 'ST'-based hashtable for parameterized keys and values.
--
-- NOTE: This API makes use of 'unsafeCoerce' to implement the parameterized
-- hashtable abstraction.  This should be type-safe provided that the
-- 'TestEquality' instance on the key type is implemented soundly.
------------------------------------------------------------------------
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Trustworthy #-}
module Data.Parameterized.HashTable
  ( HashTable
  , new
  , newSized
  , clone
  , lookup
  , insert
  , member
  , delete
  , clear
  , Data.Parameterized.Classes.HashableF(..)
  , Control.Monad.ST.RealWorld
  ) where

import Control.Applicative
import Control.Monad.ST
import qualified Data.HashTable.ST.Basic as H
import Data.Kind
import GHC.Exts (Any)
import Unsafe.Coerce

import Prelude hiding (lookup)

import Data.Parameterized.Classes
import Data.Parameterized.Some

-- | A hash table mapping nonces to values.
newtype HashTable s (key :: k -> Type) (val :: k -> Type)
      = HashTable (H.HashTable s (Some key) Any)

-- | Create a new empty table.
new :: ST s (HashTable s key val)
new :: forall {k} s (key :: k -> *) (val :: k -> *).
ST s (HashTable s key val)
new = forall k s (key :: k -> *) (val :: k -> *).
HashTable s (Some key) Any -> HashTable s key val
HashTable forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s k v. ST s (HashTable s k v)
H.new

-- | Create a new empty table to hold 'n' elements.
newSized :: Int -> ST s (HashTable s k v)
newSized :: forall {k} s (k :: k -> *) (v :: k -> *).
Int -> ST s (HashTable s k v)
newSized Int
n = forall k s (key :: k -> *) (val :: k -> *).
HashTable s (Some key) Any -> HashTable s key val
HashTable forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall s k v. Int -> ST s (HashTable s k v)
H.newSized Int
n

-- | Create a hash table that is a copy of the current one.
clone :: (HashableF key, TestEquality key)
      => HashTable s key val
      -> ST s (HashTable s key val)
clone :: forall {k} (key :: k -> *) s (val :: k -> *).
(HashableF key, TestEquality key) =>
HashTable s key val -> ST s (HashTable s key val)
clone (HashTable HashTable s (Some key) Any
tbl) = do
  -- Create a new table
  HashTable s (Some key) Any
r <- forall s k v. ST s (HashTable s k v)
H.new
  -- Insert existing elements in
  forall k v s b. ((k, v) -> ST s b) -> HashTable s k v -> ST s ()
H.mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> v -> ST s ()
H.insert HashTable s (Some key) Any
r)) HashTable s (Some key) Any
tbl
  -- Return table
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall k s (key :: k -> *) (val :: k -> *).
HashTable s (Some key) Any -> HashTable s key val
HashTable HashTable s (Some key) Any
r

-- | Lookup value of key in table.
lookup :: (HashableF key, TestEquality key)
       => HashTable s key val
       -> key tp
       -> ST s (Maybe (val tp))
lookup :: forall {k} (key :: k -> *) s (val :: k -> *) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> ST s (Maybe (val tp))
lookup (HashTable HashTable s (Some key) Any
h) key tp
k = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. a -> b
unsafeCoerce forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (Some key) Any
h (forall k (f :: k -> *) (x :: k). f x -> Some f
Some key tp
k)
{-# INLINE lookup #-}

-- | Insert new key and value mapping into table.
insert :: (HashableF key, TestEquality key)
       => HashTable s (key :: k -> Type) (val :: k -> Type)
       -> key tp
       -> val tp
       -> ST s ()
insert :: forall k (key :: k -> *) s (val :: k -> *) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> val tp -> ST s ()
insert (HashTable HashTable s (Some key) Any
h) key tp
k val tp
v = forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> v -> ST s ()
H.insert HashTable s (Some key) Any
h (forall k (f :: k -> *) (x :: k). f x -> Some f
Some key tp
k) (forall a b. a -> b
unsafeCoerce val tp
v)

-- | Return true if the key is in the hash table.
member :: (HashableF key, TestEquality key)
       => HashTable s (key :: k -> Type) (val :: k -> Type)
       -> key (tp :: k)
       -> ST s Bool
member :: forall k (key :: k -> *) s (val :: k -> *) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> ST s Bool
member (HashTable HashTable s (Some key) Any
h) key tp
k = forall a. Maybe a -> Bool
isJust forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k s v.
(Eq k, Hashable k) =>
HashTable s k v -> k -> ST s (Maybe v)
H.lookup HashTable s (Some key) Any
h (forall k (f :: k -> *) (x :: k). f x -> Some f
Some key tp
k)

-- | Delete an element from the hash table.
delete :: (HashableF key, TestEquality key)
       => HashTable s (key :: k -> Type) (val :: k -> Type)
       -> key (tp :: k)
       -> ST s ()
delete :: forall k (key :: k -> *) s (val :: k -> *) (tp :: k).
(HashableF key, TestEquality key) =>
HashTable s key val -> key tp -> ST s ()
delete (HashTable HashTable s (Some key) Any
h) key tp
k = forall k s v. (Hashable k, Eq k) => HashTable s k v -> k -> ST s ()
H.delete HashTable s (Some key) Any
h (forall k (f :: k -> *) (x :: k). f x -> Some f
Some key tp
k)

clear :: (HashableF key, TestEquality key)
      => HashTable s (key :: k -> Type) (val :: k -> Type) -> ST s ()
clear :: forall k (key :: k -> *) s (val :: k -> *).
(HashableF key, TestEquality key) =>
HashTable s key val -> ST s ()
clear (HashTable HashTable s (Some key) Any
h) = forall k v s b. ((k, v) -> ST s b) -> HashTable s k v -> ST s ()
H.mapM_ (\(Some key
k,Any
_) -> forall k s v. (Hashable k, Eq k) => HashTable s k v -> k -> ST s ()
H.delete HashTable s (Some key) Any
h Some key
k) HashTable s (Some key) Any
h