Numeric conversion between binary and decimal interchange

Both directions evaluate the finite input exactly as a rational before rounding once to the destination. Binary-to-decimal conversion prefers quantum zero on an exact result, so it selects the representable cohort member whose quantum is closest to zero. For an inexact result, decimal projection supplies the least quantum. Decimal-to-binary conversion uses the binary rational kernels. Nearest-away first rounds the exact rational to the destination binary grid, then encodes that dyadic with the binary encoder.

Zeros and infinities retain their signs. NaNs are quieted and raise invalid exactly when signaling. The diagnostic payload is interpreted as a natural number: it is preserved when it fits the destination, otherwise replaced by zero. This is a payload-selection policy, not a claim that IEEE 754 specifies a unique payload when narrowing.

Decimal destinations use tininess before rounding. Binary destinations use the library convention: tininess after rounding to the destination precision with an unbounded exponent range. The constants for the binary midpoint and predecessor are shared with the scalar status implementation.

References

• IEEE 754-2019, §§4.3, 5.2, 5.4.2, 6.2, 7.4 and 7.5.
• ISO/IEC JTC1/SC22/WG14, N2596, §5.2.4.2.3, preferred quantum exponents: https://www.open-std.org/jtc1/sc22/wg14/www/docs/n2596.pdf.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryPayload {fmt : BinaryInterchange.FloatFormat} (x : BinaryInterchange.Model fmt) : ℕ

Extract the diagnostic payload of an IEEE binary NaN, excluding its quiet bit.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.fromBinary {fmt : BinaryInterchange.FloatFormat} (target : Format) (mode : RoundingMode) (x : BinaryInterchange.Model fmt) : Outcome

Convert a binary model to a decimal datum. Exact finite results prefer quantum zero, and a zero keeps its source sign. Custom binary models convert through their descriptors, but the IEEE class guarantees hold only for IEEE source formats.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryNaN (fmt : BinaryInterchange.FloatFormat) (negative : Bool) (payload : ℕ) : BinaryInterchange.Model fmt

Encode a quiet binary NaN with its sign and a fitting natural-number payload. toBinary uses this only for an IEEE destination.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryQuantum (fmt : BinaryInterchange.FloatFormat) (magnitude : ℚ) : ℤ

Binary grid exponent for a rational magnitude, bounded below by the subnormal quantum.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryNearestAwayDyadic (fmt : BinaryInterchange.FloatFormat) (negative : Bool) (magnitude : ℚ) : Numerics.Dyadic

Round to nearest, ties away, on the destination's binary grid. The significand can reach 2^precision after a carry, and that value is still representable unless it overflows.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.roundBinaryMagnitude (fmt : BinaryInterchange.FloatFormat) (mode : RoundingMode) (negative : Bool) (magnitude : ℚ) : BinaryInterchange.Model fmt

Round a sign and a nonnegative rational magnitude, as toBinary supplies them, into the binary destination.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryRoundsAway (mode : RoundingMode) (negative : Bool) : Bool

Whether a directed conversion increases a nonzero magnitude. Nearest modes use midpoint rules and give false here.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryOverflow (fmt : BinaryInterchange.FloatFormat) (mode : RoundingMode) (negative : Bool) (magnitude : ℚ) : Bool

IEEE overflow test: the precision-rounded unbounded result against the exponent limit. The largest finite significand of an IEEE binary layout is odd, so both nearest modes overflow at the upper midpoint itself.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryTiny (fmt : BinaryInterchange.FloatFormat) (mode : RoundingMode) (negative : Bool) (magnitude : ℚ) (rounded : BinaryInterchange.Model fmt) : Bool

Tininess after precision rounding, including exact values that deliver the smallest normal but whose rounding with an unbounded exponent range is still tiny.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryStatus (fmt : BinaryInterchange.FloatFormat) (mode : RoundingMode) (negative : Bool) (magnitude : ℚ) (rounded : BinaryInterchange.Model fmt) : Numerics.IEEEStatus

Default binary conversion flags, using exact rational comparisons. Invalid and divide-by-zero are absent on the finite path. Overflow always raises inexact.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.binaryTernary (fmt : BinaryInterchange.FloatFormat) (negative : Bool) (magnitude : ℚ) (rounded : BinaryInterchange.Model fmt) : Ordering

Ternary value of a binary conversion: the delivered value compared with the exact signed rational, read through toRat? like the inexact flag of binaryStatus. A non-finite delivery is an overflow and compares by the sign of the exact value.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.toBinary (target : BinaryInterchange.FloatFormat) (_hIEEE : target.isIEEE = true) (mode : RoundingMode) (x : Datum) : BinaryInterchange.Model.IEEEOutcome target

Convert a decimal datum to an IEEE binary destination in any of the five rounding directions. The IEEE descriptor proof excludes finite-only exceptional-value policies. Finite input coefficients and quantum exponents are evaluated exactly, so the source decimal cohort does not affect the binary result. The ternary value compares the delivered value with the exact decimal value, and infinities and NaNs have .eq.