Agda-2.7.0.1: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Utils.Time

Description

Time-related utilities.

Synopsis

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 #

toEncoding :: CPUTime -> Encoding #

toJSONList :: [CPUTime] -> Value #

toEncodingList :: [CPUTime] -> Encoding #

omitField :: CPUTime -> Bool #

Enum CPUTime Source # 
Instance details

Defined in Agda.Utils.Time

Methods

succ :: CPUTime -> CPUTime #

pred :: CPUTime -> CPUTime #

toEnum :: Int -> CPUTime #

fromEnum :: CPUTime -> Int #

enumFrom :: CPUTime -> [CPUTime] #

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

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

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

Num CPUTime Source # 
Instance details

Defined in Agda.Utils.Time

Methods

(+) :: CPUTime -> CPUTime -> CPUTime #

(-) :: CPUTime -> CPUTime -> CPUTime #

(*) :: CPUTime -> CPUTime -> CPUTime #

negate :: CPUTime -> CPUTime #

abs :: CPUTime -> CPUTime #

signum :: CPUTime -> CPUTime #

fromInteger :: Integer -> CPUTime #

Integral CPUTime Source # 
Instance details

Defined in Agda.Utils.Time

Methods

quot :: CPUTime -> CPUTime -> CPUTime #

rem :: CPUTime -> CPUTime -> CPUTime #

div :: CPUTime -> CPUTime -> CPUTime #

mod :: CPUTime -> CPUTime -> CPUTime #

quotRem :: CPUTime -> CPUTime -> (CPUTime, CPUTime) #

divMod :: CPUTime -> CPUTime -> (CPUTime, CPUTime) #

toInteger :: CPUTime -> Integer #

Real CPUTime Source # 
Instance details

Defined in Agda.Utils.Time

Methods

toRational :: CPUTime -> Rational #

Show CPUTime Source # 
Instance details

Defined in Agda.Utils.Time

Methods

showsPrec :: Int -> CPUTime -> ShowS #

show :: CPUTime -> String #

showList :: [CPUTime] -> ShowS #

NFData CPUTime Source # 
Instance details

Defined in Agda.Utils.Time

Methods

rnf :: CPUTime -> () #

Eq CPUTime Source # 
Instance details

Defined in Agda.Utils.Time

Methods

(==) :: CPUTime -> CPUTime -> Bool #

(/=) :: CPUTime -> CPUTime -> Bool #

Ord CPUTime Source # 
Instance details

Defined in Agda.Utils.Time

Methods

compare :: CPUTime -> CPUTime -> Ordering #

(<) :: CPUTime -> CPUTime -> Bool #

(<=) :: CPUTime -> CPUTime -> Bool #

(>) :: CPUTime -> CPUTime -> Bool #

(>=) :: CPUTime -> CPUTime -> Bool #

max :: CPUTime -> CPUTime -> CPUTime #

min :: CPUTime -> CPUTime -> CPUTime #

fromMilliseconds :: Integer -> CPUTime Source #