1	import Base
2	import 0xe49a3e6521e1b71e55654a885f27bcc1/parse.bend as P
3	import ./duration.bend as Dur
4	import ./period.bend as Per
5	type Iso8601.Error is Data:
6	  Unexpected{offset: Nat, char: Char}
7	  Eof{offset: Nat}
8	  Overflow{offset: Nat}
9	  Extra{offset: Nat, char: Char}
10	  Invalid{}
11	type Iso8601.DurS is Data:
12	  DurS{
13	    days: U32, h: U32, mi: U32, s: U32, nanos: U32,
14	    saw_d: Bool, saw_t: Bool, saw_h: Bool, saw_m: Bool, saw_s: Bool
15	  }
16	type Iso8601.DurM is Data:
17	  DSeek{}
18	  DNum{acc: U32}
19	  DFrac{sec: U32, acc: U32, left: Nat}
20	type Iso8601.DurC is Data:
21	  DurFail{e: Iso8601.Error}
22	  DurCont{st: Iso8601.DurS, mode: Iso8601.DurM}
23	type Iso8601.PerS is Data:
24	  PerS{
25	    years: U32, months: U32, days: U32,
26	    saw_y: Bool, saw_m: Bool, saw_w: Bool, saw_d: Bool
27	  }
28	type Iso8601.PerM is Data:
29	  PSeek{}
30	  PNum{acc: U32}
31	type Iso8601.PerC is Data:
32	  PerFail{e: Iso8601.Error}
33	  PerCont{st: Iso8601.PerS, mode: Iso8601.PerM}
34	def Iso8601.from_parse(e: P.Parse.Error) -> Iso8601.Error:
35	  match e:
36	    case P.Unexpected{offset, char}:
37	      Unexpected{offset, char}
38	    case P.Eof{offset}:
39	      Eof{offset}
40	    case P.Overflow{offset}:
41	      Overflow{offset}
42	    case P.Extra{offset, char}:
43	      Extra{offset, char}
44	def Iso8601.digit(n: U32) -> Char:
45	  Char.from_u32((Char.to_u32('0') + n : U32))
46	def Iso8601.pad_n.go(k: Nat, +n: U32, acc: String) -> String:
47	  match k:
48	    case 0n:
49	      acc
50	    case 1n++p:
51	      Iso8601.pad_n.go(
52	        p, U32.div(n, 10), SCon{Iso8601.digit(U32.mod(n, 10)), acc}
53	      )
54	def Iso8601.pad_n(n: U32, k: Nat) -> String:
55	  Iso8601.pad_n.go(k, n, SNil{})
56	def Iso8601.lead0(s: String) -> Bool:
57	  match s:
58	    case SNil{}:
59	      False{}
60	    case SCon{h, _}:
61	      Char.is_eq(h, '0')
62	def Iso8601.strip0(k: Nat, s: String, z: Bool) -> String:
63	  match k:
64	    case 0n:
65	      SCon{'0', SNil{}}
66	    case 1n++p:
67	      match s:
68	        case SNil{}:
69	          SCon{'0', SNil{}}
70	        case SCon{+h, +t}:
71	          match z:
72	            case False{}:
73	              SCon{h, t}
74	            case True{}:
75	              Iso8601.strip0(p, t, Iso8601.lead0(t))
76	def Iso8601.show_u32(+n: U32) -> String:
77	  +s = Iso8601.pad_n(n, 10n)
78	  Iso8601.strip0(10n, s, Iso8601.lead0(s))
79	def Iso8601.show.unit.go(+n: U32, c: Char, z: Bool) -> String:
80	  match z:
81	    case True{}:
82	      SNil{}
83	    case False{}:
84	      String.append(Iso8601.show_u32(n), SCon{c, SNil{}})
85	def Iso8601.show.unit(+n: U32, c: Char) -> String:
86	  Iso8601.show.unit.go(n, c, U32.is_eq(n, 0))
87	def Iso8601.frac.strip.go(+k: Nat, +n: U32, z: Bool) -> U32 & Nat:
88	  match k:
89	    case 0n:
90	      (n, 1n)
91	    case 1n:
92	      (n, 1n)
93	    case 1n++p:
94	      match z:
95	        case True{}:
96	          Iso8601.frac.strip.go(
97	            p, U32.div(n, 10), U32.is_eq(U32.mod(U32.div(n, 10), 10), 0)
98	          )
99	        case False{}:
100	          (n, k)
101	def Iso8601.frac.strip(+n: U32, k: Nat) -> U32 & Nat:
102	  Iso8601.frac.strip.go(k, n, U32.is_eq(U32.mod(n, 10), 0))
103	def Iso8601.show.frac2(nk: U32 & Nat) -> String:
104	  (n, k) = nk
105	  Iso8601.pad_n(n, k)
106	def Iso8601.show.frac(+nanos: U32) -> String:
107	  Iso8601.show.frac2(Iso8601.frac.strip(nanos, 9n))
108	def Iso8601.show.s2(+s: U32, +nanos: U32, z: Bool) -> String:
109	  match z:
110	    case True{}:
111	      String.append(Iso8601.show_u32(s), "S")
112	    case False{}:
113	      String.append(
114	        Iso8601.show_u32(s),
115	        String.append(".", String.append(Iso8601.show.frac(nanos), "S"))
116	      )
117	def Iso8601.show.s(+s: U32, +nanos: U32, need: Bool) -> String:
118	  match need:
119	    case False{}:
120	      SNil{}
121	    case True{}:
122	      Iso8601.show.s2(s, nanos, U32.is_eq(nanos, 0))
123	def Iso8601.show.t(
124	  +h: U32, +mi: U32, +s: U32, +nanos: U32
125	) -> String:
126	  String.append(
127	    Iso8601.show.unit(h, 'H'),
128	    String.append(
129	      Iso8601.show.unit(mi, 'M'),
130	      Iso8601.show.s(s, nanos, Bool.or(U32.is_gt(s, 0), U32.is_gt(nanos, 0)))
131	    )
132	  )
133	def Iso8601.show_duration.go(
134	  +days: U32, +h: U32, +mi: U32, +s: U32, +nanos: U32, has_d: Bool, has_t: Bool
135	) -> String:
136	  match has_d has_t:
137	    case False{} False{}:
138	      "PT0S"
139	    case True{} False{}:
140	      String.append("P", String.append(Iso8601.show_u32(days), "D"))
141	    case False{} True{}:
142	      String.append("PT", Iso8601.show.t(h, mi, s, nanos))
143	    case True{} True{}:
144	      String.append(
145	        "P",
146	        String.append(
147	          Iso8601.show_u32(days),
148	          String.append("DT", Iso8601.show.t(h, mi, s, nanos))
149	        )
150	      )
151	def Iso8601.show_duration.has(
152	  +days: U32, +h: U32, +mi: U32, +s: U32, +nanos: U32
153	) -> String:
154	  Iso8601.show_duration.go(
155	    days, h, mi, s, nanos,
156	    U32.is_gt(days, 0),
157	    Bool.or(
158	      U32.is_gt(h, 0),
159	      Bool.or(
160	        U32.is_gt(mi, 0),
161	        Bool.or(U32.is_gt(s, 0), U32.is_gt(nanos, 0))
162	      )
163	    )
164	  )
165	def Iso8601.show_duration(d: Dur.Duration) -> String:
166	  match d:
167	    case Dur.Duration{+days, +sod, +nanos}:
168	      Iso8601.show_duration.has(
169	        days,
170	        U32.div(sod, 3600),
171	        U32.div(U32.mod(sod, 3600), 60),
172	        U32.mod(sod, 60),
173	        nanos
174	      )
175	def Iso8601.show_period.body(+y: U32, +m: U32, +d: U32) -> String:
176	  String.append(
177	    Iso8601.show.unit(y, 'Y'),
178	    String.append(Iso8601.show.unit(m, 'M'), Iso8601.show.unit(d, 'D'))
179	  )
180	def Iso8601.show_period.p(body: String) -> String:
181	  match body:
182	    case SNil{}:
183	      "P0D"
184	    case SCon{_, _}:
185	      String.append("P", body)
186	def Iso8601.show_period(p: Per.Period) -> String:
187	  match p:
188	    case Per.Period{+y, +m, +d}:
189	      Iso8601.show_period.p(Iso8601.show_period.body(y, m, d))
190	def Iso8601.dur0() -> Iso8601.DurS:
191	  DurS{0, 0, 0, 0, 0, False{}, False{}, False{}, False{}, False{}}
192	def Iso8601.per0() -> Iso8601.PerS:
193	  PerS{0, 0, 0, False{}, False{}, False{}, False{}}
194	def Iso8601.or3(+a: Bool, +b: Bool, +c: Bool) -> Bool:
195	  Bool.or(a, Bool.or(b, c))
196	def Iso8601.or4(+a: Bool, +b: Bool, +c: Bool, +d: Bool) -> Bool:
197	  Bool.or(a, Iso8601.or3(b, c, d))
198	def Iso8601.expect.map(
199	  r: Result<&2, &2, P.Parse.Error, P.Parse.Cur>
200	) -> Result<&2, &2, Iso8601.Error, P.Parse.Cur>:
201	  match r:
202	    case Fail{e}:
203	      Fail{Iso8601.from_parse(e)}
204	    case Done{cur}:
205	      Done{cur}
206	def Iso8601.expect(
207	  cur: P.Parse.Cur, +c: Char
208	) -> Result<&2, &2, Iso8601.Error, P.Parse.Cur>:
209	  Iso8601.expect.map(P.Parse.expect_char(cur, c))
210	def Iso8601.dur.mk.ns2(
211	  r: Result<&2, &2, Dur.Duration.Error, Dur.Duration>
212	) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
213	  match r:
214	    case Fail{_}:
215	      Fail{Invalid{}}
216	    case Done{d}:
217	      Done{d}
218	def Iso8601.dur.mk.ns(
219	  r: Result<&2, &2, Dur.Duration.Error, Dur.Duration>, nanos: U32
220	) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
221	  match r:
222	    case Fail{_}:
223	      Fail{Invalid{}}
224	    case Done{d}:
225	      Iso8601.dur.mk.ns2(Dur.Duration.add(d, Dur.Duration{0, 0, nanos}))
226	def Iso8601.dur.mk.s(
227	  r: Result<&2, &2, Dur.Duration.Error, Dur.Duration>, +s: U32, nanos: U32
228	) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
229	  match r:
230	    case Fail{_}:
231	      Fail{Invalid{}}
232	    case Done{d}:
233	      Iso8601.dur.mk.ns(Dur.Duration.add(d, Dur.Duration.from_secs(s)), nanos)
234	def Iso8601.dur.mk.mi2(
235	  d: Dur.Duration, rm: Result<&2, &2, Dur.Duration.Error, Dur.Duration>,
236	  s: U32, nanos: U32
237	) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
238	  match rm:
239	    case Fail{_}:
240	      Fail{Invalid{}}
241	    case Done{dm}:
242	      Iso8601.dur.mk.s(Dur.Duration.add(d, dm), s, nanos)
243	def Iso8601.dur.mk.mi(
244	  r: Result<&2, &2, Dur.Duration.Error, Dur.Duration>, +mi: U32, s: U32, nanos: U32
245	) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
246	  match r:
247	    case Fail{_}:
248	      Fail{Invalid{}}
249	    case Done{d}:
250	      Iso8601.dur.mk.mi2(d, Dur.Duration.from_mins(mi), s, nanos)
251	def Iso8601.dur.mk.h2(
252	  d: Dur.Duration, rh: Result<&2, &2, Dur.Duration.Error, Dur.Duration>,
253	  mi: U32, s: U32, nanos: U32
254	) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
255	  match rh:
256	    case Fail{_}:
257	      Fail{Invalid{}}
258	    case Done{dh}:
259	      Iso8601.dur.mk.mi(Dur.Duration.add(d, dh), mi, s, nanos)
260	def Iso8601.dur.mk.h(
261	  r: Result<&2, &2, Dur.Duration.Error, Dur.Duration>, +h: U32, mi: U32, s: U32, nanos: U32
262	) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
263	  match r:
264	    case Fail{_}:
265	      Fail{Invalid{}}
266	    case Done{d}:
267	      Iso8601.dur.mk.h2(d, Dur.Duration.from_hours(h), mi, s, nanos)
268	def Iso8601.dur.mk(st: Iso8601.DurS) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
269	  match st:
270	    case DurS{+days, +h, +mi, +s, +nanos, _, _, _, _, _}:
271	      Iso8601.dur.mk.h(
272	        Done{Dur.Duration.from_days(days)}, h, mi, s, nanos
273	      )
274	def Iso8601.dur.valid3(
275	  st: Iso8601.DurS, has: Bool, tok: Bool
276	) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
277	  match has:
278	    case False{}:
279	      Fail{Invalid{}}
280	    case True{}:
281	      match tok:
282	        case False{}:
283	          Fail{Invalid{}}
284	        case True{}:
285	          Iso8601.dur.mk(st)
286	def Iso8601.dur.valid(+st: Iso8601.DurS) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
287	  match st:
288	    case DurS{_, _, _, _, _, +saw_d, +saw_t, +saw_h, +saw_m, +saw_s}:
289	      Iso8601.dur.valid3(
290	        st,
291	        Iso8601.or4(saw_d, saw_h, saw_m, saw_s),
292	        Bool.or(Bool.not(saw_t), Iso8601.or3(saw_h, saw_m, saw_s))
293	      )
294	def Iso8601.dur.eof(
295	  st: Iso8601.DurS, mode: Iso8601.DurM
296	) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
297	  match mode:
298	    case DSeek{}:
299	      Iso8601.dur.valid(st)
300	    case DNum{_}:
301	      Fail{Invalid{}}
302	    case DFrac{_, _, _}:
303	      Fail{Invalid{}}
304	def Iso8601.dur.put_t2(
305	  days: U32, h: U32, mi: U32, s: U32, nanos: U32,
306	  saw_d: Bool, saw_h: Bool, saw_m: Bool, saw_s: Bool, dup: Bool
307	) -> Result<&2, &2, Iso8601.Error, Iso8601.DurS>:
308	  match dup:
309	    case True{}:
310	      Fail{Invalid{}}
311	    case False{}:
312	      Done{DurS{days, h, mi, s, nanos, saw_d, True{}, saw_h, saw_m, saw_s}}
313	def Iso8601.dur.put_t(st: Iso8601.DurS) -> Result<&2, &2, Iso8601.Error, Iso8601.DurS>:
314	  match st:
315	    case DurS{days, h, mi, s, nanos, saw_d, +saw_t, saw_h, saw_m, saw_s}:
316	      Iso8601.dur.put_t2(
317	        days, h, mi, s, nanos, saw_d, saw_h, saw_m, saw_s, saw_t
318	      )
319	def Iso8601.dur.put_d2(
320	  n: U32, h: U32, mi: U32, s: U32, nanos: U32,
321	  saw_h: Bool, saw_m: Bool, saw_s: Bool, bad: Bool
322	) -> Result<&2, &2, Iso8601.Error, Iso8601.DurS>:
323	  match bad:
324	    case True{}:
325	      Fail{Invalid{}}
326	    case False{}:
327	      Done{DurS{n, h, mi, s, nanos, True{}, False{}, saw_h, saw_m, saw_s}}
328	def Iso8601.dur.put_d(
329	  st: Iso8601.DurS, n: U32
330	) -> Result<&2, &2, Iso8601.Error, Iso8601.DurS>:
331	  match st:
332	    case DurS{_, h, mi, s, nanos, +saw_d, +saw_t, saw_h, saw_m, saw_s}:
333	      Iso8601.dur.put_d2(
334	        n, h, mi, s, nanos, saw_h, saw_m, saw_s, Bool.or(saw_d, saw_t)
335	      )
336	def Iso8601.dur.put_h2(
337	  days: U32, n: U32, mi: U32, s: U32, nanos: U32,
338	  saw_d: Bool, saw_m: Bool, saw_s: Bool, bad: Bool
339	) -> Result<&2, &2, Iso8601.Error, Iso8601.DurS>:
340	  match bad:
341	    case True{}:
342	      Fail{Invalid{}}
343	    case False{}:
344	      Done{DurS{days, n, mi, s, nanos, saw_d, True{}, True{}, saw_m, saw_s}}
345	def Iso8601.dur.put_h(
346	  st: Iso8601.DurS, n: U32
347	) -> Result<&2, &2, Iso8601.Error, Iso8601.DurS>:
348	  match st:
349	    case DurS{days, _, mi, s, nanos, saw_d, +saw_t, +saw_h, +saw_m, +saw_s}:
350	      Iso8601.dur.put_h2(
351	        days, n, mi, s, nanos, saw_d, saw_m, saw_s,
352	        Bool.or(Bool.not(saw_t), Iso8601.or3(saw_h, saw_m, saw_s))
353	      )
354	def Iso8601.dur.put_m2(
355	  days: U32, h: U32, n: U32, s: U32, nanos: U32,
356	  saw_d: Bool, saw_h: Bool, saw_s: Bool, bad: Bool
357	) -> Result<&2, &2, Iso8601.Error, Iso8601.DurS>:
358	  match bad:
359	    case True{}:
360	      Fail{Invalid{}}
361	    case False{}:
362	      Done{DurS{days, h, n, s, nanos, saw_d, True{}, saw_h, True{}, saw_s}}
363	def Iso8601.dur.put_m(
364	  st: Iso8601.DurS, n: U32
365	) -> Result<&2, &2, Iso8601.Error, Iso8601.DurS>:
366	  match st:
367	    case DurS{days, h, _, s, nanos, saw_d, +saw_t, saw_h, +saw_m, +saw_s}:
368	      Iso8601.dur.put_m2(
369	        days, h, n, s, nanos, saw_d, saw_h, saw_s,
370	        Bool.or(Bool.not(saw_t), Bool.or(saw_m, saw_s))
371	      )
372	def Iso8601.dur.put_s2(
373	  days: U32, h: U32, mi: U32, n: U32, nanos: U32,
374	  saw_d: Bool, saw_h: Bool, saw_m: Bool, bad: Bool
375	) -> Result<&2, &2, Iso8601.Error, Iso8601.DurS>:
376	  match bad:
377	    case True{}:
378	      Fail{Invalid{}}
379	    case False{}:
380	      Done{DurS{days, h, mi, n, nanos, saw_d, True{}, saw_h, saw_m, True{}}}
381	def Iso8601.dur.put_s(
382	  st: Iso8601.DurS, n: U32, nanos: U32
383	) -> Result<&2, &2, Iso8601.Error, Iso8601.DurS>:
384	  match st:
385	    case DurS{days, h, mi, _, _, saw_d, +saw_t, saw_h, saw_m, +saw_s}:
386	      Iso8601.dur.put_s2(
387	        days, h, mi, n, nanos, saw_d, saw_h, saw_m,
388	        Bool.or(Bool.not(saw_t), saw_s)
389	      )
390	def Iso8601.dur.frac.scale(+acc: U32, got: Nat) -> U32:
391	  U32.mul(acc, U32.pow(10, Nat.sub(9n, got)))
392	def Iso8601.dur.cont_r(
393	  r: Result<&2, &2, Iso8601.Error, Iso8601.DurS>, mode: Iso8601.DurM
394	) -> Iso8601.DurC:
395	  match r:
396	    case Fail{e}:
397	      DurFail{e}
398	    case Done{st}:
399	      DurCont{st, mode}
400	def Iso8601.dur.ndig2(
401	  off: Nat, st: Iso8601.DurS, +acc: U32, +h: Char, s: P.Parse.St
402	) -> Iso8601.DurC:
403	  match s:
404	    case P.StOv{}:
405	      DurFail{Overflow{off}}
406	    case P.StBad{_}:
407	      DurFail{Invalid{}}
408	    case P.StOk{}:
409	      DurCont{st, DNum{P.Parse.nacc(acc, h)}}
410	def Iso8601.dur.ndig(
411	  off: Nat, st: Iso8601.DurS, +acc: U32, +h: Char
412	) -> Iso8601.DurC:
413	  Iso8601.dur.ndig2(off, st, acc, h, P.Parse.st.of(acc, h, U32.not(0)))
414	def Iso8601.dur.unit_dot(
415	  st: Iso8601.DurS, n: U32, is_dot: Bool
416	) -> Iso8601.DurC:
417	  match is_dot:
418	    case True{}:
419	      DurCont{st, DFrac{n, 0, 9n}}
420	    case False{}:
421	      DurFail{Invalid{}}
422	def Iso8601.dur.unit_s(
423	  st: Iso8601.DurS, n: U32, +c: Char, is_s: Bool
424	) -> Iso8601.DurC:
425	  match is_s:
426	    case True{}:
427	      Iso8601.dur.cont_r(Iso8601.dur.put_s(st, n, 0), DSeek{})
428	    case False{}:
429	      Iso8601.dur.unit_dot(st, n, Char.is_eq(c, '.'))
430	def Iso8601.dur.unit_m(
431	  st: Iso8601.DurS, n: U32, +c: Char, is_m: Bool
432	) -> Iso8601.DurC:
433	  match is_m:
434	    case True{}:
435	      Iso8601.dur.cont_r(Iso8601.dur.put_m(st, n), DSeek{})
436	    case False{}:
437	      Iso8601.dur.unit_s(st, n, c, Char.is_eq(c, 'S'))
438	def Iso8601.dur.unit_h(
439	  st: Iso8601.DurS, n: U32, +c: Char, is_h: Bool
440	) -> Iso8601.DurC:
441	  match is_h:
442	    case True{}:
443	      Iso8601.dur.cont_r(Iso8601.dur.put_h(st, n), DSeek{})
444	    case False{}:
445	      Iso8601.dur.unit_m(st, n, c, Char.is_eq(c, 'M'))
446	def Iso8601.dur.unit(
447	  st: Iso8601.DurS, n: U32, +c: Char
448	) -> Iso8601.DurC:
449	  Iso8601.dur.unit_h(st, n, c, Char.is_eq(c, 'H'))
450	def Iso8601.dur.unit_d(
451	  st: Iso8601.DurS, n: U32, +c: Char, is_d: Bool
452	) -> Iso8601.DurC:
453	  match is_d:
454	    case True{}:
455	      Iso8601.dur.cont_r(Iso8601.dur.put_d(st, n), DSeek{})
456	    case False{}:
457	      Iso8601.dur.unit(st, n, c)
458	def Iso8601.dur.num(
459	  off: Nat, st: Iso8601.DurS, acc: U32, +h: Char, is_dig: Bool
460	) -> Iso8601.DurC:
461	  match is_dig:
462	    case True{}:
463	      Iso8601.dur.ndig(off, st, acc, h)
464	    case False{}:
465	      Iso8601.dur.unit_d(st, acc, h, Char.is_eq(h, 'D'))
466	def Iso8601.dur.frac.s2(
467	  st: Iso8601.DurS, sec: U32, acc: U32, left: Nat, empty: Bool
468	) -> Iso8601.DurC:
469	  match empty:
470	    case True{}:
471	      DurFail{Invalid{}}
472	    case False{}:
473	      Iso8601.dur.cont_r(
474	        Iso8601.dur.put_s(st, sec, Iso8601.dur.frac.scale(acc, Nat.sub(9n, left))),
475	        DSeek{}
476	      )
477	def Iso8601.dur.frac.s(
478	  st: Iso8601.DurS, sec: U32, acc: U32, +left: Nat, is_s: Bool
479	) -> Iso8601.DurC:
480	  match is_s:
481	    case True{}:
482	      Iso8601.dur.frac.s2(st, sec, acc, left, Nat.is_eq(left, 9n))
483	    case False{}:
484	      DurFail{Invalid{}}
485	def Iso8601.dur.frac.dig(
486	  st: Iso8601.DurS, sec: U32, +acc: U32, left: Nat, +h: Char
487	) -> Iso8601.DurC:
488	  match left:
489	    case 0n:
490	      DurFail{Invalid{}}
491	    case 1n++p:
492	      DurCont{st, DFrac{sec, P.Parse.nacc(acc, h), p}}
493	def Iso8601.dur.frac(
494	  st: Iso8601.DurS, sec: U32, acc: U32, left: Nat, +h: Char, is_dig: Bool
495	) -> Iso8601.DurC:
496	  match is_dig:
497	    case True{}:
498	      Iso8601.dur.frac.dig(st, sec, acc, left, h)
499	    case False{}:
500	      Iso8601.dur.frac.s(st, sec, acc, left, Char.is_eq(h, 'S'))
501	def Iso8601.dur.seek2(
502	  off: Nat, st: Iso8601.DurS, +h: Char, is_dig: Bool
503	) -> Iso8601.DurC:
504	  match is_dig:
505	    case True{}:
506	      DurCont{st, DNum{P.Parse.nacc(0, h)}}
507	    case False{}:
508	      DurFail{Extra{off, h}}
509	def Iso8601.dur.seek(
510	  off: Nat, st: Iso8601.DurS, h: Char, is_t: Bool, is_dig: Bool
511	) -> Iso8601.DurC:
512	  match is_t:
513	    case True{}:
514	      Iso8601.dur.cont_r(Iso8601.dur.put_t(st), DSeek{})
515	    case False{}:
516	      Iso8601.dur.seek2(off, st, h, is_dig)
517	def Iso8601.dur.act(
518	  off: Nat, st: Iso8601.DurS, mode: Iso8601.DurM, +h: Char, is_t: Bool, is_dig: Bool
519	) -> Iso8601.DurC:
520	  match mode:
521	    case DSeek{}:
522	      Iso8601.dur.seek(off, st, h, is_t, is_dig)
523	    case DNum{acc}:
524	      Iso8601.dur.num(off, st, acc, h, is_dig)
525	    case DFrac{sec, acc, left}:
526	      Iso8601.dur.frac(st, sec, acc, left, h, is_dig)
527	def Iso8601.dur.go(
528	  s: String, +off: Nat, c: Iso8601.DurC
529	) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
530	  match s c:
531	    case _ DurFail{e}:
532	      Fail{e}
533	    case SNil{} DurCont{st, mode}:
534	      Iso8601.dur.eof(st, mode)
535	    case SCon{+h, t} DurCont{st, mode}:
536	      Iso8601.dur.go(
537	        t, 1n+off,
538	        Iso8601.dur.act(
539	          off, st, mode, h, Char.is_eq(h, 'T'), Char.is_digit(h)
540	        )
541	      )
542	def Iso8601.read_duration.p(
543	  r: Result<&2, &2, Iso8601.Error, P.Parse.Cur>
544	) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
545	  match r:
546	    case Fail{e}:
547	      Fail{e}
548	    case Done{P.Cur{s, off}}:
549	      Iso8601.dur.go(s, off, DurCont{Iso8601.dur0(), DSeek{}})
550	def Iso8601.read_duration(
551	  text: String
552	) -> Result<&2, &2, Iso8601.Error, Dur.Duration>:
553	  Iso8601.read_duration.p(Iso8601.expect(P.Parse.start(text), 'P'))
554	def Iso8601.per.mk2(
555	  r: Result<&2, &2, Per.Period.Error, Per.Period>
556	) -> Result<&2, &2, Iso8601.Error, Per.Period>:
557	  match r:
558	    case Fail{_}:
559	      Fail{Invalid{}}
560	    case Done{p}:
561	      Done{p}
562	def Iso8601.per.valid2(
563	  y: U32, m: U32, d: U32, ok: Bool
564	) -> Result<&2, &2, Iso8601.Error, Per.Period>:
565	  match ok:
566	    case False{}:
567	      Fail{Invalid{}}
568	    case True{}:
569	      Iso8601.per.mk2(Per.Period.from(y, m, d))
570	def Iso8601.per.valid(st: Iso8601.PerS) -> Result<&2, &2, Iso8601.Error, Per.Period>:
571	  match st:
572	    case PerS{+y, +m, +d, +saw_y, +saw_m, +saw_w, +saw_d}:
573	      Iso8601.per.valid2(y, m, d, Iso8601.or4(saw_y, saw_m, saw_w, saw_d))
574	def Iso8601.per.eof(
575	  st: Iso8601.PerS, mode: Iso8601.PerM
576	) -> Result<&2, &2, Iso8601.Error, Per.Period>:
577	  match mode:
578	    case PSeek{}:
579	      Iso8601.per.valid(st)
580	    case PNum{_}:
581	      Fail{Invalid{}}
582	def Iso8601.add_u32.go(+a: U32, +b: U32, ov: Bool) -> Result<&2, &2, Iso8601.Error, U32>:
583	  match ov:
584	    case True{}:
585	      Fail{Invalid{}}
586	    case False{}:
587	      Done{U32.add(a, b)}
588	def Iso8601.add_u32(+a: U32, +b: U32) -> Result<&2, &2, Iso8601.Error, U32>:
589	  Iso8601.add_u32.go(a, b, U32.is_gt(b, U32.sub(U32.not(0), a)))
590	def Iso8601.per.weeks2(+n: U32, ov: Bool) -> Result<&2, &2, Iso8601.Error, U32>:
591	  match ov:
592	    case True{}:
593	      Fail{Invalid{}}
594	    case False{}:
595	      Done{U32.mul(n, 7)}
596	def Iso8601.per.weeks(+n: U32) -> Result<&2, &2, Iso8601.Error, U32>:
597	  Iso8601.per.weeks2(n, U32.is_gt(n, U32.div(U32.not(0), 7)))
598	def Iso8601.per.put_y2(
599	  n: U32, m: U32, d: U32, saw_m: Bool, saw_w: Bool, saw_d: Bool, bad: Bool
600	) -> Result<&2, &2, Iso8601.Error, Iso8601.PerS>:
601	  match bad:
602	    case True{}:
603	      Fail{Invalid{}}
604	    case False{}:
605	      Done{PerS{n, m, d, True{}, saw_m, saw_w, saw_d}}
606	def Iso8601.per.put_y(
607	  st: Iso8601.PerS, n: U32
608	) -> Result<&2, &2, Iso8601.Error, Iso8601.PerS>:
609	  match st:
610	    case PerS{_, m, d, +saw_y, +saw_m, +saw_w, +saw_d}:
611	      Iso8601.per.put_y2(
612	        n, m, d, saw_m, saw_w, saw_d, Iso8601.or4(saw_y, saw_m, saw_w, saw_d)
613	      )
614	def Iso8601.per.put_m2(
615	  y: U32, n: U32, d: U32, saw_y: Bool, saw_w: Bool, saw_d: Bool, bad: Bool
616	) -> Result<&2, &2, Iso8601.Error, Iso8601.PerS>:
617	  match bad:
618	    case True{}:
619	      Fail{Invalid{}}
620	    case False{}:
621	      Done{PerS{y, n, d, saw_y, True{}, saw_w, saw_d}}
622	def Iso8601.per.put_m(
623	  st: Iso8601.PerS, n: U32
624	) -> Result<&2, &2, Iso8601.Error, Iso8601.PerS>:
625	  match st:
626	    case PerS{y, _, d, saw_y, +saw_m, +saw_w, +saw_d}:
627	      Iso8601.per.put_m2(
628	        y, n, d, saw_y, saw_w, saw_d, Iso8601.or3(saw_m, saw_w, saw_d)
629	      )
630	def Iso8601.per.put_w.go(
631	  y: U32, m: U32, saw_y: Bool, saw_m: Bool,
632	  rw: Result<&2, &2, Iso8601.Error, U32>
633	) -> Result<&2, &2, Iso8601.Error, Iso8601.PerS>:
634	  match rw:
635	    case Fail{e}:
636	      Fail{e}
637	    case Done{w}:
638	      Done{PerS{y, m, w, saw_y, saw_m, True{}, False{}}}
639	def Iso8601.per.put_w2(
640	  y: U32, m: U32, saw_y: Bool, saw_m: Bool, n: U32, bad: Bool
641	) -> Result<&2, &2, Iso8601.Error, Iso8601.PerS>:
642	  match bad:
643	    case True{}:
644	      Fail{Invalid{}}
645	    case False{}:
646	      Iso8601.per.put_w.go(y, m, saw_y, saw_m, Iso8601.per.weeks(n))
647	def Iso8601.per.put_w(
648	  st: Iso8601.PerS, n: U32
649	) -> Result<&2, &2, Iso8601.Error, Iso8601.PerS>:
650	  match st:
651	    case PerS{y, m, _, saw_y, saw_m, +saw_w, +saw_d}:
652	      Iso8601.per.put_w2(y, m, saw_y, saw_m, n, Bool.or(saw_w, saw_d))
653	def Iso8601.per.put_d.go(
654	  y: U32, m: U32, saw_y: Bool, saw_m: Bool, saw_w: Bool,
655	  rd: Result<&2, &2, Iso8601.Error, U32>
656	) -> Result<&2, &2, Iso8601.Error, Iso8601.PerS>:
657	  match rd:
658	    case Fail{e}:
659	      Fail{e}
660	    case Done{days}:
661	      Done{PerS{y, m, days, saw_y, saw_m, saw_w, True{}}}
662	def Iso8601.per.put_d2(
663	  y: U32, m: U32, d: U32, saw_y: Bool, saw_m: Bool, saw_w: Bool, n: U32, bad: Bool
664	) -> Result<&2, &2, Iso8601.Error, Iso8601.PerS>:
665	  match bad:
666	    case True{}:
667	      Fail{Invalid{}}
668	    case False{}:
669	      Iso8601.per.put_d.go(y, m, saw_y, saw_m, saw_w, Iso8601.add_u32(d, n))
670	def Iso8601.per.put_d(
671	  st: Iso8601.PerS, n: U32
672	) -> Result<&2, &2, Iso8601.Error, Iso8601.PerS>:
673	  match st:
674	    case PerS{y, m, d, saw_y, saw_m, saw_w, +saw_d}:
675	      Iso8601.per.put_d2(y, m, d, saw_y, saw_m, saw_w, n, saw_d)
676	def Iso8601.per.cont_r(
677	  r: Result<&2, &2, Iso8601.Error, Iso8601.PerS>, mode: Iso8601.PerM
678	) -> Iso8601.PerC:
679	  match r:
680	    case Fail{e}:
681	      PerFail{e}
682	    case Done{st}:
683	      PerCont{st, mode}
684	def Iso8601.per.ndig2(
685	  off: Nat, st: Iso8601.PerS, +acc: U32, +h: Char, s: P.Parse.St
686	) -> Iso8601.PerC:
687	  match s:
688	    case P.StOv{}:
689	      PerFail{Overflow{off}}
690	    case P.StBad{_}:
691	      PerFail{Invalid{}}
692	    case P.StOk{}:
693	      PerCont{st, PNum{P.Parse.nacc(acc, h)}}
694	def Iso8601.per.ndig(
695	  off: Nat, st: Iso8601.PerS, +acc: U32, +h: Char
696	) -> Iso8601.PerC:
697	  Iso8601.per.ndig2(off, st, acc, h, P.Parse.st.of(acc, h, U32.not(0)))
698	def Iso8601.per.unit_d(
699	  st: Iso8601.PerS, n: U32, is_d: Bool
700	) -> Iso8601.PerC:
701	  match is_d:
702	    case True{}:
703	      Iso8601.per.cont_r(Iso8601.per.put_d(st, n), PSeek{})
704	    case False{}:
705	      PerFail{Invalid{}}
706	def Iso8601.per.unit_w(
707	  st: Iso8601.PerS, n: U32, +c: Char, is_w: Bool
708	) -> Iso8601.PerC:
709	  match is_w:
710	    case True{}:
711	      Iso8601.per.cont_r(Iso8601.per.put_w(st, n), PSeek{})
712	    case False{}:
713	      Iso8601.per.unit_d(st, n, Char.is_eq(c, 'D'))
714	def Iso8601.per.unit_m(
715	  st: Iso8601.PerS, n: U32, +c: Char, is_m: Bool
716	) -> Iso8601.PerC:
717	  match is_m:
718	    case True{}:
719	      Iso8601.per.cont_r(Iso8601.per.put_m(st, n), PSeek{})
720	    case False{}:
721	      Iso8601.per.unit_w(st, n, c, Char.is_eq(c, 'W'))
722	def Iso8601.per.unit(
723	  st: Iso8601.PerS, n: U32, +c: Char
724	) -> Iso8601.PerC:
725	  Iso8601.per.unit_m(st, n, c, Char.is_eq(c, 'M'))
726	def Iso8601.per.unit_y(
727	  st: Iso8601.PerS, n: U32, +c: Char, is_y: Bool
728	) -> Iso8601.PerC:
729	  match is_y:
730	    case True{}:
731	      Iso8601.per.cont_r(Iso8601.per.put_y(st, n), PSeek{})
732	    case False{}:
733	      Iso8601.per.unit(st, n, c)
734	def Iso8601.per.num(
735	  off: Nat, st: Iso8601.PerS, acc: U32, +h: Char, is_dig: Bool
736	) -> Iso8601.PerC:
737	  match is_dig:
738	    case True{}:
739	      Iso8601.per.ndig(off, st, acc, h)
740	    case False{}:
741	      Iso8601.per.unit_y(st, acc, h, Char.is_eq(h, 'Y'))
742	def Iso8601.per.seek2(
743	  off: Nat, st: Iso8601.PerS, +h: Char, is_dig: Bool
744	) -> Iso8601.PerC:
745	  match is_dig:
746	    case True{}:
747	      PerCont{st, PNum{P.Parse.nacc(0, h)}}
748	    case False{}:
749	      PerFail{Extra{off, h}}
750	def Iso8601.per.seek(
751	  off: Nat, st: Iso8601.PerS, h: Char, is_t: Bool, is_dig: Bool
752	) -> Iso8601.PerC:
753	  match is_t:
754	    case True{}:
755	      PerFail{Invalid{}}
756	    case False{}:
757	      Iso8601.per.seek2(off, st, h, is_dig)
758	def Iso8601.per.act(
759	  off: Nat, st: Iso8601.PerS, mode: Iso8601.PerM, +h: Char, is_t: Bool, is_dig: Bool
760	) -> Iso8601.PerC:
761	  match mode:
762	    case PSeek{}:
763	      Iso8601.per.seek(off, st, h, is_t, is_dig)
764	    case PNum{acc}:
765	      Iso8601.per.num(off, st, acc, h, is_dig)
766	def Iso8601.per.go(
767	  s: String, +off: Nat, c: Iso8601.PerC
768	) -> Result<&2, &2, Iso8601.Error, Per.Period>:
769	  match s c:
770	    case _ PerFail{e}:
771	      Fail{e}
772	    case SNil{} PerCont{st, mode}:
773	      Iso8601.per.eof(st, mode)
774	    case SCon{+h, t} PerCont{st, mode}:
775	      Iso8601.per.go(
776	        t, 1n+off,
777	        Iso8601.per.act(
778	          off, st, mode, h, Char.is_eq(h, 'T'), Char.is_digit(h)
779	        )
780	      )
781	def Iso8601.read_period.p(
782	  r: Result<&2, &2, Iso8601.Error, P.Parse.Cur>
783	) -> Result<&2, &2, Iso8601.Error, Per.Period>:
784	  match r:
785	    case Fail{e}:
786	      Fail{e}
787	    case Done{P.Cur{s, off}}:
788	      Iso8601.per.go(s, off, PerCont{Iso8601.per0(), PSeek{}})
789	def Iso8601.read_period(
790	  text: String
791	) -> Result<&2, &2, Iso8601.Error, Per.Period>:
792	  Iso8601.read_period.p(Iso8601.expect(P.Parse.start(text), 'P'))