{-# OPTIONS_GHC -Wunused-imports #-}

-- 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.Syntax.Common.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
$c== :: CPUTime -> CPUTime -> Bool
== :: CPUTime -> CPUTime -> Bool
$c/= :: CPUTime -> CPUTime -> Bool
/= :: 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
$cshowsPrec :: Int -> CPUTime -> ShowS
showsPrec :: Int -> CPUTime -> ShowS
$cshow :: CPUTime -> String
show :: CPUTime -> String
$cshowList :: [CPUTime] -> ShowS
showList :: [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
$ccompare :: CPUTime -> CPUTime -> Ordering
compare :: CPUTime -> CPUTime -> Ordering
$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
>= :: CPUTime -> CPUTime -> Bool
$cmax :: CPUTime -> CPUTime -> CPUTime
max :: CPUTime -> CPUTime -> CPUTime
$cmin :: CPUTime -> CPUTime -> CPUTime
min :: CPUTime -> CPUTime -> CPUTime
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
$c+ :: CPUTime -> CPUTime -> CPUTime
+ :: CPUTime -> CPUTime -> CPUTime
$c- :: CPUTime -> CPUTime -> CPUTime
- :: CPUTime -> CPUTime -> CPUTime
$c* :: CPUTime -> CPUTime -> CPUTime
* :: CPUTime -> CPUTime -> CPUTime
$cnegate :: CPUTime -> CPUTime
negate :: CPUTime -> CPUTime
$cabs :: CPUTime -> CPUTime
abs :: CPUTime -> CPUTime
$csignum :: CPUTime -> CPUTime
signum :: CPUTime -> CPUTime
$cfromInteger :: Integer -> CPUTime
fromInteger :: Integer -> 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
$ctoRational :: CPUTime -> Rational
toRational :: 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
$csucc :: CPUTime -> CPUTime
succ :: CPUTime -> CPUTime
$cpred :: CPUTime -> CPUTime
pred :: CPUTime -> CPUTime
$ctoEnum :: Int -> CPUTime
toEnum :: Int -> CPUTime
$cfromEnum :: CPUTime -> Int
fromEnum :: CPUTime -> Int
$cenumFrom :: CPUTime -> [CPUTime]
enumFrom :: CPUTime -> [CPUTime]
$cenumFromThen :: CPUTime -> CPUTime -> [CPUTime]
enumFromThen :: CPUTime -> CPUTime -> [CPUTime]
$cenumFromTo :: CPUTime -> CPUTime -> [CPUTime]
enumFromTo :: CPUTime -> CPUTime -> [CPUTime]
$cenumFromThenTo :: CPUTime -> CPUTime -> CPUTime -> [CPUTime]
enumFromThenTo :: CPUTime -> CPUTime -> 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
$cquot :: CPUTime -> CPUTime -> CPUTime
quot :: CPUTime -> CPUTime -> CPUTime
$crem :: CPUTime -> CPUTime -> CPUTime
rem :: CPUTime -> CPUTime -> CPUTime
$cdiv :: CPUTime -> CPUTime -> CPUTime
div :: CPUTime -> CPUTime -> CPUTime
$cmod :: CPUTime -> CPUTime -> CPUTime
mod :: CPUTime -> CPUTime -> CPUTime
$cquotRem :: CPUTime -> CPUTime -> (CPUTime, CPUTime)
quotRem :: CPUTime -> CPUTime -> (CPUTime, CPUTime)
$cdivMod :: CPUTime -> CPUTime -> (CPUTime, CPUTime)
divMod :: CPUTime -> CPUTime -> (CPUTime, CPUTime)
$ctoInteger :: CPUTime -> Integer
toInteger :: CPUTime -> Integer
Integral, CPUTime -> ()
(CPUTime -> ()) -> NFData CPUTime
forall a. (a -> ()) -> NFData a
$crnf :: CPUTime -> ()
rnf :: 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
forall a. String -> Doc a
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 a. IO a -> m a
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
  start <- IO CPUTime -> m CPUTime
forall a. IO a -> m a
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
  x     <- m
  stop  <- liftIO $ getCPUTime
  return (x, stop - start)