time.bend
bend-kit-time@0.1.3.0 · 1,208 lines · 0 definitions
1# Clocks, Duration and Instant, Gregorian dates, RFC 3339 and HTTP-date text, and TZif time zones. Source: https://github.com/paymog/bend-kit/tree/main/time
2import Base
3import bend-kit-int@0.2.0.0/int.bend as Int
4import bend-kit-fmt@0.1.0.0/fmt.bend as Fmt
5# bend-kit-bytes@0.3.0.0
6import bend-kit-bytes@0.3.0.0/bytes.bend as Bytes
7
8# secs + nanos / 10^9 seconds, with nanos below 10^9: -0.5 s is Duration{-1, 500000000}.
9type Duration is Data:
10 Duration{secs: Int.I64, nanos: U32}
11
12# A Duration since 1970-01-01T00:00:00Z. Days are 86400 s: there are no leap seconds.
13type Instant is Data:
14 Instant{secs: Int.I64, nanos: U32}
15
16# A proleptic Gregorian date. The conversions and formats cover years 0 to 9999.
17type Date is Data:
18 Date{year: U32, month: U32, day: U32}
19
20type DateTime is Data:
21 DateTime{date: Date, hour: U32, min: U32, sec: U32, nanos: U32}
22
23def i64(x: U32) -> Int.I64:
24 Int.I64.from_u32(x)
25
26# The signed 32-bit value of x, widened.
27def i64s(x: U32) -> Int.I64:
28 match x:
29 case U32{w}:
30 Int.I64{Int.Int.sext(64n, 32n, w)}
31
32# hi * 2^32 + lo, as the bits of an I64.
33def i64.of(hi: U32, lo: U32) -> Int.I64:
34 Int.I64.or(Int.I64.shl(i64(hi), 32n), i64(lo))
35
36# Duration
37# --------
38
39def Duration.zero() -> Duration:
40 Duration{i64(0), 0}
41
42def Duration.of_secs(s: Int.I64) -> Duration:
43 Duration{s, 0}
44
45def Duration.of_ms(+ms: U32) -> Duration:
46 Duration{i64((ms / 1000 : U32)), ((ms % 1000 : U32) * 1000000 : U32)}
47
48# Whole milliseconds, rounded down.
49def Duration.to_ms(d: Duration) -> Int.I64:
50 match d:
51 case Duration{s, n}:
52 Int.I64.add(Int.I64.mul(s, i64(1000)), i64((n / 1000000 : U32)))
53
54def Duration.to_nat.of(m: Maybe<&2, Nat>, +per: Nat, +n: U32) -> Nat:
55 match m:
56 case None{}:
57 0n
58 case Some{s}:
59 (s * per + U32.to_nat(n) : Nat)
60
61# Whole milliseconds, rounded down; 0 when d is negative.
62def Duration.to_ms_nat(d: Duration) -> Nat:
63 match d:
64 case Duration{s, n}:
65 Duration.to_nat.of(Int.I64.to_nat(s), 1000n, (n / 1000000 : U32))
66
67# Whole microseconds, rounded down; 0 when d is negative.
68def Duration.to_us_nat(d: Duration) -> Nat:
69 match d:
70 case Duration{s, n}:
71 Duration.to_nat.of(Int.I64.to_nat(s), 1000000n, (n / 1000 : U32))
72
73def Duration.carry(c: Bool, s: Int.I64, +n: U32) -> Duration:
74 match c:
75 case True{}:
76 Duration{Int.I64.add(s, i64(1)), (n - 1000000000 : U32)}
77 case False{}:
78 Duration{s, n}
79
80def Duration.add(a: Duration, b: Duration) -> Duration:
81 match a b:
82 case Duration{sa, na} Duration{sb, nb}:
83 +n = (na + nb : U32)
84 Duration.carry(U32.is_ge(n, 1000000000), Int.I64.add(sa, sb), n)
85
86# n is na - nb, wrapped when na < nb.
87def Duration.borrow(c: Bool, s: Int.I64, +n: U32) -> Duration:
88 match c:
89 case True{}:
90 Duration{Int.I64.sub(s, i64(1)), (n + 1000000000 : U32)}
91 case False{}:
92 Duration{s, n}
93
94def Duration.sub(a: Duration, b: Duration) -> Duration:
95 match a b:
96 case Duration{sa, +na} Duration{sb, +nb}:
97 Duration.borrow(U32.is_lt(na, nb), Int.I64.sub(sa, sb), (na - nb : U32))
98
99def Duration.neg(d: Duration) -> Duration:
100 Duration.sub(Duration.zero(), d)
101
102def Duration.cmp.then(c: Cmp, +na: U32, +nb: U32) -> Cmp:
103 match c:
104 case EQ{}:
105 U32.cmp(na, nb)
106 case LT{}:
107 LT{}
108 case GT{}:
109 GT{}
110
111def Duration.cmp(a: Duration, b: Duration) -> Cmp:
112 match a b:
113 case Duration{sa, na} Duration{sb, nb}:
114 Duration.cmp.then(Int.I64.cmp(sa, sb), na, nb)
115
116# Instant
117# -------
118
119def Instant.epoch() -> Instant:
120 Instant{i64(0), 0}
121
122def Instant.of_unix(s: Int.I64) -> Instant:
123 Instant{s, 0}
124
125def Instant.of(d: Duration) -> Instant:
126 match d:
127 case Duration{s, n}:
128 Instant{s, n}
129
130def Instant.since_epoch(i: Instant) -> Duration:
131 match i:
132 case Instant{s, n}:
133 Duration{s, n}
134
135def Instant.add(i: Instant, d: Duration) -> Instant:
136 Instant.of(Duration.add(Instant.since_epoch(i), d))
137
138# a - b.
139def Instant.since(a: Instant, b: Instant) -> Duration:
140 Duration.sub(Instant.since_epoch(a), Instant.since_epoch(b))
141
142def Instant.cmp(a: Instant, b: Instant) -> Cmp:
143 Duration.cmp(Instant.since_epoch(a), Instant.since_epoch(b))
144
145# Clocks
146# ------
147
148# (secs hi, secs lo, nanos) of CLOCK_MONOTONIC, from an unspecified start.
149def mono.raw() -> IO(U32 & U32 & U32):
150 import "./effs/time.c"
151 import "./effs/time.js"
152
153# (secs hi, secs lo, nanos) of CLOCK_REALTIME, since the Unix epoch.
154def wall.raw() -> IO(U32 & U32 & U32):
155 import "./effs/time.c"
156 import "./effs/time.js"
157
158def raw.dur(r: U32 & U32 & U32) -> Duration:
159 (hi, lo, n) = r
160 Duration{i64.of(hi, lo), n}
161
162# Time since an unspecified start that never goes back. Use it to measure spans.
163def mono() -> IO(Duration):
164 do IO<Duration>:
165 r : U32 & U32 & U32 <- mono.raw()
166 return raw.dur(r)
167
168# Monotonic milliseconds. Pure cores that take a Nat `now` in ms take this.
169def mono.ms() -> IO(Nat):
170 do IO<Nat>:
171 d : Duration <- mono()
172 return Duration.to_ms_nat(d)
173
174# Monotonic microseconds.
175def mono.us() -> IO(Nat):
176 do IO<Nat>:
177 d : Duration <- mono()
178 return Duration.to_us_nat(d)
179
180# The wall clock. It can jump when the system time is set.
181def now() -> IO(Instant):
182 do IO<Instant>:
183 r : U32 & U32 & U32 <- wall.raw()
184 return Instant.of(raw.dur(r))
185
186# Dates
187# -----
188
189def Date.is_leap(+y: U32) -> Bool:
190 Bool.and(U32.is_eq((y % 4 : U32), 0),
191 Bool.or(U32.is_ne((y % 100 : U32), 0), U32.is_eq((y % 400 : U32), 0)))
192
193# 0 for a month outside 1 to 12.
194def Date.days_in_month(+y: U32, +m: U32) -> U32:
195 Bool.pick(U32, U32.is_eq(m, 2), Bool.pick(U32, Date.is_leap(y), 29, 28),
196 Bool.pick(U32, Bool.and(U32.is_ge(m, 1), U32.is_le(m, 12)),
197 (30 + ((m + (m >> 3n)) .&. 1) : U32), 0))
198
199def Date.valid(d: Date) -> Bool:
200 match d:
201 case Date{+y, +m, +dd}:
202 Bool.and(U32.is_le(y, 9999),
203 Bool.and(U32.is_ge(dd, 1), U32.is_le(dd, Date.days_in_month(y, m))))
204
205# z counts days from -0400-03-01, so every date from year 0 has z > 0 in a U32.
206# The civil-days algorithm is Howard Hinnant's, with the year starting in March.
207def Z.EPOCH() -> U32:
208 865565
209
210def Date.to_z.at(+y: U32, +mp: U32, +d: U32) -> U32:
211 +era = (y / 400 : U32)
212 +yoe = (y - era * 400 : U32)
213 +doy = ((153 * mp + 2) / 5 + d - 1 : U32)
214 (era * 146097 + yoe * 365 + yoe / 4 - yoe / 100 + doy : U32)
215
216def Date.to_z.go(jf: Bool, +y: U32, +m: U32, +d: U32) -> U32:
217 match jf:
218 case True{}:
219 Date.to_z.at((y + 399 : U32), (m + 9 : U32), d)
220 case False{}:
221 Date.to_z.at((y + 400 : U32), (m - 3 : U32), d)
222
223def Date.to_z(d: Date) -> U32:
224 match d:
225 case Date{+y, +m, +dd}:
226 Date.to_z.go(U32.is_le(m, 2), y, m, dd)
227
228def Date.of_z.fin(lo: Bool, +y: U32, +mp: U32, +d: U32) -> Date:
229 match lo:
230 case True{}:
231 Date{(y - 400 : U32), (mp + 3 : U32), d}
232 case False{}:
233 Date{(y - 399 : U32), (mp - 9 : U32), d}
234
235def Date.of_z(+z: U32) -> Date:
236 +era = (z / 146097 : U32)
237 +doe = (z - era * 146097 : U32)
238 +yoe = ((doe - doe / 1460 + doe / 36524 - doe / 146096) / 365 : U32)
239 +doy = (doe - (365 * yoe + yoe / 4 - yoe / 100) : U32)
240 +mp = ((5 * doy + 2) / 153 : U32)
241 Date.of_z.fin(U32.is_lt(mp, 10), (yoe + era * 400 : U32), mp,
242 (doy - (153 * mp + 2) / 5 + 1 : U32))
243
244# Days since 1970-01-01.
245def Date.to_days(d: Date) -> Int.I64:
246 Int.I64.sub(i64(Date.to_z(d)), i64(Z.EPOCH()))
247
248def Date.of_z.if(ok: Bool, +z: U32) -> Maybe<&2, Date>:
249 match ok:
250 case True{}:
251 Some{Date.of_z(z)}
252 case False{}:
253 None{}
254
255# The date days after 1970-01-01, or None outside 0000-01-01 to 9999-12-31.
256def Date.of_days(days: Int.I64) -> Maybe<&2, Date>:
257 +z = Int.I64.add(days, i64(Z.EPOCH()))
258 Date.of_z.if(Bool.and(Int.I64.is_ge(z, i64(146037)), Int.I64.is_le(z, i64(3798461))),
259 Int.I64.to_u32(z))
260
261# 1 for Monday to 7 for Sunday, as in ISO 8601.
262def Date.weekday(d: Date) -> U32:
263 ((Date.to_z(d) + 2) % 7 + 1 : U32)
264
265# Date and time
266# -------------
267
268def DateTime.valid(t: DateTime) -> Bool:
269 match t:
270 case DateTime{d, h, mi, s, n}:
271 Bool.and(Date.valid(d), Bool.and(U32.is_le(h, 23),
272 Bool.and(U32.is_le(mi, 59), Bool.and(U32.is_le(s, 59), U32.is_lt(n, 1000000000)))))
273
274# The instant of a UTC date and time. It does not check t; see DateTime.valid.
275def DateTime.to_instant(t: DateTime) -> Instant:
276 match t:
277 case DateTime{d, h, mi, s, n}:
278 Instant{Int.I64.add(Int.I64.mul(Date.to_days(d), i64(86400)),
279 i64((h * 3600 + mi * 60 + s : U32))), n}
280
281def DateTime.at(m: Maybe<&2, Date>, +sod: U32, n: U32) -> Maybe<&2, DateTime>:
282 match m:
283 case None{}:
284 None{}
285 case Some{d}:
286 Some{DateTime{d, (sod / 3600 : U32), (sod / 60 % 60 : U32), (sod % 60 : U32), n}}
287
288# r is secs % 86400, which has the sign of secs.
289def DateTime.floor(neg: Bool, q: Int.I64, r: Int.I64, n: U32) -> Maybe<&2, DateTime>:
290 match neg:
291 case True{}:
292 DateTime.at(Date.of_days(Int.I64.sub(q, i64(1))), (Int.I64.to_u32(r) + 86400 : U32), n)
293 case False{}:
294 DateTime.at(Date.of_days(q), Int.I64.to_u32(r), n)
295
296# The UTC date and time of i, or None outside years 0 to 9999.
297def DateTime.of_instant(i: Instant) -> Maybe<&2, DateTime>:
298 match i:
299 case Instant{+s, n}:
300 +r = Int.I64.mod(s, i64(86400))
301 DateTime.floor(Int.I64.is_neg(r), Int.I64.div(s, i64(86400)), r, n)
302
303# Text
304# ----
305
306def pad(+x: U32, w: Nat) -> String:
307 Fmt.Fmt.pad_left(U32.show(x), w, '0')
308
309# Milliseconds with six decimal places.
310def Duration.show_ms.pos(d: Duration) -> String:
311 match d:
312 case Duration{s, +n}:
313 Int.I64.show(Duration.to_ms(Duration{s, n})) ++ "." ++ pad((n % 1000000 : U32), 6n)
314
315def Duration.show_ms.sign(neg: Bool, d: Duration) -> String:
316 match neg:
317 case True{}:
318 "-" ++ Duration.show_ms.pos(Duration.neg(d))
319 case False{}:
320 Duration.show_ms.pos(d)
321
322def Duration.show_ms(d: Duration) -> String:
323 match d:
324 case Duration{+s, n}:
325 Duration.show_ms.sign(Int.I64.is_neg(s), Duration{s, n})
326
327# The digits of n / 10^(9 - w), with trailing zeros cut. n is not 0.
328def frac.go(f: Nat, z: Bool, +n: U32, +w: Nat) -> String:
329 match f:
330 case 0n:
331 pad(n, w)
332 case 1n+g:
333 match z:
334 case True{}:
335 +m = (n / 10 : U32)
336 frac.go(g, U32.is_eq((m % 10 : U32), 0), m, (w - 1n : Nat))
337 case False{}:
338 pad(n, w)
339
340def frac(+n: U32) -> String:
341 Bool.pick(String, U32.is_eq(n, 0), "", SCon{'.', frac.go(8n, U32.is_eq((n % 10 : U32), 0), n, 9n)})
342
343def DateTime.rfc3339(t: DateTime) -> String:
344 match t:
345 case DateTime{Date{y, mo, d}, h, mi, s, n}:
346 String.concat([pad(y, 4n), "-", pad(mo, 2n), "-", pad(d, 2n), "T", pad(h, 2n), ":",
347 pad(mi, 2n), ":", pad(s, 2n), frac(n), "Z"])
348
349def fmt.map(~f: DateTime -> String, m: Maybe<&2, DateTime>) -> Maybe<&2, String>:
350 match m:
351 case None{}:
352 None{}
353 case Some{t}:
354 Some{f(t)}
355
356# RFC 3339 in UTC, such as 1985-04-12T23:20:50.52Z. The fraction has no trailing zeros, and is left out when 0.
357def rfc3339(i: Instant) -> Maybe<&2, String>:
358 fmt.map(~DateTime.rfc3339, DateTime.of_instant(i))
359
360def WEEKDAYS() -> List<&2, String>:
361 ["Mon", "Tue", "Wed", "Thu", "Fri", "Sat", "Sun"]
362
363def MONTHS() -> List<&2, String>:
364 ["Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"]
365
366def name(xs: List<&2, String>, +i: U32) -> String:
367 Maybe.default(&2, String, List.get(&2, String, xs, U32.to_nat(i)), "")
368
369def DateTime.http_date(t: DateTime) -> String:
370 match t:
371 case DateTime{+date, h, mi, s, n}:
372 Date{y, mo, d} = date
373 String.concat([name(WEEKDAYS(), (Date.weekday(date) - 1 : U32)), ", ", pad(d, 2n), " ",
374 name(MONTHS(), (mo - 1 : U32)), " ", pad(y, 4n), " ", pad(h, 2n), ":", pad(mi, 2n), ":",
375 pad(s, 2n), " GMT"])
376
377# IMF-fixdate (RFC 9110 §5.6.7), such as Sun, 06 Nov 1994 08:49:37 GMT. It drops the fraction of a second.
378def http_date(i: Instant) -> Maybe<&2, String>:
379 fmt.map(~DateTime.http_date, DateTime.of_instant(i))
380
381# Parsers
382# -------
383
384# A parser state: the numbers read so far, newest first, and the text left.
385type P is Data:
386 P{vals: List<&2, U32>, rest: String}
387
388def is_digit(+c: U32) -> Bool:
389 Bool.and(U32.is_ge(c, 48), U32.is_le(c, 57))
390
391def digits.go(n: Nat, s: String, +acc: U32, ok: Bool) -> Maybe<&1, U32 & String>:
392 match n:
393 case 0n:
394 match ok:
395 case True{}:
396 Some{(acc, s)}
397 case False{}:
398 None{}
399 case 1n+k:
400 match s:
401 case SNil{}:
402 None{}
403 case SCon{Chr{+c}, t}:
404 digits.go(k, t, (acc * 10 + c - 48 : U32), Bool.and(ok, is_digit(c)))
405
406def push(vs: List<&2, U32>, r: Maybe<&1, U32 & String>) -> Maybe<&2, P>:
407 match r:
408 case None{}:
409 None{}
410 case Some{(v, t)}:
411 Some{P{Con{v, vs}, t}}
412
413# Exactly n digits.
414def num(n: Nat, p: P) -> Maybe<&2, P>:
415 match p:
416 case P{vs, s}:
417 push(vs, digits.go(n, s, 0, True{}))
418
419def lit.if(ok: Bool, vs: List<&2, U32>, t: String) -> Maybe<&2, P>:
420 match ok:
421 case True{}:
422 Some{P{vs, t}}
423 case False{}:
424 None{}
425
426# One char that is a or b.
427def lit2(+a: U32, +b: U32, p: P) -> Maybe<&2, P>:
428 match p:
429 case P{vs, s}:
430 match s:
431 case SNil{}:
432 None{}
433 case SCon{Chr{+c}, t}:
434 lit.if(Bool.or(U32.is_eq(c, a), U32.is_eq(c, b)), vs, t)
435
436def lit(+c: U32, p: P) -> Maybe<&2, P>:
437 lit2(c, c, p)
438
439def text(+w: String, p: P) -> Maybe<&2, P>:
440 match p:
441 case P{vs, +s}:
442 +n = String.length(w)
443 lit.if(String.eq(String.take(s, n), w), vs, String.drop(s, n))
444
445def at.head(+s: String) -> Bool:
446 match s:
447 case SNil{}:
448 False{}
449 case SCon{Chr{+c}, t}:
450 is_digit(c)
451
452# Digits after the first nine are read and dropped. d says whether s starts with a digit.
453def secfrac.go(s: String, d: Bool, +mul: U32, +acc: U32, +k: U32) -> U32 & U32 & String:
454 match s:
455 case SNil{}:
456 (k, acc, SNil{})
457 case SCon{Chr{+c}, +t}:
458 match d:
459 case True{}:
460 secfrac.go(t, at.head(t), (mul / 10 : U32), (acc + (c - 48) * mul : U32), (k + 1 : U32))
461 case False{}:
462 (k, acc, SCon{Chr{c}, t})
463
464def secfrac.fin(vs: List<&2, U32>, r: U32 & U32 & String) -> Maybe<&2, P>:
465 (k, n, t) = r
466 lit.if(U32.is_gt(k, 0), Con{n, vs}, t)
467
468def secfrac.if(dot: Bool, vs: List<&2, U32>, +s: String) -> Maybe<&2, P>:
469 match dot:
470 case True{}:
471 +t = String.drop(s, 1n)
472 secfrac.fin(vs, secfrac.go(t, at.head(t), 100000000, 0, 0))
473 case False{}:
474 Some{P{Con{0, vs}, s}}
475
476# An optional '.' and one or more digits, as nanoseconds.
477def secfrac(p: P) -> Maybe<&2, P>:
478 match p:
479 case P{vs, +s}:
480 secfrac.if(String.starts_with(s, "."), vs, s)
481
482def zone.num(+neg: U32, vs: List<&2, U32>, t: String) -> Maybe<&2, P>:
483 do Maybe<&2, P>:
484 a : P <- num(2n, P{Con{neg, vs}, t})
485 b : P <- lit(58, a)
486 num(2n, b)
487
488def zone.if(z: Bool, plus: Bool, minus: Bool, vs: List<&2, U32>, t: String) -> Maybe<&2, P>:
489 match z:
490 case True{}:
491 Some{P{Con{0, Con{0, Con{0, vs}}}, t}}
492 case False{}:
493 match plus:
494 case True{}:
495 zone.num(0, vs, t)
496 case False{}:
497 match minus:
498 case True{}:
499 zone.num(1, vs, t)
500 case False{}:
501 None{}
502
503# Z, or +hh:mm or -hh:mm, as (sign, hh, mm) with sign 1 for west of UTC.
504def zone(p: P) -> Maybe<&2, P>:
505 match p:
506 case P{vs, s}:
507 match s:
508 case SNil{}:
509 None{}
510 case SCon{Chr{+c}, t}:
511 zone.if(Bool.or(U32.is_eq(c, 90), U32.is_eq(c, 122)), U32.is_eq(c, 43), U32.is_eq(c, 45), vs, t)
512
513def index.go(xs: List<&2, String>, +w: String, +i: U32) -> U32:
514 match xs:
515 case Nil{}:
516 i
517 case Con{x, rest}:
518 Bool.pick(U32, String.eq(x, w), i, index.go(rest, w, (i + 1 : U32)))
519
520# One of names, as its index.
521def word(+names: List<&2, String>, p: P) -> Maybe<&2, P>:
522 match p:
523 case P{vs, +s}:
524 +i = index.go(names, String.take(s, 3n), 0)
525 lit.if(U32.is_lt(i, U32.from_nat(List.length(&2, String, names))), Con{i, vs}, String.drop(s, 3n))
526
527def mk.if(ok: Bool, t: DateTime) -> Maybe<&2, Instant>:
528 match ok:
529 case True{}:
530 Some{DateTime.to_instant(t)}
531 case False{}:
532 None{}
533
534def mk(+t: DateTime) -> Maybe<&2, Instant>:
535 mk.if(DateTime.valid(t), t)
536
537def rfc3339.shift(m: Maybe<&2, Instant>, +west: U32, +hh: U32, +mm: U32) -> Maybe<&2, Instant>:
538 match m:
539 case None{}:
540 None{}
541 case Some{i}:
542 +off = Duration.of_secs(i64((hh * 3600 + mm * 60 : U32)))
543 Bool.pick(Maybe<&2, Instant>, Bool.and(U32.is_le(hh, 23), U32.is_le(mm, 59)),
544 Some{Instant.add(i, Bool.pick(Duration, U32.is_eq(west, 1), off, Duration.neg(off)))}, None{})
545
546def rfc3339.fin(p: P) -> Maybe<&2, Instant>:
547 match p:
548 case P{Con{mm, Con{hh, Con{west, Con{n, Con{s, Con{mi, Con{h, Con{d, Con{mo, Con{y, Nil{}}}}}}}}}}}, SNil{}}:
549 rfc3339.shift(mk(DateTime{Date{y, mo, d}, h, mi, s, n}), west, hh, mm)
550 case _:
551 None{}
552
553# An RFC 3339 date-time (§5.6), such as 1985-04-12T23:20:50.52Z or 1996-12-19T16:39:57-08:00.
554# T and Z may be lowercase. A leap second (:60) is refused, as Instant has none.
555def rfc3339.parse(s: String) -> Maybe<&2, Instant>:
556 do Maybe<&2, Instant>:
557 a : P <- num(4n, P{Nil{}, s})
558 b : P <- lit(45, a)
559 c : P <- num(2n, b)
560 d : P <- lit(45, c)
561 e : P <- num(2n, d)
562 f : P <- lit2(84, 116, e)
563 g : P <- num(2n, f)
564 h : P <- lit(58, g)
565 i : P <- num(2n, h)
566 j : P <- lit(58, i)
567 k : P <- num(2n, j)
568 l : P <- secfrac(k)
569 m : P <- zone(l)
570 rfc3339.fin(m)
571
572def http_date.fin(p: P) -> Maybe<&2, Instant>:
573 match p:
574 case P{Con{s, Con{mi, Con{h, Con{y, Con{mo, Con{d, Con{wd, Nil{}}}}}}}}, SNil{}}:
575 mk(DateTime{Date{y, (mo + 1 : U32), d}, h, mi, s, 0})
576 case _:
577 None{}
578
579# An IMF-fixdate (RFC 9110 §5.6.7), such as Sun, 06 Nov 1994 08:49:37 GMT.
580# The day name must be one of the seven, but it is not checked against the date.
581def http_date.parse(s: String) -> Maybe<&2, Instant>:
582 do Maybe<&2, Instant>:
583 a : P <- word(WEEKDAYS(), P{Nil{}, s})
584 b : P <- text(", ", a)
585 c : P <- num(2n, b)
586 d : P <- lit(32, c)
587 e : P <- word(MONTHS(), d)
588 f : P <- lit(32, e)
589 g : P <- num(4n, f)
590 h : P <- lit(32, g)
591 i : P <- num(2n, h)
592 j : P <- lit(58, i)
593 k : P <- num(2n, j)
594 l : P <- lit(58, k)
595 m : P <- num(2n, l)
596 n : P <- text(" GMT", m)
597 http_date.fin(n)
598
599# Time zones
600# ----------
601
602# A local time type: seconds east of UTC, whether it is daylight time, and its abbreviation.
603type Ttype is Data:
604 Ttype{utoff: Int.I64, dst: Bool, abbr: String}
605
606# From at on, local time follows types[idx].
607type Trans is Data:
608 Trans{at: Int.I64, idx: U32}
609
610# A TZif zone (RFC 8536): transitions in time order, local time types, and the footer TZ string ("" in version 1).
611type Zone is Data:
612 Zone{trans: List<&2, Trans>, types: List<&2, Ttype>, tz: String}
613
614# n bytes of a byte string, big-endian.
615def be(n: Nat, s: String, +acc: U32) -> U32:
616 match n:
617 case 0n:
618 acc
619 case 1n+k:
620 match s:
621 case SNil{}:
622 acc
623 case SCon{Chr{c}, t}:
624 be(k, t, ((acc << 8n) .|. c : U32))
625
626def be32(+s: String, n: Nat) -> U32:
627 be(4n, String.drop(s, n), 0)
628
629def u8(+s: String, n: Nat) -> U32:
630 be(1n, String.drop(s, n), 0)
631
632def tzif.size(t8: Bool) -> Nat:
633 match t8:
634 case True{}:
635 8n
636 case False{}:
637 4n
638
639def tzif.time(t8: Bool, +s: String) -> Int.I64:
640 match t8:
641 case True{}:
642 i64.of(be32(s, 0n), be32(s, 4n))
643 case False{}:
644 i64s(be32(s, 0n))
645
646# ts holds the transition times and ks their type indexes.
647def tzif.trans(n: Nat, +t8: Bool, +ts: String, +ks: String) -> List<&2, Trans>:
648 match n:
649 case 0n:
650 Nil{}
651 case 1n+k:
652 Con{Trans{tzif.time(t8, ts), u8(ks, 0n)},
653 tzif.trans(k, t8, String.drop(ts, tzif.size(t8)), String.drop(ks, 1n))}
654
655# The NUL-terminated abbreviation at byte i of chars.
656def tzif.abbr(chars: String, +i: U32) -> String:
657 name(String.split(String.drop(chars, U32.to_nat(i)), Chr{0}), 0)
658
659def tzif.types(n: Nat, +s: String, +chars: String) -> List<&2, Ttype>:
660 match n:
661 case 0n:
662 Nil{}
663 case 1n+k:
664 Con{Ttype{i64s(be32(s, 0n)), U32.is_ne(u8(s, 4n), 0), tzif.abbr(chars, u8(s, 5n))},
665 tzif.types(k, String.drop(s, 6n), chars)}
666
667def tzif.if(ok: Bool, z: Zone) -> Maybe<&2, Zone>:
668 match ok:
669 case True{}:
670 Some{z}
671 case False{}:
672 None{}
673
674# Header counts, in RFC 8536 order: isut, isstd, leap, time, type, char.
675def tzif.count(+h: String, i: Nat) -> Nat:
676 U32.to_nat(be32(h, (20n + 4n * i : Nat)))
677
678# The data block's size in bytes, for header h.
679def tzif.bsize(+t8: Bool, +h: String) -> Nat:
680 +tc = tzif.count(h, 3n)
681 (tc * tzif.size(t8) + tc + tzif.count(h, 4n) * 6n + tzif.count(h, 5n) +
682 tzif.count(h, 2n) * (tzif.size(t8) + 4n) + tzif.count(h, 1n) + tzif.count(h, 0n) : Nat)
683
684# h starts at a header; its data block follows it. Version 2+ blocks have 8-byte times and a footer.
685def tzif.block(+t8: Bool, +h: String) -> Maybe<&2, Zone>:
686 +d = String.drop(h, 44n)
687 +tc = tzif.count(h, 3n)
688 +ty = tzif.count(h, 4n)
689 +at = (tc * tzif.size(t8) + tc : Nat)
690 +foot = String.drop(d, tzif.bsize(t8, h))
691 tzif.if(Bool.and(String.starts_with(h, "TZif"), Bool.and(Nat.is_gt(ty, 0n),
692 Nat.is_le((44n + tzif.bsize(t8, h) : Nat), String.length(h)))),
693 Zone{tzif.trans(tc, t8, d, String.drop(d, (tc * tzif.size(t8) : Nat))),
694 tzif.types(ty, String.drop(d, at), String.take(String.drop(d, (at + ty * 6n : Nat)), tzif.count(h, 5n))),
695 Bool.pick(String, t8, name(String.split(foot, '\n'), 1), "")})
696
697def tzif.go(v2: Bool, +s: String) -> Maybe<&2, Zone>:
698 match v2:
699 case True{}:
700 tzif.block(True{}, String.drop(s, (44n + tzif.bsize(False{}, s) : Nat)))
701 case False{}:
702 tzif.block(False{}, s)
703
704# A TZif file, such as one from /usr/share/zoneinfo. Versions 2 and up use their 64-bit block.
705# ponytail: reads the bytes as a byte String; walk Bytes directly if zone files get big.
706def tzif.parse(b: Bytes.Bytes) -> Maybe<&2, Zone>:
707 +s = Bytes.to_string(b)
708 tzif.go(U32.is_ge(u8(s, 4n), 50), s)
709
710# POSIX TZ offsets are seconds west of UTC; transition times are seconds from local midnight.
711type TzField is Data:
712 TzField{value: U32, rest: String}
713
714type TzText is Data:
715 TzText{value: String, rest: String}
716
717type TzClock is Data:
718 TzClock{value: Int.I64, rest: String}
719
720type TzDay is Data:
721 Julian{day: U32}
722 Ordinal{day: U32}
723 MonthWeek{month: U32, week: U32, weekday: U32}
724
725type TzDate is Data:
726 TzDate{day: TzDay, seconds: Int.I64}
727
728type TzDayPart is Data:
729 TzDayPart{day: TzDay, rest: String}
730
731type TzDatePart is Data:
732 TzDatePart{date: TzDate, rest: String}
733
734type TzRule is Data:
735 TzRule{std: Ttype, daylight: Ttype, start: TzDate, end: TzDate}
736
737def tz.digit(+c: U32) -> Bool:
738 Bool.and(U32.is_ge(c, 48), U32.is_le(c, 57))
739
740def tz.alpha(+c: U32) -> Bool:
741 Bool.or(Bool.and(U32.is_ge(c, 65), U32.is_le(c, 90)),
742 Bool.and(U32.is_ge(c, 97), U32.is_le(c, 122)))
743
744def tz.quoted(+c: U32) -> Bool:
745 Bool.or(tz.alpha(c), Bool.or(tz.digit(c), Bool.or(U32.is_eq(c, 43), U32.is_eq(c, 45))))
746
747def tz.number.stop(seen: Bool, acc: U32, s: String) -> Maybe<&2, TzField>:
748 match seen:
749 case True{}:
750 Some{TzField{acc, s}}
751 case False{}:
752 None{}
753
754def tz.number.step(digit: Bool, c: U32, t: String, acc: U32, seen: Bool, next: Unit -> Maybe<&2, TzField>) -> Maybe<&2, TzField>:
755 match digit:
756 case True{}:
757 next(Unit{})
758 case False{}:
759 tz.number.stop(seen, acc, SCon{Chr{c}, t})
760
761# Three digits suffice for POSIX hour, day, and month fields.
762def tz.number.go(s: String, +acc: U32, +seen: Bool) -> Maybe<&2, TzField>:
763 match s:
764 case SNil{}:
765 tz.number.stop(seen, acc, SNil{})
766 case SCon{Chr{+c}, +t}:
767 tz.number.step(Bool.and(tz.digit(c), U32.is_lt(acc, 100)),
768 c, t, acc, seen, _ => tz.number.go(t, ((acc * 10 + c - 48) : U32), True{}))
769
770def tz.number(s: String) -> Maybe<&2, TzField>:
771 tz.number.go(s, 0, False{})
772
773def tz.name.valid(ok: Bool, name: String, rest: String) -> Maybe<&2, TzText>:
774 match ok:
775 case True{}:
776 Some{TzText{name, rest}}
777 case False{}:
778 None{}
779
780def tz.name.done(rev: String, rest: String) -> Maybe<&2, TzText>:
781 +name = String.reverse(rev)
782 tz.name.valid(Nat.is_ge(String.length(name), 3n), name, rest)
783
784def tz.name.empty(quoted: Bool, rev: String) -> Maybe<&2, TzText>:
785 match quoted:
786 case True{}:
787 None{}
788 case False{}:
789 tz.name.done(rev, SNil{})
790
791def tz.name.branch(continue: Bool, rev: String, c: U32, rest: String, next: Unit -> Maybe<&2, TzText>) -> Maybe<&2, TzText>:
792 match continue:
793 case True{}:
794 next(Unit{})
795 case False{}:
796 tz.name.done(rev, SCon{Chr{c}, rest})
797
798def tz.name.allowed(ok: Bool, next: Unit -> Maybe<&2, TzText>) -> Maybe<&2, TzText>:
799 match ok:
800 case True{}:
801 next(Unit{})
802 case False{}:
803 None{}
804
805def tz.name.quoted(end: Bool, valid: Bool, rev: String, rest: String, next: Unit -> Maybe<&2, TzText>) -> Maybe<&2, TzText>:
806 match end:
807 case True{}:
808 tz.name.done(rev, rest)
809 case False{}:
810 tz.name.allowed(valid, next)
811
812def tz.name.char(quoted: Bool, end: Bool, alpha: Bool, valid: Bool, rev: String, c: U32, rest: String,
813 next: Unit -> Maybe<&2, TzText>) -> Maybe<&2, TzText>:
814 match quoted:
815 case True{}:
816 tz.name.quoted(end, valid, rev, rest, next)
817 case False{}:
818 tz.name.branch(alpha, rev, c, rest, next)
819
820def tz.name.go(s: String, +rev: String, +quoted: Bool) -> Maybe<&2, TzText>:
821 match s:
822 case SNil{}:
823 tz.name.empty(quoted, rev)
824 case SCon{Chr{+c}, +t}:
825 tz.name.char(quoted, U32.is_eq(c, 62), tz.alpha(c), tz.quoted(c), rev, c, t,
826 _ => tz.name.go(t, SCon{Chr{c}, rev}, quoted))
827
828def tz.name(s: String) -> Maybe<&2, TzText>:
829 match s:
830 case SCon{Chr{60}, t}:
831 tz.name.go(t, SNil{}, True{})
832 case _:
833 tz.name.go(s, SNil{}, False{})
834
835def tz.field.valid(ok: Bool, n: U32, rest: String) -> Maybe<&2, TzField>:
836 match ok:
837 case True{}:
838 Some{TzField{n, rest}}
839 case False{}:
840 None{}
841
842def tz.clock.tail(r: TzField, limit: U32) -> Maybe<&2, TzField>:
843 match r:
844 case TzField{+n, rest}:
845 tz.field.valid(U32.is_le(n, limit), n, rest)
846
847def tz.clock.part(s: String) -> Maybe<&2, TzField>:
848 match s:
849 case SCon{Chr{58}, t}:
850 do Maybe<&2, TzField>:
851 n : TzField <- tz.number(t)
852 tz.clock.tail(n, 59)
853 case _:
854 Some{TzField{0, s}}
855
856def tz.clock.valid(ok: Bool, +value: Int.I64, negative: Bool, rest: String) -> Maybe<&2, TzClock>:
857 match ok:
858 case False{}:
859 None{}
860 case True{}:
861 Some{TzClock{Bool.pick(Int.I64, negative, Int.I64.neg(value), value), rest}}
862
863def tz.clock.seconds(sec: TzField, +hours: U32, +minutes: U32, +max: U32, negative: Bool) -> Maybe<&2, TzClock>:
864 match sec:
865 case TzField{+seconds, rest}:
866 tz.clock.valid(U32.is_le(hours, max),
867 i64((hours * 3600 + minutes * 60 + seconds : U32)), negative, rest)
868
869def tz.clock.minutes(m: TzField, +hours: U32, +max: U32, +negative: Bool) -> Maybe<&2, TzClock>:
870 match m:
871 case TzField{+minutes, rest}:
872 do Maybe<&2, TzClock>:
873 sec : TzField <- tz.clock.part(rest)
874 tz.clock.seconds(sec, hours, minutes, max, negative)
875def tz.clock.finish(h: TzField, +max: U32, +negative: Bool) -> Maybe<&2, TzClock>:
876 match h:
877 case TzField{+hours, rest}:
878 do Maybe<&2, TzClock>:
879 m : TzField <- tz.clock.part(rest)
880 tz.clock.minutes(m, hours, max, negative)
881
882
883def tz.clock.read(s: String, max: U32, negative: Bool) -> Maybe<&2, TzClock>:
884 do Maybe<&2, TzClock>:
885 h : TzField <- tz.number(s)
886 tz.clock.finish(h, max, negative)
887def tz.clock.sign(s: String, max: U32) -> Maybe<&2, TzClock>:
888 match s:
889 case SCon{Chr{45}, t}:
890 tz.clock.read(t, max, True{})
891 case SCon{Chr{43}, t}:
892 tz.clock.read(t, max, False{})
893 case _:
894 tz.clock.read(s, max, False{})
895
896
897def tz.day.valid(ok: Bool, d: TzDay, rest: String) -> Maybe<&2, TzDayPart>:
898 match ok:
899 case True{}:
900 Some{TzDayPart{d, rest}}
901 case False{}:
902 None{}
903
904def tz.day.j(r: TzField) -> Maybe<&2, TzDayPart>:
905 match r:
906 case TzField{+n, rest}:
907 tz.day.valid(Bool.and(U32.is_ge(n, 1), U32.is_le(n, 365)), Julian{n}, rest)
908
909def tz.day.n(r: TzField) -> Maybe<&2, TzDayPart>:
910 match r:
911 case TzField{+n, rest}:
912 tz.day.valid(U32.is_le(n, 365), Ordinal{n}, rest)
913
914def tz.after(c: Char, s: String) -> String:
915 match s:
916 case SCon{h, t}:
917 Bool.pick(String, Char.is_eq(h, c), t, SNil{})
918 case SNil{}:
919 SNil{}
920
921def tz.day.weekday(c: TzField, +month: U32, +week: U32) -> Maybe<&2, TzDayPart>:
922 match c:
923 case TzField{+weekday, rest}:
924 tz.day.valid(Bool.and(U32.is_ge(month, 1), Bool.and(U32.is_le(month, 12),
925 Bool.and(U32.is_ge(week, 1), Bool.and(U32.is_le(week, 5), U32.is_le(weekday, 6))))),
926 MonthWeek{month, week, weekday}, rest)
927
928def tz.day.week(b: TzField, month: U32) -> Maybe<&2, TzDayPart>:
929 match b:
930 case TzField{week, rest}:
931 do Maybe<&2, TzDayPart>:
932 c : TzField <- tz.number(tz.after('.', rest))
933 tz.day.weekday(c, month, week)
934
935def tz.day.month(a: TzField) -> Maybe<&2, TzDayPart>:
936 match a:
937 case TzField{month, rest}:
938 do Maybe<&2, TzDayPart>:
939 b : TzField <- tz.number(tz.after('.', rest))
940 tz.day.week(b, month)
941
942def tz.day.m(s: String) -> Maybe<&2, TzDayPart>:
943 do Maybe<&2, TzDayPart>:
944 a : TzField <- tz.number(s)
945 tz.day.month(a)
946
947def tz.day(s: String) -> Maybe<&2, TzDayPart>:
948 match s:
949 case SCon{Chr{74}, t}:
950 do Maybe<&2, TzDayPart>:
951 n : TzField <- tz.number(t)
952 tz.day.j(n)
953 case SCon{Chr{77}, t}:
954 tz.day.m(t)
955 case _:
956 do Maybe<&2, TzDayPart>:
957 n : TzField <- tz.number(s)
958 tz.day.n(n)
959
960def tz.date.clock(d: TzDay, r: TzClock) -> Maybe<&2, TzDatePart>:
961 match r:
962 case TzClock{secs, end}:
963 Some{TzDatePart{TzDate{d, secs}, end}}
964
965def tz.date.time(d: TzDay, rest: String) -> Maybe<&2, TzDatePart>:
966 match rest:
967 case SCon{Chr{47}, t}:
968 do Maybe<&2, TzDatePart>:
969 r : TzClock <- tz.clock.sign(t, 167)
970 tz.date.clock(d, r)
971 case _:
972 Some{TzDatePart{TzDate{d, i64(7200)}, rest}}
973
974def tz.date.part(r: TzDayPart) -> Maybe<&2, TzDatePart>:
975 match r:
976 case TzDayPart{d, rest}:
977 tz.date.time(d, rest)
978
979def tz.date(s: String) -> Maybe<&2, TzDatePart>:
980 do Maybe<&2, TzDatePart>:
981 r : TzDayPart <- tz.day(s)
982 tz.date.part(r)
983
984def tz.rule.end(ok: Bool, standard: Ttype, daylight: Ttype, start: TzDate, end: TzDate) -> Maybe<&2, TzRule>:
985 match ok:
986 case True{}:
987 Some{TzRule{standard, daylight, start, end}}
988 case False{}:
989 None{}
990
991def tz.rule.finish(b: TzDatePart, standard: Ttype, daylight: Ttype, start: TzDate) -> Maybe<&2, TzRule>:
992 match b:
993 case TzDatePart{end, rest}:
994 tz.rule.end(String.is_empty(rest), standard, daylight, start, end)
995
996def tz.rule.start(a: TzDatePart, +standard: Ttype, +daylight: Ttype) -> Maybe<&2, TzRule>:
997 match a:
998 case TzDatePart{start, rest}:
999 do Maybe<&2, TzRule>:
1000 b : TzDatePart <- tz.date(tz.after(',', rest))
1001 tz.rule.finish(b, standard, daylight, start)
1002
1003def tz.rule.dates(+standard: Ttype, +daylight: Ttype, rest: String) -> Maybe<&2, TzRule>:
1004 do Maybe<&2, TzRule>:
1005 a : TzDatePart <- tz.date(tz.after(',', rest))
1006 tz.rule.start(a, standard, daylight)
1007
1008def tz.rule.dstclock(r: TzClock, standard: Ttype, abbr: String) -> Maybe<&2, TzRule>:
1009 match r:
1010 case TzClock{west, rest}:
1011 tz.rule.dates(standard, Ttype{Int.I64.neg(west), True{}, abbr}, rest)
1012
1013def tz.rule.offset(standard: Ttype, abbr: String, west: Int.I64, rest: String) -> Maybe<&2, TzRule>:
1014 match rest:
1015 case SCon{Chr{44}, t}:
1016 tz.rule.dates(standard, Ttype{Int.I64.sub(i64(3600), west), True{}, abbr}, rest)
1017 # POSIX leaves absent DST dates to the implementation; use the common US rules.
1018 case SNil{}:
1019 tz.rule.end(True{}, standard, Ttype{Int.I64.sub(i64(3600), west), True{}, abbr},
1020 TzDate{MonthWeek{3, 2, 0}, i64(7200)}, TzDate{MonthWeek{11, 1, 0}, i64(7200)})
1021 case _:
1022 do Maybe<&2, TzRule>:
1023 r : TzClock <- tz.clock.sign(rest, 24)
1024 tz.rule.dstclock(r, standard, abbr)
1025
1026def tz.rule.named(name: TzText, standard: Ttype, west: Int.I64) -> Maybe<&2, TzRule>:
1027 match name:
1028 case TzText{abbr, rest}:
1029 tz.rule.offset(standard, abbr, west, rest)
1030
1031def tz.rule.dst(+standard: Ttype, west: Int.I64, rest: String) -> Maybe<&2, TzRule>:
1032 match rest:
1033 case SNil{}:
1034 Some{TzRule{standard, standard, TzDate{Ordinal{0}, i64(0)}, TzDate{Ordinal{0}, i64(0)}}}
1035 case _:
1036 do Maybe<&2, TzRule>:
1037 name : TzText <- tz.name(rest)
1038 tz.rule.named(name, standard, west)
1039
1040def tz.rule.stdclock(offset: TzClock, abbr: String) -> Maybe<&2, TzRule>:
1041 match offset:
1042 case TzClock{+west, rest}:
1043 tz.rule.dst(Ttype{Int.I64.neg(west), False{}, abbr}, west, rest)
1044
1045def tz.rule.standard(name: TzText) -> Maybe<&2, TzRule>:
1046 match name:
1047 case TzText{abbr, rest}:
1048 do Maybe<&2, TzRule>:
1049 offset : TzClock <- tz.clock.sign(rest, 24)
1050 tz.rule.stdclock(offset, abbr)
1051
1052def tz.rule(s: String) -> Maybe<&2, TzRule>:
1053 do Maybe<&2, TzRule>:
1054 name : TzText <- tz.name(s)
1055 tz.rule.standard(name)
1056
1057# The day number of a rule in year y, relative to January 1.
1058def tz.day.index(d: TzDay, +y: U32) -> U32:
1059 match d:
1060 case Julian{+n}:
1061 (n - 1 + Bool.pick(U32, Bool.and(Date.is_leap(y), U32.is_ge(n, 60)), 1, 0) : U32)
1062 case Ordinal{n}:
1063 n
1064 case MonthWeek{+month, +week, +weekday}:
1065 +first_day = (Date.weekday(Date{y, month, 1}) % 7 : U32)
1066 +day = (1 + ((weekday + 7 - first_day) % 7) + (week - 1) * 7 : U32)
1067 +last = Date.days_in_month(y, month)
1068 +actual = Bool.pick(U32, U32.is_gt(day, last), (day - 7 : U32), day)
1069 Int.I64.to_u32(Int.I64.sub(Date.to_days(Date{y, month, actual}), Date.to_days(Date{y, 1, 1})))
1070
1071def tz.date.utc(d: TzDate, +y: U32, west: Int.I64) -> Int.I64:
1072 match d:
1073 case TzDate{day, sec}:
1074 Int.I64.add(Int.I64.mul(Int.I64.add(Date.to_days(Date{y, 1, 1}), i64(tz.day.index(day, y))), i64(86400)),
1075 Int.I64.add(sec, west))
1076
1077# Apply the two transitions for the UTC year and its neighbors. A /time may cross a year boundary.
1078type TzEvent is Data:
1079 TzEvent{when: Int.I64, dst: Bool}
1080
1081def tz.event.select(newer: Bool, old: Maybe<&2, TzEvent>, when: Int.I64, dst: Bool) -> Maybe<&2, TzEvent>:
1082 match newer:
1083 case True{}:
1084 Some{TzEvent{when, dst}}
1085 case False{}:
1086 old
1087
1088def tz.event.new(+now: Int.I64, old: Maybe<&2, TzEvent>, +when: Int.I64, dst: Bool) -> Maybe<&2, TzEvent>:
1089 match old:
1090 case None{}:
1091 tz.event.select(Int.I64.is_le(when, now), None{}, when, dst)
1092 case Some{TzEvent{+prev, flag}}:
1093 tz.event.select(Bool.and(Int.I64.is_le(when, now), Int.I64.is_gt(when, prev)),
1094 Some{TzEvent{prev, flag}}, when, dst)
1095
1096def tz.event.year(+now: Int.I64, old: Maybe<&2, TzEvent>, +r: TzRule, +y: U32) -> Maybe<&2, TzEvent>:
1097 match r:
1098 case TzRule{Ttype{+off, _, _}, Ttype{+dstoff, _, _}, +start, +end}:
1099 +first = tz.event.new(now, old, tz.date.utc(start, y, Int.I64.neg(off)), True{})
1100 tz.event.new(now, first, tz.date.utc(end, y, Int.I64.neg(dstoff)), False{})
1101
1102def tz.event.prev(+now: Int.I64, old: Maybe<&2, TzEvent>, +r: TzRule, +y: U32) -> Maybe<&2, TzEvent>:
1103 match y:
1104 case 0:
1105 old
1106 case _:
1107 tz.event.year(now, old, r, (y - 1 : U32))
1108
1109def tz.event.next.if(valid: Bool, now: Int.I64, old: Maybe<&2, TzEvent>, r: TzRule, y: U32) -> Maybe<&2, TzEvent>:
1110 match valid:
1111 case True{}:
1112 tz.event.year(now, old, r, (y + 1 : U32))
1113 case False{}:
1114 old
1115def tz.event.next(+now: Int.I64, old: Maybe<&2, TzEvent>, +r: TzRule, +y: U32) -> Maybe<&2, TzEvent>:
1116 tz.event.next.if(U32.is_lt(y, 9999), now, old, r, y)
1117
1118
1119def tz.event.type(ev: Maybe<&2, TzEvent>, +r: TzRule) -> Ttype:
1120 match ev:
1121 case Some{TzEvent{when, dst}}:
1122 match r:
1123 case TzRule{standard, daylight, start, end}:
1124 Bool.pick(Ttype, dst, daylight, standard)
1125 case None{}:
1126 match r:
1127 case TzRule{standard, daylight, start, end}:
1128 standard
1129
1130def tz.rule.at(+r: TzRule, +secs: Int.I64, +year: U32) -> Ttype:
1131 +a = tz.event.prev(secs, None{}, r, year)
1132 +b = tz.event.year(secs, a, r, year)
1133 tz.event.type(tz.event.next(secs, b, r, year), r)
1134
1135def tz.rule.date(d: Maybe<&2, DateTime>, r: TzRule, secs: Int.I64) -> Maybe<&2, Ttype>:
1136 match d:
1137 case None{}:
1138 None{}
1139 case Some{DateTime{Date{y, m, day}, h, mi, second, nanos}}:
1140 Some{tz.rule.at(r, secs, y)}
1141
1142def tz.rule.lookup(rule: Maybe<&2, TzRule>, +secs: Int.I64) -> Maybe<&2, Ttype>:
1143 match rule:
1144 case None{}:
1145 None{}
1146 case Some{r}:
1147 tz.rule.date(DateTime.of_instant(Instant.of_unix(secs)), r, secs)
1148
1149# The type index at secs: the last transition at or before it, or type 0 before the first.
1150# ponytail: linear scan; bisect an Array if lookups get hot.
1151def Zone.find(ts: List<&2, Trans>, +secs: Int.I64, +cur: U32) -> U32:
1152 match ts:
1153 case Nil{}:
1154 cur
1155 case Con{Trans{t, k}, rest}:
1156 Zone.find(rest, secs, Bool.pick(U32, Int.I64.is_le(t, secs), k, cur))
1157def Zone.last.go(ts: List<&2, Trans>, +secs: Int.I64, +last: Int.I64) -> Bool:
1158 match ts:
1159 case Nil{}:
1160 Int.I64.is_gt(secs, last)
1161 case Con{Trans{t, k}, rest}:
1162 Zone.last.go(rest, secs, t)
1163def Zone.last(ts: List<&2, Trans>, secs: Int.I64) -> Bool:
1164 match ts:
1165 case Nil{}:
1166 True{}
1167 case Con{Trans{t, k}, rest}:
1168 Zone.last.go(rest, secs, t)
1169
1170
1171def Zone.at.fallback(m: Maybe<&2, Ttype>, types: List<&2, Ttype>, ts: List<&2, Trans>, secs: Int.I64) -> Maybe<&2, Ttype>:
1172 match m:
1173 case Some{t}:
1174 Some{t}
1175 case None{}:
1176 List.get(&2, Ttype, types, U32.to_nat(Zone.find(ts, secs, 0)))
1177def Zone.at.footer(use: Bool, tz: String, types: List<&2, Ttype>, ts: List<&2, Trans>, +secs: Int.I64) -> Maybe<&2, Ttype>:
1178 match use:
1179 case False{}:
1180 List.get(&2, Ttype, types, U32.to_nat(Zone.find(ts, secs, 0)))
1181 case True{}:
1182 Zone.at.fallback(tz.rule.lookup(tz.rule(tz), secs), types, ts, secs)
1183
1184def Zone.at.tz(empty: Bool, tz: String, types: List<&2, Ttype>, +ts: List<&2, Trans>, +secs: Int.I64) -> Maybe<&2, Ttype>:
1185 match empty:
1186 case True{}:
1187 List.get(&2, Ttype, types, U32.to_nat(Zone.find(ts, secs, 0)))
1188 case False{}:
1189 Zone.at.footer(Zone.last(ts, secs), tz, types, ts, secs)
1190
1191
1192
1193# The local time type at i. The footer applies strictly after the final explicit transition.
1194def Zone.at(z: Zone, i: Instant) -> Maybe<&2, Ttype>:
1195 match z i:
1196 case Zone{ts, types, +tz} Instant{s, n}:
1197 Zone.at.tz(String.eq(tz, ""), tz, types, ts, s)
1198
1199def Zone.local.at(m: Maybe<&2, Ttype>, i: Instant) -> Maybe<&2, DateTime>:
1200 match m:
1201 case None{}:
1202 None{}
1203 case Some{Ttype{off, dst, abbr}}:
1204 DateTime.of_instant(Instant.add(i, Duration.of_secs(off)))
1205
1206# The local date and time at i in zone z.
1207def Zone.local(z: Zone, +i: Instant) -> Maybe<&2, DateTime>:
1208 Zone.local.at(Zone.at(z, i), i)