Grisette.Experimental.GenSymConstrained

Symbolic value generation with errors

class Mergeable a => GenSymConstrained spec a where

Class of types in which symbolic values can be generated with some specification.

See GenSym for more details. The difference of this class is that it allows constraints to be generated along with the generation of symbolic values.

Minimal complete definition

Nothing

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> spec -> m (UnionM a)

Generates a symbolic value with the given specification.

Constraint violations will throw an error in the monadic environment.

>>> runFreshT (freshConstrained () (SOrdUpperBound (1 :: SymInteger) ())) "a" :: ExceptT () UnionM (UnionM SymInteger)
ExceptT <If (<= 1 a@0) (Left ()) (Right {a@0})>

default freshConstrained :: GenSymSimpleConstrained spec a => (MonadFresh m, MonadError e m, UnionLike m) => e -> spec -> m (UnionM a)

Instances

(Mergeable a, GenSym spec a) => GenSymConstrained spec a

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> spec -> m (UnionM a)

(GenSymConstrained () a, Mergeable a) => GenSymConstrained Integer [a]

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Integer -> m (UnionM [a])

(GenSymConstrained aspec a, Mergeable a) => GenSymConstrained aspec (Maybe a)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> aspec -> m (UnionM (Maybe a))

(GenSymConstrained () a, Mergeable a, GenSymConstrained () b, Mergeable b) => GenSymConstrained () (Either a b)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> () -> m (UnionM (Either a b))

(GenSymConstrained spec (m (Maybe a)), Mergeable1 m, Mergeable a) => GenSymConstrained spec (MaybeT m a)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m0, MonadError e m0, UnionLike m0) => e -> spec -> m0 (UnionM (MaybeT m a))

(GenSymConstrained spec (m (Either a b)), Mergeable1 m, Mergeable a, Mergeable b) => GenSymConstrained spec (ExceptT a m b)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m0, MonadError e m0, UnionLike m0) => e -> spec -> m0 (UnionM (ExceptT a m b))

(GenSymConstrained spec a, Mergeable a) => GenSymConstrained (ListSpec spec) [a]

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> ListSpec spec -> m (UnionM [a])

(GenSymConstrained spec a, Mergeable a) => GenSymConstrained (SimpleListSpec spec) [a]

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SimpleListSpec spec -> m (UnionM [a])

(GenSymConstrained aspec a, Mergeable a) => GenSymConstrained (Maybe aspec) (Maybe a)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Maybe aspec -> m (UnionM (Maybe a))

(GenSymConstrained a a, Mergeable a) => GenSymConstrained [a] [a]

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> [a] -> m (UnionM [a])

GenSymConstrained (SOrdBound Integer ()) Integer

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdBound Integer () -> m (UnionM Integer)

(SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdBound a spec) a

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdBound a spec -> m (UnionM a)

(SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdLowerBound a spec) a

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdLowerBound a spec -> m (UnionM a)

(SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdUpperBound a spec) a

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdUpperBound a spec -> m (UnionM a)

(GenSymConstrained aspec a, Mergeable a, GenSymConstrained bspec b, Mergeable b) => GenSymConstrained (Either aspec bspec) (Either a b)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Either aspec bspec -> m (UnionM (Either a b))

(GenSymSimpleConstrained (m (Maybe a)) (m (Maybe a)), Mergeable1 m, Mergeable a) => GenSymConstrained (MaybeT m a) (MaybeT m a)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m0, MonadError e m0, UnionLike m0) => e -> MaybeT m a -> m0 (UnionM (MaybeT m a))

(GenSymConstrained aspec a, Mergeable a, GenSymConstrained bspec b, Mergeable b) => GenSymConstrained (aspec, bspec) (a, b)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> (aspec, bspec) -> m (UnionM (a, b))

(GenSymSimpleConstrained (m (Either e a)) (m (Either e a)), Mergeable1 m, Mergeable e, Mergeable a) => GenSymConstrained (ExceptT e m a) (ExceptT e m a)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m0, MonadError e0 m0, UnionLike m0) => e0 -> ExceptT e m a -> m0 (UnionM (ExceptT e m a))

(GenSymConstrained aspec a, Mergeable a, GenSymConstrained bspec b, Mergeable b, GenSymConstrained cspec c, Mergeable c) => GenSymConstrained (aspec, bspec, cspec) (a, b, c)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> (aspec, bspec, cspec) -> m (UnionM (a, b, c))

(GenSymConstrained aspec a, Mergeable a, GenSymConstrained bspec b, Mergeable b, GenSymConstrained cspec c, Mergeable c, GenSymConstrained dspec d, Mergeable d) => GenSymConstrained (aspec, bspec, cspec, dspec) (a, b, c, d)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> (aspec, bspec, cspec, dspec) -> m (UnionM (a, b, c, d))

(GenSymConstrained aspec a, Mergeable a, GenSymConstrained bspec b, Mergeable b, GenSymConstrained cspec c, Mergeable c, GenSymConstrained dspec d, Mergeable d, GenSymConstrained espec e, Mergeable e) => GenSymConstrained (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e0 m, UnionLike m) => e0 -> (aspec, bspec, cspec, dspec, espec) -> m (UnionM (a, b, c, d, e))

(GenSymConstrained aspec a, Mergeable a, GenSymConstrained bspec b, Mergeable b, GenSymConstrained cspec c, Mergeable c, GenSymConstrained dspec d, Mergeable d, GenSymConstrained espec e, Mergeable e, GenSymConstrained fspec f, Mergeable f) => GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e0 m, UnionLike m) => e0 -> (aspec, bspec, cspec, dspec, espec, fspec) -> m (UnionM (a, b, c, d, e, f))

(GenSymConstrained aspec a, Mergeable a, GenSymConstrained bspec b, Mergeable b, GenSymConstrained cspec c, Mergeable c, GenSymConstrained dspec d, Mergeable d, GenSymConstrained espec e, Mergeable e, GenSymConstrained fspec f, Mergeable f, GenSymConstrained gspec g, Mergeable g) => GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e0 m, UnionLike m) => e0 -> (aspec, bspec, cspec, dspec, espec, fspec, gspec) -> m (UnionM (a, b, c, d, e, f, g))

(GenSymConstrained aspec a, Mergeable a, GenSymConstrained bspec b, Mergeable b, GenSymConstrained cspec c, Mergeable c, GenSymConstrained dspec d, Mergeable d, GenSymConstrained espec e, Mergeable e, GenSymConstrained fspec f, Mergeable f, GenSymConstrained gspec g, Mergeable g, GenSymConstrained hspec h, Mergeable h) => GenSymConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e0 m, UnionLike m) => e0 -> (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) -> m (UnionM (a, b, c, d, e, f, g, h))

class Mergeable a => GenSymSimpleConstrained spec a where

Class of types in which symbolic values can be generated with some specification.

See GenSymSimple for more details. The difference of this class is that it allows constraints to be generated along with the generation of symbolic values.

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> spec -> m a

Generates a symbolic value with the given specification.

Constraint violations will throw an error in the monadic environment.

>>> runFreshT (simpleFreshConstrained () (SOrdUpperBound (1 :: SymInteger) ())) "a" :: ExceptT () UnionM SymInteger
ExceptT <If (<= 1 a@0) (Left ()) (Right a@0)>

Instances

(Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained spec a

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> spec -> m a

(GenSymSimpleConstrained spec (m (Maybe a)), Mergeable1 m, Mergeable a) => GenSymSimpleConstrained spec (MaybeT m a)

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m0, MonadError e m0, UnionLike m0) => e -> spec -> m0 (MaybeT m a)

(GenSymSimpleConstrained spec (m (Either a b)), Mergeable1 m, Mergeable a, Mergeable b) => GenSymSimpleConstrained spec (ExceptT a m b)

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m0, MonadError e m0, UnionLike m0) => e -> spec -> m0 (ExceptT a m b)

GenSymSimpleConstrained spec a => GenSymSimpleConstrained (SimpleListSpec spec) [a]

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SimpleListSpec spec -> m [a]

GenSymSimpleConstrained aspec a => GenSymSimpleConstrained (Maybe aspec) (Maybe a)

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Maybe aspec -> m (Maybe a)

GenSymSimpleConstrained a a => GenSymSimpleConstrained [a] [a]

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> [a] -> m [a]

(SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdBound a spec) a

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdBound a spec -> m a

(SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdLowerBound a spec) a

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdLowerBound a spec -> m a

(SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdUpperBound a spec) a

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdUpperBound a spec -> m a

(GenSymSimpleConstrained a a, GenSymSimpleConstrained b b) => GenSymSimpleConstrained (Either a b) (Either a b)

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> Either a b -> m (Either a b)

(GenSymSimpleConstrained (m (Maybe a)) (m (Maybe a)), Mergeable1 m, Mergeable a) => GenSymSimpleConstrained (MaybeT m a) (MaybeT m a)

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m0, MonadError e m0, UnionLike m0) => e -> MaybeT m a -> m0 (MaybeT m a)

(GenSymSimpleConstrained aspec a, GenSymSimpleConstrained bspec b) => GenSymSimpleConstrained (aspec, bspec) (a, b)

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> (aspec, bspec) -> m (a, b)

(GenSymSimpleConstrained (m (Either e a)) (m (Either e a)), Mergeable1 m, Mergeable e, Mergeable a) => GenSymSimpleConstrained (ExceptT e m a) (ExceptT e m a)

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m0, MonadError e0 m0, UnionLike m0) => e0 -> ExceptT e m a -> m0 (ExceptT e m a)

(GenSymSimpleConstrained aspec a, GenSymSimpleConstrained bspec b, GenSymSimpleConstrained cspec c) => GenSymSimpleConstrained (aspec, bspec, cspec) (a, b, c)

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> (aspec, bspec, cspec) -> m (a, b, c)

(GenSymSimpleConstrained aspec a, GenSymSimpleConstrained bspec b, GenSymSimpleConstrained cspec c, GenSymSimpleConstrained dspec d) => GenSymSimpleConstrained (aspec, bspec, cspec, dspec) (a, b, c, d)

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> (aspec, bspec, cspec, dspec) -> m (a, b, c, d)

(GenSymSimpleConstrained aspec a, GenSymSimpleConstrained bspec b, GenSymSimpleConstrained cspec c, GenSymSimpleConstrained dspec d, GenSymSimpleConstrained espec e) => GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec) (a, b, c, d, e)

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e0 m, UnionLike m) => e0 -> (aspec, bspec, cspec, dspec, espec) -> m (a, b, c, d, e)

(GenSymSimpleConstrained aspec a, GenSymSimpleConstrained bspec b, GenSymSimpleConstrained cspec c, GenSymSimpleConstrained dspec d, GenSymSimpleConstrained espec e, GenSymSimpleConstrained fspec f) => GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec) (a, b, c, d, e, f)

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e0 m, UnionLike m) => e0 -> (aspec, bspec, cspec, dspec, espec, fspec) -> m (a, b, c, d, e, f)

(GenSymSimpleConstrained aspec a, GenSymSimpleConstrained bspec b, GenSymSimpleConstrained cspec c, GenSymSimpleConstrained dspec d, GenSymSimpleConstrained espec e, GenSymSimpleConstrained fspec f, GenSymSimpleConstrained gspec g) => GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec) (a, b, c, d, e, f, g)

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e0 m, UnionLike m) => e0 -> (aspec, bspec, cspec, dspec, espec, fspec, gspec) -> m (a, b, c, d, e, f, g)

(GenSymSimpleConstrained aspec a, GenSymSimpleConstrained bspec b, GenSymSimpleConstrained cspec c, GenSymSimpleConstrained dspec d, GenSymSimpleConstrained espec e, GenSymSimpleConstrained fspec f, GenSymSimpleConstrained gspec g, GenSymSimpleConstrained hspec h) => GenSymSimpleConstrained (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) (a, b, c, d, e, f, g, h)

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e0 m, UnionLike m) => e0 -> (aspec, bspec, cspec, dspec, espec, fspec, gspec, hspec) -> m (a, b, c, d, e, f, g, h)

genSymConstrained :: forall spec a e. (GenSymConstrained spec a, Mergeable e) => e -> spec -> FreshIdent -> ExceptT e UnionM (UnionM a)

genSymSimpleConstrained :: forall spec a e. (GenSymSimpleConstrained spec a, Mergeable e) => e -> spec -> FreshIdent -> ExceptT e UnionM a

derivedFreshConstrainedNoSpec :: forall a m e. (Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a, MonadFresh m, MonadError e m, UnionLike m) => e -> () -> m (UnionM a)

We cannot provide DerivingVia style derivation for GenSymConstrained, while you can use this freshConstrained implementation to implement GenSymConstrained for your own types.

This freshConstrained implementation is for the types that does not need any specification. It will generate product types by generating each fields with () as specification, and generate all possible values for a sum type.

Note: Never use on recursive types.

derivedSimpleFreshConstrainedNoSpec :: forall a m e. (Generic a, GenSymSimpleConstrainedNoSpec (Rep a), MonadFresh m, MonadError e m, UnionLike m, Mergeable a) => e -> () -> m a

We cannot provide DerivingVia style derivation for GenSymSimpleConstrained, while you can use this simpleFreshConstrained implementation to implement GenSymSimpleConstrained fo your own types.

This simpleFreshConstrained implementation is for the types that does not need any specification. It will generate product types by generating each fields with () as specification. It will not work on sum types.

Note: Never use on recursive types.

derivedSimpleFreshConstrainedSameShape :: (Generic a, GenSymConstrainedSameShape (Rep a), Mergeable a, MonadFresh m, MonadError e m, UnionLike m) => e -> a -> m a

We cannot provide DerivingVia style derivation for GenSymSimpleConstrained, while you can use this simpleFreshConstrained implementation to implement GenSymSimpleConstrained fo your own types.

This simpleFreshConstrained implementation is for the types that can be generated with a reference value of the same type.

For sum types, it will generate the result with the same data constructor. For product types, it will generate the result by generating each field with the corresponding reference value.

Note: Can be used on recursive types.

Some common GenSymConstrained specifications

data SOrdUpperBound a spec

Exclusive bound, generates the values with the specification, then filters out the ones that are greater than or equal to the bound

Constructors

SOrdUpperBound a spec

Instances

(SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdUpperBound a spec) a

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdUpperBound a spec -> m (UnionM a)

(SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdUpperBound a spec) a

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdUpperBound a spec -> m a

data SOrdLowerBound a spec

Inclusive bound, generates the values with the specification, then filters out the ones that are less than the bound

Constructors

SOrdLowerBound a spec

Instances

(SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdLowerBound a spec) a

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdLowerBound a spec -> m (UnionM a)

(SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdLowerBound a spec) a

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdLowerBound a spec -> m a

data SOrdBound a spec

Left-inclusive, right-exclusive bound, generates the values with the specification, then filters out the ones that are out-of-bound

Constructors

SOrdBound a a spec

Instances

GenSymConstrained (SOrdBound Integer ()) Integer

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdBound Integer () -> m (UnionM Integer)

(SOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SOrdBound a spec) a

Defined in Grisette.Experimental.GenSymConstrained

Methods

freshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdBound a spec -> m (UnionM a)

(SOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SOrdBound a spec) a

Defined in Grisette.Experimental.GenSymConstrained

Methods

simpleFreshConstrained :: (MonadFresh m, MonadError e m, UnionLike m) => e -> SOrdBound a spec -> m a