{-# 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.