module Agda.Utils.Pointer
( Ptr, newPtr, derefPtr, setPtr
, updatePtr, updatePtrM
) where
import Control.Applicative
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.Typeable
data Ptr a = Ptr { ptrTag :: !Integer
, ptrRef :: !(IORef a) }
deriving (Typeable)
freshVar :: MVar Integer
freshVar = unsafePerformIO $ newMVar 0
fresh :: IO Integer
fresh = do
x <- takeMVar freshVar
putMVar freshVar $! x + 1
return x
newPtr :: a -> Ptr a
newPtr x = unsafePerformIO $ do
i <- fresh
Ptr i <$> newIORef x
derefPtr :: Ptr a -> a
derefPtr p = unsafePerformIO $ readIORef $ ptrRef p
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