{-# LANGUAGE CPP #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# OPTIONS_GHC -fno-warn-identities #-}
module Agda.Utils.Time
( ClockTime
, getClockTime
, getCPUTime
, measureTime
, CPUTime(..)
, fromMilliseconds
) where
import Control.Monad.Trans
import qualified System.CPUTime as CPU
import Data.Functor
import qualified Data.Time
import Agda.Utils.Pretty
import Agda.Utils.String
type ClockTime = Data.Time.UTCTime
getClockTime :: IO ClockTime
getClockTime = Data.Time.getCurrentTime
newtype CPUTime = CPUTime Integer
deriving (Eq, Show, Ord, Num, Real, Enum, Integral)
fromMilliseconds :: Integer -> CPUTime
fromMilliseconds n = CPUTime (n * 1000000000)
instance Pretty CPUTime where
pretty (CPUTime ps) =
text $ showThousandSep (div ps 1000000000) ++ "ms"
{-# SPECIALIZE getCPUTime :: IO CPUTime #-}
getCPUTime :: MonadIO m => m CPUTime
getCPUTime = liftIO $ CPUTime <$> CPU.getCPUTime
measureTime :: MonadIO m => m a -> m (a, CPUTime)
measureTime m = do
start <- liftIO $ getCPUTime
x <- m
stop <- liftIO $ getCPUTime
return (x, stop - start)