TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Operations.Runtime

Standard operations for configured binary values #

These definitions expose the descriptor-generic operation model on the ordinary ExecFloat.Binary carrier. They add no arithmetic implementation and preserve exception status exactly across the packing boundary.

The definitions call the descriptor-model operations through the storage codec. The companion proof module shows that packing changes neither values nor flags.

source
@[inline]
def FloatLib.Floats.ExecFloat.Binary.remainder {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (dividend divisor : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

IEEE remainder, using a nearest-even integral quotient for finite operands.

Instances For
    source
    @[inline]
    def FloatLib.Floats.ExecFloat.Binary.remainderWithStatus {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (dividend divisor : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
    IEEEOutcome

    IEEE remainder together with its exception indicators.

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

      Round to an integer and encode it in the selected direction. A custom finite-only format can saturate; use roundToIntegralExactWithStatus to detect that overflow.

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

        Round to an integer, encode it in the same direction, and report fractional loss or overflow.

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

          Multiply a configured value by 2^scale and round in the selected direction.

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

            Power-of-two scaling with the IEEE exception indicators.

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

              Return the leading binary exponent in the same configured format.

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

                Return the leading binary exponent and its IEEE exception indicators.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.ExecFloat.Binary.copySign {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (magnitude signSource : ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)) :
                  ExecFloat (Formats.BinaryInterchange.Configured.Family format code plan)

                  Copy the numerical sign of signSource onto magnitude.

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

                    Absolute value under the configured encoding policy.

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

                      Next representable configured value in the positive direction.

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

                        Next representable configured value in the negative direction.

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

                          IEEE-2008-style minNum, retaining the numeric operand against one quiet NaN.

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

                            IEEE-2008-style maxNum, retaining the numeric operand against one quiet NaN.

                            Instances For