fmt.bend source
fmt.bend on the hub · documented module
# Text formatting: a string builder, format, padding, and shortest F32 printing.import Base# A builder holds its chunks newest first, so add is O(1) and build joins once.type Builder is Data: Builder{rev: List<&2, String>}def Builder.new() -> Builder: Builder{Nil{}}def Builder.add(b: Builder, s: String) -> Builder: match b: case Builder{r}: Builder{s <> r}def Builder.build(b: Builder) -> String: match b: case Builder{r}: String.concat(List.reverse(&2, String, r))def Fmt.fill(n: Nat, +c: Char) -> String: String.repeat(SCon{c, SNil{}}, n)# Pads s with c to w chars; a string at least w long stays as is.def Fmt.pad_left(+s: String, w: Nat, +c: Char) -> String: String.append(Fmt.fill(Nat.sub(w, String.length(s)), c), s)def Fmt.pad_right(+s: String, w: Nat, +c: Char) -> String: String.append(s, Fmt.fill(Nat.sub(w, String.length(s)), c))def Fmt.center.go(+pad: Nat, s: String, +c: Char) -> String: +l = {Nat.div(pad, 2n) : Nat} Fmt.fill(l, c) ++ s ++ Fmt.fill(Nat.sub(pad, l), c)# The odd pad char goes on the right.def Fmt.center(+s: String, w: Nat, +c: Char) -> String: Fmt.center.go(Nat.sub(w, String.length(s)), s, c)type Tok is Data: TChr{c: Char} THole{} TEnd{}def Fmt.next.open.if(esc: Bool, hole: Bool, c: Char, u: String) -> Tok & String: match esc: case True{}: (TChr{'{'}, u) case False{}: match hole: case True{}: (THole{}, u) case False{}: (TChr{'{'}, SCon{c, u})def Fmt.next.open(t: String) -> Tok & String: match t: case SNil{}: (TChr{'{'}, SNil{}) case SCon{Chr{y}, u}: +c = {y : U32} Fmt.next.open.if(U32.is_eq(c, 123), U32.is_eq(c, 125), Chr{c}, u)def Fmt.next.close.if(esc: Bool, c: Char, u: String) -> Tok & String: match esc: case True{}: (TChr{'}'}, u) case False{}: (TChr{'}'}, SCon{c, u})def Fmt.next.close(t: String) -> Tok & String: match t: case SNil{}: (TChr{'}'}, SNil{}) case SCon{Chr{y}, u}: +c = {y : U32} Fmt.next.close.if(U32.is_eq(c, 125), Chr{c}, u)def Fmt.next.pick(open: Bool, close: Bool, c: Char, t: String) -> Tok & String: match open: case True{}: Fmt.next.open(t) case False{}: match close: case True{}: Fmt.next.close(t) case False{}: (TChr{c}, t)def Fmt.next(s: String) -> Tok & String: match s: case SNil{}: (TEnd{}, SNil{}) case SCon{Chr{x}, t}: +c = {x : U32} Fmt.next.pick(U32.is_eq(c, 123), U32.is_eq(c, 125), Chr{c}, t)# Each token eats at least one char, so fuel f is the template length.def Fmt.format.go(f: Nat, p: Tok & String, args: List<&2, String>) -> String: match f: case 0n: SNil{} case 1n+g: (tok, rest) = p match tok: case TEnd{}: SNil{} case TChr{c}: SCon{c, Fmt.format.go(g, Fmt.next(rest), args)} case THole{}: match args: case Nil{}: "{}" ++ Fmt.format.go(g, Fmt.next(rest), Nil{}) case Con{a, more}: a ++ Fmt.format.go(g, Fmt.next(rest), more)# "{}" takes the next argument, "{{" and "}}" print one brace, and a "{}"# past the last argument prints as is.def Fmt.format(+tpl: String, args: List<&2, String>) -> String: Fmt.format.go(String.length(tpl), Fmt.next(tpl), args)# A Big is a fixed 14 limbs of 16 bits, least significant first: 224 bits.def Big.zeros(n: Nat) -> List<&2, U32>: match n: case 0n: Nil{} case 1n+p: Con{0, Big.zeros(p)}def Big.of(+x: U32) -> List<&2, U32>: Con{U32.and(x, 65535), Con{U32.shrn(x, 16n), Big.zeros(12n)}}# m and c stay below 2^16, so a limb product fits a U32.def Big.mul(a: List<&2, U32>, +m: U32, c: U32) -> List<&2, U32>: match a: case Nil{}: Nil{} case Con{x, xs}: +t = {U32.add(U32.mul(x, m), c) : U32} Con{U32.and(t, 65535), Big.mul(xs, m, U32.shrn(t, 16n))}def Big.add(a: List<&2, U32>, b: List<&2, U32>, c: U32) -> List<&2, U32>: match a b: case Con{x, xs} Con{y, ys}: +t = {U32.add(U32.add(x, y), c) : U32} Con{U32.and(t, 65535), Big.add(xs, ys, U32.shrn(t, 16n))} case _ _: Nil{}# a - b for a >= b; w is the borrow.def Big.sub(a: List<&2, U32>, b: List<&2, U32>, w: U32) -> List<&2, U32>: match a b: case Con{x, xs} Con{y, ys}: +t = {U32.sub(U32.sub(U32.add(x, 65536), y), w) : U32} Con{U32.and(t, 65535), Big.sub(xs, ys, U32.sub(1, U32.shrn(t, 16n)))} case _ _: Nil{}def Big.cmp.then(hi: Cmp, lo: Cmp) -> Cmp: match hi: case EQ{}: lo case LT{}: LT{} case GT{}: GT{}def Big.cmp(a: List<&2, U32>, b: List<&2, U32>) -> Cmp: match a b: case Con{x, xs} Con{y, ys}: Big.cmp.then(Big.cmp(xs, ys), U32.cmp(x, y)) case _ _: EQ{}def Big.shl(k: Nat, a: List<&2, U32>) -> List<&2, U32>: match k: case 0n: a case 1n+j: Big.shl(j, Big.mul(a, 2, 0))# (q + t / s, t % s) for t < 10 s, by repeated subtraction.def Big.divsmall(f: Nat, ge: Bool, +q: U32, +t: List<&2, U32>, +s: List<&2, U32>) -> U32 & List<&2, U32>: match f: case 0n: (q, t) case 1n+g: match ge: case False{}: (q, t) case True{}: +t2 = {Big.sub(t, s, 0) : List<&2, U32>} Big.divsmall(g, Cmp.is_ge(Big.cmp(t2, s)), U32.add(q, 1), t2, s)# Burger and Dybvig's free-format digits: v = r / s, and the neighbours of# v sit at (r - mm) / s and (r + mp) / s.type St is Data: St{r: List<&2, U32>, s: List<&2, U32>, mp: List<&2, U32>, mm: List<&2, U32>}type Dig is Data: More{d: U32, st: St} Last{d: U32}# An even mantissa reads back from either bound, so the bounds count.def Short.high(even: Bool, r: List<&2, U32>, mp: List<&2, U32>, s: List<&2, U32>) -> Bool: match even: case True{}: Cmp.is_ge(Big.cmp(Big.add(r, mp, 0), s)) case False{}: Cmp.is_gt(Big.cmp(Big.add(r, mp, 0), s))def Short.low(even: Bool, r: List<&2, U32>, mm: List<&2, U32>) -> Bool: match even: case True{}: Cmp.is_le(Big.cmp(r, mm)) case False{}: Cmp.is_lt(Big.cmp(r, mm))# A tie rounds to the even digit.def Short.near(c: Cmp, +d: U32) -> U32: match c: case LT{}: d case GT{}: U32.add(d, 1) case EQ{}: U32.add(d, U32.and(d, 1))def Short.pick(tc1: Bool, tc2: Bool, +d: U32, +r: List<&2, U32>, +s: List<&2, U32>, mp: List<&2, U32>, mm: List<&2, U32>) -> Dig: match tc1: case False{}: match tc2: case False{}: More{d, St{r, s, mp, mm}} case True{}: Last{U32.add(d, 1)} case True{}: match tc2: case False{}: Last{d} case True{}: Last{Short.near(Big.cmp(Big.mul(r, 2, 0), s), d)}def Short.digit.fin(+even: Bool, qr: U32 & List<&2, U32>, +s: List<&2, U32>, +mp: List<&2, U32>, +mm: List<&2, U32>) -> Dig: (d, r) = qr +r1 = {r : List<&2, U32>} Short.pick(Short.low(even, r1, mm), Short.high(even, r1, mp, s), d, r1, s, mp, mm)def Short.digit(+even: Bool, st: St) -> Dig: match st: case St{r, s, mp, mm}: +s1 = {s : List<&2, U32>} +r10 = {Big.mul(r, 10, 0) : List<&2, U32>} Short.digit.fin(even, Big.divsmall(10n, Cmp.is_ge(Big.cmp(r10, s1)), 0, r10, s1), s1, Big.mul(mp, 10, 0), Big.mul(mm, 10, 0))def Short.gen(f: Nat, +even: Bool, o: Dig) -> List<&2, U32>: match f: case 0n: Nil{} case 1n+g: match o: case Last{d}: Con{d, Nil{}} case More{d, st}: Con{d, Short.gen(g, even, Short.digit(even, st))}# k is the decimal exponent plus 64: v = 0.d1d2... * 10^(k - 64).def Short.up(f: Nat, +even: Bool, big: Bool, st: St, +k: U32) -> St & U32: match f: case 0n: (st, k) case 1n+g: match big: case False{}: (st, k) case True{}: match st: case St{r, s, mp, mm}: +r1 = {r : List<&2, U32>} +mp1 = {mp : List<&2, U32>} +s10 = {Big.mul(s, 10, 0) : List<&2, U32>} Short.up(g, even, Short.high(even, r1, mp1, s10), St{r1, s10, mp1, mm}, U32.add(k, 1))def Short.down(f: Nat, +even: Bool, small: Bool, st: St, +k: U32) -> St & U32: match f: case 0n: (st, k) case 1n+g: match small: case False{}: (st, k) case True{}: match st: case St{r, s, mp, mm}: +r10 = {Big.mul(r, 10, 0) : List<&2, U32>} +mp10 = {Big.mul(mp, 10, 0) : List<&2, U32>} +s1 = {s : List<&2, U32>} Short.down(g, even, Bool.not(Short.high(even, Big.mul(r10, 10, 0), Big.mul(mp10, 10, 0), s1)), St{r10, s1, mp10, Big.mul(mm, 10, 0)}, U32.sub(k, 1))def Short.fix.down(+even: Bool, sk: St & U32) -> St & U32: (st, k) = sk match st: case St{r, s, mp, mm}: +r1 = {r : List<&2, U32>} +s1 = {s : List<&2, U32>} +mp1 = {mp : List<&2, U32>} Short.down(64n, even, Bool.not(Short.high(even, Big.mul(r1, 10, 0), Big.mul(mp1, 10, 0), s1)), St{r1, s1, mp1, mm}, k)def Short.fix(+even: Bool, st: St) -> St & U32: match st: case St{r, s, mp, mm}: +r1 = {r : List<&2, U32>} +s1 = {s : List<&2, U32>} +mp1 = {mp : List<&2, U32>} Short.fix.down(even, Short.up(64n, even, Short.high(even, r1, mp1, s1), St{r1, s1, mp1, mm}, 64))def Short.chars(ds: List<&2, U32>) -> String: match ds: case Nil{}: SNil{} case Con{d, t}: SCon{Chr{U32.add(48, d)}, Short.chars(t)}def Short.exp.if(small: Bool, +e: U32) -> String: match small: case True{}: SCon{'0', U32.show(e)} case False{}: U32.show(e)def Short.exp(neg: Bool, +e: U32) -> String: match neg: case True{}: SCon{'-', Short.exp.if(U32.is_lt(e, 10), e)} case False{}: SCon{'+', Short.exp.if(U32.is_lt(e, 10), e)}def Short.frac(ds: String) -> String: match ds: case SNil{}: SNil{} case SCon{h, t}: SCon{'.', SCon{h, t}}def Short.sci(ds: String, +k: U32) -> String: match ds: case SNil{}: SNil{} case SCon{h, t}: SCon{h, Short.frac(t) ++ "e" ++ Short.exp(U32.is_lt(k, 65), U32.sub(U32.max(k, 65), U32.min(k, 65)))}def Short.fixed.big(ge: Bool, +ds: String, +kn: Nat) -> String: match ge: case True{}: ds ++ Fmt.fill(Nat.sub(kn, String.length(ds)), '0') ++ ".0" case False{}: String.take(ds, kn) ++ "." ++ String.drop(ds, kn)def Short.fixed(pos: Bool, +ds: String, +k: U32) -> String: match pos: case True{}: +kn = {U32.to_nat(U32.sub(k, 64)) : Nat} Short.fixed.big(Nat.is_ge(kn, String.length(ds)), ds, kn) case False{}: "0." ++ Fmt.fill(U32.to_nat(U32.sub(64, k)), '0') ++ dsdef Short.show.if(sci: Bool, +ds: String, +k: U32) -> String: match sci: case True{}: Short.sci(ds, k) case False{}: Short.fixed(U32.is_gt(k, 64), ds, k)# Like Python's repr: plain from 1e-4 up to 1e16, scientific outside.def Short.show(ds: String, +k: U32) -> String: Short.show.if(Bool.or(U32.is_lt(k, 61), U32.is_ge(k, 81)), ds, k)def Short.digits(+even: Bool, st: St) -> String: Short.chars(Short.gen(12n, even, Short.digit(even, st)))def Short.finite.fin(+even: Bool, sk: St & U32) -> String: (st, k) = sk Short.show(Short.digits(even, st), k)# v = f * 2^(be - 150); a power-of-two f above the least exponent has a# nearer lower neighbour, so t = 1 there. A and B are the positive and# negative parts of the binary exponent.def Short.finite.go(+f: U32, +be: U32, t: Nat) -> String: +tt = {t : Nat} +a = {Nat.sub(U32.to_nat(be), 150n) : Nat} +b = {Nat.sub(150n, U32.to_nat(be)) : Nat} +even = {U32.is_zero(U32.and(f, 1)) : Bool} Short.finite.fin(even, Short.fix(even, St{Big.shl(Nat.add(Nat.add(a, 1n), tt), Big.of(f)), Big.shl(Nat.add(Nat.add(b, 1n), tt), Big.of(1)), Big.shl(Nat.add(a, tt), Big.of(1)), Big.shl(a, Big.of(1))}))def Short.edge(e: Bool) -> Nat: match e: case True{}: 1n case False{}: 0ndef Short.finite(+ex: U32, +mant: U32) -> String: Short.finite.go(U32.or(mant, U32.shln(U32.min(ex, 1), 23n)), U32.max(ex, 1), Short.edge(Bool.and(U32.is_zero(mant), U32.is_gt(ex, 1))))def Short.sign(neg: Bool, s: String) -> String: match neg: case True{}: SCon{'-', s} case False{}: sdef Short.special(inf: Bool, neg: Bool) -> String: match inf: case True{}: Short.sign(neg, "inf") case False{}: "nan"def Short.go(inf: Bool, zero: Bool, +neg: Bool, +ex: U32, +mant: U32) -> String: match inf: case True{}: Short.special(U32.is_zero(mant), neg) case False{}: match zero: case True{}: Short.sign(neg, "0.0") case False{}: Short.sign(neg, Short.finite(ex, mant))# Base's F32.bits does not reduce in the checker, so proofs could not run it.def Short.bits(x: F32) -> U32: match x: case F32{w}: U32{w}# The shortest decimal that reads back to x, with ".0" on whole numbers.def F32.shortest(x: F32) -> String: +b = {Short.bits(x) : U32} +ex = {U32.and(U32.shrn(b, 23n), 255) : U32} +mant = {U32.and(b, 8388607) : U32} Short.go(U32.is_eq(ex, 255), Bool.and(U32.is_zero(ex), U32.is_zero(mant)), U32.is_ge(b, 2147483648), ex, mant)