Test.DepTyCheck.Gen

Reexports

Definitions

wrapLazy : (a -> b) -> Lazy a -> Lazy b

Totality: total
Visibility: public export

data Gen : Emptiness -> Type -> Type

Totality: total
Visibility: export
Constructors:

Empty : Gen MaybeEmpty a

Pure : a -> Gen em a

Raw : RawGen a -> Gen em a

OneOf : (gs : GenAlternatives True alem a) -> {auto 0 _ : All IsNonEmpty gs} -> {auto 0 _ : alem `NoWeaker` em} -> Gen em a

Bind : {auto 0 _ : biem `NoWeaker` em} -> RawGen c -> (c -> Gen biem a) -> Gen em a

Labelled : Label -> (g : Gen em a) -> {auto 0 _ : IsNonEmpty g} -> Gen em a

Hints:

Applicative (Gen em)

Functor (Gen em)

Monad (Gen em)

record GenAlternatives : (0 _ : Bool) -> (0 _ : Emptiness) -> Type -> Type

Totality: total
Visibility: export
Constructor: 

MkGenAlts : LazyLst mustBeNotEmpty (Nat1, Lazy (Gen em a)) -> GenAlternatives mustBeNotEmpty em a

Projection: 

.unGenAlts : GenAlternatives mustBeNotEmpty em a -> LazyLst mustBeNotEmpty (Nat1, Lazy (Gen em a))

Hints:

Alternative (GenAlternatives False em)

Applicative (GenAlternatives ne em)

Cast (LazyLst ne a) (GenAlternatives ne em a)

Functor (GenAlternatives ne em)

Monad (GenAlternatives True em)

Gen1 : Type -> Type

Totality: total
Visibility: public export

Gen0 : Type -> Type

  Generator with least guarantees on emptiness.
  
  This type should not be used as an input argument unless it is strictly required.
  You should prefer to be polymorphic on emptiness instead.

Totality: total
Visibility: public export

chooseAny : Random a => {auto 0 _ : IfUnsolved ne NonEmpty} -> Gen ne a

Totality: total
Visibility: export

chooseAnyOf : (0 a : Type) -> Random a => {auto 0 _ : IfUnsolved ne NonEmpty} -> Gen ne a

Totality: total
Visibility: public export

choose : Random a => {auto 0 _ : IfUnsolved ne NonEmpty} -> (a, a) -> Gen ne a

Totality: total
Visibility: export

empty : Gen0 a

Totality: total
Visibility: export

label : Label -> Gen em a -> Gen em a

Totality: total
Visibility: export

relax : {auto 0 _ : iem `NoWeaker` em} -> Gen iem a -> Gen em a

Totality: total
Visibility: export

data AltsNonEmpty : Bool -> Emptiness -> Type

Totality: total
Visibility: public export
Constructors:

NT : AltsNonEmpty True NonEmpty

Sx : AltsNonEmpty altsNe MaybeEmpty

altsNonEmptyTrue : AltsNonEmpty True em

Totality: total
Visibility: export

unGen1 : MonadRandom m => CanManageLabels m => Gen1 a -> m a

Totality: total
Visibility: export

unGenAll' : RandomGen g => g -> Gen1 a -> Stream (g, a)

Totality: total
Visibility: export

unGenAll : RandomGen g => g -> Gen1 a -> Stream a

Totality: total
Visibility: export

pick1 : CanInitSeed g m => Functor m => Gen1 a -> m a

  Picks one random value from a generator

Totality: total
Visibility: export

unGen : MonadRandom m => MonadError () m => CanManageLabels m => Gen em a -> m a

Totality: total
Visibility: export

unGen' : MonadRandom m => CanManageLabels m => Gen em a -> m (Maybe a)

Totality: total
Visibility: export

unGenTryAll' : RandomGen g => g -> Gen em a -> Stream (g, Maybe a)

Totality: total
Visibility: export

unGenTryAll : RandomGen g => g -> Gen em a -> Stream (Maybe a)

Totality: total
Visibility: export

unGenTryN : RandomGen g => Nat -> g -> Gen em a -> LazyList a

Totality: total
Visibility: export

pick : CanInitSeed g m => Functor m => Gen em a -> m (Maybe a)

  Tries once to pick a random value from a generator

Totality: total
Visibility: export

pickTryN : CanInitSeed g m => Functor m => (n : Nat) -> Gen em a -> m (Maybe (Fin n, a))

  Tries to pick a random value from a generator, returning the number of unsuccessful attempts, if generated successfully

Totality: total
Visibility: export

Nil : GenAlternatives False em a

Totality: total
Visibility: export

(::) : {auto 0 _ : lem `NoWeaker` em} -> {auto 0 _ : rem `NoWeaker` em} -> {auto 0 _ : IfUnsolved e True} -> {auto 0 _ : IfUnsolved em NonEmpty} -> {auto 0 _ : IfUnsolved lem em} -> {auto 0 _ : IfUnsolved rem em} -> Lazy (Gen lem a) -> Lazy (GenAlternatives e rem a) -> GenAlternatives ne em a

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 7

(++) : {auto 0 _ : lem `NoWeaker` em} -> {auto 0 _ : rem `NoWeaker` em} -> {auto 0 _ : IfUnsolved lem em} -> {auto 0 _ : IfUnsolved rem em} -> {auto 0 _ : IfUnsolved nel False} -> {auto 0 _ : IfUnsolved ner False} -> GenAlternatives nel lem a -> Lazy (GenAlternatives ner rem a) -> GenAlternatives (nel || Delay ner) em a

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7

length : GenAlternatives ne em a -> Nat

Totality: total
Visibility: public export

processAlternatives : (Gen em a -> Gen em b) -> GenAlternatives ne em a -> GenAlternatives ne em b

Totality: total
Visibility: export

processAlternativesMaybe : (Gen em a -> Maybe (Lazy (Gen em b))) -> GenAlternatives ne em a -> GenAlternatives False em b

Totality: total
Visibility: export

processAlternatives'' : (Gen em a -> GenAlternatives neb em b) -> GenAlternatives nea em a -> GenAlternatives (nea && Delay neb) em b

Totality: total
Visibility: export

processAlternatives' : (Gen em a -> GenAlternatives ne em b) -> GenAlternatives ne em a -> GenAlternatives ne em b

Totality: total
Visibility: export

relax : GenAlternatives True em a -> GenAlternatives ne em a

Totality: total
Visibility: export

strengthen : GenAlternatives ne em a -> Maybe (GenAlternatives True em a)

Totality: total
Visibility: export

altsFromList : LazyLst ne a -> GenAlternatives ne em a

Totality: total
Visibility: public export

oneOf : {auto 0 _ : alem `NoWeaker` em} -> {auto 0 _ : AltsNonEmpty altsNe em} -> {auto 0 _ : IfUnsolved alem em} -> {auto 0 _ : IfUnsolved altsNe (em /= MaybeEmpty)} -> GenAlternatives altsNe alem a -> Gen em a

  Choose one of the given generators uniformly.
  
  All the given generators are treated as independent, i.e. `oneOf [oneOf [a, b], c]` is not the same as `oneOf [a, b, c]`.
  In this example case, generator `oneOf [a, b]` and generator `c` will have the same probability in the resulting generator.

Totality: total
Visibility: export

frequency : {auto 0 _ : alem `NoWeaker` em} -> {auto 0 _ : AltsNonEmpty altsNe em} -> {auto 0 _ : IfUnsolved alem em} -> {auto 0 _ : IfUnsolved altsNe (em /= MaybeEmpty)} -> LazyLst altsNe (Nat1, Lazy (Gen alem a)) -> Gen em a

  Choose one of the given generators with probability proportional to the given value, treating all source generators independently.
  
  This function treats given generators in the same way as `oneOf` do, but the resulting generator uses generator
  from the given list the more frequently, the higher number is has.
  If generator `g1` has the frequency `n1` and generator `g2` has the frequency `n2`, than `g1` will be used `n1/n2` times
  more frequently than `g2` in the resulting generator (in case when `g1` and `g2` always generate some value).

Totality: total
Visibility: export

elements : {auto 0 _ : AltsNonEmpty altsNe em} -> {auto 0 _ : IfUnsolved em NonEmpty} -> {auto 0 _ : IfUnsolved altsNe (em /= MaybeEmpty)} -> LazyLst altsNe a -> Gen em a

  Choose one of the given values uniformly.
  
  This function is equivalent to `oneOf` applied to list of `pure` generators per each value.

Totality: total
Visibility: export

elements' : Foldable f => {auto 0 _ : IfUnsolved f List} -> f a -> Gen0 a

Totality: total
Visibility: export

alternativesOf : Gen em a -> GenAlternatives True em a

  Shallow alternatives of a generator.
  
  If the given generator is made by one of `oneOf`, `frequency` or `elements`,
  this function returns alternatives which this generators contains.
  Otherwise it returns a single-element alternative list containing given generator.
  
  In a sense, this function is a reverse function of `oneOf`, i.g.
  `oneOf $ alternativesOf g` must be equivalent to `g` and
  `alternativesof $ oneOf gs` must be equivalent to `gs`.

Totality: total
Visibility: export

deepAlternativesOf : Nat -> Gen em a -> GenAlternatives True em a

  Any depth alternatives fetching.
  
  Alternatives of depth `0` are meant to be a single-item alternatives list with the original generator,
  alternatives of depth `1` are those returned by the `alternativesOf` function,
  alternatives of depth `n+1` are alternatives of all alternatives of depth `n` being flattened into a single alternatives list.

Totality: total
Visibility: export

forgetAlternatives : Gen em a -> Gen em a

  Returns generator with internal structure hidden for `alternativesOf`,
  except for an empty generator, which would still be returned as an empty generator.
  
  This function must not change distribution when the resulting generator used with usual `Gen` combinators.
  
  Please notice that this function does NOT influence to the result of `deepAlternativesOf`, if depth is increased by 1.

Totality: total
Visibility: export

forgetStructure : Gen em a -> Gen em a

  Returns generator with internal structure hidden to anything, including combinators,
  except for an empty generator, which would still be returned as an empty generator.
  
  Apply with care! Don't use until you understand what you are doing!
  Most probably, you need the lighter version of this function called `forgetAlternatives`.
  The difference is that `forgetAlternatives` do not influence on the resulting distribution,
  when this function may ruin it unexpectedly.
  
  But despite `forgetAlternatives`, this function acts on `deepAlternativesOf`
  like `forgetAlternatives` acts on `alternativesOf`,
  i.e. `deepAlternativesOf` would give a single alternative for any depth
  being applied to the result of this function.

Totality: total
Visibility: export

processAlternatives : (Gen em a -> Gen em b) -> Gen em a -> GenAlternatives True em b

Totality: total
Visibility: public export

mapAlternativesOf : (a -> b) -> Gen em a -> GenAlternatives True em b

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 8

mapAlternativesWith : Gen em a -> (a -> b) -> GenAlternatives True em b

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 8

withAlts : Gen em a -> Gen em a -> Gen em a

  Associative composition of two generators, merging shallow alternatives of given two generators
  
  This operation being applied to arguments `a` and `b` is *not* the same as `oneOf [a, b]`.
  Generator ``a `withAlts` b`` has equal probabilities of all shallow alternatives of generators `a` and `b`.
  For example, when there are generators
  ```idris
  g1 = oneOf [elems [0, 1, 2, 3], elems [4, 5]]
  g2 = oneOf elemts [10, 11, 12, 13, 14, 15]
  ```
  generator ``g1 `withAlts` g2`` would be equivalent to
  `oneOf [elems [0, 1, 2, 3], elems [4, 5], pure 10, pure 11, pure 12, pure 13, pure 14, pure 15]`.
  
  In other words, ``a `withAlts` b`` must be equivalent to `oneOf $ alternativesOf a ++ alternativesOf b`.

Totality: total
Visibility: export
Fixity Declaration: infixr operator, level 2

withDeepAlts : Nat -> Gen em a -> Gen em a -> Gen em a

  Associative composition of two generators, merging deep alternatives of given two generators
  
  This operation being applied to arguments `a` and `b` is *not* the same as `oneOf [a, b]`.
  Generator ``a `withDeepAlts` b`` has equal probabilities of all deep alternatives of generators `a` and `b`.
  For example, when there are generators
  ```idris
  g1 = oneOf [elems [0, 1, 2, 3], elems [4, 5]]
  g2 = oneOf elemts [10, 11, 12, 13, 14, 15]
  ```
  generator ``withDeepAlts n g1 g2`` with `n >= 2` would be equivalent to
  `oneOf elements [0, 1, 2, 3, 4, 5, 10, 11, 12, 13, 14, 15]`.
  
  In other words, ``withDeepAlts d a b`` must be equivalent to `oneOf $ deepAlternativesOf d a ++ deepAlternativesOf d b`.

Totality: total
Visibility: export

mapMaybe : (a -> Maybe b) -> Gen em a -> Gen0 b

Totality: total
Visibility: export

suchThat_withPrf : Gen em a -> (p : (a -> Bool)) -> Gen0 (Subset a (So . p))

Totality: total
Visibility: export

suchThat : Gen em a -> (a -> Bool) -> Gen0 a

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 4

suchThat_dec : Gen em a -> ((x : a) -> Dec (prop x)) -> Gen0 (Subset a prop)

Totality: total
Visibility: export

suchThat_invertedEq : DecEq b => Gen em a -> (y : b) -> (f : (a -> b)) -> Gen0 (Subset a (\x => y = f x))

  Filters the given generator so, that resulting values `x` are solutions of equation `y = f x` for given `f` and `y`.

Totality: total
Visibility: export

retryUntil_withPrf : (p : (a -> Bool)) -> (Fuel -> Gen em a) -> Fuel -> Gen0 (Subset a (So . p))

  More elegant version of `suchThat_withPrf` for fuelled generators.
  
  Tries to repeat generation until there is some fuel, and fallback to `suchThat_withPrf` in case there isn't.

Totality: total
Visibility: export

retryUntil : (a -> Bool) -> (Fuel -> Gen em a) -> Fuel -> Gen0 a

  More elegant version of `suchThat` for fuelled generators.
  
  Tries to repeat generation until there is some fuel, and fallback to `suchThat` in case there isn't.

Totality: total
Visibility: public export

retryUntil_dec : ((x : a) -> Dec (prop x)) -> (Fuel -> Gen em a) -> Fuel -> Gen0 (Subset a prop)

  More elegant version of `suchThat_dec` for fuelled generators.
  
  Tries to repeat generation until there is some fuel, and fallback to `suchThat_dec` in case there isn't.

Totality: total
Visibility: export

variant : Nat -> Gen em a -> Gen em a

Totality: total
Visibility: export

listOf : {default (choose (0, 10)) _ : Gen em Nat} -> Gen em a -> Gen em (List a)

Totality: total
Visibility: export

vectOf : Gen em a -> Gen em (Vect n a)

Totality: total
Visibility: export