
  0 | module IotaTime.Tzdb.Metadata
  1 | 
  2 | %default total
  3 | 
  4 | ||| One TZDB link from an alias to its canonical zone identifier.
  5 | public export
  6 | record ZoneAlias where
  7 |   constructor MkZoneAlias
  8 |   aliasId : String
  9 |   canonicalId : String
 10 | 
 11 | ||| Version and identifier metadata associated with a time-zone provider.
 12 | public export
 13 | record TzdbMetadata where
 14 |   constructor MkTzdbMetadata
 15 |   tzdbVersion : Maybe String
 16 |   zoneAliases : List ZoneAlias
 17 | 
 18 | versionLine : List String -> Maybe String
 19 | versionLine ["#", "version", value] = Just value
 20 | versionLine _ = Nothing
 21 | 
 22 | aliasLine : List String -> Maybe ZoneAlias
 23 | aliasLine ["L", canonical, alias] = Just (MkZoneAlias alias canonical)
 24 | aliasLine _ = Nothing
 25 | 
 26 | firstJust : (value -> Maybe result) -> List value -> Maybe result
 27 | firstJust convert [] = Nothing
 28 | firstJust convert (value :: rest) = case convert value of
 29 |   Just result => Just result
 30 |   Nothing => firstJust convert rest
 31 | 
 32 | isWhitespace : Char -> Bool
 33 | isWhitespace ' ' = True
 34 | isWhitespace '\t' = True
 35 | isWhitespace _ = False
 36 | 
 37 | tokens : String -> List String
 38 | tokens source = go [] [] (unpack source)
 39 |   where
 40 |     finish : List Char -> List String -> List String
 41 |     finish [] found = reverse found
 42 |     finish current found = reverse (pack (reverse current) :: found)
 43 | 
 44 |     go : List Char -> List String -> List Char -> List String
 45 |     go current found [] = finish current found
 46 |     go current found (value :: rest) =
 47 |       if isWhitespace value
 48 |         then case current of
 49 |           [] => go [] found rest
 50 |           _ => go [] (pack (reverse current) :: found) rest
 51 |         else go (value :: current) found rest
 52 | 
 53 | sourceLines : String -> List String
 54 | sourceLines source = go [] (unpack source)
 55 |   where
 56 |     go : List Char -> List Char -> List String
 57 |     go current [] = [pack (reverse current)]
 58 |     go current ('\r' :: '\n' :: rest) =
 59 |       pack (reverse current) :: go [] rest
 60 |     go current ('\n' :: rest) = pack (reverse current) :: go [] rest
 61 |     go current (value :: rest) = go (value :: current) rest
 62 | 
 63 | ||| Parse the version declaration and Link records from a `tzdata.zi` file.
 64 | public export
 65 | parseTzdataIdentity : String -> (Maybe String, List ZoneAlias)
 66 | parseTzdataIdentity source =
 67 |   let tokenLines = map tokens (sourceLines source)
 68 |    in (firstJust versionLine tokenLines, mapMaybe aliasLine tokenLines)
 69 | 
 70 | findAlias : String -> List ZoneAlias -> Maybe String
 71 | findAlias value [] = Nothing
 72 | findAlias value (alias :: rest) =
 73 |   if alias.aliasId == value then Just alias.canonicalId
 74 |   else findAlias value rest
 75 | 
 76 | ||| Resolve a TZDB link chain. Cycles terminate after one pass over the aliases.
 77 | public export
 78 | canonicalZoneId : TzdbMetadata -> String -> String
 79 | canonicalZoneId metadata value = go (length metadata.zoneAliases) value
 80 |   where
 81 |     go : Nat -> String -> String
 82 |     go Z current = current
 83 |     go (S fuel) current = case findAlias current metadata.zoneAliases of
 84 |       Nothing => current
 85 |       Just canonical => go fuel canonical
 86 |