1	import Base
2	
3	type Date.Error is Data:
4	  InvalidDate{year: U32, month: U32, day: U32}
5	  OutOfRange{}
6	
7	type Date is Data:
8	  Date{year: U32, month: U32, day: U32}
9	
10	def 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	
17	def 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	
24	def Date.leap(+y: U32) -> Bool:
25	  Date.leap.4(y, U32.is_eq(U32.mod(y, 4), 0))
26	
27	def Date.dim.feb(leap: Bool) -> U32:
28	  match leap:
29	    case True{}:
30	      29
31	    case False{}:
32	      28
33	
34	def 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	
52	def 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	
58	def 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	
65	def 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	
72	def Date.dim.rest(+m: U32) -> Maybe<&2, U32>:
73	  Date.dim.rest2(m, Date.is_31(m))
74	
75	def 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	
82	def Date.dim(+m: U32, leap: Bool) -> Maybe<&2, U32>:
83	  Date.dim.m(m, leap, U32.is_eq(m, 2))
84	
85	def 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	
94	def 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	
101	def 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	
110	def 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	
119	def 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	
124	def 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	
131	def 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	
134	def 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	
139	def 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	
148	def 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	
153	def Date.start_of_month(date: Date) -> Date:
154	  match date:
155	    case Date{y, m, _}:
156	      Date{y, m, 1}
157	
158	def Date.start_of_year(date: Date) -> Date:
159	  match date:
160	    case Date{y, _, _}:
161	      Date{y, 1, 1}
162	
163	def Date.end_of_year(date: Date) -> Date:
164	  match date:
165	    case Date{y, _, _}:
166	      Date{y, 12, 31}
167	
168	def 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	
173	def 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	
178	def 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	
183	def 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	
190	def 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	
197	def 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	
200	def 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	
212	def 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	
219	def 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	
222	def Date.to_days(date: Date) -> U32:
223	  match date:
224	    case Date{y, m, d}:
225	      Date.to_days.parts(y, m, d)
226	
227	def 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	
235	def Date.is_lt(a: Date, b: Date) -> Bool:
236	  U32.is_lt(Date.to_days(a), Date.to_days(b))
237	
238	def Date.is_gt(a: Date, b: Date) -> Bool:
239	  Date.is_lt(b, a)
240	
241	def Date.is_le(a: Date, b: Date) -> Bool:
242	  Bool.not(Date.is_lt(b, a))
243	
244	def Date.is_ge(a: Date, b: Date) -> Bool:
245	  Bool.not(Date.is_lt(a, b))
246	
247	def Date.from_days.doe(+z: U32, era: U32) -> U32:
248	  U32.sub(z, U32.mul(era, 146097))
249	
250	def 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	
259	def 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	
268	def Date.from_days.mp(+doy: U32) -> U32:
269	  U32.div(U32.add(U32.mul(5, doy), 2), 153)
270	
271	def 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	
274	def 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	
281	def 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	
288	def 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	
301	def Date.from_days(z: U32) -> Result<&2, &2, Date.Error, Date>:
302	  Date.from_days.parts(z)
303	
304	type Weekday is Data:
305	  Mon{}
306	  Tue{}
307	  Wed{}
308	  Thu{}
309	  Fri{}
310	  Sat{}
311	  Sun{}
312	
313	def Date.weekday.n6(+n: U32, is6: Bool) -> Weekday:
314	  match is6:
315	    case True{}:
316	      Sun{}
317	    case False{}:
318	      Sat{}
319	
320	def 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	
327	def 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	
334	def 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	
341	def 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	
348	def 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	
355	def Date.weekday.n(+n: U32) -> Weekday:
356	  Date.weekday.n1(n, U32.is_eq(n, 1))
357	
358	def 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	
365	def 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	
369	def 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	
376	def 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	
380	def 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	
387	def 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	
391	def 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	
408	def 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	
415	def 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	
422	def Weekday.fwd(+cur: U32, +tgt: U32) -> U32:
423	  Weekday.fwd.eq(cur, tgt, U32.is_eq(tgt, cur))
424	
425	def 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	
432	def 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	
439	def 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	
448	def 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	
455	def 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	
464	def 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	
471	def 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	
480	def 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