0 | module IotaTime.Clock
 1 |
 2 | import IotaTime.Instant
 3 | import IotaTime.ZonedDateTime
 4 |
 5 | %default total
 6 |
 7 | ||| A source of current instants. Application code can quantify over this
 8 | ||| capability to replace the system clock in deterministic tests.
 9 | public export
10 | interface Clock clock where
11 |   getCurrentInstant : clock -> IO Instant
12 |
13 | ||| The host operating system's UTC clock.
14 | public export
15 | data SystemClock = MkSystemClock
16 |
17 | public export
18 | Clock SystemClock where
19 |   getCurrentInstant MkSystemClock = now
20 |
21 | ||| The system clock value used by production applications.
22 | public export
23 | systemClock : SystemClock
24 | systemClock = MkSystemClock
25 |
26 | ||| A clock that always returns one instant.
27 | public export
28 | data FixedClock = MkFixedClock Instant
29 |
30 | public export
31 | Clock FixedClock where
32 |   getCurrentInstant (MkFixedClock value) = pure value
33 |
34 | ||| Construct a deterministic clock fixed at the supplied instant.
35 | public export
36 | fixedClock : Instant -> FixedClock
37 | fixedClock = MkFixedClock
38 |
39 | ||| A clock paired with a time zone and calendar representation.
40 | export
41 | record ZonedClock (calendar : Type) (clock : Type) where
42 |   constructor MkZonedClock
43 |   underlyingClock : clock
44 |   clockZone : TimeZone
45 |
46 | ||| Pair any clock with the zone used to display its current instant.
47 | public export
48 | zonedClock : {calendar : Type} -> clock -> TimeZone -> ZonedClock calendar clock
49 | zonedClock = MkZonedClock
50 |
51 | ||| Read a clock and display its current instant in the configured zone.
52 | public export
53 | getCurrentZonedDateTime : {calendar : Type} -> {clock : Type} ->
54 |                           {auto cal : Calendar calendar} ->
55 |                           {auto rep : HasCalendarBridge
56 |                             (CalendarDate calendar @{cal})} ->
57 |                           Clock clock => ZonedClock calendar clock ->
58 |                           IO (Either CalendarConversionError
59 |                             (ZonedDateTime calendar @{cal}))
60 | getCurrentZonedDateTime value = do
61 |   instant <- getCurrentInstant value.underlyingClock
62 |   pure (IotaTime.ZonedDateTime.fromInstant instant value.clockZone)
63 |