0 | module IotaTime.Tzdb.Tzif
2 | import public Data.Bits
3 | import public IotaTime.TimeZone.Core
5 | import Derive.Prelude
7 | %language ElabReflection
12 | data TzifVersion = Version1 | Version2 | Version3 | Version4
14 | %runElab derive `{TzifVersion
} [Eq]
20 | | UnsupportedVersion Bits8
21 | | InvalidSecondHeader
22 | | MissingTransitionType
23 | | InvalidTransitionTypeIndex Integer
24 | | InvalidAbbreviationIndex Integer
25 | | UnterminatedAbbreviation Integer
26 | | InvalidUtcOffset Integer
31 | record TzifData where
32 | constructor MkTzifData
33 | version : TzifVersion
34 | initialTransition : TransitionInfo
35 | transitions : List (Instant, TransitionInfo)
36 | posixFooter : Maybe String
39 | constructor MkHeader
40 | headerVersion : TzifVersion
44 | transitionCount : Nat
46 | abbreviationCount : Nat
48 | record RawType where
49 | constructor MkRawType
52 | rawAbbreviationIndex : Integer
54 | takeBytes : Nat -> List Bits8 -> Either TzifError (List Bits8, List Bits8)
55 | takeBytes Z bytes = Right ([], bytes)
56 | takeBytes (S count) [] = Left UnexpectedEnd
57 | takeBytes (S count) (byte :: bytes) = do
58 | (taken, remaining) <- takeBytes count bytes
59 | Right (byte :: taken, remaining)
61 | byteValue : Bits8 -> Integer
64 | unsignedBigEndian : List Bits8 -> Integer
65 | unsignedBigEndian = foldl (\value, byte => value * 256 + byteValue byte) 0
67 | signedBigEndian : Nat -> List Bits8 -> Integer
68 | signedBigEndian width bytes =
69 | let unsigned = unsignedBigEndian bytes
70 | in let signBoundary = power 2 (pred (8 * width))
71 | in let modulus = power 2 (8 * width)
72 | in if unsigned >= signBoundary then unsigned - modulus else unsigned
74 | power : Integer -> Nat -> Integer
76 | power base (S exponent) = base * power base exponent
78 | readUnsigned32 : List Bits8 -> Either TzifError (Integer, List Bits8)
79 | readUnsigned32 bytes = do
80 | (value, remaining) <- takeBytes 4 bytes
81 | Right (unsignedBigEndian value, remaining)
83 | readSigned : Nat -> List Bits8 -> Either TzifError (Integer, List Bits8)
84 | readSigned width bytes = do
85 | (value, remaining) <- takeBytes width bytes
86 | Right (signedBigEndian width value, remaining)
88 | readCounts : List Bits8 -> Either TzifError
89 | ((Nat, Nat, Nat, Nat, Nat, Nat), List Bits8)
90 | readCounts bytes = do
91 | (gmt, afterGmt) <- readUnsigned32 bytes
92 | (standard, afterStandard) <- readUnsigned32 afterGmt
93 | (leaps, afterLeaps) <- readUnsigned32 afterStandard
94 | (transitions, afterTransitions) <- readUnsigned32 afterLeaps
95 | (types, afterTypes) <- readUnsigned32 afterTransitions
96 | (abbreviations, remaining) <- readUnsigned32 afterTypes
97 | Right ((cast gmt, cast standard, cast leaps, cast transitions,
98 | cast types, cast abbreviations), remaining)
100 | parseVersion : Bits8 -> Either TzifError TzifVersion
101 | parseVersion 0 = Right Version1
102 | parseVersion 49 = Right Version1
103 | parseVersion 50 = Right Version2
104 | parseVersion 51 = Right Version3
105 | parseVersion 52 = Right Version4
106 | parseVersion value = Left (UnsupportedVersion value)
108 | parseHeader : List Bits8 -> Either TzifError (Header, List Bits8)
109 | parseHeader bytes = do
110 | (magic, afterMagic) <- takeBytes 4 bytes
111 | if magic /= [84, 90, 105, 102]
112 | then Left InvalidMagic
114 | (versionByte, afterVersion) <- case the (List Bits8) afterMagic of
115 | [] => Left UnexpectedEnd
116 | value :: rest => Right (value, rest)
117 | parsedVersion <- parseVersion versionByte
118 | (_, afterReserved) <- takeBytes 15 afterVersion
119 | ((gmt, standard, leaps, transitionValues, types, abbreviations), remaining) <-
120 | readCounts afterReserved
121 | Right (MkHeader parsedVersion gmt standard leaps transitionValues
122 | types abbreviations, remaining)
124 | readManySigned : Nat -> Nat -> List Bits8 ->
125 | Either TzifError (List Integer, List Bits8)
126 | readManySigned Z width bytes = Right ([], bytes)
127 | readManySigned (S count) width bytes = do
128 | (value, afterValue) <- readSigned width bytes
129 | (values, remaining) <- readManySigned count width afterValue
130 | Right (value :: values, remaining)
132 | readManyBytes : Nat -> List Bits8 -> Either TzifError (List Integer, List Bits8)
133 | readManyBytes count bytes = do
134 | (values, remaining) <- takeBytes count bytes
135 | Right (map byteValue values, remaining)
137 | readRawTypes : Nat -> List Bits8 -> Either TzifError (List RawType, List Bits8)
138 | readRawTypes Z bytes = Right ([], bytes)
139 | readRawTypes (S count) bytes = do
140 | (offset, afterOffset) <- readSigned 4 bytes
141 | (inDst, abbreviationIndex, afterType) <-
142 | case the (List Bits8) afterOffset of
143 | dst :: index :: rest => Right (dst /= 0, byteValue index, rest)
144 | _ => Left UnexpectedEnd
145 | (types, remaining) <- readRawTypes count afterType
146 | Right (MkRawType offset inDst abbreviationIndex :: types, remaining)
148 | indexList : Integer -> List element -> Maybe element
149 | indexList index values = if index < 0 then Nothing else go (cast index) values
151 | go : Nat -> List element -> Maybe element
152 | go Z (value :: _) = Just value
153 | go (S index) (_ :: rest) = go index rest
156 | abbreviationAt : Integer -> List Bits8 -> Either TzifError String
157 | abbreviationAt index bytes = case indexList index bytes of
158 | Nothing => Left (InvalidAbbreviationIndex index)
159 | Just _ => collect (drop (cast index) bytes)
161 | collect : List Bits8 -> Either TzifError String
162 | collect [] = Left (UnterminatedAbbreviation index)
163 | collect (0 :: _) = Right ""
164 | collect (byte :: rest) = map (strCons (cast byte)) (collect rest)
166 | toTransitionInfo : List Bits8 -> RawType -> Either TzifError TransitionInfo
167 | toTransitionInfo abbreviations raw = do
168 | valueOffset <- case refineOffsetSeconds raw.rawOffset of
169 | Left _ => Left (InvalidUtcOffset raw.rawOffset)
170 | Right offset => Right offset
171 | valueAbbreviation <- abbreviationAt raw.rawAbbreviationIndex abbreviations
172 | Right (transitionInfo valueOffset raw.rawInDst valueAbbreviation)
174 | chooseInitial : List (RawType, TransitionInfo) -> Either TzifError TransitionInfo
175 | chooseInitial [] = Left MissingTransitionType
176 | chooseInitial values@((_, first) :: _) = Right (findStandard values first)
178 | findStandard : List (RawType, TransitionInfo) -> TransitionInfo -> TransitionInfo
179 | findStandard [] fallback = fallback
180 | findStandard ((raw, info) :: rest) fallback =
181 | if raw.rawInDst then findStandard rest fallback else info
183 | buildTransitions : List Integer -> List Integer -> List TransitionInfo ->
184 | Either TzifError (List (Instant, TransitionInfo))
185 | buildTransitions [] [] types = Right []
186 | buildTransitions (instant :: instants) (index :: indices) types = do
187 | info <- case indexList index types of
188 | Nothing => Left (InvalidTransitionTypeIndex index)
189 | Just value => Right value
190 | remaining <- buildTransitions instants indices types
191 | Right ((fromSecondsSinceUnixEpoch instant, info) :: remaining)
192 | buildTransitions _ _ _ = Left UnexpectedEnd
194 | annotateSavings : Maybe Offset -> List (Instant, TransitionInfo) ->
195 | List (Instant, TransitionInfo)
196 | annotateSavings standardOffset [] = []
197 | annotateSavings standardOffset ((instant, info) :: rest) =
198 | if isDaylightSavingTime info
199 | then let annotated = case standardOffset of
201 | Just standard => transitionInfoWithSavings (utcOffset info)
202 | (minusClamped (utcOffset info) standard) (abbreviation info)
203 | in (instant, annotated) :: annotateSavings standardOffset rest
204 | else let annotated = transitionInfoWithSavings
205 | (utcOffset info) IotaTime.Offset.empty (abbreviation info)
206 | in (instant, annotated) ::
207 | annotateSavings (Just (utcOffset info)) rest
209 | parsePayload : Nat -> Header -> List Bits8 ->
210 | Either TzifError ((TransitionInfo, List (Instant, TransitionInfo)),
212 | parsePayload width header bytes = do
213 | (instants, afterInstants) <- readManySigned header.transitionCount width bytes
214 | (indices, afterIndices) <- readManyBytes header.transitionCount afterInstants
215 | (rawTypes, afterTypes) <- readRawTypes header.typeCount afterIndices
216 | (abbreviations, afterAbbreviations) <- takeBytes header.abbreviationCount afterTypes
217 | (_, remaining) <- takeBytes
218 | (header.leapCount * (width + 4) + header.isStdCount + header.isGmtCount)
220 | infos <- traverse (toTransitionInfo abbreviations) rawTypes
221 | initial <- chooseInitial (zip rawTypes infos)
222 | parsedTransitions <- buildTransitions instants indices infos
223 | let initialStandard = if isDaylightSavingTime initial
225 | else Just (utcOffset initial)
226 | Right ((initial, annotateSavings initialStandard parsedTransitions), remaining)
228 | skipPayload : Nat -> Header -> List Bits8 -> Either TzifError (List Bits8)
229 | skipPayload width header bytes = do
230 | let size = header.transitionCount * width + header.transitionCount +
231 | header.typeCount * 6 + header.abbreviationCount +
232 | header.leapCount * (width + 4) + header.isStdCount + header.isGmtCount
233 | (_, remaining) <- takeBytes size bytes
236 | bytesToString : List Bits8 -> String
237 | bytesToString = pack . map cast
239 | parseFooter : List Bits8 -> Either TzifError (Maybe String)
240 | parseFooter [] = Right Nothing
241 | parseFooter (10 :: rest) = case reverse rest of
242 | 10 :: reversedFooter => Right (Just (bytesToString (reverse reversedFooter)))
243 | _ => Left InvalidFooter
244 | parseFooter _ = Left InvalidFooter
249 | parseTzif : List Bits8 -> Either TzifError TzifData
250 | parseTzif bytes = do
251 | (firstHeader, afterFirstHeader) <- parseHeader bytes
252 | case firstHeader.headerVersion of
254 | ((initial, parsedTransitions), remaining) <-
255 | parsePayload 4 firstHeader afterFirstHeader
257 | [] => Right (MkTzifData Version1 initial parsedTransitions Nothing)
258 | _ => Left TrailingData
259 | expectedVersion => do
260 | afterFirstPayload <- skipPayload 4 firstHeader afterFirstHeader
261 | (secondHeader, afterSecondHeader) <- parseHeader afterFirstPayload
262 | if secondHeader.headerVersion /= expectedVersion
263 | then Left InvalidSecondHeader
265 | ((initial, parsedTransitions), remaining) <-
266 | parsePayload 8 secondHeader afterSecondHeader
267 | footer <- parseFooter remaining
268 | Right (MkTzifData expectedVersion initial parsedTransitions footer)