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 aPure : a -> Gen em aRaw : RawGen a -> Gen em aOneOf : (gs : GenAlternatives True alem a) -> {auto 0 _ : All IsNonEmpty gs} -> {auto 0 _ : alem `NoWeaker` em} -> Gen em aBind : {auto 0 _ : biem `NoWeaker` em} -> RawGen c -> (c -> Gen biem a) -> Gen em aLabelled : 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 exportchooseAny : 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 NonEmptySx : AltsNonEmpty altsNe MaybeEmpty
altsNonEmptyTrue : AltsNonEmpty True em- Totality: total
Visibility: export allDetermValues : Gen em a -> LazyList a Returns a lazy list of all values that this generator can generate, except for those values which use raw generators, like `choose` or `chooseAny`.
Totality: total
Visibility: exportunGen1 : 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: exportunGen : 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: exportpickTryN : 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: exportNil : 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: exportfrequency : {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: exportelements : {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: exportelements' : 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: exportdeepAlternativesOf : 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: exportforgetAlternatives : 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: exportforgetStructure : 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: exportprocessAlternatives : (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 2withDeepAlts : 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: exportguard : Bool -> Gen0 () A function that behaves for `Gen0` like `guard` function for `Alternative`.
It can be used as a handy way to filter directly in do-notation.
Generally, try to avoid direct filterings since they can lead to very ineffective generation.
Totality: total
Visibility: public exportmapMaybe : (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: exportretryUntil_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: exportretryUntil : (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 exportretryUntil_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: exportvariant : 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