TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.FixedPoint.Configured.Runtime

Executable exact fixed-point operations #

Same-scale addition, negation, and subtraction are exact. Multiplication composes the two scales in its result type rather than silently selecting a rounding policy.

source
@[reducible, inline]
abbrev FloatLib.Floats.ExecFloat.FixedPoint.scale (radix : Numerics.Radix) (fractionalDigits : ℕ) :
ℕ

Integer denominator of the configured fixed-point grid.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.FixedPoint.ofCode {radix : Numerics.Radix} {fractionalDigits : ℕ} (code : Formats.FixedPoint.Code radix fractionalDigits) :
    FixedPoint radix fractionalDigits

    Wrap a complete fixed-point code without conversion.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.ExecFloat.FixedPoint.toCode {radix : Numerics.Radix} {fractionalDigits : ℕ} (value : FixedPoint radix fractionalDigits) :
      Formats.FixedPoint.Code radix fractionalDigits

      Recover the complete fixed-point code without conversion.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.ExecFloat.FixedPoint.ofCoefficient {radix : Numerics.Radix} {fractionalDigits : ℕ} (coefficient : ℤ) :
        FixedPoint radix fractionalDigits

        Construct a value from its exact stored integer coefficient.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.ExecFloat.FixedPoint.roundRat {radix : Numerics.Radix} {fractionalDigits : ℕ} (value : ℚ) :
          FixedPoint radix fractionalDigits

          Round an exact rational once to the nearest fixed-point grid value, breaking ties to even.

          This is the construction policy used by decimal and scientific literals. It never converts through a host floating-point value.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.ExecFloat.FixedPoint.coefficient {radix : Numerics.Radix} {fractionalDigits : ℕ} (value : FixedPoint radix fractionalDigits) :
            ℤ

            Recover the exact stored integer coefficient.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.ExecFloat.FixedPoint.toRat {radix : Numerics.Radix} {fractionalDigits : ℕ} (value : FixedPoint radix fractionalDigits) :
              ℚ

              Decode a configured fixed-point value to its exact rational meaning.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.ExecFloat.FixedPoint.add {radix : Numerics.Radix} {fractionalDigits : ℕ} (left right : FixedPoint radix fractionalDigits) :
                FixedPoint radix fractionalDigits

                Exact same-scale addition.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.ExecFloat.FixedPoint.neg {radix : Numerics.Radix} {fractionalDigits : ℕ} (value : FixedPoint radix fractionalDigits) :
                  FixedPoint radix fractionalDigits

                  Exact additive inverse at the same scale.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Floats.ExecFloat.FixedPoint.sub {radix : Numerics.Radix} {fractionalDigits : ℕ} (left right : FixedPoint radix fractionalDigits) :
                    FixedPoint radix fractionalDigits

                    Exact same-scale subtraction.

                    Instances For
                      source
                      @[inline]
                      def FloatLib.Floats.ExecFloat.FixedPoint.mul {radix : Numerics.Radix} {p q : ℕ} (left : FixedPoint radix p) (right : FixedPoint radix q) :
                      FixedPoint radix (p + q)

                      Exact multiplication with the composed output scale visible in the result type.

                      Instances For