Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Utils.Time

Description

Time-related utilities.

Synopsis

- type ClockTime = UTCTime
- getClockTime :: IO ClockTime
- getCPUTime :: MonadIO m => m CPUTime
- measureTime :: MonadIO m => m a -> m (a, CPUTime)
- newtype CPUTime = CPUTime Integer
- fromMilliseconds :: Integer -> CPUTime

# Documentation

type ClockTime = UTCTime Source #

Timestamps.

getClockTime :: IO ClockTime Source #

The current time.

getCPUTime :: MonadIO m => m CPUTime Source #

measureTime :: MonadIO m => m a -> m (a, CPUTime) Source #

Measure the time of a computation. Of course, does not work with exceptions.

newtype CPUTime Source #

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

Constructors

CPUTime Integer |

#### Instances

Instances details

EncodeTCM CPUTime Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods encodeTCM :: CPUTime -> TCM Value Source #
Pretty CPUTime Source # | Print CPU time in milli (10^-3) seconds.
Instance details Defined in Agda.Utils.Time Methods pretty :: CPUTime -> Doc Source # prettyPrec :: Int -> CPUTime -> Doc Source # prettyList :: [CPUTime] -> Doc Source #
ToJSON CPUTime Source # |
Instance details Defined in Agda.Interaction.JSONTop Methods toJSON :: CPUTime -> Value Source # toEncoding :: CPUTime -> Encoding Source # toJSONList :: [CPUTime] -> Value Source # toEncodingList :: [CPUTime] -> Encoding Source # omitField :: CPUTime -> Bool Source #
NFData CPUTime Source # |
Instance details Defined in Agda.Utils.Time Methods rnf :: CPUTime -> () Source #
Enum CPUTime Source # |

Instance details

Defined in Agda.Utils.Time

Methods

succ :: CPUTime -> CPUTime Source #

pred :: CPUTime -> CPUTime Source #

toEnum :: Int -> CPUTime Source #

fromEnum :: CPUTime -> Int Source #

enumFrom :: CPUTime -> [CPUTime] Source #

enumFromThen :: CPUTime -> CPUTime -> [CPUTime] Source #

enumFromTo :: CPUTime -> CPUTime -> [CPUTime] Source #

enumFromThenTo :: CPUTime -> CPUTime -> CPUTime -> [CPUTime] Source #

Num CPUTime Source # |
Instance details Defined in Agda.Utils.Time Methods (+) :: CPUTime -> CPUTime -> CPUTime Source # (-) :: CPUTime -> CPUTime -> CPUTime Source # (*) :: CPUTime -> CPUTime -> CPUTime Source # negate :: CPUTime -> CPUTime Source # abs :: CPUTime -> CPUTime Source # signum :: CPUTime -> CPUTime Source # fromInteger :: Integer -> CPUTime Source #
Integral CPUTime Source # |
Instance details Defined in Agda.Utils.Time Methods quot :: CPUTime -> CPUTime -> CPUTime Source # rem :: CPUTime -> CPUTime -> CPUTime Source # div :: CPUTime -> CPUTime -> CPUTime Source # mod :: CPUTime -> CPUTime -> CPUTime Source # quotRem :: CPUTime -> CPUTime -> (CPUTime, CPUTime) Source # divMod :: CPUTime -> CPUTime -> (CPUTime, CPUTime) Source # toInteger :: CPUTime -> Integer Source #
Real CPUTime Source # |
Instance details Defined in Agda.Utils.Time Methods toRational :: CPUTime -> Rational Source #
Show CPUTime Source # |
Instance details Defined in Agda.Utils.Time Methods showsPrec :: Int -> CPUTime -> ShowS Source # show :: CPUTime -> String Source # showList :: [CPUTime] -> ShowS Source #
Eq CPUTime Source # |
Instance details Defined in Agda.Utils.Time Methods (==) :: CPUTime -> CPUTime -> Bool Source # (/=) :: CPUTime -> CPUTime -> Bool Source #
Ord CPUTime Source # |
Instance details Defined in Agda.Utils.Time Methods compare :: CPUTime -> CPUTime -> Ordering Source # (<) :: CPUTime -> CPUTime -> Bool Source # (<=) :: CPUTime -> CPUTime -> Bool Source # (>) :: CPUTime -> CPUTime -> Bool Source # (>=) :: CPUTime -> CPUTime -> Bool Source # max :: CPUTime -> CPUTime -> CPUTime Source # min :: CPUTime -> CPUTime -> CPUTime Source #

fromMilliseconds :: Integer -> CPUTime Source #