| Copyright | (c) Sirui Lu 2021-2023 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | Trustworthy |
| Language | Haskell2010 |
Grisette.Core.Data.Class.GenSym
Description
Synopsis
- newtype FreshIndex = FreshIndex Int
- data FreshIdent where
- FreshIdent :: String -> FreshIdent
- FreshIdentWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent
- name :: String -> FreshIdent
- nameWithInfo :: forall a. (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent
- class Monad m => MonadFresh m where
- nextFreshIndex :: m FreshIndex
- getFreshIdent :: m FreshIdent
- data FreshT m a
- type Fresh = FreshT Identity
- runFreshT :: Monad m => FreshT m a -> FreshIdent -> m a
- runFresh :: Fresh a -> FreshIdent -> a
- 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 -> FreshIdent -> UnionM a
- genSymSimple :: forall spec a. GenSymSimple spec a => spec -> FreshIdent -> a
- derivedNoSpecFresh :: forall bool a m u. (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 bool a m u. (Mergeable a, MonadFresh m) => [a] -> m (UnionM a)
- chooseSimpleFresh :: forall a m. (SimpleMergeable a, MonadFresh m) => [a] -> m a
- chooseUnionFresh :: forall bool a m u. (Mergeable a, MonadFresh m) => [UnionM a] -> m (UnionM a)
- choose :: forall bool a u. Mergeable a => [a] -> FreshIdent -> UnionM a
- chooseSimple :: forall a. SimpleMergeable a => [a] -> FreshIdent -> a
- chooseUnion :: forall a u. Mergeable a => [UnionM a] -> FreshIdent -> 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
data FreshIdent where Source #
Identifier type used for GenSym
The constructor is hidden intentionally. You can construct an identifier by:
- a raw name
The following two expressions will refer to the same identifier (the solver won't distinguish them and would assign the same value to them). The user may need to use unique names to avoid unintentional identifier collision.
>>>name "a"a
>>>"a" :: FreshIdent -- available when OverloadedStrings is enableda
- bundle the calling file location with the name to ensure global uniqueness
Identifiers created at different locations will not be the same. The identifiers created at the same location will be the same.
>>>$$(nameWithLoc "a") -- a sample result could be "a:<interactive>:18:4-18"a:<interactive>:...
- bundle the calling file location with some user provided information
Identifiers created with different name or different additional information will not be the same.
>>>nameWithInfo "a" (1 :: Int)a:1
Constructors
| FreshIdent :: String -> FreshIdent | |
| FreshIdentWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent |
Instances
name :: String -> FreshIdent Source #
Simple name identifier. The same identifier refers to the same symbolic variable in the whole program.
The user may need to use unique names to avoid unintentional identifier collision.
nameWithInfo :: forall a. (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent Source #
Identifier with extra information. The same name with the same information refers to the same symbolic variable in the whole program.
The user may need to use unique names or additional information to avoid unintentional identifier collision.
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 FreshIdent and a state monad for
the FreshIndex.
Methods
nextFreshIndex :: m FreshIndex Source #
Increase the index by one and return the new index.
getFreshIdent :: m FreshIdent Source #
Get the identifier.
Instances
| Monad m => MonadFresh (FreshT m) Source # | |
Defined in Grisette.Core.Data.Class.GenSym | |
A symbolic generation monad transformer. It is a reader monad transformer for identifiers and a state monad transformer for indices.
Each time a fresh symbolic variable is generated, the index should be increased.
Instances
runFreshT :: Monad m => FreshT m a -> FreshIdent -> m a Source #
Run the symbolic generation with the given identifier and 0 as the initial index.
runFresh :: Fresh a -> FreshIdent -> a Source #
Run the symbolic generation with the given identifier and 0 as the initial index.
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 -> FreshIdent -> 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 -> FreshIdent -> 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 bool a m u. (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 bool a m u. (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 bool a m u. (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 bool a u. Mergeable a => [a] -> FreshIdent -> 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] -> FreshIdent -> 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 u. Mergeable a => [UnionM a] -> FreshIdent -> 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
| |
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
| Show spec => Show (SimpleListSpec spec) Source # | |
Defined in Grisette.Core.Data.Class.GenSym Methods showsPrec :: Int -> SimpleListSpec spec -> ShowS # show :: SimpleListSpec spec -> String # showList :: [SimpleListSpec spec] -> ShowS # | |
| (GenSymSimple spec a, Mergeable a) => GenSym (SimpleListSpec spec) [a] Source # | |
Defined in Grisette.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => SimpleListSpec spec -> m (UnionM [a]) Source # | |
| GenSymSimple spec a => GenSymSimple (SimpleListSpec spec) [a] Source # | |
Defined in Grisette.Core.Data.Class.GenSym Methods simpleFresh :: MonadFresh m => SimpleListSpec spec -> m [a] Source # | |
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.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.Core.Data.Class.GenSym Methods fresh :: MonadFresh m => EnumGenUpperBound v -> m (UnionM v) Source # | |