clock.bend

cswap-bend-cli@0.1.0.0 · 243 lines · 43 definitions

1import Base
2
3# Wall-clock time as unix seconds, and ISO 8601 text both ways. `U32` holds
4# unix seconds until 2106. Dates before 1970 are not representable: they
5# parse to None.
6
7# Unix seconds now. The foreign effect calls time(2); Base's IO.now is a
8# monotonic tick, not wall time.
9def Clock.now_s() -> IO(U32):
10  import "./effs/now_s.c"
11  import "./effs/now_s.js"
12
13def now_s() -> IO(U32):
14  Clock.now_s()
15
16def sel(c: Bool, x: U32, y: U32) -> U32:
17  match c:
18    case True{}:
19      x
20    case False{}:
21      y
22
23def sel.s(c: Bool, x: String, y: String) -> String:
24  match c:
25    case True{}:
26      x
27    case False{}:
28      y
29
30# ---- seconds to text -------------------------------------------------------
31
32def pad2(+n: U32) -> String:
33  sel.s(U32.is_lt(n, 10), "0" ++ U32.show(n), U32.show(n))
34
35def pad4(+n: U32) -> String:
36  sel.s(U32.is_lt(n, 10), "000", sel.s(U32.is_lt(n, 100), "00", sel.s(U32.is_lt(n, 1000), "0", ""))) ++ U32.show(n)
37
38# Civil date (year, (month, day)) of a day count since 1970-01-01
39# (Hinnant's civil_from_days, all unsigned: z + 719468 is positive).
40def civil.adj(+y: U32, +m: U32, d: U32) -> U32 & (U32 & U32):
41  (sel(U32.is_le(m, 2), (y + 1 : U32), y), (m, d))
42
43def civil.ymd(+y: U32, +mp: U32, +doy: U32) -> U32 & (U32 & U32):
44  civil.adj(y, sel(U32.is_lt(mp, 10), (mp + 3 : U32), (mp - 9 : U32)), (doy - ((153 * mp + 2) / 5) + 1 : U32))
45
46def civil.fin(+yoe: U32, +era: U32, +doy: U32) -> U32 & (U32 & U32):
47  civil.ymd((yoe + era * 400 : U32), ((5 * doy + 2) / 153 : U32), doy)
48
49def civil.doy(+era: U32, +doe: U32, +yoe: U32) -> U32 & (U32 & U32):
50  civil.fin(yoe, era, (doe - (365 * yoe + yoe / 4 - yoe / 100) : U32))
51
52def civil.yoe(+era: U32, +doe: U32) -> U32 & (U32 & U32):
53  civil.doy(era, doe, ((doe - doe / 1460 + doe / 36524 - doe / 146096) / 365 : U32))
54
55def civil.doe(+z: U32) -> U32 & (U32 & U32):
56  civil.yoe((z / 146097 : U32), (z % 146097 : U32))
57
58def civil(days: U32) -> U32 & (U32 & U32):
59  civil.doe((days + 719468 : U32))
60
61def iso.fmt(ymd: U32 & (U32 & U32), +s: U32, suffix: String) -> String:
62  (y, (m, d)) = ymd
63  pad4(y) ++ "-" ++ pad2(m) ++ "-" ++ pad2(d) ++ "T"
64    ++ pad2((s / 3600 : U32)) ++ ":" ++ pad2(((s / 60) % 60 : U32)) ++ ":" ++ pad2((s % 60 : U32)) ++ suffix
65
66# `2026-10-30T09:00:00Z`, as the reference's strftime writes it.
67def iso8601_utc(+t: U32) -> String:
68  iso.fmt(civil((t / 86400 : U32)), (t % 86400 : U32), "Z")
69
70# `2026-10-30T09:00:00+00:00`, as the reference's isoformat writes it.
71def iso8601_offset(+t: U32) -> String:
72  iso.fmt(civil((t / 86400 : U32)), (t % 86400 : U32), "+00:00")
73
74# ---- text to seconds -------------------------------------------------------
75
76def all_digits(s: String) -> Bool:
77  match s:
78    case SNil{}:
79      True{}
80    case SCon{c, t}:
81      Char.is_digit(c) && all_digits(t)
82
83def num.pick(ok: Bool, s: String) -> Maybe<&2, U32>:
84  match ok:
85    case True{}:
86      U32.read(s)
87    case False{}:
88      None{}
89
90# The n digits of `s` at offset `off`, as a number.
91def num(+s: String, off: Nat, +n: Nat) -> Maybe<&2, U32>:
92  +slice = String.take(String.drop(s, off), n)
93  num.pick(all_digits(slice) && Nat.is_eq(String.length(slice), n), slice)
94
95def at.pick(m: Maybe<&2, Char>, a: Char, b: Char) -> Bool:
96  match m:
97    case None{}:
98      False{}
99    case Some{+c}:
100      Char.is_eq(c, a) || Char.is_eq(c, b)
101
102# True when the char at `i` is `a` or `b`.
103def at(+s: String, i: Nat, a: Char, b: Char) -> Bool:
104  at.pick(String.get(s, i), a, b)
105
106def valid(+y: U32, +mo: U32, +d: U32, +h: U32, +mi: U32, +s: U32) -> Bool:
107  U32.is_ge(y, 1970) && U32.is_ge(mo, 1) && U32.is_le(mo, 12) && U32.is_ge(d, 1) && U32.is_le(d, 31)
108    && U32.is_lt(h, 24) && U32.is_lt(mi, 60) && U32.is_lt(s, 60)
109
110def days.era(+era: U32, +yoe: U32, +doy: U32) -> U32:
111  (era * 146097 + (yoe * 365 + yoe / 4 - yoe / 100 + doy) - 719468 : U32)
112
113def days.fin(+y: U32, +mp: U32, +d: U32) -> U32:
114  days.era((y / 400 : U32), (y % 400 : U32), (((153 * mp + 2) / 5) + d - 1 : U32))
115
116# Days since 1970-01-01 of a civil date (days_from_civil; y >= 1970).
117def days(+y: U32, +m: U32, +d: U32) -> U32:
118  days.fin(sel(U32.is_le(m, 2), (y - 1 : U32), y), sel(U32.is_gt(m, 2), (m - 3 : U32), (m + 9 : U32)), d)
119
120def digits_end.pick(d: Bool, c: Char, t: String, dropped: String) -> String:
121  match d:
122    case True{}:
123      dropped
124    case False{}:
125      SCon{c, t}
126
127# Drop a leading run of digits.
128def digits_end(s: String) -> String:
129  match s:
130    case SNil{}:
131      SNil{}
132    case SCon{+c, +t}:
133      digits_end.pick(Char.is_digit(c), c, t, digits_end(t))
134
135def frac.pick(dot: Bool, c: Char, t: String) -> String:
136  match dot:
137    case True{}:
138      digits_end(t)
139    case False{}:
140      SCon{c, t}
141
142def frac(s: String) -> String:
143  match s:
144    case SNil{}:
145      SNil{}
146    case SCon{+c, t}:
147      frac.pick(Char.is_eq(c, '.') || Char.is_eq(c, ','), c, t)
148
149def tz.min.sel(a: Bool, b: Bool, c: Bool, +t: String) -> Maybe<&2, U32>:
150  match a b c:
151    case True{} _ _:
152      Some{0}
153    case False{} True{} _:
154      num(t, 3n, 2n)
155    case False{} False{} True{}:
156      num(t, 2n, 2n)
157    case False{} False{} False{}:
158      None{}
159
160def tz.min.pick(+n: Nat, +t: String) -> Maybe<&2, U32>:
161  tz.min.sel(Nat.is_eq(n, 2n), Nat.is_eq(n, 5n), Nat.is_eq(n, 4n), t)
162
163def tz.min(+t: String) -> Maybe<&2, U32>:
164  tz.min.pick(String.length(t), t)
165
166def tz.off.pick(ok: Bool, neg: Bool, +mag: U32) -> Maybe<&2, U32>:
167  match ok:
168    case False{}:
169      None{}
170    case True{}:
171      Some{sel(neg, (86400 - mag : U32), (86400 + mag : U32))}
172
173# The zone offset in seconds, biased by 86400 so it stays unsigned: `Z`,
174# `+HH:MM`, `-HH`, `+HHMM`, or none (read as UTC, as the reference's naive
175# stamps are).
176def tz.off(neg: Bool, +h: U32, +m: U32) -> Maybe<&2, U32>:
177  tz.off.pick(U32.is_lt(h, 24) && U32.is_lt(m, 60), neg, (h * 3600 + m * 60 : U32))
178
179def tz.hm(neg: Bool, +t: String) -> Maybe<&2, U32>:
180  do Maybe<&2, U32>:
181    h : U32 <- num(t, 0n, 2n)
182    m : U32 <- tz.min(t)
183    tz.off(neg, h, m)
184
185def tz.z(t: String) -> Maybe<&2, U32>:
186  match t:
187    case SNil{}:
188      Some{86400}
189    case SCon{c, u}:
190      None{}
191
192def tz.head(z: Bool, plus: Bool, minus: Bool, t: String) -> Maybe<&2, U32>:
193  match z plus minus:
194    case True{} _ _:
195      tz.z(t)
196    case False{} True{} _:
197      tz.hm(False{}, t)
198    case False{} False{} True{}:
199      tz.hm(True{}, t)
200    case False{} False{} False{}:
201      None{}
202
203def tz(s: String) -> Maybe<&2, U32>:
204  match s:
205    case SNil{}:
206      Some{86400}
207    case SCon{+c, t}:
208      tz.head(Char.is_eq(c, 'Z') || Char.is_eq(c, 'z'), Char.is_eq(c, '+'), Char.is_eq(c, '-'), t)
209
210# local = utc + offset, so utc = local - offset (offset = biased - 86400).
211def shift(+local: U32, biased: U32) -> U32:
212  (local + 86400 - biased : U32)
213
214def finish(ok: Bool, +local: U32, off: Maybe<&2, U32>) -> Maybe<&2, U32>:
215  match ok off:
216    case False{} _:
217      None{}
218    case True{} None{}:
219      None{}
220    case True{} Some{o}:
221      Some{shift(local, o)}
222
223def parse.fin(+s: String, +y: U32, +mo: U32, +d: U32, +h: U32, +mi: U32, +sec: U32) -> Maybe<&2, U32>:
224  finish(valid(y, mo, d, h, mi, sec) && at(s, 4n, '-', '-') && at(s, 7n, '-', '-')
225    && at(s, 10n, 'T', ' ') && at(s, 13n, ':', ':') && at(s, 16n, ':', ':'),
226    (days(y, mo, d) * 86400 + h * 3600 + mi * 60 + sec : U32), tz(frac(String.drop(s, 19n))))
227
228def parse.time(+s: String, y: U32, mo: U32, d: U32) -> Maybe<&2, U32>:
229  do Maybe<&2, U32>:
230    h : U32 <- num(s, 11n, 2n)
231    mi : U32 <- num(s, 14n, 2n)
232    sec : U32 <- num(s, 17n, 2n)
233    parse.fin(s, y, mo, d, h, mi, sec)
234
235# Unix seconds of `2026-10-30T09:00:00+00:00`, `...Z`, `...00.123456Z`, a
236# `-HH:MM` offset, or a bare stamp (read as UTC); None when malformed.
237def parse_iso8601(+s: String) -> Maybe<&2, U32>:
238  do Maybe<&2, U32>:
239    y : U32 <- num(s, 0n, 4n)
240    mo : U32 <- num(s, 5n, 2n)
241    d : U32 <- num(s, 8n, 2n)
242    parse.time(s, y, mo, d)
243