
   0 | module IotaTime.Tzdb.Windows
   1 | 
   2 | import IotaTime.Internal.Gregorian
   3 | import IotaTime.TimeZone.Core
   4 | import IotaTime.Tzdb.Windows.Types
   5 | import Data.String
   6 | 
   7 | %default total
   8 | 
   9 | byteValue : Bits8 -> Integer
  10 | byteValue = cast
  11 | 
  12 | unsignedLittleEndian : List Bits8 -> Integer
  13 | unsignedLittleEndian = go 1
  14 |   where
  15 |     go : Integer -> List Bits8 -> Integer
  16 |     go multiplier [] = 0
  17 |     go multiplier (byte :: rest) =
  18 |       byteValue byte * multiplier + go (multiplier * 256) rest
  19 | 
  20 | signedLittleEndian32 : List Bits8 -> Integer
  21 | signedLittleEndian32 bytes =
  22 |   let unsigned = unsignedLittleEndian bytes
  23 |    in if unsigned >= 2147483648 then unsigned - 4294967296 else unsigned
  24 | 
  25 | takeBytes : Nat -> List Bits8 -> Maybe (List Bits8, List Bits8)
  26 | takeBytes Z bytes = Just ([], bytes)
  27 | takeBytes (S count) [] = Nothing
  28 | takeBytes (S count) (byte :: rest) = do
  29 |   (taken, remaining) <- takeBytes count rest
  30 |   Just (byte :: taken, remaining)
  31 | 
  32 | readLittleEndian : Nat -> List Bits8 -> Maybe (Integer, List Bits8)
  33 | readLittleEndian width bytes = do
  34 |   (value, remaining) <- takeBytes width bytes
  35 |   Just (unsignedLittleEndian value, remaining)
  36 | 
  37 | readSigned32 : List Bits8 -> Maybe (Integer, List Bits8)
  38 | readSigned32 bytes = do
  39 |   (value, remaining) <- takeBytes 4 bytes
  40 |   Just (signedLittleEndian32 value, remaining)
  41 | 
  42 | prefixValue : List Char -> String -> Maybe String
  43 | prefixValue expectedPrefix source = map pack (strip expectedPrefix (unpack source))
  44 |   where
  45 |     strip : List Char -> List Char -> Maybe (List Char)
  46 |     strip [] remaining = Just remaining
  47 |     strip (expected :: rest) (actual :: remaining) =
  48 |       if expected == actual then strip rest remaining else Nothing
  49 |     strip _ _ = Nothing
  50 | 
  51 | hexDigit : Char -> Maybe Integer
  52 | hexDigit value =
  53 |   if value >= '0' && value <= '9' then Just (cast value - cast '0')
  54 |   else if value >= 'a' && value <= 'f' then Just (cast value - cast 'a' + 10)
  55 |   else if value >= 'A' && value <= 'F' then Just (cast value - cast 'A' + 10)
  56 |   else Nothing
  57 | 
  58 | hexBytes : String -> Maybe (List Bits8)
  59 | hexBytes source = go (unpack source)
  60 |   where
  61 |     go : List Char -> Maybe (List Bits8)
  62 |     go [] = Just []
  63 |     go (high :: low :: rest) = do
  64 |       highValue <- hexDigit high
  65 |       lowValue <- hexDigit low
  66 |       remaining <- go rest
  67 |       Just (cast (highValue * 16 + lowValue) :: remaining)
  68 |     go _ = Nothing
  69 | 
  70 | dynamicLine : String -> Maybe (Integer, List Bits8)
  71 | dynamicLine source = do
  72 |   value <- prefixValue ['D', 'Y', 'N', 'A', 'M', 'I', 'C', '\t'] source
  73 |   parseYear [] (unpack value)
  74 |   where
  75 |     decimalDigits : List Char -> Maybe Integer
  76 |     decimalDigits [] = Nothing
  77 |     decimalDigits digits = go 0 digits
  78 |       where
  79 |         go : Integer -> List Char -> Maybe Integer
  80 |         go value [] = Just value
  81 |         go value (digit :: rest) = if digit >= '0' && digit <= '9'
  82 |           then go (value * 10 + cast digit - cast '0') rest
  83 |           else Nothing
  84 | 
  85 |     parseYear : List Char -> List Char -> Maybe (Integer, List Bits8)
  86 |     parseYear digits ('\t' :: encoded) = do
  87 |       year <- decimalDigits (reverse digits)
  88 |       bytes <- hexBytes (pack encoded)
  89 |       Just (year, bytes)
  90 |     parseYear digits (value :: rest) = parseYear (value :: digits) rest
  91 |     parseYear _ [] = Nothing
  92 | 
  93 | parseDynamicLines : List String -> Either WindowsRegistryProtocolError
  94 |   (List (Integer, List Bits8), List String)
  95 | parseDynamicLines [] = Left IncompleteRegistryZone
  96 | parseDynamicLines ("END" :: rest) = Right ([], rest)
  97 | parseDynamicLines (line :: rest) = case dynamicLine line of
  98 |   Nothing => Left (InvalidDynamicRegistryLine line)
  99 |   Just value => do
 100 |     (remainingValues, remainingLines) <- parseDynamicLines rest
 101 |     Right (value :: remainingValues, remainingLines)
 102 | 
 103 | parseRegistryZone : List String -> Either WindowsRegistryProtocolError
 104 |   (WindowsRegistryZone, List String)
 105 | parseRegistryZone (idLine :: standardLine :: daylightLine :: tziLine :: rest) = do
 106 |   zoneId <- maybe (Left (UnexpectedRegistryLine idLine)) Right
 107 |     (prefixValue ['I', 'D', '\t'] idLine)
 108 |   standardName <- maybe (Left (UnexpectedRegistryLine standardLine)) Right
 109 |     (prefixValue ['S', 'T', 'D', '\t'] standardLine)
 110 |   daylightName <- maybe (Left (UnexpectedRegistryLine daylightLine)) Right
 111 |     (prefixValue ['D', 'S', 'T', '\t'] daylightLine)
 112 |   encoded <- maybe (Left (UnexpectedRegistryLine tziLine)) Right
 113 |     (prefixValue ['T', 'Z', 'I', '\t'] tziLine)
 114 |   defaultTzi <- maybe (Left (InvalidRegistryHex encoded)) Right
 115 |     (hexBytes encoded)
 116 |   (dynamicTzi, remaining) <- parseDynamicLines rest
 117 |   Right (MkWindowsRegistryZone zoneId standardName daylightName
 118 |     defaultTzi dynamicTzi, remaining)
 119 | parseRegistryZone _ = Left IncompleteRegistryZone
 120 | 
 121 | parseRegistryZones : List String -> Either WindowsRegistryProtocolError
 122 |   (List WindowsRegistryZone)
 123 | parseRegistryZones [] = Right []
 124 | parseRegistryZones ("ZONE" :: rest) = do
 125 |   (zone, remaining) <- parseRegistryZone rest
 126 |   zones <- assert_total (parseRegistryZones remaining)
 127 |   Right (zone :: zones)
 128 | parseRegistryZones (line :: _) = Left (UnexpectedRegistryLine line)
 129 | 
 130 | ||| Parse the strict protocol produced by the Windows command adapter.
 131 | public export
 132 | parseWindowsRegistrySnapshot : String ->
 133 |   Either WindowsRegistryProtocolError WindowsRegistrySnapshot
 134 | parseWindowsRegistrySnapshot source = case lines source of
 135 |   [] => Left MissingLocalZoneId
 136 |   localLine :: rest => case prefixValue ['L', 'O', 'C', 'A', 'L', '\t'] localLine of
 137 |     Nothing => Left MissingLocalZoneId
 138 |     Just "" => Left MissingLocalZoneId
 139 |     Just localZoneId => map (MkWindowsRegistrySnapshot localZoneId)
 140 |       (parseRegistryZones rest)
 141 | 
 142 | readTransitionDate : List Bits8 -> Maybe
 143 |   (WindowsTransitionDate, Integer, List Bits8)
 144 | readTransitionDate bytes = do
 145 |   (year, afterYear) <- readLittleEndian 2 bytes
 146 |   (month, afterMonth) <- readLittleEndian 2 afterYear
 147 |   (weekday, afterWeekday) <- readLittleEndian 2 afterMonth
 148 |   (week, afterWeek) <- readLittleEndian 2 afterWeekday
 149 |   (hour, afterHour) <- readLittleEndian 2 afterWeek
 150 |   (minute, afterMinute) <- readLittleEndian 2 afterHour
 151 |   (second, afterSecond) <- readLittleEndian 2 afterMinute
 152 |   (milliseconds, remaining) <- readLittleEndian 2 afterSecond
 153 |   Just (MkWindowsTransitionDate year month week weekday hour minute second,
 154 |     milliseconds, remaining)
 155 | 
 156 | ||| Decode a binary Windows REG_TZI_FORMAT value. Display names are stored in
 157 | ||| separate registry values and are supplied explicitly.
 158 | public export
 159 | parseWindowsTzi : String -> String -> List Bits8 ->
 160 |                   Either WindowsZoneError WindowsZoneRule
 161 | parseWindowsTzi standardName daylightName bytes =
 162 |   if length bytes /= 44
 163 |     then Left (WindowsTziLength (cast (length bytes)))
 164 |     else case decode bytes of
 165 |       Nothing => Left (WindowsTziLength (cast (length bytes)))
 166 |       Just (bias, standardBias, daylightBias,
 167 |             standardDate, standardMilliseconds,
 168 |             daylightDate, daylightMilliseconds) =>
 169 |         if standardMilliseconds /= 0
 170 |           then Left (WindowsTransitionMillisecondsUnsupported
 171 |             standardMilliseconds)
 172 |         else if daylightMilliseconds /= 0
 173 |           then Left (WindowsTransitionMillisecondsUnsupported
 174 |             daylightMilliseconds)
 175 |         else Right (MkWindowsZoneRule bias standardBias daylightBias
 176 |           standardName daylightName daylightDate standardDate)
 177 |   where
 178 |     decode : List Bits8 -> Maybe
 179 |       (Integer, Integer, Integer, WindowsTransitionDate, Integer,
 180 |        WindowsTransitionDate, Integer)
 181 |     decode source = do
 182 |       (bias, afterBias) <- readSigned32 source
 183 |       (standardBias, afterStandardBias) <- readSigned32 afterBias
 184 |       (daylightBias, afterDaylightBias) <- readSigned32 afterStandardBias
 185 |       (standardDate, standardMilliseconds, afterStandard) <-
 186 |         readTransitionDate afterDaylightBias
 187 |       (daylightDate, daylightMilliseconds, remaining) <-
 188 |         readTransitionDate afterStandard
 189 |       case remaining of
 190 |         [] => Just (bias, standardBias, daylightBias,
 191 |           standardDate, standardMilliseconds,
 192 |           daylightDate, daylightMilliseconds)
 193 |         _ => Nothing
 194 | 
 195 | windowsOffset : Integer -> Either WindowsZoneError Offset
 196 | windowsOffset bias =
 197 |   let seconds = negate (bias * 60)
 198 |    in case refineOffsetSeconds seconds of
 199 |         Left _ => Left (WindowsOffsetOutOfRange seconds)
 200 |         Right value => Right value
 201 | 
 202 | transitionSeconds : WindowsTransitionDate -> Either WindowsZoneError Integer
 203 | transitionSeconds transition =
 204 |   if transition.hour < 0 || transition.hour > 23 ||
 205 |      transition.minute < 0 || transition.minute > 59 ||
 206 |      transition.second < 0 || transition.second > 59
 207 |     then Left (WindowsTimeOutOfRange transition.hour transition.minute
 208 |       transition.second)
 209 |     else Right (transition.hour * 3600 + transition.minute * 60 +
 210 |       transition.second)
 211 | 
 212 | windowsRule : WindowsTransitionDate -> Either WindowsZoneError RecurrenceRule
 213 | windowsRule transition = do
 214 |   if transition.year /= 0
 215 |     then Left (WindowsAbsoluteTransitionUnsupported transition.year)
 216 |     else Right ()
 217 |   seconds <- transitionSeconds transition
 218 |   case monthWeekDayRule transition.month transition.week transition.weekday
 219 |     seconds WallTime of
 220 |       Left error => Left (WindowsRecurrenceError error)
 221 |       Right value => Right value
 222 | 
 223 | windowsZoneRecurrence : WindowsZoneRule ->
 224 |                         Either WindowsZoneError ZoneRecurrence
 225 | windowsZoneRecurrence rule = do
 226 |   standardOffset <- windowsOffset
 227 |     (rule.biasMinutes + rule.standardBiasMinutes)
 228 |   daylightOffset <- windowsOffset
 229 |     (rule.biasMinutes + rule.daylightBiasMinutes)
 230 |   start <- windowsRule rule.daylightStart
 231 |   end <- windowsRule rule.standardStart
 232 |   Right (zoneRecurrence
 233 |     (transitionInfo standardOffset False rule.standardName)
 234 |     (transitionInfoWithSavings daylightOffset
 235 |       (minusClamped daylightOffset standardOffset) rule.daylightName)
 236 |     start end)
 237 | 
 238 | ||| Validate Windows TZI data and construct an invariant-preserving zone.
 239 | public export
 240 | windowsRecurringTimeZone : String -> TransitionInfo ->
 241 |                            List (Instant, TransitionInfo) -> WindowsZoneRule ->
 242 |                            Either WindowsTimeZoneError TimeZone
 243 | windowsRecurringTimeZone valueId initial transitions rule = do
 244 |   recurrence <- case windowsZoneRecurrence rule of
 245 |     Left error => Left (InvalidWindowsRule error)
 246 |     Right value => Right value
 247 |   case refineRecurringTimeZone valueId initial transitions recurrence of
 248 |     Left error => Left (InvalidWindowsTransitions error)
 249 |     Right value => Right value
 250 | 
 251 | noDaylightTransitions : WindowsZoneRule -> Bool
 252 | noDaylightTransitions rule =
 253 |   rule.daylightStart.month == 0 && rule.standardStart.month == 0
 254 | 
 255 | incompleteDaylightTransitions : WindowsZoneRule -> Bool
 256 | incompleteDaylightTransitions rule =
 257 |   (rule.daylightStart.month == 0) /= (rule.standardStart.month == 0)
 258 | 
 259 | windowsZoneEra : WindowsZoneRule -> Either WindowsZoneError
 260 |   (TransitionInfo, Maybe ZoneRecurrence)
 261 | windowsZoneEra rule =
 262 |   if incompleteDaylightTransitions rule
 263 |     then Left IncompleteWindowsDaylightRule
 264 |   else do
 265 |     standardOffset <- windowsOffset
 266 |       (rule.biasMinutes + rule.standardBiasMinutes)
 267 |     let standardInfo = transitionInfo standardOffset False rule.standardName
 268 |     if noDaylightTransitions rule
 269 |       then Right (standardInfo, Nothing)
 270 |       else map (\recurrence => (standardInfo, Just recurrence))
 271 |         (windowsZoneRecurrence rule)
 272 | 
 273 | ||| Validate a complete Windows TZI value. Month-zero transition dates describe
 274 | ||| a fixed standard-offset zone; paired nonzero dates describe recurrence.
 275 | public export
 276 | windowsTimeZone : String -> WindowsZoneRule ->
 277 |                   Either WindowsTimeZoneError TimeZone
 278 | windowsTimeZone valueId rule =
 279 |   case windowsZoneEra rule of
 280 |     Left error => Left (InvalidWindowsRule error)
 281 |     Right (standardInfo, Nothing) =>
 282 |       Right (fixedTimeZone valueId (utcOffset standardInfo))
 283 |     Right (standardInfo, Just recurrence) =>
 284 |       case refineRecurringTimeZone valueId standardInfo [] recurrence of
 285 |         Left error => Left (InvalidWindowsTransitions error)
 286 |         Right value => Right value
 287 | 
 288 | dynamicYearsValid : List WindowsDynamicRule -> Bool
 289 | dynamicYearsValid [] = True
 290 | dynamicYearsValid (first :: rest) = go first.effectiveYear rest
 291 |   where
 292 |     go : Integer -> List WindowsDynamicRule -> Bool
 293 |     go previous [] = True
 294 |     go previous (next :: remaining) =
 295 |       previous < next.effectiveYear && go next.effectiveYear remaining
 296 | 
 297 | yearStart : Integer -> Instant
 298 | yearStart year = fromNanosecondsSinceEpoch
 299 |   (gregorianDaysFromCivil year 1 1 * 86400 * 1000000000)
 300 | 
 301 | dynamicEraSpecs : Bool -> List WindowsDynamicRule -> Either WindowsZoneError
 302 |   (List (Maybe Instant, TransitionInfo, Maybe ZoneRecurrence))
 303 | dynamicEraSpecs first [] = Right []
 304 | dynamicEraSpecs first (entry :: rest) = do
 305 |   (initial, recurrence) <- windowsZoneEra entry.dynamicRule
 306 |   remaining <- dynamicEraSpecs False rest
 307 |   let boundary = if first then Nothing else Just (yearStart entry.effectiveYear)
 308 |   Right ((boundary, initial, recurrence) :: remaining)
 309 | 
 310 | ||| Construct a zone from Windows Dynamic DST values. When values are present,
 311 | ||| the first applies without a lower bound and the last remains in force.
 312 | public export
 313 | windowsDynamicTimeZone : String -> WindowsZoneRule -> List WindowsDynamicRule ->
 314 |                          Either WindowsTimeZoneError TimeZone
 315 | windowsDynamicTimeZone valueId defaultRule [] = windowsTimeZone valueId defaultRule
 316 | windowsDynamicTimeZone valueId defaultRule dynamicRules =
 317 |   if not (dynamicYearsValid dynamicRules)
 318 |     then Left DynamicYearsNotStrictlyIncreasing
 319 |     else do
 320 |       specs <- case dynamicEraSpecs True dynamicRules of
 321 |         Left error => Left (InvalidWindowsRule error)
 322 |         Right value => Right value
 323 |       case refineTimeZoneEras valueId specs of
 324 |         Left error => Left (InvalidWindowsTransitions error)
 325 |         Right value => Right value
 326 | 
 327 | parseDynamicTzi : String -> String -> List (Integer, List Bits8) ->
 328 |                   Either WindowsRegistryError (List WindowsDynamicRule)
 329 | parseDynamicTzi standardName daylightName [] = Right []
 330 | parseDynamicTzi standardName daylightName ((year, bytes) :: rest) = do
 331 |   rule <- case parseWindowsTzi standardName daylightName bytes of
 332 |     Left error => Left (InvalidDynamicTzi year error)
 333 |     Right value => Right value
 334 |   remaining <- parseDynamicTzi standardName daylightName rest
 335 |   Right (MkWindowsDynamicRule year rule :: remaining)
 336 | 
 337 | ||| Convert registry bytes captured by a native adapter into a validated zone.
 338 | public export
 339 | windowsRegistryTimeZoneAs : String -> WindowsRegistryZone ->
 340 |                           Either WindowsRegistryError TimeZone
 341 | windowsRegistryTimeZoneAs valueId registry = do
 342 |   defaultRule <- case parseWindowsTzi registry.registryStandardName
 343 |     registry.registryDaylightName registry.registryDefaultTzi of
 344 |       Left error => Left (InvalidDefaultTzi error)
 345 |       Right value => Right value
 346 |   dynamicRules <- parseDynamicTzi registry.registryStandardName
 347 |     registry.registryDaylightName registry.registryDynamicTzi
 348 |   case windowsDynamicTimeZone valueId defaultRule dynamicRules of
 349 |     Left error => Left (InvalidRegistryTimeZone error)
 350 |     Right value => Right value
 351 | 
 352 | ||| Convert registry bytes using the Windows registry identifier as zone
 353 | ||| identity.
 354 | public export
 355 | windowsRegistryTimeZone : WindowsRegistryZone ->
 356 |                           Either WindowsRegistryError TimeZone
 357 | windowsRegistryTimeZone registry =
 358 |   windowsRegistryTimeZoneAs registry.registryZoneId registry