src/time.bend

bend-kube-runtime@0.2.0.0 · 163 lines · 32 definitions

1import Base
2
3# Time
4# ====
5#
6# Unix time to RFC 3339 in UTC, as Kubernetes writes MicroTime
7# ("2026-10-29T14:30:00.123456Z") and Time ("2026-10-29T14:30:00Z").
8# Dates use Howard Hinnant's civil_from_days. A Wall counts days and the
9# second within the day separately, so it is valid for millions of years;
10# the plain-seconds forms (Time.rfc3339) end in 2106.
11
12type Civil is Data:
13  Civil{year: U32, month: U32, day: U32}
14
15def Time.civil.month.go(+mp: U32, low: Bool) -> U32:
16  match low:
17    case True{}:
18      (mp + 3 : U32)
19    case False{}:
20      (mp - 9 : U32)
21
22def Time.civil.month(+mp: U32) -> U32:
23  Time.civil.month.go(mp, U32.is_lt(mp, 10))
24
25def Time.civil.year.go(+y: U32, early: Bool) -> U32:
26  match early:
27    case True{}:
28      (y + 1 : U32)
29    case False{}:
30      y
31
32def Time.civil.year(+y: U32, +m: U32) -> U32:
33  Time.civil.year.go(y, U32.is_le(m, 2))
34
35def Time.civil.fin(+y: U32, +doy: U32, +mp: U32) -> Civil:
36  Civil{Time.civil.year(y, Time.civil.month(mp)), Time.civil.month(mp),
37    (doy - (153 * mp + 2) / 5 + 1 : U32)}
38
39def Time.civil.doy(+y: U32, +doy: U32) -> Civil:
40  Time.civil.fin(y, doy, ((5 * doy + 2) / 153 : U32))
41
42def Time.civil.yoe(+era: U32, +doe: U32, +yoe: U32) -> Civil:
43  Time.civil.doy((yoe + era * 400 : U32), (doe - (365 * yoe + yoe / 4 - yoe / 100) : U32))
44
45def Time.civil.doe(+era: U32, +doe: U32) -> Civil:
46  Time.civil.yoe(era, doe, ((doe - doe / 1460 + doe / 36524 - doe / 146096) / 365 : U32))
47
48def Time.civil.era(+z: U32) -> Civil:
49  Time.civil.doe((z / 146097 : U32), (z - (z / 146097) * 146097 : U32))
50
51# The date of a count of days since 1970-01-01.
52def Time.civil(+days: U32) -> Civil:
53  Time.civil.era((days + 719468 : U32))
54
55def Time.pad.go(+s: String, width: Nat) -> String:
56  String.repeat("0", Nat.sub(width, String.length(s))) ++ s
57
58# n in at least width digits, zero-padded.
59def Time.pad(+n: U32, width: Nat) -> String:
60  Time.pad.go(U32.show(n), width)
61
62def Time.date(c: Civil) -> String:
63  match c:
64    case Civil{y, m, d}:
65      Time.pad(y, 4n) ++ "-" ++ Time.pad(m, 2n) ++ "-" ++ Time.pad(d, 2n)
66
67def Time.clock(+secs: U32) -> String:
68  Time.pad((secs / 3600 : U32), 2n) ++ ":" ++ Time.pad(((secs / 60) % 60 : U32), 2n) ++ ":"
69    ++ Time.pad((secs % 60 : U32), 2n)
70
71# "YYYY-MM-DDTHH:MM:SS"
72def Time.stamp(+secs: U32) -> String:
73  Time.date(Time.civil((secs / 86400 : U32))) ++ "T" ++ Time.clock((secs % 86400 : U32))
74
75# metav1.Time: second precision.
76def Time.rfc3339(+secs: U32) -> String:
77  Time.stamp(secs) ++ "Z"
78
79# metav1.MicroTime: microsecond precision.
80def Time.rfc3339_micro(+secs: U32, +usecs: U32) -> String:
81  Time.stamp(secs) ++ "." ++ Time.pad(usecs, 6n) ++ "Z"
82
83# A wall-clock reading (sys.bend's Sys.wall).
84type Wall is Data:
85  Wall{days: U32, secs: U32, usecs: U32}
86
87def Wall.of(w: U32 & (U32 & U32)) -> Wall:
88  match w:
89    case (d, (s, us)):
90      Wall{d, s, us}
91
92# "YYYY-MM-DDTHH:MM:SS.ffffffZ" (metav1.MicroTime).
93def Wall.micro(w: Wall) -> String:
94  match w:
95    case Wall{d, +s, +us}:
96      Time.date(Time.civil(d)) ++ "T" ++ Time.clock(s) ++ "." ++ Time.pad(us, 6n) ++ "Z"
97
98# "YYYY-MM-DDTHH:MM:SSZ" (metav1.Time).
99def Wall.rfc3339(w: Wall) -> String:
100  match w:
101    case Wall{d, +s, us}:
102      Time.date(Time.civil(d)) ++ "T" ++ Time.clock(s) ++ "Z"
103
104# Milliseconds, modulo 2^32: only for differences under 49 days, which
105# wrap correctly in U32 subtraction.
106def Wall.ms(w: Wall) -> U32:
107  match w:
108    case Wall{+d, +s, +us}:
109      ((d * 86400 + s) * 1000 + us / 1000 : U32)
110
111# A decimal stamp unique to the microsecond, for names.
112def Wall.id(w: Wall) -> String:
113  match w:
114    case Wall{d, +s, +us}:
115      U32.show(d) ++ Time.pad(s, 5n) ++ Time.pad(us, 6n)
116
117# Parsing
118# -------
119
120# Days since 1970-01-01 of a civil date (Howard Hinnant's days_from_civil),
121# for years from 1970.
122def Time.days.go(+y: U32, +m: U32, +d: U32, +mp: U32) -> U32:
123  ((y / 400) * 146097 + (y % 400) * 365 + (y % 400) / 4 - (y % 400) / 100 +
124    (153 * mp + 2) / 5 + d - 1 - 719468 : U32)
125
126def Time.days.early(+y: U32, +m: U32, +d: U32, early: Bool) -> U32:
127  match early:
128    case True{}:
129      Time.days.go((y - 1 : U32), m, d, (m + 9 : U32))
130    case False{}:
131      Time.days.go(y, m, d, (m - 3 : U32))
132
133def Time.days(+y: U32, +m: U32, +d: U32) -> U32:
134  Time.days.early(y, m, d, U32.is_le(m, 2))
135
136def Time.sub(s: String, i: Nat, n: Nat) -> String:
137  String.take(String.drop(s, i), n)
138
139def Time.parse.go(y: Maybe<&2, U32>, mo: Maybe<&2, U32>, d: Maybe<&2, U32>, h: Maybe<&2, U32>,
140  mi: Maybe<&2, U32>, se: Maybe<&2, U32>, ok: Bool) -> Maybe<&2, U32>:
141  match y mo d h mi se ok:
142    case Some{+y1} Some{+mo1} Some{+d1} Some{h1} Some{mi1} Some{se1} True{}:
143      Some{(Time.days(y1, mo1, d1) * 86400 + h1 * 3600 + mi1 * 60 + se1 : U32)}
144    case _ _ _ _ _ _ _:
145      None{}
146
147def Time.parse.seps(+s: String) -> Bool:
148  Bool.and(Bool.and(String.eq(Time.sub(s, 4n, 1n), "-"), String.eq(Time.sub(s, 7n, 1n), "-")),
149    Bool.and(Bool.and(String.eq(Time.sub(s, 10n, 1n), "T"), String.eq(Time.sub(s, 13n, 1n), ":")),
150      Bool.and(String.eq(Time.sub(s, 16n, 1n), ":"), String.ends_with(s, "Z"))))
151
152# Seconds since the epoch of "YYYY-MM-DDTHH:MM:SS[.fff]Z" (metav1.Time and
153# MicroTime; the fraction is dropped), or None.
154def Time.parse(+s: String) -> Maybe<&2, U32>:
155  Time.parse.go(U32.read(Time.sub(s, 0n, 4n)), U32.read(Time.sub(s, 5n, 2n)),
156    U32.read(Time.sub(s, 8n, 2n)), U32.read(Time.sub(s, 11n, 2n)), U32.read(Time.sub(s, 14n, 2n)),
157    U32.read(Time.sub(s, 17n, 2n)), Time.parse.seps(s))
158
159# Seconds since the epoch of a wall-clock reading.
160def Wall.secs(w: Wall) -> U32:
161  match w:
162    case Wall{d, s, us}:
163      (d * 86400 + s : U32)