Grisette.Core.Data.Class.Substitute

Substituting symbolic constants

class SubstituteSym a where

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

Instances

SubstituteSym Int16

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int16 -> Int16

SubstituteSym Int32

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int32 -> Int32

SubstituteSym Int64

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int64 -> Int64

SubstituteSym Int8

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int8 -> Int8

SubstituteSym Word16

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word16 -> Word16

SubstituteSym Word32

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word32 -> Word32

SubstituteSym Word64

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word64 -> Word64

SubstituteSym Word8

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word8 -> Word8

SubstituteSym ByteString

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> ByteString -> ByteString

SubstituteSym SomeIntN

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeIntN -> SomeIntN

SubstituteSym SomeWordN

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeWordN -> SomeWordN

SubstituteSym SomeSymIntN

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeSymIntN -> SomeSymIntN

SubstituteSym SomeSymWordN

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SomeSymWordN -> SomeSymWordN

SubstituteSym SymBool

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymBool -> SymBool

SubstituteSym SymInteger

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymInteger -> SymInteger

SubstituteSym Integer

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Integer -> Integer

SubstituteSym ()

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> () -> ()

SubstituteSym Bool

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Bool -> Bool

SubstituteSym Char

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Char -> Char

SubstituteSym Int

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Int -> Int

SubstituteSym Word

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Word -> Word

SubstituteSym a => SubstituteSym (Identity a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Identity a -> Identity a

(Generic a, SubstituteSym' (Rep a)) => SubstituteSym (Default a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Default a -> Default a

(KnownNat n, 1 <= n) => SubstituteSym (IntN n)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> IntN n -> IntN n

(KnownNat n, 1 <= n) => SubstituteSym (WordN n)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WordN n -> WordN n

(KnownNat n, 1 <= n) => SubstituteSym (SymIntN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymIntN n -> SymIntN n

(KnownNat n, 1 <= n) => SubstituteSym (SymWordN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> SymWordN n -> SymWordN n

SubstituteSym a => SubstituteSym (Maybe a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Maybe a -> Maybe a

SubstituteSym a => SubstituteSym [a]

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> [a] -> [a]

(SubstituteSym a, SubstituteSym b) => SubstituteSym (Either a b)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Either a b -> Either a b

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => SubstituteSym (sa -~> sb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

substituteSym :: LinkedRep cb sb0 => TypedSymbol cb -> sb0 -> (sa -~> sb) -> sa -~> sb

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => SubstituteSym (sa =~> sb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

substituteSym :: LinkedRep cb sb0 => TypedSymbol cb -> sb0 -> (sa =~> sb) -> sa =~> sb

SubstituteSym (m (Maybe a)) => SubstituteSym (MaybeT m a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> MaybeT m a -> MaybeT m a

(SubstituteSym a, SubstituteSym b) => SubstituteSym (a, b)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b) -> (a, b)

SubstituteSym (m (Either e a)) => SubstituteSym (ExceptT e m a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> ExceptT e m a -> ExceptT e m a

SubstituteSym (m a) => SubstituteSym (IdentityT m a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> IdentityT m a -> IdentityT m a

SubstituteSym (m (a, s)) => SubstituteSym (WriterT s m a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a

SubstituteSym (m (a, s)) => SubstituteSym (WriterT s m a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> WriterT s m a -> WriterT s m a

(SubstituteSym a, SubstituteSym b, SubstituteSym c) => SubstituteSym (a, b, c)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c) -> (a, b, c)

(SubstituteSym (f a), SubstituteSym (g a)) => SubstituteSym (Sum f g a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> Sum f g a -> Sum f g a

(SubstituteSym a, SubstituteSym b, SubstituteSym c, SubstituteSym d) => SubstituteSym (a, b, c, d)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d) -> (a, b, c, d)

(SubstituteSym a, SubstituteSym b, SubstituteSym c, SubstituteSym d, SubstituteSym e) => SubstituteSym (a, b, c, d, e)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e) -> (a, b, c, d, e)

(SubstituteSym a, SubstituteSym b, SubstituteSym c, SubstituteSym d, SubstituteSym e, SubstituteSym f) => SubstituteSym (a, b, c, d, e, f)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f) -> (a, b, c, d, e, f)

(SubstituteSym a, SubstituteSym b, SubstituteSym c, SubstituteSym d, SubstituteSym e, SubstituteSym f, SubstituteSym g) => SubstituteSym (a, b, c, d, e, f, g)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g)

(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)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h)

class SubstituteSym' a where

Auxiliary class for SubstituteSym instance derivation

Methods

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

Auxiliary function for substituteSym derivation

Instances

SubstituteSym' (U1 :: Type -> Type)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> U1 c -> U1 c

(SubstituteSym' a, SubstituteSym' b) => SubstituteSym' (a :*: b)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a :*: b) c -> (a :*: b) c

(SubstituteSym' a, SubstituteSym' b) => SubstituteSym' (a :+: b)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> (a :+: b) c -> (a :+: b) c

SubstituteSym c => SubstituteSym' (K1 i c :: Type -> Type)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> K1 i c c0 -> K1 i c c0

SubstituteSym' a => SubstituteSym' (M1 i c a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym' :: LinkedRep cb sb => TypedSymbol cb -> sb -> M1 i c a c0 -> M1 i c a c0