time.bend
bend-kit-time@0.1.1.0 · 704 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.carry(c: Bool, s: Int.I64, +n: U32) -> Duration:
55 match c:
56 case True{}:
57 Duration{Int.I64.add(s, i64(1)), (n - 1000000000 : U32)}
58 case False{}:
59 Duration{s, n}
60
61def Duration.add(a: Duration, b: Duration) -> Duration:
62 match a b:
63 case Duration{sa, na} Duration{sb, nb}:
64 +n = (na + nb : U32)
65 Duration.carry(U32.is_ge(n, 1000000000), Int.I64.add(sa, sb), n)
66
67# n is na - nb, wrapped when na < nb.
68def Duration.borrow(c: Bool, s: Int.I64, +n: U32) -> Duration:
69 match c:
70 case True{}:
71 Duration{Int.I64.sub(s, i64(1)), (n + 1000000000 : U32)}
72 case False{}:
73 Duration{s, n}
74
75def Duration.sub(a: Duration, b: Duration) -> Duration:
76 match a b:
77 case Duration{sa, +na} Duration{sb, +nb}:
78 Duration.borrow(U32.is_lt(na, nb), Int.I64.sub(sa, sb), (na - nb : U32))
79
80def Duration.neg(d: Duration) -> Duration:
81 Duration.sub(Duration.zero(), d)
82
83def Duration.cmp.then(c: Cmp, +na: U32, +nb: U32) -> Cmp:
84 match c:
85 case EQ{}:
86 U32.cmp(na, nb)
87 case LT{}:
88 LT{}
89 case GT{}:
90 GT{}
91
92def Duration.cmp(a: Duration, b: Duration) -> Cmp:
93 match a b:
94 case Duration{sa, na} Duration{sb, nb}:
95 Duration.cmp.then(Int.I64.cmp(sa, sb), na, nb)
96
97# Instant
98# -------
99
100def Instant.epoch() -> Instant:
101 Instant{i64(0), 0}
102
103def Instant.of_unix(s: Int.I64) -> Instant:
104 Instant{s, 0}
105
106def Instant.of(d: Duration) -> Instant:
107 match d:
108 case Duration{s, n}:
109 Instant{s, n}
110
111def Instant.since_epoch(i: Instant) -> Duration:
112 match i:
113 case Instant{s, n}:
114 Duration{s, n}
115
116def Instant.add(i: Instant, d: Duration) -> Instant:
117 Instant.of(Duration.add(Instant.since_epoch(i), d))
118
119# a - b.
120def Instant.since(a: Instant, b: Instant) -> Duration:
121 Duration.sub(Instant.since_epoch(a), Instant.since_epoch(b))
122
123def Instant.cmp(a: Instant, b: Instant) -> Cmp:
124 Duration.cmp(Instant.since_epoch(a), Instant.since_epoch(b))
125
126# Clocks
127# ------
128
129# (secs hi, secs lo, nanos) of CLOCK_MONOTONIC, from an unspecified start.
130def mono.raw() -> IO(U32 & U32 & U32):
131 import "./effs/time.c"
132 import "./effs/time.js"
133
134# (secs hi, secs lo, nanos) of CLOCK_REALTIME, since the Unix epoch.
135def wall.raw() -> IO(U32 & U32 & U32):
136 import "./effs/time.c"
137 import "./effs/time.js"
138
139def raw.dur(r: U32 & U32 & U32) -> Duration:
140 (hi, lo, n) = r
141 Duration{i64.of(hi, lo), n}
142
143# Time since an unspecified start that never goes back. Use it to measure spans.
144def mono() -> IO(Duration):
145 do IO<Duration>:
146 r : U32 & U32 & U32 <- mono.raw()
147 return raw.dur(r)
148
149# The wall clock. It can jump when the system time is set.
150def now() -> IO(Instant):
151 do IO<Instant>:
152 r : U32 & U32 & U32 <- wall.raw()
153 return Instant.of(raw.dur(r))
154
155# Dates
156# -----
157
158def Date.is_leap(+y: U32) -> Bool:
159 Bool.and(U32.is_eq((y % 4 : U32), 0),
160 Bool.or(U32.is_ne((y % 100 : U32), 0), U32.is_eq((y % 400 : U32), 0)))
161
162# 0 for a month outside 1 to 12.
163def Date.days_in_month(+y: U32, +m: U32) -> U32:
164 Bool.pick(U32, U32.is_eq(m, 2), Bool.pick(U32, Date.is_leap(y), 29, 28),
165 Bool.pick(U32, Bool.and(U32.is_ge(m, 1), U32.is_le(m, 12)),
166 (30 + ((m + (m >> 3n)) .&. 1) : U32), 0))
167
168def Date.valid(d: Date) -> Bool:
169 match d:
170 case Date{+y, +m, +dd}:
171 Bool.and(U32.is_le(y, 9999),
172 Bool.and(U32.is_ge(dd, 1), U32.is_le(dd, Date.days_in_month(y, m))))
173
174# z counts days from -0400-03-01, so every date from year 0 has z > 0 in a U32.
175# The civil-days algorithm is Howard Hinnant's, with the year starting in March.
176def Z.EPOCH() -> U32:
177 865565
178
179def Date.to_z.at(+y: U32, +mp: U32, +d: U32) -> U32:
180 +era = (y / 400 : U32)
181 +yoe = (y - era * 400 : U32)
182 +doy = ((153 * mp + 2) / 5 + d - 1 : U32)
183 (era * 146097 + yoe * 365 + yoe / 4 - yoe / 100 + doy : U32)
184
185def Date.to_z.go(jf: Bool, +y: U32, +m: U32, +d: U32) -> U32:
186 match jf:
187 case True{}:
188 Date.to_z.at((y + 399 : U32), (m + 9 : U32), d)
189 case False{}:
190 Date.to_z.at((y + 400 : U32), (m - 3 : U32), d)
191
192def Date.to_z(d: Date) -> U32:
193 match d:
194 case Date{+y, +m, +dd}:
195 Date.to_z.go(U32.is_le(m, 2), y, m, dd)
196
197def Date.of_z.fin(lo: Bool, +y: U32, +mp: U32, +d: U32) -> Date:
198 match lo:
199 case True{}:
200 Date{(y - 400 : U32), (mp + 3 : U32), d}
201 case False{}:
202 Date{(y - 399 : U32), (mp - 9 : U32), d}
203
204def Date.of_z(+z: U32) -> Date:
205 +era = (z / 146097 : U32)
206 +doe = (z - era * 146097 : U32)
207 +yoe = ((doe - doe / 1460 + doe / 36524 - doe / 146096) / 365 : U32)
208 +doy = (doe - (365 * yoe + yoe / 4 - yoe / 100) : U32)
209 +mp = ((5 * doy + 2) / 153 : U32)
210 Date.of_z.fin(U32.is_lt(mp, 10), (yoe + era * 400 : U32), mp,
211 (doy - (153 * mp + 2) / 5 + 1 : U32))
212
213# Days since 1970-01-01.
214def Date.to_days(d: Date) -> Int.I64:
215 Int.I64.sub(i64(Date.to_z(d)), i64(Z.EPOCH()))
216
217def Date.of_z.if(ok: Bool, +z: U32) -> Maybe<&2, Date>:
218 match ok:
219 case True{}:
220 Some{Date.of_z(z)}
221 case False{}:
222 None{}
223
224# The date days after 1970-01-01, or None outside 0000-01-01 to 9999-12-31.
225def Date.of_days(days: Int.I64) -> Maybe<&2, Date>:
226 +z = Int.I64.add(days, i64(Z.EPOCH()))
227 Date.of_z.if(Bool.and(Int.I64.is_ge(z, i64(146037)), Int.I64.is_le(z, i64(3798461))),
228 Int.I64.to_u32(z))
229
230# 1 for Monday to 7 for Sunday, as in ISO 8601.
231def Date.weekday(d: Date) -> U32:
232 ((Date.to_z(d) + 2) % 7 + 1 : U32)
233
234# Date and time
235# -------------
236
237def DateTime.valid(t: DateTime) -> Bool:
238 match t:
239 case DateTime{d, h, mi, s, n}:
240 Bool.and(Date.valid(d), Bool.and(U32.is_le(h, 23),
241 Bool.and(U32.is_le(mi, 59), Bool.and(U32.is_le(s, 59), U32.is_lt(n, 1000000000)))))
242
243# The instant of a UTC date and time. It does not check t; see DateTime.valid.
244def DateTime.to_instant(t: DateTime) -> Instant:
245 match t:
246 case DateTime{d, h, mi, s, n}:
247 Instant{Int.I64.add(Int.I64.mul(Date.to_days(d), i64(86400)),
248 i64((h * 3600 + mi * 60 + s : U32))), n}
249
250def DateTime.at(m: Maybe<&2, Date>, +sod: U32, n: U32) -> Maybe<&2, DateTime>:
251 match m:
252 case None{}:
253 None{}
254 case Some{d}:
255 Some{DateTime{d, (sod / 3600 : U32), (sod / 60 % 60 : U32), (sod % 60 : U32), n}}
256
257# r is secs % 86400, which has the sign of secs.
258def DateTime.floor(neg: Bool, q: Int.I64, r: Int.I64, n: U32) -> Maybe<&2, DateTime>:
259 match neg:
260 case True{}:
261 DateTime.at(Date.of_days(Int.I64.sub(q, i64(1))), (Int.I64.to_u32(r) + 86400 : U32), n)
262 case False{}:
263 DateTime.at(Date.of_days(q), Int.I64.to_u32(r), n)
264
265# The UTC date and time of i, or None outside years 0 to 9999.
266def DateTime.of_instant(i: Instant) -> Maybe<&2, DateTime>:
267 match i:
268 case Instant{+s, n}:
269 +r = Int.I64.mod(s, i64(86400))
270 DateTime.floor(Int.I64.is_neg(r), Int.I64.div(s, i64(86400)), r, n)
271
272# Text
273# ----
274
275def pad(+x: U32, w: Nat) -> String:
276 Fmt.Fmt.pad_left(U32.show(x), w, '0')
277
278# Milliseconds with six decimal places.
279def Duration.show_ms.pos(d: Duration) -> String:
280 match d:
281 case Duration{s, +n}:
282 Int.I64.show(Duration.to_ms(Duration{s, n})) ++ "." ++ pad((n % 1000000 : U32), 6n)
283
284def Duration.show_ms.sign(neg: Bool, d: Duration) -> String:
285 match neg:
286 case True{}:
287 "-" ++ Duration.show_ms.pos(Duration.neg(d))
288 case False{}:
289 Duration.show_ms.pos(d)
290
291def Duration.show_ms(d: Duration) -> String:
292 match d:
293 case Duration{+s, n}:
294 Duration.show_ms.sign(Int.I64.is_neg(s), Duration{s, n})
295
296# The digits of n / 10^(9 - w), with trailing zeros cut. n is not 0.
297def frac.go(f: Nat, z: Bool, +n: U32, +w: Nat) -> String:
298 match f:
299 case 0n:
300 pad(n, w)
301 case 1n+g:
302 match z:
303 case True{}:
304 +m = (n / 10 : U32)
305 frac.go(g, U32.is_eq((m % 10 : U32), 0), m, (w - 1n : Nat))
306 case False{}:
307 pad(n, w)
308
309def frac(+n: U32) -> String:
310 Bool.pick(String, U32.is_eq(n, 0), "", SCon{'.', frac.go(8n, U32.is_eq((n % 10 : U32), 0), n, 9n)})
311
312def DateTime.rfc3339(t: DateTime) -> String:
313 match t:
314 case DateTime{Date{y, mo, d}, h, mi, s, n}:
315 String.concat([pad(y, 4n), "-", pad(mo, 2n), "-", pad(d, 2n), "T", pad(h, 2n), ":",
316 pad(mi, 2n), ":", pad(s, 2n), frac(n), "Z"])
317
318def fmt.map(~f: DateTime -> String, m: Maybe<&2, DateTime>) -> Maybe<&2, String>:
319 match m:
320 case None{}:
321 None{}
322 case Some{t}:
323 Some{f(t)}
324
325# RFC 3339 in UTC, such as 1985-04-12T23:20:50.52Z. The fraction has no trailing zeros, and is left out when 0.
326def rfc3339(i: Instant) -> Maybe<&2, String>:
327 fmt.map(~DateTime.rfc3339, DateTime.of_instant(i))
328
329def WEEKDAYS() -> List<&2, String>:
330 ["Mon", "Tue", "Wed", "Thu", "Fri", "Sat", "Sun"]
331
332def MONTHS() -> List<&2, String>:
333 ["Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"]
334
335def name(xs: List<&2, String>, +i: U32) -> String:
336 Maybe.default(&2, String, List.get(&2, String, xs, U32.to_nat(i)), "")
337
338def DateTime.http_date(t: DateTime) -> String:
339 match t:
340 case DateTime{+date, h, mi, s, n}:
341 Date{y, mo, d} = date
342 String.concat([name(WEEKDAYS(), (Date.weekday(date) - 1 : U32)), ", ", pad(d, 2n), " ",
343 name(MONTHS(), (mo - 1 : U32)), " ", pad(y, 4n), " ", pad(h, 2n), ":", pad(mi, 2n), ":",
344 pad(s, 2n), " GMT"])
345
346# IMF-fixdate (RFC 9110 §5.6.7), such as Sun, 06 Nov 1994 08:49:37 GMT. It drops the fraction of a second.
347def http_date(i: Instant) -> Maybe<&2, String>:
348 fmt.map(~DateTime.http_date, DateTime.of_instant(i))
349
350# Parsers
351# -------
352
353# A parser state: the numbers read so far, newest first, and the text left.
354type P is Data:
355 P{vals: List<&2, U32>, rest: String}
356
357def is_digit(+c: U32) -> Bool:
358 Bool.and(U32.is_ge(c, 48), U32.is_le(c, 57))
359
360def digits.go(n: Nat, s: String, +acc: U32, ok: Bool) -> Maybe<&1, U32 & String>:
361 match n:
362 case 0n:
363 match ok:
364 case True{}:
365 Some{(acc, s)}
366 case False{}:
367 None{}
368 case 1n+k:
369 match s:
370 case SNil{}:
371 None{}
372 case SCon{Chr{+c}, t}:
373 digits.go(k, t, (acc * 10 + c - 48 : U32), Bool.and(ok, is_digit(c)))
374
375def push(vs: List<&2, U32>, r: Maybe<&1, U32 & String>) -> Maybe<&2, P>:
376 match r:
377 case None{}:
378 None{}
379 case Some{(v, t)}:
380 Some{P{Con{v, vs}, t}}
381
382# Exactly n digits.
383def num(n: Nat, p: P) -> Maybe<&2, P>:
384 match p:
385 case P{vs, s}:
386 push(vs, digits.go(n, s, 0, True{}))
387
388def lit.if(ok: Bool, vs: List<&2, U32>, t: String) -> Maybe<&2, P>:
389 match ok:
390 case True{}:
391 Some{P{vs, t}}
392 case False{}:
393 None{}
394
395# One char that is a or b.
396def lit2(+a: U32, +b: U32, p: P) -> Maybe<&2, P>:
397 match p:
398 case P{vs, s}:
399 match s:
400 case SNil{}:
401 None{}
402 case SCon{Chr{+c}, t}:
403 lit.if(Bool.or(U32.is_eq(c, a), U32.is_eq(c, b)), vs, t)
404
405def lit(+c: U32, p: P) -> Maybe<&2, P>:
406 lit2(c, c, p)
407
408def text(+w: String, p: P) -> Maybe<&2, P>:
409 match p:
410 case P{vs, +s}:
411 +n = String.length(w)
412 lit.if(String.eq(String.take(s, n), w), vs, String.drop(s, n))
413
414def at.head(+s: String) -> Bool:
415 match s:
416 case SNil{}:
417 False{}
418 case SCon{Chr{+c}, t}:
419 is_digit(c)
420
421# Digits after the first nine are read and dropped. d says whether s starts with a digit.
422def secfrac.go(s: String, d: Bool, +mul: U32, +acc: U32, +k: U32) -> U32 & U32 & String:
423 match s:
424 case SNil{}:
425 (k, acc, SNil{})
426 case SCon{Chr{+c}, +t}:
427 match d:
428 case True{}:
429 secfrac.go(t, at.head(t), (mul / 10 : U32), (acc + (c - 48) * mul : U32), (k + 1 : U32))
430 case False{}:
431 (k, acc, SCon{Chr{c}, t})
432
433def secfrac.fin(vs: List<&2, U32>, r: U32 & U32 & String) -> Maybe<&2, P>:
434 (k, n, t) = r
435 lit.if(U32.is_gt(k, 0), Con{n, vs}, t)
436
437def secfrac.if(dot: Bool, vs: List<&2, U32>, +s: String) -> Maybe<&2, P>:
438 match dot:
439 case True{}:
440 +t = String.drop(s, 1n)
441 secfrac.fin(vs, secfrac.go(t, at.head(t), 100000000, 0, 0))
442 case False{}:
443 Some{P{Con{0, vs}, s}}
444
445# An optional '.' and one or more digits, as nanoseconds.
446def secfrac(p: P) -> Maybe<&2, P>:
447 match p:
448 case P{vs, +s}:
449 secfrac.if(String.starts_with(s, "."), vs, s)
450
451def zone.num(+neg: U32, vs: List<&2, U32>, t: String) -> Maybe<&2, P>:
452 do Maybe<&2, P>:
453 a : P <- num(2n, P{Con{neg, vs}, t})
454 b : P <- lit(58, a)
455 num(2n, b)
456
457def zone.if(z: Bool, plus: Bool, minus: Bool, vs: List<&2, U32>, t: String) -> Maybe<&2, P>:
458 match z:
459 case True{}:
460 Some{P{Con{0, Con{0, Con{0, vs}}}, t}}
461 case False{}:
462 match plus:
463 case True{}:
464 zone.num(0, vs, t)
465 case False{}:
466 match minus:
467 case True{}:
468 zone.num(1, vs, t)
469 case False{}:
470 None{}
471
472# Z, or +hh:mm or -hh:mm, as (sign, hh, mm) with sign 1 for west of UTC.
473def zone(p: P) -> Maybe<&2, P>:
474 match p:
475 case P{vs, s}:
476 match s:
477 case SNil{}:
478 None{}
479 case SCon{Chr{+c}, t}:
480 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)
481
482def index.go(xs: List<&2, String>, +w: String, +i: U32) -> U32:
483 match xs:
484 case Nil{}:
485 i
486 case Con{x, rest}:
487 Bool.pick(U32, String.eq(x, w), i, index.go(rest, w, (i + 1 : U32)))
488
489# One of names, as its index.
490def word(+names: List<&2, String>, p: P) -> Maybe<&2, P>:
491 match p:
492 case P{vs, +s}:
493 +i = index.go(names, String.take(s, 3n), 0)
494 lit.if(U32.is_lt(i, U32.from_nat(List.length(&2, String, names))), Con{i, vs}, String.drop(s, 3n))
495
496def mk.if(ok: Bool, t: DateTime) -> Maybe<&2, Instant>:
497 match ok:
498 case True{}:
499 Some{DateTime.to_instant(t)}
500 case False{}:
501 None{}
502
503def mk(+t: DateTime) -> Maybe<&2, Instant>:
504 mk.if(DateTime.valid(t), t)
505
506def rfc3339.shift(m: Maybe<&2, Instant>, +west: U32, +hh: U32, +mm: U32) -> Maybe<&2, Instant>:
507 match m:
508 case None{}:
509 None{}
510 case Some{i}:
511 +off = Duration.of_secs(i64((hh * 3600 + mm * 60 : U32)))
512 Bool.pick(Maybe<&2, Instant>, Bool.and(U32.is_le(hh, 23), U32.is_le(mm, 59)),
513 Some{Instant.add(i, Bool.pick(Duration, U32.is_eq(west, 1), off, Duration.neg(off)))}, None{})
514
515def rfc3339.fin(p: P) -> Maybe<&2, Instant>:
516 match p:
517 case P{Con{mm, Con{hh, Con{west, Con{n, Con{s, Con{mi, Con{h, Con{d, Con{mo, Con{y, Nil{}}}}}}}}}}}, SNil{}}:
518 rfc3339.shift(mk(DateTime{Date{y, mo, d}, h, mi, s, n}), west, hh, mm)
519 case _:
520 None{}
521
522# An RFC 3339 date-time (§5.6), such as 1985-04-12T23:20:50.52Z or 1996-12-19T16:39:57-08:00.
523# T and Z may be lowercase. A leap second (:60) is refused, as Instant has none.
524def rfc3339.parse(s: String) -> Maybe<&2, Instant>:
525 do Maybe<&2, Instant>:
526 a : P <- num(4n, P{Nil{}, s})
527 b : P <- lit(45, a)
528 c : P <- num(2n, b)
529 d : P <- lit(45, c)
530 e : P <- num(2n, d)
531 f : P <- lit2(84, 116, e)
532 g : P <- num(2n, f)
533 h : P <- lit(58, g)
534 i : P <- num(2n, h)
535 j : P <- lit(58, i)
536 k : P <- num(2n, j)
537 l : P <- secfrac(k)
538 m : P <- zone(l)
539 rfc3339.fin(m)
540
541def http_date.fin(p: P) -> Maybe<&2, Instant>:
542 match p:
543 case P{Con{s, Con{mi, Con{h, Con{y, Con{mo, Con{d, Con{wd, Nil{}}}}}}}}, SNil{}}:
544 mk(DateTime{Date{y, (mo + 1 : U32), d}, h, mi, s, 0})
545 case _:
546 None{}
547
548# An IMF-fixdate (RFC 9110 §5.6.7), such as Sun, 06 Nov 1994 08:49:37 GMT.
549# The day name must be one of the seven, but it is not checked against the date.
550def http_date.parse(s: String) -> Maybe<&2, Instant>:
551 do Maybe<&2, Instant>:
552 a : P <- word(WEEKDAYS(), P{Nil{}, s})
553 b : P <- text(", ", a)
554 c : P <- num(2n, b)
555 d : P <- lit(32, c)
556 e : P <- word(MONTHS(), d)
557 f : P <- lit(32, e)
558 g : P <- num(4n, f)
559 h : P <- lit(32, g)
560 i : P <- num(2n, h)
561 j : P <- lit(58, i)
562 k : P <- num(2n, j)
563 l : P <- lit(58, k)
564 m : P <- num(2n, l)
565 n : P <- text(" GMT", m)
566 http_date.fin(n)
567
568# Time zones
569# ----------
570
571# A local time type: seconds east of UTC, whether it is daylight time, and its abbreviation.
572type Ttype is Data:
573 Ttype{utoff: Int.I64, dst: Bool, abbr: String}
574
575# From at on, local time follows types[idx].
576type Trans is Data:
577 Trans{at: Int.I64, idx: U32}
578
579# A TZif zone (RFC 8536): transitions in time order, local time types, and the footer TZ string ("" in version 1).
580type Zone is Data:
581 Zone{trans: List<&2, Trans>, types: List<&2, Ttype>, tz: String}
582
583# n bytes of a byte string, big-endian.
584def be(n: Nat, s: String, +acc: U32) -> U32:
585 match n:
586 case 0n:
587 acc
588 case 1n+k:
589 match s:
590 case SNil{}:
591 acc
592 case SCon{Chr{c}, t}:
593 be(k, t, ((acc << 8n) .|. c : U32))
594
595def be32(+s: String, n: Nat) -> U32:
596 be(4n, String.drop(s, n), 0)
597
598def u8(+s: String, n: Nat) -> U32:
599 be(1n, String.drop(s, n), 0)
600
601def tzif.size(t8: Bool) -> Nat:
602 match t8:
603 case True{}:
604 8n
605 case False{}:
606 4n
607
608def tzif.time(t8: Bool, +s: String) -> Int.I64:
609 match t8:
610 case True{}:
611 i64.of(be32(s, 0n), be32(s, 4n))
612 case False{}:
613 i64s(be32(s, 0n))
614
615# ts holds the transition times and ks their type indexes.
616def tzif.trans(n: Nat, +t8: Bool, +ts: String, +ks: String) -> List<&2, Trans>:
617 match n:
618 case 0n:
619 Nil{}
620 case 1n+k:
621 Con{Trans{tzif.time(t8, ts), u8(ks, 0n)},
622 tzif.trans(k, t8, String.drop(ts, tzif.size(t8)), String.drop(ks, 1n))}
623
624# The NUL-terminated abbreviation at byte i of chars.
625def tzif.abbr(chars: String, +i: U32) -> String:
626 name(String.split(String.drop(chars, U32.to_nat(i)), Chr{0}), 0)
627
628def tzif.types(n: Nat, +s: String, +chars: String) -> List<&2, Ttype>:
629 match n:
630 case 0n:
631 Nil{}
632 case 1n+k:
633 Con{Ttype{i64s(be32(s, 0n)), U32.is_ne(u8(s, 4n), 0), tzif.abbr(chars, u8(s, 5n))},
634 tzif.types(k, String.drop(s, 6n), chars)}
635
636def tzif.if(ok: Bool, z: Zone) -> Maybe<&2, Zone>:
637 match ok:
638 case True{}:
639 Some{z}
640 case False{}:
641 None{}
642
643# Header counts, in RFC 8536 order: isut, isstd, leap, time, type, char.
644def tzif.count(+h: String, i: Nat) -> Nat:
645 U32.to_nat(be32(h, (20n + 4n * i : Nat)))
646
647# The data block's size in bytes, for header h.
648def tzif.bsize(+t8: Bool, +h: String) -> Nat:
649 +tc = tzif.count(h, 3n)
650 (tc * tzif.size(t8) + tc + tzif.count(h, 4n) * 6n + tzif.count(h, 5n) +
651 tzif.count(h, 2n) * (tzif.size(t8) + 4n) + tzif.count(h, 1n) + tzif.count(h, 0n) : Nat)
652
653# h starts at a header; its data block follows it. Version 2+ blocks have 8-byte times and a footer.
654def tzif.block(+t8: Bool, +h: String) -> Maybe<&2, Zone>:
655 +d = String.drop(h, 44n)
656 +tc = tzif.count(h, 3n)
657 +ty = tzif.count(h, 4n)
658 +at = (tc * tzif.size(t8) + tc : Nat)
659 +foot = String.drop(d, tzif.bsize(t8, h))
660 tzif.if(Bool.and(String.starts_with(h, "TZif"), Bool.and(Nat.is_gt(ty, 0n),
661 Nat.is_le((44n + tzif.bsize(t8, h) : Nat), String.length(h)))),
662 Zone{tzif.trans(tc, t8, d, String.drop(d, (tc * tzif.size(t8) : Nat))),
663 tzif.types(ty, String.drop(d, at), String.take(String.drop(d, (at + ty * 6n : Nat)), tzif.count(h, 5n))),
664 Bool.pick(String, t8, name(String.split(foot, '\n'), 1), "")})
665
666def tzif.go(v2: Bool, +s: String) -> Maybe<&2, Zone>:
667 match v2:
668 case True{}:
669 tzif.block(True{}, String.drop(s, (44n + tzif.bsize(False{}, s) : Nat)))
670 case False{}:
671 tzif.block(False{}, s)
672
673# A TZif file, such as one from /usr/share/zoneinfo. Versions 2 and up use their 64-bit block.
674# ponytail: reads the bytes as a byte String; walk Bytes directly if zone files get big.
675def tzif.parse(b: Bytes.Bytes) -> Maybe<&2, Zone>:
676 +s = Bytes.to_string(b)
677 tzif.go(U32.is_ge(u8(s, 4n), 50), s)
678
679# The type index at secs: the last transition at or before it, or type 0 before the first.
680# ponytail: linear scan; bisect an Array if lookups get hot.
681def Zone.find(ts: List<&2, Trans>, +secs: Int.I64, +cur: U32) -> U32:
682 match ts:
683 case Nil{}:
684 cur
685 case Con{Trans{t, k}, rest}:
686 Zone.find(rest, secs, Bool.pick(U32, Int.I64.is_le(t, secs), k, cur))
687
688# The local time type at i.
689# ponytail: past the last transition the last type holds; evaluate the footer TZ rule for slim files and years past 2037.
690def Zone.at(z: Zone, i: Instant) -> Maybe<&2, Ttype>:
691 match z i:
692 case Zone{ts, types, tz} Instant{s, n}:
693 List.get(&2, Ttype, types, U32.to_nat(Zone.find(ts, s, 0)))
694
695def Zone.local.at(m: Maybe<&2, Ttype>, i: Instant) -> Maybe<&2, DateTime>:
696 match m:
697 case None{}:
698 None{}
699 case Some{Ttype{off, dst, abbr}}:
700 DateTime.of_instant(Instant.add(i, Duration.of_secs(off)))
701
702# The local date and time at i in zone z.
703def Zone.local(z: Zone, +i: Instant) -> Maybe<&2, DateTime>:
704 Zone.local.at(Zone.at(z, i), i)