1	import 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	
12	type Civil is Data:
13	  Civil{year: U32, month: U32, day: U32}
14	
15	def 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	
22	def Time.civil.month(+mp: U32) -> U32:
23	  Time.civil.month.go(mp, U32.is_lt(mp, 10))
24	
25	def 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	
32	def Time.civil.year(+y: U32, +m: U32) -> U32:
33	  Time.civil.year.go(y, U32.is_le(m, 2))
34	
35	def 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	
39	def Time.civil.doy(+y: U32, +doy: U32) -> Civil:
40	  Time.civil.fin(y, doy, ((5 * doy + 2) / 153 : U32))
41	
42	def 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	
45	def Time.civil.doe(+era: U32, +doe: U32) -> Civil:
46	  Time.civil.yoe(era, doe, ((doe - doe / 1460 + doe / 36524 - doe / 146096) / 365 : U32))
47	
48	def 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.
52	def Time.civil(+days: U32) -> Civil:
53	  Time.civil.era((days + 719468 : U32))
54	
55	def 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.
59	def Time.pad(+n: U32, width: Nat) -> String:
60	  Time.pad.go(U32.show(n), width)
61	
62	def 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	
67	def 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"
72	def 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.
76	def Time.rfc3339(+secs: U32) -> String:
77	  Time.stamp(secs) ++ "Z"
78	
79	# metav1.MicroTime: microsecond precision.
80	def 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).
84	type Wall is Data:
85	  Wall{days: U32, secs: U32, usecs: U32}
86	
87	def 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).
93	def 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).
99	def 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.
106	def 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.
112	def 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)