- data Clock : ClockType -> Type
- Totality: total
Constructor: - MkClock : Integer -> Integer -> Clock type
- data ClockType : Type
The various types of system clock available.
Totality: total
Constructors:
- UTC : ClockType
- Monotonic : ClockType
- Duration : ClockType
- Process : ClockType
- Thread : ClockType
- GCCPU : ClockType
- GCReal : ClockType
- data ClockTypeMandatory : Type
Note: Back-ends are required to implement UTC, monotonic time, CPU time
in current process/thread, and time duration; the rest are optional.
Totality: total
Constructors:
- Mandatory : ClockTypeMandatory
- Optional : ClockTypeMandatory
- addDuration : Clock type -> Clock Duration -> Clock type
Add a duration to a clock value.
Totality: total- clockTime : (typ : ClockType) -> IO (clockTimeReturnType typ)
Fetch the system clock of a given kind. If the clock is mandatory,
we return a (Clock type) else (Maybe (Clock type)).
Totality: total- clockTimeReturnType : ClockType -> Type
- Totality: total
- isClockMandatory : ClockType -> ClockTypeMandatory
- Totality: total
- makeDuration : Integer -> Integer -> Clock Duration
Make a duration value.
Totality: total- nanoseconds : Clock type -> Integer
A helper to deconstruct a Clock.
Totality: total- seconds : Clock type -> Integer
A helper to deconstruct a Clock.
Totality: total- showTime : Nat -> Nat -> Clock type -> String
- Totality: total
- subtractDuration : Clock type -> Clock Duration -> Clock type
Subtract a duration from a clock value.
Totality: total- timeDifference : Clock type -> Clock type -> Clock Duration
Compute difference between two clocks of the same type.
Totality: total