System.Clock

Types and functions for reasoning about time.

Definitions

data ClockType : Type

  The various types of system clock available.

Totality: total
Visibility: public export
Constructors:

UTC : ClockType

  The time elapsed since the "epoch:" 00:00:00 UTC, January 1, 1970

Monotonic : ClockType

  The time elapsed since some arbitrary point in the past

Duration : ClockType

  Representing a time duration.

Process : ClockType

  The amount of CPU time used by the current process.

Thread : ClockType

  The amount of CPU time used by the current thread.

GCCPU : ClockType

  The current process's CPU time consumed by the garbage collector.

GCReal : ClockType

  The current process's real time consumed by the garbage collector.

Hints:

Eq (Clock type)

Ord (Clock type)

Show ClockType

Show (Clock type)

data Clock : ClockType -> Type

  A clock recording some time in seconds and nanoseconds. The "type" of time
  recorded is indicated by the given `ClockType`.

Totality: total
Visibility: public export
Constructor: 

MkClock : Integer -> Integer -> Clock type

Hints:

Eq (Clock type)

Ord (Clock type)

Show (Clock type)

showTime : Nat -> Nat -> Clock type -> String

  Display a `Clock`'s content, padding the seconds and nanoseconds as
  appropriate.
  
  @ s   the number of digits used to display the seconds
  @ ns  the number of digits used to display the nanosecondns
  @ clk the Clock whose contents to display

Totality: total
Visibility: export

seconds : Clock type -> Integer

  A helper to deconstruct a Clock.

Totality: total
Visibility: public export

nanoseconds : Clock type -> Integer

  A helper to deconstruct a Clock.

Totality: total
Visibility: public export

makeDuration : Integer -> Integer -> Clock Duration

  Make a duration value.
  
  @ s  the number of seconds in the duration
  @ ns the number of nanoseconds in the duration

Totality: total
Visibility: public export

data ClockTypeMandatory : Type

  Note: Backends are required to implement UTC, monotonic time, CPU time in
  current process/thread, and time duration; the rest are optional.

Totality: total
Visibility: export
Constructors:

Mandatory : ClockTypeMandatory

Optional : ClockTypeMandatory

isClockMandatory : ClockType -> ClockTypeMandatory

  Determine whether the specified `ClockType` is required to be implemented by
  all backends.

Totality: total
Visibility: public export

clockTimeReturnType : ClockType -> Type

  The return type of a function using a `Clock` depends on the type of
  `Clock`:
  * `Optional` clocks may not be implemented, so we might not return anything
  * `Mandatory` clocks have to be implemented, so we _will_ return something

Totality: total
Visibility: public export

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, we return a `Maybe (Clock type)`.

Totality: total
Visibility: public export

toNano : Clock type -> Integer

  Convert the time in the given clock to nanoseconds.

Totality: total
Visibility: public export

fromNano : Integer -> Clock type

  Convert some time in nanoseconds to a `Clock` containing that time.
  
  @ n the time in nanoseconds

Totality: total
Visibility: public export

timeDifference : Clock type -> Clock type -> Clock Duration

  Compute difference between two clocks of the same type.
  @ end the end time
  @ start the start time

Totality: total
Visibility: public export

addDuration : Clock type -> Clock Duration -> Clock type

  Add a duration to a clock value.

Totality: total
Visibility: public export

subtractDuration : Clock type -> Clock Duration -> Clock type

  Subtract a duration from a clock value.

Totality: total
Visibility: public export