    {-# LANGUAGE ScopedTypeVariables #-}
    -- The following (possibly unnecessary) options are included due to
    -- the use of unsafePerformIO below.
    {-# OPTIONS_GHC -fno-cse -fno-full-laziness #-}

    -- |
    -- Module      :  Test.ChasingBottoms.IsBottom
    -- Copyright   :  (c) Nils Anders Danielsson 2004-2022, 2024
    -- License     :  See the file LICENCE.
    --
    -- Maintainer  :  http://www.cse.chalmers.se/~nad/
    -- Stability   :  experimental
    -- Portability :  non-portable (exceptions)
    --

    module Test.ChasingBottoms.IsBottom
      ( isBottom
      , isBottomIO
      , bottom
      , nonBottomError
      , isBottomTimeOut
      , isBottomTimeOutIO
      ) where

    import Prelude hiding (catch)
    import qualified Control.Exception as E
    import System.IO.Unsafe (unsafePerformIO)
    import qualified Test.ChasingBottoms.TimeOut as T

    -- | @'isBottom' a@ returns 'False' if @a@ is distinct from bottom. If
    -- @a@ equals bottom and results in an exception of a certain kind
    -- (see below), then @'isBottom' a = 'True'@. If @a@ never reaches a
    -- weak head normal form and never throws one of these exceptions,
    -- then @'isBottom' a@ never terminates.
    --
    -- The exceptions that yield 'True' correspond to \"pure bottoms\",
    -- i.e. bottoms that can originate in pure code:
    --
    --   * 'E.ArrayException'
    --
    --   * 'E.ErrorCall'
    --
    --   * 'E.NoMethodError'
    --
    --   * 'E.NonTermination'
    --
    --   * 'E.PatternMatchFail'
    --
    --   * 'E.RecConError'
    --
    --   * 'E.RecSelError'
    --
    --   * 'E.RecUpdError'
    --
    -- Assertions are excluded, because their behaviour depends on
    -- compiler flags (not pure, and a failed assertion should really
    -- yield an exception and nothing else). The same applies to
    -- arithmetic exceptions (machine dependent, except possibly for
    -- 'E.DivideByZero', but the value infinity makes that case unclear as
    -- well).

    -- Should we use throw or throwIO below?
    --   It doesn't seem to matter, and I don't think it matters, but
    --   using throw won't give us any problems.

    -- Check out a discussion about evaluate around
    -- http://www.haskell.org/pipermail/glasgow-haskell-users/2002-May/003393.html.

    -- From the docs:
    --   evaluate undefined `seq` return ()  ==> return ()
    --   catch (evaluate undefined) (\e -> return ())  ==> return ()

    isBottom :: a -> Bool
    isBottom :: forall a. a -> Bool
    isBottom = Maybe Int -> a -> Bool
    forall a. Maybe Int -> a -> Bool
    isBottomTimeOut Maybe Int
    forall a. Maybe a
    Nothing

    -- | 'bottom' generates a bottom that is suitable for testing using
    -- 'isBottom'.
    bottom :: a
    bottom :: forall a. a
    bottom = [Char] -> a
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "_|_"

    -- | @'nonBottomError' s@ raises an exception ('E.AssertionFailed')
    -- that is not caught by 'isBottom'. Use @s@ to describe the
    -- exception.

    nonBottomError :: String -> a
    nonBottomError :: forall a. [Char] -> a
    nonBottomError = AssertionFailed -> a
    forall a e. Exception e => e -> a
    E.throw (AssertionFailed -> a)
    -> ([Char] -> AssertionFailed) -> [Char] -> a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> AssertionFailed
    E.AssertionFailed

    -- | @'isBottomTimeOut' timeOutLimit@ works like 'isBottom', but if
    -- @timeOutLimit@ is @'Just' lim@, then computations taking more than
    -- @lim@ seconds are also considered to be equal to bottom. Note that
    -- this is a very crude approximation of what a bottom is. Also note
    -- that this \"function\" may return different answers upon different
    -- invocations. Take it for what it is worth.
    --
    -- 'isBottomTimeOut' is subject to all the same vagaries as
    -- 'T.timeOut'.

    -- The following pragma is included due to the use of unsafePerformIO
    -- below.
    {-# NOINLINE isBottomTimeOut #-}
    isBottomTimeOut :: Maybe Int -> a -> Bool
    isBottomTimeOut :: forall a. Maybe Int -> a -> Bool
    isBottomTimeOut Maybe Int
    timeOutLimit a
    f =
      IO Bool -> Bool
    forall a. IO a -> a
    unsafePerformIO (IO Bool -> Bool) -> IO Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Maybe Int -> a -> IO Bool
    forall a. Maybe Int -> a -> IO Bool
    isBottomTimeOutIO Maybe Int
    timeOutLimit a
    f

    -- | A variant of 'isBottom' that lives in the 'IO' monad.

    isBottomIO :: a -> IO Bool
    isBottomIO :: forall a. a -> IO Bool
    isBottomIO = Maybe Int -> a -> IO Bool
    forall a. Maybe Int -> a -> IO Bool
    isBottomTimeOutIO Maybe Int
    forall a. Maybe a
    Nothing

    -- | A variant of 'isBottomTimeOut' that lives in the 'IO' monad.

    isBottomTimeOutIO :: Maybe Int -> a -> IO Bool
    isBottomTimeOutIO :: forall a. Maybe Int -> a -> IO Bool
    isBottomTimeOutIO Maybe Int
    timeOutLimit a
    f =
      IO a -> IO Bool
    forall {a}. IO a -> IO Bool
    maybeTimeOut (a -> IO a
    forall a. a -> IO a
    E.evaluate a
    f) IO Bool -> [Handler Bool] -> IO Bool
    forall a. IO a -> [Handler a] -> IO a
    `E.catches`
        [ (ArrayException -> IO Bool) -> Handler Bool
    forall a e. Exception e => (e -> IO a) -> Handler a
    E.Handler (\(ArrayException
    _ :: E.ArrayException)   -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True)
        , (ErrorCall -> IO Bool) -> Handler Bool
    forall a e. Exception e => (e -> IO a) -> Handler a
    E.Handler (\(ErrorCall
    _ :: E.ErrorCall)        -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True)
        , (NoMethodError -> IO Bool) -> Handler Bool
    forall a e. Exception e => (e -> IO a) -> Handler a
    E.Handler (\(NoMethodError
    _ :: E.NoMethodError)    -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True)
        , (NonTermination -> IO Bool) -> Handler Bool
    forall a e. Exception e => (e -> IO a) -> Handler a
    E.Handler (\(NonTermination
    _ :: E.NonTermination)   -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True)
        , (PatternMatchFail -> IO Bool) -> Handler Bool
    forall a e. Exception e => (e -> IO a) -> Handler a
    E.Handler (\(PatternMatchFail
    _ :: E.PatternMatchFail) -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True)
        , (RecConError -> IO Bool) -> Handler Bool
    forall a e. Exception e => (e -> IO a) -> Handler a
    E.Handler (\(RecConError
    _ :: E.RecConError)      -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True)
        , (RecSelError -> IO Bool) -> Handler Bool
    forall a e. Exception e => (e -> IO a) -> Handler a
    E.Handler (\(RecSelError
    _ :: E.RecSelError)      -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True)
        , (RecUpdError -> IO Bool) -> Handler Bool
    forall a e. Exception e => (e -> IO a) -> Handler a
    E.Handler (\(RecUpdError
    _ :: E.RecUpdError)      -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True)
        ]
      where
      maybeTimeOut :: IO a -> IO Bool
    maybeTimeOut IO a
    io = case Maybe Int
    timeOutLimit of
        Maybe Int
    Nothing -> do
          IO a
    io
          Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        Just Int
    lim -> do
          Result a
    result <- Int -> IO a -> IO (Result a)
    forall a. Int -> IO a -> IO (Result a)
    T.timeOut Int
    lim IO a
    io
          case Result a
    result of               -- Note that evaluate bottom /= bottom.
            T.Value a
    _        -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
            Result a
    T.NonTermination -> Bool -> IO Bool
    forall a. a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
            T.Exception SomeException
    e    -> SomeException -> IO Bool
    forall a e. Exception e => e -> a
    E.throw SomeException
    e  -- Catch the exception above.