0 | module IotaTime.ZonedDateTime
  1 |
  2 | import public IotaTime.TimeZone.Core
  3 | import public IotaTime.Duration
  4 | import public IotaTime.OffsetDateTime
  5 |
  6 | %default total
  7 |
  8 | export
  9 | record ZonedDateTimeRep (calendar : Type) (cal : Calendar calendar) where
 10 |   constructor MkZonedDateTime
 11 |   zonedValue : OffsetDateTime calendar @{cal}
 12 |   zonedZone : TimeZone
 13 |
 14 | public export
 15 | ZonedDateTime : (calendar : Type) -> {auto cal : Calendar calendar} -> Type
 16 | ZonedDateTime calendar @{cal} = ZonedDateTimeRep calendar cal
 17 |
 18 | public export
 19 | {calendar : Type} -> {cal : Calendar calendar} ->
 20 |   Eq (OffsetDateTime calendar @{cal}) =>
 21 |   Eq (ZonedDateTimeRep calendar cal) where
 22 |   left == right =
 23 |     left.zonedValue == right.zonedValue && left.zonedZone == right.zonedZone
 24 |
 25 | ||| Display an instant in a zone using the zone's effective offset. Conversion
 26 | ||| fails only when the resulting local day is outside the calendar's range.
 27 | export
 28 | inZone : {calendar : Type} -> {auto cal : Calendar calendar} ->
 29 |          {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
 30 |          TimeZone -> Instant ->
 31 |          Either CalendarConversionError (ZonedDateTime calendar @{cal})
 32 | inZone valueZone valueInstant =
 33 |   map (\value => MkZonedDateTime value valueZone)
 34 |     (IotaTime.OffsetDateTime.fromInstant
 35 |       (zoneOffsetAt valueZone valueInstant) valueInstant)
 36 |
 37 | ||| HodaTime-compatible instant-first constructor.
 38 | public export
 39 | fromInstant : {calendar : Type} -> {auto cal : Calendar calendar} ->
 40 |               {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
 41 |               Instant -> TimeZone ->
 42 |               Either CalendarConversionError (ZonedDateTime calendar @{cal})
 43 | fromInstant valueInstant valueZone = inZone valueZone valueInstant
 44 |
 45 | export
 46 | zonedOffsetDateTime : {calendar : Type} -> {auto cal : Calendar calendar} ->
 47 |                       ZonedDateTime calendar @{cal} ->
 48 |                       OffsetDateTime calendar @{cal}
 49 | zonedOffsetDateTime = zonedValue
 50 |
 51 | export
 52 | zonedLocalDateTime : {calendar : Type} -> {auto cal : Calendar calendar} ->
 53 |                      ZonedDateTime calendar @{cal} ->
 54 |                      CalendarDateTime calendar @{cal}
 55 | zonedLocalDateTime = localDateTime . zonedValue
 56 |
 57 | public export
 58 | toCalendarDateTime : {calendar : Type} -> {auto cal : Calendar calendar} ->
 59 |                      ZonedDateTime calendar @{cal} ->
 60 |                      CalendarDateTime calendar @{cal}
 61 | toCalendarDateTime = zonedLocalDateTime
 62 |
 63 | public export
 64 | toCalendarDate : {calendar : Type} -> {auto cal : Calendar calendar} ->
 65 |                  ZonedDateTime calendar @{cal} -> CalendarDate calendar @{cal}
 66 | toCalendarDate = datePart . zonedLocalDateTime
 67 |
 68 | public export
 69 | toLocalTime : {calendar : Type} -> {auto cal : Calendar calendar} ->
 70 |               ZonedDateTime calendar @{cal} -> LocalTime
 71 | toLocalTime = localTimeOfDay . zonedLocalDateTime
 72 |
 73 | public export
 74 | year : {calendar : Type} -> {auto cal : Calendar calendar} ->
 75 |   ZonedDateTime calendar @{cal} -> Year
 76 | year = IotaTime.Calendar.yearFor . toCalendarDate
 77 |
 78 | public export
 79 | month : {calendar : Type} -> {auto cal : Calendar calendar} ->
 80 |    (value : ZonedDateTime calendar @{cal}) ->
 81 |    MonthRep @{cal} (IotaTime.ZonedDateTime.year value)
 82 | month value = IotaTime.Calendar.monthFor (toCalendarDate value)
 83 |
 84 | public export
 85 | day : {calendar : Type} -> {auto cal : Calendar calendar} ->
 86 |       ZonedDateTime calendar @{cal} -> DayOfMonth
 87 | day = IotaTime.Calendar.dayFor . toCalendarDate
 88 |
 89 | public export
 90 | hour : {calendar : Type} -> {auto cal : Calendar calendar} ->
 91 |   ZonedDateTime calendar @{cal} -> Hour
 92 | hour = IotaTime.LocalTime.hour . toLocalTime
 93 |
 94 | public export
 95 | minute : {calendar : Type} -> {auto cal : Calendar calendar} ->
 96 |     ZonedDateTime calendar @{cal} -> Minute
 97 | minute = IotaTime.LocalTime.minute . toLocalTime
 98 |
 99 | public export
100 | second : {calendar : Type} -> {auto cal : Calendar calendar} ->
101 |     ZonedDateTime calendar @{cal} -> Second
102 | second = IotaTime.LocalTime.second . toLocalTime
103 |
104 | public export
105 | nanosecond : {calendar : Type} -> {auto cal : Calendar calendar} ->
106 |         ZonedDateTime calendar @{cal} -> Nanosecond
107 | nanosecond = IotaTime.LocalTime.nanosecond . toLocalTime
108 |
109 | export
110 | zonedOffset : {calendar : Type} -> {auto cal : Calendar calendar} ->
111 |               ZonedDateTime calendar @{cal} -> Offset
112 | zonedOffset = offsetOf . zonedValue
113 |
114 | export
115 | zonedInstant : {calendar : Type} -> {auto cal : Calendar calendar} ->
116 |                {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
117 |                ZonedDateTime calendar @{cal} -> Instant
118 | zonedInstant = IotaTime.OffsetDateTime.toInstant . zonedValue
119 |
120 | public export
121 | toInstant : {calendar : Type} -> {auto cal : Calendar calendar} ->
122 |             {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
123 |             ZonedDateTime calendar @{cal} -> Instant
124 | toInstant = zonedInstant
125 |
126 | public export
127 | {calendar : Type} -> {cal : Calendar calendar} ->
128 |   HasCalendarBridge (CalendarDate calendar @{cal}) =>
129 |   Eq (CalendarDate calendar @{cal}) =>
130 |   Ord (ZonedDateTimeRep calendar cal) where
131 |   compare left right =
132 |     compare (zonedInstant left) (zonedInstant right) <+>
133 |     compare
134 |       (IotaTime.TimeZone.Core.zoneId left.zonedZone)
135 |       (IotaTime.TimeZone.Core.zoneId right.zonedZone)
136 |
137 | public export
138 | {calendar : Type} -> {cal : Calendar calendar} ->
139 |   HasCalendarBridge (CalendarDate calendar @{cal}) =>
140 |   Show (ZonedDateTimeRep calendar cal) where
141 |   show value = "fromInstant (" ++
142 |     show (zonedInstant value) ++ ") (" ++
143 |     show value.zonedZone ++ ")"
144 |
145 | export
146 | zoneOf : {calendar : Type} -> {auto cal : Calendar calendar} ->
147 |          ZonedDateTime calendar @{cal} -> TimeZone
148 | zoneOf = zonedZone
149 |
150 | public export
151 | zoneId : {calendar : Type} -> {auto cal : Calendar calendar} ->
152 |          ZonedDateTime calendar @{cal} -> String
153 | zoneId = IotaTime.TimeZone.Core.zoneId . zonedZone
154 |
155 | public export
156 | inDst : {calendar : Type} -> {auto cal : Calendar calendar} ->
157 |         {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
158 |         ZonedDateTime calendar @{cal} -> Bool
159 | inDst value = isDaylightSavingTime
160 |   (activeTransitionAt value.zonedZone (zonedInstant value))
161 |
162 | public export
163 | zoneAbbreviation : {calendar : Type} -> {auto cal : Calendar calendar} ->
164 |                    {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
165 |                    ZonedDateTime calendar @{cal} -> String
166 | zoneAbbreviation value = abbreviation
167 |   (activeTransitionAt value.zonedZone (zonedInstant value))
168 |
169 | ||| The complete result of resolving a local date-time into a zone.
170 | public export
171 | data ZonedMapping : (calendar : Type) ->
172 |                     (cal : Calendar calendar) -> Type where
173 |   ZonedSkipped : ZonedMapping calendar cal
174 |   ZonedUnambiguous : ZonedDateTime calendar @{cal} -> ZonedMapping calendar cal
175 |   ZonedAmbiguous : (earliest : ZonedDateTime calendar @{cal}) ->
176 |                    (next : ZonedDateTime calendar @{cal}) ->
177 |                    (additional : List (ZonedDateTime calendar @{cal})) ->
178 |                    ZonedMapping calendar cal
179 |
180 | attachZone : {calendar : Type} -> {auto cal : Calendar calendar} ->
181 |              TimeZone -> OffsetDateTime calendar @{cal} ->
182 |              ZonedDateTime calendar @{cal}
183 | attachZone valueZone value = MkZonedDateTime value valueZone
184 |
185 | attachAll : {calendar : Type} -> {auto cal : Calendar calendar} ->
186 |             TimeZone -> List (OffsetDateTime calendar @{cal}) ->
187 |             List (ZonedDateTime calendar @{cal})
188 | attachAll valueZone = map (attachZone valueZone)
189 |
190 | ||| Resolve a local date-time without choosing silently between skipped or
191 | ||| ambiguous mappings.
192 | public export
193 | resolveLocal : {calendar : Type} -> {auto cal : Calendar calendar} ->
194 |                {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
195 |                TimeZone -> CalendarDateTime calendar @{cal} ->
196 |                ZonedMapping calendar cal
197 | resolveLocal valueZone local = case mappingCandidates valueZone local of
198 |   [] => ZonedSkipped
199 |   [value] => ZonedUnambiguous (attachZone valueZone value)
200 |   first :: second :: rest => ZonedAmbiguous
201 |     (attachZone valueZone first)
202 |     (attachZone valueZone second)
203 |     (attachAll valueZone rest)
204 |
205 | ||| Return every valid mapping of a local calendar date-time, in instant order.
206 | public export
207 | fromCalendarDateTimeAll : {calendar : Type} -> {auto cal : Calendar calendar} ->
208 |                           {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
209 |                           CalendarDateTime calendar @{cal} -> TimeZone ->
210 |                           List (ZonedDateTime calendar @{cal})
211 | fromCalendarDateTimeAll local valueZone = case resolveLocal valueZone local of
212 |   ZonedSkipped => []
213 |   ZonedUnambiguous value => [value]
214 |   ZonedAmbiguous first second rest => first :: second :: rest
215 |
216 | public export
217 | data ZonedDateTimeError
218 |   = DateTimeDoesNotExist
219 |   | DateTimeAmbiguous
220 |   | LenientResolutionFailed
221 |   | ZonedCalendarOutOfRange CalendarConversionError
222 |
223 | ||| Resolve only a unique local mapping. Skipped and ambiguous values are
224 | ||| returned as typed errors rather than exceptions.
225 | public export
226 | fromCalendarDateTimeStrictly : {calendar : Type} ->
227 |                                {auto cal : Calendar calendar} ->
228 |                                {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
229 |                                CalendarDateTime calendar @{cal} -> TimeZone ->
230 |                                Either ZonedDateTimeError
231 |                                  (ZonedDateTime calendar @{cal})
232 | fromCalendarDateTimeStrictly local valueZone =
233 |   case resolveLocal valueZone local of
234 |     ZonedSkipped => Left DateTimeDoesNotExist
235 |     ZonedUnambiguous value => Right value
236 |     ZonedAmbiguous _ _ _ => Left DateTimeAmbiguous
237 |
238 | ||| Apply HodaTime's lenient rules: choose the earliest ambiguous mapping and
239 | ||| shift skipped values forward by the transition gap.
240 | public export
241 | fromCalendarDateTimeLeniently : {calendar : Type} ->
242 |                                 {auto cal : Calendar calendar} ->
243 |                                 {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
244 |                                 CalendarDateTime calendar @{cal} -> TimeZone ->
245 |                                 Either ZonedDateTimeError
246 |                                   (ZonedDateTime calendar @{cal})
247 | fromCalendarDateTimeLeniently local valueZone =
248 |   case lenientLocalMapping valueZone local of
249 |     Left error => Left (ZonedCalendarOutOfRange error)
250 |     Right Nothing => Left LenientResolutionFailed
251 |     Right (Just value) => Right (attachZone valueZone value)
252 |
253 | ||| Change zones while preserving the represented instant.
254 | public export
255 | withZone : {calendar : Type} -> {auto cal : Calendar calendar} ->
256 |            {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
257 |            TimeZone -> ZonedDateTime calendar @{cal} ->
258 |            Either CalendarConversionError (ZonedDateTime calendar @{cal})
259 | withZone valueZone value = inZone valueZone (zonedInstant value)
260 |
261 | ||| Change calendars while preserving the instant and zone.
262 | public export
263 | withCalendar : {source : Type} -> {target : Type} ->
264 |                {auto sourceCal : Calendar source} ->
265 |                {auto targetCal : Calendar target} ->
266 |                {auto sourceRep : HasCalendarBridge (CalendarDate source @{sourceCal})} ->
267 |                {auto targetRep : HasCalendarBridge (CalendarDate target @{targetCal})} ->
268 |                ZonedDateTime source @{sourceCal} ->
269 |                Either CalendarConversionError (ZonedDateTime target @{targetCal})
270 | withCalendar {target} @{sourceCal} @{targetCal} @{sourceRep} @{targetRep} value =
271 |   inZone {calendar = target} @{targetCal} @{targetRep} value.zonedZone
272 |     (zonedInstant @{sourceCal} @{sourceRep} value)
273 |
274 | ||| Add elapsed time on the global timeline, then re-evaluate the zone offset.
275 | export
276 | addZonedDuration : {calendar : Type} -> {auto cal : Calendar calendar} ->
277 |                    {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
278 |                    Duration -> ZonedDateTime calendar @{cal} ->
279 |                    Either CalendarConversionError (ZonedDateTime calendar @{cal})
280 | addZonedDuration amount value =
281 |   inZone value.zonedZone (addDuration (zonedInstant value) amount)
282 |
283 | ||| Add fixed elapsed time, following HodaTime's value-first argument order.
284 | public export
285 | add : {calendar : Type} -> {auto cal : Calendar calendar} ->
286 |   {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
287 |   ZonedDateTime calendar @{cal} -> Duration ->
288 |   Either CalendarConversionError (ZonedDateTime calendar @{cal})
289 | add value amount = addZonedDuration amount value
290 |
291 | ||| Subtract elapsed time on the global timeline, then re-evaluate the zone offset.
292 | export
293 | subtractZonedDuration : {calendar : Type} -> {auto cal : Calendar calendar} ->
294 |                         {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
295 |                         Duration -> ZonedDateTime calendar @{cal} ->
296 |                         Either CalendarConversionError (ZonedDateTime calendar @{cal})
297 | subtractZonedDuration amount value =
298 |   inZone value.zonedZone (subtractDuration (zonedInstant value) amount)
299 |
300 | ||| Subtract fixed elapsed time, following HodaTime's value-first argument order.
301 | public export
302 | minus : {calendar : Type} -> {auto cal : Calendar calendar} ->
303 |         {auto rep : HasCalendarBridge (CalendarDate calendar @{cal})} ->
304 |         ZonedDateTime calendar @{cal} -> Duration ->
305 |         Either CalendarConversionError (ZonedDateTime calendar @{cal})
306 | minus value amount = subtractZonedDuration amount value
307 |