0 | module IotaTime.Pattern.ZonedDateTime
  1 |
  2 | import IotaTime.Calendar.Gregorian
  3 | import IotaTime.CalendarDateTime
  4 | import IotaTime.TimeZone
  5 | import IotaTime.Pattern
  6 | import IotaTime.Pattern.Calendar
  7 | import IotaTime.Pattern.CalendarDate
  8 | import IotaTime.Pattern.CalendarDateTime
  9 | import IotaTime.Pattern.LocalTime
 10 | import IotaTime.Pattern.Scalar
 11 | import IotaTime.Period
 12 | import IotaTime.ZonedDateTime
 13 |
 14 | %default total
 15 |
 16 | ||| A format-only ZonedDateTime pattern. Parsing requires loading a zone and
 17 | ||| choosing how skipped or ambiguous local times are resolved.
 18 | export
 19 | record ZonedDateTimePattern state value where
 20 |   constructor MkZonedDateTimePattern
 21 |   zonedFormatPart : value -> String
 22 |
 23 | ||| Build a format-only ZonedDateTime pattern from a local date-time pattern
 24 | ||| and a function that renders the zone suffix.
 25 | public export
 26 | zonedDateTimePattern :
 27 |   {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 28 |   Pattern state (CalendarDateTime calendar) ->
 29 |   (ZonedDateTime calendar -> String) ->
 30 |   ZonedDateTimePattern state (ZonedDateTime calendar)
 31 | zonedDateTimePattern local render = MkZonedDateTimePattern
 32 |   (\value => IotaTime.Pattern.format local
 33 |     (IotaTime.ZonedDateTime.toCalendarDateTime value) ++ render value)
 34 |
 35 | ||| Format a zoned value using its local date-time and rendered zone suffix.
 36 | public export
 37 | formatZonedDateTime : ZonedDateTimePattern state value -> value -> String
 38 | formatZonedDateTime pattern = pattern.zonedFormatPart
 39 |
 40 | ||| ISO local date-time followed by a space and the zone ID.
 41 | public export
 42 | pZonedDateTime : {calendar : Type} ->
 43 |   {auto patterned : CalendarPattern calendar} ->
 44 |   ZonedDateTimePattern (DateFields, TimeFields) (ZonedDateTime calendar)
 45 | pZonedDateTime = zonedDateTimePattern ps
 46 |   (\value => " " ++ IotaTime.ZonedDateTime.zoneId value)
 47 |
 48 | ||| ISO local date-time followed by a quoted, escaped zone ID. This form can
 49 | ||| represent Windows identifiers containing spaces.
 50 | public export
 51 | pZonedDateTimeQuoted : {calendar : Type} ->
 52 |   {auto patterned : CalendarPattern calendar} ->
 53 |   ZonedDateTimePattern (DateFields, TimeFields) (ZonedDateTime calendar)
 54 | pZonedDateTimeQuoted = zonedDateTimePattern ps
 55 |   (\value => " " ++ IotaTime.Pattern.format pZoneIdQuoted
 56 |     (IotaTime.ZonedDateTime.zoneId value))
 57 |
 58 | public export
 59 | data ZonedDateTimePatternError providerError resolverError
 60 |   = ZonedDateTimeParseError PatternError
 61 |   | ZonedDateTimeProviderError providerError
 62 |   | ZonedDateTimeResolutionError resolverError
 63 |
 64 | zoneInfoPattern : {calendar : Type} ->
 65 |   {auto patterned : CalendarPattern calendar} ->
 66 |   Pattern state (CalendarDateTime calendar) ->
 67 |   Pattern zoneState String ->
 68 |   Pattern (state, zoneState) (CalendarDateTime calendar, String)
 69 | zoneInfoPattern local zone = pairPattern fst snd
 70 |   (\dateTime, zoneId => (dateTime, zoneId))
 71 |   (local <% char ' ') zone
 72 |
 73 | ||| Parse using explicit local date-time and zone-ID patterns, then load and
 74 | ||| resolve the captured zone. This lets protocols choose token or quoted zone
 75 | ||| syntax in advance.
 76 | public export
 77 | parseZonedDateTimePatternWith :
 78 |   {m : Type -> Type} -> Monad m =>
 79 |   {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
 80 |   Pattern state (CalendarDateTime calendar) ->
 81 |   Pattern zoneState String ->
 82 |   (String -> m (Either providerError TimeZone)) ->
 83 |   (CalendarDateTime calendar -> TimeZone ->
 84 |     Either resolverError (ZonedDateTime calendar)) ->
 85 |   String ->
 86 |   m (Either (ZonedDateTimePatternError providerError resolverError)
 87 |     (ZonedDateTime calendar))
 88 | parseZonedDateTimePatternWith local zone provider resolver source =
 89 |   case IotaTime.Pattern.parse (zoneInfoPattern local zone) source of
 90 |     Left error => pure (Left (ZonedDateTimeParseError error))
 91 |     Right (dateTime, zoneId) => do
 92 |       loaded <- provider zoneId
 93 |       pure $ case loaded of
 94 |         Left error => Left (ZonedDateTimeProviderError error)
 95 |         Right valueZone => case resolver dateTime valueZone of
 96 |           Left error => Left (ZonedDateTimeResolutionError error)
 97 |           Right value => Right value
 98 |
 99 | ||| Parse using a local date-time pattern, load the captured zone ID, and
100 | ||| resolve the local value according to the caller's chosen policy.
101 | ||| The provider effect is any `Monad`, allowing use from `IO`, effect
102 | ||| interpreters, or pure test monads.
103 | public export
104 | parseZonedDateTimeWith :
105 |   {m : Type -> Type} -> Monad m =>
106 |   {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
107 |   Pattern state (CalendarDateTime calendar) ->
108 |   (String -> m (Either providerError TimeZone)) ->
109 |   (CalendarDateTime calendar -> TimeZone ->
110 |     Either resolverError (ZonedDateTime calendar)) ->
111 |   String ->
112 |   m (Either (ZonedDateTimePatternError providerError resolverError)
113 |     (ZonedDateTime calendar))
114 | parseZonedDateTimeWith local provider resolver source =
115 |   parseZonedDateTimePatternWith local pZoneIdToken provider resolver source
116 |
117 | ||| Parse the standard ISO local date-time and zone-ID layout in the provider's
118 | ||| monad.
119 | public export
120 | parseStandardZonedDateTime :
121 |   {m : Type -> Type} -> Monad m =>
122 |   {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
123 |   (String -> m (Either providerError TimeZone)) ->
124 |   (CalendarDateTime calendar -> TimeZone ->
125 |     Either resolverError (ZonedDateTime calendar)) ->
126 |   String ->
127 |   m (Either (ZonedDateTimePatternError providerError resolverError)
128 |     (ZonedDateTime calendar))
129 | parseStandardZonedDateTime = parseZonedDateTimeWith ps