Explicit rounding runtime for configured binary values #
The six IEEE arithmetic operations lift from the descriptor model to the ordinary configured
ExecFloat.Binary carrier with an explicit rounding direction:
open scoped FloatLib.IEEERounding
ExecFloat.Binary.add x y (rounding := +∞)
ExecFloat.Binary.div x y (rounding := -∞)
Operands come first. The rounding argument is required and may be supplied by name. No global floating-point environment or rounding-mode instance is changed.
The constructor names .towardPositiveInfinity and .towardNegativeInfinity are always
available. The shorter +∞ and -∞ terms are opt-in so they do not collide with extended-real
notation elsewhere in a development.
These functions round one primitive operation. To evaluate an algebraic expression exactly and
round only its final result, use ExecFloat.ExactExpression with ExecFloat.roundOnceWith and a
binary conversion context built by ExecFloat.Binary.Conversion.Context.withRounding.
The *WithStatus variants return the configured value together with the five IEEE exception
indicators computed by the descriptor model. There is no hidden floating-point environment:
applications that need sticky flags combine successive statuses explicitly with
Numerics.IEEEStatus.union.
FMA means fused multiply-add. It forms the exact value x * y + z and rounds once; ordinary
x * y + z rounds the product and then the sum. IEEE 754 specifies FMA as a primitive, including
its exceptional-value and status behavior. ExactExpression handles larger finite algebraic
expressions.
A configured binary result paired with the IEEE exception indicators raised by one operation.
This is an alias for a pair rather than another result structure. Pattern matching exposes the
configured value first and its Model.IEEEStatus second.
Instances For
Repack a model outcome without changing any IEEE exception indicator.
Instances For
Decode the value component of a configured outcome, preserving its status exactly.
Instances For
Add two configured values and round the exact sum in the selected IEEE direction.
Instances For
Subtract two configured values and round the exact difference in the selected direction.
Instances For
Multiply two configured values and round the exact product in the selected direction.
Instances For
Divide two configured values and round the exact quotient in the selected direction.
Instances For
Form the exact product-plus-addend and round once in the selected direction.
This is the IEEE fused operation; mul followed by add rounds twice.
Instances For
Take square root and round the exact nonnegative result in the selected direction.
Instances For
Status-bearing operations #
Add with an explicit rounding direction and return all IEEE exception indicators.
Instances For
Subtract with an explicit rounding direction and return all IEEE exception indicators.
Instances For
Multiply with an explicit rounding direction and return all IEEE exception indicators.
Instances For
Divide with an explicit rounding direction and return all IEEE exception indicators.
Instances For
Fused multiply-add with an explicit rounding direction and IEEE exception indicators.
Instances For
Square root with an explicit rounding direction and return all IEEE exception indicators.