TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.BinaryInterchange.Configured.Formatting

External character output for configured binary values #

Storage selection affects neither the characters nor the exception indicators. The descriptor model supplies the shared decimal and hexadecimal algorithms.

source
def FloatLib.Floats.ExecFloat.Binary.formatWithStatus {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) (radix : Formats.BinaryInterchange.Model.TextRadix) (precision : Formats.BinaryInterchange.Model.TextPrecision) (value : ExecFloat (Formats.BinaryInterchange.Configured.Family fmt code plan)) :
Formats.BinaryInterchange.Model.TextOutcome

Decimal or hexadecimal output at exact or requested precision, including rounding status.

Instances For
    source
    def FloatLib.Floats.ExecFloat.Binary.formatDecimal {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family fmt code plan)) :
    String

    Exact decimal output, preserving the sign and diagnostic information of special values.

    Instances For
      source
      def FloatLib.Floats.ExecFloat.Binary.formatHex {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family fmt code plan)) :
      String

      Exact hexadecimal output with an integral significand and a decimal binary exponent.

      Instances For
        source
        def FloatLib.Floats.ExecFloat.Binary.formatDecimalWithStatus {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) (style : Formats.BinaryInterchange.Model.DecimalStyle) (value : ExecFloat (Formats.BinaryInterchange.Configured.Family fmt code plan)) :
        Formats.BinaryInterchange.Model.TextOutcome

        Fixed or scientific decimal output, with explicit rounding and exception status.

        Instances For
          source
          def FloatLib.Floats.ExecFloat.Binary.formatFixed {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family fmt code plan)) (places : ℕ) :
          String

          Nearest-even fixed output with exactly places digits after the decimal point.

          Instances For
            source
            def FloatLib.Floats.ExecFloat.Binary.formatScientific {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (value : ExecFloat (Formats.BinaryInterchange.Configured.Family fmt code plan)) (places : ℕ) :
            String

            Nearest-even scientific output with places + 1 significant digits.

            Instances For
              source
              @[simp]
              theorem FloatLib.Floats.ExecFloat.Binary.formatDecimalWithStatus_ofModel {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) (style : Formats.BinaryInterchange.Model.DecimalStyle) (value : Formats.BinaryInterchange.Model fmt) :
              formatDecimalWithStatus rounding style (ofModel value) = Formats.BinaryInterchange.Model.formatDecimalWithStatus rounding style value

              Decimal notation and its status flags are independent of the storage representation.

              source
              @[simp]
              theorem FloatLib.Floats.ExecFloat.Binary.formatFixed_ofModel {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (value : Formats.BinaryInterchange.Model fmt) (places : ℕ) :
              formatFixed (ofModel value) places = value.formatFixed places

              Repacking a value does not change fixed decimal output.

              source
              @[simp]
              theorem FloatLib.Floats.ExecFloat.Binary.formatScientific_ofModel {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (value : Formats.BinaryInterchange.Model fmt) (places : ℕ) :
              formatScientific (ofModel value) places = value.formatScientific places

              Repacking a value does not change scientific decimal output.

              source
              @[simp]
              theorem FloatLib.Floats.ExecFloat.Binary.formatWithStatus_ofModel {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (rounding : Formats.BinaryInterchange.Model.IEEERoundingMode) (radix : Formats.BinaryInterchange.Model.TextRadix) (precision : Formats.BinaryInterchange.Model.TextPrecision) (value : Formats.BinaryInterchange.Model fmt) :
              formatWithStatus rounding radix precision (ofModel value) = Formats.BinaryInterchange.Model.formatWithStatus rounding radix precision value

              Configured precision output is identical to descriptor-model output, including status.

              source
              @[simp]
              theorem FloatLib.Floats.ExecFloat.Binary.formatDecimal_ofModel {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (value : Formats.BinaryInterchange.Model fmt) :
              formatDecimal (ofModel value) = value.formatDecimal

              Repacking a model word leaves its exact decimal output unchanged.

              source
              @[simp]
              theorem FloatLib.Floats.ExecFloat.Binary.formatHex_ofModel {fmt : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan fmt} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model fmt) code] (value : Formats.BinaryInterchange.Model fmt) :
              formatHex (ofModel value) = value.formatHex

              Repacking a model word leaves its exact hexadecimal output unchanged.