TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.FixedPoint.Configured.Conversion.Runtime

Exact fixed-point conversion runtime #

An unbounded configured fixed-point destination has no overflow and no exceptional values. Every finite rational is rounded once to the nearest grid coefficient, with ties to even. Infinity and exceptional observations are rejected because the representation has no corresponding code.

Proofs of the reduction equations live in Conversion.Proof; destination capability instances live in Conversion.Instances.

source
@[inline]
def FloatLib.Floats.ExecFloat.FixedPoint.Conversion.run {radix : Numerics.Radix} {fractionalDigits : ℕ} (_context : Unit) :
Numerics.NumericalValue ℚ → ConversionOutcome (FixedPoint radix fractionalDigits)

Quantize one complete rational observation into an unbounded fixed-point grid.

Instances For
    source
    def FloatLib.Floats.ExecFloat.FixedPoint.Conversion.spec {radix : Numerics.Radix} {fractionalDigits : ℕ} :
    Numerics.Quantization.Spec Unit (Numerics.NumericalValue ℚ) (ConversionOutcome (FixedPoint radix fractionalDigits))

    The stored coefficient is nearest-even on the scaled integer grid, with exact status.

    The half-unit bound and even-tie rule are numerical predicates on the delivered coefficient. The coefficient equality also retains the unique complete code chosen by the integer rounder. Infinity and exceptional observations retain their complete rejection reasons.

    Instances For
      source
      @[instance_reducible]
      instance FloatLib.Floats.ExecFloat.FixedPoint.Conversion.exactDecoder {radix : Numerics.Radix} {fractionalDigits : ℕ} :
      ExactDecoder (FixedPoint radix fractionalDigits) ℚ

      Exact fixed-point values decode canonically to rational observations.