Single-round binary algebraic operations

These operations evaluate exact expressions and round only the final result. The norm forms an exact dyadic sum of squares. Square roots use integer square root after exact target scaling, and other roots compare integer powers of rational boundaries without a refinement budget. All widths and complete descriptors use the same algorithms. Specialization on the descriptor lets compiled calls share format constants and remove inapplicable encoding branches. Integer powers can materialize large exact integers, because the exponent is not capped.

Signed zero, infinities and invalid arguments are handled before exact evaluation. A zero integer exponent returns one, including for a quiet NaN base, but signaling NaNs are quieted first. Degree zero is invalid for rootN.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.roundAlgebraicRat (fmt : FloatFormat) (value : ℚ) : Model fmt

Round an exact rational value once, using the complete format descriptor.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Algebraic.hypotDyadic (fmt : FloatFormat) (left right : Numerics.Dyadic) : Model fmt

Square root of an exact dyadic sum of squares, with no intermediate format rounding.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.rsqrt {fmt : FloatFormat} (value : Model fmt) : Model fmt

Reciprocal square root, rounded once from the exact reciprocal radicand.

Positive infinity gives positive zero. Signed zero gives the correspondingly signed overflow value. Negative nonzero inputs are invalid, and NaNs follow the unary propagation policy.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.hypot {fmt : FloatFormat} (left right : Model fmt) : Model fmt

Euclidean norm, rounded once from the exact sum of squares.

An infinite operand gives positive overflow, including when the other operand is a quiet NaN. A signaling NaN takes precedence. Two zeros give positive zero, independently of their signs.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.powInt {fmt : FloatFormat} (value : Model fmt) (exponent : ℤ) : Model fmt

Integer-exponent power with one final rounding.

For nonzero finite bases, exponentiation takes place in the exact rationals, including negative exponents. Zero and infinity retain a negative sign exactly for an odd exponent. A signaling NaN is quieted before the zero-exponent rule, and otherwise the zero exponent returns one.

@[specialize #[0]]

def FloatLib.Floats.Formats.BinaryInterchange.Model.rootN {fmt : FloatFormat} (value : Model fmt) (degree : ℤ) : Model fmt

Integer root with one final rounding, including reciprocal roots for negative degrees.

Even degrees require a nonnegative input, while odd degrees use the signed real root. For positive degrees, negative zero gives negative zero for odd degrees and positive zero for even degrees. For negative degrees, either zero gives overflow with a negative sign exactly when the input is negative zero and the degree is odd. NaN inputs are quieted for every degree, keeping their payload. Negative nonzero inputs with even degree, and every other input with degree zero, are invalid.