~/bend-docscommunity

spec/math/generic.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as Generic

8 imports
import Base
import ../lib/common.bend as C
import ../../src/math/num.bend as N
import ../../src/math/generic.bend as G
import ../../src/math/natural.bend as M
import ./natural.bend as NS
import ./w64.bend as SW
import ../../src/math/u64.bend as W

Definitions

def fits source · line 60 · raw

@+w:Nat -> @+n:Nat -> Bool

n fits w bits: n < 2^w (spec/lib/common.bend states it without 2^w)

def err source · line 74 · raw

@e:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.MathError -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError

def lift_nat source · line 91 · raw

@r:Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.MathError, Nat> -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>

def pick source · line 112 · raw

@-T:Data -> @c:Bool -> @+a:T -> @+b:T -> T

def prod_go source · line 121 · raw

@+w:Nat -> @xs:List<&2, Nat> -> @+acc:Nat -> @ok:Bool -> Pair(Nat, Bool)

a fold that stops at the first prefix of w bits or more (prod, lcm_all: a later 0 can shrink the value, the overflow already happened)

def lcm_go source · line 130 · raw

@+w:Nat -> @xs:List<&2, Nat> -> @+acc:Nat -> @ok:Bool -> Pair(Nat, Bool)

def u32_val source · line 278 · raw

@x:U32 -> Nat

---- instance models ---- U32: the value and the U32 of a value below 2^32 (width 32)

def u32_of source · line 281 · raw

@n:Nat -> U32

def u64_val source · line 285 · raw

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

U64: the two-limb value and the U64 of a value below 2^64 (width 64)

def u64_of source · line 288 · raw

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

Templates

template checked_pick source · line 63 · raw

@-T:Data -> @-of:(@_:Nat -> T) -> @+n:Nat -> @ok:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, T>

template checked source · line 71 · raw

@-T:Data -> @-of:(@_:Nat -> T) -> @+w:Nat -> @+n:Nat -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, T>

n as a T, or Overflow when it needs more than w bits

template lift source · line 84 · raw

@-T:Data -> @-of:(@_:Nat -> T) -> @r:Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.MathError, Nat> -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, T>

a Nat result carried to T (values that are no larger than an argument)

template lift_qr source · line 98 · raw

@-T:Data -> @-of:(@_:Nat -> T) -> @r:Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.MathError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/natural.QuotRem> -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/generic.QuotRem<T>>

template vals source · line 105 · raw

@-T:Data -> @-val:(@_:T -> Nat) -> @xs:List<&2, T> -> List<&2, Nat>

template prefix_fin source · line 139 · raw

@-T:Data -> @-of:(@_:Nat -> T) -> @r:Pair(Nat, Bool) -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, T>

template Gcd.agrees source · line 145 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+a:T -> @+b:T -> Type

template Lcm.checked source · line 148 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+w:Nat -> @+a:T -> @+b:T -> Type

template GcdAll.agrees source · line 151 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @xs:List<&2, T> -> Type

template LcmAll.checked source · line 154 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+w:Nat -> @xs:List<&2, T> -> Type

template Isqrt.agrees source · line 157 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+n:T -> Type

template Iroot.agrees source · line 160 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+n:T -> @+k:Nat -> Type

template Ilog.agrees source · line 163 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @+n:T -> @+b:T -> Type

template Factorial.checked source · line 166 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+w:Nat -> @+n:T -> Type

template Perm.checked source · line 169 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+w:Nat -> @+n:T -> @+k:T -> Type

template Comb.checked source · line 172 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+w:Nat -> @+n:T -> @+k:T -> Type

template PowMod.agrees source · line 175 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+b:T -> @+e:T -> @+m:T -> Type

template ModInverse.agrees source · line 178 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+a:T -> @+m:T -> Type

template DivMod.agrees source · line 181 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+a:T -> @+b:T -> Type

template BitLength.agrees source · line 184 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @+n:T -> Type

template Clamp.agrees source · line 187 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+x:T -> @+lo:T -> @+hi:T -> Type

template Min.agrees source · line 190 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+a:T -> @+b:T -> Type

template Max.agrees source · line 193 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+a:T -> @+b:T -> Type

template Abs.identity source · line 197 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+x:T -> Type

unsigned: |x| is x

template Sign.agrees source · line 201 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+x:T -> Type

unsigned: 1 above zero, else 0

template Sum.checked source · line 205 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+w:Nat -> @xs:List<&2, T> -> Type

the partial sums only grow, so the sum overflows exactly when the total does

template Prod.checked source · line 208 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+w:Nat -> @xs:List<&2, T> -> Type

template Pow.checked source · line 211 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @-val:(@_:T -> Nat) -> @-of:(@_:Nat -> T) -> @+w:Nat -> @+x:T -> @+k:Nat -> Type

template FMin.select source · line 218 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+a:T -> @+b:T -> Type

template FMax.select source · line 221 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+a:T -> @+b:T -> Type

template fclamp_pick source · line 224 · raw

@-T:Data -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+x:T -> @+lo:T -> @+hi:T -> @bad:Bool -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, T>

template FClamp.select source · line 232 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+x:T -> @+lo:T -> @+hi:T -> Type

Domain when hi < lo; else min(max(x, lo), hi) by the two selections

template FAbs.value source · line 235 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+x:T -> Type

template FSign.select source · line 239 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+x:T -> Type

1 above zero, -1 below, x itself otherwise (zeros keep their sign, NaN stays)

template fold_add source · line 242 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @xs:List<&2, T> -> @+acc:T -> T

template fold_mul source · line 249 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @xs:List<&2, T> -> @+acc:T -> T

template FSum.fold source · line 257 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @xs:List<&2, T> -> Type

((0 + x0) + x1) + ..., every addition rounded

template FProd.fold source · line 260 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @xs:List<&2, T> -> Type

template binpow source · line 266 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @fuel:Nat -> @+k:Nat -> @+base:T -> @+acc:T -> T

right-to-left binary exponentiation: acc *= base on a 1 bit, base *= base while bits remain, each product rounded (k = 0 is a fixed point, so any fuel past k's bit length gives the same result)

template FPow.binary source · line 273 · raw

@-T:Data -> @-op:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Op<T> -> T) -> @-test:(@_:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.Test<T> -> Bool) -> @+x:T -> @+k:Nat -> Type