1	import Base
2	
3	# Text for the terminal dashboard: styled segments, truncation to a width,
4	# durations, percentages and usage bars. Pure; widths are in characters (a
5	# Bend String is a list of code points), so the box-drawing glyphs count one.
6	
7	# What a segment looks like. `RPlain` carries no escape at all.
8	type Role is Data:
9	  RPlain{}
10	  RBold{}
11	  RAccent{}
12	  RAccentB{}
13	  RMuted{}
14	  ROk{}
15	  RWarn{}
16	  RCrit{}
17	  RTrack{}
18	
19	# A run of text in one style; `dim` fades it (a stale measurement).
20	type Seg is Data:
21	  Seg{text: String, role: Role, dim: Bool}
22	
23	def sg(+t: String, +r: Role) -> Seg:
24	  Seg{t, r, False{}}
25	
26	def sel.s(+c: Bool, +x: String, +y: String) -> String:
27	  match c:
28	    case True{}:
29	      x
30	    case False{}:
31	      y
32	
33	def sel.u(+c: Bool, +x: U32, +y: U32) -> U32:
34	  match c:
35	    case True{}:
36	      x
37	    case False{}:
38	      y
39	
40	def spaces(+n: Nat) -> String:
41	  String.repeat(" ", n)
42	
43	# Pad on the right / left to `w` characters (never truncates).
44	def pad_right(+s: String, +w: Nat) -> String:
45	  s ++ spaces(Nat.sub(w, String.length(s)))
46	
47	def pad_left(+s: String, +w: Nat) -> String:
48	  spaces(Nat.sub(w, String.length(s))) ++ s
49	
50	# ---- numbers --------------------------------------------------------------
51	
52	# Centi-percent (4750 = 47.5 %) to a whole percent, halves to even as Python's
53	# `f"{pct:.0f}"` does.
54	def round_even(+c: U32) -> U32:
55	  sel.u(U32.is_lt((c % 100 : U32), 50), (c / 100 : U32),
56	    sel.u(U32.is_gt((c % 100 : U32), 50), ((c / 100 : U32) + 1 : U32),
57	      sel.u(U32.is_eq((((c / 100 : U32)) % 2 : U32), 0), (c / 100 : U32), ((c / 100 : U32) + 1 : U32))))
58	
59	# " 47%" (width 4), as the reference's `{pct:3.0f}%`.
60	def pct_text(+c: U32) -> String:
61	  pad_left(U32.show(round_even(c)), 3n) ++ "%"
62	
63	def hm(+s: U32) -> String:
64	  sel.s(U32.is_eq(((s % 3600) / 60 : U32), 0), U32.show((s / 3600 : U32)) ++ "h",
65	    U32.show((s / 3600 : U32)) ++ "h " ++ U32.show(((s % 3600) / 60 : U32)) ++ "m")
66	
67	def dh(+s: U32) -> String:
68	  sel.s(U32.is_eq(((s % 86400) / 3600 : U32), 0), U32.show((s / 86400 : U32)) ++ "d",
69	    U32.show((s / 86400 : U32)) ++ "d " ++ U32.show(((s % 86400) / 3600 : U32)) ++ "h")
70	
71	# ---- lines -----------------------------------------------------------------
72	
73	# The shortest honest duration: 45s, 12m, 2h 13m, 2h, 3d 4h, 3d.
74	def duration(+s: U32) -> String:
75	  sel.s(U32.is_lt(s, 60), U32.show(s) ++ "s",
76	    sel.s(U32.is_lt(s, 3600), U32.show((s / 60 : U32)) ++ "m",
77	      sel.s(U32.is_lt(s, 86400), hm(s), dh(s))))
78	
79	def seg_len(+s: Seg) -> Nat:
80	  match s:
81	    case Seg{t, r, d}:
82	      String.length(t)
83	
84	def line_len(+l: List<&2, Seg>) -> Nat:
85	  match l:
86	    case Nil{}:
87	      0n
88	    case Con{s, t}:
89	      Nat.add(seg_len(s), line_len(t))
90	
91	def cut(+s: Seg, +n: Nat) -> Seg:
92	  match s:
93	    case Seg{x, r, d}:
94	      Seg{String.take(x, n), r, d}
95	
96	def take_pick(+over: Bool, +s: Seg, +n: Nat, +rest: List<&2, Seg>) -> List<&2, Seg>:
97	  match over:
98	    case True{}:
99	      Con{cut(s, n), Nil{}}
100	    case False{}:
101	      Con{s, rest}
102	
103	# The first `n` characters of a line.
104	def take_chars(+l: List<&2, Seg>, +n: Nat) -> List<&2, Seg>:
105	  match l:
106	    case Nil{}:
107	      Nil{}
108	    case Con{s, t}:
109	      take_pick(Nat.is_gt(seg_len(s), n), s, n, take_chars(t, Nat.sub(n, seg_len(s))))
110	
111	def ellipsized(+l: List<&2, Seg>, +w: Nat) -> List<&2, Seg>:
112	  List.append(&2, Seg, take_chars(l, Nat.sub(w, 1n)), Con{sg("…", RMuted{}), Nil{}})
113	
114	def fit_if(+over: Bool, +l: List<&2, Seg>, +w: Nat) -> List<&2, Seg>:
115	  match over:
116	    case True{}:
117	      ellipsized(l, w)
118	    case False{}:
119	      l
120	
121	# ---- bars -------------------------------------------------------------------
122	
123	# A line no wider than `w`: longer ones end in an ellipsis.
124	def fit(+l: List<&2, Seg>, +w: Nat) -> List<&2, Seg>:
125	  fit_if(Nat.is_gt(line_len(l), w), l, w)
126	
127	def sev_ok(+warn: Bool) -> Role:
128	  match warn:
129	    case True{}:
130	      RWarn{}
131	    case False{}:
132	      ROk{}
133	
134	def sev_warn(+c: U32) -> Role:
135	  sev_ok(U32.is_ge(c, 7000))
136	
137	def sev_pick(+crit: Bool, +c: U32) -> Role:
138	  match crit:
139	    case True{}:
140	      RCrit{}
141	    case False{}:
142	      sev_warn(c)
143	
144	# Bar colour from the centi-percent: red from 90 %, amber from 70 %.
145	def severity(+c: U32) -> Role:
146	  sev_pick(U32.is_ge(c, 9000), c)
147	
148	def is_tick(+t: Maybe<&2, Nat>, +i: Nat) -> Bool:
149	  match t:
150	    case None{}:
151	      False{}
152	    case Some{k}:
153	      Nat.is_eq(k, i)
154	
155	def cell_kind(+tick: Bool, +filled: Bool, +half: Bool, +r: Role, +dim: Bool) -> Seg:
156	  match tick filled half:
157	    case True{} _ _:
158	      sg("┃", RWarn{})
159	    case False{} True{} _:
160	      Seg{"━", r, dim}
161	    case False{} False{} True{}:
162	      Seg{"╸", r, dim}
163	    case False{} False{} False{}:
164	      sg("─", RTrack{})
165	
166	def cell(+i: Nat, +full: Nat, +half: Bool, +tick: Maybe<&2, Nat>, +r: Role, +dim: Bool) -> Seg:
167	  cell_kind(is_tick(tick, i), Nat.is_lt(i, full), Nat.is_eq(i, full) && half, r, dim)
168	
169	# `n` cells from index `i`.
170	def cells(+n: Nat, +i: Nat, +full: Nat, +half: Bool, +tick: Maybe<&2, Nat>, +r: Role, +dim: Bool) -> List<&2, Seg>:
171	  match n:
172	    case 0n:
173	      Nil{}
174	    case 1n+p:
175	      Con{cell(i, full, half, tick, r, dim), cells(p, Nat.add(i, 1n), full, half, tick, r, dim)}
176	
177	# Where the threshold tick sits: round(threshold / 100 * width), kept in range.
178	def tick_at(+thr: Maybe<&2, U32>, +w: Nat) -> Maybe<&2, Nat>:
179	  match thr:
180	    case None{}:
181	      None{}
182	    case Some{t}:
183	      Some{Nat.min(Nat.sub(w, 1n), U32.to_nat((((t * U32.from_nat(w)) + 5000 : U32) / 10000 : U32)))}
184	
185	# A usage bar of `w` cells for a centi-percent (None: an empty track).
186	def bar(+pct: Maybe<&2, U32>, +w: Nat, +thr: Maybe<&2, U32>, +stale: Bool) -> List<&2, Seg>:
187	  match pct:
188	    case None{}:
189	      Con{sg(String.repeat("─", w), RTrack{}), Nil{}}
190	    case Some{c}:
191	      cells(w, 0n, U32.to_nat(((U32.min(c, 10000) * U32.from_nat(w)) / 10000 : U32)), U32.is_ge((((U32.min(c, 10000) * U32.from_nat(w)) % 10000 : U32)), 5000), tick_at(thr, w), severity(c), stale)
192	
193	# ---- painting -----------------------------------------------------------------
194	
195	def sgr(+r: Role) -> String:
196	  match r:
197	    case RPlain{}:
198	      ""
199	    case RBold{}:
200	      "1"
201	    case RAccent{}:
202	      "38;5;173"
203	    case RAccentB{}:
204	      "1;38;5;173"
205	    case RMuted{}:
206	      "38;5;245"
207	    case ROk{}:
208	      "38;5;108"
209	    case RWarn{}:
210	      "38;5;179"
211	    case RCrit{}:
212	      "38;5;167"
213	    case RTrack{}:
214	      "38;5;238"
215	
216	def codes(+r: Role, +dim: Bool) -> String:
217	  sel.s(String.is_empty(sgr(r)), sel.s(dim, "2", ""), sel.s(dim, sgr(r) ++ ";2", sgr(r)))
218	
219	def paint_with(+color: Bool, +t: String, +c: String) -> String:
220	  sel.s(color && Bool.not(String.is_empty(c)), "\u{1B}[" ++ c ++ "m" ++ t ++ "\u{1B}[0m", t)
221	
222	def paint_seg(+s: Seg, +color: Bool) -> String:
223	  match s:
224	    case Seg{t, r, d}:
225	      paint_with(color, t, codes(r, d))
226	
227	def paint_all(+l: List<&2, Seg>, +color: Bool) -> String:
228	  match l:
229	    case Nil{}:
230	      ""
231	    case Con{s, t}:
232	      paint_seg(s, color) ++ paint_all(t, color)
233	
234	def style_key(+s: Seg) -> String:
235	  match s:
236	    case Seg{t, r, d}:
237	      codes(r, d)
238	
239	def same_style(+a: Seg, +b: Seg) -> Bool:
240	  String.eq(style_key(a), style_key(b))
241	
242	def join_seg(+a: Seg, +b: Seg) -> Seg:
243	  match a b:
244	    case Seg{x, r, d} Seg{y, r2, d2}:
245	      Seg{x ++ y, r, d}
246	
247	def merge_acc(+same: Bool, +cur: Seg, +s: Seg) -> Seg:
248	  match same:
249	    case True{}:
250	      join_seg(cur, s)
251	    case False{}:
252	      s
253	
254	def merge_emit(+same: Bool, +cur: Seg, +rest: List<&2, Seg>) -> List<&2, Seg>:
255	  match same:
256	    case True{}:
257	      rest
258	    case False{}:
259	      Con{cur, rest}
260	
261	def merge_go(+l: List<&2, Seg>, +cur: Seg) -> List<&2, Seg>:
262	  match l:
263	    case Nil{}:
264	      Con{cur, Nil{}}
265	    case Con{s, t}:
266	      merge_emit(same_style(cur, s), cur, merge_go(t, merge_acc(same_style(cur, s), cur, s)))
267	
268	# Neighbouring segments in one style become one (one escape per run).
269	def merged(+l: List<&2, Seg>) -> List<&2, Seg>:
270	  match l:
271	    case Nil{}:
272	      Nil{}
273	    case Con{s, t}:
274	      merge_go(t, s)
275	
276	def paint(+l: List<&2, Seg>, +color: Bool) -> String:
277	  paint_all(merged(l), color)
278	
279	def render_rest(+ls: List<&2, List<&2, Seg>>, +color: Bool) -> String:
280	  match ls:
281	    case Nil{}:
282	      ""
283	    case Con{l, t}:
284	      "\n" ++ paint(l, color) ++ render_rest(t, color)
285	
286	# Lines joined with newlines, each painted (or plain under NO_COLOR).
287	def render(+ls: List<&2, List<&2, Seg>>, +color: Bool) -> String:
288	  match ls:
289	    case Nil{}:
290	      ""
291	    case Con{l, t}:
292	      paint(l, color) ++ render_rest(t, color)
293	
294	
295	# ---- merging neighbours ----------------------------------------------------------