datetime.bend
bend-datetime@0.4.0.0 · 395 lines · 0 definitions
1import Base
2import bend-datetime@0.4.0.0/date.bend as D
3import bend-datetime@0.4.0.0/duration.bend as Dur
4import bend-datetime@0.4.0.0/instant.bend as I
5import bend-datetime@0.4.0.0/period.bend as Per
6
7type TimeFrac is Data:
8 FracNone{}
9 Frac{digits: Nat, value: U32}
10
11type TimeOfDay.Error is Data:
12 InvalidTime{hour: U32, minute: U32, second: U32}
13
14type TimeOfDay is Data:
15 TimeOfDay{hour: U32, minute: U32, second: U32, frac: TimeFrac}
16
17type UtcOffset.Error is Data:
18 InvalidOffset{hour: U32, minute: U32}
19 NegativeZero{}
20
21type UtcOffset is Data:
22 OffsetZero{}
23 OffsetEast{hour: U32, minute: U32}
24 OffsetWest{hour: U32, minute: U32}
25
26type OffsetDateTime is Data:
27 OffsetDateTime{date: D.Date, time: TimeOfDay, offset: UtcOffset}
28
29type LocalDateTime is Data:
30 LocalDateTime{date: D.Date, time: TimeOfDay}
31
32def 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
40def 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
51def 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
64def 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
75def 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
82def UtcOffset.zero() -> UtcOffset:
83 OffsetZero{}
84
85def Datetime.sod(+h: U32, +mi: U32, +s: U32) -> U32:
86 U32.add(U32.add(U32.mul(h, 3600), U32.mul(mi, 60)), s)
87
88def Datetime.off_sec(+h: U32, +mi: U32) -> U32:
89 U32.add(U32.mul(h, 3600), U32.mul(mi, 60))
90
91def 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
98def 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
107def Datetime.utc_east(days: U32, +local: U32, +off: U32) -> U32 & U32:
108 Datetime.utc_east2(days, local, off, U32.is_ge(local, off))
109
110def 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
119def 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
124def 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
135def 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
146def Datetime.inst_of2(ds: U32 & U32, nanos: U32) -> I.Instant:
147 (days, sod) = ds
148 I.Instant{days, sod, nanos}
149
150def 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
160def OffsetDateTime.to_instant(odt: OffsetDateTime) -> I.Instant:
161 match odt:
162 case OffsetDateTime{date, time, offset}:
163 Datetime.inst_of(date, time, offset)
164
165def OffsetDateTime.same_instant(
166 +a: OffsetDateTime, +b: OffsetDateTime
167) -> Bool:
168 I.Instant.is_eq(OffsetDateTime.to_instant(a), OffsetDateTime.to_instant(b))
169
170def OffsetDateTime.from(
171 date: D.Date, time: TimeOfDay, offset: UtcOffset
172) -> OffsetDateTime:
173 OffsetDateTime{date, time, offset}
174
175def 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
184def 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
189def 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
198def 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
215def 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
221def 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
230def OffsetDateTime.from_instant_utc(
231 i: I.Instant
232) -> Result<&2, &2, D.Date.Error, OffsetDateTime>:
233 OffsetDateTime.from_instant(i, OffsetZero{})
234
235def 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
244def 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
253def 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
262def 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
271def LocalDateTime.from(date: D.Date, time: TimeOfDay) -> LocalDateTime:
272 LocalDateTime{date, time}
273
274def 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
281def OffsetDateTime.to_local(odt: OffsetDateTime) -> LocalDateTime:
282 match odt:
283 case OffsetDateTime{date, time, _}:
284 LocalDateTime.from(date, time)
285
286def 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
291def 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
298def Datetime.frac_of(+nanos: U32, z: Bool) -> TimeFrac:
299 match z:
300 case True{}:
301 FracNone{}
302 case False{}:
303 Frac{9n, nanos}
304
305def 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
314def 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
331def 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
338def 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
347def 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
352def 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
357def 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
362def 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
371def 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
378def 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
387def 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