date.bend
bend-datetime@0.4.0.0 · 486 lines · 0 definitions
1import Base
2
3type Date.Error is Data:
4 InvalidDate{year: U32, month: U32, day: U32}
5 OutOfRange{}
6
7type Date is Data:
8 Date{year: U32, month: U32, day: U32}
9
10def Date.leap.100(+y: U32, d100: Bool) -> Bool:
11 match d100:
12 case False{}:
13 True{}
14 case True{}:
15 U32.is_eq(U32.mod(y, 400), 0)
16
17def Date.leap.4(+y: U32, d4: Bool) -> Bool:
18 match d4:
19 case False{}:
20 False{}
21 case True{}:
22 Date.leap.100(y, U32.is_eq(U32.mod(y, 100), 0))
23
24def Date.leap(+y: U32) -> Bool:
25 Date.leap.4(y, U32.is_eq(U32.mod(y, 4), 0))
26
27def Date.dim.feb(leap: Bool) -> U32:
28 match leap:
29 case True{}:
30 29
31 case False{}:
32 28
33
34def Date.is_31(+m: U32) -> Bool:
35 Bool.or(
36 U32.is_eq(m, 1),
37 Bool.or(
38 U32.is_eq(m, 3),
39 Bool.or(
40 U32.is_eq(m, 5),
41 Bool.or(
42 U32.is_eq(m, 7),
43 Bool.or(
44 U32.is_eq(m, 8),
45 Bool.or(U32.is_eq(m, 10), U32.is_eq(m, 12))
46 )
47 )
48 )
49 )
50 )
51
52def Date.is_30(+m: U32) -> Bool:
53 Bool.or(
54 U32.is_eq(m, 4),
55 Bool.or(U32.is_eq(m, 6), Bool.or(U32.is_eq(m, 9), U32.is_eq(m, 11)))
56 )
57
58def Date.dim.rest3(m: U32, d30: Bool) -> Maybe<&2, U32>:
59 match d30:
60 case True{}:
61 Some{30}
62 case False{}:
63 None{}
64
65def Date.dim.rest2(+m: U32, d31: Bool) -> Maybe<&2, U32>:
66 match d31:
67 case True{}:
68 Some{31}
69 case False{}:
70 Date.dim.rest3(m, Date.is_30(m))
71
72def Date.dim.rest(+m: U32) -> Maybe<&2, U32>:
73 Date.dim.rest2(m, Date.is_31(m))
74
75def Date.dim.m(+m: U32, leap: Bool, feb: Bool) -> Maybe<&2, U32>:
76 match feb:
77 case True{}:
78 Some{Date.dim.feb(leap)}
79 case False{}:
80 Date.dim.rest(m)
81
82def Date.dim(+m: U32, leap: Bool) -> Maybe<&2, U32>:
83 Date.dim.m(m, leap, U32.is_eq(m, 2))
84
85def Date.from.day2(
86 +y: U32, +m: U32, +d: U32, ok: Bool
87) -> Result<&2, &2, Date.Error, Date>:
88 match ok:
89 case False{}:
90 Fail{InvalidDate{y, m, d}}
91 case True{}:
92 Done{Date{y, m, d}}
93
94def Date.from.day(
95 +y: U32, +m: U32, +d: U32, dim: U32
96) -> Result<&2, &2, Date.Error, Date>:
97 Date.from.day2(
98 y, m, d, Bool.and(U32.is_ge(d, 1), U32.is_le(d, dim))
99 )
100
101def Date.from.dim(
102 +y: U32, +m: U32, +d: U32, dim: Maybe<&2, U32>
103) -> Result<&2, &2, Date.Error, Date>:
104 match dim:
105 case None{}:
106 Fail{InvalidDate{y, m, d}}
107 case Some{n}:
108 Date.from.day(y, m, d, n)
109
110def Date.from.y(
111 +y: U32, +m: U32, +d: U32, ok: Bool
112) -> Result<&2, &2, Date.Error, Date>:
113 match ok:
114 case False{}:
115 Fail{InvalidDate{y, m, d}}
116 case True{}:
117 Date.from.dim(y, m, d, Date.dim(m, Date.leap(y)))
118
119def Date.from(
120 +y: U32, +m: U32, +d: U32
121) -> Result<&2, &2, Date.Error, Date>:
122 Date.from.y(y, m, d, Bool.and(U32.is_ge(y, 1), U32.is_le(y, 9999)))
123
124def Date.dim_of.go(dim: Maybe<&2, U32>) -> Result<&2, &2, Date.Error, U32>:
125 match dim:
126 case None{}:
127 Fail{OutOfRange{}}
128 case Some{+n}:
129 Done{n}
130
131def Date.dim_of(+y: U32, +m: U32) -> Result<&2, &2, Date.Error, U32>:
132 Date.dim_of.go(Date.dim(m, Date.leap(y)))
133
134def Date.days_in_month(date: Date) -> Result<&2, &2, Date.Error, U32>:
135 match date:
136 case Date{+y, +m, _}:
137 Date.dim_of(y, m)
138
139def Date.end_of_month.go(
140 +y: U32, +m: U32, r: Result<&2, &2, Date.Error, U32>
141) -> Result<&2, &2, Date.Error, Date>:
142 match r:
143 case Fail{e}:
144 Fail{e}
145 case Done{dim}:
146 Done{Date{y, m, dim}}
147
148def Date.end_of_month(date: Date) -> Result<&2, &2, Date.Error, Date>:
149 match date:
150 case Date{+y, +m, _}:
151 Date.end_of_month.go(y, m, Date.dim_of(y, m))
152
153def Date.start_of_month(date: Date) -> Date:
154 match date:
155 case Date{y, m, _}:
156 Date{y, m, 1}
157
158def Date.start_of_year(date: Date) -> Date:
159 match date:
160 case Date{y, _, _}:
161 Date{y, 1, 1}
162
163def Date.end_of_year(date: Date) -> Date:
164 match date:
165 case Date{y, _, _}:
166 Date{y, 12, 31}
167
168def Date.with_day(date: Date, d: U32) -> Result<&2, &2, Date.Error, Date>:
169 match date:
170 case Date{+y, +m, _}:
171 Date.from(y, m, d)
172
173def Date.with_month(date: Date, m: U32) -> Result<&2, &2, Date.Error, Date>:
174 match date:
175 case Date{+y, _, +d}:
176 Date.from(y, m, d)
177
178def Date.with_year(date: Date, y: U32) -> Result<&2, &2, Date.Error, Date>:
179 match date:
180 case Date{_, +m, +d}:
181 Date.from(y, m, d)
182
183def Date.y_adj(y: U32, jf: Bool) -> U32:
184 match jf:
185 case True{}:
186 U32.sub(y, 1)
187 case False{}:
188 y
189
190def Date.mp(m: U32, jf: Bool) -> U32:
191 match jf:
192 case True{}:
193 U32.add(m, 9)
194 case False{}:
195 U32.sub(m, 3)
196
197def Date.doy(+m: U32, +d: U32, jf: Bool) -> U32:
198 U32.sub(U32.add(U32.div(U32.add(U32.mul(153, Date.mp(m, jf)), 2), 5), d), 1)
199
200def Date.to_days.era(+era: U32, +yoe: U32, doy: U32) -> U32:
201 U32.add(
202 U32.mul(era, 146097),
203 U32.add(
204 U32.sub(
205 U32.add(U32.mul(yoe, 365), U32.div(yoe, 4)),
206 U32.div(yoe, 100)
207 ),
208 doy
209 )
210 )
211
212def Date.to_days.yoe(+ya: U32, doy: U32) -> U32:
213 Date.to_days.era(
214 U32.div(ya, 400),
215 U32.sub(ya, U32.mul(U32.div(ya, 400), 400)),
216 doy
217 )
218
219def Date.to_days.parts(+y: U32, +m: U32, +d: U32) -> U32:
220 Date.to_days.yoe(Date.y_adj(y, U32.is_le(m, 2)), Date.doy(m, d, U32.is_le(m, 2)))
221
222def Date.to_days(date: Date) -> U32:
223 match date:
224 case Date{y, m, d}:
225 Date.to_days.parts(y, m, d)
226
227def Date.is_eq(a: Date, b: Date) -> Bool:
228 match a b:
229 case Date{+y1, +m1, +d1} Date{+y2, +m2, +d2}:
230 Bool.and(
231 U32.is_eq(y1, y2),
232 Bool.and(U32.is_eq(m1, m2), U32.is_eq(d1, d2))
233 )
234
235def Date.is_lt(a: Date, b: Date) -> Bool:
236 U32.is_lt(Date.to_days(a), Date.to_days(b))
237
238def Date.is_gt(a: Date, b: Date) -> Bool:
239 Date.is_lt(b, a)
240
241def Date.is_le(a: Date, b: Date) -> Bool:
242 Bool.not(Date.is_lt(b, a))
243
244def Date.is_ge(a: Date, b: Date) -> Bool:
245 Bool.not(Date.is_lt(a, b))
246
247def Date.from_days.doe(+z: U32, era: U32) -> U32:
248 U32.sub(z, U32.mul(era, 146097))
249
250def Date.from_days.yoe(+doe: U32) -> U32:
251 U32.div(
252 U32.sub(
253 U32.add(U32.sub(doe, U32.div(doe, 1460)), U32.div(doe, 36524)),
254 U32.div(doe, 146096)
255 ),
256 365
257 )
258
259def Date.from_days.doy(+doe: U32, +yoe: U32) -> U32:
260 U32.sub(
261 doe,
262 U32.sub(
263 U32.add(U32.mul(365, yoe), U32.div(yoe, 4)),
264 U32.div(yoe, 100)
265 )
266 )
267
268def Date.from_days.mp(+doy: U32) -> U32:
269 U32.div(U32.add(U32.mul(5, doy), 2), 153)
270
271def Date.from_days.day(+doy: U32, +mp: U32) -> U32:
272 U32.add(U32.sub(doy, U32.div(U32.add(U32.mul(153, mp), 2), 5)), 1)
273
274def Date.from_days.month(+mp: U32, lt: Bool) -> U32:
275 match lt:
276 case True{}:
277 U32.add(mp, 3)
278 case False{}:
279 U32.sub(mp, 9)
280
281def Date.from_days.year(+y: U32, jan: Bool) -> U32:
282 match jan:
283 case True{}:
284 U32.add(y, 1)
285 case False{}:
286 y
287
288def Date.from_days.parts(+z: U32) -> Result<&2, &2, Date.Error, Date>:
289 +era = U32.div(z, 146097)
290 +doe = Date.from_days.doe(z, era)
291 +yoe = Date.from_days.yoe(doe)
292 +doy = Date.from_days.doy(doe, yoe)
293 +mp = Date.from_days.mp(doy)
294 +m = Date.from_days.month(mp, U32.is_lt(mp, 10))
295 Date.from(
296 Date.from_days.year(U32.add(yoe, U32.mul(era, 400)), U32.is_le(m, 2)),
297 m,
298 Date.from_days.day(doy, mp)
299 )
300
301def Date.from_days(z: U32) -> Result<&2, &2, Date.Error, Date>:
302 Date.from_days.parts(z)
303
304type Weekday is Data:
305 Mon{}
306 Tue{}
307 Wed{}
308 Thu{}
309 Fri{}
310 Sat{}
311 Sun{}
312
313def Date.weekday.n6(+n: U32, is6: Bool) -> Weekday:
314 match is6:
315 case True{}:
316 Sun{}
317 case False{}:
318 Sat{}
319
320def Date.weekday.n5(+n: U32, is5: Bool) -> Weekday:
321 match is5:
322 case True{}:
323 Sat{}
324 case False{}:
325 Date.weekday.n6(n, U32.is_eq(n, 6))
326
327def Date.weekday.n4(+n: U32, is4: Bool) -> Weekday:
328 match is4:
329 case True{}:
330 Fri{}
331 case False{}:
332 Date.weekday.n5(n, U32.is_eq(n, 5))
333
334def Date.weekday.n3(+n: U32, is3: Bool) -> Weekday:
335 match is3:
336 case True{}:
337 Thu{}
338 case False{}:
339 Date.weekday.n4(n, U32.is_eq(n, 4))
340
341def Date.weekday.n2(+n: U32, is2: Bool) -> Weekday:
342 match is2:
343 case True{}:
344 Wed{}
345 case False{}:
346 Date.weekday.n3(n, U32.is_eq(n, 3))
347
348def Date.weekday.n1(+n: U32, is1: Bool) -> Weekday:
349 match is1:
350 case True{}:
351 Tue{}
352 case False{}:
353 Date.weekday.n2(n, U32.is_eq(n, 2))
354
355def Date.weekday.n(+n: U32) -> Weekday:
356 Date.weekday.n1(n, U32.is_eq(n, 1))
357
358def Date.weekday.zero(+n: U32, z: Bool) -> Weekday:
359 match z:
360 case True{}:
361 Mon{}
362 case False{}:
363 Date.weekday.n(n)
364
365def Date.weekday(date: Date) -> Weekday:
366 +n = U32.mod(U32.add(Date.to_days(date), 2), 7)
367 Date.weekday.zero(n, U32.is_eq(n, 0))
368
369def Date.add_ov(+z: U32, n: U32, ok: Bool) -> Result<&2, &2, Date.Error, Date>:
370 match ok:
371 case False{}:
372 Fail{OutOfRange{}}
373 case True{}:
374 Date.from_days(U32.add(z, n))
375
376def Date.add_days(+date: Date, +n: U32) -> Result<&2, &2, Date.Error, Date>:
377 +z = Date.to_days(date)
378 Date.add_ov(z, n, U32.is_le(n, U32.sub(U32.not(0), z)))
379
380def Date.sub_ov(+z: U32, n: U32, ok: Bool) -> Result<&2, &2, Date.Error, Date>:
381 match ok:
382 case False{}:
383 Fail{OutOfRange{}}
384 case True{}:
385 Date.from_days(U32.sub(z, n))
386
387def Date.sub_days(+date: Date, +n: U32) -> Result<&2, &2, Date.Error, Date>:
388 +z = Date.to_days(date)
389 Date.sub_ov(z, n, U32.is_ge(z, n))
390
391def Weekday.to_u32(w: Weekday) -> U32:
392 match w:
393 case Mon{}:
394 0
395 case Tue{}:
396 1
397 case Wed{}:
398 2
399 case Thu{}:
400 3
401 case Fri{}:
402 4
403 case Sat{}:
404 5
405 case Sun{}:
406 6
407
408def Weekday.fwd.gap(+cur: U32, +tgt: U32, gt: Bool) -> U32:
409 match gt:
410 case True{}:
411 U32.sub(tgt, cur)
412 case False{}:
413 U32.sub(U32.add(tgt, 7), cur)
414
415def Weekday.fwd.eq(+cur: U32, +tgt: U32, eq: Bool) -> U32:
416 match eq:
417 case True{}:
418 7
419 case False{}:
420 Weekday.fwd.gap(cur, tgt, U32.is_gt(tgt, cur))
421
422def Weekday.fwd(+cur: U32, +tgt: U32) -> U32:
423 Weekday.fwd.eq(cur, tgt, U32.is_eq(tgt, cur))
424
425def Date.next_weekday(
426 +d: Date, w: Weekday
427) -> Result<&2, &2, Date.Error, Date>:
428 Date.add_days(
429 d, Weekday.fwd(Weekday.to_u32(Date.weekday(d)), Weekday.to_u32(w))
430 )
431
432def Date.previous_weekday(
433 +d: Date, w: Weekday
434) -> Result<&2, &2, Date.Error, Date>:
435 Date.sub_days(
436 d, Weekday.fwd(Weekday.to_u32(w), Weekday.to_u32(Date.weekday(d)))
437 )
438
439def Date.next_or_same.go(
440 +d: Date, w: Weekday, eq: Bool
441) -> Result<&2, &2, Date.Error, Date>:
442 match eq:
443 case True{}:
444 Done{d}
445 case False{}:
446 Date.next_weekday(d, w)
447
448def Date.next_or_same_weekday(
449 +d: Date, +w: Weekday
450) -> Result<&2, &2, Date.Error, Date>:
451 Date.next_or_same.go(
452 d, w, U32.is_eq(Weekday.to_u32(Date.weekday(d)), Weekday.to_u32(w))
453 )
454
455def Date.previous_or_same.go(
456 +d: Date, w: Weekday, eq: Bool
457) -> Result<&2, &2, Date.Error, Date>:
458 match eq:
459 case True{}:
460 Done{d}
461 case False{}:
462 Date.previous_weekday(d, w)
463
464def Date.previous_or_same_weekday(
465 +d: Date, +w: Weekday
466) -> Result<&2, &2, Date.Error, Date>:
467 Date.previous_or_same.go(
468 d, w, U32.is_eq(Weekday.to_u32(Date.weekday(d)), Weekday.to_u32(w))
469 )
470
471def Date.until_days.go(
472 +zs: U32, +ze: U32, lt: Bool
473) -> Result<&2, &2, Date.Error, U32>:
474 match lt:
475 case True{}:
476 Fail{OutOfRange{}}
477 case False{}:
478 Done{U32.sub(ze, zs)}
479
480def Date.until_days(
481 start: Date, end: Date
482) -> Result<&2, &2, Date.Error, U32>:
483 +zs = Date.to_days(start)
484 +ze = Date.to_days(end)
485 Date.until_days.go(zs, ze, U32.is_lt(ze, zs))
486