0 | module IotaTime.Instant
  1 |
  2 | import IotaTime.Duration
  3 | import System.Clock
  4 |
  5 | %default total
  6 |
  7 | nanosecondsPerSecond : Integer
  8 | nanosecondsPerSecond = 1000000000
  9 |
 10 | secondsPerDay : Integer
 11 | secondsPerDay = 86400
 12 |
 13 | unixEpochOffsetDays : Integer
 14 | unixEpochOffsetDays = 11017
 15 |
 16 | unixEpochOffsetNanoseconds : Integer
 17 | unixEpochOffsetNanoseconds =
 18 |   unixEpochOffsetDays * secondsPerDay * nanosecondsPerSecond
 19 |
 20 | ||| A fixed point on the global timeline, measured in nanoseconds from
 21 | ||| March 1, 2000 at 00:00:00 UTC.
 22 | |||
 23 | ||| Representation benchmark note: if profiling shows scalar `Integer`
 24 | ||| arithmetic to be costly, compare it with a proof-oriented record of an
 25 | ||| `Integer` day, `Fin 86400` second-of-day, and `Fin 1000000000` nanosecond.
 26 | ||| The scalar is preferred until then because canonical form is structural
 27 | ||| and arithmetic cannot overflow or require normalization proofs.
 28 | export
 29 | record Instant where
 30 |   constructor MkInstant
 31 |   storedNanoseconds : Integer
 32 |
 33 | public export
 34 | Eq Instant where
 35 |   left == right = left.storedNanoseconds == right.storedNanoseconds
 36 |
 37 | public export
 38 | Ord Instant where
 39 |   compare left right = compare left.storedNanoseconds right.storedNanoseconds
 40 |
 41 | public export
 42 | Show Instant where
 43 |   show value = "fromNanosecondsSinceEpoch " ++ show value.storedNanoseconds
 44 |
 45 | ||| Construct an instant from nanoseconds relative to the library epoch.
 46 | public export
 47 | fromNanosecondsSinceEpoch : Integer -> Instant
 48 | fromNanosecondsSinceEpoch = MkInstant
 49 |
 50 | ||| Read an instant as nanoseconds relative to the library epoch.
 51 | public export
 52 | toNanosecondsSinceEpoch : Instant -> Integer
 53 | toNanosecondsSinceEpoch = storedNanoseconds
 54 |
 55 | ||| Backward-compatible name for `toNanosecondsSinceEpoch`.
 56 | export
 57 | ticks : Instant -> Integer
 58 | ticks = toNanosecondsSinceEpoch
 59 |
 60 | ||| Converting a scalar nanosecond count to an instant and back is exact.
 61 | public export
 62 | instantNanosecondsRoundTrip : (value : Integer) ->
 63 |   toNanosecondsSinceEpoch (fromNanosecondsSinceEpoch value) = value
 64 | instantNanosecondsRoundTrip value = Refl
 65 |
 66 | ||| Reconstructing an instant from its scalar nanosecond count is exact.
 67 | public export
 68 | instantRoundTrip : (value : Instant) ->
 69 |   fromNanosecondsSinceEpoch (toNanosecondsSinceEpoch value) = value
 70 | instantRoundTrip (MkInstant value) = Refl
 71 |
 72 | ||| Construct an instant from whole seconds relative to the Unix epoch.
 73 | public export
 74 | fromSecondsSinceUnixEpoch : Integer -> Instant
 75 | fromSecondsSinceUnixEpoch seconds =
 76 |   MkInstant (seconds * nanosecondsPerSecond - unixEpochOffsetNanoseconds)
 77 |
 78 | ||| Construct an instant from nanoseconds relative to the Unix epoch.
 79 | public export
 80 | fromNanosecondsSinceUnixEpoch : Integer -> Instant
 81 | fromNanosecondsSinceUnixEpoch value =
 82 |   MkInstant (value - unixEpochOffsetNanoseconds)
 83 |
 84 | ||| Read an instant as nanoseconds relative to the Unix epoch.
 85 | public export
 86 | toNanosecondsSinceUnixEpoch : Instant -> Integer
 87 | toNanosecondsSinceUnixEpoch value =
 88 |   value.storedNanoseconds + unixEpochOffsetNanoseconds
 89 |
 90 | ||| Read an instant as whole seconds relative to the Unix epoch, truncated toward negative infinity.
 91 | public export
 92 | toSecondsSinceUnixEpoch : Instant -> Integer
 93 | toSecondsSinceUnixEpoch value =
 94 |   toNanosecondsSinceUnixEpoch value `div` nanosecondsPerSecond
 95 |
 96 | ||| Add a fixed duration to an instant.
 97 | export
 98 | addDuration : Instant -> Duration -> Instant
 99 | addDuration instant duration = MkInstant
100 |   (instant.storedNanoseconds +
101 |     toDurationNanoseconds duration)
102 |
103 | public export
104 | add : Instant -> Duration -> Instant
105 | add = addDuration
106 |
107 | ||| Subtract a fixed duration from an instant.
108 | export
109 | subtractDuration : Instant -> Duration -> Instant
110 | subtractDuration instant duration = MkInstant
111 |   (instant.storedNanoseconds -
112 |     toDurationNanoseconds duration)
113 |
114 | public export
115 | minus : Instant -> Duration -> Instant
116 | minus = subtractDuration
117 |
118 | ||| Compute the signed fixed duration from the second instant to the first.
119 | public export
120 | difference : Instant -> Instant -> Duration
121 | difference left right = durationFromNanoseconds
122 |   (left.storedNanoseconds - right.storedNanoseconds)
123 |
124 | ||| Read the current UTC system clock as an instant.
125 | public export
126 | now : IO Instant
127 | now = do
128 |   current <- clockTime UTC
129 |   pure (fromNanosecondsSinceUnixEpoch (toNano current))
130 |
131 | ||| The library epoch: March 1, 2000 at 00:00:00 UTC.
132 | public export
133 | epoch : Instant
134 | epoch = MkInstant 0