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
2	import Base
3	import bend-kit-int@0.2.0.0/int.bend as Int
4	import bend-kit-fmt@0.1.0.0/fmt.bend as Fmt
5	# bend-kit-bytes@0.3.0.0
6	import 0x49814d83de8f70993a43e1002be29ecd/bytes.bend as Bytes
7	
8	# secs + nanos / 10^9 seconds, with nanos below 10^9: -0.5 s is Duration{-1, 500000000}.
9	type 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.
13	type 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.
17	type Date is Data:
18	  Date{year: U32, month: U32, day: U32}
19	
20	type DateTime is Data:
21	  DateTime{date: Date, hour: U32, min: U32, sec: U32, nanos: U32}
22	
23	def i64(x: U32) -> Int.I64:
24	  Int.I64.from_u32(x)
25	
26	# The signed 32-bit value of x, widened.
27	def 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.
33	def 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	
39	def Duration.zero() -> Duration:
40	  Duration{i64(0), 0}
41	
42	def Duration.of_secs(s: Int.I64) -> Duration:
43	  Duration{s, 0}
44	
45	def Duration.of_ms(+ms: U32) -> Duration:
46	  Duration{i64((ms / 1000 : U32)), ((ms % 1000 : U32) * 1000000 : U32)}
47	
48	# Whole milliseconds, rounded down.
49	def 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	
54	def 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	
61	def 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.
68	def 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	
75	def 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	
80	def Duration.neg(d: Duration) -> Duration:
81	  Duration.sub(Duration.zero(), d)
82	
83	def 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	
92	def 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	
100	def Instant.epoch() -> Instant:
101	  Instant{i64(0), 0}
102	
103	def Instant.of_unix(s: Int.I64) -> Instant:
104	  Instant{s, 0}
105	
106	def Instant.of(d: Duration) -> Instant:
107	  match d:
108	    case Duration{s, n}:
109	      Instant{s, n}
110	
111	def Instant.since_epoch(i: Instant) -> Duration:
112	  match i:
113	    case Instant{s, n}:
114	      Duration{s, n}
115	
116	def Instant.add(i: Instant, d: Duration) -> Instant:
117	  Instant.of(Duration.add(Instant.since_epoch(i), d))
118	
119	# a - b.
120	def Instant.since(a: Instant, b: Instant) -> Duration:
121	  Duration.sub(Instant.since_epoch(a), Instant.since_epoch(b))
122	
123	def 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.
130	def 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.
135	def wall.raw() -> IO(U32 & U32 & U32):
136	  import "./effs/time.c"
137	  import "./effs/time.js"
138	
139	def 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.
144	def 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.
150	def 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	
158	def 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.
163	def 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	
168	def 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.
176	def Z.EPOCH() -> U32:
177	  865565
178	
179	def 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	
185	def 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	
192	def 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	
197	def 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	
204	def 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.
214	def Date.to_days(d: Date) -> Int.I64:
215	  Int.I64.sub(i64(Date.to_z(d)), i64(Z.EPOCH()))
216	
217	def 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.
225	def 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.
231	def Date.weekday(d: Date) -> U32:
232	  ((Date.to_z(d) + 2) % 7 + 1 : U32)
233	
234	# Date and time
235	# -------------
236	
237	def 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.
244	def 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	
250	def 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.
258	def 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.
266	def 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	
275	def pad(+x: U32, w: Nat) -> String:
276	  Fmt.Fmt.pad_left(U32.show(x), w, '0')
277	
278	# Milliseconds with six decimal places.
279	def 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	
284	def 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	
291	def 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.
297	def 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	
309	def 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	
312	def 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	
318	def 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.
326	def rfc3339(i: Instant) -> Maybe<&2, String>:
327	  fmt.map(~DateTime.rfc3339, DateTime.of_instant(i))
328	
329	def WEEKDAYS() -> List<&2, String>:
330	  ["Mon", "Tue", "Wed", "Thu", "Fri", "Sat", "Sun"]
331	
332	def MONTHS() -> List<&2, String>:
333	  ["Jan", "Feb", "Mar", "Apr", "May", "Jun", "Jul", "Aug", "Sep", "Oct", "Nov", "Dec"]
334	
335	def name(xs: List<&2, String>, +i: U32) -> String:
336	  Maybe.default(&2, String, List.get(&2, String, xs, U32.to_nat(i)), "")
337	
338	def 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.
347	def 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.
354	type P is Data:
355	  P{vals: List<&2, U32>, rest: String}
356	
357	def is_digit(+c: U32) -> Bool:
358	  Bool.and(U32.is_ge(c, 48), U32.is_le(c, 57))
359	
360	def 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	
375	def 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.
383	def 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	
388	def 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.
396	def 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	
405	def lit(+c: U32, p: P) -> Maybe<&2, P>:
406	  lit2(c, c, p)
407	
408	def 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	
414	def 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.
422	def 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	
433	def 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	
437	def 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.
446	def secfrac(p: P) -> Maybe<&2, P>:
447	  match p:
448	    case P{vs, +s}:
449	      secfrac.if(String.starts_with(s, "."), vs, s)
450	
451	def 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	
457	def 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.
473	def 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	
482	def 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.
490	def 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	
496	def 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	
503	def mk(+t: DateTime) -> Maybe<&2, Instant>:
504	  mk.if(DateTime.valid(t), t)
505	
506	def 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	
515	def 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.
524	def 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	
541	def 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.
550	def 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.
572	type Ttype is Data:
573	  Ttype{utoff: Int.I64, dst: Bool, abbr: String}
574	
575	# From at on, local time follows types[idx].
576	type 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).
580	type 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.
584	def 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	
595	def be32(+s: String, n: Nat) -> U32:
596	  be(4n, String.drop(s, n), 0)
597	
598	def u8(+s: String, n: Nat) -> U32:
599	  be(1n, String.drop(s, n), 0)
600	
601	def tzif.size(t8: Bool) -> Nat:
602	  match t8:
603	    case True{}:
604	      8n
605	    case False{}:
606	      4n
607	
608	def 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.
616	def 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.
625	def tzif.abbr(chars: String, +i: U32) -> String:
626	  name(String.split(String.drop(chars, U32.to_nat(i)), Chr{0}), 0)
627	
628	def 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	
636	def 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.
644	def 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.
648	def 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.
654	def 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	
666	def 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.
675	def 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	# POSIX TZ offsets are seconds west of UTC; transition times are seconds from local midnight.
680	type TzField is Data:
681	  TzField{value: U32, rest: String}
682	
683	type TzText is Data:
684	  TzText{value: String, rest: String}
685	
686	type TzClock is Data:
687	  TzClock{value: Int.I64, rest: String}
688	
689	type TzDay is Data:
690	  Julian{day: U32}
691	  Ordinal{day: U32}
692	  MonthWeek{month: U32, week: U32, weekday: U32}
693	
694	type TzDate is Data:
695	  TzDate{day: TzDay, seconds: Int.I64}
696	
697	type TzDayPart is Data:
698	  TzDayPart{day: TzDay, rest: String}
699	
700	type TzDatePart is Data:
701	  TzDatePart{date: TzDate, rest: String}
702	
703	type TzRule is Data:
704	  TzRule{std: Ttype, daylight: Ttype, start: TzDate, end: TzDate}
705	
706	def tz.digit(+c: U32) -> Bool:
707	  Bool.and(U32.is_ge(c, 48), U32.is_le(c, 57))
708	
709	def tz.alpha(+c: U32) -> Bool:
710	  Bool.or(Bool.and(U32.is_ge(c, 65), U32.is_le(c, 90)),
711	    Bool.and(U32.is_ge(c, 97), U32.is_le(c, 122)))
712	
713	def tz.quoted(+c: U32) -> Bool:
714	  Bool.or(tz.alpha(c), Bool.or(tz.digit(c), Bool.or(U32.is_eq(c, 43), U32.is_eq(c, 45))))
715	
716	def tz.number.stop(seen: Bool, acc: U32, s: String) -> Maybe<&2, TzField>:
717	  match seen:
718	    case True{}:
719	      Some{TzField{acc, s}}
720	    case False{}:
721	      None{}
722	
723	def tz.number.step(digit: Bool, c: U32, t: String, acc: U32, seen: Bool, next: Unit -> Maybe<&2, TzField>) -> Maybe<&2, TzField>:
724	  match digit:
725	    case True{}:
726	      next(Unit{})
727	    case False{}:
728	      tz.number.stop(seen, acc, SCon{Chr{c}, t})
729	
730	# Three digits suffice for POSIX hour, day, and month fields.
731	def tz.number.go(s: String, +acc: U32, +seen: Bool) -> Maybe<&2, TzField>:
732	  match s:
733	    case SNil{}:
734	      tz.number.stop(seen, acc, SNil{})
735	    case SCon{Chr{+c}, +t}:
736	      tz.number.step(Bool.and(tz.digit(c), U32.is_lt(acc, 100)),
737	        c, t, acc, seen, _ => tz.number.go(t, ((acc * 10 + c - 48) : U32), True{}))
738	
739	def tz.number(s: String) -> Maybe<&2, TzField>:
740	  tz.number.go(s, 0, False{})
741	
742	def tz.name.valid(ok: Bool, name: String, rest: String) -> Maybe<&2, TzText>:
743	  match ok:
744	    case True{}:
745	      Some{TzText{name, rest}}
746	    case False{}:
747	      None{}
748	
749	def tz.name.done(rev: String, rest: String) -> Maybe<&2, TzText>:
750	  +name = String.reverse(rev)
751	  tz.name.valid(Nat.is_ge(String.length(name), 3n), name, rest)
752	
753	def tz.name.empty(quoted: Bool, rev: String) -> Maybe<&2, TzText>:
754	  match quoted:
755	    case True{}:
756	      None{}
757	    case False{}:
758	      tz.name.done(rev, SNil{})
759	
760	def tz.name.branch(continue: Bool, rev: String, c: U32, rest: String, next: Unit -> Maybe<&2, TzText>) -> Maybe<&2, TzText>:
761	  match continue:
762	    case True{}:
763	      next(Unit{})
764	    case False{}:
765	      tz.name.done(rev, SCon{Chr{c}, rest})
766	
767	def tz.name.allowed(ok: Bool, next: Unit -> Maybe<&2, TzText>) -> Maybe<&2, TzText>:
768	  match ok:
769	    case True{}:
770	      next(Unit{})
771	    case False{}:
772	      None{}
773	
774	def tz.name.quoted(end: Bool, valid: Bool, rev: String, rest: String, next: Unit -> Maybe<&2, TzText>) -> Maybe<&2, TzText>:
775	  match end:
776	    case True{}:
777	      tz.name.done(rev, rest)
778	    case False{}:
779	      tz.name.allowed(valid, next)
780	
781	def tz.name.char(quoted: Bool, end: Bool, alpha: Bool, valid: Bool, rev: String, c: U32, rest: String,
782	  next: Unit -> Maybe<&2, TzText>) -> Maybe<&2, TzText>:
783	  match quoted:
784	    case True{}:
785	      tz.name.quoted(end, valid, rev, rest, next)
786	    case False{}:
787	      tz.name.branch(alpha, rev, c, rest, next)
788	
789	def tz.name.go(s: String, +rev: String, +quoted: Bool) -> Maybe<&2, TzText>:
790	  match s:
791	    case SNil{}:
792	      tz.name.empty(quoted, rev)
793	    case SCon{Chr{+c}, +t}:
794	      tz.name.char(quoted, U32.is_eq(c, 62), tz.alpha(c), tz.quoted(c), rev, c, t,
795	        _ => tz.name.go(t, SCon{Chr{c}, rev}, quoted))
796	
797	def tz.name(s: String) -> Maybe<&2, TzText>:
798	  match s:
799	    case SCon{Chr{60}, t}:
800	      tz.name.go(t, SNil{}, True{})
801	    case _:
802	      tz.name.go(s, SNil{}, False{})
803	
804	def tz.field.valid(ok: Bool, n: U32, rest: String) -> Maybe<&2, TzField>:
805	  match ok:
806	    case True{}:
807	      Some{TzField{n, rest}}
808	    case False{}:
809	      None{}
810	
811	def tz.clock.tail(r: TzField, limit: U32) -> Maybe<&2, TzField>:
812	  match r:
813	    case TzField{+n, rest}:
814	      tz.field.valid(U32.is_le(n, limit), n, rest)
815	
816	def tz.clock.part(s: String) -> Maybe<&2, TzField>:
817	  match s:
818	    case SCon{Chr{58}, t}:
819	      do Maybe<&2, TzField>:
820	        n : TzField <- tz.number(t)
821	        tz.clock.tail(n, 59)
822	    case _:
823	      Some{TzField{0, s}}
824	
825	def tz.clock.valid(ok: Bool, +value: Int.I64, negative: Bool, rest: String) -> Maybe<&2, TzClock>:
826	  match ok:
827	    case False{}:
828	      None{}
829	    case True{}:
830	      Some{TzClock{Bool.pick(Int.I64, negative, Int.I64.neg(value), value), rest}}
831	
832	def tz.clock.seconds(sec: TzField, +hours: U32, +minutes: U32, +max: U32, negative: Bool) -> Maybe<&2, TzClock>:
833	  match sec:
834	    case TzField{+seconds, rest}:
835	      tz.clock.valid(U32.is_le(hours, max),
836	        i64((hours * 3600 + minutes * 60 + seconds : U32)), negative, rest)
837	
838	def tz.clock.minutes(m: TzField, +hours: U32, +max: U32, +negative: Bool) -> Maybe<&2, TzClock>:
839	  match m:
840	    case TzField{+minutes, rest}:
841	      do Maybe<&2, TzClock>:
842	        sec : TzField <- tz.clock.part(rest)
843	        tz.clock.seconds(sec, hours, minutes, max, negative)
844	def tz.clock.finish(h: TzField, +max: U32, +negative: Bool) -> Maybe<&2, TzClock>:
845	  match h:
846	    case TzField{+hours, rest}:
847	      do Maybe<&2, TzClock>:
848	        m : TzField <- tz.clock.part(rest)
849	        tz.clock.minutes(m, hours, max, negative)
850	
851	
852	def tz.clock.read(s: String, max: U32, negative: Bool) -> Maybe<&2, TzClock>:
853	  do Maybe<&2, TzClock>:
854	    h : TzField <- tz.number(s)
855	    tz.clock.finish(h, max, negative)
856	def tz.clock.sign(s: String, max: U32) -> Maybe<&2, TzClock>:
857	  match s:
858	    case SCon{Chr{45}, t}:
859	      tz.clock.read(t, max, True{})
860	    case SCon{Chr{43}, t}:
861	      tz.clock.read(t, max, False{})
862	    case _:
863	      tz.clock.read(s, max, False{})
864	
865	
866	def tz.day.valid(ok: Bool, d: TzDay, rest: String) -> Maybe<&2, TzDayPart>:
867	  match ok:
868	    case True{}:
869	      Some{TzDayPart{d, rest}}
870	    case False{}:
871	      None{}
872	
873	def tz.day.j(r: TzField) -> Maybe<&2, TzDayPart>:
874	  match r:
875	    case TzField{+n, rest}:
876	      tz.day.valid(Bool.and(U32.is_ge(n, 1), U32.is_le(n, 365)), Julian{n}, rest)
877	
878	def tz.day.n(r: TzField) -> Maybe<&2, TzDayPart>:
879	  match r:
880	    case TzField{+n, rest}:
881	      tz.day.valid(U32.is_le(n, 365), Ordinal{n}, rest)
882	
883	def tz.after(c: Char, s: String) -> String:
884	  match s:
885	    case SCon{h, t}:
886	      Bool.pick(String, Char.is_eq(h, c), t, SNil{})
887	    case SNil{}:
888	      SNil{}
889	
890	def tz.day.weekday(c: TzField, +month: U32, +week: U32) -> Maybe<&2, TzDayPart>:
891	  match c:
892	    case TzField{+weekday, rest}:
893	      tz.day.valid(Bool.and(U32.is_ge(month, 1), Bool.and(U32.is_le(month, 12),
894	        Bool.and(U32.is_ge(week, 1), Bool.and(U32.is_le(week, 5), U32.is_le(weekday, 6))))),
895	        MonthWeek{month, week, weekday}, rest)
896	
897	def tz.day.week(b: TzField, month: U32) -> Maybe<&2, TzDayPart>:
898	  match b:
899	    case TzField{week, rest}:
900	      do Maybe<&2, TzDayPart>:
901	        c : TzField <- tz.number(tz.after('.', rest))
902	        tz.day.weekday(c, month, week)
903	
904	def tz.day.month(a: TzField) -> Maybe<&2, TzDayPart>:
905	  match a:
906	    case TzField{month, rest}:
907	      do Maybe<&2, TzDayPart>:
908	        b : TzField <- tz.number(tz.after('.', rest))
909	        tz.day.week(b, month)
910	
911	def tz.day.m(s: String) -> Maybe<&2, TzDayPart>:
912	  do Maybe<&2, TzDayPart>:
913	    a : TzField <- tz.number(s)
914	    tz.day.month(a)
915	
916	def tz.day(s: String) -> Maybe<&2, TzDayPart>:
917	  match s:
918	    case SCon{Chr{74}, t}:
919	      do Maybe<&2, TzDayPart>:
920	        n : TzField <- tz.number(t)
921	        tz.day.j(n)
922	    case SCon{Chr{77}, t}:
923	      tz.day.m(t)
924	    case _:
925	      do Maybe<&2, TzDayPart>:
926	        n : TzField <- tz.number(s)
927	        tz.day.n(n)
928	
929	def tz.date.clock(d: TzDay, r: TzClock) -> Maybe<&2, TzDatePart>:
930	  match r:
931	    case TzClock{secs, end}:
932	      Some{TzDatePart{TzDate{d, secs}, end}}
933	
934	def tz.date.time(d: TzDay, rest: String) -> Maybe<&2, TzDatePart>:
935	  match rest:
936	    case SCon{Chr{47}, t}:
937	      do Maybe<&2, TzDatePart>:
938	        r : TzClock <- tz.clock.sign(t, 167)
939	        tz.date.clock(d, r)
940	    case _:
941	      Some{TzDatePart{TzDate{d, i64(7200)}, rest}}
942	
943	def tz.date.part(r: TzDayPart) -> Maybe<&2, TzDatePart>:
944	  match r:
945	    case TzDayPart{d, rest}:
946	      tz.date.time(d, rest)
947	
948	def tz.date(s: String) -> Maybe<&2, TzDatePart>:
949	  do Maybe<&2, TzDatePart>:
950	    r : TzDayPart <- tz.day(s)
951	    tz.date.part(r)
952	
953	def tz.rule.end(ok: Bool, standard: Ttype, daylight: Ttype, start: TzDate, end: TzDate) -> Maybe<&2, TzRule>:
954	  match ok:
955	    case True{}:
956	      Some{TzRule{standard, daylight, start, end}}
957	    case False{}:
958	      None{}
959	
960	def tz.rule.finish(b: TzDatePart, standard: Ttype, daylight: Ttype, start: TzDate) -> Maybe<&2, TzRule>:
961	  match b:
962	    case TzDatePart{end, rest}:
963	      tz.rule.end(String.is_empty(rest), standard, daylight, start, end)
964	
965	def tz.rule.start(a: TzDatePart, +standard: Ttype, +daylight: Ttype) -> Maybe<&2, TzRule>:
966	  match a:
967	    case TzDatePart{start, rest}:
968	      do Maybe<&2, TzRule>:
969	        b : TzDatePart <- tz.date(tz.after(',', rest))
970	        tz.rule.finish(b, standard, daylight, start)
971	
972	def tz.rule.dates(+standard: Ttype, +daylight: Ttype, rest: String) -> Maybe<&2, TzRule>:
973	  do Maybe<&2, TzRule>:
974	    a : TzDatePart <- tz.date(tz.after(',', rest))
975	    tz.rule.start(a, standard, daylight)
976	
977	def tz.rule.dstclock(r: TzClock, standard: Ttype, abbr: String) -> Maybe<&2, TzRule>:
978	  match r:
979	    case TzClock{west, rest}:
980	      tz.rule.dates(standard, Ttype{Int.I64.neg(west), True{}, abbr}, rest)
981	
982	def tz.rule.offset(standard: Ttype, abbr: String, west: Int.I64, rest: String) -> Maybe<&2, TzRule>:
983	  match rest:
984	    case SCon{Chr{44}, t}:
985	      tz.rule.dates(standard, Ttype{Int.I64.sub(i64(3600), west), True{}, abbr}, rest)
986	    # POSIX leaves absent DST dates to the implementation; use the common US rules.
987	    case SNil{}:
988	      tz.rule.end(True{}, standard, Ttype{Int.I64.sub(i64(3600), west), True{}, abbr},
989	        TzDate{MonthWeek{3, 2, 0}, i64(7200)}, TzDate{MonthWeek{11, 1, 0}, i64(7200)})
990	    case _:
991	      do Maybe<&2, TzRule>:
992	        r : TzClock <- tz.clock.sign(rest, 24)
993	        tz.rule.dstclock(r, standard, abbr)
994	
995	def tz.rule.named(name: TzText, standard: Ttype, west: Int.I64) -> Maybe<&2, TzRule>:
996	  match name:
997	    case TzText{abbr, rest}:
998	      tz.rule.offset(standard, abbr, west, rest)
999	
1000	def tz.rule.dst(+standard: Ttype, west: Int.I64, rest: String) -> Maybe<&2, TzRule>:
1001	  match rest:
1002	    case SNil{}:
1003	      Some{TzRule{standard, standard, TzDate{Ordinal{0}, i64(0)}, TzDate{Ordinal{0}, i64(0)}}}
1004	    case _:
1005	      do Maybe<&2, TzRule>:
1006	        name : TzText <- tz.name(rest)
1007	        tz.rule.named(name, standard, west)
1008	
1009	def tz.rule.stdclock(offset: TzClock, abbr: String) -> Maybe<&2, TzRule>:
1010	  match offset:
1011	    case TzClock{+west, rest}:
1012	      tz.rule.dst(Ttype{Int.I64.neg(west), False{}, abbr}, west, rest)
1013	
1014	def tz.rule.standard(name: TzText) -> Maybe<&2, TzRule>:
1015	  match name:
1016	    case TzText{abbr, rest}:
1017	      do Maybe<&2, TzRule>:
1018	        offset : TzClock <- tz.clock.sign(rest, 24)
1019	        tz.rule.stdclock(offset, abbr)
1020	
1021	def tz.rule(s: String) -> Maybe<&2, TzRule>:
1022	  do Maybe<&2, TzRule>:
1023	    name : TzText <- tz.name(s)
1024	    tz.rule.standard(name)
1025	
1026	# The day number of a rule in year y, relative to January 1.
1027	def tz.day.index(d: TzDay, +y: U32) -> U32:
1028	  match d:
1029	    case Julian{+n}:
1030	      (n - 1 + Bool.pick(U32, Bool.and(Date.is_leap(y), U32.is_ge(n, 60)), 1, 0) : U32)
1031	    case Ordinal{n}:
1032	      n
1033	    case MonthWeek{+month, +week, +weekday}:
1034	      +first_day = (Date.weekday(Date{y, month, 1}) % 7 : U32)
1035	      +day = (1 + ((weekday + 7 - first_day) % 7) + (week - 1) * 7 : U32)
1036	      +last = Date.days_in_month(y, month)
1037	      +actual = Bool.pick(U32, U32.is_gt(day, last), (day - 7 : U32), day)
1038	      Int.I64.to_u32(Int.I64.sub(Date.to_days(Date{y, month, actual}), Date.to_days(Date{y, 1, 1})))
1039	
1040	def tz.date.utc(d: TzDate, +y: U32, west: Int.I64) -> Int.I64:
1041	  match d:
1042	    case TzDate{day, sec}:
1043	      Int.I64.add(Int.I64.mul(Int.I64.add(Date.to_days(Date{y, 1, 1}), i64(tz.day.index(day, y))), i64(86400)),
1044	        Int.I64.add(sec, west))
1045	
1046	# Apply the two transitions for the UTC year and its neighbors. A /time may cross a year boundary.
1047	type TzEvent is Data:
1048	  TzEvent{when: Int.I64, dst: Bool}
1049	
1050	def tz.event.select(newer: Bool, old: Maybe<&2, TzEvent>, when: Int.I64, dst: Bool) -> Maybe<&2, TzEvent>:
1051	  match newer:
1052	    case True{}:
1053	      Some{TzEvent{when, dst}}
1054	    case False{}:
1055	      old
1056	
1057	def tz.event.new(+now: Int.I64, old: Maybe<&2, TzEvent>, +when: Int.I64, dst: Bool) -> Maybe<&2, TzEvent>:
1058	  match old:
1059	    case None{}:
1060	      tz.event.select(Int.I64.is_le(when, now), None{}, when, dst)
1061	    case Some{TzEvent{+prev, flag}}:
1062	      tz.event.select(Bool.and(Int.I64.is_le(when, now), Int.I64.is_gt(when, prev)),
1063	        Some{TzEvent{prev, flag}}, when, dst)
1064	
1065	def tz.event.year(+now: Int.I64, old: Maybe<&2, TzEvent>, +r: TzRule, +y: U32) -> Maybe<&2, TzEvent>:
1066	  match r:
1067	    case TzRule{Ttype{+off, _, _}, Ttype{+dstoff, _, _}, +start, +end}:
1068	      +first = tz.event.new(now, old, tz.date.utc(start, y, Int.I64.neg(off)), True{})
1069	      tz.event.new(now, first, tz.date.utc(end, y, Int.I64.neg(dstoff)), False{})
1070	
1071	def tz.event.prev(+now: Int.I64, old: Maybe<&2, TzEvent>, +r: TzRule, +y: U32) -> Maybe<&2, TzEvent>:
1072	  match y:
1073	    case 0:
1074	      old
1075	    case _:
1076	      tz.event.year(now, old, r, (y - 1 : U32))
1077	
1078	def tz.event.next.if(valid: Bool, now: Int.I64, old: Maybe<&2, TzEvent>, r: TzRule, y: U32) -> Maybe<&2, TzEvent>:
1079	  match valid:
1080	    case True{}:
1081	      tz.event.year(now, old, r, (y + 1 : U32))
1082	    case False{}:
1083	      old
1084	def tz.event.next(+now: Int.I64, old: Maybe<&2, TzEvent>, +r: TzRule, +y: U32) -> Maybe<&2, TzEvent>:
1085	  tz.event.next.if(U32.is_lt(y, 9999), now, old, r, y)
1086	
1087	
1088	def tz.event.type(ev: Maybe<&2, TzEvent>, +r: TzRule) -> Ttype:
1089	  match ev:
1090	    case Some{TzEvent{when, dst}}:
1091	      match r:
1092	        case TzRule{standard, daylight, start, end}:
1093	          Bool.pick(Ttype, dst, daylight, standard)
1094	    case None{}:
1095	      match r:
1096	        case TzRule{standard, daylight, start, end}:
1097	          standard
1098	
1099	def tz.rule.at(+r: TzRule, +secs: Int.I64, +year: U32) -> Ttype:
1100	  +a = tz.event.prev(secs, None{}, r, year)
1101	  +b = tz.event.year(secs, a, r, year)
1102	  tz.event.type(tz.event.next(secs, b, r, year), r)
1103	
1104	def tz.rule.date(d: Maybe<&2, DateTime>, r: TzRule, secs: Int.I64) -> Maybe<&2, Ttype>:
1105	  match d:
1106	    case None{}:
1107	      None{}
1108	    case Some{DateTime{Date{y, m, day}, h, mi, second, nanos}}:
1109	      Some{tz.rule.at(r, secs, y)}
1110	
1111	def tz.rule.lookup(rule: Maybe<&2, TzRule>, +secs: Int.I64) -> Maybe<&2, Ttype>:
1112	  match rule:
1113	    case None{}:
1114	      None{}
1115	    case Some{r}:
1116	      tz.rule.date(DateTime.of_instant(Instant.of_unix(secs)), r, secs)
1117	
1118	# The type index at secs: the last transition at or before it, or type 0 before the first.
1119	# ponytail: linear scan; bisect an Array if lookups get hot.
1120	def Zone.find(ts: List<&2, Trans>, +secs: Int.I64, +cur: U32) -> U32:
1121	  match ts:
1122	    case Nil{}:
1123	      cur
1124	    case Con{Trans{t, k}, rest}:
1125	      Zone.find(rest, secs, Bool.pick(U32, Int.I64.is_le(t, secs), k, cur))
1126	def Zone.last.go(ts: List<&2, Trans>, +secs: Int.I64, +last: Int.I64) -> Bool:
1127	  match ts:
1128	    case Nil{}:
1129	      Int.I64.is_gt(secs, last)
1130	    case Con{Trans{t, k}, rest}:
1131	      Zone.last.go(rest, secs, t)
1132	def Zone.last(ts: List<&2, Trans>, secs: Int.I64) -> Bool:
1133	  match ts:
1134	    case Nil{}:
1135	      True{}
1136	    case Con{Trans{t, k}, rest}:
1137	      Zone.last.go(rest, secs, t)
1138	
1139	
1140	def Zone.at.fallback(m: Maybe<&2, Ttype>, types: List<&2, Ttype>, ts: List<&2, Trans>, secs: Int.I64) -> Maybe<&2, Ttype>:
1141	  match m:
1142	    case Some{t}:
1143	      Some{t}
1144	    case None{}:
1145	      List.get(&2, Ttype, types, U32.to_nat(Zone.find(ts, secs, 0)))
1146	def Zone.at.footer(use: Bool, tz: String, types: List<&2, Ttype>, ts: List<&2, Trans>, +secs: Int.I64) -> Maybe<&2, Ttype>:
1147	  match use:
1148	    case False{}:
1149	      List.get(&2, Ttype, types, U32.to_nat(Zone.find(ts, secs, 0)))
1150	    case True{}:
1151	      Zone.at.fallback(tz.rule.lookup(tz.rule(tz), secs), types, ts, secs)
1152	
1153	def Zone.at.tz(empty: Bool, tz: String, types: List<&2, Ttype>, +ts: List<&2, Trans>, +secs: Int.I64) -> Maybe<&2, Ttype>:
1154	  match empty:
1155	    case True{}:
1156	      List.get(&2, Ttype, types, U32.to_nat(Zone.find(ts, secs, 0)))
1157	    case False{}:
1158	      Zone.at.footer(Zone.last(ts, secs), tz, types, ts, secs)
1159	
1160	
1161	
1162	# The local time type at i. The footer applies strictly after the final explicit transition.
1163	def Zone.at(z: Zone, i: Instant) -> Maybe<&2, Ttype>:
1164	  match z i:
1165	    case Zone{ts, types, +tz} Instant{s, n}:
1166	      Zone.at.tz(String.eq(tz, ""), tz, types, ts, s)
1167	
1168	def Zone.local.at(m: Maybe<&2, Ttype>, i: Instant) -> Maybe<&2, DateTime>:
1169	  match m:
1170	    case None{}:
1171	      None{}
1172	    case Some{Ttype{off, dst, abbr}}:
1173	      DateTime.of_instant(Instant.add(i, Duration.of_secs(off)))
1174	
1175	# The local date and time at i in zone z.
1176	def Zone.local(z: Zone, +i: Instant) -> Maybe<&2, DateTime>:
1177	  Zone.local.at(Zone.at(z, i), i)