Human-readable exact dyadic formatting

Dyadics with normalized exponents in [-18, 18] are printed as exact decimals; the remaining values use a significand times a power of two. This diagnostic notation limits expansion caused by the exponent, while the printed significand can still be arbitrarily large. Formatting uses integer arithmetic throughout.

def FloatLib.Numerics.Dyadic.Formatting.normalizeMagnitudeLoop : ℕ → ℕ → ℤ → ℕ × ℤ

Fuel-bounded worker that removes trailing binary zeroes from a magnitude.

def FloatLib.Numerics.Dyadic.Formatting.normalizeMagnitude (significand : ℕ) (exponent : ℤ) : ℕ × ℤ

Remove powers of two from a nonzero significand.

def FloatLib.Numerics.Dyadic.Formatting.trimFraction (digits : String) : String

Remove decimal zeroes that carry no information after the decimal point.

def FloatLib.Numerics.Dyadic.Formatting.withDecimalPoint (digits : String) (places : ℕ) : String

Insert a decimal point places digits from the right.

def FloatLib.Numerics.Dyadic.format (value : Dyadic) : String

Format an exact dyadic without changing its value.

The decimal branch is deliberately bounded. An arbitrary static format may have an enormous exponent range, so attempting to materialize every exact decimal expansion would make inspecting one extreme value allocate an unreasonable string.