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.Internal.Core.Data.Class.SubstituteSym

Contents

Substituting symbolic constants

Description

Synopsis

class SubstituteSym a where
- substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a
class SubstituteSym' a where
- substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> a c -> a c

Substituting symbolic constants

class SubstituteSym a where Source #

Substitution of symbolic constants.

>>> a = "a" :: TypedSymbol Bool
>>> v = "x" .&& "y" :: SymBool
>>> substituteSym a v (["a" .&& "b", "a"] :: [SymBool])
[(&& (&& x y) b),(&& x y)]

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 SubstituteSym via (Default X)

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> a -> a Source #

Instances

Instances details

SubstituteSym Int16 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int16 -> Int16 Source #
SubstituteSym Int32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int32 -> Int32 Source #
SubstituteSym Int64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int64 -> Int64 Source #
SubstituteSym Int8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int8 -> Int8 Source #
SubstituteSym Word16 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word16 -> Word16 Source #
SubstituteSym Word32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word32 -> Word32 Source #
SubstituteSym Word64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word64 -> Word64 Source #
SubstituteSym Word8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word8 -> Word8 Source #
SubstituteSym ByteString Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> ByteString -> ByteString Source #
SubstituteSym SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymBool -> SymBool Source #
SubstituteSym SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymInteger -> SymInteger Source #
SubstituteSym Text Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Text -> Text Source #
SubstituteSym Integer Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Integer -> Integer Source #
SubstituteSym () Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> () -> () Source #
SubstituteSym Bool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Bool -> Bool Source #
SubstituteSym Char Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Char -> Char Source #
SubstituteSym Int Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int -> Int Source #
SubstituteSym Word Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word -> Word Source #
SubstituteSym a => SubstituteSym (Identity a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Identity a -> Identity a Source #
(Generic a, SubstituteSym' (Rep a)) => SubstituteSym (Default a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Default a -> Default a Source #
(Mergeable a, SubstituteSym a) => SubstituteSym (UnionM a) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> UnionM a -> UnionM a Source #
(KnownNat n, 1 <= n) => SubstituteSym (IntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> IntN n -> IntN n Source #
(KnownNat n, 1 <= n) => SubstituteSym (WordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WordN n -> WordN n Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => SubstituteSym (bv n)) => SubstituteSym (SomeBV bv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeBV bv -> SomeBV bv Source #
(KnownNat n, 1 <= n) => SubstituteSym (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => SubstituteSym (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymWordN n -> SymWordN n Source #
SubstituteSym a => SubstituteSym (Maybe a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Maybe a -> Maybe a Source #
SubstituteSym a => SubstituteSym [a] Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> [a] -> [a] Source #
(SubstituteSym a, SubstituteSym b) => SubstituteSym (Either a b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Either a b -> Either a b Source #
(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => SubstituteSym (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb0 => TypedSymbol cb -> sb0 -> (sa -~> sb) -> sa -~> sb Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => SubstituteSym (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb0 => TypedSymbol cb -> sb0 -> (sa =~> sb) -> sa =~> sb Source #
SubstituteSym (m (Maybe a)) => SubstituteSym (MaybeT m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> MaybeT m a -> MaybeT m a Source #
(SubstituteSym a, SubstituteSym b) => SubstituteSym (a, b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b) -> (a, b) Source #
SubstituteSym (m (Either e a)) => SubstituteSym (ExceptT e m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> ExceptT e m a -> ExceptT e m a Source #
SubstituteSym (m a) => SubstituteSym (IdentityT m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> IdentityT m a -> IdentityT m a Source #
SubstituteSym (m (a, s)) => SubstituteSym (WriterT s m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a Source #
SubstituteSym (m (a, s)) => SubstituteSym (WriterT s m a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a Source #
(SubstituteSym a, SubstituteSym b, SubstituteSym c) => SubstituteSym (a, b, c) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c) -> (a, b, c) Source #
(SubstituteSym (f a), SubstituteSym (g a)) => SubstituteSym (Sum f g a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Sum f g a -> Sum f g a Source #
(SubstituteSym a, SubstituteSym b, SubstituteSym c, SubstituteSym d) => SubstituteSym (a, b, c, d) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d) -> (a, b, c, d) Source #
(SubstituteSym a, SubstituteSym b, SubstituteSym c, SubstituteSym d, SubstituteSym e) => SubstituteSym (a, b, c, d, e) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e) -> (a, b, c, d, e) Source #
(SubstituteSym a, SubstituteSym b, SubstituteSym c, SubstituteSym d, SubstituteSym e, SubstituteSym f) => SubstituteSym (a, b, c, d, e, f) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f) -> (a, b, c, d, e, f) Source #
(SubstituteSym a, SubstituteSym b, SubstituteSym c, SubstituteSym d, SubstituteSym e, SubstituteSym f, SubstituteSym g) => SubstituteSym (a, b, c, d, e, f, g) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g) Source #
(SubstituteSym a, SubstituteSym b, SubstituteSym c, SubstituteSym d, SubstituteSym e, SubstituteSym f, SubstituteSym g, SubstituteSym h) => SubstituteSym (a, b, c, d, e, f, g, h) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h) Source #

class SubstituteSym' a where Source #

Auxiliary class for SubstituteSym instance derivation

Methods

substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> a c -> a c Source #

Auxiliary function for substituteSym derivation

Instances

Instances details

SubstituteSym' (U1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> U1 c -> U1 c Source #
SubstituteSym' (V1 :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> V1 c -> V1 c Source #
(SubstituteSym' a, SubstituteSym' b) => SubstituteSym' (a :*: b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a :: b) c -> (a :: b) c Source #
(SubstituteSym' a, SubstituteSym' b) => SubstituteSym' (a :+: b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a :+: b) c -> (a :+: b) c Source #
SubstituteSym c => SubstituteSym' (K1 i c :: Type -> Type) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> K1 i c c0 -> K1 i c c0 Source #
SubstituteSym' a => SubstituteSym' (M1 i c a) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.SubstituteSym Methods substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> M1 i c a c0 -> M1 i c a c0 Source #