IotaTime.Clock

Definitions

interface Clock : Type -> Type

  A source of current instants. Application code can quantify over this
  capability to replace the system clock in deterministic tests.

Parameters: clock
Methods:

getCurrentInstant : clock -> IO Instant

Implementations:

Clock SystemClock

Clock FixedClock

getCurrentInstant : Clock clock => clock -> IO Instant

Totality: total
Visibility: public export

data SystemClock : Type

  The host operating system's UTC clock.

Totality: total
Visibility: public export
Constructor: 

MkSystemClock : SystemClock

Hint: 

Clock SystemClock

systemClock : SystemClock

  The system clock value used by production applications.

Totality: total
Visibility: public export

data FixedClock : Type

  A clock that always returns one instant.

Totality: total
Visibility: public export
Constructor: 

MkFixedClock : Instant -> FixedClock

Hint: 

Clock FixedClock

fixedClock : Instant -> FixedClock

  Construct a deterministic clock fixed at the supplied instant.

Totality: total
Visibility: public export

record ZonedClock : Type -> Type -> Type

  A clock paired with a time zone and calendar representation.

Totality: total
Visibility: export
Constructor: 

MkZonedClock : clock -> TimeZone -> ZonedClock calendar clock

Projections:

.clockZone : ZonedClock calendar clock -> TimeZone

.underlyingClock : ZonedClock calendar clock -> clock

zonedClock : clock -> TimeZone -> ZonedClock calendar clock

  Pair any clock with the zone used to display its current instant.

Totality: total
Visibility: public export

getCurrentZonedDateTime : {auto cal : Calendar calendar} -> HasCalendarBridge (CalendarDate calendar) => Clock clock => ZonedClock calendar clock -> IO (Either CalendarConversionError (ZonedDateTime calendar))

  Read a clock and display its current instant in the configured zone.

Totality: total
Visibility: public export