1	# Text formatting: a string builder, format, padding, and shortest F32 printing.
2	import Base
3	
4	# A builder holds its chunks newest first, so add is O(1) and build joins once.
5	type Builder is Data:
6	  Builder{rev: List<&2, String>}
7	
8	def Builder.new() -> Builder:
9	  Builder{Nil{}}
10	
11	def Builder.add(b: Builder, s: String) -> Builder:
12	  match b:
13	    case Builder{r}:
14	      Builder{s <> r}
15	
16	def Builder.build(b: Builder) -> String:
17	  match b:
18	    case Builder{r}:
19	      String.concat(List.reverse(&2, String, r))
20	
21	def Fmt.fill(n: Nat, +c: Char) -> String:
22	  String.repeat(SCon{c, SNil{}}, n)
23	
24	# Pads s with c to w chars; a string at least w long stays as is.
25	def Fmt.pad_left(+s: String, w: Nat, +c: Char) -> String:
26	  String.append(Fmt.fill(Nat.sub(w, String.length(s)), c), s)
27	
28	def Fmt.pad_right(+s: String, w: Nat, +c: Char) -> String:
29	  String.append(s, Fmt.fill(Nat.sub(w, String.length(s)), c))
30	
31	def Fmt.center.go(+pad: Nat, s: String, +c: Char) -> String:
32	  +l = {Nat.div(pad, 2n) : Nat}
33	  Fmt.fill(l, c) ++ s ++ Fmt.fill(Nat.sub(pad, l), c)
34	
35	# The odd pad char goes on the right.
36	def Fmt.center(+s: String, w: Nat, +c: Char) -> String:
37	  Fmt.center.go(Nat.sub(w, String.length(s)), s, c)
38	
39	type Tok is Data:
40	  TChr{c: Char}
41	  THole{}
42	  TEnd{}
43	
44	def Fmt.next.open.if(esc: Bool, hole: Bool, c: Char, u: String) ->
45	  Tok & String:
46	  match esc:
47	    case True{}:
48	      (TChr{'{'}, u)
49	    case False{}:
50	      match hole:
51	        case True{}:
52	          (THole{}, u)
53	        case False{}:
54	          (TChr{'{'}, SCon{c, u})
55	
56	def Fmt.next.open(t: String) -> Tok & String:
57	  match t:
58	    case SNil{}:
59	      (TChr{'{'}, SNil{})
60	    case SCon{Chr{y}, u}:
61	      +c = {y : U32}
62	      Fmt.next.open.if(U32.is_eq(c, 123), U32.is_eq(c, 125), Chr{c}, u)
63	
64	def Fmt.next.close.if(esc: Bool, c: Char, u: String) -> Tok & String:
65	  match esc:
66	    case True{}:
67	      (TChr{'}'}, u)
68	    case False{}:
69	      (TChr{'}'}, SCon{c, u})
70	
71	def Fmt.next.close(t: String) -> Tok & String:
72	  match t:
73	    case SNil{}:
74	      (TChr{'}'}, SNil{})
75	    case SCon{Chr{y}, u}:
76	      +c = {y : U32}
77	      Fmt.next.close.if(U32.is_eq(c, 125), Chr{c}, u)
78	
79	def Fmt.next.pick(open: Bool, close: Bool, c: Char, t: String) -> Tok & String:
80	  match open:
81	    case True{}:
82	      Fmt.next.open(t)
83	    case False{}:
84	      match close:
85	        case True{}:
86	          Fmt.next.close(t)
87	        case False{}:
88	          (TChr{c}, t)
89	
90	def Fmt.next(s: String) -> Tok & String:
91	  match s:
92	    case SNil{}:
93	      (TEnd{}, SNil{})
94	    case SCon{Chr{x}, t}:
95	      +c = {x : U32}
96	      Fmt.next.pick(U32.is_eq(c, 123), U32.is_eq(c, 125), Chr{c}, t)
97	
98	# Each token eats at least one char, so fuel f is the template length.
99	def Fmt.format.go(f: Nat, p: Tok & String, args: List<&2, String>) -> String:
100	  match f:
101	    case 0n:
102	      SNil{}
103	    case 1n+g:
104	      (tok, rest) = p
105	      match tok:
106	        case TEnd{}:
107	          SNil{}
108	        case TChr{c}:
109	          SCon{c, Fmt.format.go(g, Fmt.next(rest), args)}
110	        case THole{}:
111	          match args:
112	            case Nil{}:
113	              "{}" ++ Fmt.format.go(g, Fmt.next(rest), Nil{})
114	            case Con{a, more}:
115	              a ++ Fmt.format.go(g, Fmt.next(rest), more)
116	
117	# "{}" takes the next argument, "{{" and "}}" print one brace, and a "{}"
118	# past the last argument prints as is.
119	def Fmt.format(+tpl: String, args: List<&2, String>) -> String:
120	  Fmt.format.go(String.length(tpl), Fmt.next(tpl), args)
121	
122	# A Big is a fixed 14 limbs of 16 bits, least significant first: 224 bits.
123	def Big.zeros(n: Nat) -> List<&2, U32>:
124	  match n:
125	    case 0n:
126	      Nil{}
127	    case 1n+p:
128	      Con{0, Big.zeros(p)}
129	
130	def Big.of(+x: U32) -> List<&2, U32>:
131	  Con{U32.and(x, 65535), Con{U32.shrn(x, 16n), Big.zeros(12n)}}
132	
133	# m and c stay below 2^16, so a limb product fits a U32.
134	def Big.mul(a: List<&2, U32>, +m: U32, c: U32) -> List<&2, U32>:
135	  match a:
136	    case Nil{}:
137	      Nil{}
138	    case Con{x, xs}:
139	      +t = {U32.add(U32.mul(x, m), c) : U32}
140	      Con{U32.and(t, 65535), Big.mul(xs, m, U32.shrn(t, 16n))}
141	
142	def Big.add(a: List<&2, U32>, b: List<&2, U32>, c: U32) -> List<&2, U32>:
143	  match a b:
144	    case Con{x, xs} Con{y, ys}:
145	      +t = {U32.add(U32.add(x, y), c) : U32}
146	      Con{U32.and(t, 65535), Big.add(xs, ys, U32.shrn(t, 16n))}
147	    case _ _:
148	      Nil{}
149	
150	# a - b for a >= b; w is the borrow.
151	def Big.sub(a: List<&2, U32>, b: List<&2, U32>, w: U32) -> List<&2, U32>:
152	  match a b:
153	    case Con{x, xs} Con{y, ys}:
154	      +t = {U32.sub(U32.sub(U32.add(x, 65536), y), w) : U32}
155	      Con{U32.and(t, 65535), Big.sub(xs, ys, U32.sub(1, U32.shrn(t, 16n)))}
156	    case _ _:
157	      Nil{}
158	
159	def Big.cmp.then(hi: Cmp, lo: Cmp) -> Cmp:
160	  match hi:
161	    case EQ{}:
162	      lo
163	    case LT{}:
164	      LT{}
165	    case GT{}:
166	      GT{}
167	
168	def Big.cmp(a: List<&2, U32>, b: List<&2, U32>) -> Cmp:
169	  match a b:
170	    case Con{x, xs} Con{y, ys}:
171	      Big.cmp.then(Big.cmp(xs, ys), U32.cmp(x, y))
172	    case _ _:
173	      EQ{}
174	
175	def Big.shl(k: Nat, a: List<&2, U32>) -> List<&2, U32>:
176	  match k:
177	    case 0n:
178	      a
179	    case 1n+j:
180	      Big.shl(j, Big.mul(a, 2, 0))
181	
182	# (q + t / s, t % s) for t < 10 s, by repeated subtraction.
183	def Big.divsmall(f: Nat, ge: Bool, +q: U32, +t: List<&2, U32>,
184	  +s: List<&2, U32>) -> U32 & List<&2, U32>:
185	  match f:
186	    case 0n:
187	      (q, t)
188	    case 1n+g:
189	      match ge:
190	        case False{}:
191	          (q, t)
192	        case True{}:
193	          +t2 = {Big.sub(t, s, 0) : List<&2, U32>}
194	          Big.divsmall(g, Cmp.is_ge(Big.cmp(t2, s)), U32.add(q, 1), t2, s)
195	
196	# Burger and Dybvig's free-format digits: v = r / s, and the neighbours of
197	# v sit at (r - mm) / s and (r + mp) / s.
198	type St is Data:
199	  St{r: List<&2, U32>, s: List<&2, U32>, mp: List<&2, U32>,
200	    mm: List<&2, U32>}
201	
202	type Dig is Data:
203	  More{d: U32, st: St}
204	  Last{d: U32}
205	
206	# An even mantissa reads back from either bound, so the bounds count.
207	def Short.high(even: Bool, r: List<&2, U32>, mp: List<&2, U32>,
208	  s: List<&2, U32>) -> Bool:
209	  match even:
210	    case True{}:
211	      Cmp.is_ge(Big.cmp(Big.add(r, mp, 0), s))
212	    case False{}:
213	      Cmp.is_gt(Big.cmp(Big.add(r, mp, 0), s))
214	
215	def Short.low(even: Bool, r: List<&2, U32>, mm: List<&2, U32>) -> Bool:
216	  match even:
217	    case True{}:
218	      Cmp.is_le(Big.cmp(r, mm))
219	    case False{}:
220	      Cmp.is_lt(Big.cmp(r, mm))
221	
222	# A tie rounds to the even digit.
223	def Short.near(c: Cmp, +d: U32) -> U32:
224	  match c:
225	    case LT{}:
226	      d
227	    case GT{}:
228	      U32.add(d, 1)
229	    case EQ{}:
230	      U32.add(d, U32.and(d, 1))
231	
232	def Short.pick(tc1: Bool, tc2: Bool, +d: U32, +r: List<&2, U32>,
233	  +s: List<&2, U32>, mp: List<&2, U32>, mm: List<&2, U32>) -> Dig:
234	  match tc1:
235	    case False{}:
236	      match tc2:
237	        case False{}:
238	          More{d, St{r, s, mp, mm}}
239	        case True{}:
240	          Last{U32.add(d, 1)}
241	    case True{}:
242	      match tc2:
243	        case False{}:
244	          Last{d}
245	        case True{}:
246	          Last{Short.near(Big.cmp(Big.mul(r, 2, 0), s), d)}
247	
248	def Short.digit.fin(+even: Bool, qr: U32 & List<&2, U32>, +s: List<&2, U32>,
249	  +mp: List<&2, U32>, +mm: List<&2, U32>) -> Dig:
250	  (d, r) = qr
251	  +r1 = {r : List<&2, U32>}
252	  Short.pick(Short.low(even, r1, mm), Short.high(even, r1, mp, s), d, r1, s,
253	    mp, mm)
254	
255	def Short.digit(+even: Bool, st: St) -> Dig:
256	  match st:
257	    case St{r, s, mp, mm}:
258	      +s1 = {s : List<&2, U32>}
259	      +r10 = {Big.mul(r, 10, 0) : List<&2, U32>}
260	      Short.digit.fin(even,
261	        Big.divsmall(10n, Cmp.is_ge(Big.cmp(r10, s1)), 0, r10, s1), s1,
262	        Big.mul(mp, 10, 0), Big.mul(mm, 10, 0))
263	
264	def Short.gen(f: Nat, +even: Bool, o: Dig) -> List<&2, U32>:
265	  match f:
266	    case 0n:
267	      Nil{}
268	    case 1n+g:
269	      match o:
270	        case Last{d}:
271	          Con{d, Nil{}}
272	        case More{d, st}:
273	          Con{d, Short.gen(g, even, Short.digit(even, st))}
274	
275	# k is the decimal exponent plus 64: v = 0.d1d2... * 10^(k - 64).
276	def Short.up(f: Nat, +even: Bool, big: Bool, st: St, +k: U32) -> St & U32:
277	  match f:
278	    case 0n:
279	      (st, k)
280	    case 1n+g:
281	      match big:
282	        case False{}:
283	          (st, k)
284	        case True{}:
285	          match st:
286	            case St{r, s, mp, mm}:
287	              +r1 = {r : List<&2, U32>}
288	              +mp1 = {mp : List<&2, U32>}
289	              +s10 = {Big.mul(s, 10, 0) : List<&2, U32>}
290	              Short.up(g, even, Short.high(even, r1, mp1, s10),
291	                St{r1, s10, mp1, mm}, U32.add(k, 1))
292	
293	def Short.down(f: Nat, +even: Bool, small: Bool, st: St, +k: U32) ->
294	  St & U32:
295	  match f:
296	    case 0n:
297	      (st, k)
298	    case 1n+g:
299	      match small:
300	        case False{}:
301	          (st, k)
302	        case True{}:
303	          match st:
304	            case St{r, s, mp, mm}:
305	              +r10 = {Big.mul(r, 10, 0) : List<&2, U32>}
306	              +mp10 = {Big.mul(mp, 10, 0) : List<&2, U32>}
307	              +s1 = {s : List<&2, U32>}
308	              Short.down(g, even,
309	                Bool.not(Short.high(even, Big.mul(r10, 10, 0),
310	                  Big.mul(mp10, 10, 0), s1)),
311	                St{r10, s1, mp10, Big.mul(mm, 10, 0)}, U32.sub(k, 1))
312	
313	def Short.fix.down(+even: Bool, sk: St & U32) -> St & U32:
314	  (st, k) = sk
315	  match st:
316	    case St{r, s, mp, mm}:
317	      +r1 = {r : List<&2, U32>}
318	      +s1 = {s : List<&2, U32>}
319	      +mp1 = {mp : List<&2, U32>}
320	      Short.down(64n, even,
321	        Bool.not(Short.high(even, Big.mul(r1, 10, 0), Big.mul(mp1, 10, 0), s1)),
322	        St{r1, s1, mp1, mm}, k)
323	
324	def Short.fix(+even: Bool, st: St) -> St & U32:
325	  match st:
326	    case St{r, s, mp, mm}:
327	      +r1 = {r : List<&2, U32>}
328	      +s1 = {s : List<&2, U32>}
329	      +mp1 = {mp : List<&2, U32>}
330	      Short.fix.down(even,
331	        Short.up(64n, even, Short.high(even, r1, mp1, s1), St{r1, s1, mp1, mm},
332	          64))
333	
334	def Short.chars(ds: List<&2, U32>) -> String:
335	  match ds:
336	    case Nil{}:
337	      SNil{}
338	    case Con{d, t}:
339	      SCon{Chr{U32.add(48, d)}, Short.chars(t)}
340	
341	def Short.exp.if(small: Bool, +e: U32) -> String:
342	  match small:
343	    case True{}:
344	      SCon{'0', U32.show(e)}
345	    case False{}:
346	      U32.show(e)
347	
348	def Short.exp(neg: Bool, +e: U32) -> String:
349	  match neg:
350	    case True{}:
351	      SCon{'-', Short.exp.if(U32.is_lt(e, 10), e)}
352	    case False{}:
353	      SCon{'+', Short.exp.if(U32.is_lt(e, 10), e)}
354	
355	def Short.frac(ds: String) -> String:
356	  match ds:
357	    case SNil{}:
358	      SNil{}
359	    case SCon{h, t}:
360	      SCon{'.', SCon{h, t}}
361	
362	def Short.sci(ds: String, +k: U32) -> String:
363	  match ds:
364	    case SNil{}:
365	      SNil{}
366	    case SCon{h, t}:
367	      SCon{h, Short.frac(t) ++ "e" ++
368	        Short.exp(U32.is_lt(k, 65), U32.sub(U32.max(k, 65), U32.min(k, 65)))}
369	
370	def Short.fixed.big(ge: Bool, +ds: String, +kn: Nat) -> String:
371	  match ge:
372	    case True{}:
373	      ds ++ Fmt.fill(Nat.sub(kn, String.length(ds)), '0') ++ ".0"
374	    case False{}:
375	      String.take(ds, kn) ++ "." ++ String.drop(ds, kn)
376	
377	def Short.fixed(pos: Bool, +ds: String, +k: U32) -> String:
378	  match pos:
379	    case True{}:
380	      +kn = {U32.to_nat(U32.sub(k, 64)) : Nat}
381	      Short.fixed.big(Nat.is_ge(kn, String.length(ds)), ds, kn)
382	    case False{}:
383	      "0." ++ Fmt.fill(U32.to_nat(U32.sub(64, k)), '0') ++ ds
384	
385	def Short.show.if(sci: Bool, +ds: String, +k: U32) -> String:
386	  match sci:
387	    case True{}:
388	      Short.sci(ds, k)
389	    case False{}:
390	      Short.fixed(U32.is_gt(k, 64), ds, k)
391	
392	# Like Python's repr: plain from 1e-4 up to 1e16, scientific outside.
393	def Short.show(ds: String, +k: U32) -> String:
394	  Short.show.if(Bool.or(U32.is_lt(k, 61), U32.is_ge(k, 81)), ds, k)
395	
396	def Short.digits(+even: Bool, st: St) -> String:
397	  Short.chars(Short.gen(12n, even, Short.digit(even, st)))
398	
399	def Short.finite.fin(+even: Bool, sk: St & U32) -> String:
400	  (st, k) = sk
401	  Short.show(Short.digits(even, st), k)
402	
403	# v = f * 2^(be - 150); a power-of-two f above the least exponent has a
404	# nearer lower neighbour, so t = 1 there. A and B are the positive and
405	# negative parts of the binary exponent.
406	def Short.finite.go(+f: U32, +be: U32, t: Nat) -> String:
407	  +tt = {t : Nat}
408	  +a = {Nat.sub(U32.to_nat(be), 150n) : Nat}
409	  +b = {Nat.sub(150n, U32.to_nat(be)) : Nat}
410	  +even = {U32.is_zero(U32.and(f, 1)) : Bool}
411	  Short.finite.fin(even, Short.fix(even,
412	    St{Big.shl(Nat.add(Nat.add(a, 1n), tt), Big.of(f)),
413	      Big.shl(Nat.add(Nat.add(b, 1n), tt), Big.of(1)),
414	      Big.shl(Nat.add(a, tt), Big.of(1)), Big.shl(a, Big.of(1))}))
415	
416	def Short.edge(e: Bool) -> Nat:
417	  match e:
418	    case True{}:
419	      1n
420	    case False{}:
421	      0n
422	
423	def Short.finite(+ex: U32, +mant: U32) -> String:
424	  Short.finite.go(U32.or(mant, U32.shln(U32.min(ex, 1), 23n)), U32.max(ex, 1),
425	    Short.edge(Bool.and(U32.is_zero(mant), U32.is_gt(ex, 1))))
426	
427	def Short.sign(neg: Bool, s: String) -> String:
428	  match neg:
429	    case True{}:
430	      SCon{'-', s}
431	    case False{}:
432	      s
433	
434	def Short.special(inf: Bool, neg: Bool) -> String:
435	  match inf:
436	    case True{}:
437	      Short.sign(neg, "inf")
438	    case False{}:
439	      "nan"
440	
441	def Short.go(inf: Bool, zero: Bool, +neg: Bool, +ex: U32, +mant: U32) ->
442	  String:
443	  match inf:
444	    case True{}:
445	      Short.special(U32.is_zero(mant), neg)
446	    case False{}:
447	      match zero:
448	        case True{}:
449	          Short.sign(neg, "0.0")
450	        case False{}:
451	          Short.sign(neg, Short.finite(ex, mant))
452	
453	# Base's F32.bits does not reduce in the checker, so proofs could not run it.
454	def Short.bits(x: F32) -> U32:
455	  match x:
456	    case F32{w}:
457	      U32{w}
458	
459	# The shortest decimal that reads back to x, with ".0" on whole numbers.
460	def F32.shortest(x: F32) -> String:
461	  +b = {Short.bits(x) : U32}
462	  +ex = {U32.and(U32.shrn(b, 23n), 255) : U32}
463	  +mant = {U32.and(b, 8388607) : U32}
464	  Short.go(U32.is_eq(ex, 255), Bool.and(U32.is_zero(ex), U32.is_zero(mant)),
465	    U32.is_ge(b, 2147483648), ex, mant)