-- 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
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
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
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
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
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]
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
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 -> ()
forall a. (a -> ()) -> NFData a
rnf :: CPUTime -> ()
$crnf :: CPUTime -> ()
NFData)

fromMilliseconds :: Integer -> CPUTime
fromMilliseconds :: Integer -> CPUTime
fromMilliseconds Integer
n = Integer -> CPUTime
CPUTime (Integer
n 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 forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
showThousandSep (forall a. Integral a => a -> a -> a
div Integer
ps Integer
1000000000) forall a. [a] -> [a] -> [a]
++ String
"ms"

{-# SPECIALIZE getCPUTime :: IO CPUTime #-}
getCPUTime :: MonadIO m => m CPUTime
getCPUTime :: forall (m :: * -> *). MonadIO m => m CPUTime
getCPUTime = forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Integer -> CPUTime
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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadIO m => m CPUTime
getCPUTime
  a
x     <- m a
m
  CPUTime
stop  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadIO m => m CPUTime
getCPUTime
  forall (m :: * -> *) a. Monad m => a -> m a
return (a
x, CPUTime
stop forall a. Num a => a -> a -> a
- CPUTime
start)