| 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 :: forall (knd :: SymbolKind). IsSymbolKind knd => a -> Maybe (SymbolSet knd)
- class (forall a. ExtractSym a => ExtractSym (f a)) => ExtractSym1 (f :: Type -> Type) where
- liftExtractSymMaybe :: forall (knd :: SymbolKind) a. IsSymbolKind knd => (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd)
- extractSymMaybe1 :: forall f a (knd :: SymbolKind). (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) => f a -> Maybe (SymbolSet knd)
- extractSym1 :: forall f a (knd :: SymbolKind). (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) => f a -> SymbolSet knd
- class (forall a. ExtractSym a => ExtractSym1 (f a)) => ExtractSym2 (f :: Type -> Type -> Type) where
- liftExtractSymMaybe2 :: forall (knd :: SymbolKind) a b. IsSymbolKind knd => (a -> Maybe (SymbolSet knd)) -> (b -> Maybe (SymbolSet knd)) -> f a b -> Maybe (SymbolSet knd)
- extractSymMaybe2 :: forall f a b (knd :: SymbolKind). (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) => f a b -> Maybe (SymbolSet knd)
- extractSym2 :: forall f a b (knd :: SymbolKind). (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) => f a b -> SymbolSet knd
- data family ExtractSymArgs arity (knd :: SymbolKind) a
- class GExtractSym arity (f :: Type -> Type) where
- gextractSymMaybe :: forall (knd :: SymbolKind) a. IsSymbolKind knd => ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd)
- genericExtractSymMaybe :: forall a (knd :: SymbolKind). (Generic a, GExtractSym Arity0 (Rep a), IsSymbolKind knd) => a -> Maybe (SymbolSet knd)
- genericLiftExtractSymMaybe :: forall f (knd :: SymbolKind) a. (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 :: forall (knd :: SymbolKind). IsSymbolKind knd => a -> Maybe (SymbolSet knd) Source #
Instances
class (forall a. ExtractSym a => ExtractSym (f a)) => ExtractSym1 (f :: Type -> Type) where Source #
Lifting of ExtractSym to unary type constructors.
Methods
liftExtractSymMaybe :: forall (knd :: SymbolKind) a. IsSymbolKind knd => (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd) Source #
Lifts the extractSymMaybe function to unary type constructors.
Instances
extractSymMaybe1 :: forall f a (knd :: SymbolKind). (ExtractSym1 f, ExtractSym a, IsSymbolKind knd) => f a -> Maybe (SymbolSet knd) Source #
Lift the standard extractSymMaybe to unary type constructors.
extractSym1 :: forall f a (knd :: SymbolKind). (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 :: Type -> Type -> Type) where Source #
Lifting of ExtractSym to binary type constructors.
Methods
liftExtractSymMaybe2 :: forall (knd :: SymbolKind) a b. 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 :: forall f a b (knd :: SymbolKind). (ExtractSym2 f, ExtractSym a, ExtractSym b, IsSymbolKind knd) => f a b -> Maybe (SymbolSet knd) Source #
Lift the standard extractSymMaybe to binary type constructors.
extractSym2 :: forall f a b (knd :: SymbolKind). (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 Source #
The arguments to the generic extractSym function.
Instances
| data ExtractSymArgs Arity0 _ _1 Source # | |
| newtype ExtractSymArgs Arity1 knd a Source # | |
class GExtractSym arity (f :: Type -> Type) where Source #
The class of types that can generically extract the symbols.
Methods
gextractSymMaybe :: forall (knd :: SymbolKind) a. IsSymbolKind knd => ExtractSymArgs arity knd a -> f a -> Maybe (SymbolSet knd) Source #
Instances
genericExtractSymMaybe :: forall a (knd :: SymbolKind). (Generic a, GExtractSym Arity0 (Rep a), IsSymbolKind knd) => a -> Maybe (SymbolSet knd) Source #
Generic extractSym function.
genericLiftExtractSymMaybe :: forall f (knd :: SymbolKind) a. (Generic1 f, GExtractSym Arity1 (Rep1 f), IsSymbolKind knd) => (a -> Maybe (SymbolSet knd)) -> f a -> Maybe (SymbolSet knd) Source #
Generic liftExtractSymMaybe function.