| Copyright | (c) Sirui Lu 2024 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | None |
| Language | Haskell2010 |
Grisette.Experimental
Description
Synopsis
- class Mergeable a => GenSymConstrained spec a where
- freshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> spec -> m (Union a)
- class Mergeable a => GenSymSimpleConstrained spec a where
- simpleFreshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> spec -> m a
- genSymConstrained :: (GenSymConstrained spec a, Mergeable e) => e -> spec -> Identifier -> ExceptT e Union (Union a)
- genSymSimpleConstrained :: (GenSymSimpleConstrained spec a, Mergeable e) => e -> spec -> Identifier -> ExceptT e Union a
- derivedSimpleFreshConstrainedNoSpec :: (Generic a, GenSymSimpleConstrainedNoSpec (Rep a), MonadFresh m, MonadError e m, MonadUnion m, Mergeable a) => e -> () -> m a
- derivedSimpleFreshConstrainedSameShape :: (Generic a, GenSymConstrainedSameShape (Rep a), Mergeable a, MonadFresh m, MonadError e m, MonadUnion m) => e -> a -> m a
- derivedFreshConstrainedNoSpec :: (Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a, MonadFresh m, MonadError e m, MonadUnion m) => e -> () -> m (Union a)
- data SymOrdUpperBound a spec = SymOrdUpperBound a spec
- data SymOrdLowerBound a spec = SymOrdLowerBound a spec
- data SymOrdBound a spec = SymOrdBound a a spec
Experimental features
The experimental features are likely to be changed in the future, and they do not comply with the semantics versioning policy.
Use the APIs with caution.
Symbolic Generation with Errors Class
class Mergeable a => GenSymConstrained spec a where Source #
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, MonadUnion m) => e -> spec -> m (Union a) Source #
Generates a symbolic value with the given specification.
Constraint violations will throw an error in the monadic environment.
>>>runFreshT (freshConstrained () (SymOrdUpperBound (1 :: SymInteger) ())) "a" :: ExceptT () Union (Union SymInteger)ExceptT <If (<= 1 a@0) (Left ()) (Right {a@0})>
default freshConstrained :: (GenSymSimpleConstrained spec a, MonadFresh m, MonadError e m, MonadUnion m) => e -> spec -> m (Union a) Source #
Instances
class Mergeable a => GenSymSimpleConstrained spec a where Source #
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, MonadUnion m) => e -> spec -> m a Source #
Generates a symbolic value with the given specification.
Constraint violations will throw an error in the monadic environment.
>>>runFreshT (simpleFreshConstrained () (SymOrdUpperBound (1 :: SymInteger) ())) "a" :: ExceptT () Union SymIntegerExceptT <If (<= 1 a@0) (Left ()) (Right a@0)>
Instances
genSymConstrained :: (GenSymConstrained spec a, Mergeable e) => e -> spec -> Identifier -> ExceptT e Union (Union a) Source #
Generates a symbolic value with the given specification, also place the necessary constraints.
genSymSimpleConstrained :: (GenSymSimpleConstrained spec a, Mergeable e) => e -> spec -> Identifier -> ExceptT e Union a Source #
Generates a symbolic value with the given specification, also place the necessary constraints.
derivedSimpleFreshConstrainedNoSpec :: (Generic a, GenSymSimpleConstrainedNoSpec (Rep a), MonadFresh m, MonadError e m, MonadUnion m, Mergeable a) => e -> () -> m a Source #
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, MonadUnion m) => e -> a -> m a Source #
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.
derivedFreshConstrainedNoSpec :: (Generic a, GenSymConstrainedNoSpec (Rep a), Mergeable a, MonadFresh m, MonadError e m, MonadUnion m) => e -> () -> m (Union a) Source #
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.
Some common GenSymConstrained specifications
data SymOrdUpperBound a spec Source #
Exclusive bound, generates the values with the specification, then filters out the ones that are greater than or equal to the bound
Constructors
| SymOrdUpperBound a spec |
Instances
| (SymOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SymOrdUpperBound a spec) a Source # | |
Defined in Grisette.Experimental.GenSymConstrained Methods freshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> SymOrdUpperBound a spec -> m (Union a) Source # | |
| (SymOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SymOrdUpperBound a spec) a Source # | |
Defined in Grisette.Experimental.GenSymConstrained Methods simpleFreshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> SymOrdUpperBound a spec -> m a Source # | |
data SymOrdLowerBound a spec Source #
Inclusive bound, generates the values with the specification, then filters out the ones that are less than the bound
Constructors
| SymOrdLowerBound a spec |
Instances
| (SymOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SymOrdLowerBound a spec) a Source # | |
Defined in Grisette.Experimental.GenSymConstrained Methods freshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> SymOrdLowerBound a spec -> m (Union a) Source # | |
| (SymOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SymOrdLowerBound a spec) a Source # | |
Defined in Grisette.Experimental.GenSymConstrained Methods simpleFreshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> SymOrdLowerBound a spec -> m a Source # | |
data SymOrdBound a spec Source #
Left-inclusive, right-exclusive bound, generates the values with the specification, then filters out the ones that are out-of-bound
Constructors
| SymOrdBound a a spec |
Instances
| GenSymConstrained (SymOrdBound Integer ()) Integer Source # | |
Defined in Grisette.Experimental.GenSymConstrained Methods freshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> SymOrdBound Integer () -> m (Union Integer) Source # | |
| (SymOrd a, Mergeable a, GenSym spec a) => GenSymConstrained (SymOrdBound a spec) a Source # | |
Defined in Grisette.Experimental.GenSymConstrained Methods freshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> SymOrdBound a spec -> m (Union a) Source # | |
| (SymOrd a, Mergeable a, GenSymSimple spec a) => GenSymSimpleConstrained (SymOrdBound a spec) a Source # | |
Defined in Grisette.Experimental.GenSymConstrained Methods simpleFreshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> SymOrdBound a spec -> m a Source # | |