TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

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

Bounded fixed-point conversion runtime #

Bounded fixed point offers three overflow policies. reject returns outOfRange, wrap reduces the rounded coefficient modulo 2 ^ width, and saturate clamps it to the signed range. Conversion.Instances installs checked conversion as the context-free default.

source
inductive FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.OverflowPolicy :
Type

Overflow policy for conversion into bounded fixed point.

  • reject : OverflowPolicy

    Reject a rounded coefficient outside the signed destination range.

  • wrap : OverflowPolicy

    Reduce the rounded coefficient modulo 2 ^ width.

  • saturate : OverflowPolicy

    Clamp the rounded coefficient to the signed destination range.

Instances For
    source
    @[instance_reducible]
    instance FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.instDecidableEqOverflowPolicy :
    DecidableEq OverflowPolicy
    source
    def FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.instReprOverflowPolicy.repr :
    OverflowPolicy → ℕ → Std.Format
    Instances For
      source
      @[instance_reducible]
      instance FloatLib.Floats.ExecFloat.BoundedFixedPoint.Conversion.instReprOverflowPolicy :
      Repr OverflowPolicy
      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 complete rational observation under an explicit 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 canonically to their exact stored rational.