Arithmetic runtime for configured binary values #
The six IEEE arithmetic operations lift from the descriptor model to configured binary values with
the model's options, a rounding direction mode and status:
open FloatLib.Rounding
ExecFloat.Binary.add x y (mode := up)
ExecFloat.Binary.div x y (mode := down) (status := true)
Operands come first, and mode defaults to nearest-even. The direction and status are ordinary
arguments and results, and no rounding-mode instance is changed.
The constructor names .up and .down are always available, and open FloatLib.Rounding lets
callers write them bare.
The default call, nearest-even without status, runs the certified implementation selected for the
format, the same ExecFloat.add through ExecFloat.fma that the operators +, -, *, /
run, so x.add y, ExecFloat.Binary.add x y, and x + y compile to the same kernel call. The
other directions, and every call with status := true, decode the operands through the
configured codec, run the model operation with the same options, and encode the result. Square
root sends nearest-away rounding to the selected kernel too, since an exact square root is never a
tie.
Each operation is a @[macro_inline] selector, so with literal options only the chosen branch is
compiled. Its decoding theorem toModel_add and its siblings in Configured.Rounding.Proof hold
for every capability whose reference operation is the configured model operation, which is true of
every capability instance this library declares.
These functions round one primitive operation. To evaluate an algebraic expression exactly and
round only its final result, use ExecFloat.ExactExpression with ExecFloat.roundOnce, which
takes the same (mode := ...) option.
With status := true an operation returns the configured value together with the five IEEE
exception indicators and the ternary value computed by the descriptor model. There is no hidden
floating-point environment: IEEEOutcome.bind feeds one result to the next operation and keeps
the union of their flags, which are sticky in the IEEE sense.
ofRat q rounds an exact rational once into the format with the same mode and status options.
Literals are rounded the same way.
FMA means fused multiply-add. It forms the exact value x * y + z and rounds once, while 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 with the IEEE exception indicators and the ternary value of one operation.
The fields mirror Model.IEEEOutcome, with the value in configured storage. The numeric
projections .1, .2, and .3 select the value, the status, and the ternary value.
- value : Binary format.expWidth format.fracWidth format.encoding format.exponentBias ⋯ ⋯ ⋯ ⋯ plan code
Delivered configured result.
- status : Numerics.IEEEStatus
Exception indicators raised while computing
value. - ternary : Ordering
The delivered value compared with the exact result, as
Model.IEEEOutcome.ternary.
Instances For
Repack a model outcome without changing any IEEE exception indicator or the ternary value.
Instances For
Decode the value component of a configured outcome, preserving its status and ternary value.
Instances For
Feed the value of outcome to the next operation next, keeping the union of both statuses and
the ternary value of next.
The flags are sticky: a flag raised by either step is set in the result. The ternary value is not
accumulated. It compares the final value with the exact result of next on its rounded input,
not with the exact value of the whole computation.
(ExecFloat.Binary.div x y (status := true)).bind fun q => ExecFloat.Binary.sqrt q (status := true)
Instances For
#eval shows the three fields, displaying the value as its format does.
The default outcome has the supplied default value, a clear status, and the ternary value .eq.
With the standard configured binary value instance, that value is +0.
Boolean equality compares the three fields, the value with its own ==. For configured binary
values that is IEEE numerical comparison, so outcomes holding NaNs are unequal.
Structural equality of the three fields.
Round an exact rational once into the configured format, in mode (nearest-even by default). With
status := true the result also carries the IEEE exception indicators and the ternary value.
The expected type selects the format, as in (ExecFloat.Binary.ofRat (1 / 3) (mode := up) : Binary32). Numeric and scientific literals round the same way, to nearest-even.
Instances For
Add two configured values, rounding the exact sum in mode (nearest-even by default). With
status := true the result also carries the IEEE exception indicators and the ternary value.
Nearest-even addition without status is ExecFloat.add, the selected kernel that + runs.
Instances For
Subtract two configured values, rounding the exact difference in mode (nearest-even by
default). With status := true the result also carries the IEEE exception indicators and the
ternary value.
Nearest-even subtraction without status is ExecFloat.sub, the selected kernel that - runs.
Instances For
Multiply two configured values, rounding the exact product in mode (nearest-even by default).
With status := true the result also carries the IEEE exception indicators and the ternary value.
Nearest-even multiplication without status is ExecFloat.mul, the selected kernel that * runs.
Instances For
Divide two configured values, rounding the exact quotient in mode (nearest-even by default).
With status := true the result also carries the IEEE exception indicators and the ternary value.
Nearest-even division without status is ExecFloat.div, the selected kernel that / runs.
Instances For
Form the exact product-plus-addend and round once in mode (nearest-even by default). With
status := true the result also carries the IEEE exception indicators and the ternary value.
This is the IEEE fused operation, whereas mul followed by add rounds twice. Nearest-even FMA
without status is ExecFloat.fma, the selected kernel.
Instances For
Take the square root of a configured value, rounding the exact result in mode (nearest-even by
default). With status := true the result also carries the IEEE exception indicators and the
ternary value.
Both nearest modes without status run ExecFloat.sqrt, the selected kernel: an exact square root
is never a tie.