| Copyright | (c) Sirui Lu 2021-2024 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Grisette.Internal.Core.Data.Class.GenSym
Description
Synopsis
- newtype FreshIndex = FreshIndex Int
- class Monad m => MonadFresh m where
- getFreshIndex :: m FreshIndex
- setFreshIndex :: FreshIndex -> m ()
- getIdentifier :: m Identifier
- localIdentifier :: (Identifier -> Identifier) -> m a -> m a
- nextFreshIndex :: MonadFresh m => m FreshIndex
- liftFresh :: MonadFresh m => Fresh a -> m a
- newtype FreshT m a = FreshT {
- runFreshTFromIndex :: Identifier -> FreshIndex -> m (a, FreshIndex)
- type Fresh = FreshT Identity
- runFreshT :: Monad m => FreshT m a -> Identifier -> m a
- runFresh :: Fresh a -> Identifier -> a
- mrgRunFreshT :: (Monad m, TryMerge m, Mergeable a) => FreshT m a -> Identifier -> m a
- freshString :: (MonadFresh m, IsString s) => String -> m s
- class Mergeable a => GenSym spec a where
- fresh :: MonadFresh m => spec -> m (UnionM a)
- class GenSymSimple spec a where
- simpleFresh :: MonadFresh m => spec -> m a
- genSym :: GenSym spec a => spec -> Identifier -> UnionM a
- genSymSimple :: forall spec a. GenSymSimple spec a => spec -> Identifier -> a
- derivedNoSpecFresh :: forall a m. (Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) => () -> m (UnionM a)
- derivedNoSpecSimpleFresh :: forall a m. (Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) => () -> m a
- derivedSameShapeSimpleFresh :: forall a m. (Generic a, GenSymSameShape (Rep a), MonadFresh m) => a -> m a
- chooseFresh :: forall a m. (Mergeable a, MonadFresh m) => [a] -> m (UnionM a)
- chooseSimpleFresh :: forall a m. (SimpleMergeable a, MonadFresh m) => [a] -> m a
- chooseUnionFresh :: forall a m. (Mergeable a, MonadFresh m) => [UnionM a] -> m (UnionM a)
- choose :: forall a. Mergeable a => [a] -> Identifier -> UnionM a
- chooseSimple :: forall a. SimpleMergeable a => [a] -> Identifier -> a
- chooseUnion :: forall a. Mergeable a => [UnionM a] -> Identifier -> UnionM a
- data ListSpec spec = ListSpec {
- genListMinLength :: Int
- genListMaxLength :: Int
- genListSubSpec :: spec
- data SimpleListSpec spec = SimpleListSpec {
- genSimpleListLength :: Int
- genSimpleListSubSpec :: spec
- data EnumGenBound a = EnumGenBound a a
- newtype EnumGenUpperBound a = EnumGenUpperBound a
Indices and identifiers for fresh symbolic value generation
newtype FreshIndex Source #
Index type used for GenSym.
To generate fresh variables, a monadic stateful context will be maintained. The index should be increased every time a new symbolic constant is generated.
Constructors
| FreshIndex Int |
Instances
Monad for fresh symbolic value generation
class Monad m => MonadFresh m where Source #
Monad class for fresh symbolic value generation.
The monad should be a reader monad for the Identifier and a state monad for
the FreshIndex.
Methods
getFreshIndex :: m FreshIndex Source #
Get the current index for fresh variable generation.
setFreshIndex :: FreshIndex -> m () Source #
Set the current index for fresh variable generation.
getIdentifier :: m Identifier Source #
Get the identifier.
localIdentifier :: (Identifier -> Identifier) -> m a -> m a Source #
Change the identifier locally and use a new index from 0 locally.
Instances
nextFreshIndex :: MonadFresh m => m FreshIndex Source #
Get the next fresh index and increase the current index.
liftFresh :: MonadFresh m => Fresh a -> m a Source #
Lifts an Fresh aMonadFresh.
A symbolic generation monad transformer.
It is a reader monad transformer for an identifier and a state monad transformer for indices.
Each time a fresh symbolic variable is generated, the index should be increased.
Constructors
| FreshT | |
Fields
| |
Instances
runFreshT :: Monad m => FreshT m a -> Identifier -> m a Source #
Run the symbolic generation with the given identifier and 0 as the initial index.
runFresh :: Fresh a -> Identifier -> a Source #
Run the symbolic generation with the given identifier and 0 as the initial index.
mrgRunFreshT :: (Monad m, TryMerge m, Mergeable a) => FreshT m a -> Identifier -> m a Source #
freshString :: (MonadFresh m, IsString s) => String -> m s Source #
Generate a fresh string with the given postfix.
>>>runFresh (freshString "b") "a" :: String"a@0[b]"
Symbolic value generation
class Mergeable a => GenSym spec a where Source #
Class of types in which symbolic values can be generated with respect to some specification.
The result will be wrapped in a union-like monad. This ensures that we can generate those types with complex merging rules.
The uniqueness of symbolic constants is managed with the a monadic context.
Fresh and FreshT can be useful.
Minimal complete definition
Nothing
Methods
fresh :: MonadFresh m => spec -> m (UnionM a) Source #
Generate a symbolic value given some specification. Within a single
MonadFresh context, calls to fresh would generate unique symbolic
constants.
The following example generates a symbolic boolean. No specification is needed.
>>>runFresh (fresh ()) "a" :: UnionM SymBool{a@0}
The following example generates booleans, which cannot be merged into a
single value with type Bool. No specification is needed.
>>>runFresh (fresh ()) "a" :: UnionM Bool{If a@0 False True}
The following example generates Maybe Bools.
There are more than one symbolic constants introduced, and their uniqueness
is ensured. No specification is needed.
>>>runFresh (fresh ()) "a" :: UnionM (Maybe Bool){If a@0 Nothing (If a@1 (Just False) (Just True))}
The following example generates lists of symbolic booleans with length 1 to 2.
>>>runFresh (fresh (ListSpec 1 2 ())) "a" :: UnionM [SymBool]{If a@2 [a@1] [a@0,a@1]}
When multiple symbolic values are generated, there will not be any identifier collision
>>>runFresh (do; a <- fresh (); b <- fresh (); return (a, b)) "a" :: (UnionM SymBool, UnionM SymBool)({a@0},{a@1})
default fresh :: GenSymSimple spec a => MonadFresh m => spec -> m (UnionM a) Source #
Instances
class GenSymSimple spec a where Source #
Class of types in which symbolic values can be generated with respect to some specification.
The result will not be wrapped in a union-like monad.
The uniqueness of symbolic constants is managed with the a monadic context.
Fresh and FreshT can be useful.
Methods
simpleFresh :: MonadFresh m => spec -> m a Source #
Generate a symbolic value given some specification. The uniqueness is ensured.
The following example generates a symbolic boolean. No specification is needed.
>>>runFresh (simpleFresh ()) "a" :: SymBoola@0
The following code generates list of symbolic boolean with length 2. As the length is fixed, we don't have to wrap the result in unions.
>>>runFresh (simpleFresh (SimpleListSpec 2 ())) "a" :: [SymBool][a@0,a@1]
Instances
genSym :: GenSym spec a => spec -> Identifier -> UnionM a Source #
Generate a symbolic variable wrapped in a Union without the monadic context. A globally unique identifier should be supplied to ensure the uniqueness of symbolic constants in the generated symbolic values.
>>>genSym (ListSpec 1 2 ()) "a" :: UnionM [SymBool]{If a@2 [a@1] [a@0,a@1]}
genSymSimple :: forall spec a. GenSymSimple spec a => spec -> Identifier -> a Source #
Generate a simple symbolic variable wrapped in a Union without the monadic context. A globally unique identifier should be supplied to ensure the uniqueness of symbolic constants in the generated symbolic values.
>>>genSymSimple (SimpleListSpec 2 ()) "a" :: [SymBool][a@0,a@1]
derivedNoSpecFresh :: forall a m. (Generic a, GenSymNoSpec (Rep a), Mergeable a, MonadFresh m) => () -> m (UnionM a) Source #
We cannot provide DerivingVia style derivation for GenSym, while you can
use this fresh implementation to implement GenSym for your own types.
This fresh 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.
derivedNoSpecSimpleFresh :: forall a m. (Generic a, GenSymSimpleNoSpec (Rep a), MonadFresh m) => () -> m a Source #
We cannot provide DerivingVia style derivation for GenSymSimple, while
you can use this simpleFresh implementation to implement GenSymSimple fo
your own types.
This simpleFresh 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.
derivedSameShapeSimpleFresh :: forall a m. (Generic a, GenSymSameShape (Rep a), MonadFresh m) => a -> m a Source #
We cannot provide DerivingVia style derivation for GenSymSimple, while
you can use this simpleFresh implementation to implement GenSymSimple fo
your own types.
This simpleFresh 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.
Symbolic choices
chooseFresh :: forall a m. (Mergeable a, MonadFresh m) => [a] -> m (UnionM a) Source #
Symbolically chooses one of the provided values.
The procedure creates n - 1 fresh symbolic boolean variables every time it
is evaluated, and use these variables to conditionally select one of the n
provided expressions.
The result will be wrapped in a union-like monad, and also a monad
maintaining the MonadFresh context.
>>>runFresh (chooseFresh [1,2,3]) "a" :: UnionM Integer{If a@0 1 (If a@1 2 3)}
chooseSimpleFresh :: forall a m. (SimpleMergeable a, MonadFresh m) => [a] -> m a Source #
Symbolically chooses one of the provided values.
The procedure creates n - 1 fresh symbolic boolean variables every time it is evaluated, and use
these variables to conditionally select one of the n provided expressions.
The result will not be wrapped in a union-like monad, but will be
wrapped in a monad maintaining the Fresh context.
>>>import Data.Proxy>>>runFresh (chooseSimpleFresh [ssym "b", ssym "c", ssym "d"]) "a" :: SymInteger(ite a@0 b (ite a@1 c d))
chooseUnionFresh :: forall a m. (Mergeable a, MonadFresh m) => [UnionM a] -> m (UnionM a) Source #
Symbolically chooses one of the provided values wrapped in union-like
monads. The procedure creates n - 1 fresh symbolic boolean variables every
time it is evaluated, and use these variables to conditionally select one of
the n provided expressions.
The result will be wrapped in a union-like monad, and also a monad
maintaining the Fresh context.
>>>let a = runFresh (chooseFresh [1, 2]) "a" :: UnionM Integer>>>let b = runFresh (chooseFresh [2, 3]) "b" :: UnionM Integer>>>runFresh (chooseUnionFresh [a, b]) "c" :: UnionM Integer{If (&& c@0 a@0) 1 (If (|| c@0 b@0) 2 3)}
choose :: forall a. Mergeable a => [a] -> Identifier -> UnionM a Source #
A wrapper for chooseFresh that executes the MonadFresh context.
A globally unique identifier should be supplied to ensure the uniqueness of
symbolic constants in the generated symbolic values.
chooseSimple :: forall a. SimpleMergeable a => [a] -> Identifier -> a Source #
A wrapper for chooseSimpleFresh that executes the MonadFresh context.
A globally unique identifier should be supplied to ensure the uniqueness of
symbolic constants in the generated symbolic values.
chooseUnion :: forall a. Mergeable a => [UnionM a] -> Identifier -> UnionM a Source #
A wrapper for chooseUnionFresh that executes the MonadFresh context.
A globally unique identifier should be supplied to ensure the uniqueness of
symbolic constants in the generated symbolic values.
Some common GenSym specifications
Specification for list generation.
>>>runFresh (fresh (ListSpec 0 2 ())) "c" :: UnionM [SymBool]{If c@2 [] (If c@3 [c@1] [c@0,c@1])}
>>>runFresh (fresh (ListSpec 0 2 (SimpleListSpec 1 ()))) "c" :: UnionM [[SymBool]]{If c@2 [] (If c@3 [[c@1]] [[c@0],[c@1]])}
Constructors
| ListSpec | |
Fields
| |
Instances
| Show spec => Show (ListSpec spec) Source # | |
| (GenSymConstrained spec a, Mergeable a) => GenSymConstrained (ListSpec spec) [a] Source # | |
Defined in Grisette.Experimental.GenSymConstrained Methods freshConstrained :: (MonadFresh m, MonadError e m, MonadUnion m) => e -> ListSpec spec -> m (UnionM [a]) Source # | |
| (GenSym spec a, Mergeable a) => GenSym (ListSpec spec) [a] Source # | |
Defined in Grisette.Internal.Core.Data.Class.GenSym | |
data SimpleListSpec spec Source #
Specification for list generation of a specific length.
>>>runFresh (simpleFresh (SimpleListSpec 2 ())) "c" :: [SymBool][c@0,c@1]
Constructors
| SimpleListSpec | |
Fields
| |
Instances
data EnumGenBound a Source #
Specification for numbers with lower bound (inclusive) and upper bound (exclusive)
>>>runFresh (fresh (EnumGenBound @Integer 0 4)) "c" :: UnionM Integer{If c@0 0 (If c@1 1 (If c@2 2 3))}
Constructors
| EnumGenBound a a |
Instances
| (Enum v, Mergeable v) => GenSym (EnumGenBound v) v Source # | |
Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => EnumGenBound v -> m (UnionM v) Source # | |
newtype EnumGenUpperBound a Source #
Specification for enum values with upper bound (exclusive). The result would chosen from [0 .. upperbound].
>>>runFresh (fresh (EnumGenUpperBound @Integer 4)) "c" :: UnionM Integer{If c@0 0 (If c@1 1 (If c@2 2 3))}
Constructors
| EnumGenUpperBound a |
Instances
| (Enum v, Mergeable v) => GenSym (EnumGenUpperBound v) v Source # | |
Defined in Grisette.Internal.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => EnumGenUpperBound v -> m (UnionM v) Source # | |