TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.DecimalInterchange.Formatting.Words

Decimal character conversion for BID and DPD words #

The encoding and width select only the source/destination codec. Parsing, precision rounding, and status handling use the shared datum operations. Exact output followed by input recovers the canonical word: redundant encodings are not character-level representation information.

source
structure FloatLib.Floats.Formats.DecimalInterchange.Formatting.WordOutcome (f : Format) :
Type

An encoded decimal result and the five conversion flags.

  • word : BitVec f.bitWidth

    The result encoded in the selected BID or DPD layout.

  • status : Status

    IEEE exception indicators raised by character conversion.

Instances For
    source
    def FloatLib.Floats.Formats.DecimalInterchange.Formatting.instDecidableEqWordOutcome.decEq {f✝ : Format} (x✝ x✝¹ : WordOutcome f✝) :
    Decidable (x✝ = x✝¹)
    Instances For
      source
      @[instance_reducible]
      instance FloatLib.Floats.Formats.DecimalInterchange.Formatting.instDecidableEqWordOutcome {f✝ : Format} :
      DecidableEq (WordOutcome f✝)
      source
      @[instance_reducible]
      instance FloatLib.Floats.Formats.DecimalInterchange.Formatting.instReprWordOutcome {f✝ : Format} :
      Repr (WordOutcome f✝)
      source
      def FloatLib.Floats.Formats.DecimalInterchange.Formatting.instReprWordOutcome.repr {f✝ : Format} :
      WordOutcome f✝ → ℕ → Std.Format
      Instances For
        source
        def FloatLib.Floats.Formats.DecimalInterchange.Formatting.parseWord (encoding : Encoding) (f : Format) (mode : RoundingMode) (text : String) :
        WordOutcome f

        Parse and round once, then encode the valid result as BID or DPD.

        Instances For
          source
          def FloatLib.Floats.Formats.DecimalInterchange.Formatting.formatWord (encoding : Encoding) (f : Format) (mode : RoundingMode) (precision : Precision) (word : BitVec f.bitWidth) :
          TextOutcome

          Decode a word and apply the requested decimal output precision.

          Instances For
            source
            theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.decode_parseWord (encoding : Encoding) (f : Format) (mode : RoundingMode) (text : String) :
            encoding.decode f (parseWord encoding f mode text).word = (parse f mode text).value

            The word parser encodes precisely the datum parser's result, including special fields.

            source
            @[simp]
            theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.parseWord_status (encoding : Encoding) (f : Format) (mode : RoundingMode) (text : String) :
            (parseWord encoding f mode text).status = (parse f mode text).status

            Encoding introduces no additional flags.

            source
            theorem FloatLib.Floats.Formats.DecimalInterchange.Formatting.parseWord_formatWord_exact (encoding : Encoding) (f : Format) (outputMode inputMode : RoundingMode) (word : BitVec f.bitWidth) :
            parseWord encoding f inputMode (formatWord encoding f outputMode Numerics.DecimalText.Precision.exact word).text = { word := encoding.canonicalize f word }

            Exact text roundtrips every word to its canonical representative, in any pair of modes.