TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.DecimalInterchange.DPD.Runtime

Densely packed decimal interchange encoding #

IEEE 754-2019 §3.5.2(c)(1) combines the leading decimal digit and the high exponent bits in a five-bit combination field. The remaining digits use Cowlishaw declets. All redundant declets decode; encoding chooses the canonical representation.

source
def FloatLib.Floats.Formats.DecimalInterchange.DPD.combination (leading highExponent : ℕ) :
ℕ

Combine a leading digit with the high two exponent bits.

Instances For
    source
    def FloatLib.Floats.Formats.DecimalInterchange.DPD.leadingDigit (field : ℕ) :
    ℕ

    Leading digit extracted from a finite combination field (field < 30).

    Instances For
      source
      def FloatLib.Floats.Formats.DecimalInterchange.DPD.highExponent (field : ℕ) :
      ℕ

      High exponent bits extracted from a finite combination field.

      Instances For
        source
        def FloatLib.Floats.Formats.DecimalInterchange.DPD.encodeFields (f : Format) (leading exponent trailing : ℕ) :
        ℕ

        Assemble the leading digit, biased exponent, and already-packed trailing declets.

        Instances For
          source
          def FloatLib.Floats.Formats.DecimalInterchange.DPD.encodeFinite (f : Format) (c e : ℕ) :
          ℕ

          Encode a finite decimal coefficient and biased exponent.

          Instances For
            source
            def FloatLib.Floats.Formats.DecimalInterchange.DPD.decodeFinite (f : Format) (n : ℕ) :
            ℕ × ℕ

            Decode a finite word, accepting every trailing declet.

            Instances For
              source
              def FloatLib.Floats.Formats.DecimalInterchange.DPD.codec :
              Codec

              The complete DPD interchange codec. Its laws are proved in DPD.Proof.

              Instances For
                source
                def FloatLib.Floats.Formats.DecimalInterchange.DPD.decode (f : Format) (word : BitVec f.bitWidth) :
                Datum

                Decode a DPD word at the selected interchange layout, including redundant declets.

                Instances For
                  source
                  def FloatLib.Floats.Formats.DecimalInterchange.DPD.encode? (f : Format) (d : Datum) :
                  Option (BitVec f.bitWidth)

                  Encode a datum exactly as DPD, rejecting unrepresentable inputs without rounding.

                  Instances For
                    source
                    def FloatLib.Floats.Formats.DecimalInterchange.DPD.canonicalize (f : Format) (word : BitVec f.bitWidth) :
                    BitVec f.bitWidth

                    Replace redundant declets and unused special bits by their canonical encodings.

                    Instances For