{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash      #-}
{-# LANGUAGE PolyKinds      #-}
{-# LANGUAGE UnboxedTuples  #-}
module PureSAT.Assert (
    assertST,
    -- * Utilities
    throwST,
    raiseST#,
) where

import Control.Exception (AssertionFailed (..), Exception (..))
import GHC.Exts          (State#, raiseIO#, unsafeCoerce#)
import GHC.ST            (ST (..))
import GHC.Stack         (HasCallStack, callStack, prettyCallStack)

assertST :: HasCallStack => String -> Bool -> ST s ()
assertST :: forall s. HasCallStack => String -> Bool -> ST s ()
assertST String
_   Bool
True  = () -> ST s ()
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
assertST String
msg Bool
False = AssertionFailed -> ST s ()
forall e s a. Exception e => e -> ST s a
throwST (String -> AssertionFailed
AssertionFailed (String
"Assertion failed\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ CallStack -> String
prettyCallStack CallStack
HasCallStack => CallStack
callStack))

raiseST# :: a -> State# s -> (# State# s, b #)
raiseST# :: forall a s b. a -> State# s -> (# State# s, b #)
raiseST# = (Any -> State# RealWorld -> (# State# RealWorld, Any #))
-> a -> State# s -> (# State# s, b #)
forall a b. a -> b
unsafeCoerce# Any -> State# RealWorld -> (# State# RealWorld, Any #)
forall a b. a -> State# RealWorld -> (# State# RealWorld, b #)
raiseIO#

throwST :: Exception e => e -> ST s a
throwST :: forall e s a. Exception e => e -> ST s a
throwST e
e = STRep s a -> ST s a
forall s a. STRep s a -> ST s a
ST (SomeException -> STRep s a
forall a s b. a -> State# s -> (# State# s, b #)
raiseST# (e -> SomeException
forall e. Exception e => e -> SomeException
toException e
e))