def Short.finite.go

bend-kit-fmt@0.1.0.0 · fmt.bend:403

import Base

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))}))