1	import Base
2	import ./date.bend as D
3	import ./duration.bend as Dur
4	import ./instant.bend as I
5	import ./period.bend as Per
6	
7	type TimeFrac is Data:
8	  FracNone{}
9	  Frac{digits: Nat, value: U32}
10	
11	type TimeOfDay.Error is Data:
12	  InvalidTime{hour: U32, minute: U32, second: U32}
13	
14	type TimeOfDay is Data:
15	  TimeOfDay{hour: U32, minute: U32, second: U32, frac: TimeFrac}
16	
17	type UtcOffset.Error is Data:
18	  InvalidOffset{hour: U32, minute: U32}
19	  NegativeZero{}
20	
21	type UtcOffset is Data:
22	  OffsetZero{}
23	  OffsetEast{hour: U32, minute: U32}
24	  OffsetWest{hour: U32, minute: U32}
25	
26	type OffsetDateTime is Data:
27	  OffsetDateTime{date: D.Date, time: TimeOfDay, offset: UtcOffset}
28	
29	type LocalDateTime is Data:
30	  LocalDateTime{date: D.Date, time: TimeOfDay}
31	
32	def TimeOfDay.from.frac(+h: U32, +mi: U32, +s: U32, frac: TimeFrac, ok: Bool) ->
33	  Result<&2, &2, TimeOfDay.Error, TimeOfDay>:
34	  match ok:
35	    case False{}:
36	      Fail{InvalidTime{h, mi, s}}
37	    case True{}:
38	      Done{TimeOfDay{h, mi, s, frac}}
39	
40	def TimeOfDay.from(
41	  +h: U32, +mi: U32, +s: U32, frac: TimeFrac
42	) -> Result<&2, &2, TimeOfDay.Error, TimeOfDay>:
43	  TimeOfDay.from.frac(
44	    h, mi, s, frac,
45	    Bool.and(
46	      U32.is_le(h, 23),
47	      Bool.and(U32.is_le(mi, 59), U32.is_le(s, 59))
48	    )
49	  )
50	
51	def UtcOffset.from.zero(
52	  z: Bool, west: Bool, +h: U32, +mi: U32
53	) -> Result<&2, &2, UtcOffset.Error, UtcOffset>:
54	  match z west:
55	    case True{} True{}:
56	      Fail{NegativeZero{}}
57	    case True{} False{}:
58	      Done{OffsetZero{}}
59	    case False{} True{}:
60	      Done{OffsetWest{h, mi}}
61	    case False{} False{}:
62	      Done{OffsetEast{h, mi}}
63	
64	def UtcOffset.from.range(
65	  west: Bool, +h: U32, +mi: U32, ok: Bool
66	) -> Result<&2, &2, UtcOffset.Error, UtcOffset>:
67	  match ok:
68	    case False{}:
69	      Fail{InvalidOffset{h, mi}}
70	    case True{}:
71	      UtcOffset.from.zero(
72	        Bool.and(U32.is_eq(h, 0), U32.is_eq(mi, 0)), west, h, mi
73	      )
74	
75	def UtcOffset.from(
76	  west: Bool, +h: U32, +mi: U32
77	) -> Result<&2, &2, UtcOffset.Error, UtcOffset>:
78	  UtcOffset.from.range(
79	    west, h, mi, Bool.and(U32.is_le(h, 23), U32.is_le(mi, 59))
80	  )
81	
82	def UtcOffset.zero() -> UtcOffset:
83	  OffsetZero{}
84	
85	def Datetime.sod(+h: U32, +mi: U32, +s: U32) -> U32:
86	  U32.add(U32.add(U32.mul(h, 3600), U32.mul(mi, 60)), s)
87	
88	def Datetime.off_sec(+h: U32, +mi: U32) -> U32:
89	  U32.add(U32.mul(h, 3600), U32.mul(mi, 60))
90	
91	def Datetime.frac_nanos(frac: TimeFrac) -> U32:
92	  match frac:
93	    case FracNone{}:
94	      0
95	    case Frac{digits, value}:
96	      U32.mul(value, U32.pow(10, Nat.sub(9n, digits)))
97	
98	def Datetime.utc_east2(
99	  days: U32, +local: U32, +off: U32, ge: Bool
100	) -> U32 & U32:
101	  match ge:
102	    case True{}:
103	      (days, U32.sub(local, off))
104	    case False{}:
105	      (U32.sub(days, 1), U32.sub(U32.add(local, 86400), off))
106	
107	def Datetime.utc_east(days: U32, +local: U32, +off: U32) -> U32 & U32:
108	  Datetime.utc_east2(days, local, off, U32.is_ge(local, off))
109	
110	def Datetime.utc_west2(
111	  days: U32, +local: U32, +off: U32, ge: Bool
112	) -> U32 & U32:
113	  match ge:
114	    case True{}:
115	      (U32.add(days, 1), U32.sub(U32.add(local, off), 86400))
116	    case False{}:
117	      (days, U32.add(local, off))
118	
119	def Datetime.utc_west(days: U32, +local: U32, +off: U32) -> U32 & U32:
120	  Datetime.utc_west2(
121	    days, local, off, U32.is_ge(U32.add(local, off), 86400)
122	  )
123	
124	def Datetime.apply_off(
125	  days: U32, local: U32, offset: UtcOffset
126	) -> U32 & U32:
127	  match offset:
128	    case OffsetZero{}:
129	      (days, local)
130	    case OffsetEast{h, mi}:
131	      Datetime.utc_east(days, local, Datetime.off_sec(h, mi))
132	    case OffsetWest{h, mi}:
133	      Datetime.utc_west(days, local, Datetime.off_sec(h, mi))
134	
135	def Datetime.unapply_off(
136	  days: U32, utc: U32, offset: UtcOffset
137	) -> U32 & U32:
138	  match offset:
139	    case OffsetZero{}:
140	      (days, utc)
141	    case OffsetEast{h, mi}:
142	      Datetime.utc_west(days, utc, Datetime.off_sec(h, mi))
143	    case OffsetWest{h, mi}:
144	      Datetime.utc_east(days, utc, Datetime.off_sec(h, mi))
145	
146	def Datetime.inst_of2(ds: U32 & U32, nanos: U32) -> I.Instant:
147	  (days, sod) = ds
148	  I.Instant{days, sod, nanos}
149	
150	def Datetime.inst_of(
151	  date: D.Date, time: TimeOfDay, offset: UtcOffset
152	) -> I.Instant:
153	  match time:
154	    case TimeOfDay{h, mi, s, frac}:
155	      Datetime.inst_of2(
156	        Datetime.apply_off(D.Date.to_days(date), Datetime.sod(h, mi, s), offset),
157	        Datetime.frac_nanos(frac)
158	      )
159	
160	def OffsetDateTime.to_instant(odt: OffsetDateTime) -> I.Instant:
161	  match odt:
162	    case OffsetDateTime{date, time, offset}:
163	      Datetime.inst_of(date, time, offset)
164	
165	def OffsetDateTime.same_instant(
166	  +a: OffsetDateTime, +b: OffsetDateTime
167	) -> Bool:
168	  I.Instant.is_eq(OffsetDateTime.to_instant(a), OffsetDateTime.to_instant(b))
169	
170	def OffsetDateTime.from(
171	  date: D.Date, time: TimeOfDay, offset: UtcOffset
172	) -> OffsetDateTime:
173	  OffsetDateTime{date, time, offset}
174	
175	def OffsetDateTime.to_unix.map(
176	  r: Result<&2, &2, I.Instant.Error, U32>
177	) -> Result<&2, &2, D.Date.Error, U32>:
178	  match r:
179	    case Fail{_}:
180	      Fail{D.OutOfRange{}}
181	    case Done{n}:
182	      Done{n}
183	
184	def OffsetDateTime.to_unix(
185	  odt: OffsetDateTime
186	) -> Result<&2, &2, D.Date.Error, U32>:
187	  OffsetDateTime.to_unix.map(I.Instant.to_unix(OffsetDateTime.to_instant(odt)))
188	
189	def OffsetDateTime.from_instant.clock(
190	  offset: UtcOffset, date: D.Date, r: Result<&2, &2, TimeOfDay.Error, TimeOfDay>
191	) -> Result<&2, &2, D.Date.Error, OffsetDateTime>:
192	  match r:
193	    case Fail{_}:
194	      Fail{D.OutOfRange{}}
195	    case Done{t}:
196	      Done{OffsetDateTime.from(date, t, offset)}
197	
198	def OffsetDateTime.from_instant.date(
199	  +sod: U32, offset: UtcOffset, r: Result<&2, &2, D.Date.Error, D.Date>
200	) -> Result<&2, &2, D.Date.Error, OffsetDateTime>:
201	  match r:
202	    case Fail{e}:
203	      Fail{e}
204	    case Done{date}:
205	      OffsetDateTime.from_instant.clock(
206	        offset, date,
207	        TimeOfDay.from(
208	          U32.div(sod, 3600),
209	          U32.div(U32.mod(sod, 3600), 60),
210	          U32.mod(sod, 60),
211	          FracNone{}
212	        )
213	      )
214	
215	def OffsetDateTime.from_instant.pair(
216	  ds: U32 & U32, offset: UtcOffset
217	) -> Result<&2, &2, D.Date.Error, OffsetDateTime>:
218	  (days, sod) = ds
219	  OffsetDateTime.from_instant.date(sod, offset, D.Date.from_days(days))
220	
221	def OffsetDateTime.from_instant(
222	  i: I.Instant, +offset: UtcOffset
223	) -> Result<&2, &2, D.Date.Error, OffsetDateTime>:
224	  match i:
225	    case I.Instant{days, sod, _}:
226	      OffsetDateTime.from_instant.pair(
227	        Datetime.unapply_off(days, sod, offset), offset
228	      )
229	
230	def OffsetDateTime.from_instant_utc(
231	  i: I.Instant
232	) -> Result<&2, &2, D.Date.Error, OffsetDateTime>:
233	  OffsetDateTime.from_instant(i, OffsetZero{})
234	
235	def OffsetDateTime.add.odt(
236	  r: Result<&2, &2, D.Date.Error, OffsetDateTime>
237	) -> Result<&2, &2, I.Instant.Error, OffsetDateTime>:
238	  match r:
239	    case Fail{_}:
240	      Fail{I.OutOfRange{}}
241	    case Done{o}:
242	      Done{o}
243	
244	def OffsetDateTime.add.map(
245	  offset: UtcOffset, r: Result<&2, &2, I.Instant.Error, I.Instant>
246	) -> Result<&2, &2, I.Instant.Error, OffsetDateTime>:
247	  match r:
248	    case Fail{e}:
249	      Fail{e}
250	    case Done{i}:
251	      OffsetDateTime.add.odt(OffsetDateTime.from_instant(i, offset))
252	
253	def OffsetDateTime.add(
254	  +odt: OffsetDateTime, d: Dur.Duration
255	) -> Result<&2, &2, I.Instant.Error, OffsetDateTime>:
256	  match odt:
257	    case OffsetDateTime{_, _, +offset}:
258	      OffsetDateTime.add.map(
259	        offset, I.Instant.add(OffsetDateTime.to_instant(odt), d)
260	      )
261	
262	def OffsetDateTime.sub(
263	  +odt: OffsetDateTime, d: Dur.Duration
264	) -> Result<&2, &2, I.Instant.Error, OffsetDateTime>:
265	  match odt:
266	    case OffsetDateTime{_, _, +offset}:
267	      OffsetDateTime.add.map(
268	        offset, I.Instant.sub(OffsetDateTime.to_instant(odt), d)
269	      )
270	
271	def LocalDateTime.from(date: D.Date, time: TimeOfDay) -> LocalDateTime:
272	  LocalDateTime{date, time}
273	
274	def LocalDateTime.at_offset(
275	  local: LocalDateTime, offset: UtcOffset
276	) -> OffsetDateTime:
277	  match local:
278	    case LocalDateTime{date, time}:
279	      OffsetDateTime.from(date, time, offset)
280	
281	def OffsetDateTime.to_local(odt: OffsetDateTime) -> LocalDateTime:
282	  match odt:
283	    case OffsetDateTime{date, time, _}:
284	      LocalDateTime.from(date, time)
285	
286	def OffsetDateTime.from_unix(
287	  secs: U32
288	) -> Result<&2, &2, D.Date.Error, OffsetDateTime>:
289	  OffsetDateTime.from_instant_utc(I.Instant.from_unix(secs))
290	
291	def Datetime.ldt_inst(ldt: LocalDateTime) -> I.Instant:
292	  match ldt:
293	    case LocalDateTime{date, TimeOfDay{+h, +mi, +s, frac}}:
294	      I.Instant{
295	        D.Date.to_days(date), Datetime.sod(h, mi, s), Datetime.frac_nanos(frac)
296	      }
297	
298	def Datetime.frac_of(+nanos: U32, z: Bool) -> TimeFrac:
299	  match z:
300	    case True{}:
301	      FracNone{}
302	    case False{}:
303	      Frac{9n, nanos}
304	
305	def Datetime.inst_ldt.tod(
306	  date: D.Date, r: Result<&2, &2, TimeOfDay.Error, TimeOfDay>
307	) -> Result<&2, &2, I.Instant.Error, LocalDateTime>:
308	  match r:
309	    case Fail{_}:
310	      Fail{I.OutOfRange{}}
311	    case Done{tod}:
312	      Done{LocalDateTime{date, tod}}
313	
314	def Datetime.inst_ldt.date(
315	  +sod: U32, +nanos: U32, r: Result<&2, &2, D.Date.Error, D.Date>
316	) -> Result<&2, &2, I.Instant.Error, LocalDateTime>:
317	  match r:
318	    case Fail{_}:
319	      Fail{I.OutOfRange{}}
320	    case Done{date}:
321	      Datetime.inst_ldt.tod(
322	        date,
323	        TimeOfDay.from(
324	          U32.div(sod, 3600),
325	          U32.div(U32.mod(sod, 3600), 60),
326	          U32.mod(sod, 60),
327	          Datetime.frac_of(nanos, U32.is_eq(nanos, 0))
328	        )
329	      )
330	
331	def Datetime.inst_ldt(
332	  i: I.Instant
333	) -> Result<&2, &2, I.Instant.Error, LocalDateTime>:
334	  match i:
335	    case I.Instant{+days, +sod, +nanos}:
336	      Datetime.inst_ldt.date(sod, nanos, D.Date.from_days(days))
337	
338	def LocalDateTime.add.map(
339	  r: Result<&2, &2, I.Instant.Error, I.Instant>
340	) -> Result<&2, &2, I.Instant.Error, LocalDateTime>:
341	  match r:
342	    case Fail{e}:
343	      Fail{e}
344	    case Done{i}:
345	      Datetime.inst_ldt(i)
346	
347	def LocalDateTime.add(
348	  ldt: LocalDateTime, d: Dur.Duration
349	) -> Result<&2, &2, I.Instant.Error, LocalDateTime>:
350	  LocalDateTime.add.map(I.Instant.add(Datetime.ldt_inst(ldt), d))
351	
352	def LocalDateTime.sub(
353	  ldt: LocalDateTime, d: Dur.Duration
354	) -> Result<&2, &2, I.Instant.Error, LocalDateTime>:
355	  LocalDateTime.add.map(I.Instant.sub(Datetime.ldt_inst(ldt), d))
356	
357	def LocalDateTime.until(
358	  start: LocalDateTime, end: LocalDateTime
359	) -> Result<&2, &2, I.Instant.Error, Dur.Duration>:
360	  I.Instant.until(Datetime.ldt_inst(start), Datetime.ldt_inst(end))
361	
362	def LocalDateTime.add_period.map(
363	  time: TimeOfDay, r: Result<&2, &2, D.Date.Error, D.Date>
364	) -> Result<&2, &2, D.Date.Error, LocalDateTime>:
365	  match r:
366	    case Fail{e}:
367	      Fail{e}
368	    case Done{date2}:
369	      Done{LocalDateTime{date2, time}}
370	
371	def LocalDateTime.add_period(
372	  ldt: LocalDateTime, p: Per.Period
373	) -> Result<&2, &2, D.Date.Error, LocalDateTime>:
374	  match ldt:
375	    case LocalDateTime{+date, +time}:
376	      LocalDateTime.add_period.map(time, Per.Period.add_to(p, date))
377	
378	def OffsetDateTime.add_period.map(
379	  offset: UtcOffset, r: Result<&2, &2, D.Date.Error, LocalDateTime>
380	) -> Result<&2, &2, D.Date.Error, OffsetDateTime>:
381	  match r:
382	    case Fail{e}:
383	      Fail{e}
384	    case Done{ldt}:
385	      Done{LocalDateTime.at_offset(ldt, offset)}
386	
387	def OffsetDateTime.add_period(
388	  +odt: OffsetDateTime, p: Per.Period
389	) -> Result<&2, &2, D.Date.Error, OffsetDateTime>:
390	  match odt:
391	    case OffsetDateTime{_, _, +offset}:
392	      OffsetDateTime.add_period.map(
393	        offset, LocalDateTime.add_period(OffsetDateTime.to_local(odt), p)
394	      )
395