TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.DecimalInterchange.Queries.Runtime

Decimal classification and quantum queries #

The predicates of IEEE 754-2019 §§5.7.2–5.7.3 are non-signaling, including on signaling NaNs. Normality depends on numerical magnitude, not coefficient length: different members of one cohort have the same classification. quantumExponent is an additional finite-datum query, not an IEEE operation name. Canonicality belongs to the stored word because decoding accepts redundant words.

source
@[reducible, inline]
abbrev FloatLib.Floats.Formats.DecimalInterchange.Class :
Type

Decimal classification uses the shared ten IEEE floating-point classes.

Instances For
    source
    def FloatLib.Floats.Formats.DecimalInterchange.Datum.isFinite :
    Datum → Bool

    Finiteness includes either sign of zero.

    Instances For
      source
      def FloatLib.Floats.Formats.DecimalInterchange.Datum.isZero :
      Datum → Bool

      Test numerical zero, independently of its sign and quantum.

      Instances For
        source
        def FloatLib.Floats.Formats.DecimalInterchange.Datum.isInfinite :
        Datum → Bool

        Test either signed infinity.

        Instances For
          source
          def FloatLib.Floats.Formats.DecimalInterchange.Datum.isNaN :
          Datum → Bool

          Test either signaling or quiet NaN.

          Instances For
            source
            def FloatLib.Floats.Formats.DecimalInterchange.Datum.isNormal (f : Format) :
            Datum → Bool

            A finite value is normal when its magnitude reaches the format's normal threshold.

            Instances For
              source
              def FloatLib.Floats.Formats.DecimalInterchange.Datum.isSubnormal (f : Format) :
              Datum → Bool

              A subnormal is nonzero and smaller in magnitude than the normal threshold.

              Instances For
                source
                def FloatLib.Floats.Formats.DecimalInterchange.Datum.classify (f : Format) :
                Datum → Class

                Classify a datum without changing it or raising invalid on a signaling NaN.

                Instances For
                  source
                  def FloatLib.Floats.Formats.DecimalInterchange.Datum.quantumExponent :
                  Datum → Option ℤ

                  Return a finite datum's stored quantum exponent; special values return none.

                  Instances For
                    source
                    def FloatLib.Floats.Formats.DecimalInterchange.Datum.sameQuantum :
                    Datum → Datum → Bool

                    Equal finite quanta, or two infinities, or two NaNs, as specified by §5.7.3. Signs, coefficients and NaN signaling bits are immaterial.

                    Instances For
                      source
                      def FloatLib.Floats.Formats.DecimalInterchange.Datum.radix :
                      Datum → ℕ

                      The decimal radix, including for a special operand.

                      Instances For
                        source
                        def FloatLib.Floats.Formats.DecimalInterchange.Encoding.isCanonical (encoding : Encoding) (f : Format) (w : BitVec f.bitWidth) :
                        Bool

                        Test canonical storage, including redundant DPD declets, oversized BID coefficients and ignored infinity/NaN bits. Decoding alone cannot distinguish these representations.

                        Instances For