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 explicit-direction operations 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 instead raises invalid. This binding documents integer zero as its default invalid delivery and reports invalid explicitly in the result status.

Signed destinations use the existing 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

Signedness and width are independent of the decimal source format.

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 for this binding's invalid delivery.

• status : Status

  Flags raised by this operation alone; successful exact variants 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

This binding's invalid integer result is 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 versus quiet conversion; it does not change the rounding direction or the delivered integer.

@[reducible, inline]

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

Nearest integer, ties to even; suppress inexact, but report invalid conversion.

@[reducible, inline]

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

Nearest integer, ties away from zero; suppress inexact, but report invalid conversion.

@[reducible, inline]

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

Round toward zero; suppress inexact, but report invalid conversion.

@[reducible, inline]

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

Round toward positive infinity; suppress inexact, but report invalid conversion.

@[reducible, inline]

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

Round toward negative infinity; suppress inexact, but report invalid conversion.

@[reducible, inline]

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

Nearest integer, ties to even; report inexact precisely when a valid result changes value.

@[reducible, inline]

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

Nearest integer, ties away from zero; report inexact on a valid numerical change.

@[reducible, inline]

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

Round toward zero; report inexact on a valid numerical change.

@[reducible, inline]

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

Round toward positive infinity; report inexact on a valid numerical change.

@[reducible, inline]

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

Round toward negative infinity; report inexact on a valid numerical change.

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

Convert an arbitrary signed integer directly 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 × Status

Pack a signed conversion into the existing fixed-width carrier, retaining its status. The conversion has already checked the range; packing does not implement wraparound conversion.

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

Pack an unsigned conversion after its range check.