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). projectMagnitude requires a nonnegative input. project handles either sign and takes the sign of an exact zero as its own argument.

structure FloatLib.Floats.Formats.DecimalInterchange.Outcome : Type

A decimal result with the exceptions raised by this operation.

• value : Datum

  The delivered decimal datum.

• status : Numerics.IEEEStatus

  Exceptions raised while computing the datum.

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqOutcome : DecidableEq Outcome

def FloatLib.Floats.Formats.DecimalInterchange.instDecidableEqOutcome.decEq (x✝ x✝¹ : Outcome) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.instReprOutcome : Repr Outcome

def FloatLib.Floats.Formats.DecimalInterchange.instReprOutcome.repr : Outcome → ℕ → Std.Format

def FloatLib.Floats.Formats.DecimalInterchange.Format.minNormal (f : Format) : ℚ

Least positive normal value, independent of the chosen cohort.

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

Greatest finite magnitude with sign negative, in its largest-quantum representation.

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.

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

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

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 without forming the powers used for rounding or tininess.

def FloatLib.Floats.Formats.DecimalInterchange.clampScaledExponent (f : Format) (coefficient : ℕ) (exponent : ℤ) : ℤ

Clamp the exponent of coefficient * 10^exponent to a range where projection stays cheap.

A zero coefficient gets exponent zero. Otherwise the exponent is kept between a lower bound, where the magnitude is below half the least subnormal quantum, and maxQuantum + precision, where it overflows. projectScaled_eq proves that projecting the clamped magnitude gives the same outcome.

def FloatLib.Floats.Formats.DecimalInterchange.projectScaled (f : Format) (mode : RoundingMode) (negative : Bool) (coefficient : ℕ) (exponent preferred : ℤ) : Outcome

Project the exact magnitude coefficient * 10^exponent with a preferred quantum.

The exponent is clamped with clampScaledExponent before the power of ten is formed, so huge exponents such as 10^(10^12) are never materialized. The outcome equals projectMagnitude f mode negative (coefficient * 10^exponent) preferred.

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.