Standard operations for configured binary values

These definitions expose the descriptor-generic operation model on the ordinary ExecFloat.Binary carrier. They add no arithmetic implementation: each one calls the descriptor-model operation through the storage codec, and Configured.Operations.Proof shows that packing changes neither values, flags, nor ternary values.

@[macro_inline]

def FloatLib.Floats.ExecFloat.Binary.remainder {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (dividend divisor : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) (status : Bool := false) : match status with | true => IEEEOutcome | false => Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

IEEE remainder, using a nearest-even integral quotient for finite operands. With status := true the result also carries the invalid indicator.

@[macro_inline]

def FloatLib.Floats.ExecFloat.Binary.roundToIntegral {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome | false => Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Round to an integer and encode it in mode (nearest-even by default). With status := true the result also reports fractional loss and, for a custom finite-only format that saturates, overflow.

@[macro_inline]

def FloatLib.Floats.ExecFloat.Binary.scale {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) (n : ℤ) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.nearest) (status : Bool := false) : match status with | true => IEEEOutcome | false => Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Multiply by 2^n and round in mode (nearest-even by default), IEEE 754 scaleB. With status := true the result also carries the IEEE exception indicators and the ternary value.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.binaryExponentInt {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Formats.BinaryInterchange.Model.IntegerExponentOutcome

Exact integer-result IEEE logB, with no packing or exponent rounding.

@[macro_inline]

def FloatLib.Floats.ExecFloat.Binary.binaryExponent {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) (status : Bool := false) : match status with | true => IEEEOutcome | false => Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Leading binary exponent rounded to nearest-even into the configured format. binaryExponentInt is the exact integer version. With status := true the result also carries the IEEE exception indicators and the ternary value.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.toInt? {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) (mode : Formats.BinaryInterchange.Model.IEEERoundingMode := Formats.BinaryInterchange.Model.IEEERoundingMode.towardZero) : Option ℤ

The integer that rounds the exact value of a finite configured value in mode, toward zero by default as a C or Python integer cast does, or none for a NaN or an infinity.

The integer is unbounded, so no finite value overflows, while roundToIntegral keeps the result in the format.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.copySign {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (magnitude signSource : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Copy the numerical sign of signSource onto magnitude.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.abs {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Absolute value under the configured encoding policy.

@[macro_inline]

def FloatLib.Floats.ExecFloat.Binary.nextUp {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) (status : Bool := false) : match status with | true => IEEEOutcome | false => Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Next representable configured value in the positive direction. With status := true the result also carries the invalid indicator of a signaling NaN.

@[macro_inline]

def FloatLib.Floats.ExecFloat.Binary.nextDown {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) (status : Bool := false) : match status with | true => IEEEOutcome | false => Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

Next representable configured value in the negative direction. With status := true the result also carries the invalid indicator of a signaling NaN.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.minNum {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

IEEE-2008-style minNum, retaining the numeric operand against one quiet NaN.

@[inline]

def FloatLib.Floats.ExecFloat.Binary.maxNum {format : Formats.BinaryInterchange.FloatFormat} {plan : Formats.BinaryInterchange.Configured.StoragePlan format} {code : Type} [ModelCodec plan (Formats.BinaryInterchange.Model format) code] (left right : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code) : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code

IEEE-2008-style maxNum, retaining the numeric operand against one quiet NaN.