Decimal conversions to and from integers

IEEE 754-2019 §§5.4.1, 5.8 and 7.2(j) require rounding to an integer before checking its destination range. In particular, a negative fraction can convert to unsigned zero, and a value just outside an endpoint can round into range.

The ten operations, one per direction and exactness, share the exact coefficient rounder used by decimal integral rounding. No intervening decimal precision rounding occurs. The Exact variants signal inexact only on successful conversion. Every NaN, infinity, or rounded integer outside the destination range raises invalid instead, and the invalid result is integer zero.

Signed destinations use the two's-complement FixedInt bounds. Unsigned destinations use the range of BitVec. Width zero denotes only zero in both cases. Integer sources have no signed zero and therefore convert to +0.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.IntegerFormat : Type

Integer destination format, whose signedness and width do not depend on the decimal source.

structure FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.IntegerOutcome : Type

An integer result and the flags raised by this conversion alone.

• value : ℤ

  The rounded integer when valid, or zero when the conversion is invalid.

• status : Numerics.IEEEStatus

  Flags raised by this operation alone. A successful Exact variant may raise inexact.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.instDecidableEqIntegerOutcome.decEq (x✝ x✝¹ : IntegerOutcome) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.instDecidableEqIntegerOutcome : DecidableEq IntegerOutcome

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.instReprIntegerOutcome.repr : IntegerOutcome → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.instReprIntegerOutcome : Repr IntegerOutcome

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.roundInteger (mode : RoundingMode) (value : ℚ) : ℤ

Round an exact rational once to the integer grid, with sign-sensitive directed rounding.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.invalidOutcome : IntegerOutcome

Invalid result: integer zero with only the invalid flag set.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToInteger (destination : IntegerFormat) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) : IntegerOutcome

Shared conversion kernel. signalInexact selects exact or quiet conversion and changes neither the rounding direction nor the delivered integer.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToIntegerTiesToEven (destination : IntegerFormat) : Datum → IntegerOutcome

Convert to the nearest integer, ties to even. Never raises inexact, and raises invalid only for a nonfinite input or a rounded result outside the destination range.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToIntegerTiesToAway (destination : IntegerFormat) : Datum → IntegerOutcome

Convert to the nearest integer, ties away from zero. Never raises inexact, and raises invalid only for a nonfinite input or a rounded result outside the destination range.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToIntegerTowardZero (destination : IntegerFormat) : Datum → IntegerOutcome

Convert toward zero. Never raises inexact, and raises invalid only for a nonfinite input or a rounded result outside the destination range.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToIntegerTowardPositive (destination : IntegerFormat) : Datum → IntegerOutcome

Convert toward positive infinity. Never raises inexact, and raises invalid only for a nonfinite input or a rounded result outside the destination range.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToIntegerTowardNegative (destination : IntegerFormat) : Datum → IntegerOutcome

Convert toward negative infinity. Never raises inexact, and raises invalid only for a nonfinite input or a rounded result outside the destination range.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToIntegerExactTiesToEven (destination : IntegerFormat) : Datum → IntegerOutcome

Convert to the nearest integer, ties to even, raising inexact when a valid result changes.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToIntegerExactTiesToAway (destination : IntegerFormat) : Datum → IntegerOutcome

Convert to the nearest integer, ties away, raising inexact when a valid result changes.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToIntegerExactTowardZero (destination : IntegerFormat) : Datum → IntegerOutcome

Convert toward zero, raising inexact when a valid result changes value.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToIntegerExactTowardPositive (destination : IntegerFormat) : Datum → IntegerOutcome

Convert toward positive infinity, raising inexact when a valid result changes value.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToIntegerExactTowardNegative (destination : IntegerFormat) : Datum → IntegerOutcome

Convert toward negative infinity, raising inexact when a valid result changes value.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertFromInt (destination : Format) (mode : RoundingMode) (source : ℤ) : Outcome

Convert an arbitrary signed integer to a decimal destination, with preferred quantum zero and one destination rounding (§5.4.1).

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertFromFixedInt (destination : Format) (mode : RoundingMode) {width : ℕ} (source : Numerics.Representations.FixedInt width) : Outcome

Convert a two's-complement source by its exact signed value.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertFromUnsigned (destination : Format) (mode : RoundingMode) {width : ℕ} (source : BitVec width) : Outcome

Convert an unsigned word by its exact nonnegative value.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToFixedInt (width : ℕ) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) : Numerics.Representations.FixedInt width × Numerics.IEEEStatus

Pack a signed conversion into the fixed-width carrier, keeping its status. The conversion has already checked the range, so packing never wraps around.

def FloatLib.Floats.Formats.DecimalInterchange.Conversion.Integer.convertToUnsigned (width : ℕ) (mode : RoundingMode) (signalInexact : Bool) (source : Datum) : BitVec width × Numerics.IEEEStatus

Pack an unsigned conversion after its range check.