fmt.bend

bend-kit-fmt@0.1.0.0 · 465 lines · 59 definitions

1# Text formatting: a string builder, format, padding, and shortest F32 printing.
2import Base
3
4# A builder holds its chunks newest first, so add is O(1) and build joins once.
5type Builder is Data:
6  Builder{rev: List<&2, String>}
7
8def Builder.new() -> Builder:
9  Builder{Nil{}}
10
11def Builder.add(b: Builder, s: String) -> Builder:
12  match b:
13    case Builder{r}:
14      Builder{s <> r}
15
16def Builder.build(b: Builder) -> String:
17  match b:
18    case Builder{r}:
19      String.concat(List.reverse(&2, String, r))
20
21def 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.
25def Fmt.pad_left(+s: String, w: Nat, +c: Char) -> String:
26  String.append(Fmt.fill(Nat.sub(w, String.length(s)), c), s)
27
28def Fmt.pad_right(+s: String, w: Nat, +c: Char) -> String:
29  String.append(s, Fmt.fill(Nat.sub(w, String.length(s)), c))
30
31def 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.
36def Fmt.center(+s: String, w: Nat, +c: Char) -> String:
37  Fmt.center.go(Nat.sub(w, String.length(s)), s, c)
38
39type Tok is Data:
40  TChr{c: Char}
41  THole{}
42  TEnd{}
43
44def 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
56def 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
64def 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
71def 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
79def 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
90def 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.
99def 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.
119def 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.
123def 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
130def 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.
134def 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
142def 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.
151def 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
159def 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
168def 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
175def 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.
183def 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.
198type St is Data:
199  St{r: List<&2, U32>, s: List<&2, U32>, mp: List<&2, U32>,
200    mm: List<&2, U32>}
201
202type 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.
207def 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
215def 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.
223def 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
232def 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
248def 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
255def 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
264def 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).
276def 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
293def 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
313def 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
324def 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
334def 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
341def 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
348def 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
355def Short.frac(ds: String) -> String:
356  match ds:
357    case SNil{}:
358      SNil{}
359    case SCon{h, t}:
360      SCon{'.', SCon{h, t}}
361
362def 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
370def 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
377def 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
385def 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.
393def 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
396def Short.digits(+even: Bool, st: St) -> String:
397  Short.chars(Short.gen(12n, even, Short.digit(even, st)))
398
399def 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.
406def 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
416def Short.edge(e: Bool) -> Nat:
417  match e:
418    case True{}:
419      1n
420    case False{}:
421      0n
422
423def 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
427def Short.sign(neg: Bool, s: String) -> String:
428  match neg:
429    case True{}:
430      SCon{'-', s}
431    case False{}:
432      s
433
434def Short.special(inf: Bool, neg: Bool) -> String:
435  match inf:
436    case True{}:
437      Short.sign(neg, "inf")
438    case False{}:
439      "nan"
440
441def 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.
454def 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.
460def 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)