fmt.bend checks

raw source on the hub · import bend-kit-fmt@0.1.0.0/fmt.bend as Fmt

Text formatting: a string builder, format, padding, and shortest F32 printing.

1 import

import Base

Types

type Builder source · line 5 · raw

Data

A builder holds its chunks newest first, so add is O(1) and build joins once.

Builder
```
@rev:List<&2, String> -> Builder
```

type Tok source · line 39 · raw

Data

TChr
```
@c:Char -> Tok
```
THole
```
Tok
```
TEnd
```
Tok
```

type St source · line 198 · raw

Data

Burger and Dybvig's free-format digits: v = r / s, and the neighbours of v sit at (r - mm) / s and (r + mp) / s.

St

@r:List<&2, U32> -> @s:List<&2, U32> -> @mp:List<&2, U32> -> @mm:List<&2, U32> -> St

type Dig source · line 202 · raw

Data

More
```
@d:U32 -> @st:St -> Dig
```
Last
```
@d:U32 -> Dig
```

Definitions

def Builder.new source · line 8 · raw

Builder

def Builder.add source · line 11 · raw

@b:Builder -> @s:String -> Builder

def Builder.build source · line 16 · raw

@b:Builder -> String

def Fmt.fill source · line 21 · raw

@n:Nat -> @+c:Char -> String

def Fmt.pad_left source · line 25 · raw

@+s:String -> @w:Nat -> @+c:Char -> String

Pads s with c to w chars; a string at least w long stays as is.

def Fmt.pad_right source · line 28 · raw

@+s:String -> @w:Nat -> @+c:Char -> String

def Fmt.center.go source · line 31 · raw

@+pad:Nat -> @s:String -> @+c:Char -> String

def Fmt.center source · line 36 · raw

@+s:String -> @w:Nat -> @+c:Char -> String

The odd pad char goes on the right.

def Fmt.next.open.if source · line 44 · raw

@esc:Bool -> @hole:Bool -> @c:Char -> @u:String -> Pair(Tok, String)

def Fmt.next.open source · line 56 · raw

@t:String -> Pair(Tok, String)

def Fmt.next.close.if source · line 64 · raw

@esc:Bool -> @c:Char -> @u:String -> Pair(Tok, String)

def Fmt.next.close source · line 71 · raw

@t:String -> Pair(Tok, String)

def Fmt.next.pick source · line 79 · raw

@open:Bool -> @close:Bool -> @c:Char -> @t:String -> Pair(Tok, String)

def Fmt.next source · line 90 · raw

@s:String -> Pair(Tok, String)

def Fmt.format.go source · line 99 · raw

@f:Nat -> @p:Pair(Tok, String) -> @args:List<&2, String> -> String

Each token eats at least one char, so fuel f is the template length.

def Fmt.format source · line 119 · raw

@+tpl:String -> @args:List<&2, String> -> String

"{}" takes the next argument, "{{" and "}}" print one brace, and a "{}" past the last argument prints as is.

def Big.zeros source · line 123 · raw

@n:Nat -> List<&2, U32>

A Big is a fixed 14 limbs of 16 bits, least significant first: 224 bits.

def Big.of source · line 130 · raw

@+x:U32 -> List<&2, U32>

def Big.mul source · line 134 · raw

@a:List<&2, U32> -> @+m:U32 -> @c:U32 -> List<&2, U32>

m and c stay below 2^16, so a limb product fits a U32.

def Big.add source · line 142 · raw

@a:List<&2, U32> -> @b:List<&2, U32> -> @c:U32 -> List<&2, U32>

def Big.sub source · line 151 · raw

@a:List<&2, U32> -> @b:List<&2, U32> -> @w:U32 -> List<&2, U32>

a - b for a >= b; w is the borrow.

def Big.cmp.then source · line 159 · raw

@hi:Cmp -> @lo:Cmp -> Cmp

def Big.cmp source · line 168 · raw

@a:List<&2, U32> -> @b:List<&2, U32> -> Cmp

def Big.shl source · line 175 · raw

@k:Nat -> @a:List<&2, U32> -> List<&2, U32>

def Big.divsmall source · line 183 · raw

@f:Nat -> @ge:Bool -> @+q:U32 -> @+t:List<&2, U32> -> @+s:List<&2, U32> -> Pair(U32, List<&2, U32>)

(q + t / s, t % s) for t < 10 s, by repeated subtraction.

def Short.high source · line 207 · raw

@even:Bool -> @r:List<&2, U32> -> @mp:List<&2, U32> -> @s:List<&2, U32> -> Bool

An even mantissa reads back from either bound, so the bounds count.

def Short.low source · line 215 · raw

@even:Bool -> @r:List<&2, U32> -> @mm:List<&2, U32> -> Bool

def Short.near source · line 223 · raw

@c:Cmp -> @+d:U32 -> U32

A tie rounds to the even digit.

def Short.pick source · line 232 · raw

@tc1:Bool -> @tc2:Bool -> @+d:U32 -> @+r:List<&2, U32> -> @+s:List<&2, U32> -> @mp:List<&2, U32> -> @mm:List<&2, U32> -> Dig

def Short.digit.fin source · line 248 · raw

@+even:Bool -> @qr:Pair(U32, List<&2, U32>) -> @+s:List<&2, U32> -> @+mp:List<&2, U32> -> @+mm:List<&2, U32> -> Dig

def Short.digit source · line 255 · raw

@+even:Bool -> @st:St -> Dig

def Short.gen source · line 264 · raw

@f:Nat -> @+even:Bool -> @o:Dig -> List<&2, U32>

def Short.up source · line 276 · raw

@f:Nat -> @+even:Bool -> @big:Bool -> @st:St -> @+k:U32 -> Pair(St, U32)

k is the decimal exponent plus 64: v = 0.d1d2... * 10^(k - 64).

def Short.down source · line 293 · raw

@f:Nat -> @+even:Bool -> @small:Bool -> @st:St -> @+k:U32 -> Pair(St, U32)

def Short.fix.down source · line 313 · raw

@+even:Bool -> @sk:Pair(St, U32) -> Pair(St, U32)

def Short.fix source · line 324 · raw

@+even:Bool -> @st:St -> Pair(St, U32)

def Short.chars source · line 334 · raw

@ds:List<&2, U32> -> String

def Short.exp.if source · line 341 · raw

@small:Bool -> @+e:U32 -> String

def Short.exp source · line 348 · raw

@neg:Bool -> @+e:U32 -> String

def Short.frac source · line 355 · raw

@ds:String -> String

def Short.sci source · line 362 · raw

@ds:String -> @+k:U32 -> String

def Short.fixed.big source · line 370 · raw

@ge:Bool -> @+ds:String -> @+kn:Nat -> String

def Short.fixed source · line 377 · raw

@pos:Bool -> @+ds:String -> @+k:U32 -> String

def Short.show.if source · line 385 · raw

@sci:Bool -> @+ds:String -> @+k:U32 -> String

def Short.show source · line 393 · raw

@ds:String -> @+k:U32 -> String

Like Python's repr: plain from 1e-4 up to 1e16, scientific outside.

def Short.digits source · line 396 · raw

@+even:Bool -> @st:St -> String

def Short.finite.fin source · line 399 · raw

@+even:Bool -> @sk:Pair(St, U32) -> String

def Short.finite.go source · line 406 · raw

@+f:U32 -> @+be:U32 -> @t:Nat -> String

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.edge source · line 416 · raw

@e:Bool -> Nat

def Short.finite source · line 423 · raw

@+ex:U32 -> @+mant:U32 -> String

def Short.sign source · line 427 · raw

@neg:Bool -> @s:String -> String

def Short.special source · line 434 · raw

@inf:Bool -> @neg:Bool -> String

def Short.go source · line 441 · raw

@inf:Bool -> @zero:Bool -> @+neg:Bool -> @+ex:U32 -> @+mant:U32 -> String

def Short.bits source · line 454 · raw

@x:F32 -> U32

Base's F32.bits does not reduce in the checker, so proofs could not run it.

def F32.shortest source · line 460 · raw

@x:F32 -> String

The shortest decimal that reads back to x, with ".0" on whole numbers.