Idris2Doc : Hedgehog.Internal.Gen

Hedgehog.Internal.Gen

(source)
Definitions
record Gen : Type -> Type
  Generates random values of type `a`

  Totality: total
  Visibility: public export
  Constructor: 
MkGen : (Size -> StdGen -> Cotree a) -> Gen a

  Projection: 
.unGen : Gen a -> Size -> StdGen -> Cotree a

  Hints:
  
Applicative Gen
  
Functor Gen
  
Monad Gen
.unGen : Gen a -> Size -> StdGen -> Cotree a
  Totality: total
  Visibility: public export
unGen : Gen a -> Size -> StdGen -> Cotree a
  Totality: total
  Visibility: public export
runGen : Size -> StdGen -> Gen a -> Cotree a
  Totality: total
  Visibility: public export
mapGen : (Cotree a -> Cotree b) -> Gen a -> Gen b
  Totality: total
  Visibility: public export
fromTree : Cotree a -> Gen a
  Lift a predefined shrink tree in to a generator, ignoring the seed and the
  size.

  Totality: total
  Visibility: public export
toTree : Gen a -> Gen (Cotree a)
  Observe a generator's shrink tree.

  Totality: total
  Visibility: public export
generate : (Size -> StdGen -> a) -> Gen a
  Totality: total
  Visibility: public export
shrink : (a -> Colist a) -> Gen a -> Gen a
  Totality: total
  Visibility: public export
prune : Gen a -> Gen a
  Totality: total
  Visibility: public export
sized : (Size -> Gen a) -> Gen a
  Construct a generator that depends on the size parameter.

  Totality: total
  Visibility: public export
scale : (Size -> Size) -> Gen a -> Gen a
  Adjust the size parameter by transforming it with the given function.

  Totality: total
  Visibility: public export
resize : Size -> Gen a -> Gen a
  Override the size parameter. Returns a generator which uses the given size
  instead of the runtime-size parameter.

  Totality: total
  Visibility: public export
golden : Size -> Size
  Scale a size using the golden ratio.
  
    > golden x = x / φ
    > golden x = x / 1.61803..

  Totality: total
  Visibility: public export
small : Gen a -> Gen a
  Make a generator smaller by scaling its size parameter.

  Totality: total
  Visibility: public export
integral_ : ToInteger a => Range a -> Gen a
  Generates a random integral number in the [inclusive,inclusive] range.
  
  This generator does not shrink.

  Totality: total
  Visibility: public export
integral : ToInteger a => Range a -> Gen a
  Generates a random integral number in the given @[inclusive,inclusive]@ range.
  
  When the generator tries to shrink, it will shrink towards the
  'Range.origin' of the specified 'Range'.
  
  For example, the following generator will produce a number between @1970@
  and @2100@, but will shrink towards @2000@:
  
  ```
  integral (Range.'Range.constantFrom' 2000 1970 2100) :: 'Gen' 'Int'
  ```
  
    Some sample outputs from this generator might look like:
  
    > === Outcome ===
    > 1973
    > === Shrinks ===
    > 2000
    > 1987
    > 1980
    > 1976
    > 1974
  
    > === Outcome ===
    > 2061
    > === Shrinks ===
    > 2000
    > 2031
    > 2046
    > 2054
    > 2058
    > 2060
  

  Totality: total
  Visibility: public export
int : Range Int -> Gen Int
  Generates a random machine integer in the given range.
  
  This is a specialization of `integral`, offered for convenience.

  Totality: total
  Visibility: public export
int8 : Range Int8 -> Gen Int8
  Generates a random 8-bit integer in the given range.
  
  This is a specialization of `integral`, offered for convenience.

  Totality: total
  Visibility: public export
anyInt8 : Gen Int8
  Generates a random 8-bit integer in the full available range.
  
  This shrinks exponentially towards 0.

  Totality: total
  Visibility: public export
int16 : Range Int16 -> Gen Int16
  Generates a random 16-bit integer in the given range.
  
  This is a specialization of `integral`, offered for convenience.

  Totality: total
  Visibility: public export
anyInt16 : Gen Int16
  Generates a random 16-bit integer in the full available range.
  
  This shrinks exponentially towards 0.

  Totality: total
  Visibility: public export
int32 : Range Int32 -> Gen Int32
  Generates a random 32-bit integer in the given range.
  
  This is a specialization of `integral`, offered for convenience.

  Totality: total
  Visibility: public export
anyInt32 : Gen Int32
  Generates a random 32-bit integer in the full available range.
  
  This shrinks exponentially towards 0.

  Totality: total
  Visibility: public export
int64 : Range Int64 -> Gen Int64
  Generates a random 64-bit integer in the given range.
  
  This is a specialization of `integral`, offered for convenience.

  Totality: total
  Visibility: public export
anyInt64 : Gen Int64
  Generates a random 64-bit integer in the full available range.
  
  This shrinks exponentially towards 0.

  Totality: total
  Visibility: public export
bits8 : Range Bits8 -> Gen Bits8
  Generates a random 8-bit integer in the given range.
  
  This is a specialization of 'integral', offered for convenience.

  Totality: total
  Visibility: public export
anyBits8 : Gen Bits8
  Generates a random 8-bit signed integer in the full available range.
  
  This shrinks exponentially towards 0.

  Totality: total
  Visibility: public export
bits16 : Range Bits16 -> Gen Bits16
  Generates a random 16-bit integer in the given range.
  
  This is a specialization of 'integral', offered for convenience.

  Totality: total
  Visibility: public export
anyBits16 : Gen Bits16
  Generates a random 16-bit signed integer in the full available range.
  
  This shrinks exponentially towards 0.

  Totality: total
  Visibility: public export
bits32 : Range Bits32 -> Gen Bits32
  Generates a random 32-bit integer in the given range.
  
  This is a specialization of 'integral', offered for convenience.

  Totality: total
  Visibility: public export
anyBits32 : Gen Bits32
  Generates a random 32-bit signed integer in the full available range.
  
  This shrinks exponentially towards 0.

  Totality: total
  Visibility: public export
bits64 : Range Bits64 -> Gen Bits64
  Generates a random 64-bit integer in the given range.
  
  This is a specialization of 'integral', offered for convenience.

  Totality: total
  Visibility: public export
anyBits64 : Gen Bits64
  Generates a random 64-bit signed integer in the full available range.
  
  This shrinks exponentially towards 0.

  Totality: total
  Visibility: public export
integer : Range Integer -> Gen Integer
  Generates a random Integer in the given range.
  
  This is a specialization of 'integral', offered for convenience.

  Totality: total
  Visibility: public export
nat : Range Nat -> Gen Nat
  Generates a random Nat in the given range.
  
  This is a specialization of 'integral', offered for convenience.

  Totality: total
  Visibility: public export
size : Range Size -> Gen Size
  Generates a random Size in the given range.
  
  This is a specialization of 'integral', offered for convenience.

  Totality: total
  Visibility: public export
fin : Range (Fin n) -> Gen (Fin n)
  Generates a random (Fin n) in the given range.

  Totality: total
  Visibility: public export
double_ : Range Double -> Gen Double
  Generates a random fractional number in the [inclusive,exclusive) range.
  
  This generator does not shrink.

  Totality: total
  Visibility: export
double : Range Double -> Gen Double
  Generates a random floating-point number in the given range.
  
  This generator works the same as 'integral', but for floating point numbers.
  

  Totality: total
  Visibility: export
constant : a -> Gen a
  Trivial generator that always produces the same element.
  
  This is another name for `pure`.

  Totality: total
  Visibility: public export
element : Vect (S k) a -> Gen a
  Randomly selects one of the elements in the vector.
  
  This generator shrinks towards the first element in the vector.

  Totality: total
  Visibility: public export
element_ : Vect (S k) a -> Gen a
  Randomly selects one of the elements in the vector.
  
  This generator does not shrink.

  Totality: total
  Visibility: public export
choice : Vect (S k) (Gen a) -> Gen a
  Randomly selects one of the generators in the vector.
  
  This generator shrinks towards the first generator in the vector.

  Totality: total
  Visibility: public export
choice_ : Vect (S k) (Gen a) -> Gen a
  Randomly selects one of the generators in the vector.
  
  This generator does not shrink towards a particular
  generator in the vector

  Totality: total
  Visibility: public export
frequency : Vect (S k) (Nat, Gen a) -> Gen a
  Uses a weighted distribution to randomly select one of the generators in
  the vector.
  
  This generator shrinks towards the first generator in the vector.
  
  Note that if the given frequencies sum up to 0, the first element
  of the vector

  Totality: total
  Visibility: public export
bool : Gen Bool
  Generates a random boolean.
  
  This generator shrinks to `False`.

  Totality: total
  Visibility: public export
unit : Gen ()
  Generates constant values of type `Unit"

  Totality: total
  Visibility: export
char : Range Char -> Gen Char
  Generates a character in the given `Range`.
  
  Shrinks towards the origin of the range.

  Totality: total
  Visibility: export
charc : Char -> Char -> Gen Char
  Generates a character in the interval [lower,uppper].
  
  Shrinks towards the lower value.

  Totality: total
  Visibility: export
binit : Gen Char
  Generates an ASCII binit: `'0'..'1'`

  Totality: total
  Visibility: export
octit : Gen Char
  Generates an ASCII octit: `'0'..'7'`

  Totality: total
  Visibility: export
digit : Gen Char
  Generates an ASCII digit: `'0'..'9'`

  Totality: total
  Visibility: export
hexit : Gen Char
  Generates an ASCII hexit: `'0'..'9', 'a'..'f', 'A'..'F'`

  Totality: total
  Visibility: export
lower : Gen Char
  Generates an ASCII lowercase letter: `'a'..'z'`

  Totality: total
  Visibility: export
upper : Gen Char
  Generates an ASCII uppercase letter: `'A'..'Z'`

  Totality: total
  Visibility: export
alpha : Gen Char
  Generates an ASCII letter: `'a'..'z', 'A'..'Z'`

  Totality: total
  Visibility: export
alphaNum : Gen Char
  Generates an ASCII letter or digit: `'a'..'z', 'A'..'Z', '0'..'9'`

  Totality: total
  Visibility: export
ascii : Gen Char
  Generates an ASCII character: `'\0'..'\127'`

  Totality: total
  Visibility: export
printableAscii : Gen Char
  Generates an printable ASCII character: `'\32'..'\126'`
  Note: This includes the space character but no
        line breaks or tabs

  Totality: total
  Visibility: export
latin : Gen Char
  Generates a latin character: `'\0'..'\255'`

  Totality: total
  Visibility: export
printableLatin : Gen Char
  Generates a printable latin character: `'\32'..'\126'` and `'\160'..'\255'`

  Totality: total
  Visibility: export
unicode : Gen Char
  Generates a Unicode character, excluding noncharacters
  and invalid standalone surrogates:
  `'\0'..'\1114111'` (excluding '\55296'..'\57343', '\65534', '\65535')`

  Totality: total
  Visibility: export
printableUnicode : Gen Char
  Generates a printable Unicode character, excluding noncharacters
  and invalid standalone surrogates:
  `'\0'..'\1114111'` (excluding '\0' .. '\31', '\127' .. '\159',
  '\55296'..'\57343', and '\65534', '\65535')`

  Totality: total
  Visibility: export
unicodeAll : Gen Char
  Generates a Unicode character, including noncharacters
  but excluding invalid standalone surrogates: `0000..10FFFF`
  (excluding D800..DFFFF)

  Totality: total
  Visibility: export
maybe : Gen a -> Gen (Maybe a)
  Generates a 'Nothing' some of the time.

  Totality: total
  Visibility: export
either : Gen a -> Gen b -> Gen (Either a b)
  Generates either an 'a' or a 'b'.
  
  As the size grows, this generator generates @Right@s more often than @Left@s.

  Totality: total
  Visibility: export
either_ : Gen a -> Gen b -> Gen (Either a b)
  Generates either an 'a' or a 'b', without bias.
  
  This generator generates as many @Right@s as it does @Left@s.

  Totality: total
  Visibility: export
vect : (n : Nat) -> Gen a -> Gen (Vect n a)
  Generates a list using a 'Range' to determine the length.

  Totality: total
  Visibility: export
list : Range Nat -> Gen a -> Gen (List a)
  Generates a list using a 'Range' to determine the length.

  Totality: total
  Visibility: export
snocList : Range Nat -> Gen a -> Gen (SnocList a)
  Generates a snoc list using a 'Range' to determine the length.

  Totality: total
  Visibility: export
list1 : Range Nat -> Gen a -> Gen (List1 a)
  Generates a non-empty list using a `Range` to determine the length.

  Totality: total
  Visibility: export
string : Range Nat -> Gen Char -> Gen String
  Generates a string using 'Range' to determine the length.

  Totality: total
  Visibility: export
hlist : All Gen ts -> Gen (HList ts)
  Generates an heterogeneous list being provided a generator for each element

  Totality: total
  Visibility: export
hvect : All Gen ts -> Gen (HVect ts)
  Generates an heterogeneous vect being provided a generator for each element

  Totality: total
  Visibility: export
np : NP Gen ts -> Gen (NP I ts)
  Turns an n-ary product of generators into a generator
  of n-ary products of the same type.

  Totality: total
  Visibility: export
ns : NP Gen ts -> {auto 0 _ : NonEmpty ts} -> Gen (NS I ts)
  Turns an n-ary product of generators into a generator
  of n-ary sums of the same type. This is a generalisation
  of choice and shrinks towards the first sum type
  in the list.

  Totality: total
  Visibility: export
ns_ : NP Gen ts -> {auto 0 _ : NonEmpty ts} -> Gen (NS I ts)
  Turns an n-ary product of generators into a generator
  of n-ary sums of the same type. This is a generalisation
  of `choice_` and does not shrink towards a particular
  sum type.

  Totality: total
  Visibility: export
sop : POP Gen tss -> {auto 0 _ : NonEmpty tss} -> Gen (SOP I tss)
  Totality: total
  Visibility: export
printWith : (HasIO io, Show a) => Size -> StdGen -> Gen a -> io ()
  Print the value produced by a generator, and the first level of shrinks,
  for the given size and seed.
  
  Use 'print' to generate a value from a random seed.

  Totality: total
  Visibility: export
print : Show a => HasIO io => Gen a -> io ()
  Run a generator with a random seed and print the outcome, and the first
  level of shrinks.
  
  @
  Gen.print (Gen.'enum' \'a\' \'f\')
  @
  
    > === Outcome ===
    > 'd'
    > === Shrinks ===
    > 'a'
    > 'b'
    > 'c'

  Totality: total
  Visibility: export
sample : HasIO io => Gen a -> io a
  Generate a sample from a generator.

  Totality: total
  Visibility: export
renderTree : Show a => Nat -> Nat -> Size -> StdGen -> Gen a -> String
  Render the shrink tree produced by a generator, for the given size and
  seed up to the given depth and width.

  Totality: total
  Visibility: export
printTreeWith : Show a => HasIO io => Nat -> Nat -> Size -> StdGen -> Gen a -> io ()
  Print the shrink tree produced by a generator, for the given size and
  seed.
  
  Use 'printTree' to generate a value from a random seed.

  Totality: total
  Visibility: export
printTree : Show a => HasIO io => Nat -> Nat -> Gen a -> io ()
  Run a generator with a random seed and print the resulting shrink tree.
  
  @
  Gen.printTree (Gen.'enum' \'a\' \'f\')
  @
  
    > 'd'
    >  ├╼'a'
    >  ├╼'b'
    >  │  └╼'a'
    >  └╼'c'
    >     ├╼'a'
    >     └╼'b'
    >        └╼'a'
  
    /This may not terminate when the tree is very large./
  

  Totality: total
  Visibility: export