| 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 | Safe-Inferred |
| Language | Haskell2010 |
Grisette.Internal.Core.Data.Class.ExtractSym
Description
Synopsis
- class ExtractSym a where
- extractSym :: a -> AnySymbolSet
- extractSymMaybe :: IsSymbolKind knd => a -> Maybe (SymbolSet knd)
- class (forall a. ExtractSym a => ExtractSym (f a)) => ExtractSym1 f where
- liftExtractSymMaybe :: IsSymbolKind knd => (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
- extractSymMaybe1 :: (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) => f a -> Maybe (SymbolSet knd)
- extractSym1 :: (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) => f a -> SymbolSet knd
- class (forall a. ExtractSym a => ExtractSym1 (f a)) => ExtractSym2 f where
- liftExtractSymMaybe2 :: IsSymbolKind knd => (a -> Maybe (SymbolSet knd)) -> (b -> Maybe (SymbolSet knd)) -> f a b -> Maybe (SymbolSet knd)
- extractSymMaybe2 :: (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) => f a b -> Maybe (SymbolSet knd)
- extractSym2 :: (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) => f a b -> SymbolSet knd
- data family ExtractSymArgs arity (knd :: SymbolKind) a :: Type
- class GExtractSym arity f where
- gextractSymMaybe :: IsSymbolKind knd => ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd)
- genericExtractSymMaybe :: (Generic a, GExtractSym Arity0 (Rep a), IsSymbolKind knd) => a -> Maybe (SymbolSet knd)
- genericLiftExtractSymMaybe :: (Generic1 f, GExtractSym Arity1 (Rep1 f), IsSymbolKind knd) => (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
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)SymbolSet {a :: Bool}
>>>extractSym (mrgIf "a" (mrgReturn ["b"]) (mrgReturn ["c", "d"]) :: Union [SymBool])SymbolSet {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)
Minimal complete definition
Methods
extractSym :: a -> AnySymbolSet Source #
extractSymMaybe :: IsSymbolKind knd => a -> Maybe (SymbolSet knd) Source #
Instances
class (forall a. ExtractSym a => ExtractSym (f a)) => ExtractSym1 f where Source #
Lifting of ExtractSym to unary type constructors.
Methods
liftExtractSymMaybe :: IsSymbolKind knd => (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd) Source #
Lifts the extractSymMaybe function to unary type constructors.
Instances
extractSymMaybe1 :: (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) => f a -> Maybe (SymbolSet knd) Source #
Lift the standard extractSymMaybe to unary type constructors.
extractSym1 :: (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) => f a -> SymbolSet knd 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
liftExtractSymMaybe2 :: IsSymbolKind knd => (a -> Maybe (SymbolSet knd)) -> (b -> Maybe (SymbolSet knd)) -> f a b -> Maybe (SymbolSet knd) Source #
Lifts the extractSymMaybe function to binary type constructors.
Instances
extractSymMaybe2 :: (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) => f a b -> Maybe (SymbolSet knd) Source #
Lift the standard extractSymMaybe to binary type constructors.
extractSym2 :: (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) => f a b -> SymbolSet knd Source #
Lift the standard extractSym to binary type constructors.
Generic ExtractSym
data family ExtractSymArgs arity (knd :: SymbolKind) a :: Type Source #
The arguments to the generic extractSym function.
Instances
| data ExtractSymArgs Arity0 _ _1 Source # | |
| newtype ExtractSymArgs Arity1 knd a Source # | |
class GExtractSym arity f where Source #
The class of types that can generically extract the symbols.
Methods
gextractSymMaybe :: IsSymbolKind knd => ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd) Source #
Instances
genericExtractSymMaybe :: (Generic a, GExtractSym Arity0 (Rep a), IsSymbolKind knd) => a -> Maybe (SymbolSet knd) Source #
Generic extractSym function.
genericLiftExtractSymMaybe :: (Generic1 f, GExtractSym Arity1 (Rep1 f), IsSymbolKind knd) => (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd) Source #
Generic liftExtractSymMaybe function.