    {-# LANGUAGE ScopedTypeVariables, DeriveDataTypeable #-}

    -- |
    -- Module      :  Test.ChasingBottoms.TimeOut
    -- Copyright   :  (c) Nils Anders Danielsson 2004-2020
    -- License     :  See the file LICENCE.
    --
    -- Maintainer  :  http://www.cse.chalmers.se/~nad/
    -- Stability   :  experimental
    -- Portability :  non-portable (preemptive scheduling)
    --
    -- When dealing with \"hard bottoms\", i.e. non-terminating
    -- computations that do not result in exceptions, the following functions
    -- may be handy.
    --
    -- Note that a computation is considered to have terminated when it
    -- has reached weak head normal form (i.e. something distinct from
    -- bottom).

    module Test.ChasingBottoms.TimeOut
      ( Result(..)
      , timeOut
      , timeOut'
      , timeOutMicro
      , timeOutMicro'
      ) where

    import Control.Concurrent
    import Data.Dynamic
    import qualified Control.Exception as E

    import {-# SOURCE #-} qualified Test.ChasingBottoms.IsBottom as B

    data Result a
      = Value a
      | NonTermination
      | Exception E.SomeException
        deriving (Int -> Result a -> ShowS
    [Result a] -> ShowS
    Result a -> String
    (Int -> Result a -> ShowS)
    -> (Result a -> String) -> ([Result a] -> ShowS) -> Show (Result a)
    forall a. Show a => Int -> Result a -> ShowS
    forall a. Show a => [Result a] -> ShowS
    forall a. Show a => Result a -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Result a] -> ShowS
    $cshowList :: forall a. Show a => [Result a] -> ShowS
    show :: Result a -> String
    $cshow :: forall a. Show a => Result a -> String
    showsPrec :: Int -> Result a -> ShowS
    $cshowsPrec :: forall a. Show a => Int -> Result a -> ShowS
    Show, Typeable)

    -- | @'timeOut' n c@ runs @c@ for at most @n@ seconds (modulo
    -- scheduling issues).
    --
    --   * If the computation terminates before that, then @'Value' v@ is
    --     returned, where @v@ is the resulting value. Note that this
    --     value may be equal to bottom, e.g. if @c = 'return'
    --     'B.bottom'@.
    --
    --   * If the computation does not terminate, then 'NonTermination' is
    --     returned.
    --
    --   * If the computation raises an exception, then @'Exception' e@ is
    --     returned, where @e@ is the exception.
    --
    -- Note that a user-defined exception is used to terminate the
    -- computation, so if @c@ catches all exceptions, or blocks
    -- asynchronous exceptions, then 'timeOut' may fail to function
    -- properly.

    timeOut :: Int -> IO a -> IO (Result a)
    timeOut :: Int -> IO a -> IO (Result a)
    timeOut = Int -> IO a -> IO (Result a)
    forall a. Int -> IO a -> IO (Result a)
    timeOutMicro (Int -> IO a -> IO (Result a))
    -> (Int -> Int) -> Int -> IO a -> IO (Result a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * 10Int -> Integer -> Int
    forall a b. (Num a, Integral b) => a -> b -> a
    ^6)

    -- | 'timeOutMicro' takes a delay in microseconds. Note that the
    -- resolution is not necessarily very high (the last time I checked it
    -- was 0.02 seconds when using the standard runtime system settings
    -- for GHC).

    timeOutMicro :: Int -> IO a -> IO (Result a)
    timeOutMicro :: Int -> IO a -> IO (Result a)
    timeOutMicro delay :: Int
    delay io :: IO a
    io = do
      MVar (Result a)
    mv <- IO (MVar (Result a))
    forall a. IO (MVar a)
    newEmptyMVar
      let putException :: SomeException -> IO ()
    putException = MVar (Result a) -> Result a -> IO ()
    forall a. MVar a -> a -> IO ()
    putMVar MVar (Result a)
    mv (Result a -> IO ())
    -> (SomeException -> Result a) -> SomeException -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SomeException -> Result a
    forall a. SomeException -> Result a
    Exception
      ThreadId
    ioThread <- IO () -> IO ThreadId
    forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
    forall a b. (a -> b) -> a -> b
    $
        (IO a
    io IO a -> (a -> IO ()) -> IO ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= MVar (Result a) -> Result a -> IO ()
    forall a. MVar a -> a -> IO ()
    putMVar MVar (Result a)
    mv (Result a -> IO ()) -> (a -> Result a) -> a -> IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Result a
    forall a. a -> Result a
    Value)
        IO () -> (SomeException -> IO ()) -> IO ()
    forall e a. Exception e => IO a -> (e -> IO a) -> IO a
    `E.catch` (\(SomeException
    e :: E.SomeException) ->
                    case SomeException -> Maybe Die
    forall e. Exception e => SomeException -> Maybe e
    E.fromException SomeException
    e of
                      Just Die -> () -> IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()  -- Thread properly killed.
                      Nothing  -> SomeException -> IO ()
    putException SomeException
    e)
      ThreadId
    reaper <- IO () -> IO ThreadId
    forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
    forall a b. (a -> b) -> a -> b
    $ do
        Int -> IO ()
    threadDelay Int
    delay
        MVar (Result a) -> Result a -> IO ()
    forall a. MVar a -> a -> IO ()
    putMVar MVar (Result a)
    mv Result a
    forall a. Result a
    NonTermination
      Result a
    result <- MVar (Result a) -> IO (Result a)
    forall a. MVar a -> IO a
    takeMVar MVar (Result a)
    mv
      ThreadId -> IO ()
    killThread' ThreadId
    ioThread
      ThreadId -> IO ()
    killThread ThreadId
    reaper
      Result a -> IO (Result a)
    forall (m :: * -> *) a. Monad m => a -> m a
    return Result a
    result

    -- Since 'ioThread' above should return exceptions raised in the code
    -- it seems like a bad idea to kill the thread using killThread, which
    -- raises @'AsyncException' 'ThreadKilled'@. We use the locally
    -- defined type 'Die' instead.

    data Die = Die deriving (Int -> Die -> ShowS
    [Die] -> ShowS
    Die -> String
    (Int -> Die -> ShowS)
    -> (Die -> String) -> ([Die] -> ShowS) -> Show Die
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Die] -> ShowS
    $cshowList :: [Die] -> ShowS
    show :: Die -> String
    $cshow :: Die -> String
    showsPrec :: Int -> Die -> ShowS
    $cshowsPrec :: Int -> Die -> ShowS
    Show, Typeable)

    instance E.Exception Die

    killThread' :: ThreadId -> IO ()
    killThread' threadId :: ThreadId
    threadId = ThreadId -> Die -> IO ()
    forall e. Exception e => ThreadId -> e -> IO ()
    E.throwTo ThreadId
    threadId Die
    Die

    -- | 'timeOut'' is a variant which can be used for pure
    -- computations. The definition,
    --
    -- @
    --   'timeOut'' n = 'timeOut' n . 'E.evaluate'
    -- @
    --
    -- ensures that @'timeOut'' 1 'B.bottom'@ usually returns @'Exception'
    -- \<something\>@. (@'timeOut' 1 ('return' 'B.bottom')@ usually
    -- returns @'Value' 'B.bottom'@; in other words, the computation
    -- reaches whnf almost immediately, defeating the purpose of the
    -- time-out.)

    timeOut' :: Int -> a -> IO (Result a)
    timeOut' :: Int -> a -> IO (Result a)
    timeOut' n :: Int
    n = Int -> IO a -> IO (Result a)
    forall a. Int -> IO a -> IO (Result a)
    timeOut Int
    n (IO a -> IO (Result a)) -> (a -> IO a) -> a -> IO (Result a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> IO a
    forall a. a -> IO a
    E.evaluate

    -- | 'timeOutMicro'' is the equivalent variant of 'timeOutMicro':
    --
    -- @
    --  'timeOutMicro'' n = 'timeOutMicro' n . 'E.evaluate'
    -- @

    timeOutMicro' :: Int -> a -> IO (Result a)
    timeOutMicro' :: Int -> a -> IO (Result a)
    timeOutMicro' n :: Int
    n = Int -> IO a -> IO (Result a)
    forall a. Int -> IO a -> IO (Result a)
    timeOutMicro Int
    n (IO a -> IO (Result a)) -> (a -> IO a) -> a -> IO (Result a)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> IO a
    forall a. a -> IO a
    E.evaluate

    ------------------------------------------------------------------------

    -- There shouldn't be any memory leaks in the code above. Profiling
    -- the code below also seems to suggest that there aren't any
    -- problems. However, GHCi (with :set +r) eats up more and more memory
    -- if the computation below is rerun a couple of times. Hmm, that
    -- seems to be the case also when running simply (reverse [1..]). It
    -- probably means that GHCi never releases any memory.

    main :: IO ()
    main = do
      let n :: Int
    n = 1; d :: Int
    d = 000000
      {-# SCC "a" #-} Int -> [Integer] -> IO (Result [Integer])
    forall a. Int -> a -> IO (Result a)
    timeOut' Int
    n ([Integer] -> [Integer]
    forall a. [a] -> [a]
    reverse [1..]) IO (Result [Integer]) -> (Result [Integer] -> IO ()) -> IO ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Result [Integer] -> IO ()
    forall a. Show a => a -> IO ()
    print
      Int -> IO ()
    threadDelay Int
    d
      {-# SCC "b" #-} Int -> [Integer] -> IO (Result [Integer])
    forall a. Int -> a -> IO (Result a)
    timeOut' Int
    n ([Integer] -> [Integer]
    forall a. [a] -> [a]
    reverse [1..]) IO (Result [Integer]) -> (Result [Integer] -> IO ()) -> IO ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Result [Integer] -> IO ()
    forall a. Show a => a -> IO ()
    print
      Int -> IO ()
    threadDelay Int
    d
      {-# SCC "c" #-} Int -> [Integer] -> IO (Result [Integer])
    forall a. Int -> a -> IO (Result a)
    timeOut' Int
    n ([Integer] -> [Integer]
    forall a. [a] -> [a]
    reverse [1..]) IO (Result [Integer]) -> (Result [Integer] -> IO ()) -> IO ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Result [Integer] -> IO ()
    forall a. Show a => a -> IO ()
    print
      Int -> IO ()
    threadDelay Int
    d
      {-# SCC "d" #-} Int -> [Integer] -> IO (Result [Integer])
    forall a. Int -> a -> IO (Result a)
    timeOut' Int
    n ([Integer] -> [Integer]
    forall a. [a] -> [a]
    reverse [1..]) IO (Result [Integer]) -> (Result [Integer] -> IO ()) -> IO ()
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= Result [Integer] -> IO ()
    forall a. Show a => a -> IO ()
    print