1	# ezsys/src/clock: Unix time as ISO 8601 UTC, `YYYY-MM-DDTHH:MM:SS.mmmZ`.
2	# Pure: the wall clock itself is the effect in src/sys.bend. The input is
3	# whole seconds since 1970-01-01T00:00:00Z as a U32, which reaches
4	# 2106-02-07T06:28:15Z, and the milliseconds past that second.
5	#
6	# The date is Howard Hinnant's civil_from_days
7	# (https://howardhinnant.github.io/date_algorithms.html#civil_from_days), the
8	# proleptic Gregorian calendar in 400-year eras of 146097 days, its years
9	# starting on 1 March so that the leap day is the last day of a year. Every
10	# intermediate value is unsigned and fits in a U32 for every U32 input.
11	import Base
12	
13	# a calendar date
14	type Ymd is Data:
15	  Ymd{year: U32, month: U32, day: U32}
16	
17	# the k-th decimal digit character (9 for anything past it)
18	def time.digit.at(place: Nat) -> Char:
19	  match place:
20	    case 0n:
21	      '0'
22	    case 1n+k1:
23	      match k1:
24	        case 0n:
25	          '1'
26	        case 1n+k2:
27	          match k2:
28	            case 0n:
29	              '2'
30	            case 1n+k3:
31	              match k3:
32	                case 0n:
33	                  '3'
34	                case 1n+k4:
35	                  match k4:
36	                    case 0n:
37	                      '4'
38	                    case 1n+k5:
39	                      match k5:
40	                        case 0n:
41	                          '5'
42	                        case 1n+k6:
43	                          match k6:
44	                            case 0n:
45	                              '6'
46	                            case 1n+k7:
47	                              match k7:
48	                                case 0n:
49	                                  '7'
50	                                case 1n+k8:
51	                                  match k8:
52	                                    case 0n:
53	                                      '8'
54	                                    case 1n+_k9:
55	                                      '9'
56	
57	# the decimal digit of n's last place
58	def time.digit(num: U32) -> Char:
59	  time.digit.at(U32.to_nat((num % 10 : U32)))
60	
61	# the month of a March-based month index (0 is March)
62	def time.civil.month(+mp: U32) -> U32:
63	  Bool.pick(U32, (mp < 10 : U32), (mp + 3 : U32), (mp - 9 : U32))
64	
65	# the calendar year of a March-based year: January and February are the
66	# next calendar year's
67	def time.civil.year(+year: U32, +month: U32) -> U32:
68	  Bool.pick(U32, (month <= 2 : U32), (year + 1 : U32), year)
69	
70	# the year, month and day of a day number (days since 1970-01-01)
71	def time.civil(days: U32) -> Ymd:
72	  +z = (days + 719468 : U32)
73	  +era = (z / 146097 : U32)
74	  +doe = (z - era * 146097 : U32)
75	  +yoe = ((doe - doe / 1460 + doe / 36524 - doe / 146096) / 365 : U32)
76	  +doy = (doe - (365 * yoe + yoe / 4 - yoe / 100) : U32)
77	  +mp = ((5 * doy + 2) / 153 : U32)
78	  +m = time.civil.month(mp)
79	  Ymd{time.civil.year((yoe + era * 400 : U32), m), m,
80	    (doy - (153 * mp + 2) / 5 + 1 : U32)}
81	
82	# two decimal places: tens and units
83	def time.two(+num: U32) -> String:
84	  SCon{time.digit((num / 10 : U32)), SCon{time.digit(num), SNil{}}}
85	
86	# three decimal places: hundreds, tens and units
87	def time.three(+num: U32) -> String:
88	  SCon{time.digit((num / 100 : U32)), SCon{time.digit((num / 10 : U32)),
89	    SCon{time.digit(num), SNil{}}}}
90	
91	# four decimal places: thousands, hundreds, tens and units
92	def time.four(+num: U32) -> String:
93	  SCon{time.digit((num / 1000 : U32)), SCon{time.digit((num / 100 : U32)),
94	    SCon{time.digit((num / 10 : U32)), SCon{time.digit(num), SNil{}}}}}
95	
96	# YYYY-MM-DD
97	def time.ymd(year: U32, month: U32, day: U32) -> String:
98	  time.four(year) ++ SCon{'-', time.two(month) ++ SCon{'-', time.two(day)}}
99	
100	# the date of a calendar date
101	def time.ymd.of(date: Ymd) -> String:
102	  match date:
103	    case Ymd{year, month, day}:
104	      time.ymd(year, month, day)
105	
106	# YYYY-MM-DD of a day number
107	def time.date(days: U32) -> String:
108	  time.ymd.of(time.civil(days))
109	
110	# HH:MM:SS.mmmZ of a second of the day and a millisecond (its last three
111	# decimal places)
112	def time.clock(+sod: U32, ms: U32) -> String:
113	  time.two((sod / 3600 : U32)) ++ SCon{':', time.two((sod % 3600 / 60 : U32))
114	    ++ SCon{':', time.two((sod % 60 : U32)) ++ SCon{'.',
115	    time.three(ms) ++ SCon{'Z', SNil{}}}}}
116	
117	# ISO 8601 UTC of seconds since the epoch and a millisecond
118	def time.iso(+secs: U32, ms: U32) -> String:
119	  time.date((secs / 86400 : U32)) ++ SCon{'T',
120	    time.clock((secs % 86400 : U32), ms)}
121	
122	# ISO 8601 UTC of a clock reading: seconds and milliseconds
123	def time.iso.of(now: U32 & U32) -> String:
124	  (secs, ms) = now
125	  time.iso(secs, ms)
126	
127	# --- weekdays and ISO 8601 weeks ---
128	
129	# the days of the week
130	type Wd is Data:
131	  Mon{}
132	  Tue{}
133	  Wed{}
134	  Thu{}
135	  Fri{}
136	  Sat{}
137	  Sun{}
138	
139	# the next day of the week: Sunday is followed by Monday
140	def time.wd.next(day: Wd) -> Wd:
141	  match day:
142	    case Mon{}:
143	      Tue{}
144	    case Tue{}:
145	      Wed{}
146	    case Wed{}:
147	      Thu{}
148	    case Thu{}:
149	      Fri{}
150	    case Fri{}:
151	      Sat{}
152	    case Sat{}:
153	      Sun{}
154	    case Sun{}:
155	      Mon{}
156	
157	# the ISO 8601 weekday number of a day of the week: 1 Monday to 7 Sunday
158	def time.wd.num(day: Wd) -> U32:
159	  match day:
160	    case Mon{}:
161	      1
162	    case Tue{}:
163	      2
164	    case Wed{}:
165	      3
166	    case Thu{}:
167	      4
168	    case Fri{}:
169	      5
170	    case Sat{}:
171	      6
172	    case Sun{}:
173	      7
174	
175	# the day of the week `left` days after `day`, one day at a time
176	def time.wd.go(left: Nat, day: Wd) -> Wd:
177	  match left:
178	    case 0n:
179	      day
180	    case 1n+more:
181	      time.wd.go(more, time.wd.next(day))
182	
183	# the ISO weekday of day `num` after 1970-01-01, a Thursday, counted one
184	# day at a time: the weekday's definition, which time.weekday computes
185	# faster
186	def time.weekday.nat(num: Nat) -> U32:
187	  time.wd.num(time.wd.go(num, Thu{}))
188	
189	# two weekdays added as offsets from Monday (Monday is 0, Sunday 6), so
190	# `time.wd.plus(day, off)` is the weekday `off` days after `day`
191	def time.wd.plus(day: Wd, off: Wd) -> Wd:
192	  match day off:
193	    case Mon{} Mon{}:
194	      Mon{}
195	    case Mon{} Tue{}:
196	      Tue{}
197	    case Mon{} Wed{}:
198	      Wed{}
199	    case Mon{} Thu{}:
200	      Thu{}
201	    case Mon{} Fri{}:
202	      Fri{}
203	    case Mon{} Sat{}:
204	      Sat{}
205	    case Mon{} Sun{}:
206	      Sun{}
207	    case Tue{} Mon{}:
208	      Tue{}
209	    case Tue{} Tue{}:
210	      Wed{}
211	    case Tue{} Wed{}:
212	      Thu{}
213	    case Tue{} Thu{}:
214	      Fri{}
215	    case Tue{} Fri{}:
216	      Sat{}
217	    case Tue{} Sat{}:
218	      Sun{}
219	    case Tue{} Sun{}:
220	      Mon{}
221	    case Wed{} Mon{}:
222	      Wed{}
223	    case Wed{} Tue{}:
224	      Thu{}
225	    case Wed{} Wed{}:
226	      Fri{}
227	    case Wed{} Thu{}:
228	      Sat{}
229	    case Wed{} Fri{}:
230	      Sun{}
231	    case Wed{} Sat{}:
232	      Mon{}
233	    case Wed{} Sun{}:
234	      Tue{}
235	    case Thu{} Mon{}:
236	      Thu{}
237	    case Thu{} Tue{}:
238	      Fri{}
239	    case Thu{} Wed{}:
240	      Sat{}
241	    case Thu{} Thu{}:
242	      Sun{}
243	    case Thu{} Fri{}:
244	      Mon{}
245	    case Thu{} Sat{}:
246	      Tue{}
247	    case Thu{} Sun{}:
248	      Wed{}
249	    case Fri{} Mon{}:
250	      Fri{}
251	    case Fri{} Tue{}:
252	      Sat{}
253	    case Fri{} Wed{}:
254	      Sun{}
255	    case Fri{} Thu{}:
256	      Mon{}
257	    case Fri{} Fri{}:
258	      Tue{}
259	    case Fri{} Sat{}:
260	      Wed{}
261	    case Fri{} Sun{}:
262	      Thu{}
263	    case Sat{} Mon{}:
264	      Sat{}
265	    case Sat{} Tue{}:
266	      Sun{}
267	    case Sat{} Wed{}:
268	      Mon{}
269	    case Sat{} Thu{}:
270	      Tue{}
271	    case Sat{} Fri{}:
272	      Wed{}
273	    case Sat{} Sat{}:
274	      Thu{}
275	    case Sat{} Sun{}:
276	      Fri{}
277	    case Sun{} Mon{}:
278	      Sun{}
279	    case Sun{} Tue{}:
280	      Mon{}
281	    case Sun{} Wed{}:
282	      Tue{}
283	    case Sun{} Thu{}:
284	      Wed{}
285	    case Sun{} Fri{}:
286	      Thu{}
287	    case Sun{} Sat{}:
288	      Fri{}
289	    case Sun{} Sun{}:
290	      Sat{}
291	
292	# the day of the week a word's value in days after a Monday, one bit at a
293	# time from the lowest: the value is the bit plus twice the rest's
294	def time.wd.bits(len: Nat, word: Word(len)) -> Wd:
295	  match len:
296	    case 0n:
297	      Mon{}
298	    case 1n+more:
299	      match word:
300	        case WCon{False{}, rest}:
301	          +off = time.wd.bits(more, rest)
302	          time.wd.plus(off, off)
303	        case WCon{True{}, rest}:
304	          +off = time.wd.bits(more, rest)
305	          time.wd.next(time.wd.plus(off, off))
306	
307	# the ISO weekday of a day number, in 32 steps, one a bit
308	def time.weekday(days: U32) -> U32:
309	  match days:
310	    case U32{word}:
311	      time.wd.num(time.wd.plus(Thu{}, time.wd.bits(32n, word)))
312	
313	# the day number of 1 January of a year from 1970 on: Howard Hinnant's
314	# days_from_civil for month 1, day 1
315	def time.jan1(year: U32) -> U32:
316	  +yr = (year - 1 : U32)
317	  +era = (yr / 400 : U32)
318	  +yoe = (yr - era * 400 : U32)
319	  (era * 146097 + yoe * 365 + yoe / 4 - yoe / 100 + 306 - 719468 : U32)
320	
321	# the Thursday of a day's ISO week (Monday to Sunday)
322	def time.thursday(+days: U32) -> U32:
323	  (days + 4 - time.weekday(days) : U32)
324	
325	# the ISO year and week of a week's Thursday: the Thursday's calendar year,
326	# and how many Thursdays of that year it is
327	def time.week.of(+thu: U32, date: Ymd) -> U32 & U32:
328	  match date:
329	    case Ymd{+year, _month, _day}:
330	      (year, ((thu - time.jan1(year)) / 7 + 1 : U32))
331	
332	# the ISO 8601 week-numbering year and week of a day number
333	def time.week(+days: U32) -> U32 & U32:
334	  +thu = time.thursday(days)
335	  time.week.of(thu, time.civil(thu))
336	
337	# the ISO 8601 week-numbering year and week of seconds since the epoch
338	def time.iso_week(+secs: U32) -> U32 & U32:
339	  time.week((secs / 86400 : U32))
340	
341	# YYYY-Www of an ISO year and week, as `date +%G-W%V` writes it
342	def time.week.text(week: U32 & U32) -> String:
343	  (year, num) = week
344	  time.four(year) ++ SCon{'-', SCon{'W', time.two(num)}}
345	
346	# YYYY-Www of seconds since the epoch
347	def time.iso_week_text(+secs: U32) -> String:
348	  time.week.text(time.iso_week(secs))
349	
350	# a date, a second of the day and a weekday as the civil fields
351	def time.fields.of(
352	  date: Ymd,
353	  +sod: U32,
354	  wd: U32
355	) -> U32 & U32 & U32 & U32 & U32 & U32 & U32:
356	  match date:
357	    case Ymd{year, month, day}:
358	      (year, month, day, (sod / 3600 : U32), (sod % 3600 / 60 : U32),
359	        (sod % 60 : U32), wd)
360	
361	# year, month, day, hour, minute, second and ISO weekday of seconds since
362	# the epoch, in UTC
363	def time.fields(+secs: U32) -> U32 & U32 & U32 & U32 & U32 & U32 & U32:
364	  time.fields.of(time.civil((secs / 86400 : U32)), (secs % 86400 : U32),
365	    time.weekday((secs / 86400 : U32)))