TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Reduction.Runtime

Correctly rounded reductions for configured binary values #

These functions lift the format-generic reduction kernel to the ordinary configured ExecFloat.Binary carrier. Operands are decoded into the exact model, reduced there, and the single final result is packed back into the configured carrier.

For finite operands, sum forms the exact mathematical sum and rounds once. dot forms every product exactly, sums those products exactly, and rounds once. The configured type fixes the source and destination format, while the rounding direction remains an explicit argument.

source
def FloatLib.Floats.ExecFloat.Binary.sumWithStatus {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (values : Array (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) :
IEEEOutcome

Correctly sum configured values and return the result with IEEE exception indicators.

Every operand is decoded exactly, the complete sum is accumulated without intermediate rounding, and the result is rounded once in rounding.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Binary.sum {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (values : Array (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) :
    ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

    Correctly sum configured values with one final rounding.

    Instances For
      source
      @[inline]
      def FloatLib.Floats.ExecFloat.Binary.sumListWithStatus {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (values : List (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) :
      IEEEOutcome

      List entry point for correctly rounded configured summation with status.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.ExecFloat.Binary.sumList {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (values : List (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) :
        ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

        List entry point for correctly rounded configured summation.

        Instances For
          source
          def FloatLib.Floats.ExecFloat.Binary.dotWithStatus {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : Array (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) :
          Except Numerics.ReductionError IEEEOutcome

          Correctly compute a configured dot product and return IEEE exception indicators.

          Products and their sum are exact until one final rounding. Unequal lengths return ReductionError.lengthMismatch; no pair is silently discarded.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.ExecFloat.Binary.dot {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : Array (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) :
            Except Numerics.ReductionError (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

            Correctly compute a configured dot product with one final rounding.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.ExecFloat.Binary.dotListWithStatus {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : List (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) :
              Except Numerics.ReductionError IEEEOutcome

              List entry point for a correctly rounded configured dot product with status.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.ExecFloat.Binary.dotList {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : List (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))) (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) :
                Except Numerics.ReductionError (ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan))

                List entry point for a correctly rounded configured dot product.

                Instances For