Format-generic executable hyperbolic functions

sinh, cosh, and tanh are built from exact dyadics, exact rationals, and the configured exponential kernel, so the same algorithms elaborate for arbitrary binary descriptors.

The small-argument branches evaluate the polynomial stored in Config.sinhCoeffsAsc exactly. For generated configurations, Config.sinhTerms selects its length from the destination fraction width using a Taylor-tail target; binary32's coefficient table has one additional term. sinh rounds the polynomial once. cosh integrates it exactly before one final rational rounding. tanh approximates s / sqrt (1 + s^2), where s is the truncated sinh value, using an integer square root with tanhGuardBits extra bits. Larger arguments use dyadic approximations from the exponential polynomial, combined before destination rounding. Bounded alignment preserves the sign of tiny contributions at rounding midpoints. These algorithms have no proved general real-error or ULP bound yet.

The provider entry points inspect the decoded input exponent before requesting approximation data. For nonzero inputs with leading exponent below -(fracWidth + 2), sinh and tanh return the input and cosh returns one. Large inputs return the rounded limit of tanh, or the descriptor's native overflow result for sinh and cosh. These conservative magnitude branches bypass even caller-supplied approximation coefficients and avoid huge fixed-point conversions for extreme inputs. The remaining inputs are compared with the destination's rounded encoding of 1/2 to choose between the polynomial and exponential branches. The lower-level polynomial and dyadic helpers do not apply these magnitude guards.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.mulDyadic (left right : Numerics.Dyadic) : Numerics.Dyadic

Exact dyadic multiplication without rounding.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.dyadicOfInt (value : ℤ) : Numerics.Dyadic

Embed an integer as an exact dyadic.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.oneDyadic : Numerics.Dyadic

Exact dyadic one.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.zeroDyadic : Numerics.Dyadic

Exact dyadic zero.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.evalDyadicPolyAsc (coefficients : List ℤ) (value : Numerics.Dyadic) : Numerics.Dyadic

Evaluate ascending integer coefficients as an exact polynomial in a dyadic argument.

An empty coefficient list evaluates to zero.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.roundDyadicDivNat (fmt : FloatFormat) (value : Numerics.Dyadic) (denominator : ℕ) : Model fmt

Round value / denominator to the destination format for a positive denominator. A zero numerator preserves its sign; a zero denominator with nonzero numerator gives invalidResult.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.ofNat (fmt : FloatFormat) (value : ℕ) : Model fmt

Round a nonnegative natural number directly into the destination format.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.sinhSeriesNumerator (config : Config) (exact : Numerics.Dyadic) : Numerics.Dyadic

Exact numerator of the truncated odd Taylor series of sinh at a dyadic argument.

For the Taylor data supplied by Config, dividing by config.sinhDenominator gives x + x^3/3! + ..., truncated to config.sinhCoeffsAsc.length terms. A custom configuration instead evaluates its supplied odd polynomial.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.sinhTaylorSmallWith {fmt : FloatFormat} (config : Config) (x : Model fmt) : Model fmt

Evaluate the truncated sinh series at a finite input and round once.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.coshTaylorSmallWith {fmt : FloatFormat} (config : Config) (x : Model fmt) : Model fmt

Evaluate the integral of the configured sinh polynomial, with constant term one.

If the odd coefficients are aᵢ / D, the even coefficients after the constant are aᵢ / ((2*i+2)*D). Multiplying by (2*n)!, where n is the coefficient count, makes every coefficient integral without assuming divisibility properties of a caller-supplied configuration. Keeping this polynomial exact retains the quartic correction at near-one rounding midpoints.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.tanhGuardBits : ℕ

Extra bits carried by the integer square root in the small-argument tanh branch.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.tanhTaylorSmallWith {fmt : FloatFormat} (config : Config) (x : Model fmt) : Model fmt

Approximate tanh for small arguments from a truncated sinh series.

The real identity is tanh x = sinh x / sqrt (1 + sinh x ^ 2). Substituting the truncated series gives an approximation whose magnitude is a / sqrt b, after clearing powers of two from its numerator and denominator. The implementation computes q = floor (sqrt (a^2 * 4^k / b)), restores the input sign, and rounds q * 2^(-k) once. The choice of k gives the square-root calculation extra working bits controlled by tanhGuardBits; a real-error or ULP bound for the complete calculation remains unproved.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.expDyadicWith (config : Config) (exact : Numerics.Dyadic) : Numerics.Dyadic

Keep the exponential polynomial's dyadic result until its caller finishes the operation.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.roundExpDyadic (fmt : FloatFormat) (value : Numerics.Dyadic) : Model fmt

Classify an exponential-derived dyadic before asking the destination rounder to align it.

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

Combine dyadics for one destination rounding without allocating their entire exponent gap.

A sufficiently small addend is replaced by a signed sticky contribution below the destination's rounding bits. Its sign still resolves a midpoint in the larger operand. Otherwise exact alignment shifts by at most a significand's bit length plus fmt.fracWidth + 3.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.expMulDyadicWith {fmt : FloatFormat} (config : Config) (x : Model fmt) (scale : Numerics.Dyadic) : Model fmt

Approximate exp x * scale for a finite input, scaling before destination-format rounding.

The range reduction and polynomial are the same as in expWithProvider. Scaling the dyadic before classifying its range retains the upper finite interval when scale = 1/2.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.hyperbolicSumWith (fmt : FloatFormat) (config : Config) (exact scale : Numerics.Dyadic) (subtract : Bool) : Model fmt

Combine both scaled exponential approximations before the hyperbolic result is rounded.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Transcendentals.tanhExpWith (fmt : FloatFormat) (config : Config) (exact : Numerics.Dyadic) : Model fmt

Form (exp (2*x) - 1) / (exp (2*x) + 1) before destination rounding.

Doubling the decoded argument avoids an intermediate overflow. Outside the quotient's transition range, return its rounded limit before aligning with one; the remaining shifts are bounded by the polynomial's bit length and the destination precision.

@[noinline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sinhLarge {fmt : FloatFormat} (getConfig : Unit → Transcendentals.Config) (x half : Model fmt) : Model fmt

Evaluate the exponential branch used by sinhWithProvider.

The provider passes the destination's rounded encoding of 1/2. Its decoded dyadic value scales each exponential before their difference is rounded, avoiding an intermediate destination-format rounding of either exponential.

def FloatLib.Floats.Formats.BinaryInterchange.Model.sinhWithProvider {fmt : FloatFormat} (getConfig : Unit → Transcendentals.Config) (x : Model fmt) : Model fmt

Evaluate hyperbolic sine with a delayed configuration provider.

Tiny inputs return unchanged before configuration generation. A decoded leading exponent above log2 (abs maxNormalExponent + 2) implies magnitude greater than abs maxNormalExponent + 2, where the result overflows; use the descriptor's overflow policy without evaluating an exponential. The remaining inputs below the encoded half use the exact truncated series; larger inputs combine dyadic exponential approximations scaled by that encoded half before rounding.

def FloatLib.Floats.Formats.BinaryInterchange.Model.coshWithProvider {fmt : FloatFormat} (getConfig : Unit → Transcendentals.Config) (x : Model fmt) : Model fmt

Evaluate hyperbolic cosine with a delayed configuration provider.

Tiny inputs return one and sufficiently large inputs return the descriptor's positive overflow result before configuration generation, using the same input bounds as sinhWithProvider. The remaining inputs below the encoded half use an exact even polynomial. Larger finite inputs add dyadic approximations of exp x / 2 and exp (-x) / 2 before rounding.

def FloatLib.Floats.Formats.BinaryInterchange.Model.tanhWithProvider {fmt : FloatFormat} (getConfig : Unit → Transcendentals.Config) (x : Model fmt) : Model fmt

Evaluate hyperbolic tangent with a provider called only after special values and magnitude guards.

Tiny inputs return unchanged. A decoded leading exponent above log2 (fracWidth + 3) implies |x| > fracWidth + 3, well past the nearest-even transition to signed one. Returning that limit before fixed-point conversion also avoids allocating an integer proportional to a huge input.

def FloatLib.Floats.Formats.BinaryInterchange.Model.sinhWith {fmt : FloatFormat} (config : Transcendentals.Config) (x : Model fmt) : Model fmt

Deterministic hyperbolic sine using the configured exponential kernel.

def FloatLib.Floats.Formats.BinaryInterchange.Model.coshWith {fmt : FloatFormat} (config : Transcendentals.Config) (x : Model fmt) : Model fmt

Deterministic hyperbolic cosine using the configured exponential kernel.

def FloatLib.Floats.Formats.BinaryInterchange.Model.tanhWith {fmt : FloatFormat} (config : Transcendentals.Config) (x : Model fmt) : Model fmt

Deterministic hyperbolic tangent.

After the magnitude guards, small inputs substitute a truncated sinh series into s / sqrt (1 + s^2). Larger finite inputs round the rational quotient formed from the dyadic approximation to exp (2 * |x|), then clamp it from below to the small-branch value at the encoded half. The sign is restored after this comparison.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.sinh {fmt : FloatFormat} (x : Model fmt) : Model fmt

Hyperbolic sine using the default configuration for the destination format.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.cosh {fmt : FloatFormat} (x : Model fmt) : Model fmt

Hyperbolic cosine using the default configuration for the destination format.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.tanh {fmt : FloatFormat} (x : Model fmt) : Model fmt

Hyperbolic tangent using the default configuration for the destination format.