{-# LANGUAGE ScopedTypeVariables, DeriveDataTypeable #-}

-- |
-- Module      :  Test.ChasingBottoms.TimeOut
-- 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 (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
$cshowsPrec :: forall a. Show a => Int -> Result a -> ShowS
showsPrec :: Int -> Result a -> ShowS
$cshow :: forall a. Show a => Result a -> String
show :: Result a -> String
$cshowList :: forall a. Show a => [Result a] -> ShowS
showList :: [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 :: forall a. 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
* Int
10Int -> Integer -> Int
forall a b. (Num a, Integral b) => a -> b -> a
^Integer
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 :: forall a. Int -> IO a -> IO (Result a)
timeOutMicro Int
delay 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 a b. IO a -> (a -> IO b) -> IO b
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
Die -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- Thread properly killed.
                  Maybe Die
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 a. a -> IO 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
$cshowsPrec :: Int -> Die -> ShowS
showsPrec :: Int -> Die -> ShowS
$cshow :: Die -> String
show :: Die -> String
$cshowList :: [Die] -> ShowS
showList :: [Die] -> ShowS
Show, Typeable)

instance E.Exception Die

killThread' :: ThreadId -> IO ()
killThread' 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' :: forall a. Int -> a -> IO (Result a)
timeOut' 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' :: forall a. Int -> a -> IO (Result a)
timeOutMicro' 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 = Int
1; d :: Int
d = Int
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 [Integer
1..]) IO (Result [Integer]) -> (Result [Integer] -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
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 [Integer
1..]) IO (Result [Integer]) -> (Result [Integer] -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
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 [Integer
1..]) IO (Result [Integer]) -> (Result [Integer] -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
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 [Integer
1..]) IO (Result [Integer]) -> (Result [Integer] -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Result [Integer] -> IO ()
forall a. Show a => a -> IO ()
print