
   0 | module IotaTime.Pattern.Locale
   1 | 
   2 | import Data.String
   3 | import Data.String.Parser
   4 | import IotaTime.Locale
   5 | import IotaTime.Pattern
   6 | import IotaTime.Pattern.Calendar
   7 | import IotaTime.Pattern.CalendarDate
   8 | import IotaTime.Pattern.Offset
   9 | import IotaTime.Pattern.OffsetDateTime
  10 | import IotaTime.Pattern.LocalTime
  11 | import IotaTime.Calendar
  12 | import IotaTime.Calendar.Gregorian
  13 | import IotaTime.CalendarDateTime
  14 | import IotaTime.LocalTime
  15 | import IotaTime.Offset
  16 | import IotaTime.OffsetDateTime
  17 | import IotaTime.Period
  18 | import IotaTime.ZonedDateTime
  19 | 
  20 | %default total
  21 | 
  22 | ||| Failure to translate an operating-system `strftime` layout into a typed
  23 | ||| iotaTime pattern.
  24 | public export
  25 | data StrftimeError
  26 |   = UnsupportedSpecifier Char
  27 |   | DanglingPercent
  28 |   | MissingOffsetSpecifier
  29 |   | MissingZoneSpecifier
  30 | 
  31 | public export
  32 | Eq StrftimeError where
  33 |   UnsupportedSpecifier left == UnsupportedSpecifier right = left == right
  34 |   DanglingPercent == DanglingPercent = True
  35 |   MissingOffsetSpecifier == MissingOffsetSpecifier = True
  36 |   MissingZoneSpecifier == MissingZoneSpecifier = True
  37 |   _ == _ = False
  38 | 
  39 | public export
  40 | Show StrftimeError where
  41 |   show (UnsupportedSpecifier value) =
  42 |     "unsupported strftime specifier: %" ++ pack [value]
  43 |   show DanglingPercent = "strftime layout ends with a bare %"
  44 |   show MissingOffsetSpecifier = "strftime layout has no numeric %z offset"
  45 |   show MissingZoneSpecifier = "strftime layout has no %Z zone abbreviation"
  46 | 
  47 | data LayoutToken = LiteralToken Char | ConversionToken Char
  48 | 
  49 | data LayoutFragment = LiteralRun String | Conversion Char
  50 | 
  51 | compositeTokens : Char -> Maybe (List LayoutToken)
  52 | compositeTokens 'T' = Just
  53 |   [ ConversionToken 'H', LiteralToken ':', ConversionToken 'M'
  54 |   , LiteralToken ':', ConversionToken 'S'
  55 |   ]
  56 | compositeTokens 'R' = Just
  57 |   [ ConversionToken 'H', LiteralToken ':', ConversionToken 'M' ]
  58 | compositeTokens 'r' = Just
  59 |   [ ConversionToken 'I', LiteralToken ':', ConversionToken 'M'
  60 |   , LiteralToken ':', ConversionToken 'S', LiteralToken ' '
  61 |   , ConversionToken 'p'
  62 |   ]
  63 | compositeTokens 'F' = Just
  64 |   [ ConversionToken 'Y', LiteralToken '-', ConversionToken 'm'
  65 |   , LiteralToken '-', ConversionToken 'd'
  66 |   ]
  67 | compositeTokens 'D' = Just
  68 |   [ ConversionToken 'm', LiteralToken '/', ConversionToken 'd'
  69 |   , LiteralToken '/', ConversionToken 'y'
  70 |   ]
  71 | compositeTokens _ = Nothing
  72 | 
  73 | tokenize : List Char -> Either StrftimeError (List LayoutToken)
  74 | tokenize [] = Right []
  75 | tokenize ['%'] = Left DanglingPercent
  76 | tokenize ('%' :: specifier :: rest) = do
  77 |   suffix <- tokenize rest
  78 |   case specifier of
  79 |     '%' => Right (LiteralToken '%' :: suffix)
  80 |     'n' => Right (LiteralToken '\n' :: suffix)
  81 |     't' => Right (LiteralToken '\t' :: suffix)
  82 |     _ => case compositeTokens specifier of
  83 |       Just expansion => Right (expansion ++ suffix)
  84 |       Nothing => Right (ConversionToken specifier :: suffix)
  85 | tokenize (value :: rest) = map (LiteralToken value ::) (tokenize rest)
  86 | 
  87 | toFragments : List LayoutToken -> List LayoutFragment
  88 | toFragments = foldr step []
  89 |   where
  90 |     step : LayoutToken -> List LayoutFragment -> List LayoutFragment
  91 |     step (LiteralToken value) (LiteralRun text :: rest) =
  92 |       LiteralRun (pack [value] ++ text) :: rest
  93 |     step (LiteralToken value) rest = LiteralRun (pack [value]) :: rest
  94 |     step (ConversionToken value) rest = Conversion value :: rest
  95 | 
  96 | dateConversion : {calendar : Type} -> {auto patterned : CalendarPattern calendar} ->
  97 |                  Locale -> Char ->
  98 |                  Either StrftimeError
  99 |                    (Pattern DateFields (CalendarDate calendar))
 100 | dateConversion {calendar} locale 'Y' = Right (pyyyy {calendar})
 101 | dateConversion {calendar} locale 'y' = Right (pyy {calendar})
 102 | dateConversion {calendar} locale 'm' = Right (pMM {calendar})
 103 | dateConversion {calendar} locale 'd' = Right (pdd {calendar})
 104 | dateConversion {calendar} locale 'e' = Right (pdaySpace {calendar})
 105 | dateConversion {calendar} locale 'B' = Right (pMMMM' {calendar} locale)
 106 | dateConversion {calendar} locale 'b' = Right (pMMM' {calendar} locale)
 107 | dateConversion {calendar} locale 'h' = Right (pMMM' {calendar} locale)
 108 | dateConversion {calendar} locale 'A' = Right (pdddd' {calendar} locale)
 109 | dateConversion {calendar} locale 'a' = Right (pddd' {calendar} locale)
 110 | dateConversion _ value = Left (UnsupportedSpecifier value)
 111 | 
 112 | fragmentPattern : Pattern state value ->
 113 |                   (Char -> Either StrftimeError (Pattern state value)) ->
 114 |                   LayoutFragment -> Either StrftimeError (Pattern state value)
 115 | fragmentPattern template _ (LiteralRun text) =
 116 |   Right (literalField template text)
 117 | fragmentPattern _ conversion (Conversion value) = conversion value
 118 | 
 119 | assemble : Pattern state value ->
 120 |            (Char -> Either StrftimeError (Pattern state value)) ->
 121 |            List LayoutFragment -> Either StrftimeError (Pattern state value)
 122 | assemble template _ [] = Right (literalField template "")
 123 | assemble template conversion [fragment] =
 124 |   fragmentPattern template conversion fragment
 125 | assemble template conversion (fragment :: rest) = do
 126 |   first <- fragmentPattern template conversion fragment
 127 |   remaining <- assemble template conversion rest
 128 |   Right (first <+> remaining)
 129 | 
 130 | ||| Compile a calendar date pattern from a supported `strftime` layout.
 131 | ||| Locale month and weekday names are used for textual fields.
 132 | compileDatePattern : {default Gregorian calendar : Type} ->
 133 |                      {auto patterned : CalendarPattern calendar} ->
 134 |                      Locale -> String ->
 135 |                      Either StrftimeError
 136 |                        (Pattern DateFields (CalendarDate calendar))
 137 | compileDatePattern {calendar} locale layout = do
 138 |   tokens <- tokenize (unpack layout)
 139 |   assemble (pyyyy {calendar}) (dateConversion {calendar} locale)
 140 |     (toFragments tokens)
 141 | 
 142 | ||| Compile the operating system's preferred date layout for a calendar.
 143 | public export
 144 | localeDatePattern : {default Gregorian calendar : Type} ->
 145 |                     {auto patterned : CalendarPattern calendar} ->
 146 |                     Locale ->
 147 |                     Either StrftimeError
 148 |                       (Pattern DateFields (CalendarDate calendar))
 149 | localeDatePattern {calendar} locale =
 150 |   compileDatePattern {calendar} locale (rawDateFormat locale)
 151 | 
 152 | timeConversion : Locale -> Char ->
 153 |                  Either StrftimeError (Pattern TimeFields LocalTime)
 154 | timeConversion _ 'H' = Right pHH
 155 | timeConversion _ 'I' = Right phh
 156 | timeConversion _ 'l' = Right phhSpace
 157 | timeConversion _ 'M' = Right pmm
 158 | timeConversion _ 'S' = Right pss
 159 | timeConversion locale 'p' = Right (ppp' locale)
 160 | timeConversion _ value = Left (UnsupportedSpecifier value)
 161 | 
 162 | ||| Compile a local-time pattern from a supported `strftime` layout.
 163 | compileTimePattern : Locale -> String ->
 164 |                      Either StrftimeError (Pattern TimeFields LocalTime)
 165 | compileTimePattern locale layout = do
 166 |   tokens <- tokenize (unpack layout)
 167 |   assemble pHH (timeConversion locale) (toFragments tokens)
 168 | 
 169 | ||| Compile the operating system's preferred local-time layout.
 170 | public export
 171 | localeTimePattern : Locale ->
 172 |                     Either StrftimeError (Pattern TimeFields LocalTime)
 173 | localeTimePattern locale = compileTimePattern locale (rawTimeFormat locale)
 174 | 
 175 | ||| Parser state for a combined calendar date and local-time pattern.
 176 | export
 177 | record DateTimeFieldsRep where
 178 |   constructor MkDateTimeFields
 179 |   parsedDateFields : DateFields
 180 |   parsedTimeFields : TimeFields
 181 | 
 182 | ||| Opaque parser state for combined calendar date and local-time patterns.
 183 | public export
 184 | DateTimeFields : Type
 185 | DateTimeFields = DateTimeFieldsRep
 186 | 
 187 | ||| Combine date and time seeds for `parseWith` on a partial date-time pattern.
 188 | public export
 189 | dateTimeFields : DateFields -> TimeFields -> DateTimeFields
 190 | dateTimeFields = MkDateTimeFields
 191 | 
 192 | initialDateTimeFields : {calendar : Type} ->
 193 |                         {auto patterned : CalendarPattern calendar} ->
 194 |                         DateTimeFields
 195 | initialDateTimeFields {calendar} = dateTimeFields
 196 |   (patternInitialState (pyyyy {calendar})) (patternInitialState pHH)
 197 | 
 198 | finishDateTime : {calendar : Type} ->
 199 |                  {auto patterned : CalendarPattern calendar} ->
 200 |                  DateTimeFields ->
 201 |                  Either PatternError (CalendarDateTime calendar)
 202 | finishDateTime {calendar} fields = do
 203 |   date <- patternFinish (pyyyy {calendar}) fields.parsedDateFields
 204 |   time <- patternFinish pHH fields.parsedTimeFields
 205 |   Right (on time date)
 206 | 
 207 | liftDateUpdate : (DateFields -> DateFields) ->
 208 |                  DateTimeFields -> DateTimeFields
 209 | liftDateUpdate update fields =
 210 |   { parsedDateFields := update fields.parsedDateFields } fields
 211 | 
 212 | liftTimeUpdate : (TimeFields -> TimeFields) ->
 213 |                  DateTimeFields -> DateTimeFields
 214 | liftTimeUpdate update fields =
 215 |   { parsedTimeFields := update fields.parsedTimeFields } fields
 216 | 
 217 | liftDatePattern : {calendar : Type} ->
 218 |                   {auto patterned : CalendarPattern calendar} ->
 219 |                   Pattern DateFields (CalendarDate calendar) ->
 220 |                   Pattern DateTimeFields (CalendarDateTime calendar)
 221 | liftDatePattern {calendar} pattern = MkPattern
 222 |   (initialDateTimeFields {calendar})
 223 |   (finishDateTime {calendar})
 224 |   (map (map liftDateUpdate) (patternParsePart pattern))
 225 |   (patternFormatPart pattern . datePart)
 226 | 
 227 | liftTimePattern : {calendar : Type} ->
 228 |                   {auto patterned : CalendarPattern calendar} ->
 229 |                   Pattern TimeFields LocalTime ->
 230 |                   Pattern DateTimeFields (CalendarDateTime calendar)
 231 | liftTimePattern {calendar} pattern = MkPattern
 232 |   (initialDateTimeFields {calendar})
 233 |   (finishDateTime {calendar})
 234 |   (map (map liftTimeUpdate) (patternParsePart pattern))
 235 |   (patternFormatPart pattern . localTimeOfDay)
 236 | 
 237 | dateTimeConversion : {calendar : Type} ->
 238 |                      {auto patterned : CalendarPattern calendar} ->
 239 |                      Locale -> Char ->
 240 |                      Either StrftimeError
 241 |                        (Pattern DateTimeFields (CalendarDateTime calendar))
 242 | dateTimeConversion {calendar} locale value =
 243 |   case dateConversion {calendar} locale value of
 244 |     Right pattern => Right (liftDatePattern {calendar} pattern)
 245 |     Left (UnsupportedSpecifier _) =>
 246 |       map (liftTimePattern {calendar}) (timeConversion locale value)
 247 |     Left error => Left error
 248 | 
 249 | isZoneSpecifier : Char -> Bool
 250 | isZoneSpecifier value = value == 'Z' || value == 'z'
 251 | 
 252 | trimTrailingSpaces : String -> String
 253 | trimTrailingSpaces = pack . reverse . dropSpaces . reverse . unpack
 254 |   where
 255 |     dropSpaces : List Char -> List Char
 256 |     dropSpaces (' ' :: rest) = dropSpaces rest
 257 |     dropSpaces values = values
 258 | 
 259 | stripZones : List LayoutFragment -> List LayoutFragment
 260 | stripZones [] = []
 261 | stripZones (LiteralRun text :: Conversion value :: rest) =
 262 |   if isZoneSpecifier value
 263 |     then let trimmed = trimTrailingSpaces text in
 264 |       if trimmed == ""
 265 |         then stripZones rest
 266 |         else LiteralRun trimmed :: stripZones rest
 267 |     else LiteralRun text :: stripZones (Conversion value :: rest)
 268 | stripZones (LiteralRun text :: rest) =
 269 |   LiteralRun text :: stripZones rest
 270 | stripZones (Conversion value :: rest) =
 271 |   if isZoneSpecifier value
 272 |     then stripZones rest
 273 |     else Conversion value :: stripZones rest
 274 | 
 275 | ||| Compile a calendar-local date-time pattern from a supported `strftime`
 276 | ||| layout. Zone specifiers are omitted because this pattern has no zone value.
 277 | compileDateTimePattern : {default Gregorian calendar : Type} ->
 278 |                          {auto patterned : CalendarPattern calendar} ->
 279 |                          Locale -> String ->
 280 |                          Either StrftimeError
 281 |                            (Pattern DateTimeFields
 282 |                              (CalendarDateTime calendar))
 283 | compileDateTimePattern {calendar} locale layout = do
 284 |   tokens <- tokenize (unpack layout)
 285 |   assemble (liftDatePattern {calendar} (pyyyy {calendar}))
 286 |     (dateTimeConversion {calendar} locale)
 287 |     (stripZones (toFragments tokens))
 288 | 
 289 | ||| Compile the operating system's preferred local date-time layout for a calendar.
 290 | public export
 291 | localeDateTimePattern : {default Gregorian calendar : Type} ->
 292 |                         {auto patterned : CalendarPattern calendar} ->
 293 |                         Locale ->
 294 |                         Either StrftimeError
 295 |                           (Pattern DateTimeFields
 296 |                             (CalendarDateTime calendar))
 297 | localeDateTimePattern {calendar} locale =
 298 |   compileDateTimePattern {calendar} locale (rawDateTimeFormat locale)
 299 | 
 300 | trailingLiterals : List LayoutFragment -> Either StrftimeError String
 301 | trailingLiterals [] = Right ""
 302 | trailingLiterals (LiteralRun text :: rest) =
 303 |   map (text ++) (trailingLiterals rest)
 304 | trailingLiterals (Conversion value :: rest) =
 305 |   Left (UnsupportedSpecifier value)
 306 | 
 307 | splitOffset : List LayoutFragment ->
 308 |               Either StrftimeError (List LayoutFragment, String)
 309 | splitOffset [] = Left MissingOffsetSpecifier
 310 | splitOffset (Conversion 'z' :: rest) =
 311 |   map (\trailing => ([], trailing)) (trailingLiterals rest)
 312 | splitOffset (fragment :: rest) = do
 313 |   (before, trailing) <- splitOffset rest
 314 |   Right (fragment :: before, trailing)
 315 | 
 316 | ||| Compile an offset date-time layout containing a numeric `%z` field.
 317 | compileOffsetDateTimePattern : {default Gregorian calendar : Type} ->
 318 |   {auto patterned : CalendarPattern calendar} -> Locale -> String ->
 319 |   Either StrftimeError
 320 |     (Pattern (DateTimeFields, Offset) (OffsetDateTime calendar))
 321 | compileOffsetDateTimePattern {calendar} locale layout = do
 322 |   tokens <- tokenize (unpack layout)
 323 |   (before, trailing) <- splitOffset (toFragments tokens)
 324 |   localPattern <- assemble (liftDatePattern {calendar} (pyyyy {calendar}))
 325 |     (dateTimeConversion {calendar} locale) before
 326 |   Right (offsetDateTimePattern localPattern
 327 |     (pOffsetCompact <% string trailing))
 328 | 
 329 | ||| Compile the operating system's preferred offset date-time layout for a calendar.
 330 | public export
 331 | localeOffsetDateTimePattern : {default Gregorian calendar : Type} ->
 332 |   {auto patterned : CalendarPattern calendar} -> Locale ->
 333 |   Either StrftimeError
 334 |     (Pattern (DateTimeFields, Offset) (OffsetDateTime calendar))
 335 | localeOffsetDateTimePattern {calendar} locale =
 336 |   compileOffsetDateTimePattern {calendar} locale (rawDateTimeFormat locale)
 337 | 
 338 | ||| Errors from layout compilation, local parsing, zone loading, or local-time
 339 | ||| resolution while parsing a zoned date-time.
 340 | public export
 341 | data ZonedPatternError providerError resolverError
 342 |   = ZonedLayoutError StrftimeError
 343 |   | ZonedParseError PatternError
 344 |   | ZonedProviderError providerError
 345 |   | ZonedResolutionError resolverError
 346 | 
 347 | stripPrefix : List Char -> List Char -> Maybe (List Char)
 348 | stripPrefix [] values = Just values
 349 | stripPrefix (expected :: expectedRest) (actual :: values) =
 350 |   if expected == actual then stripPrefix expectedRest values else Nothing
 351 | stripPrefix _ _ = Nothing
 352 | 
 353 | removeSuffix : List Char -> List Char -> Maybe (List Char)
 354 | removeSuffix values suffix =
 355 |   map reverse (stripPrefix (reverse suffix) (reverse values))
 356 | 
 357 | isZoneCharacter : Char -> Bool
 358 | isZoneCharacter value =
 359 |   value /= ' ' && value /= '\t' && value /= '\n' && value /= '\r'
 360 | 
 361 | zoneTokenPattern : String -> Pattern String String
 362 | zoneTokenPattern trailing = MkPattern
 363 |   ""
 364 |   Right
 365 |   (Parser.P (\state =>
 366 |     let remaining = strSubstr state.pos (state.maxPos - state.pos) state.input in
 367 |     case removeSuffix (unpack remaining) (unpack trailing) of
 368 |       Nothing => pure (Parser.Fail state.pos "zone abbreviation")
 369 |       Just [] => pure (Parser.Fail state.pos "zone abbreviation")
 370 |       Just token => if all isZoneCharacter token
 371 |         then pure (Parser.OK (Right (const (pack token)))
 372 |           ({ pos := state.maxPos } state))
 373 |         else pure (Parser.Fail state.pos "zone abbreviation")))
 374 |   id
 375 | 
 376 | splitZone : List LayoutFragment ->
 377 |             Either StrftimeError (List LayoutFragment, String)
 378 | splitZone [] = Left MissingZoneSpecifier
 379 | splitZone (Conversion 'Z' :: rest) =
 380 |   map (\trailing => ([], trailing)) (trailingLiterals rest)
 381 | splitZone (fragment :: rest) = do
 382 |   (before, trailing) <- splitZone rest
 383 |   Right (fragment :: before, trailing)
 384 | 
 385 | zoneInfoPattern : {calendar : Type} ->
 386 |   {auto patterned : CalendarPattern calendar} -> Locale -> String ->
 387 |   Either StrftimeError
 388 |     (Pattern (DateTimeFields, String) (CalendarDateTime calendar, String))
 389 | zoneInfoPattern {calendar} locale layout = do
 390 |   tokens <- tokenize (unpack layout)
 391 |   (before, trailing) <- splitZone (toFragments tokens)
 392 |   localPattern <- assemble (liftDatePattern {calendar} (pyyyy {calendar}))
 393 |     (dateTimeConversion {calendar} locale) before
 394 |   Right (pairPattern fst snd (\local, zone => (local, zone))
 395 |     localPattern (zoneTokenPattern trailing))
 396 | 
 397 | ||| Parse a locale %Z layout, load the captured zone in any `Monad`, and resolve
 398 | ||| local time.
 399 | public export
 400 | parseZonedDateTime :
 401 |   {default Gregorian calendar : Type} ->
 402 |   {auto patterned : CalendarPattern calendar} ->
 403 |   {m : Type -> Type} -> Monad m =>
 404 |   (String -> m (Either providerError TimeZone)) ->
 405 |   (CalendarDateTime calendar -> TimeZone ->
 406 |     Either resolverError (ZonedDateTime calendar)) ->
 407 |   Locale -> String ->
 408 |   m (Either (ZonedPatternError providerError resolverError)
 409 |     (ZonedDateTime calendar))
 410 | parseZonedDateTime {calendar} provider resolver locale source =
 411 |   case zoneInfoPattern {calendar} locale (rawDateTimeFormat locale) of
 412 |     Left error => pure (Left (ZonedLayoutError error))
 413 |     Right pattern => case IotaTime.Pattern.parse pattern source of
 414 |       Left error => pure (Left (ZonedParseError error))
 415 |       Right (local, zoneToken) => do
 416 |         loaded <- provider zoneToken
 417 |         pure $ case loaded of
 418 |           Left error => Left (ZonedProviderError error)
 419 |           Right zone => case resolver local zone of
 420 |             Left error => Left (ZonedResolutionError error)
 421 |             Right value => Right value
 422 |