bend-collections

Search uses release 1.0.0.0 · 4,483 definitions

Releases (1)

1.0.0.0 indexed

Definitions (4,483)

src/math/f64.bend

def mul_n2
def mul_n
def fin_zero
def mul_z
def inf_or_nan
def mul_b
def mul_cls
def mul
def digit_finthe next quotient digit of r * 2^32 / b (r < b, b >= 2^52) and the remainder
def digit
def dq_fin
def dq_mid
def div_qta in [b, 2b): 2^62 + floor((a - b) * 2^62 / b), sticky, by two 32-bit digits
def div_q
def div_ab
def div_n
def div_za
def div_z
def div_b
def div_cls
def div
def sq_fin
def sq_d2the root is S0 - 2: remainder (2 S0 - 3) - (D - (2 S0 - 1)) with c = 2 S0 - 1
def sq_d1S0^2 - N = D > 0: the root is S0 - 1 when D <= 2 S0 - 1 (remainder c - D)
def sq_neg
def sq_remN - S0^2 = a - b for a = u 2^32, b = q^2: the root is S0 when b <= a
def sq_qu
def sq_clampq = 2^32 (r = 2 s) is taken as q = 2^32 - 1 with u = 2 s
def sq_div
def sq_root_sone step of Zimmermann's SqrtRem (Karatsuba square root) from s = isqrt(nh): r = nh - s^2, (q, u) = divmod(r 2^32, 2 s) give S0 = s 2^32 + q with N - S0^2 = u 2^32 - q^2 for N = nh 2^64; S0 - 2 <= isqrt(N) <= S0 and the exact remainder decides the root and its sticky bit without squaring S0
def sq_root
def sq_evenm * 2^(E - OFF - 1075) with the unbiased exponent made even (E odd); the root of m * 2^72 has its top bit at 62
def sq_n
def sq_pos
def sq_sign
def sq_cls
def sqrt
def lt_s
def le_s
def unordered
def zeros
def lt_z
def lt
def le_z
def le
def eq_z
def eq
def low_bitsn mod 2^k and n div 2^k by k halvings (no 2^32 constant: the proof checker would expand it in unary)
def high_bits
def jam_natthe jam of n >> d (the bits shifted out OR-ed into bit 0)
def word64
def sig63n with its top bit moved to bit 62 (b = bit_length(n)): shifted up when b <= 63 (every runtime Nat), jammed down otherwise
def of_nat_z
def of_natthe double nearest to n (exact below 2^53)
def pow22^k for k <= 1023
def dmant_zthe significand with its hidden bit (bit 52 of a normal number) and the scale of its unit, the exponent plus Z = 3000 (1926 for subnormals), as in spec/math/f64.bend's mant and xexp
def dmant
def dexp_z
def dexp
def rw_top
def rw_z
def round_wthe double nearest to (-1)^s * w * 2^(x - 3000), for x >= 63: every exact result below is an integer of at most 64 bits at a scale, rounded once
type RMode
def b64
def ri_upwhether the integer part q (remainder r, half h of the unit) moves up one
def ri_q
def ri_kk < 64 fractional bits: q = w >> k, r = w - (q << k), h = 2^(k-1)
def ri_fin
def ri_cls
def to_integral
def trunc
def floor
def ceil
def roundties to even (Python's round(x) and C's rint)
def tu_neg
def tu_int
def tu_big|x| >= 2^52: w << k with k + bit_length(w) <= 64
def tu_fin
def tu_top
def tu_cls
def to_u64x truncated toward zero as an unsigned 64-bit integer: NaN is a domain error, a value outside [0, 2^64) (infinities included) an overflow
def tu32_w
def tu32
def to_u32
def floor_u64
def ceil_u64
def round_u64
def of_u64the double nearest to an unsigned 64-bit integer (exact below 2^53)
def of_u32
type Expa signed exponent: -mag when neg
def exp_pick
def exp_oft - 3000 as a signed exponent
def fx_fin
def fx_z
def fx_cls
def frexp(m, e) with x = m * 2^e and 0.5 <= |m| < 1; zeros and infinities give (x, 0)
def ld_neg
def ld_fin
def ld_e
def ld_z