Copyright	(c) Sirui Lu 2024
License	BSD-3-Clause (see the LICENSE file)
Maintainer	siruilu@cs.washington.edu
Stability	Experimental
Portability	GHC only
Safe Haskell	None
Language	Haskell2010

Grisette.Internal.SymPrim.AllSyms

Contents

Get all symbolic primitive values in a value
Generic AllSyms

Description

Synopsis

data SomeSym where
- SomeSym :: forall con sym. LinkedRep con sym => sym -> SomeSym
class AllSyms a where
- allSymsS :: a -> [SomeSym] -> [SomeSym]
- allSyms :: a -> [SomeSym]
class (forall a. AllSyms a => AllSyms (f a)) => AllSyms1 (f :: Type -> Type) where
- liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> f a -> [SomeSym] -> [SomeSym]
allSymsS1 :: (AllSyms1 f, AllSyms a) => f a -> [SomeSym] -> [SomeSym]
class (forall a. AllSyms a => AllSyms1 (f a)) => AllSyms2 (f :: Type -> Type -> Type) where
- liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> f a b -> [SomeSym] -> [SomeSym]
allSymsS2 :: (AllSyms2 f, AllSyms a, AllSyms b) => f a b -> [SomeSym] -> [SomeSym]
allSymsSize :: AllSyms a => a -> Int
symSize :: LinkedRep con sym => sym -> Int
symsSize :: LinkedRep con sym => [sym] -> Int
data family AllSymsArgs arity a
class GAllSyms arity (f :: Type -> Type) where
- gallSymsS :: AllSymsArgs arity a -> f a -> [SomeSym] -> [SomeSym]
genericAllSymsS :: (Generic a, GAllSyms Arity0 (Rep a)) => a -> [SomeSym] -> [SomeSym]
genericLiftAllSymsS :: (Generic1 f, GAllSyms Arity1 (Rep1 f)) => (a -> [SomeSym] -> [SomeSym]) -> f a -> [SomeSym] -> [SomeSym]

Get all symbolic primitive values in a value

data SomeSym where Source #

Some symbolic value with LinkedRep constraint.

Constructors

SomeSym :: forall con sym. LinkedRep con sym => sym -> SomeSym

Instances

Instances details

Show SomeSym Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods showsPrec :: Int -> SomeSym -> ShowS # show :: SomeSym -> String # showList :: [SomeSym] -> ShowS #

class AllSyms a where Source #

Extract all symbolic primitive values that are represented as SMT terms.

>>> allSyms (["a" + 1 :: SymInteger, -"b"], "c" :: SymBool)
[(+ 1 a),(- b),c]

This is usually used for getting a statistical summary of the size of a symbolic value with allSymsSize.

Note: This type class can be derived for algebraic data types. You may need the DerivingVia and DerivingStrategies extenstions.

data X = ... deriving Generic deriving AllSyms via (Default X)

Minimal complete definition

allSymsS | allSyms

Methods

allSymsS :: a -> [SomeSym] -> [SomeSym] Source #

Convert a value to a list of symbolic primitive values. It should prepend to an existing list of symbolic primitive values.

allSyms :: a -> [SomeSym] Source #

Specialized allSymsS that prepends to an empty list.

Instances

Instances details

AllSyms ByteString Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: ByteString -> [SomeSym] -> [SomeSym] Source # allSyms :: ByteString -> [SomeSym] Source #
AllSyms Int16 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Int16 -> [SomeSym] -> [SomeSym] Source # allSyms :: Int16 -> [SomeSym] Source #
AllSyms Int32 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Int32 -> [SomeSym] -> [SomeSym] Source # allSyms :: Int32 -> [SomeSym] Source #
AllSyms Int64 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Int64 -> [SomeSym] -> [SomeSym] Source # allSyms :: Int64 -> [SomeSym] Source #
AllSyms Int8 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Int8 -> [SomeSym] -> [SomeSym] Source # allSyms :: Int8 -> [SomeSym] Source #
AllSyms Word16 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Word16 -> [SomeSym] -> [SomeSym] Source # allSyms :: Word16 -> [SomeSym] Source #
AllSyms Word32 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Word32 -> [SomeSym] -> [SomeSym] Source # allSyms :: Word32 -> [SomeSym] Source #
AllSyms Word64 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Word64 -> [SomeSym] -> [SomeSym] Source # allSyms :: Word64 -> [SomeSym] Source #
AllSyms Word8 Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Word8 -> [SomeSym] -> [SomeSym] Source # allSyms :: Word8 -> [SomeSym] Source #
AllSyms AssertionError Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: AssertionError -> [SomeSym] -> [SomeSym] Source # allSyms :: AssertionError -> [SomeSym] Source #
AllSyms VerificationConditions Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: VerificationConditions -> [SomeSym] -> [SomeSym] Source # allSyms :: VerificationConditions -> [SomeSym] Source #
AllSyms AlgReal Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: AlgReal -> [SomeSym] -> [SomeSym] Source # allSyms :: AlgReal -> [SomeSym] Source #
AllSyms FPRoundingMode Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: FPRoundingMode -> [SomeSym] -> [SomeSym] Source # allSyms :: FPRoundingMode -> [SomeSym] Source #
AllSyms SymAlgReal Source #
Instance details Defined in Grisette.Internal.SymPrim.SymAlgReal Methods allSymsS :: SymAlgReal -> [SomeSym] -> [SomeSym] Source # allSyms :: SymAlgReal -> [SomeSym] Source #
AllSyms SymBool Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBool Methods allSymsS :: SymBool -> [SomeSym] -> [SomeSym] Source # allSyms :: SymBool -> [SomeSym] Source #
AllSyms SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods allSymsS :: SymFPRoundingMode -> [SomeSym] -> [SomeSym] Source # allSyms :: SymFPRoundingMode -> [SomeSym] Source #
AllSyms SymInteger Source #
Instance details Defined in Grisette.Internal.SymPrim.SymInteger Methods allSymsS :: SymInteger -> [SomeSym] -> [SomeSym] Source # allSyms :: SymInteger -> [SomeSym] Source #
AllSyms Text Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Text -> [SomeSym] -> [SomeSym] Source # allSyms :: Text -> [SomeSym] Source #
AllSyms Integer Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Integer -> [SomeSym] -> [SomeSym] Source # allSyms :: Integer -> [SomeSym] Source #
AllSyms () Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: () -> [SomeSym] -> [SomeSym] Source # allSyms :: () -> [SomeSym] Source #
AllSyms Bool Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Bool -> [SomeSym] -> [SomeSym] Source # allSyms :: Bool -> [SomeSym] Source #
AllSyms Char Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Char -> [SomeSym] -> [SomeSym] Source # allSyms :: Char -> [SomeSym] Source #
AllSyms Double Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Double -> [SomeSym] -> [SomeSym] Source # allSyms :: Double -> [SomeSym] Source #
AllSyms Float Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Float -> [SomeSym] -> [SomeSym] Source # allSyms :: Float -> [SomeSym] Source #
AllSyms Int Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Int -> [SomeSym] -> [SomeSym] Source # allSyms :: Int -> [SomeSym] Source #
AllSyms Word Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Word -> [SomeSym] -> [SomeSym] Source # allSyms :: Word -> [SomeSym] Source #
(Generic a, GAllSyms Arity0 (Rep a)) => AllSyms (Default a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods allSymsS :: Default a -> [SomeSym] -> [SomeSym] Source # allSyms :: Default a -> [SomeSym] Source #
AllSyms a => AllSyms (Identity a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Identity a -> [SomeSym] -> [SomeSym] Source # allSyms :: Identity a -> [SomeSym] Source #
AllSyms a => AllSyms (Ratio a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Ratio a -> [SomeSym] -> [SomeSym] Source # allSyms :: Ratio a -> [SomeSym] Source #
AllSyms a => AllSyms (AsKey a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods allSymsS :: AsKey a -> [SomeSym] -> [SomeSym] Source # allSyms :: AsKey a -> [SomeSym] Source #
AllSyms a => AllSyms (Union a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods allSymsS :: Union a -> [SomeSym] -> [SomeSym] Source # allSyms :: Union a -> [SomeSym] Source #
AllSyms a => AllSyms (UnionBase a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase Methods allSymsS :: UnionBase a -> [SomeSym] -> [SomeSym] Source # allSyms :: UnionBase a -> [SomeSym] Source #
(KnownNat n, 1 <= n) => AllSyms (IntN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: IntN n -> [SomeSym] -> [SomeSym] Source # allSyms :: IntN n -> [SomeSym] Source #
(KnownNat n, 1 <= n) => AllSyms (WordN n) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: WordN n -> [SomeSym] -> [SomeSym] Source # allSyms :: WordN n -> [SomeSym] Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => AllSyms (bv n), MaySomeBV bv) => AllSyms (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods allSymsS :: SomeBV bv -> [SomeSym] -> [SomeSym] Source # allSyms :: SomeBV bv -> [SomeSym] Source #
(KnownNat n, 1 <= n) => AllSyms (SymIntN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods allSymsS :: SymIntN n -> [SomeSym] -> [SomeSym] Source # allSyms :: SymIntN n -> [SomeSym] Source #
(KnownNat n, 1 <= n) => AllSyms (SymWordN n) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymBV Methods allSymsS :: SymWordN n -> [SomeSym] -> [SomeSym] Source # allSyms :: SymWordN n -> [SomeSym] Source #
AllSyms a => AllSyms (Maybe a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Maybe a -> [SomeSym] -> [SomeSym] Source # allSyms :: Maybe a -> [SomeSym] Source #
AllSyms a => AllSyms [a] Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: [a] -> [SomeSym] -> [SomeSym] Source # allSyms :: [a] -> [SomeSym] Source #
(Generic1 f, GAllSyms Arity1 (Rep1 f), AllSyms a) => AllSyms (Default1 f a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods allSymsS :: Default1 f a -> [SomeSym] -> [SomeSym] Source # allSyms :: Default1 f a -> [SomeSym] Source #
(AllSyms a1, AllSyms a2) => AllSyms (Either a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Either a1 a2 -> [SomeSym] -> [SomeSym] Source # allSyms :: Either a1 a2 -> [SomeSym] Source #
AllSyms (Proxy a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Proxy a -> [SomeSym] -> [SomeSym] Source # allSyms :: Proxy a -> [SomeSym] Source #
(AllSyms1 f, AllSyms a) => AllSyms (AsKey1 f a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods allSymsS :: AsKey1 f a -> [SomeSym] -> [SomeSym] Source # allSyms :: AsKey1 f a -> [SomeSym] Source #
ValidFP eb sb => AllSyms (FP eb sb) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: FP eb sb -> [SomeSym] -> [SomeSym] Source # allSyms :: FP eb sb -> [SomeSym] Source #
ValidFP eb sb => AllSyms (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods allSymsS :: SymFP eb sb -> [SomeSym] -> [SomeSym] Source # allSyms :: SymFP eb sb -> [SomeSym] Source #
AllSyms (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymGeneralFun Methods allSymsS :: (sa -~> sb) -> [SomeSym] -> [SomeSym] Source # allSyms :: (sa -~> sb) -> [SomeSym] Source #
AllSyms (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymTabularFun Methods allSymsS :: (sa =~> sb) -> [SomeSym] -> [SomeSym] Source # allSyms :: (sa =~> sb) -> [SomeSym] Source #
(AllSyms1 a1, AllSyms a2) => AllSyms (MaybeT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: MaybeT a1 a2 -> [SomeSym] -> [SomeSym] Source # allSyms :: MaybeT a1 a2 -> [SomeSym] Source #
(AllSyms a1, AllSyms a2) => AllSyms (a1, a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2) -> [SomeSym] Source #
(AllSyms a1, AllSyms1 a2, AllSyms a3) => AllSyms (ExceptT a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: ExceptT a1 a2 a3 -> [SomeSym] -> [SomeSym] Source # allSyms :: ExceptT a1 a2 a3 -> [SomeSym] Source #
(AllSyms1 m, AllSyms a) => AllSyms (IdentityT m a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: IdentityT m a -> [SomeSym] -> [SomeSym] Source # allSyms :: IdentityT m a -> [SomeSym] Source #
(AllSyms a1, AllSyms1 a2, AllSyms a3) => AllSyms (WriterT a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: WriterT a1 a2 a3 -> [SomeSym] -> [SomeSym] Source # allSyms :: WriterT a1 a2 a3 -> [SomeSym] Source #
(AllSyms a1, AllSyms1 a2, AllSyms a3) => AllSyms (WriterT a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: WriterT a1 a2 a3 -> [SomeSym] -> [SomeSym] Source # allSyms :: WriterT a1 a2 a3 -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3) => AllSyms (a1, a2, a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2, a3) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2, a3) -> [SomeSym] Source #
(AllSyms (f a), AllSyms (g a)) => AllSyms (Sum f g a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: Sum f g a -> [SomeSym] -> [SomeSym] Source # allSyms :: Sum f g a -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4) => AllSyms (a1, a2, a3, a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2, a3, a4) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2, a3, a4) -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5) => AllSyms (a1, a2, a3, a4, a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2, a3, a4, a5) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2, a3, a4, a5) -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6) => AllSyms (a1, a2, a3, a4, a5, a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2, a3, a4, a5, a6) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2, a3, a4, a5, a6) -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7) => AllSyms (a1, a2, a3, a4, a5, a6, a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2, a3, a4, a5, a6, a7) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2, a3, a4, a5, a6, a7) -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8) -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9) -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10) -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11) -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12) -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12, AllSyms a13) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13) -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12, AllSyms a13, AllSyms a14) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14) -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12, AllSyms a13, AllSyms a14, AllSyms a15) => AllSyms (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods allSymsS :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> [SomeSym] -> [SomeSym] Source # allSyms :: (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15) -> [SomeSym] Source #

class (forall a. AllSyms a => AllSyms (f a)) => AllSyms1 (f :: Type -> Type) where Source #

Lifting of the AllSyms class to unary type constructors.

Methods

liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> f a -> [SomeSym] -> [SomeSym] Source #

Lift the allSymsS function to unary type constructors.

Instances

Instances details

AllSyms1 Identity Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> Identity a -> [SomeSym] -> [SomeSym] Source #
AllSyms1 Union Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Control.Monad.Union Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> Union a -> [SomeSym] -> [SomeSym] Source #
AllSyms1 UnionBase Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Core.Data.UnionBase Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> UnionBase a -> [SomeSym] -> [SomeSym] Source #
AllSyms1 Maybe Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> Maybe a -> [SomeSym] -> [SomeSym] Source #
AllSyms1 [] Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> [a] -> [SomeSym] -> [SomeSym] Source #
(Generic1 f, GAllSyms Arity1 (Rep1 f)) => AllSyms1 (Default1 f) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> Default1 f a -> [SomeSym] -> [SomeSym] Source #
AllSyms a => AllSyms1 (Either a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a0 -> [SomeSym] -> [SomeSym]) -> Either a a0 -> [SomeSym] -> [SomeSym] Source #
AllSyms1 (Proxy :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> Proxy a -> [SomeSym] -> [SomeSym] Source #
AllSyms1 f => AllSyms1 (AsKey1 f) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> AsKey1 f a -> [SomeSym] -> [SomeSym] Source #
AllSyms1 a => AllSyms1 (MaybeT a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a0 -> [SomeSym] -> [SomeSym]) -> MaybeT a a0 -> [SomeSym] -> [SomeSym] Source #
AllSyms a => AllSyms1 ((,) a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a0 -> [SomeSym] -> [SomeSym]) -> (a, a0) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms1 a2) => AllSyms1 (ExceptT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> ExceptT a1 a2 a -> [SomeSym] -> [SomeSym] Source #
AllSyms1 m => AllSyms1 (IdentityT m) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> IdentityT m a -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms1 a2) => AllSyms1 (WriterT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> WriterT a1 a2 a -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms1 a2) => AllSyms1 (WriterT a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> WriterT a1 a2 a -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2) => AllSyms1 ((,,) a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a) -> [SomeSym] -> [SomeSym] Source #
(AllSyms1 f, AllSyms1 g) => AllSyms1 (Sum f g) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> Sum f g a -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3) => AllSyms1 ((,,,) a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4) => AllSyms1 ((,,,,) a1 a2 a3 a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5) => AllSyms1 ((,,,,,) a1 a2 a3 a4 a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6) => AllSyms1 ((,,,,,,) a1 a2 a3 a4 a5 a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7) => AllSyms1 ((,,,,,,,) a1 a2 a3 a4 a5 a6 a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8) => AllSyms1 ((,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9) => AllSyms1 ((,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10) => AllSyms1 ((,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11) => AllSyms1 ((,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12) => AllSyms1 ((,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12, AllSyms a13) => AllSyms1 ((,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12, AllSyms a13, AllSyms a14) => AllSyms1 ((,,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13 a14) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS :: (a -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a) -> [SomeSym] -> [SomeSym] Source #

allSymsS1 :: (AllSyms1 f, AllSyms a) => f a -> [SomeSym] -> [SomeSym] Source #

Lift the standard allSymsS function to unary type constructors.

class (forall a. AllSyms a => AllSyms1 (f a)) => AllSyms2 (f :: Type -> Type -> Type) where Source #

Lifting of the AllSyms class to binary type constructors.

Methods

liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> f a b -> [SomeSym] -> [SomeSym] Source #

Lift the allSymsS function to binary type constructors.

Instances

Instances details

AllSyms2 Either Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> Either a b -> [SomeSym] -> [SomeSym] Source #
AllSyms2 (,) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a, b) -> [SomeSym] -> [SomeSym] Source #
AllSyms a => AllSyms2 ((,,) a) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a0 -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a, a0, b) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2) => AllSyms2 ((,,,) a1 a2) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a, b) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3) => AllSyms2 ((,,,,) a1 a2 a3) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a, b) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4) => AllSyms2 ((,,,,,) a1 a2 a3 a4) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a, b) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5) => AllSyms2 ((,,,,,,) a1 a2 a3 a4 a5) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a, b) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6) => AllSyms2 ((,,,,,,,) a1 a2 a3 a4 a5 a6) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a, b) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7) => AllSyms2 ((,,,,,,,,) a1 a2 a3 a4 a5 a6 a7) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a, b) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8) => AllSyms2 ((,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a, b) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9) => AllSyms2 ((,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a, b) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10) => AllSyms2 ((,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a, b) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11) => AllSyms2 ((,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a, b) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12) => AllSyms2 ((,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a, b) -> [SomeSym] -> [SomeSym] Source #
(AllSyms a1, AllSyms a2, AllSyms a3, AllSyms a4, AllSyms a5, AllSyms a6, AllSyms a7, AllSyms a8, AllSyms a9, AllSyms a10, AllSyms a11, AllSyms a12, AllSyms a13) => AllSyms2 ((,,,,,,,,,,,,,,) a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 a13) Source #
Instance details Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms Methods liftAllSymsS2 :: (a -> [SomeSym] -> [SomeSym]) -> (b -> [SomeSym] -> [SomeSym]) -> (a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a, b) -> [SomeSym] -> [SomeSym] Source #

allSymsS2 :: (AllSyms2 f, AllSyms a, AllSyms b) => f a b -> [SomeSym] -> [SomeSym] Source #

Lift the standard allSymsS function to binary type constructors.

allSymsSize :: AllSyms a => a -> Int Source #

Get the total size of symbolic terms in a value. Duplicate sub-terms are counted for only once.

>>> allSymsSize ("a" :: SymInteger, "a" + "b" :: SymInteger, ("a" + "b") * "c" :: SymInteger)
5

The 5 terms are a, b, (+ a b), c, and (* (+ a b) c).

symSize :: LinkedRep con sym => sym -> Int Source #

Get the size of a symbolic term. Duplicate sub-terms are counted for only once.

>>> symSize (1 :: SymInteger)
1
>>> symSize ("a" :: SymInteger)
1
>>> symSize ("a" + 1 :: SymInteger)
3
>>> symSize (("a" + 1) * ("a" + 1) :: SymInteger)
4

symsSize :: LinkedRep con sym => [sym] -> Int Source #

Get the sum of the sizes of a list of symbolic terms. Duplicate sub-terms are counted for only once.

>>> symsSize [1, "a" :: SymInteger, "a" + 1 :: SymInteger]
3

Generic `AllSyms`

data family AllSymsArgs arity a Source #

The arguments to the generic AllSyms function.

Instances

Instances details

data AllSymsArgs Arity0 _ Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms data AllSymsArgs Arity0 _ = AllSymsArgs0
newtype AllSymsArgs Arity1 a Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms newtype AllSymsArgs Arity1 a = AllSymsArgs1 (a -> [SomeSym] -> [SomeSym])

class GAllSyms arity (f :: Type -> Type) where Source #

The class of types that can generically extract all symbolic primitives.

Methods

gallSymsS :: AllSymsArgs arity a -> f a -> [SomeSym] -> [SomeSym] Source #

Instances

Instances details

GAllSyms Arity1 Par1 Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods gallSymsS :: AllSymsArgs Arity1 a -> Par1 a -> [SomeSym] -> [SomeSym] Source #
GAllSyms arity (U1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods gallSymsS :: AllSymsArgs arity a -> U1 a -> [SomeSym] -> [SomeSym] Source #
GAllSyms arity (V1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods gallSymsS :: AllSymsArgs arity a -> V1 a -> [SomeSym] -> [SomeSym] Source #
AllSyms1 f => GAllSyms Arity1 (Rec1 f) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods gallSymsS :: AllSymsArgs Arity1 a -> Rec1 f a -> [SomeSym] -> [SomeSym] Source #
(GAllSyms arity a, GAllSyms arity b) => GAllSyms arity (a :*: b) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods gallSymsS :: AllSymsArgs arity a0 -> (a :*: b) a0 -> [SomeSym] -> [SomeSym] Source #
(GAllSyms arity a, GAllSyms arity b) => GAllSyms arity (a :+: b) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods gallSymsS :: AllSymsArgs arity a0 -> (a :+: b) a0 -> [SomeSym] -> [SomeSym] Source #
AllSyms c => GAllSyms arity (K1 i c :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods gallSymsS :: AllSymsArgs arity a -> K1 i c a -> [SomeSym] -> [SomeSym] Source #
(AllSyms1 f, GAllSyms Arity1 g) => GAllSyms Arity1 (f :.: g) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods gallSymsS :: AllSymsArgs Arity1 a -> (f :.: g) a -> [SomeSym] -> [SomeSym] Source #
GAllSyms arity a => GAllSyms arity (M1 i c a) Source #
Instance details Defined in Grisette.Internal.Internal.Decl.SymPrim.AllSyms Methods gallSymsS :: AllSymsArgs arity a0 -> M1 i c a a0 -> [SomeSym] -> [SomeSym] Source #

genericAllSymsS :: (Generic a, GAllSyms Arity0 (Rep a)) => a -> [SomeSym] -> [SomeSym] Source #

Generic allSymsS function.

genericLiftAllSymsS :: (Generic1 f, GAllSyms Arity1 (Rep1 f)) => (a -> [SomeSym] -> [SomeSym]) -> f a -> [SomeSym] -> [SomeSym] Source #

Generic liftAllSymsS function.

Get all symbolic primitive values in a value

Instances

Instances

Instances

Instances

Generic AllSyms

Instances

Instances

Generic `AllSyms`