1	import Base
2	import 0xe49a3e6521e1b71e55654a885f27bcc1/parse.bend as P
3	import ./date.bend as D
4	import ./datetime.bend as DT
5	import ./instant.bend as I
6	
7	type Format.Error is Data:
8	  Unexpected{offset: Nat, char: Char}
9	  Eof{offset: Nat}
10	  Overflow{offset: Nat}
11	  Extra{offset: Nat, char: Char}
12	  InvalidDate{year: U32, month: U32, day: U32}
13	  InvalidTime{hour: U32, minute: U32, second: U32}
14	  InvalidOffset{hour: U32, minute: U32}
15	  NegativeZeroOffset{}
16	  BadFraction{offset: Nat}
17	
18	type Format.FracP is Data:
19	  FracP{frac: DT.TimeFrac, cur: P.Parse.Cur}
20	
21	type Format.OffP is Data:
22	  OffP{offset: DT.UtcOffset, cur: P.Parse.Cur}
23	
24	type Format.DateP is Data:
25	  DateP{date: D.Date, cur: P.Parse.Cur}
26	
27	def Format.from_parse(e: P.Parse.Error) -> Format.Error:
28	  match e:
29	    case P.Unexpected{offset, char}:
30	      Unexpected{offset, char}
31	    case P.Eof{offset}:
32	      Eof{offset}
33	    case P.Overflow{offset}:
34	      Overflow{offset}
35	    case P.Extra{offset, char}:
36	      Extra{offset, char}
37	
38	def Format.digit(n: U32) -> Char:
39	  Char.from_u32((Char.to_u32('0') + n : U32))
40	
41	def Format.pad2(+n: U32) -> String:
42	  SCon{
43	    Format.digit(U32.div(n, 10)),
44	    SCon{Format.digit(U32.mod(n, 10)), SNil{}}
45	  }
46	
47	def Format.pad4(+n: U32) -> String:
48	  SCon{
49	    Format.digit(U32.div(n, 1000)),
50	    SCon{
51	      Format.digit(U32.mod(U32.div(n, 100), 10)),
52	      SCon{
53	        Format.digit(U32.mod(U32.div(n, 10), 10)),
54	        SCon{Format.digit(U32.mod(n, 10)), SNil{}}
55	      }
56	    }
57	  }
58	
59	def Format.pad_n.go(k: Nat, +n: U32, acc: String) -> String:
60	  match k:
61	    case 0n:
62	      acc
63	    case 1n++p:
64	      Format.pad_n.go(
65	        p, U32.div(n, 10), SCon{Format.digit(U32.mod(n, 10)), acc}
66	      )
67	
68	def Format.pad_n(n: U32, k: Nat) -> String:
69	  Format.pad_n.go(k, n, SNil{})
70	
71	def Format.show_date(date: D.Date) -> String:
72	  match date:
73	    case D.Date{y, m, d}:
74	      String.append(
75	        Format.pad4(y),
76	        String.append(
77	          "-", String.append(Format.pad2(m), String.append("-", Format.pad2(d)))
78	        )
79	      )
80	
81	def Format.show_frac(frac: DT.TimeFrac) -> String:
82	  match frac:
83	    case DT.FracNone{}:
84	      SNil{}
85	    case DT.Frac{digits, value}:
86	      SCon{'.', Format.pad_n(value, digits)}
87	
88	def Format.show_off(offset: DT.UtcOffset) -> String:
89	  match offset:
90	    case DT.OffsetZero{}:
91	      "Z"
92	    case DT.OffsetEast{h, mi}:
93	      String.append(
94	        "+", String.append(Format.pad2(h), String.append(":", Format.pad2(mi)))
95	      )
96	    case DT.OffsetWest{h, mi}:
97	      String.append(
98	        "-", String.append(Format.pad2(h), String.append(":", Format.pad2(mi)))
99	      )
100	
101	def Format.show_time(time: DT.TimeOfDay) -> String:
102	  match time:
103	    case DT.TimeOfDay{h, mi, s, frac}:
104	      String.append(
105	        Format.pad2(h),
106	        String.append(
107	          ":",
108	          String.append(
109	            Format.pad2(mi),
110	            String.append(
111	              ":", String.append(Format.pad2(s), Format.show_frac(frac))
112	            )
113	          )
114	        )
115	      )
116	
117	def Format.show.join(ds: String, ts: String, os: String) -> String:
118	  String.append(ds, String.append("T", String.append(ts, os)))
119	
120	def Format.show(odt: DT.OffsetDateTime) -> String:
121	  match odt:
122	    case DT.OffsetDateTime{date, time, offset}:
123	      Format.show.join(
124	        Format.show_date(date), Format.show_time(time), Format.show_off(offset)
125	      )
126	
127	def Format.cur_off(cur: P.Parse.Cur) -> Nat:
128	  match cur:
129	    case P.Cur{_, off}:
130	      off
131	
132	def Format.nacc(+acc: U32, +h: Char) -> U32:
133	  U32.add(U32.mul(acc, 10), (Char.to_u32(h) - Char.to_u32('0') : U32))
134	
135	def Format.frac.end_ok2(
136	  s: String, acc: U32, off: Nat, got: Nat, z: Bool
137	) -> Result<&2, &2, Format.Error, Format.FracP>:
138	  match z:
139	    case True{}:
140	      Fail{BadFraction{off}}
141	    case False{}:
142	      Done{FracP{DT.Frac{got, acc}, P.Cur{s, off}}}
143	
144	def Format.frac.end_ok(
145	  s: String, acc: U32, off: Nat, +got: Nat
146	) -> Result<&2, &2, Format.Error, Format.FracP>:
147	  Format.frac.end_ok2(s, acc, off, got, Nat.is_eq(got, 0n))
148	
149	def Format.frac.go(
150	  s: String, n: Nat, dig: Bool, +h: Char, +acc: U32, off: Nat, got: Nat
151	) -> Result<&2, &2, Format.Error, Format.FracP>:
152	  match s n dig:
153	    case _ 0n True{}:
154	      Fail{BadFraction{off}}
155	    case _ 0n False{}:
156	      Format.frac.end_ok(SCon{h, s}, acc, off, got)
157	    case _ 1n++p False{}:
158	      Format.frac.end_ok(SCon{h, s}, acc, off, got)
159	    case SNil{} 1n++p True{}:
160	      Format.frac.end_ok(SNil{}, Format.nacc(acc, h), 1n+off, 1n+got)
161	    case SCon{+h2, t} 1n++p True{}:
162	      Format.frac.go(
163	        t, p, Char.is_digit(h2), h2, Format.nacc(acc, h), 1n+off, 1n+got
164	      )
165	
166	def Format.frac.start(
167	  s: String, off: Nat
168	) -> Result<&2, &2, Format.Error, Format.FracP>:
169	  match s:
170	    case SNil{}:
171	      Fail{BadFraction{off}}
172	    case SCon{+h, t}:
173	      Format.frac.go(t, 9n, Char.is_digit(h), h, 0, off, 0n)
174	
175	def Format.frac.digits2(
176	  r: Result<&2, &2, P.Parse.Error, P.Parse.Cur>
177	) -> Result<&2, &2, Format.Error, Format.FracP>:
178	  match r:
179	    case Fail{e}:
180	      Fail{Format.from_parse(e)}
181	    case Done{P.Cur{rest, off}}:
182	      Format.frac.start(rest, off)
183	
184	def Format.frac.dot(
185	  cur: P.Parse.Cur, is_dot: Bool
186	) -> Result<&2, &2, Format.Error, Format.FracP>:
187	  match is_dot:
188	    case False{}:
189	      Done{FracP{DT.FracNone{}, cur}}
190	    case True{}:
191	      Format.frac.digits2(P.Parse.expect_char(cur, '.'))
192	
193	def Format.frac.after2(
194	  cur: P.Parse.Cur, m: Maybe<&2, Char>
195	) -> Result<&2, &2, Format.Error, Format.FracP>:
196	  match m:
197	    case None{}:
198	      Done{FracP{DT.FracNone{}, cur}}
199	    case Some{c}:
200	      Format.frac.dot(cur, Char.is_eq(c, '.'))
201	
202	def Format.frac.after(
203	  +cur: P.Parse.Cur
204	) -> Result<&2, &2, Format.Error, Format.FracP>:
205	  Format.frac.after2(cur, P.Parse.peek(cur))
206	
207	def Format.off.mk(
208	  west: Bool, h: U32, mi: U32, cur: P.Parse.Cur,
209	  r: Result<&2, &2, DT.UtcOffset.Error, DT.UtcOffset>
210	) -> Result<&2, &2, Format.Error, Format.OffP>:
211	  match r:
212	    case Fail{DT.NegativeZero{}}:
213	      Fail{NegativeZeroOffset{}}
214	    case Fail{DT.InvalidOffset{hh, mm}}:
215	      Fail{InvalidOffset{hh, mm}}
216	    case Done{off}:
217	      Done{OffP{off, cur}}
218	
219	def Format.off.min2(
220	  +west: Bool, +h: U32, r: Result<&2, &2, P.Parse.Error, P.Parse.Dec>
221	) -> Result<&2, &2, Format.Error, Format.OffP>:
222	  match r:
223	    case Fail{e}:
224	      Fail{Format.from_parse(e)}
225	    case Done{P.Dec{+mi, cur}}:
226	      Format.off.mk(west, h, mi, cur, DT.UtcOffset.from(west, h, mi))
227	
228	def Format.off.colon(
229	  west: Bool, h: U32, r: Result<&2, &2, P.Parse.Error, P.Parse.Cur>
230	) -> Result<&2, &2, Format.Error, Format.OffP>:
231	  match r:
232	    case Fail{e}:
233	      Fail{Format.from_parse(e)}
234	    case Done{cur}:
235	      Format.off.min2(west, h, P.Parse.read_fixed_decimal(cur, 2n, 99))
236	
237	def Format.off.hour2(
238	  west: Bool, r: Result<&2, &2, P.Parse.Error, P.Parse.Dec>
239	) -> Result<&2, &2, Format.Error, Format.OffP>:
240	  match r:
241	    case Fail{e}:
242	      Fail{Format.from_parse(e)}
243	    case Done{P.Dec{h, cur}}:
244	      Format.off.colon(west, h, P.Parse.expect_char(cur, ':'))
245	
246	def Format.off.sign2(
247	  west: Bool, r: Result<&2, &2, P.Parse.Error, P.Parse.Cur>
248	) -> Result<&2, &2, Format.Error, Format.OffP>:
249	  match r:
250	    case Fail{e}:
251	      Fail{Format.from_parse(e)}
252	    case Done{cur}:
253	      Format.off.hour2(west, P.Parse.read_fixed_decimal(cur, 2n, 99))
254	
255	def Format.off.z2(
256	  r: Result<&2, &2, P.Parse.Error, P.Parse.Cur>
257	) -> Result<&2, &2, Format.Error, Format.OffP>:
258	  match r:
259	    case Fail{e}:
260	      Fail{Format.from_parse(e)}
261	    case Done{cur}:
262	      Done{OffP{DT.OffsetZero{}, cur}}
263	
264	def Format.off.minus(
265	  minus: Bool, cur: P.Parse.Cur, +c: Char
266	) -> Result<&2, &2, Format.Error, Format.OffP>:
267	  match minus:
268	    case True{}:
269	      Format.off.sign2(True{}, P.Parse.expect_char(cur, '-'))
270	    case False{}:
271	      Fail{Unexpected{Format.cur_off(cur), c}}
272	
273	def Format.off.pm(
274	  plus: Bool, minus: Bool, cur: P.Parse.Cur, +c: Char
275	) -> Result<&2, &2, Format.Error, Format.OffP>:
276	  match plus:
277	    case True{}:
278	      Format.off.sign2(False{}, P.Parse.expect_char(cur, '+'))
279	    case False{}:
280	      Format.off.minus(minus, cur, c)
281	
282	def Format.off.ch2(
283	  z: Bool, plus: Bool, minus: Bool, cur: P.Parse.Cur, +c: Char
284	) -> Result<&2, &2, Format.Error, Format.OffP>:
285	  match z:
286	    case True{}:
287	      Format.off.z2(P.Parse.expect_char(cur, 'Z'))
288	    case False{}:
289	      Format.off.pm(plus, minus, cur, c)
290	
291	def Format.off.ch(
292	  cur: P.Parse.Cur, +c: Char
293	) -> Result<&2, &2, Format.Error, Format.OffP>:
294	  Format.off.ch2(
295	    Char.is_eq(c, 'Z'), Char.is_eq(c, '+'), Char.is_eq(c, '-'), cur, c
296	  )
297	
298	def Format.off.after2(
299	  cur: P.Parse.Cur, m: Maybe<&2, Char>
300	) -> Result<&2, &2, Format.Error, Format.OffP>:
301	  match m:
302	    case None{}:
303	      Fail{Eof{Format.cur_off(cur)}}
304	    case Some{c}:
305	      Format.off.ch(cur, c)
306	
307	def Format.off.after(
308	  +cur: P.Parse.Cur
309	) -> Result<&2, &2, Format.Error, Format.OffP>:
310	  Format.off.after2(cur, P.Parse.peek(cur))
311	
312	def Format.civil.mk(
313	  +y: U32, +m: U32, +d: U32, cur: P.Parse.Cur,
314	  r: Result<&2, &2, D.Date.Error, D.Date>
315	) -> Result<&2, &2, Format.Error, Format.DateP>:
316	  match r:
317	    case Fail{D.InvalidDate{yy, mm, dd}}:
318	      Fail{InvalidDate{yy, mm, dd}}
319	    case Fail{D.OutOfRange{}}:
320	      Fail{InvalidDate{y, m, d}}
321	    case Done{date}:
322	      Done{DateP{date, cur}}
323	
324	def Format.civil.d2(
325	  +y: U32, +m: U32, r: Result<&2, &2, P.Parse.Error, P.Parse.Dec>
326	) -> Result<&2, &2, Format.Error, Format.DateP>:
327	  match r:
328	    case Fail{e}:
329	      Fail{Format.from_parse(e)}
330	    case Done{P.Dec{+d, cur}}:
331	      Format.civil.mk(y, m, d, cur, D.Date.from(y, m, d))
332	
333	def Format.civil.dash2(
334	  y: U32, m: U32, r: Result<&2, &2, P.Parse.Error, P.Parse.Cur>
335	) -> Result<&2, &2, Format.Error, Format.DateP>:
336	  match r:
337	    case Fail{e}:
338	      Fail{Format.from_parse(e)}
339	    case Done{cur}:
340	      Format.civil.d2(y, m, P.Parse.read_fixed_decimal(cur, 2n, 99))
341	
342	def Format.civil.m2(
343	  y: U32, r: Result<&2, &2, P.Parse.Error, P.Parse.Dec>
344	) -> Result<&2, &2, Format.Error, Format.DateP>:
345	  match r:
346	    case Fail{e}:
347	      Fail{Format.from_parse(e)}
348	    case Done{P.Dec{m, cur}}:
349	      Format.civil.dash2(y, m, P.Parse.expect_char(cur, '-'))
350	
351	def Format.civil.dash1(
352	  y: U32, r: Result<&2, &2, P.Parse.Error, P.Parse.Cur>
353	) -> Result<&2, &2, Format.Error, Format.DateP>:
354	  match r:
355	    case Fail{e}:
356	      Fail{Format.from_parse(e)}
357	    case Done{cur}:
358	      Format.civil.m2(y, P.Parse.read_fixed_decimal(cur, 2n, 99))
359	
360	def Format.civil.y(
361	  r: Result<&2, &2, P.Parse.Error, P.Parse.Dec>
362	) -> Result<&2, &2, Format.Error, Format.DateP>:
363	  match r:
364	    case Fail{e}:
365	      Fail{Format.from_parse(e)}
366	    case Done{P.Dec{y, cur}}:
367	      Format.civil.dash1(y, P.Parse.expect_char(cur, '-'))
368	
369	def Format.civil(text: String) -> Result<&2, &2, Format.Error, Format.DateP>:
370	  Format.civil.y(P.Parse.read_fixed_decimal(P.Parse.start(text), 4n, 9999))
371	
372	def Format.read_date.fin2(
373	  date: D.Date, r: Result<&2, &2, P.Parse.Error, Unit>
374	) -> Result<&2, &2, Format.Error, D.Date>:
375	  match r:
376	    case Fail{e}:
377	      Fail{Format.from_parse(e)}
378	    case Done{_}:
379	      Done{date}
380	
381	def Format.read_date.fin(
382	  r: Result<&2, &2, Format.Error, Format.DateP>
383	) -> Result<&2, &2, Format.Error, D.Date>:
384	  match r:
385	    case Fail{e}:
386	      Fail{e}
387	    case Done{DateP{date, cur}}:
388	      Format.read_date.fin2(date, P.Parse.finish(cur))
389	
390	def Format.read_date(text: String) -> Result<&2, &2, Format.Error, D.Date>:
391	  Format.read_date.fin(Format.civil(text))
392	
393	def Format.read.fin2(
394	  odt: DT.OffsetDateTime, r: Result<&2, &2, P.Parse.Error, Unit>
395	) -> Result<&2, &2, Format.Error, DT.OffsetDateTime>:
396	  match r:
397	    case Fail{e}:
398	      Fail{Format.from_parse(e)}
399	    case Done{_}:
400	      Done{odt}
401	
402	def Format.read.off2(
403	  date: D.Date, time: DT.TimeOfDay,
404	  r: Result<&2, &2, Format.Error, Format.OffP>
405	) -> Result<&2, &2, Format.Error, DT.OffsetDateTime>:
406	  match r:
407	    case Fail{e}:
408	      Fail{e}
409	    case Done{OffP{offset, cur}}:
410	      Format.read.fin2(DT.OffsetDateTime.from(date, time, offset), P.Parse.finish(cur))
411	
412	def Format.read.time2(
413	  date: D.Date, +h: U32, +mi: U32, +s: U32, frac: DT.TimeFrac, cur: P.Parse.Cur,
414	  r: Result<&2, &2, DT.TimeOfDay.Error, DT.TimeOfDay>
415	) -> Result<&2, &2, Format.Error, DT.OffsetDateTime>:
416	  match r:
417	    case Fail{DT.InvalidTime{hh, mm, ss}}:
418	      Fail{InvalidTime{hh, mm, ss}}
419	    case Done{time}:
420	      Format.read.off2(date, time, Format.off.after(cur))
421	
422	def Format.read.frac2(
423	  date: D.Date, +h: U32, +mi: U32, +s: U32,
424	  r: Result<&2, &2, Format.Error, Format.FracP>
425	) -> Result<&2, &2, Format.Error, DT.OffsetDateTime>:
426	  match r:
427	    case Fail{e}:
428	      Fail{e}
429	    case Done{FracP{+frac, cur}}:
430	      Format.read.time2(
431	        date, h, mi, s, frac, cur, DT.TimeOfDay.from(h, mi, s, frac)
432	      )
433	
434	def Format.read.sec2(
435	  date: D.Date, h: U32, mi: U32,
436	  r: Result<&2, &2, P.Parse.Error, P.Parse.Dec>
437	) -> Result<&2, &2, Format.Error, DT.OffsetDateTime>:
438	  match r:
439	    case Fail{e}:
440	      Fail{Format.from_parse(e)}
441	    case Done{P.Dec{s, cur}}:
442	      Format.read.frac2(date, h, mi, s, Format.frac.after(cur))
443	
444	def Format.read.colon2(
445	  date: D.Date, h: U32, mi: U32,
446	  r: Result<&2, &2, P.Parse.Error, P.Parse.Cur>
447	) -> Result<&2, &2, Format.Error, DT.OffsetDateTime>:
448	  match r:
449	    case Fail{e}:
450	      Fail{Format.from_parse(e)}
451	    case Done{cur}:
452	      Format.read.sec2(date, h, mi, P.Parse.read_fixed_decimal(cur, 2n, 99))
453	
454	def Format.read.min2(
455	  date: D.Date, h: U32, r: Result<&2, &2, P.Parse.Error, P.Parse.Dec>
456	) -> Result<&2, &2, Format.Error, DT.OffsetDateTime>:
457	  match r:
458	    case Fail{e}:
459	      Fail{Format.from_parse(e)}
460	    case Done{P.Dec{mi, cur}}:
461	      Format.read.colon2(date, h, mi, P.Parse.expect_char(cur, ':'))
462	
463	def Format.read.colon1(
464	  date: D.Date, h: U32, r: Result<&2, &2, P.Parse.Error, P.Parse.Cur>
465	) -> Result<&2, &2, Format.Error, DT.OffsetDateTime>:
466	  match r:
467	    case Fail{e}:
468	      Fail{Format.from_parse(e)}
469	    case Done{cur}:
470	      Format.read.min2(date, h, P.Parse.read_fixed_decimal(cur, 2n, 99))
471	
472	def Format.read.hour2(
473	  date: D.Date, r: Result<&2, &2, P.Parse.Error, P.Parse.Dec>
474	) -> Result<&2, &2, Format.Error, DT.OffsetDateTime>:
475	  match r:
476	    case Fail{e}:
477	      Fail{Format.from_parse(e)}
478	    case Done{P.Dec{h, cur}}:
479	      Format.read.colon1(date, h, P.Parse.expect_char(cur, ':'))
480	
481	def Format.read.t2(
482	  date: D.Date, r: Result<&2, &2, P.Parse.Error, P.Parse.Cur>
483	) -> Result<&2, &2, Format.Error, DT.OffsetDateTime>:
484	  match r:
485	    case Fail{e}:
486	      Fail{Format.from_parse(e)}
487	    case Done{cur}:
488	      Format.read.hour2(date, P.Parse.read_fixed_decimal(cur, 2n, 99))
489	
490	def Format.read.after_date(
491	  r: Result<&2, &2, Format.Error, Format.DateP>
492	) -> Result<&2, &2, Format.Error, DT.OffsetDateTime>:
493	  match r:
494	    case Fail{e}:
495	      Fail{e}
496	    case Done{DateP{date, cur}}:
497	      Format.read.t2(date, P.Parse.expect_char(cur, 'T'))
498	
499	def Format.read(
500	  text: String
501	) -> Result<&2, &2, Format.Error, DT.OffsetDateTime>:
502	  Format.read.after_date(Format.civil(text))
503	
504	def Format.show_read(
505	  r: Result<&2, &2, Format.Error, DT.OffsetDateTime>
506	) -> Result<&2, &2, Format.Error, String>:
507	  match r:
508	    case Fail{e}:
509	      Fail{e}
510	    case Done{odt}:
511	      Done{Format.show(odt)}
512	
513	def Format.show_instant.map(
514	  r: Result<&2, &2, D.Date.Error, DT.OffsetDateTime>
515	) -> Result<&2, &2, D.Date.Error, String>:
516	  match r:
517	    case Fail{e}:
518	      Fail{e}
519	    case Done{odt}:
520	      Done{Format.show(odt)}
521	
522	def Format.show_instant(
523	  i: I.Instant
524	) -> Result<&2, &2, D.Date.Error, String>:
525	  Format.show_instant.map(DT.OffsetDateTime.from_instant_utc(i))
526	
527	def Format.read_instant.map(
528	  r: Result<&2, &2, Format.Error, DT.OffsetDateTime>
529	) -> Result<&2, &2, Format.Error, I.Instant>:
530	  match r:
531	    case Fail{e}:
532	      Fail{e}
533	    case Done{odt}:
534	      Done{DT.OffsetDateTime.to_instant(odt)}
535	
536	def Format.read_instant(
537	  text: String
538	) -> Result<&2, &2, Format.Error, I.Instant>:
539	  Format.read_instant.map(Format.read(text))