TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.DecimalInterchange.Codec.Runtime

Decimal word assembly and special values #

IEEE 754-2019 §3.5.2 reserves combination fields 11110 for infinity and 11111 for NaN in both encodings. The next bit is one for a signaling NaN. Canonical encodings clear unused bits. A decoder accepts every word, retaining the sign and the NaN's signaling bit and decimal payload.

Codec separates these shared rules from BID/DPD coefficient encoding. encode? rejects unrepresentable datums; it does not round them.

source
def FloatLib.Floats.Formats.DecimalInterchange.Bits.pack (f : Format) (negative : Bool) (payload : ℕ) :
BitVec f.bitWidth

Assemble a sign and the remaining bits into an exact-width interchange word.

Instances For
    source
    def FloatLib.Floats.Formats.DecimalInterchange.Bits.negative (f : Format) (word : BitVec f.bitWidth) :
    Bool

    Read the sign bit.

    Instances For
      source
      def FloatLib.Floats.Formats.DecimalInterchange.Bits.payload (f : Format) (word : BitVec f.bitWidth) :
      ℕ

      Read all bits below the sign.

      Instances For
        source
        structure FloatLib.Floats.Formats.DecimalInterchange.Codec :
        Type

        Executable coefficient encodings, separated from their laws in Codec.Proof. Finite decoding returns (coefficient, biasedExponent).

        • encodeFinite : Format → ℕ → ℕ → ℕ

          Pack a finite coefficient and biased exponent into the unsigned payload.

        • decodeFinite : Format → ℕ → ℕ × ℕ

          Recover a finite coefficient and biased exponent from the unsigned payload.

        • encodePayload : Format → ℕ → ℕ

          Encode the diagnostic payload of a NaN.

        • decodePayload : Format → ℕ → ℕ

          Decode the diagnostic payload of a NaN.

        Instances For
          source
          def FloatLib.Floats.Formats.DecimalInterchange.Codec.encode (codec : Codec) (f : Format) :
          Datum → BitVec f.bitWidth

          Assemble a datum without rounding. Correct round trips require Datum.Valid; use encode? when representability has not already been established.

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

            Checked interchange encoding. none means that this width cannot represent the supplied datum exactly, including its quantum exponent or NaN payload.

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

              Decode every interchange word, accepting the noncanonical encodings specified by IEEE 754-2019 §3.5.2.

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

                Re-encode a decoded datum, clearing unused special-value bits and replacing redundant significand encodings by their canonical representatives.

                Instances For