Numbers
Int is a 64-bit signed integer whose overflow traps, and F64 an IEEE double. The wrapping, checked and saturating methods are there for when you want another overflow behavior. BigInt, fixed-point Dec (for money) and exact Ratio cover the rest. Nothing converts implicitly: n.to_f64, x.round, big(n), decimal(s).
| Receiver | Methods |
|---|---|
Int | abs to_f64 band(m) bor(m) bxor(m) shl(n) shr(n) bnot popcount clz ctz rotl(n) rotr(n) byteswap gcd(b) lcm(b) wrapping_add(b) wrapping_sub(b) wrapping_mul(b) checked_add(b) checked_sub(b) checked_mul(b) checked_div(b) saturating_add(b) saturating_sub(b) saturating_mul(b) format(spec) (bitwise on the 64-bit pattern; shr is logical; a shift outside 0..63 gives 0; checked_* give Opt; gcd and lcm trap on overflow) |
F64 | abs round floor ceil trunc sqrt pow(y) exp ln log2 log10 sin cos tan asin acos atan atan2(x) hypot(y) is_nan is_finite fmt(digits), and sinh cosh tanh asinh acosh atanh cbrt exp2 expm1 log1p erf erfc gamma lgamma fmod(y) remainder(y) copysign(y) nextafter(y) fdim(y) fma(y, z) is_inf format(spec) checked_round checked_floor checked_ceil checked_trunc (round floor ceil trunc give Int, trapping when there is none; checked_* give Opt[Int]; fmt is fixed point with 0..=20 digits) |
BigInt | add(b) sub(b) mul(b) div(b) rem(b) divmod(b) pow(e) neg abs sign to_int to_f64 to_dec (division truncates like Int) |
Dec | add(d) sub(d) mul(d) div(d, scale) round(scale) scale neg abs sign to_f64; add sub mul are exact, div and round round half to even; prints like 12.50. Equal values with different scales differ (1.5 < 1.50) |
Complex | fields re im; add(w) sub(w) mul(w) div(w) pow(w) scale(k) neg conj abs arg norm exp ln sqrt sin cos tan sinh cosh tanh asin acos atan asinh acosh atanh (abs is the magnitude, norm its square, arg the angle; pow(0, 0) is 1; the inverse functions take the principal branch) |
Rng | fields state gamma; next int(lo, hi) f64 normal(mean, sd) uniform(lo, hi) exp(rate) bool(p) binomial(n, p) poisson(mean) geometric(p) gamma(shape, scale) beta(a, b) weighted(ws) split stream(k): each gives (value, next_rng), split gives two independent generators and stream(k) the kth independent stream |
Ratio | fields num den (BigInt, always normalized: gcd 1, den > 0), add(r) sub(r) mul(r) div(r) neg abs inv pow(k) sign is_int floor ceil trunc round to_f64 to_dec(scale) (floor ceil trunc round give BigInt, round is half to even; to_f64 is correctly rounded). < <= > >= and sorting compare values; prints as 3/4 or 5. Division by zero traps |
+, -, * and unary - on BigInt, Dec and Ratio call add sub mul neg, and / on BigInt and Ratio calls div (a Dec division takes a scale: d.div(e, 2)), also through [T: Add] bounds.
Constructors: big(n), parse_big(s) and decimal(s) (both Opt), ratio(n, d) and ratio_big(n, d) (a zero denominator traps), parse_ratio(s), complex(re, im) and polar(r, theta), pi() euler() inf() nan(), min(a, b), max(a, b), clamp(x, lo, hi).
Random numbers are pure: each call takes a seed and returns (value, next_seed). rand(seed) is non-negative, rand_int(seed, lo, hi) is in lo..hi (it traps unless lo < hi), rand_f64(seed) is in [0, 1), and rand_normal(seed, mean, sd), rand_uniform(seed, lo, hi), rand_exp(seed, rate) and rand_bool(seed, p) give the usual distributions, as do rand_binomial(seed, n, p), rand_poisson(seed, mean), rand_geometric(seed, p), rand_gamma(seed, shape, scale) and rand_beta(seed, a, b); rand_weighted(seed, ws) picks an index with probability proportional to its weight. Bad parameters trap. rng(seed) is a splittable generator (a SplitMix64) that gives the same numbers as the seed functions, with every distribution as a method. xs.shuffle(seed) and xs.choice(seed) use the same generator.
F64 order and conversions
F64 arithmetic is IEEE 754 double precision, the same in both tiers. Comparison is a total order, so that ==, <, sort, unique, contains, min, max and map and set keys agree with each other:
- On numbers it is the numeric order, and
-0.0 == 0.0:-0.0 < 0.0is false andx >= 0.0holds for-0.0(so does awhere _ >= 0.0refinement). The two zeros stay distinct values:-0.0prints as-0.0and1.0 / -0.0is-inf(). A sort is stable, so[0.0, -0.0].sortkeeps their order, and a map keeps the key it got first. - NaN equals itself and sorts above
inf(), sonan() == nan()is true,nan() < 1.0is false, and a sorted list ends with its NaNs.x.is_nantests for it.
round floor ceil trunc round to a whole number (round takes halves away from zero) and give it as an Int. When there is no such Int, for NaN, an infinity, or a value at or above 2^63 or below -2^63, they trap with integer overflow, like Int arithmetic; they don’t saturate. checked_round checked_floor checked_ceil checked_trunc give Opt[Int] with none in those cases, so x.checked_round.or(0) picks a default.
sspur check proves each conversion safe or warns with W_CONVERSION_MAY_TRAP (ADR 0044), so code that checks without that warning never traps in one. It asks Z3, with what is known at the conversion: where refinements of parameters, aliases and record fields, pre, the enclosing if, and and or conditions, let bindings and vars between assignments, literal arithmetic, n.to_f64 of an Int, xs.len, min, max, clamp and the common F64 methods. A function that isn’t pub and can’t be exported to C is also proved at each of its calls. So p: F64 where _ >= 0.0 and _ <= 1.0 makes (p * 100.0).round safe, if x.is_finite and x.abs < 9.2e18 then x.floor else 0 is safe, and x > 0.0 alone is not (NaN sorts above every number). The results are cached per program and per definition, so a repeated check doesn’t prove anything again and an edit only proves again what depended on it; without Z3, check prints a note saying how many conversions it didn’t check. The language server and the MCP check tool report it too; run, test and the playground don’t.