TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.FixedPoint.Exact.Runtime

Exact fixed-point representation and execution #

The code stores an unbounded integer coefficient with its radix and fractional precision in the type. Its exact rational decoder and coefficient operations are defined together here: addition, subtraction, and negation keep the scale; multiplication composes the two operand scales.

No operation rounds or overflows. Exact.Proof defines the rational numerical system and proves these operations refine exact arithmetic. Bounded coefficient policies live in FixedPoint.Bounded.

source
@[inline]
def FloatLib.Floats.Formats.FixedPoint.scale (radix : Numerics.Radix) (fractionalDigits : ℕ) :
ℕ

Natural denominator of a fixed-point grid with the given radix and fractional precision.

Instances For
    source
    structure FloatLib.Floats.Formats.FixedPoint.Code (radix : Numerics.Radix) (fractionalDigits : ℕ) :
    Type

    An integer coefficient interpreted with fractionalDigits radix digits after the point.

    • coefficient : ℤ

      Signed integer numerator before division by radix.base ^ fractionalDigits.

    Instances For
      source
      def FloatLib.Floats.Formats.FixedPoint.instDecidableEqCode.decEq {radix✝ : Numerics.Radix} {fractionalDigits✝ : ℕ} (x✝ x✝¹ : Code radix✝ fractionalDigits✝) :
      Decidable (x✝ = x✝¹)
      Instances For
        source
        @[instance_reducible]
        instance FloatLib.Floats.Formats.FixedPoint.instDecidableEqCode {radix✝ : Numerics.Radix} {fractionalDigits✝ : ℕ} :
        DecidableEq (Code radix✝ fractionalDigits✝)
        source
        @[instance_reducible]
        instance FloatLib.Floats.Formats.FixedPoint.instReprCode {radix✝ : Numerics.Radix} {fractionalDigits✝ : ℕ} :
        Repr (Code radix✝ fractionalDigits✝)
        source
        def FloatLib.Floats.Formats.FixedPoint.instReprCode.repr {radix✝ : Numerics.Radix} {fractionalDigits✝ : ℕ} :
        Code radix✝ fractionalDigits✝ → ℕ → Std.Format
        Instances For

          Executable operations #

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

          Exact rational value of a fixed-point code.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.FixedPoint.Code.ofInt (radix : Numerics.Radix) (fractionalDigits : ℕ) (coefficient : ℤ) :
            Code radix fractionalDigits

            Encode an integer coefficient directly.

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

              Exact addition of fixed-point values with a common scale.

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

                Exact additive inverse at the same scale.

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

                  Exact subtraction at a common scale.

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

                    Exact multiplication. Multiplying scales p and q produces scale p + q; no hidden rescaling or rounding occurs.

                    Instances For