0 | module IotaTime.Tzdb.Posix
2 | import public IotaTime.TimeZone.Core
10 | = ExpectedIdentifier
12 | | ExpectedCharacter Char
13 | | InvalidTime Integer Integer Integer
14 | | PosixOffsetOutOfRange Integer
15 | | PosixRuleOutOfRange RecurrenceRuleError
16 | | MissingDaylightRules
17 | | UnexpectedTrailingInput String
21 | = PosixFixed TransitionInfo
22 | | PosixRecurring ZoneRecurrence
24 | Parser : Type -> Type
25 | Parser value = List Char -> Either PosixTzError (value, List Char)
27 | parseIdentifier : Parser String
28 | parseIdentifier ('<' :: rest) =
29 | let (name, remaining) = span (/= '>') rest
30 | in case remaining of
31 | '>' :: after => if null name
32 | then Left ExpectedIdentifier
33 | else Right (pack name, after)
34 | _ => Left (ExpectedCharacter '>')
35 | parseIdentifier input =
36 | let (name, remaining) = span isAlpha input
37 | in if length name >= 3
38 | then Right (pack name, remaining)
39 | else Left ExpectedIdentifier
41 | parseDigits : Parser Integer
43 | let (digits, remaining) = span isDigit input
45 | then Left ExpectedNumber
46 | else Right (foldl (\value, digit =>
47 | value * 10 + cast digit - cast '0') 0 digits, remaining)
49 | parseOptionalComponent : List Char -> Either PosixTzError (Integer, List Char)
50 | parseOptionalComponent (':' :: rest) = parseDigits rest
51 | parseOptionalComponent input = Right (0, input)
53 | parseSignedTime : Parser Integer
54 | parseSignedTime input = do
55 | let (sign, unsigned) = case input of
56 | '-' :: rest => (-
1, rest)
57 | '+' :: rest => (1, rest)
59 | (hours, afterHours) <- parseDigits unsigned
60 | (minutes, afterMinutes) <- parseOptionalComponent afterHours
61 | (seconds, remaining) <- parseOptionalComponent afterMinutes
62 | if minutes > 59 || seconds > 59
63 | then Left (InvalidTime hours minutes seconds)
64 | else Right (sign * (hours * 3600 + minutes * 60 + seconds), remaining)
66 | parseOffset : Parser Offset
67 | parseOffset input = do
68 | (posixSeconds, remaining) <- parseSignedTime input
69 | let utcSeconds = negate posixSeconds
70 | case refineOffsetSeconds utcSeconds of
71 | Left _ => Left (PosixOffsetOutOfRange utcSeconds)
72 | Right value => Right (value, remaining)
74 | expect : Char -> List Char -> Either PosixTzError (List Char)
75 | expect wanted (actual :: rest) =
76 | if actual == wanted then Right rest else Left (ExpectedCharacter wanted)
77 | expect wanted [] = Left (ExpectedCharacter wanted)
79 | parseMode : List Char -> (TransitionTimeMode, List Char)
80 | parseMode ('s' :: rest) = (StandardTime, rest)
81 | parseMode ('u' :: rest) = (UniversalTime, rest)
82 | parseMode ('g' :: rest) = (UniversalTime, rest)
83 | parseMode ('z' :: rest) = (UniversalTime, rest)
84 | parseMode ('w' :: rest) = (WallTime, rest)
85 | parseMode input = (WallTime, input)
87 | parseRuleTime : List Char -> Either PosixTzError
88 | ((Integer, TransitionTimeMode), List Char)
89 | parseRuleTime ('/' :: rest) = do
90 | (seconds, afterTime) <- parseSignedTime rest
91 | let (mode, remaining) = parseMode afterTime
92 | Right ((seconds, mode), remaining)
93 | parseRuleTime input = Right ((7200, WallTime), input)
95 | parseMonthRule : Parser RecurrenceRule
96 | parseMonthRule input = do
97 | (month, afterMonth) <- parseDigits input
98 | afterFirstDot <- expect '.' afterMonth
99 | (week, afterWeek) <- parseDigits afterFirstDot
100 | afterSecondDot <- expect '.' afterWeek
101 | (weekday, afterWeekday) <- parseDigits afterSecondDot
102 | ((seconds, mode), remaining) <- parseRuleTime afterWeekday
103 | rule <- mapFst PosixRuleOutOfRange (monthWeekDayRule month week weekday seconds mode)
104 | Right (rule, remaining)
106 | parseJulianRule : Bool -> Parser RecurrenceRule
107 | parseJulianRule withoutLeap input = do
108 | (day, afterDay) <- parseDigits input
109 | ((seconds, mode), remaining) <- parseRuleTime afterDay
110 | rule <- mapFst PosixRuleOutOfRange (if withoutLeap
111 | then julianWithoutLeapRule day seconds mode
112 | else julianWithLeapRule day seconds mode)
113 | Right (rule, remaining)
115 | parseRule : Parser RecurrenceRule
116 | parseRule ('M' :: rest) = parseMonthRule rest
117 | parseRule ('J' :: rest) = parseJulianRule True rest
118 | parseRule input = parseJulianRule False input
120 | parseDaylight : String -> Offset -> String -> List Char ->
121 | Either PosixTzError (PosixZone, List Char)
122 | parseDaylight standardName standardOffset daylightName input = do
123 | (daylightOffset, afterOffset) <- case input of
124 | ',' :: _ => defaultOffset
125 | [] => defaultOffset
126 | _ => parseOffset input
127 | afterStartComma <- expect ',' afterOffset
128 | (startRule, afterStart) <- parseRule afterStartComma
129 | afterEndComma <- expect ',' afterStart
130 | (endRule, remaining) <- parseRule afterEndComma
131 | let standardInfo = transitionInfo standardOffset False standardName
132 | daylightInfo = transitionInfoWithSavings daylightOffset
133 | (minusClamped daylightOffset standardOffset) daylightName
134 | Right (PosixRecurring
135 | (zoneRecurrence standardInfo daylightInfo startRule endRule), remaining)
137 | defaultOffset : Either PosixTzError (Offset, List Char)
138 | defaultOffset = case refineOffsetSeconds
139 | (totalOffsetSeconds standardOffset + 3600) of
140 | Left _ => Left (PosixOffsetOutOfRange
141 | (totalOffsetSeconds standardOffset + 3600))
142 | Right value => Right (value, input)
146 | parsePosixZone : String -> Either PosixTzError PosixZone
147 | parsePosixZone source = do
148 | (standardName, afterStandardName) <- parseIdentifier (unpack source)
149 | (standardOffset, afterStandardOffset) <- parseOffset afterStandardName
150 | case afterStandardOffset of
151 | [] => Right (PosixFixed
152 | (transitionInfo standardOffset False standardName))
154 | (daylightName, afterDaylightName) <- parseIdentifier afterStandardOffset
155 | if null afterDaylightName
156 | then Left MissingDaylightRules
158 | (zone, remaining) <- parseDaylight standardName standardOffset
159 | daylightName afterDaylightName
162 | _ => Left (UnexpectedTrailingInput (pack remaining))