TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Info.Profile

Inspection profiles for binary-interchange formats #

Representation, exceptional values, rounding rules, and theorem groups used by #float_info. Info.Command resolves the carrier and supplies its storage and execution details. Complex and interval profiles also use inspectSummary to read their component descriptor.

Each theorem group states its scope. Applicability distinguishes destination-only IEEE contracts from contracts requiring IEEE encodings on both sides of a cast.

source
structure FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.Summary :
Type

Closed descriptor data extracted by the #float_info elaborator.

  • expWidth : ℕ

    Number of stored exponent bits.

  • fracWidth : ℕ

    Number of stored fraction bits.

  • exponentBias : ℕ

    Bias subtracted from a stored normal exponent.

  • encoding : FloatFormat.Encoding

    Exceptional-value encoding policy.

  • bitWidth : ℕ

    Total encoded width, including the sign bit.

  • minNormalExponent : ℤ

    Smallest unbiased exponent of a normal value.

  • maxNormalExponent : ℤ

    Largest unbiased exponent of a finite normal value.

  • isIEEE : Bool

    Whether the descriptor uses the conventional IEEE bias and exceptional-value encoding.

Instances For
    source
    def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.inspectSummary (format : Lean.Expr) :
    Lean.MetaM Summary

    Read the descriptor fields used by scalar, complex, and interval reports.

    Instances For
      source
      def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.encodingName :
      FloatFormat.Encoding → String

      Human-readable name of a binary exceptional-value policy.

      Instances For
        source
        def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.standardName (summary : Summary) :
        String

        Name the standard IEEE layouts. Other IEEE-style widths get a general label.

        Instances For
          source
          def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.nanDescription (encoding : FloatFormat.Encoding) :
          String

          Precise NaN population and metadata retained by an encoding policy.

          Instances For
            source
            def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.signalingNaNDescription (encoding : FloatFormat.Encoding) (fracWidth : ℕ) :
            String

            Whether the encoding has a signaling NaN. IEEE signaling NaNs require a nonzero fraction with a clear quiet bit, so at least one fraction bit must lie below the quiet bit.

            Instances For
              source
              def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.ieeeApplicability (summary : Summary) :
              ExecFloat.TheoremApplicability

              Descriptor-level applicability of theorem families specialized to conventional IEEE layouts.

              Instances For
                source
                def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.ieeeCrossFormatApplicability (summary : Summary) :
                ExecFloat.TheoremApplicability

                Applicability of a cross-format IEEE theorem when the inspected descriptor may occupy either side.

                Instances For
                  source
                  def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.finiteOnlyApplicability (summary : Summary) :
                  ExecFloat.TheoremApplicability

                  Applicability of the all-words-finite range-limited enclosure theorems.

                  Instances For
                    source
                    def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.integralApplicability (summary : Summary) :
                    ExecFloat.TheoremApplicability

                    Applicability of integral rounding when every neighboring integer fits the format range.

                    Instances For
                      source
                      def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.sixDigits (significand : ℕ) (exponent : ℤ) :
                      Option String

                      Six significant decimal digits of the positive dyadic significand * 2 ^ exponent, as 3.40282e38, computed exactly and rounded half up. It is none for zero or an exponent of magnitude beyond a million, whose expansion would be slow.

                      Instances For
                        source
                        def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.withApproximation (exact : String) (significand : ℕ) (exponent : ℤ) :
                        String

                        An exact text with the six-digit decimal approximation of a dyadic, when one is cheap.

                        Instances For
                          source
                          def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.twoPower (exponent : ℤ) :
                          String

                          A power of two 2 ^ exponent with its decimal approximation.

                          Instances For
                            source
                            def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.largestFinite (summary : Summary) :
                            String

                            The largest finite value, (2 - 2 ^ -k) * 2 ^ maxNormalExponent, where k is the fraction width, or k - 1 when the all-ones fraction at the top exponent is a NaN.

                            Instances For
                              source
                              def FloatLib.Floats.Formats.BinaryInterchange.FloatInfo.profile (summary : Summary) (standard storage : String) (executionIdentity : List ExecFloat.InfoEntry) :
                              ExecFloat.FormatProfile

                              Build the complete user-facing inspection profile for a binary descriptor.

                              Instances For