spec/math/random/rand.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/spec/math/random/rand.bend as Rand

5 imports

import Base
import ../../lib/common.bend as C
import ../../../src/math/u64.bend as W
import ../w64.bend as SW
import ./source.bend as SRC

Definitions

def b2n source · line 31 · raw

@b:Bool -> Nat

def and_bits source · line 38 · raw

@w:Nat -> @+a:Nat -> @+b:Nat -> Nat

def pow2mod source · line 45 · raw

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

def accept source · line 52 · raw

@+hi:Nat -> @ok:Bool -> Maybe<&2, Nat>

def lemire source · line 60 · raw

@+w:Nat -> @+n:Nat -> @+hi:Nat -> @+lo:Nat -> Maybe<&2, Nat>

Lemire: the product x * n = hi * 2^w + lo

def draw_pos source · line 63 · raw

@+w:Nat -> @+x:Nat -> @+n:Nat -> @+m:Nat -> @pow2:Bool -> Maybe<&2, Nat>

def draw source · line 70 · raw

@+w:Nat -> @+x:Nat -> @n:Nat -> Maybe<&2, Nat>

def hit source · line 77 · raw

@m:Maybe<&2, Nat> -> @+k:Nat -> Nat

def count source · line 85 · raw

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

the number of source outputs x < N that draw k

Templates

template below_go source · line 96 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @fuel:Nat -> @+n:Nat -> @m:Maybe<&2, Nat> -> @+x:Nat -> @+s:S -> Pair(Nat, S)

the bounded draw once a draw of x (with verdict m) has left state s: m if accepted, else (while fuel lasts) the next draw; with no fuel left, the last candidate floor(x n / 2^64). The verdict is matched before the recursion, so a draw that is not yet decided keeps the rest unexpanded.

template below source · line 108 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64, S)) -> @fuel:Nat -> @+n:Nat -> @+s:S -> Pair(Nat, S)

the first accepted draw of 64-bit outputs among fuel + 1 draws

template occurrences source · line 111 · raw

@-A:Data -> @-V:Data -> @-rel:(@_:A -> @_:V -> Bool) -> @+v:V -> @xs:List<&2, A> -> Nat