src/clock.bend

ezsys@0.1.0.0 · 365 lines · 32 definitions

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.
11import Base
12
13# a calendar date
14type Ymd is Data:
15  Ymd{year: U32, month: U32, day: U32}
16
17# the k-th decimal digit character (9 for anything past it)
18def 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
58def 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)
62def 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
67def 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)
71def 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
83def 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
87def 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
92def 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
97def 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
101def 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
107def 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)
112def 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
118def 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
123def 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
130type 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
140def 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
158def 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
176def 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
186def 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`
191def 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
294def 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
308def 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
315def 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)
322def 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
327def 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
333def 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
338def 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
342def 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
347def 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
351def 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
363def 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)))