TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.DecimalInterchange.Conversion.Binary.Runtime

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; decimal projection supplies the least quantum for an inexact result. For an exact result, the selected quantum is closest to zero among its representable cohort members. Decimal-to-binary conversion uses the existing binary rational kernels. Nearest-away first rounds the exact rational to the destination binary grid, then encodes that representable dyadic with the existing 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 an explicit payload-selection policy, not a claim that IEEE 754 uniquely specifies a payload when narrowing.

Decimal destinations use tininess before rounding. Binary destinations use the existing 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 #

source
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.

Instances For
    source
    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; the source zero sign is retained. The numerical path also accepts custom binary models according to their descriptors; IEEE class guarantees apply to IEEE source formats.

    Instances For
      source
      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.

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

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

        Instances For
          source
          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 equal 2^precision at a carry; this is still exactly representable before overflow.

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

            Round a signed rational magnitude directly into the binary destination. The magnitude is supplied as a nonnegative rational by toBinary.

            Instances For
              source
              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 instead of this directed-mode predicate.

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

                IEEE overflow compares the precision-rounded unbounded result with the exponent limit. For IEEE binary layouts the largest finite significand is odd, so both nearest modes include the upper midpoint.

                Instances For
                  source
                  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 which deliver the smallest normal but whose unbounded-precision-grid rounding is still tiny.

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

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

                    Instances For
                      source
                      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.

                      Instances For