src/math/f64.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F64

5 imports

import Base
import ./num.bend as N
import ./u64.bend as W
import ./w64.bend as X
import ./natural.bend as M

Types

type F64 source · line 29 · raw

Data

Bits
```
@lo:U32 -> @hi:U32 -> F64
```

type RMode source · line 677 · raw

Data

Trunc
```
RMode
```
Floor
```
RMode
```
Ceil
```
RMode
```
Even
```
RMode
```

type Exp source · line 825 · raw

Data

a signed exponent: -mag when neg

Exp
```
@neg:Bool -> @mag:Nat -> Exp
```

type Ratio source · line 1195 · raw

Data

+-num / 2^den in lowest terms (num odd or den = 0)

Ratio

@neg:Bool -> @num:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @den:Nat -> Ratio

Definitions

def word_lo source · line 32 · raw

@x:F64 -> U32

def word_hi source · line 37 · raw

@x:F64 -> U32

def of_bits source · line 42 · raw

@+hi:U32 -> @+lo:U32 -> F64

def off source · line 45 · raw

Nat

def sgn source · line 48 · raw

@s:Bool -> U32

def signbit source · line 57 · raw

@+x:F64 -> Bool

def exp_field source · line 60 · raw

@+x:F64 -> Nat

def frac source · line 63 · raw

@+x:F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def mag source · line 66 · raw

@+x:F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def nz source · line 69 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Bool

def is_nan source · line 72 · raw

@+x:F64 -> Bool

def is_inf source · line 75 · raw

@+x:F64 -> Bool

def is_finite source · line 78 · raw

@+x:F64 -> Bool

def is_zero source · line 81 · raw

@+x:F64 -> Bool

def nan source · line 86 · raw

F64

def inf source · line 89 · raw

@s:Bool -> F64

def zero source · line 92 · raw

@s:Bool -> F64

def one source · line 95 · raw

F64

def neg source · line 98 · raw

@+x:F64 -> F64

def abs source · line 101 · raw

@+x:F64 -> F64

def copysign source · line 104 · raw

@+x:F64 -> @+y:F64 -> F64

def nan_or source · line 107 · raw

@+x:F64 -> @bad:Bool -> F64

def pack64 source · line 116 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

def pack source · line 121 · raw

@s:Bool -> @+e:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

sign, exponent field e and significand m; the hidden bit of m (bit 52) carries into the exponent field, as packToF64's addition does

def zero_e source · line 124 · raw

@+e:Nat -> @z:Bool -> Nat

def rp_fin3 source · line 131 · raw

@+s:Bool -> @+e:Nat -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

def rp_fin2 source · line 134 · raw

@+s:Bool -> @+e:Nat -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @tie:Bool -> F64

def rp_fin source · line 139 · raw

@+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

sig has its top bit at 62 and e is the plain exponent (0 <= e <= 0x7FD): add half an ulp of the kept 53 bits, shift, and clear bit 0 on a tie

def rp_over source · line 142 · raw

@+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @over:Bool -> F64

def rp_neg source · line 149 · raw

@+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @below:Bool -> F64

def round_pack source · line 157 · raw

@+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

e is the biased exponent minus one, offset by OFF; sig has its top bit at 62

def rp62_pick source · line 161 · raw

@+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @low:Bool -> F64

sig below 2^62 is shifted up once

def rp62 source · line 168 · raw

@+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

def nrp_exp source · line 171 · raw

@+e:Nat -> @+sd:Nat -> @z:Bool -> Nat

def nrp_pick source · line 178 · raw

@+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+sd:Nat -> @direct:Bool -> F64

def nrp_sd source · line 185 · raw

@+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+sd:Nat -> F64

def norm_round_pack source · line 189 · raw

@+s:Bool -> @+e:Nat -> @+sig:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

SoftFloat's normRoundPackToF64 (e offset)

def norm_e source · line 194 · raw

@+e:Nat -> @+f:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Nat

the offset exponent and 53-bit significand (hidden bit at 52) of a nonzero finite value, subnormals normalized (SoftFloat's normSubnormalF64Sig)

def norm_f source · line 201 · raw

@+e:Nat -> @+f:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def am_small source · line 210 · raw

@+e:Nat -> @+f9:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def am_big source · line 218 · raw

@+big:F64 -> @+s:Bool -> @+el:Nat -> @+fl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+es:Nat -> @+fs:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @top:Bool -> F64

|x| + |y| with sign s, the larger exponent eL

def am_eq_n source · line 225 · raw

@+x:F64 -> @+s:Bool -> @+e:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @top:Bool -> F64

def am_eq source · line 232 · raw

@+x:F64 -> @+s:Bool -> @+e:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

def am_case source · line 239 · raw

@+x:F64 -> @+y:F64 -> @+s:Bool -> @+ea:Nat -> @+eb:Nat -> @c:Cmp -> F64

def add_mags source · line 248 · raw

@+x:F64 -> @+y:F64 -> @+s:Bool -> F64

def sm_small source · line 251 · raw

@+e:Nat -> @+f10:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def sm_big source · line 259 · raw

@+big:F64 -> @+s:Bool -> @+el:Nat -> @+fl:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+es:Nat -> @+fs:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @top:Bool -> F64

|big| - |small| with sign s, the larger exponent eL

def sm_exact3 source · line 266 · raw

@+s:Bool -> @+e1:Nat -> @+d:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+sd:Nat -> @under:Bool -> F64

def sm_exact source · line 274 · raw

@+s:Bool -> @+e1:Nat -> @+d:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

an exact difference of equal exponents, normalized without rounding

def sm_eq2 source · line 277 · raw

@+s:Bool -> @+e:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @c:Cmp -> F64

def cmp64 source · line 286 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Cmp

def sm_eq source · line 289 · raw

@+s:Bool -> @+e:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @top:Bool -> F64

def sm_case source · line 296 · raw

@+x:F64 -> @+y:F64 -> @+s:Bool -> @+ea:Nat -> @+eb:Nat -> @c:Cmp -> F64

def sub_mags source · line 305 · raw

@+x:F64 -> @+y:F64 -> @+s:Bool -> F64

def add_pick source · line 308 · raw

@+x:F64 -> @+y:F64 -> @same:Bool -> F64

def add source · line 315 · raw

@+x:F64 -> @+y:F64 -> F64

def sub source · line 318 · raw

@+x:F64 -> @+y:F64 -> F64

def mul_n2 source · line 323 · raw

@+s:Bool -> @+e:Nat -> @p:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64) -> F64

def mul_n source · line 327 · raw

@+s:Bool -> @+ea:Nat -> @+ma:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+mb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

def fin_zero source · line 330 · raw

@+e:Nat -> @+f:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Bool

def mul_z source · line 333 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @z:Bool -> F64

def inf_or_nan source · line 340 · raw

@+s:Bool -> @bad:Bool -> F64

def mul_b source · line 347 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @top:Bool -> F64

def mul_cls source · line 354 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @top:Bool -> F64

def mul source · line 361 · raw

@+x:F64 -> @+y:F64 -> F64

def digit_fin source · line 367 · raw

@+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:U32 -> Pair(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64)

the next quotient digit of r * 2^32 / b (r < b, b >= 2^52) and the remainder

def digit source · line 370 · raw

@+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Nat -> Pair(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64)

def dq_fin source · line 373 · raw

@+s:Bool -> @+e:Nat -> @+d1:U32 -> @p:Pair(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64) -> F64

def dq_mid source · line 377 · raw

@+s:Bool -> @+e:Nat -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Nat -> @p:Pair(U32, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64) -> F64

def div_qt source · line 382 · raw

@+s:Bool -> @+e:Nat -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Nat -> F64

a in [b, 2b): 2^62 + floor((a - b) * 2^62 / b), sticky, by two 32-bit digits

def div_q source · line 385 · raw

@+s:Bool -> @+e:Nat -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

def div_ab source · line 388 · raw

@+s:Bool -> @+ea:Nat -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @less:Bool -> F64

def div_n source · line 395 · raw

@+s:Bool -> @+ea:Nat -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

def div_za source · line 398 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @za:Bool -> F64

def div_z source · line 405 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @zb:Bool -> F64

def div_b source · line 412 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @top:Bool -> F64

def div_cls source · line 419 · raw

@+s:Bool -> @+ea:Nat -> @+fa:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+eb:Nat -> @+fb:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @top:Bool -> F64

def div source · line 426 · raw

@+x:F64 -> @+y:F64 -> F64

def sq_fin source · line 431 · raw

@+e:Nat -> @+t:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @sticky:Bool -> F64

def sq_d2 source · line 435 · raw

@+e:Nat -> @+s0:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+c:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

the root is S0 - 2: remainder (2 S0 - 3) - (D - (2 S0 - 1)) with c = 2 S0 - 1

def sq_d1 source · line 439 · raw

@+e:Nat -> @+s0:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+c:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @small:Bool -> F64

S0^2 - N = D > 0: the root is S0 - 1 when D <= 2 S0 - 1 (remainder c - D)

def sq_neg source · line 446 · raw

@+e:Nat -> @+s0:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

def sq_rem source · line 450 · raw

@+e:Nat -> @+s0:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @ge:Bool -> F64

N - S0^2 = a - b for a = u 2^32, b = q^2: the root is S0 when b <= a

def sq_qu source · line 457 · raw

@+e:Nat -> @+s:U32 -> @+q:U32 -> @+u:U32 -> F64

def sq_clamp source · line 461 · raw

@+e:Nat -> @+s:U32 -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+u:U32 -> @small:Bool -> F64

q = 2^32 (r = 2 s) is taken as q = 2^32 - 1 with u = 2 s

def sq_div source · line 468 · raw

@+e:Nat -> @+s:U32 -> @p:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, U32) -> F64

def sq_root_s source · line 476 · raw

@+e:Nat -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s:U32 -> F64

one 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 source · line 479 · raw

@+e:Nat -> @+nh:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

def sq_even source · line 484 · raw

@+e:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

m * 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 source · line 487 · raw

@+e:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @odd:Bool -> F64

def sq_pos source · line 494 · raw

@+e:Nat -> @+f:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @negative:Bool -> F64

def sq_sign source · line 501 · raw

@+x:F64 -> @negative:Bool -> @+e:Nat -> @+f:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @zr:Bool -> F64

def sq_cls source · line 508 · raw

@+x:F64 -> @s:Bool -> @+e:Nat -> @+f:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @top:Bool -> F64

def sqrt source · line 515 · raw

@+x:F64 -> F64

def lt_s source · line 520 · raw

@+x:F64 -> @+y:F64 -> @sa:Bool -> @sb:Bool -> Bool

def le_s source · line 531 · raw

@+x:F64 -> @+y:F64 -> @sa:Bool -> @sb:Bool -> Bool

def unordered source · line 542 · raw

@+x:F64 -> @+y:F64 -> Bool

def zeros source · line 545 · raw

@+x:F64 -> @+y:F64 -> Bool

def lt_z source · line 548 · raw

@+x:F64 -> @+y:F64 -> @bad:Bool -> @z:Bool -> Bool

def lt source · line 557 · raw

@+x:F64 -> @+y:F64 -> Bool

def le_z source · line 560 · raw

@+x:F64 -> @+y:F64 -> @bad:Bool -> @z:Bool -> Bool

def le source · line 569 · raw

@+x:F64 -> @+y:F64 -> Bool

def eq_z source · line 572 · raw

@+x:F64 -> @+y:F64 -> @bad:Bool -> @z:Bool -> Bool

def eq source · line 581 · raw

@+x:F64 -> @+y:F64 -> Bool

def low_bits source · line 586 · raw

@k:Nat -> @+n:Nat -> Nat

n 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 source · line 593 · raw

@k:Nat -> @+n:Nat -> Nat

def jam_nat source · line 601 · raw

@+d:Nat -> @+n:Nat -> Nat

the jam of n >> d (the bits shifted out OR-ed into bit 0)

def word64 source · line 604 · raw

@+s:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def sig63 source · line 609 · raw

@+n:Nat -> @+b:Nat -> @fits:Bool -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

n 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 source · line 616 · raw

@+n:Nat -> @z:Bool -> F64

def of_nat source · line 624 · raw

@+n:Nat -> F64

the double nearest to n (exact below 2^53)

def pow2 source · line 628 · raw

@+k:Nat -> F64

2^k for k <= 1023

def dmant_z source · line 636 · raw

@+f:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @z:Bool -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

the 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 source · line 643 · raw

@+x:F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def dexp_z source · line 646 · raw

@+e:Nat -> @z:Bool -> Nat

def dexp source · line 653 · raw

@+x:F64 -> Nat

def rw_top source · line 656 · raw

@+s:Bool -> @+x:Nat -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @top:Bool -> F64

def rw_z source · line 663 · raw

@+s:Bool -> @+x:Nat -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @z:Bool -> F64

def round_w source · line 672 · raw

@+s:Bool -> @+x:Nat -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

the 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

def b64 source · line 683 · raw

@b:Bool -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def ri_up source · line 691 · raw

@m:RMode -> @+s:Bool -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Bool

whether the integer part q (remainder r, half h of the unit) moves up one

def ri_q source · line 702 · raw

@m:RMode -> @+s:Bool -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+h:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

def ri_k source · line 706 · raw

@m:RMode -> @+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @small:Bool -> F64

k < 64 fractional bits: q = w >> k, r = w - (q << k), h = 2^(k-1)

def ri_fin source · line 713 · raw

@m:RMode -> @+x:F64 -> @int:Bool -> F64

def ri_cls source · line 720 · raw

@m:RMode -> @+x:F64 -> @top:Bool -> F64

def to_integral source · line 727 · raw

@m:RMode -> @+x:F64 -> F64

def trunc source · line 730 · raw

@+x:F64 -> F64

def floor source · line 733 · raw

@+x:F64 -> F64

def ceil source · line 736 · raw

@+x:F64 -> F64

def round source · line 740 · raw

@+x:F64 -> F64

ties to even (Python's round(x) and C's rint)

def tu_neg source · line 745 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @bad:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

def tu_int source · line 752 · raw

@+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

def tu_big source · line 756 · raw

@+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @fits:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

|x| >= 2^52: w << k with k + bit_length(w) <= 64

def tu_fin source · line 763 · raw

@+x:F64 -> @big:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

def tu_top source · line 770 · raw

@isn:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

def tu_cls source · line 777 · raw

@+x:F64 -> @top:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

def to_u64 source · line 786 · raw

@+x:F64 -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

x 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 source · line 789 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @fits:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>

def tu32 source · line 796 · raw

@r:Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>

def to_u32 source · line 803 · raw

@+x:F64 -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32>

def floor_u64 source · line 806 · raw

@+x:F64 -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

def ceil_u64 source · line 809 · raw

@+x:F64 -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

def round_u64 source · line 812 · raw

@+x:F64 -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64>

def of_u64 source · line 816 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

the double nearest to an unsigned 64-bit integer (exact below 2^53)

def of_u32 source · line 819 · raw

@+u:U32 -> F64

def exp_pick source · line 828 · raw

@+t:Nat -> @pos:Bool -> Exp

def exp_of source · line 836 · raw

@+t:Nat -> Exp

t - 3000 as a signed exponent

def fx_fin source · line 839 · raw

@+x:F64 -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+b:Nat -> Pair(F64, Exp)

def fx_z source · line 842 · raw

@+x:F64 -> @z:Bool -> Pair(F64, Exp)

def fx_cls source · line 849 · raw

@+x:F64 -> @top:Bool -> Pair(F64, Exp)

def frexp source · line 857 · raw

@+x:F64 -> Pair(F64, Exp)

(m, e) with x = m * 2^e and 0.5 <= |m| < 1; zeros and infinities give (x, 0)

def ld_neg source · line 860 · raw

@+x:F64 -> @+k:Nat -> @tiny:Bool -> F64

def ld_fin source · line 867 · raw

@+x:F64 -> @+neg:Bool -> @+k:Nat -> F64

def ld_e source · line 874 · raw

@+x:F64 -> @+e:Exp -> F64

def ld_z source · line 879 · raw

@+x:F64 -> @+e:Exp -> @z:Bool -> F64

def ld_cls source · line 886 · raw

@+x:F64 -> @+e:Exp -> @top:Bool -> F64

def ldexp source · line 894 · raw

@+x:F64 -> @+e:Exp -> F64

x * 2^e, rounded once (overflow to infinity, gradual underflow)

def ulp_cls source · line 897 · raw

@+x:F64 -> @top:Bool -> F64

def ulp source · line 905 · raw

@+x:F64 -> F64

the value of the least significant bit of x (Python's math.ulp)

def with_sign source · line 910 · raw

@+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

def na_step source · line 913 · raw

@+x:F64 -> @up:Bool -> F64

def na_z source · line 920 · raw

@+x:F64 -> @+y:F64 -> @z:Bool -> F64

def na_eq source · line 927 · raw

@+x:F64 -> @+y:F64 -> @same:Bool -> F64

def na_nan source · line 934 · raw

@+x:F64 -> @+y:F64 -> @bad:Bool -> F64

def nextafter source · line 942 · raw

@+x:F64 -> @+y:F64 -> F64

the next double after x toward y (IEEE nextAfter; y when x == y)

def fpick source · line 945 · raw

@+x:F64 -> @+y:F64 -> @first:Bool -> F64

def fmin_z source · line 952 · raw

@+x:F64 -> @+y:F64 -> @z:Bool -> F64

def fmin_ny source · line 959 · raw

@+x:F64 -> @+y:F64 -> @ny:Bool -> F64

def fmin_nx source · line 966 · raw

@+x:F64 -> @+y:F64 -> @nx:Bool -> F64

def fmin source · line 974 · raw

@+x:F64 -> @+y:F64 -> F64

IEEE 754-2019 minimumNumber: a NaN operand is ignored, -0 < +0

def fmax_z source · line 977 · raw

@+x:F64 -> @+y:F64 -> @z:Bool -> F64

def fmax_ny source · line 984 · raw

@+x:F64 -> @+y:F64 -> @ny:Bool -> F64

def fmax_nx source · line 991 · raw

@+x:F64 -> @+y:F64 -> @nx:Bool -> F64

def fmax source · line 999 · raw

@+x:F64 -> @+y:F64 -> F64

IEEE 754-2019 maximumNumber

def is_normal source · line 1004 · raw

@+x:F64 -> Bool

def is_subnormal source · line 1007 · raw

@+x:F64 -> Bool

def to_bits source · line 1010 · raw

@+x:F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64

def of_bits64 source · line 1013 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

def ii_k source · line 1016 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @small:Bool -> Bool

def ii_fin source · line 1023 · raw

@+x:F64 -> @int:Bool -> Bool

def is_integer source · line 1031 · raw

@+x:F64 -> Bool

finite with no fractional bits

def mf_frac source · line 1036 · raw

@+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+u:Nat -> @+k:Nat -> @small:Bool -> F64

def mf_fin source · line 1043 · raw

@+x:F64 -> @int:Bool -> Pair(F64, F64)

def mf_cls source · line 1050 · raw

@+x:F64 -> @top:Bool -> Pair(F64, F64)

def modf source · line 1058 · raw

@+x:F64 -> Pair(F64, F64)

(fractional part, integral part), both with the sign of x (Python's modf)

def fm_go source · line 1063 · raw

@fuel:Nat -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+d:Nat -> @st:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64) -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64)

(q, r) of mx * 2^d by b from (q0, r0) of mx by b: ten bits a step, so each partial remainder r * 2^t stays below 2^63

def fm_qr source · line 1073 · raw

@+x:F64 -> @+y:F64 -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64)

the last quotient digit and remainder of mant(x) * 2^(e(x) - e(y)) by mant(y)

def fmod_fin source · line 1076 · raw

@+x:F64 -> @+y:F64 -> @far:Bool -> F64

def fmod_z source · line 1083 · raw

@+x:F64 -> @+y:F64 -> @zx:Bool -> F64

def fmod_yi source · line 1090 · raw

@+x:F64 -> @+y:F64 -> @yi:Bool -> F64

def fmod_bad source · line 1097 · raw

@+x:F64 -> @+y:F64 -> @bad:Bool -> F64

def fmod source · line 1105 · raw

@+x:F64 -> @+y:F64 -> F64

x - n y for n = trunc(x / y), exact, with the sign of x (C's fmod)

def rm_pick source · line 1108 · raw

@+s:Bool -> @+u:Nat -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @flip:Bool -> F64

def rm_fix source · line 1117 · raw

@+s:Bool -> @+u:Nat -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+q:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> F64

remainder r of divisor b at scale u, last quotient digit q: round the quotient to nearest (ties to even) by flipping to r - b

def rm_qr source · line 1120 · raw

@+x:F64 -> @+y:F64 -> @p:Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64) -> F64

def rm_near source · line 1124 · raw

@+x:F64 -> @+y:F64 -> @one:Bool -> F64

def rm_far source · line 1131 · raw

@+x:F64 -> @+y:F64 -> @far:Bool -> F64

def rm_z source · line 1138 · raw

@+x:F64 -> @+y:F64 -> @zx:Bool -> F64

def rm_yi source · line 1145 · raw

@+x:F64 -> @+y:F64 -> @yi:Bool -> F64

def rm_bad source · line 1152 · raw

@+x:F64 -> @+y:F64 -> @bad:Bool -> F64

def remainder source · line 1160 · raw

@+x:F64 -> @+y:F64 -> F64

IEEE remainder: x - n y for n = x / y rounded to nearest, ties to even

def ic_d source · line 1165 · raw

@+a:F64 -> @+b:F64 -> @+rel:F64 -> @+at:F64 -> @+d:F64 -> Bool

def ic_inf source · line 1168 · raw

@+a:F64 -> @+b:F64 -> @+rel:F64 -> @+at:F64 -> @big:Bool -> Bool

def ic_eq source · line 1175 · raw

@+a:F64 -> @+b:F64 -> @+rel:F64 -> @+at:F64 -> @same:Bool -> Bool

def ic_tol source · line 1182 · raw

@+a:F64 -> @+b:F64 -> @+rel:F64 -> @+at:F64 -> @bad:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Bool>

def isclose source · line 1191 · raw

@+a:F64 -> @+b:F64 -> @+rel:F64 -> @+at:F64 -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Bool>

Python's math.isclose (CPython's algorithm): a negative tolerance is a domain error

def ctz_go source · line 1199 · raw

@fuel:Nat -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @odd:Bool -> Nat

trailing zeros of w (at most fuel), one halving at a time

def ctz source · line 1208 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Nat

def ar_small source · line 1211 · raw

@+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @+j:Nat -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Ratio>

def ar_big source · line 1214 · raw

@+s:Bool -> @+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+k:Nat -> @fits:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Ratio>

def ar_fin source · line 1221 · raw

@+x:F64 -> @big:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Ratio>

def ar_z source · line 1228 · raw

@+x:F64 -> @z:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Ratio>

def ar_top source · line 1235 · raw

@isn:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Ratio>

def ar_cls source · line 1242 · raw

@+x:F64 -> @top:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Ratio>

def as_integer_ratio source · line 1252 · raw

@+x:F64 -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Ratio>

x = +-num / 2^den exactly, in lowest terms (Python's as_integer_ratio with the denominator's exponent); NaN is a domain error, infinities and integers of 2^64 or more overflow

def f64_op source · line 1257 · raw

@o:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<F64> -> F64

def f64_is source · line 1290 · raw

@t:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<F64> -> Bool