{-# LANGUAGE CPP #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE UnboxedTuples #-}
{-# LANGUAGE UnliftedFFITypes #-}
{-# LANGUAGE ViewPatterns #-}

-- |
-- Module      :   Grisette.Internal.SymPrim.Prim.Internal.Utils
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.Prim.Internal.Utils
  ( pattern Dyn,
    cmpHetero,
    eqHetero,
    cmpHeteroRep,
    eqHeteroRep,
    eqTypeRepBool,
    WeakThreadId,
    weakThreadId,
    WeakThreadIdRef,
    myWeakThreadId,
    weakThreadRefAlive,
    mkWeakThreadIdRefWithFinalizer,
    addStableNameFinalizer,
    addThreadIdFinalizer,
    mkWeakStableNameRefWithFinalizer,
    SomeStableName (..),
    mkWeakSomeStableNameRefWithFinalizer,
    mkWeakSomeStableNameRef,
  )
where

#if MIN_VERSION_base(4,19,0)
import GHC.Conc.Sync
  ( ThreadId(ThreadId),
    ThreadStatus (ThreadDied, ThreadFinished),
    fromThreadId,
    myThreadId,
    threadStatus,
  )
import GHC.Exts (mkWeak#, mkWeakNoFinalizer#)
#else
import GHC.Conc
  ( ThreadId (ThreadId),
    ThreadStatus (ThreadDied, ThreadFinished),
    myThreadId,
    threadStatus,
  )
import GHC.Exts (Addr#, ThreadId#, unsafeCoerce#, mkWeak#, mkWeakNoFinalizer#)
#if __GLASGOW_HASKELL__ >= 904
#elif __GLASGOW_HASKELL__ >= 900
import Foreign.C.Types (CLong (CLong))
#else
import Foreign.C.Types (CInt (CInt))
#endif
#endif
import Data.Typeable (cast)
import Data.Word (Word64)
import GHC.IO (IO (IO))
import GHC.StableName (StableName (StableName), eqStableName)
import GHC.Weak (Weak (Weak))
import System.Mem.Weak (deRefWeak)
import Type.Reflection
  ( TypeRep,
    Typeable,
    eqTypeRep,
    typeRep,
    type (:~~:) (HRefl),
  )

-- | Pattern synonym for dynamic type casting.
pattern Dyn :: (Typeable a, Typeable b) => a -> b
pattern $mDyn :: forall {r} {a} {b}.
(Typeable a, Typeable b) =>
b -> (a -> r) -> ((# #) -> r) -> r
Dyn x <- (cast -> Just x)

-- | Compare two values of different types, resolve the type equality using the
-- type representation.
cmpHeteroRep :: forall a b. TypeRep a -> TypeRep b -> (a -> a -> Bool) -> a -> b -> Bool
cmpHeteroRep :: forall a b.
TypeRep a -> TypeRep b -> (a -> a -> Bool) -> a -> b -> Bool
cmpHeteroRep TypeRep a
ta TypeRep b
tb a -> a -> Bool
f a
a b
b = case TypeRep a -> TypeRep b -> Maybe (a :~~: b)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
ta TypeRep b
tb of
  Just a :~~: b
HRefl -> a -> a -> Bool
f a
a a
b
b
  Maybe (a :~~: b)
_ -> Bool
False
{-# INLINE cmpHeteroRep #-}

-- | Compare two values of different types.
cmpHetero :: forall a b. (Typeable a, Typeable b) => (a -> a -> Bool) -> a -> b -> Bool
cmpHetero :: forall a b.
(Typeable a, Typeable b) =>
(a -> a -> Bool) -> a -> b -> Bool
cmpHetero = TypeRep a -> TypeRep b -> (a -> a -> Bool) -> a -> b -> Bool
forall a b.
TypeRep a -> TypeRep b -> (a -> a -> Bool) -> a -> b -> Bool
cmpHeteroRep (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @b)
{-# INLINE cmpHetero #-}

-- | Compare two values of different types for equality.
eqHetero :: forall a b. (Typeable a, Typeable b, Eq a) => a -> b -> Bool
eqHetero :: forall a b. (Typeable a, Typeable b, Eq a) => a -> b -> Bool
eqHetero = (a -> a -> Bool) -> a -> b -> Bool
forall a b.
(Typeable a, Typeable b) =>
(a -> a -> Bool) -> a -> b -> Bool
cmpHetero a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)
{-# INLINE eqHetero #-}

-- | Compare two values of different types for equality, resolve the type
-- equality using the type representation.
eqHeteroRep :: forall a b. (Eq a) => TypeRep a -> TypeRep b -> a -> b -> Bool
eqHeteroRep :: forall a b. Eq a => TypeRep a -> TypeRep b -> a -> b -> Bool
eqHeteroRep TypeRep a
ta TypeRep b
tb = TypeRep a -> TypeRep b -> (a -> a -> Bool) -> a -> b -> Bool
forall a b.
TypeRep a -> TypeRep b -> (a -> a -> Bool) -> a -> b -> Bool
cmpHeteroRep TypeRep a
ta TypeRep b
tb a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)
{-# INLINE eqHeteroRep #-}

-- | Compare two type representations for equality.
eqTypeRepBool :: forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool :: forall ka kb (a :: ka) (b :: kb). TypeRep a -> TypeRep b -> Bool
eqTypeRepBool TypeRep a
a TypeRep b
b = case TypeRep a -> TypeRep b -> Maybe (a :~~: b)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
a TypeRep b
b of
  Just a :~~: b
HRefl -> Bool
True
  Maybe (a :~~: b)
_ -> Bool
False
{-# INLINE eqTypeRepBool #-}

-- | A weak identifier to a thread id that doesn't prevent its garbage
-- collection.
type WeakThreadId = Word64

-- | A weak reference to a thread id that doesn't prevent its garbage
-- collection.
type WeakThreadIdRef = Weak ThreadId

{-# INLINE weakThreadId #-}

-- | Get an id of a thread that doesn't prevent its garbage collection.
weakThreadId :: ThreadId -> Word64
#if MIN_VERSION_base(4,19,0)
weakThreadId :: ThreadId -> Word64
weakThreadId = ThreadId -> Word64
fromThreadId
#else
#if __GLASGOW_HASKELL__ >= 904
weakThreadId (ThreadId t#) = rts_getThreadId (threadIdToAddr# t#)
#else
weakThreadId (ThreadId t#) = fromIntegral $ rts_getThreadId (threadIdToAddr# t#)
#endif

foreign import ccall unsafe "rts_getThreadId"
#if __GLASGOW_HASKELL__ >= 904
  -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/6163
  rts_getThreadId :: Addr# -> Word64
#elif __GLASGOW_HASKELL__ >= 900
  -- https://gitlab.haskell.org/ghc/ghc/-/merge_requests/1254
  rts_getThreadId :: Addr# -> CLong
#else
  rts_getThreadId :: Addr# -> CInt
#endif

-- Note: FFI imports take Addr# instead of ThreadId# because of
-- https://gitlab.haskell.org/ghc/ghc/-/issues/8281, which would prevent loading
-- effectful-core into GHCi.
--
-- Previous workaround was to use an internal library with just this module, but
-- this is not viable because of bugs in stack (sigh).
--
-- The coercion is fine because GHC represents ThreadId# as a pointer.
{-# INLINE threadIdToAddr# #-}
threadIdToAddr# :: ThreadId# -> Addr#
threadIdToAddr# = unsafeCoerce#
#endif

-- | Get a weak identifier to the current thread id.
myWeakThreadId :: IO WeakThreadId
myWeakThreadId :: IO Word64
myWeakThreadId = ThreadId -> Word64
weakThreadId (ThreadId -> Word64) -> IO ThreadId -> IO Word64
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ThreadId
myThreadId
{-# INLINE myWeakThreadId #-}

-- | Check if a weak reference to a thread id is still alive.
weakThreadRefAlive :: WeakThreadIdRef -> IO Bool
weakThreadRefAlive :: WeakThreadIdRef -> IO Bool
weakThreadRefAlive WeakThreadIdRef
wtid = do
  tid <- WeakThreadIdRef -> IO (Maybe ThreadId)
forall v. Weak v -> IO (Maybe v)
deRefWeak WeakThreadIdRef
wtid
  case tid of
    Maybe ThreadId
Nothing -> Bool -> IO Bool
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    Just ThreadId
tid -> do
      st <- ThreadId -> IO ThreadStatus
threadStatus ThreadId
tid
      return $ st `notElem` [ThreadFinished, ThreadDied]
{-# INLINE weakThreadRefAlive #-}

-- | Create a weak reference to a thread id with a finalizer.
mkWeakThreadIdRefWithFinalizer :: ThreadId -> IO () -> IO (Weak ThreadId)
mkWeakThreadIdRefWithFinalizer :: ThreadId -> IO () -> IO WeakThreadIdRef
mkWeakThreadIdRefWithFinalizer t :: ThreadId
t@(ThreadId ThreadId#
t#) (IO State# RealWorld -> (# State# RealWorld, () #)
finalizer) = (State# RealWorld -> (# State# RealWorld, WeakThreadIdRef #))
-> IO WeakThreadIdRef
forall a. (State# RealWorld -> (# State# RealWorld, a #)) -> IO a
IO ((State# RealWorld -> (# State# RealWorld, WeakThreadIdRef #))
 -> IO WeakThreadIdRef)
-> (State# RealWorld -> (# State# RealWorld, WeakThreadIdRef #))
-> IO WeakThreadIdRef
forall a b. (a -> b) -> a -> b
$ \State# RealWorld
s ->
  case ThreadId#
-> ThreadId
-> (State# RealWorld -> (# State# RealWorld, () #))
-> State# RealWorld
-> (# State# RealWorld, Weak# ThreadId #)
forall a b c.
a
-> b
-> (State# RealWorld -> (# State# RealWorld, c #))
-> State# RealWorld
-> (# State# RealWorld, Weak# b #)
mkWeak# ThreadId#
t# ThreadId
t State# RealWorld -> (# State# RealWorld, () #)
finalizer State# RealWorld
s of
    (# State# RealWorld
s1, Weak# ThreadId
w #) -> (# State# RealWorld
s1, Weak# ThreadId -> WeakThreadIdRef
forall v. Weak# v -> Weak v
Weak Weak# ThreadId
w #)

-- | Add a finalizer to a thread id.
addThreadIdFinalizer :: ThreadId -> IO () -> IO ()
addThreadIdFinalizer :: ThreadId -> IO () -> IO ()
addThreadIdFinalizer t :: ThreadId
t@(ThreadId ThreadId#
t#) (IO State# RealWorld -> (# State# RealWorld, () #)
finalizer) = (State# RealWorld -> (# State# RealWorld, () #)) -> IO ()
forall a. (State# RealWorld -> (# State# RealWorld, a #)) -> IO a
IO ((State# RealWorld -> (# State# RealWorld, () #)) -> IO ())
-> (State# RealWorld -> (# State# RealWorld, () #)) -> IO ()
forall a b. (a -> b) -> a -> b
$ \State# RealWorld
s ->
  case ThreadId#
-> ThreadId
-> (State# RealWorld -> (# State# RealWorld, () #))
-> State# RealWorld
-> (# State# RealWorld, Weak# ThreadId #)
forall a b c.
a
-> b
-> (State# RealWorld -> (# State# RealWorld, c #))
-> State# RealWorld
-> (# State# RealWorld, Weak# b #)
mkWeak# ThreadId#
t# ThreadId
t State# RealWorld -> (# State# RealWorld, () #)
finalizer State# RealWorld
s of
    (# State# RealWorld
s1, Weak# ThreadId
_ #) -> (# State# RealWorld
s1, () #)

-- | Create a weak reference to a stable name with a finalizer.
mkWeakStableNameRefWithFinalizer ::
  StableName a -> IO () -> IO (Weak (StableName a))
mkWeakStableNameRefWithFinalizer :: forall a. StableName a -> IO () -> IO (Weak (StableName a))
mkWeakStableNameRefWithFinalizer t :: StableName a
t@(StableName StableName# a
t#) (IO State# RealWorld -> (# State# RealWorld, () #)
finalizer) = (State# RealWorld -> (# State# RealWorld, Weak (StableName a) #))
-> IO (Weak (StableName a))
forall a. (State# RealWorld -> (# State# RealWorld, a #)) -> IO a
IO ((State# RealWorld -> (# State# RealWorld, Weak (StableName a) #))
 -> IO (Weak (StableName a)))
-> (State# RealWorld
    -> (# State# RealWorld, Weak (StableName a) #))
-> IO (Weak (StableName a))
forall a b. (a -> b) -> a -> b
$ \State# RealWorld
s ->
  case StableName# a
-> StableName a
-> (State# RealWorld -> (# State# RealWorld, () #))
-> State# RealWorld
-> (# State# RealWorld, Weak# (StableName a) #)
forall a b c.
a
-> b
-> (State# RealWorld -> (# State# RealWorld, c #))
-> State# RealWorld
-> (# State# RealWorld, Weak# b #)
mkWeak# StableName# a
t# StableName a
t State# RealWorld -> (# State# RealWorld, () #)
finalizer State# RealWorld
s of
    (# State# RealWorld
s1, Weak# (StableName a)
w #) -> (# State# RealWorld
s1, Weak# (StableName a) -> Weak (StableName a)
forall v. Weak# v -> Weak v
Weak Weak# (StableName a)
w #)

-- | Add a finalizer to a stable name.
addStableNameFinalizer :: StableName a -> IO () -> IO ()
addStableNameFinalizer :: forall a. StableName a -> IO () -> IO ()
addStableNameFinalizer t :: StableName a
t@(StableName StableName# a
t#) (IO State# RealWorld -> (# State# RealWorld, () #)
finalizer) = (State# RealWorld -> (# State# RealWorld, () #)) -> IO ()
forall a. (State# RealWorld -> (# State# RealWorld, a #)) -> IO a
IO ((State# RealWorld -> (# State# RealWorld, () #)) -> IO ())
-> (State# RealWorld -> (# State# RealWorld, () #)) -> IO ()
forall a b. (a -> b) -> a -> b
$ \State# RealWorld
s ->
  case StableName# a
-> StableName a
-> (State# RealWorld -> (# State# RealWorld, () #))
-> State# RealWorld
-> (# State# RealWorld, Weak# (StableName a) #)
forall a b c.
a
-> b
-> (State# RealWorld -> (# State# RealWorld, c #))
-> State# RealWorld
-> (# State# RealWorld, Weak# b #)
mkWeak# StableName# a
t# StableName a
t State# RealWorld -> (# State# RealWorld, () #)
finalizer State# RealWorld
s of
    (# State# RealWorld
s1, Weak# (StableName a)
_ #) -> (# State# RealWorld
s1, () #)

-- | A type-erased stable name.
data SomeStableName where
  SomeStableName :: StableName a -> SomeStableName

instance Eq SomeStableName where
  SomeStableName StableName a
l == :: SomeStableName -> SomeStableName -> Bool
== SomeStableName StableName a
r = StableName a -> StableName a -> Bool
forall a b. StableName a -> StableName b -> Bool
eqStableName StableName a
l StableName a
r

-- | Create a weak reference to a stable name.
mkWeakSomeStableNameRef :: SomeStableName -> IO (Weak SomeStableName)
mkWeakSomeStableNameRef :: SomeStableName -> IO (Weak SomeStableName)
mkWeakSomeStableNameRef t :: SomeStableName
t@(SomeStableName (StableName StableName# a
t#)) = (State# RealWorld -> (# State# RealWorld, Weak SomeStableName #))
-> IO (Weak SomeStableName)
forall a. (State# RealWorld -> (# State# RealWorld, a #)) -> IO a
IO ((State# RealWorld -> (# State# RealWorld, Weak SomeStableName #))
 -> IO (Weak SomeStableName))
-> (State# RealWorld
    -> (# State# RealWorld, Weak SomeStableName #))
-> IO (Weak SomeStableName)
forall a b. (a -> b) -> a -> b
$ \State# RealWorld
s ->
  case StableName# a
-> SomeStableName
-> State# RealWorld
-> (# State# RealWorld, Weak# SomeStableName #)
forall a b.
a -> b -> State# RealWorld -> (# State# RealWorld, Weak# b #)
mkWeakNoFinalizer# StableName# a
t# SomeStableName
t State# RealWorld
s of
    (# State# RealWorld
s1, Weak# SomeStableName
w #) -> (# State# RealWorld
s1, Weak# SomeStableName -> Weak SomeStableName
forall v. Weak# v -> Weak v
Weak Weak# SomeStableName
w #)

-- | Create a weak reference to a stable name with a finalizer.
mkWeakSomeStableNameRefWithFinalizer ::
  SomeStableName -> IO () -> IO (Weak SomeStableName)
mkWeakSomeStableNameRefWithFinalizer :: SomeStableName -> IO () -> IO (Weak SomeStableName)
mkWeakSomeStableNameRefWithFinalizer
  t :: SomeStableName
t@(SomeStableName (StableName StableName# a
t#))
  (IO State# RealWorld -> (# State# RealWorld, () #)
finalizer) = (State# RealWorld -> (# State# RealWorld, Weak SomeStableName #))
-> IO (Weak SomeStableName)
forall a. (State# RealWorld -> (# State# RealWorld, a #)) -> IO a
IO ((State# RealWorld -> (# State# RealWorld, Weak SomeStableName #))
 -> IO (Weak SomeStableName))
-> (State# RealWorld
    -> (# State# RealWorld, Weak SomeStableName #))
-> IO (Weak SomeStableName)
forall a b. (a -> b) -> a -> b
$ \State# RealWorld
s ->
    case StableName# a
-> SomeStableName
-> (State# RealWorld -> (# State# RealWorld, () #))
-> State# RealWorld
-> (# State# RealWorld, Weak# SomeStableName #)
forall a b c.
a
-> b
-> (State# RealWorld -> (# State# RealWorld, c #))
-> State# RealWorld
-> (# State# RealWorld, Weak# b #)
mkWeak# StableName# a
t# SomeStableName
t State# RealWorld -> (# State# RealWorld, () #)
finalizer State# RealWorld
s of
      (# State# RealWorld
s1, Weak# SomeStableName
w #) -> (# State# RealWorld
s1, Weak# SomeStableName -> Weak SomeStableName
forall v. Weak# v -> Weak v
Weak Weak# SomeStableName
w #)