bend-kit-fmt Releases (1): 0.1.0.0 0xea2956cd4e05ac318643319cb7fb3c29 indexed https://jend.leeeet.dev/files.txt?path=bend-kit-fmt@0.1.0.0 Definitions (59): Fmt.Builder (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Builder) # 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>} Fmt.Builder.new (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Builder.new) def Builder.new() -> Builder: Fmt.Builder.add (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Builder.add) def Builder.add(b: Builder, s: String) -> Builder: Fmt.Builder.build (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Builder.build) def Builder.build(b: Builder) -> String: Fmt.Fmt.fill (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Fmt.fill) def Fmt.fill(n: Nat, +c: Char) -> String: Fmt.Fmt.pad_left (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Fmt.pad_left) # 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: Fmt.Fmt.pad_right (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Fmt.pad_right) def Fmt.pad_right(+s: String, w: Nat, +c: Char) -> String: Fmt.Fmt.center.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Fmt.center.go) def Fmt.center.go(+pad: Nat, s: String, +c: Char) -> String: Fmt.Fmt.center (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Fmt.center) # The odd pad char goes on the right. def Fmt.center(+s: String, w: Nat, +c: Char) -> String: Fmt.Tok (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Tok) type Tok is Data: TChr{c: Char} THole{} TEnd{} Fmt.Fmt.next.open.if (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Fmt.next.open.if) def Fmt.next.open.if(esc: Bool, hole: Bool, c: Char, u: String) -> Tok & String: Fmt.Fmt.next.open (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Fmt.next.open) def Fmt.next.open(t: String) -> Tok & String: Fmt.Fmt.next.close.if (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Fmt.next.close.if) def Fmt.next.close.if(esc: Bool, c: Char, u: String) -> Tok & String: Fmt.Fmt.next.close (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Fmt.next.close) def Fmt.next.close(t: String) -> Tok & String: Fmt.Fmt.next.pick (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Fmt.next.pick) def Fmt.next.pick(open: Bool, close: Bool, c: Char, t: String) -> Tok & String: Fmt.Fmt.next (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Fmt.next) def Fmt.next(s: String) -> Tok & String: Fmt.Fmt.format.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Fmt.format.go) # 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: Fmt.Fmt.format (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Fmt.format) # "{}" 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.Big.zeros (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Big.zeros) # A Big is a fixed 14 limbs of 16 bits, least significant first: 224 bits. def Big.zeros(n: Nat) -> List<&2, U32>: Fmt.Big.of (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Big.of) def Big.of(+x: U32) -> List<&2, U32>: Fmt.Big.mul (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Big.mul) # 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>: Fmt.Big.add (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Big.add) def Big.add(a: List<&2, U32>, b: List<&2, U32>, c: U32) -> List<&2, U32>: Fmt.Big.sub (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Big.sub) # 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>: Fmt.Big.cmp.then (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Big.cmp.then) def Big.cmp.then(hi: Cmp, lo: Cmp) -> Cmp: Fmt.Big.cmp (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Big.cmp) def Big.cmp(a: List<&2, U32>, b: List<&2, U32>) -> Cmp: Fmt.Big.shl (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Big.shl) def Big.shl(k: Nat, a: List<&2, U32>) -> List<&2, U32>: Fmt.Big.divsmall (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Big.divsmall) # (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>: Fmt.St (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=St) # 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>} Fmt.Dig (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Dig) type Dig is Data: More{d: U32, st: St} Last{d: U32} Fmt.Short.high (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.high) # 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: Fmt.Short.low (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.low) def Short.low(even: Bool, r: List<&2, U32>, mm: List<&2, U32>) -> Bool: Fmt.Short.near (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.near) # A tie rounds to the even digit. def Short.near(c: Cmp, +d: U32) -> U32: Fmt.Short.pick (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.pick) 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: Fmt.Short.digit.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.digit.fin) def Short.digit.fin(+even: Bool, qr: U32 & List<&2, U32>, +s: List<&2, U32>, +mp: List<&2, U32>, +mm: List<&2, U32>) -> Dig: Fmt.Short.digit (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.digit) def Short.digit(+even: Bool, st: St) -> Dig: Fmt.Short.gen (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.gen) def Short.gen(f: Nat, +even: Bool, o: Dig) -> List<&2, U32>: Fmt.Short.up (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.up) # 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: Fmt.Short.down (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.down) def Short.down(f: Nat, +even: Bool, small: Bool, st: St, +k: U32) -> St & U32: Fmt.Short.fix.down (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.fix.down) def Short.fix.down(+even: Bool, sk: St & U32) -> St & U32: Fmt.Short.fix (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.fix) def Short.fix(+even: Bool, st: St) -> St & U32: Fmt.Short.chars (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.chars) def Short.chars(ds: List<&2, U32>) -> String: Fmt.Short.exp.if (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.exp.if) def Short.exp.if(small: Bool, +e: U32) -> String: Fmt.Short.exp (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.exp) def Short.exp(neg: Bool, +e: U32) -> String: Fmt.Short.frac (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.frac) def Short.frac(ds: String) -> String: Fmt.Short.sci (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.sci) def Short.sci(ds: String, +k: U32) -> String: Fmt.Short.fixed.big (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.fixed.big) def Short.fixed.big(ge: Bool, +ds: String, +kn: Nat) -> String: Fmt.Short.fixed (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.fixed) def Short.fixed(pos: Bool, +ds: String, +k: U32) -> String: Fmt.Short.show.if (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.show.if) def Short.show.if(sci: Bool, +ds: String, +k: U32) -> String: Fmt.Short.show (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.show) # Like Python's repr: plain from 1e-4 up to 1e16, scientific outside. def Short.show(ds: String, +k: U32) -> String: Fmt.Short.digits (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.digits) def Short.digits(+even: Bool, st: St) -> String: Fmt.Short.finite.fin (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.finite.fin) def Short.finite.fin(+even: Bool, sk: St & U32) -> String: Fmt.Short.finite.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.finite.go) # 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: Fmt.Short.edge (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.edge) def Short.edge(e: Bool) -> Nat: Fmt.Short.finite (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.finite) def Short.finite(+ex: U32, +mant: U32) -> String: Fmt.Short.sign (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.sign) def Short.sign(neg: Bool, s: String) -> String: Fmt.Short.special (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.special) def Short.special(inf: Bool, neg: Bool) -> String: Fmt.Short.go (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.go) def Short.go(inf: Bool, zero: Bool, +neg: Bool, +ex: U32, +mant: U32) -> String: Fmt.Short.bits (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=Short.bits) # Base's F32.bits does not reduce in the checker, so proofs could not run it. def Short.bits(x: F32) -> U32: Fmt.F32.shortest (https://jend.leeeet.dev/definition.txt?path=bend-kit-fmt@0.1.0.0/fmt.bend&name=F32.shortest) # The shortest decimal that reads back to x, with ".0" on whole numbers. def F32.shortest(x: F32) -> String: