{-# LANGUAGE CPP #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE StandaloneDeriving #-}
module Agda.Utils.Pointer
( Ptr, newPtr, derefPtr, setPtr
, updatePtr, updatePtrM
) where
import Control.DeepSeq
import Control.Concurrent.MVar
import Data.Foldable
import Data.Function
import Data.Hashable
import Data.IORef
import Data.Traversable
import System.IO.Unsafe
import Data.Data (Data (..))
import Data.Typeable (Typeable)
#include "undefined.h"
import Agda.Utils.Impossible
data Ptr a = Ptr { ptrTag :: !Integer
, ptrRef :: !(IORef a) }
deriving Data
instance Typeable a => Data (IORef a) where
gunfold _ _ _ = __IMPOSSIBLE__
toConstr = __IMPOSSIBLE__
dataTypeOf = __IMPOSSIBLE__
{-# NOINLINE freshVar #-}
freshVar :: MVar Integer
freshVar = unsafePerformIO $ newMVar 0
fresh :: IO Integer
fresh = do
x <- takeMVar freshVar
putMVar freshVar $! x + 1
return x
{-# NOINLINE newPtr #-}
newPtr :: a -> Ptr a
newPtr x = unsafePerformIO $ do
i <- fresh
Ptr i <$> newIORef x
derefPtr :: Ptr a -> a
derefPtr p = unsafePerformIO $ readIORef $ ptrRef p
{-# NOINLINE updatePtr #-}
updatePtr :: (a -> a) -> Ptr a -> Ptr a
updatePtr f p = unsafePerformIO $ p <$ modifyIORef (ptrRef p) f
setPtr :: a -> Ptr a -> Ptr a
setPtr !x = updatePtr (const x)
updatePtrM :: Functor f => (a -> f a) -> Ptr a -> f (Ptr a)
updatePtrM f p = flip setPtr p <$> f (derefPtr p)
instance Show a => Show (Ptr a) where
show p = "#" ++ show (ptrTag p) ++ "{" ++ show (derefPtr p) ++ "}"
instance Functor Ptr where
fmap f = newPtr . f . derefPtr
instance Foldable Ptr where
foldMap f = f . derefPtr
instance Traversable Ptr where
traverse f p = newPtr <$> f (derefPtr p)
instance Eq (Ptr a) where
(==) = (==) `on` ptrTag
instance Ord (Ptr a) where
compare = compare `on` ptrTag
instance Hashable (Ptr a) where
hashWithSalt salt = (hashWithSalt salt) . ptrTag
instance NFData (Ptr a) where rnf x = seq x ()