generator

Generators of random values, for properties, after Hedgehog: a generator makes a value together with every smaller value to try instead of it, a rose tree, so that each generator shrinks, and a generator made of others shrinks by theirs — there is no shrink to write apart, and none to get out of step with the generator. A generator is a pure function of a seed and a size; a property draws from it by an effect (check.forAll), which the runner gives. Generators are values passed by hand: there is no search for “the” generator of a type. Import it by a name, import generator as Generator, as it has a map, a list and an int.

Seed

data Seed = MkSeed Int

Where a random value comes from: a state of a congruential generator modulo the prime 2^31 - 1, split in two by two different steps, a value drawn from it by a third step and a fifth power (which mixes what the steps, being linear, do not, and loses nothing: modulo this prime, no two numbers have the same fifth power). It is no cryptographic generator: enough to spread the values a test tries, the same seed always making the same value.

modulus

modulus : Int

seed

seed : Int -> Seed

A seed from any number (as heff test --seed N gives it).

split

split : Seed -> (Seed, Seed)

Two seeds from one: what a generator draws from the first does not change what is drawn from the second.

bounded

bounded : Int -> Seed -> Int

A number from 0 to n - 1 (n at least 1), from the seed.

Tree

data Tree a = Node a (List (Unit -> Tree a))

A value and the smaller ones to try instead, each with its own: each is made only when it is asked for, as a shrink is tried only while the ones before it did not fail.

root

root : {a : Type} -> Tree a -> a

children

children : {a : Type} -> Tree a -> List (Unit -> Tree a)

mapTree

mapTree : {a b : Type} -> (a -> b) -> Tree a -> Tree b

bindTree

bindTree : {a b : Type} -> Tree a -> (a -> Tree b) -> Tree b

A tree of trees, as one: the outer value’s shrinks first, each with the inner value made again from it, then the inner value’s.

Generator

data Generator a = MkGenerator (Seed -> Int -> Tree a)

A generator: from a seed and a size (0 to 100, growing over a property’s runs, so that the first values tried are small), a value and its shrinks.

run

run : {a : Type} -> Generator a -> Seed -> Int -> Tree a

The tree a generator makes from a seed, at a size.

sample

sample : {a : Type} -> Generator a -> List a

Values made from 10 seeds, at sizes growing to 100: what a generator makes, for a look at it.

constant

constant : {a : Type} -> a -> Generator a

Always x, which does not shrink.

map

map : {a b : Type} -> (a -> b) -> Generator a -> Generator b

f of what g makes; it shrinks as g does.

bind

bind : {a b : Type} -> Generator a -> (a -> Generator b) -> Generator b

A value of g, and a generator made from it: shrinking tries the first value’s shrinks first, the second made again from each.

pure

pure : {a : Type} -> a -> Generator a

instanceMonadGenerator

instance instanceMonadGenerator : Prelude.Monad Generator

A generator as a [Monad]: [pure] and [bind], what do takes by name.

map2

map2 : {a b c : Type}
     -> (a -> b -> c)
     -> Generator a
     -> Generator b
     -> Generator c

f of what both make.

pair

pair : {a b : Type} -> Generator a -> Generator b -> Generator (a, b)

Both, as a pair.

resize

resize : {a : Type} -> Int -> Generator a -> Generator a

The generator at the size given, whatever the size is.

sized

sized : {a : Type} -> (Int -> Generator a) -> Generator a

A generator chosen by the size.

towards

towards : Int -> Int -> List Int

The values to try instead of x, nearer o: o itself first, then ever nearer x, so that the search for the smallest that fails is a binary one.

>>> towards 0 100
Cons 0 (Cons 50 (Cons 75 (Cons 88 (Cons 94 (Cons 97 (Cons 99 Nil))))))

int

int : Int -> Int -> Generator Int

A number from lo to hi, shrinking toward the one nearest 0. The range grows with the size, from that number at size 0 to all of it at 100.

>>> sample (int 0 9)
Cons 0 (Cons 1 (Cons 2 (Cons 1 (Cons 2 (Cons 0 (Cons 6 (Cons 7 (Cons 4 (Cons 7 Nil)))))))))

uniform

uniform : Int -> Int -> Generator Int

A number from lo to hi, any of them as likely at any size, shrinking toward lo.

bool

bool : Generator Bool

False or True, shrinking to False.

NonEmptyList

data NonEmptyList a = MkNonEmptyList a (List a)

A list of one element at least: the first, and the rest — what element, oneOf and frequency choose from.

element

element : {a : Type} -> NonEmptyList a -> Generator a

One of these, shrinking toward the first.

>>> sample (element (MkNonEmptyList "a" ["b", "c"]))
Cons "c" (Cons "a" (Cons "c" (Cons "b" (Cons "c" (Cons "a" (Cons "b" (Cons "c" (Cons "b" (Cons "b" Nil)))))))))

oneOf

oneOf : {a : Type} -> NonEmptyList (Generator a) -> Generator a

What one of these makes, shrinking toward the first.

frequency

frequency : {a : Type} -> NonEmptyList (Int, Generator a) -> Generator a

What one of these makes, each as often as its weight says, shrinking toward the first. (Of weights all 0, each as often as the others, as oneOf chooses.)

>>> sample (frequency (MkNonEmptyList (MkPair 0 (constant "a")) [MkPair 0 (constant "b")]))
Cons "a" (Cons "b" (Cons "a" (Cons "a" (Cons "b" (Cons "a" (Cons "b" (Cons "a" (Cons "a" (Cons "a" Nil)))))))))

maybe

maybe : {a : Type} -> Generator a -> Generator (Prelude.Maybe a)

Nothing now and then, else Just of what g makes; it shrinks to Nothing.

interleave

interleave : {a : Type} -> Int -> List (Tree a) -> Tree (List a)

The list of these trees’ values, shrinking by fewer elements (lo at least), then by smaller ones.

list

list : {a : Type} -> Int -> Int -> Generator a -> Generator (List a)

A list of lo to hi elements of g, longer with the size, shrinking to fewer and smaller elements.

>>> root (run (list 0 3 (int 0 9)) (seed 1) 100)
Cons 8 (Cons 1 Nil)

string

string : Int -> Int -> NonEmptyList Rune -> Generator String

A string of lo to hi of the characters of alphabet (whatever units each takes).

shrinks

shrinks : {a : Type} -> Tree a -> List a

The shrinks of a tree, a level deep: what a generator tries first instead of what it made.

(both elements taken out, then each one, then the 8 made smaller, then the 1)

>>> shrinks (run (list 0 3 (int 0 9)) (seed 1) 100)
Cons Nil (Cons (Cons 1 Nil) (Cons (Cons 8 Nil) (Cons (Cons 0 (Cons 1 Nil)) (Cons (Cons 4 (Cons 1 Nil)) (Cons (Cons 6 (Cons 1 Nil)) (Cons (Cons 7 (Cons 1 Nil)) (Cons (Cons 8 (Cons 0 Nil)) Nil)))))))