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) or d (binary64).
| 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 |
Trealla's abs/1 and unary minus wrap a computed native INT64_MIN; binary subtraction promotes it to a bignum on both hosts.
Decimal and C hex literals are parsed into a rational before rounding: no double rounding through binary64 for a binary32 literal.
Every finite binary float has a terminating decimal expansion. Writing N*5^k e-k avoids padding and is exactly representable by strtof/strtod.