Shortest decimal text of binary values

The display of a finite binary value is normally the shortest decimal that reads back as the same value. A value whose exact decimal has at most d significant digits, where d digits always identify a value of the format (17 for binary64, 9 for binary32, 5 for binary16, 4 for bfloat16), prints exactly instead, so 65504 stays 65504 in binary16 and 3.75 stays 3.75 in an 8-bit format.

The digits come from exact integer arithmetic on the interval of decimals that round to the value. The coarsest decimal grid 10^q meeting that interval is found by starting from its width and climbing, and the grid point nearest to the value is chosen, ties to even. The candidate is then converted by the parser's own decimal conversion. It is printed only if that conversion returns the value, and otherwise the exact decimal expansion is printed, so reading the text back returns the value by construction (Model.parse_format_of_isFinite).

Fixed notation is used from 0.0001 up to 10^d, and smaller and larger values use one leading digit and an e exponent.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.Range : Type

Magnitudes from low * 2^scale to high * 2^scale that read back as one finite nonzero value, each end included when its flag is set.

• low : ℕ

  Least magnitude, as a multiple of 2^scale.

• high : ℕ

  Greatest magnitude, as a multiple of 2^scale.

• lowIncluded : Bool

  Whether low itself reads back as the value.

• highIncluded : Bool

  Whether high itself reads back as the value.

• scale : ℤ

  Binary exponent of the unit.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.range (mode : IEEERoundingMode) (negative : Bool) (significand : ℕ) (exponent : ℤ) (binadeBottom : Bool) : Range

The range of magnitudes that round in mode to the value significand * 2^exponent.

Neighbors lie one unit 2^exponent away, except below the first value of a binade, where the step is half as large (binadeBottom). Nearest-even includes both midpoints exactly when the significand is even, and the directed modes take the half-open gap on the side they round from.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.step (scale q : ℤ) : ℕ × ℕ

10^q / 2^scale as a numerator and a denominator.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.first (range : Range) (lowFloor lowCeil : ℕ) : ℕ

The least multiple of a grid in the interval, from the floor and ceiling of its low end.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.last (range : Range) (highFloor highCeil : ℕ) : ℕ

The greatest multiple of a grid in the interval, from the floor and ceiling of its high end.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.bounds (value num den : ℕ) : ℕ × ℕ

Floor and ceiling of value * den / num.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.descend (range : Range) : ℕ → ℤ → ℕ → ℕ → Option (ℤ × ℕ × ℕ × ℕ × ℕ × ℕ × ℕ)

From the grid 10^q = (num / den) * 2^scale, lower q until the interval contains a multiple. Returns the grid with the floors and ceilings of both interval ends in its units.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.climb (range : Range) : ℕ → ℕ → ℕ → ℕ → ℕ → ℕ → ℕ × ℕ × ℕ

Coarsen a grid that meets the interval tenfold while the coarser grid still meets it, counting the steps. Floors and ceilings of the interval ends on the coarser grid are those of the finer grid divided by ten, so this needs no further exact arithmetic on the ends. Grids that meet the interval are closed under refinement, so the first miss leaves the coarsest one.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.search (range : Range) (target : ℕ) (negative : Bool) : Option Numerics.DecimalText.Decimal

The multiple of the coarsest decimal grid in the interval that is nearest to target * 2^scale, ties to the even multiple, with the given sign.

The initial grid comes from the interval width and 1233 / 4096 < log₁₀ 2. Descent allows for the estimate's error, then climbing finds the coarsest grid that meets the interval. Both loop bounds come from the exact integers' bit lengths, without a fixed precision or exponent limit.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.digits (fmt : FloatFormat) : ℕ

The number of significant decimal digits that always identify a value of the format, one more than the digits of 2^precision: 17 for binary64, 9 for binary32, 5 for binary16, 4 for bfloat16 and 3 for an 8-bit format with four significant bits.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.verified {fmt : FloatFormat} (mode : IEEERoundingMode) (value : Model fmt) (exact : Numerics.Dyadic) : Numerics.DecimalText.Decimal

The shortest candidate of search for the finite nonzero value value with exact value exact, kept only if the parser's value conversion in mode returns value. The exact decimal value replaces a candidate that does not.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.decimal {fmt : FloatFormat} (mode : IEEERoundingMode) (value : Model fmt) (exact : Numerics.Dyadic) : Numerics.DecimalText.Decimal

The decimal record displayed for the finite value value with exact value exact: zero with its sign, the exact value when it has at most digits fmt significant digits, and otherwise the verified shortest decimal.

An exact value with that few digits has a binary exponent within the bounds tested first, so values far outside them go straight to the search without expanding their exact decimal.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Shortest.characters (count : ℕ) (record : Numerics.DecimalText.Decimal) : List Char

Characters of a displayed decimal record: fixed notation when the leading digit lies between four places after the point and count places before it, otherwise one leading digit and an e exponent. Both read back as the value and sign of the record.