TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Bounded fixed-point conversion runtime #

Conversion into bounded fixed point takes the OverflowPolicy of its arithmetic as its context: reject returns outOfRange, wrap reduces the rounded coefficient modulo 2 ^ width, and saturate clamps it to the signed range. Conversion.Instances installs reject as the context-free default.

source
@[inline]
def FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.coefficientInRange {radix : Numerics.Radix} {fractionalDigits width : ℕ} (exact : ℚ) :
Bool

Whether the ties-to-even rounded coefficient fits the signed destination width.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.finiteStatus {radix : Numerics.Radix} {fractionalDigits width : ℕ} (policy : OverflowPolicy) (exact : ℚ) (rounded : BoundedFixedPoint radix fractionalDigits width) :
    ConversionStatus

    Status for a delivered bounded fixed-point conversion.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.quantizeFinite {radix : Numerics.Radix} {fractionalDigits width : ℕ} (policy : OverflowPolicy) (exact : ℚ) :
      ConversionOutcome (BoundedFixedPoint radix fractionalDigits width)

      Quantize one finite rational according to the named bounded-overflow policy.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.run {radix : Numerics.Radix} {fractionalDigits width : ℕ} (policy : OverflowPolicy) :
        Numerics.NumericalValue ℚ → ConversionOutcome (BoundedFixedPoint radix fractionalDigits width)

        Convert a rational observation, finite or not, under a bounded-overflow policy.

        Instances For
          source
          def FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.coefficientSpec {radix : Numerics.Radix} {fractionalDigits width : ℕ} (policy : OverflowPolicy) (exact : ℚ) (stored : ℤ) :
          Prop

          The signed output coefficient after nearest-even rounding and the selected overflow policy.

          The wrapping relation uses centered integer reduction, and saturation uses the signed range endpoints. Neither clause refers to a fixed-width encoding kernel.

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

            Conversion relates the delivered coefficient to integer rounding, range, wrap, and clamp.

            The status is retained in full. Rejection of a finite input occurs exactly when the nearest-even coefficient is out of range under reject. The other policies always deliver a value.

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

              Bounded fixed-point values decode to their exact stored rational.