| 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.ExtractSym
Description
Synopsis
- class ExtractSym a where
- extractSym :: a -> SymbolSet
- class (forall a. ExtractSym a => ExtractSym (f a)) => ExtractSym1 f where
- liftExtractSym :: (a -> SymbolSet) -> f a -> SymbolSet
- extractSym1 :: (ExtractSym1 f, ExtractSym a) => f a -> SymbolSet
- class (forall a. ExtractSym a => ExtractSym1 (f a)) => ExtractSym2 f where
- liftExtractSym2 :: (a -> SymbolSet) -> (b -> SymbolSet) -> f a b -> SymbolSet
- extractSym2 :: (ExtractSym2 f, ExtractSym a, ExtractSym b) => f a b -> SymbolSet
- data family ExtractSymArgs arity a :: Type
- class GExtractSym arity f where
- gextractSym :: ExtractSymArgs arity a -> f a -> SymbolSet
- genericExtractSym :: (Generic a, GExtractSym Arity0 (Rep a)) => a -> SymbolSet
- genericLiftExtractSym :: (Generic1 f, GExtractSym Arity1 (Rep1 f)) => (a -> SymbolSet) -> f a -> SymbolSet
Extracting symbolic constant set from a value
class ExtractSym a where Source #
Extracts all the symbols (symbolic constants) that are transitively contained in the given value.
>>>extractSym ("a" :: SymBool) :: SymbolSetSymbolSet {a :: Bool}
>>>extractSym (mrgIf "a" (mrgReturn ["b"]) (mrgReturn ["c", "d"]) :: Union [SymBool]) :: SymbolSetSymbolSet {a :: Bool, b :: Bool, c :: Bool, d :: Bool}
Note 1: This type class can be derived for algebraic data types.
You may need the DerivingVia and DerivingStrategies extensions.
data X = ... deriving Generic deriving ExtractSym via (Default X)
Methods
extractSym :: a -> SymbolSet Source #
Instances
class (forall a. ExtractSym a => ExtractSym (f a)) => ExtractSym1 f where Source #
Lifting of ExtractSym to unary type constructors.
Methods
liftExtractSym :: (a -> SymbolSet) -> f a -> SymbolSet Source #
Lifts the extractSym function to unary type constructors.
Instances
extractSym1 :: (ExtractSym1 f, ExtractSym a) => f a -> SymbolSet Source #
Lift the standard extractSym to unary type constructors.
class (forall a. ExtractSym a => ExtractSym1 (f a)) => ExtractSym2 f where Source #
Lifting of ExtractSym to binary type constructors.
Methods
liftExtractSym2 :: (a -> SymbolSet) -> (b -> SymbolSet) -> f a b -> SymbolSet Source #
Lifts the extractSym function to binary type constructors.
Instances
| ExtractSym2 Either Source # | |
Defined in Grisette.Internal.Core.Data.Class.ExtractSym | |
| ExtractSym2 (,) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ExtractSym | |
| ExtractSym a => ExtractSym2 ((,,) a) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ExtractSym | |
| (ExtractSym a, ExtractSym b) => ExtractSym2 ((,,,) a b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ExtractSym | |
extractSym2 :: (ExtractSym2 f, ExtractSym a, ExtractSym b) => f a b -> SymbolSet Source #
Lift the standard extractSym to binary type constructors.
Generic ExtractSym
data family ExtractSymArgs arity a :: Type Source #
The arguments to the generic extractSym function.
Instances
| data ExtractSymArgs Arity0 _ Source # | |
Defined in Grisette.Internal.Core.Data.Class.ExtractSym | |
| newtype ExtractSymArgs Arity1 a Source # | |
Defined in Grisette.Internal.Core.Data.Class.ExtractSym | |
class GExtractSym arity f where Source #
The class of types that can generically extract the symbols.
Methods
gextractSym :: ExtractSymArgs arity a -> f a -> SymbolSet Source #
Instances
genericExtractSym :: (Generic a, GExtractSym Arity0 (Rep a)) => a -> SymbolSet Source #
Generic extractSym function.
genericLiftExtractSym :: (Generic1 f, GExtractSym Arity1 (Rep1 f)) => (a -> SymbolSet) -> f a -> SymbolSet Source #
Generic liftExtractSym function.