    -- To avoid warning on derived Integral instance for CPUTime.
    {-# OPTIONS_GHC -fno-warn-identities #-}

    -- | Time-related utilities.

    module Agda.Utils.Time
      ( ClockTime
      , getClockTime
      , getCPUTime
      , measureTime
      , CPUTime(..)
      , fromMilliseconds
      ) where

    import Control.DeepSeq
    import Control.Monad.Trans
    import qualified System.CPUTime as CPU

    import qualified Data.Time

    import Agda.Utils.Pretty
    import Agda.Utils.String

    -- | Timestamps.

    type ClockTime = Data.Time.UTCTime

    -- | The current time.

    getClockTime :: IO ClockTime
    getClockTime :: IO ClockTime
    getClockTime = IO ClockTime
    Data.Time.getCurrentTime

    -- | CPU time in pico (10^-12) seconds.

    newtype CPUTime = CPUTime Integer
      deriving (CPUTime -> CPUTime -> Bool
    (CPUTime -> CPUTime -> Bool)
    -> (CPUTime -> CPUTime -> Bool) -> Eq CPUTime
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: CPUTime -> CPUTime -> Bool
    $c/= :: CPUTime -> CPUTime -> Bool
    == :: CPUTime -> CPUTime -> Bool
    $c== :: CPUTime -> CPUTime -> Bool
    Eq, Int -> CPUTime -> ShowS
    [CPUTime] -> ShowS
    CPUTime -> String
    (Int -> CPUTime -> ShowS)
    -> (CPUTime -> String) -> ([CPUTime] -> ShowS) -> Show CPUTime
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [CPUTime] -> ShowS
    $cshowList :: [CPUTime] -> ShowS
    show :: CPUTime -> String
    $cshow :: CPUTime -> String
    showsPrec :: Int -> CPUTime -> ShowS
    $cshowsPrec :: Int -> CPUTime -> ShowS
    Show, Eq CPUTime
    Eq CPUTime
    -> (CPUTime -> CPUTime -> Ordering)
    -> (CPUTime -> CPUTime -> Bool)
    -> (CPUTime -> CPUTime -> Bool)
    -> (CPUTime -> CPUTime -> Bool)
    -> (CPUTime -> CPUTime -> Bool)
    -> (CPUTime -> CPUTime -> CPUTime)
    -> (CPUTime -> CPUTime -> CPUTime)
    -> Ord CPUTime
    CPUTime -> CPUTime -> Bool
    CPUTime -> CPUTime -> Ordering
    CPUTime -> CPUTime -> CPUTime
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: CPUTime -> CPUTime -> CPUTime
    $cmin :: CPUTime -> CPUTime -> CPUTime
    max :: CPUTime -> CPUTime -> CPUTime
    $cmax :: CPUTime -> CPUTime -> CPUTime
    >= :: CPUTime -> CPUTime -> Bool
    $c>= :: CPUTime -> CPUTime -> Bool
    > :: CPUTime -> CPUTime -> Bool
    $c> :: CPUTime -> CPUTime -> Bool
    <= :: CPUTime -> CPUTime -> Bool
    $c<= :: CPUTime -> CPUTime -> Bool
    < :: CPUTime -> CPUTime -> Bool
    $c< :: CPUTime -> CPUTime -> Bool
    compare :: CPUTime -> CPUTime -> Ordering
    $ccompare :: CPUTime -> CPUTime -> Ordering
    Ord, Integer -> CPUTime
    CPUTime -> CPUTime
    CPUTime -> CPUTime -> CPUTime
    (CPUTime -> CPUTime -> CPUTime)
    -> (CPUTime -> CPUTime -> CPUTime)
    -> (CPUTime -> CPUTime -> CPUTime)
    -> (CPUTime -> CPUTime)
    -> (CPUTime -> CPUTime)
    -> (CPUTime -> CPUTime)
    -> (Integer -> CPUTime)
    -> Num CPUTime
    forall a.
    (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (Integer -> a)
    -> Num a
    fromInteger :: Integer -> CPUTime
    $cfromInteger :: Integer -> CPUTime
    signum :: CPUTime -> CPUTime
    $csignum :: CPUTime -> CPUTime
    abs :: CPUTime -> CPUTime
    $cabs :: CPUTime -> CPUTime
    negate :: CPUTime -> CPUTime
    $cnegate :: CPUTime -> CPUTime
    * :: CPUTime -> CPUTime -> CPUTime
    $c* :: CPUTime -> CPUTime -> CPUTime
    - :: CPUTime -> CPUTime -> CPUTime
    $c- :: CPUTime -> CPUTime -> CPUTime
    + :: CPUTime -> CPUTime -> CPUTime
    $c+ :: CPUTime -> CPUTime -> CPUTime
    Num, Num CPUTime
    Ord CPUTime
    Num CPUTime -> Ord CPUTime -> (CPUTime -> Rational) -> Real CPUTime
    CPUTime -> Rational
    forall a. Num a -> Ord a -> (a -> Rational) -> Real a
    toRational :: CPUTime -> Rational
    $ctoRational :: CPUTime -> Rational
    Real, Int -> CPUTime
    CPUTime -> Int
    CPUTime -> [CPUTime]
    CPUTime -> CPUTime
    CPUTime -> CPUTime -> [CPUTime]
    CPUTime -> CPUTime -> CPUTime -> [CPUTime]
    (CPUTime -> CPUTime)
    -> (CPUTime -> CPUTime)
    -> (Int -> CPUTime)
    -> (CPUTime -> Int)
    -> (CPUTime -> [CPUTime])
    -> (CPUTime -> CPUTime -> [CPUTime])
    -> (CPUTime -> CPUTime -> [CPUTime])
    -> (CPUTime -> CPUTime -> CPUTime -> [CPUTime])
    -> Enum CPUTime
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    enumFromThenTo :: CPUTime -> CPUTime -> CPUTime -> [CPUTime]
    $cenumFromThenTo :: CPUTime -> CPUTime -> CPUTime -> [CPUTime]
    enumFromTo :: CPUTime -> CPUTime -> [CPUTime]
    $cenumFromTo :: CPUTime -> CPUTime -> [CPUTime]
    enumFromThen :: CPUTime -> CPUTime -> [CPUTime]
    $cenumFromThen :: CPUTime -> CPUTime -> [CPUTime]
    enumFrom :: CPUTime -> [CPUTime]
    $cenumFrom :: CPUTime -> [CPUTime]
    fromEnum :: CPUTime -> Int
    $cfromEnum :: CPUTime -> Int
    toEnum :: Int -> CPUTime
    $ctoEnum :: Int -> CPUTime
    pred :: CPUTime -> CPUTime
    $cpred :: CPUTime -> CPUTime
    succ :: CPUTime -> CPUTime
    $csucc :: CPUTime -> CPUTime
    Enum, Enum CPUTime
    Real CPUTime
    Real CPUTime
    -> Enum CPUTime
    -> (CPUTime -> CPUTime -> CPUTime)
    -> (CPUTime -> CPUTime -> CPUTime)
    -> (CPUTime -> CPUTime -> CPUTime)
    -> (CPUTime -> CPUTime -> CPUTime)
    -> (CPUTime -> CPUTime -> (CPUTime, CPUTime))
    -> (CPUTime -> CPUTime -> (CPUTime, CPUTime))
    -> (CPUTime -> Integer)
    -> Integral CPUTime
    CPUTime -> Integer
    CPUTime -> CPUTime -> (CPUTime, CPUTime)
    CPUTime -> CPUTime -> CPUTime
    forall a.
    Real a
    -> Enum a
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> (a, a))
    -> (a -> a -> (a, a))
    -> (a -> Integer)
    -> Integral a
    toInteger :: CPUTime -> Integer
    $ctoInteger :: CPUTime -> Integer
    divMod :: CPUTime -> CPUTime -> (CPUTime, CPUTime)
    $cdivMod :: CPUTime -> CPUTime -> (CPUTime, CPUTime)
    quotRem :: CPUTime -> CPUTime -> (CPUTime, CPUTime)
    $cquotRem :: CPUTime -> CPUTime -> (CPUTime, CPUTime)
    mod :: CPUTime -> CPUTime -> CPUTime
    $cmod :: CPUTime -> CPUTime -> CPUTime
    div :: CPUTime -> CPUTime -> CPUTime
    $cdiv :: CPUTime -> CPUTime -> CPUTime
    rem :: CPUTime -> CPUTime -> CPUTime
    $crem :: CPUTime -> CPUTime -> CPUTime
    quot :: CPUTime -> CPUTime -> CPUTime
    $cquot :: CPUTime -> CPUTime -> CPUTime
    Integral, CPUTime -> ()
    (CPUTime -> ()) -> NFData CPUTime
    forall a. (a -> ()) -> NFData a
    rnf :: CPUTime -> ()
    $crnf :: CPUTime -> ()
    NFData)

    fromMilliseconds :: Integer -> CPUTime
    fromMilliseconds :: Integer -> CPUTime
    fromMilliseconds Integer
    n = Integer -> CPUTime
    CPUTime (Integer
    n Integer -> Integer -> Integer
    forall a. Num a => a -> a -> a
    * Integer
    1000000000)

    -- | Print CPU time in milli (10^-3) seconds.

    instance Pretty CPUTime where
      pretty :: CPUTime -> Doc
    pretty (CPUTime Integer
    ps) =
        String -> Doc
    text (String -> Doc) -> String -> Doc
    forall a b. (a -> b) -> a -> b
    $ Integer -> String
    forall a. Show a => a -> String
    showThousandSep (Integer -> Integer -> Integer
    forall a. Integral a => a -> a -> a
    div Integer
    ps Integer
    1000000000) String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    "ms"

    {-# SPECIALIZE getCPUTime :: IO CPUTime #-}
    getCPUTime :: MonadIO m => m CPUTime
    getCPUTime :: forall (m :: * -> *). MonadIO m => m CPUTime
    getCPUTime = IO CPUTime -> m CPUTime
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO CPUTime -> m CPUTime) -> IO CPUTime -> m CPUTime
    forall a b. (a -> b) -> a -> b
    $ Integer -> CPUTime
    CPUTime (Integer -> CPUTime) -> IO Integer -> IO CPUTime
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> IO Integer
    CPU.getCPUTime

    -- | Measure the time of a computation.
    --   Of course, does not work with exceptions.
    measureTime :: MonadIO m => m a -> m (a, CPUTime)
    measureTime :: forall (m :: * -> *) a. MonadIO m => m a -> m (a, CPUTime)
    measureTime m a
    m = do
      CPUTime
    start <- IO CPUTime -> m CPUTime
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO CPUTime -> m CPUTime) -> IO CPUTime -> m CPUTime
    forall a b. (a -> b) -> a -> b
    $ IO CPUTime
    forall (m :: * -> *). MonadIO m => m CPUTime
    getCPUTime
      a
    x     <- m a
    m
      CPUTime
    stop  <- IO CPUTime -> m CPUTime
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO CPUTime -> m CPUTime) -> IO CPUTime -> m CPUTime
    forall a b. (a -> b) -> a -> b
    $ IO CPUTime
    forall (m :: * -> *). MonadIO m => m CPUTime
    getCPUTime
      (a, CPUTime) -> m (a, CPUTime)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a
    x, CPUTime
    stop CPUTime -> CPUTime -> CPUTime
    forall a. Num a => a -> a -> a
    - CPUTime
    start)