TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.Runtime

Mixed-format P3109 arithmetic #

The source types select exact decoders and finite values are embedded into Rat, so a configured IEEE accumulator, a P3109 operand, and an exact rational can occur in one expression. IEEE negative zero loses its sign in this domain, as required by §4.8.1. Every exceptional observation becomes the report's one NaN.

Destination supplies the final report projection. Destination.p3109 selects any P3109 descriptor. External destinations live in Arithmetic.External, so importing this module installs no alternative IEEE arithmetic or conversion instances. The operation always evaluates the whole closed expression before projecting, including fused add-add and scaled arithmetic.

Reference: P3109 unapproved interim report 4.0.3, revision 34f5964, §§4.5, 4.8–4.10 and 5.8.

source
def FloatLib.Floats.Formats.P3109.Arithmetic.canonical :
Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ

Canonicalize exceptions to the report's sole NaN datum.

Instances For
    source
    structure FloatLib.Floats.Formats.P3109.Arithmetic.Destination (Result : Type) :
    Type

    A final report projection, kept apart from ordinary destination conversion.

    Instances For
      source
      def FloatLib.Floats.Formats.P3109.Arithmetic.Destination.p3109 (format : Format) :
      Destination (ExecFloat.P3109 format)

      A P3109 result format with its complete report projection policy.

      Instances For
        source
        @[inline]
        def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.decode {Source SourceExact : Type} [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (value : Source) :
        Numerics.NumericalValue ℚ

        Decode through the source's exact interface and discard IEEE zero signs and NaN metadata.

        Instances For
          source
          @[inline]
          def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.convert {Source SourceExact Result : Type} [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (destination : Destination Result) (value : Source) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
          Result

          Conversion from an independently typed source through one destination projection, rounding in mode (nearest-even by default) before saturation (none by default) applies.

          Instances For
            source
            @[inline]
            def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.unary {Source SourceExact Result : Type} [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (destination : Destination Result) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (value : Source) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
            Result

            Apply a closed unary operation before the destination projection.

            Instances For
              source
              @[inline]
              def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.binary {Left LeftExact Right RightExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] (destination : Destination Result) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : Left) (right : Right) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
              Result

              Apply a closed binary operation to independently typed operands, then project once.

              Instances For
                source
                @[inline]
                def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.ternary {Left LeftExact Right RightExact Third ThirdExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] [ExecFloat.ExactDecoder Third ThirdExact] [ExecFloat.ExactMap ThirdExact ℚ] (destination : Destination Result) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : Left) (right : Right) (third : Third) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
                Result

                Evaluate a complete ternary closed expression before the sole destination projection.

                Instances For
                  source
                  @[inline]
                  def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.recip {Source SourceExact Result : Type} [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] (destination : Destination Result) (value : Source) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
                  Result

                  Mixed reciprocal, with zero mapped to NaN before projection.

                  Instances For
                    source
                    @[inline]
                    def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.add {Left LeftExact Right RightExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] (destination : Destination Result) (left : Left) (right : Right) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
                    Result

                    Mixed addition, retaining closed-domain infinities and NaN.

                    Instances For
                      source
                      @[inline]
                      def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.sub {Left LeftExact Right RightExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] (destination : Destination Result) (left : Left) (right : Right) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
                      Result

                      Mixed subtraction with no intermediate rounding.

                      Instances For
                        source
                        @[inline]
                        def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.mul {Left LeftExact Right RightExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] (destination : Destination Result) (left : Left) (right : Right) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
                        Result

                        Mixed multiplication with no intermediate rounding.

                        Instances For
                          source
                          @[inline]
                          def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.div {Left LeftExact Right RightExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] (destination : Destination Result) (left : Left) (right : Right) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
                          Result

                          Mixed division with the report's zero-denominator rule.

                          Instances For
                            source
                            @[inline]
                            def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.fma {Left LeftExact Right RightExact Third ThirdExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] [ExecFloat.ExactDecoder Third ThirdExact] [ExecFloat.ExactMap ThirdExact ℚ] (destination : Destination Result) (left : Left) (right : Right) (addend : Third) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
                            Result

                            Mixed fused multiply-add, including an independently typed accumulator.

                            Instances For
                              source
                              @[inline]
                              def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.faa {Left LeftExact Right RightExact Third ThirdExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] [ExecFloat.ExactDecoder Third ThirdExact] [ExecFloat.ExactMap ThirdExact ℚ] (destination : Destination Result) (left : Left) (middle : Right) (right : Third) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
                              Result

                              Mixed fused add-add, with neither addition rounded before the result projection.

                              Instances For
                                source
                                @[inline]
                                def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.scaledBinary {Left LeftExact Right RightExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] {LeftScale LeftScaleExact RightScale RightScaleExact : Type} [ExecFloat.ExactDecoder LeftScale LeftScaleExact] [ExecFloat.ExactMap LeftScaleExact ℚ] [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] (destination : Destination Result) (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (leftScale : LeftScale) (left : Left) (rightScale : RightScale) (right : Right) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
                                Result

                                Scaled binary operation from §5.8, with an implicit exact result scale of one.

                                Input scaling is closed multiplication: a zero scale times infinity is NaN, and a NaN scale propagates even when its element is zero. The complete scaled expression is projected once.

                                Instances For
                                  source
                                  @[inline]
                                  def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.scaledAdd {Left LeftExact Right RightExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] {LeftScale LeftScaleExact RightScale RightScaleExact : Type} [ExecFloat.ExactDecoder LeftScale LeftScaleExact] [ExecFloat.ExactMap LeftScaleExact ℚ] [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] (destination : Destination Result) (leftScale : LeftScale) (left : Left) (rightScale : RightScale) (right : Right) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
                                  Result

                                  Add two exactly scaled operands and project once.

                                  Instances For
                                    source
                                    @[inline]
                                    def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.scaledSub {Left LeftExact Right RightExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] {LeftScale LeftScaleExact RightScale RightScaleExact : Type} [ExecFloat.ExactDecoder LeftScale LeftScaleExact] [ExecFloat.ExactMap LeftScaleExact ℚ] [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] (destination : Destination Result) (leftScale : LeftScale) (left : Left) (rightScale : RightScale) (right : Right) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
                                    Result

                                    Subtract two exactly scaled operands and project once.

                                    Instances For
                                      source
                                      @[inline]
                                      def FloatLib.Floats.Formats.P3109.Arithmetic.Mixed.scaledMul {Left LeftExact Right RightExact Result : Type} [ExecFloat.ExactDecoder Left LeftExact] [ExecFloat.ExactMap LeftExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] {LeftScale LeftScaleExact RightScale RightScaleExact : Type} [ExecFloat.ExactDecoder LeftScale LeftScaleExact] [ExecFloat.ExactMap LeftScaleExact ℚ] [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] (destination : Destination Result) (leftScale : LeftScale) (left : Left) (rightScale : RightScale) (right : Right) (mode : RoundingMode := RoundingMode.nearest) (saturation : SaturationMode := SaturationMode.none) :
                                      Result

                                      Multiply two exactly scaled operands and project once.

                                      Instances For