ieee.pl
IEEE 754 binary32 and binary64 arithmetic with integers only, rounding to nearest, ties to even.
Operands and results are unsigned bit patterns, never host floats. Finite intermediates are exact rationals, and round_ratio is the single rounding boundary, gradual underflow and overflow included. All public inputs must be concrete.
Predicates
K is s (binary32), d (binary64) or x (the x87 80-bit extended format of C's long double on x86-64: a sign, 15 exponent bits and a 64-bit significand whose integer bit is explicit, in the low 80 bits of the pattern). An x NaN operand follows the x87's rule instead of SSE's: when both operands are NaNs, a quiet one wins over a signaling one, else the one with the larger significand, else the first.
| Predicate | Notes |
|---|---|
ieee_binaryK, Op, A, B, R | Op is add, sub, mul or div |
ieee_negK, A, B | flips the sign bit |
ieee_convertFrom, To, A, B | between the two formats |
ieee_from_intK, N, B | N any integer |
ieee_to_intK, B, N | truncates; fails for nonfinite inputs, and the caller checks the destination integer's range |
ieee_compareK, Cond, A, B, R | R is 1 or 0; Cond is eq, ne, lt, le, gt, ge, o (ordered) or uo (unordered) |
ieee_parseK, Chars, B | a decimal or C hexadecimal significand, without a C type suffix: the frontend selects K after removing the suffix |
ieee_decimalK, B, Chars | an exact decimal, not necessarily the shortest; fails for nonfinite inputs |
format(K, fraction bits, exponent bits, bias): the fraction excludes the integer bit, which x stores explicitly (integer_bit/2).
| 39 | s | 23 | 8 | 127 |
| 40 | d | 52 | 11 | 1023 |
| 41 | x | 63 | 15 | 16383 |
B is the format-K bit pattern nearest the integer N, ties to even.
Trealla's abs/1 and unary minus wrap a computed native INT64_MIN; binary subtraction promotes it to a bignum on both hosts.
N is the finite float B truncated toward zero. Fails for an infinity or NaN; the caller checks that N fits the destination integer.
R is A Op B in format K, Op add, sub, mul or div, rounded to nearest, ties to even, with SSE's NaN rules (x87's for K = x, header).
B is the format-From float A converted to format To, rounded to nearest; a NaN keeps as much of its payload as fits, aligned at the top, and is quieted.
R is 1 when A Cond B holds for format-K floats, else 0. When either operand is a NaN only ne and uo hold, as C's != and SSE's unordered compare give.
B is the format-K float nearest the decimal or C hexadecimal literal Cs, without a type suffix. Literals are parsed into a rational before rounding: no double rounding through binary64 for a binary32 literal.
Cs is an exact decimal for the finite float B, not necessarily the shortest; fails for an infinity or NaN. Every finite binary float has a terminating decimal expansion. Writing N*5^k e-k avoids padding and is exactly representable by strtof/strtod.