time.bend

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