module Agda.Utils.Pointer
  ( Ptr, newPtr, derefPtr, setPtr
  , updatePtr, updatePtrM
  ) where

import Control.DeepSeq
import Control.Concurrent.MVar

import Data.Function
import Data.Hashable
import Data.IORef

import System.IO.Unsafe

import Data.Data (Data (..))
import Data.Typeable (Typeable)

import Agda.Utils.Impossible

data Ptr a = Ptr { forall a. Ptr a -> Integer
ptrTag :: !Integer
                 , forall a. Ptr a -> IORef a
ptrRef :: !(IORef a) }
  deriving Typeable (Ptr a)
Typeable (Ptr a)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Ptr a -> c (Ptr a))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (Ptr a))
-> (Ptr a -> Constr)
-> (Ptr a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Ptr a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ptr a)))
-> ((forall b. Data b => b -> b) -> Ptr a -> Ptr a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ptr a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ptr a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Ptr a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Ptr a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Ptr a -> m (Ptr a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ptr a -> m (Ptr a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Ptr a -> m (Ptr a))
-> Data (Ptr a)
Ptr a -> DataType
Ptr a -> Constr
(forall b. Data b => b -> b) -> Ptr a -> Ptr a
forall {a}. Data a => Typeable (Ptr a)
forall a. Data a => Ptr a -> DataType
forall a. Data a => Ptr a -> Constr
forall a. Data a => (forall b. Data b => b -> b) -> Ptr a -> Ptr a
forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Ptr a -> u
forall a u. Data a => (forall d. Data d => d -> u) -> Ptr a -> [u]
forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ptr a -> r
forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ptr a -> r
forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Ptr a -> m (Ptr a)
forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ptr a -> m (Ptr a)
forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ptr a)
forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ptr a -> c (Ptr a)
forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Ptr a))
forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ptr a))
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Ptr a -> u
forall u. (forall d. Data d => d -> u) -> Ptr a -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ptr a -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ptr a -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ptr a -> m (Ptr a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ptr a -> m (Ptr a)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ptr a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ptr a -> c (Ptr a)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Ptr a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ptr a))
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ptr a -> m (Ptr a)
$cgmapMo :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ptr a -> m (Ptr a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Ptr a -> m (Ptr a)
$cgmapMp :: forall a (m :: * -> *).
(Data a, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Ptr a -> m (Ptr a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Ptr a -> m (Ptr a)
$cgmapM :: forall a (m :: * -> *).
(Data a, Monad m) =>
(forall d. Data d => d -> m d) -> Ptr a -> m (Ptr a)
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Ptr a -> u
$cgmapQi :: forall a u.
Data a =>
Int -> (forall d. Data d => d -> u) -> Ptr a -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Ptr a -> [u]
$cgmapQ :: forall a u. Data a => (forall d. Data d => d -> u) -> Ptr a -> [u]
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ptr a -> r
$cgmapQr :: forall a r r'.
Data a =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Ptr a -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ptr a -> r
$cgmapQl :: forall a r r'.
Data a =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Ptr a -> r
gmapT :: (forall b. Data b => b -> b) -> Ptr a -> Ptr a
$cgmapT :: forall a. Data a => (forall b. Data b => b -> b) -> Ptr a -> Ptr a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ptr a))
$cdataCast2 :: forall a (t :: * -> * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Ptr a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Ptr a))
$cdataCast1 :: forall a (t :: * -> *) (c :: * -> *).
(Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Ptr a))
dataTypeOf :: Ptr a -> DataType
$cdataTypeOf :: forall a. Data a => Ptr a -> DataType
toConstr :: Ptr a -> Constr
$ctoConstr :: forall a. Data a => Ptr a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ptr a)
$cgunfold :: forall a (c :: * -> *).
Data a =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Ptr a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ptr a -> c (Ptr a)
$cgfoldl :: forall a (c :: * -> *).
Data a =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Ptr a -> c (Ptr a)
Data

-- cheating because you shouldn't be digging this far anyway
instance Typeable a => Data (IORef a) where
  gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (IORef a)
gunfold forall b r. Data b => c (b -> r) -> c r
_ forall r. r -> c r
_ Constr
_ = c (IORef a)
forall a. HasCallStack => a
__IMPOSSIBLE__
  toConstr :: IORef a -> Constr
toConstr      = IORef a -> Constr
forall a. HasCallStack => a
__IMPOSSIBLE__
  dataTypeOf :: IORef a -> DataType
dataTypeOf    = IORef a -> DataType
forall a. HasCallStack => a
__IMPOSSIBLE__

{-# NOINLINE freshVar #-}
freshVar :: MVar Integer
freshVar :: MVar Integer
freshVar = IO (MVar Integer) -> MVar Integer
forall a. IO a -> a
unsafePerformIO (IO (MVar Integer) -> MVar Integer)
-> IO (MVar Integer) -> MVar Integer
forall a b. (a -> b) -> a -> b
$ Integer -> IO (MVar Integer)
forall a. a -> IO (MVar a)
newMVar Integer
0

fresh :: IO Integer
fresh :: IO Integer
fresh = do
    Integer
x <- MVar Integer -> IO Integer
forall a. MVar a -> IO a
takeMVar MVar Integer
freshVar
    MVar Integer -> Integer -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar Integer
freshVar (Integer -> IO ()) -> Integer -> IO ()
forall a b. (a -> b) -> a -> b
$! Integer
x Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
    Integer -> IO Integer
forall (m :: * -> *) a. Monad m => a -> m a
return Integer
x

{-# NOINLINE newPtr #-}
newPtr :: a -> Ptr a
newPtr :: forall a. a -> Ptr a
newPtr a
x = IO (Ptr a) -> Ptr a
forall a. IO a -> a
unsafePerformIO (IO (Ptr a) -> Ptr a) -> IO (Ptr a) -> Ptr a
forall a b. (a -> b) -> a -> b
$ do
  Integer
i <- IO Integer
fresh
  Integer -> IORef a -> Ptr a
forall a. Integer -> IORef a -> Ptr a
Ptr Integer
i (IORef a -> Ptr a) -> IO (IORef a) -> IO (Ptr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> IO (IORef a)
forall a. a -> IO (IORef a)
newIORef a
x

derefPtr :: Ptr a -> a
derefPtr :: forall a. Ptr a -> a
derefPtr Ptr a
p = IO a -> a
forall a. IO a -> a
unsafePerformIO (IO a -> a) -> IO a -> a
forall a b. (a -> b) -> a -> b
$ IORef a -> IO a
forall a. IORef a -> IO a
readIORef (IORef a -> IO a) -> IORef a -> IO a
forall a b. (a -> b) -> a -> b
$ Ptr a -> IORef a
forall a. Ptr a -> IORef a
ptrRef Ptr a
p

{-# NOINLINE updatePtr #-}
updatePtr :: (a -> a) -> Ptr a -> Ptr a
updatePtr :: forall a. (a -> a) -> Ptr a -> Ptr a
updatePtr a -> a
f Ptr a
p = IO (Ptr a) -> Ptr a
forall a. IO a -> a
unsafePerformIO (IO (Ptr a) -> Ptr a) -> IO (Ptr a) -> Ptr a
forall a b. (a -> b) -> a -> b
$ Ptr a
p Ptr a -> IO () -> IO (Ptr a)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ IORef a -> (a -> a) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef (Ptr a -> IORef a
forall a. Ptr a -> IORef a
ptrRef Ptr a
p) a -> a
f

setPtr :: a -> Ptr a -> Ptr a
setPtr :: forall a. a -> Ptr a -> Ptr a
setPtr !a
x = (a -> a) -> Ptr a -> Ptr a
forall a. (a -> a) -> Ptr a -> Ptr a
updatePtr (a -> a -> a
forall a b. a -> b -> a
const a
x)

-- | If @f a@ contains many copies of @a@ they will all be the same pointer in
--   the result. If the function is well-behaved (i.e. preserves the implicit
--   equivalence, this shouldn't matter).
updatePtrM :: Functor f => (a -> f a) -> Ptr a -> f (Ptr a)
updatePtrM :: forall (f :: * -> *) a.
Functor f =>
(a -> f a) -> Ptr a -> f (Ptr a)
updatePtrM a -> f a
f Ptr a
p = (a -> Ptr a -> Ptr a) -> Ptr a -> a -> Ptr a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> Ptr a -> Ptr a
forall a. a -> Ptr a -> Ptr a
setPtr Ptr a
p (a -> Ptr a) -> f a -> f (Ptr a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f a
f (Ptr a -> a
forall a. Ptr a -> a
derefPtr Ptr a
p)

instance Show a => Show (Ptr a) where
  show :: Ptr a -> String
show Ptr a
p = String
"#" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Ptr a -> Integer
forall a. Ptr a -> Integer
ptrTag Ptr a
p) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"{" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (Ptr a -> a
forall a. Ptr a -> a
derefPtr Ptr a
p) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"

instance Functor Ptr where
  fmap :: forall a b. (a -> b) -> Ptr a -> Ptr b
fmap a -> b
f = b -> Ptr b
forall a. a -> Ptr a
newPtr (b -> Ptr b) -> (Ptr a -> b) -> Ptr a -> Ptr b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f (a -> b) -> (Ptr a -> a) -> Ptr a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ptr a -> a
forall a. Ptr a -> a
derefPtr

instance Foldable Ptr where
  foldMap :: forall m a. Monoid m => (a -> m) -> Ptr a -> m
foldMap a -> m
f = a -> m
f (a -> m) -> (Ptr a -> a) -> Ptr a -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ptr a -> a
forall a. Ptr a -> a
derefPtr

instance Traversable Ptr where
  traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Ptr a -> f (Ptr b)
traverse a -> f b
f Ptr a
p = b -> Ptr b
forall a. a -> Ptr a
newPtr (b -> Ptr b) -> f b -> f (Ptr b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f (Ptr a -> a
forall a. Ptr a -> a
derefPtr Ptr a
p)

instance Eq (Ptr a) where
  == :: Ptr a -> Ptr a -> Bool
(==) = Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Integer -> Integer -> Bool)
-> (Ptr a -> Integer) -> Ptr a -> Ptr a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Ptr a -> Integer
forall a. Ptr a -> Integer
ptrTag

instance Ord (Ptr a) where
  compare :: Ptr a -> Ptr a -> Ordering
compare = Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Integer -> Integer -> Ordering)
-> (Ptr a -> Integer) -> Ptr a -> Ptr a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Ptr a -> Integer
forall a. Ptr a -> Integer
ptrTag

instance Hashable (Ptr a) where
  hashWithSalt :: Int -> Ptr a -> Int
hashWithSalt Int
salt = (Int -> Integer -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
salt) (Integer -> Int) -> (Ptr a -> Integer) -> Ptr a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ptr a -> Integer
forall a. Ptr a -> Integer
ptrTag

instance NFData (Ptr a) where rnf :: Ptr a -> ()
rnf Ptr a
x = Ptr a -> () -> ()
seq Ptr a
x ()