TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.DecimalInterchange.Projection.Runtime

Cohort-aware rational projection #

Precision rounding precedes the overflow test (IEEE 754-2019 §7.4). Decimal tininess is detected before rounding (§7.5), and the underflow flag requires both tininess and inexactness. Exact results select the cohort member closest to the preferred quantum (§5.2). The magnitude interface requires a nonnegative input; project handles either sign and receives the sign of an exact zero separately.

source
@[reducible, inline]
abbrev FloatLib.Floats.Formats.DecimalInterchange.Status :
Type

The shared IEEE exception indicators, also used by binary arithmetic.

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

    A decimal result with the exceptions raised by this operation.

    • value : Datum

      The delivered decimal datum.

    • status : Status

      Exceptions raised while computing the datum.

    Instances For
      source
      def FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqOutcome.decEq (x✝ x✝¹ : Outcome) :
      Decidable (x✝ = x✝¹)
      Instances For
        source
        @[instance_reducible]
        instance FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqOutcome :
        DecidableEq Outcome
        source
        @[instance_reducible]
        instance FloatLib.Floats.Formats.DecimalInterchange.instReprOutcome :
        Repr Outcome
        source
        def FloatLib.Floats.Formats.DecimalInterchange.instReprOutcome.repr :
        Outcome → ℕ → Std.Format
        Instances For
          source
          def FloatLib.Floats.Formats.DecimalInterchange.Format.minNormal (f : Format) :
          ℚ

          Least positive normal value, independent of the chosen cohort.

          Instances For
            source
            def FloatLib.Floats.Formats.DecimalInterchange.Format.maxFinite (f : Format) (negative : Bool) :
            Datum

            Greatest finite magnitude and its largest-quantum representation.

            Instances For
              source
              def FloatLib.Floats.Formats.DecimalInterchange.roundedPair (f : Format) (mode : RoundingMode) (negative : Bool) (magnitude : ℚ) :
              ℕ × ℤ

              Precision-rounded coefficient and exponent with an unbounded upper exponent. The only possible carry is exactly 10 ^ precision.

              Instances For
                source
                def FloatLib.Floats.Formats.DecimalInterchange.RoundingMode.overflowToInfinity (mode : RoundingMode) (negative : Bool) :
                Bool

                Whether overflow delivers an infinity rather than the greatest finite value.

                Instances For
                  source
                  def FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude (f : Format) (mode : RoundingMode) (negative : Bool) (magnitude : ℚ) (preferred : ℤ) :
                  Outcome

                  Project a nonnegative rational magnitude, retaining the supplied sign even at zero. Exact zero selects its cohort directly, without allocating powers for rounding or tininess.

                  Instances For
                    source
                    def FloatLib.Floats.Formats.DecimalInterchange.project (f : Format) (mode : RoundingMode) (value : ℚ) (preferred : ℤ) (negativeZero : Bool := false) :
                    Outcome

                    Round an exact rational value with an operation's preferred quantum. negativeZero is consulted only when the exact input equals zero.

                    Instances For