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 :: TypedSymbol b -> Sym b -> a -> a

Instances

SubstituteSym Int16

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Int16 -> Int16

SubstituteSym Int32

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Int32 -> Int32

SubstituteSym Int64

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Int64 -> Int64

SubstituteSym Int8

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Int8 -> Int8

SubstituteSym Word16

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Word16 -> Word16

SubstituteSym Word32

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Word32 -> Word32

SubstituteSym Word64

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Word64 -> Word64

SubstituteSym ByteString

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> ByteString -> ByteString

SubstituteSym Word8

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Word8 -> Word8

SubstituteSym Integer

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Integer -> Integer

SubstituteSym ()

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> () -> ()

SubstituteSym Bool

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Bool -> Bool

SubstituteSym Char

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Char -> Char

SubstituteSym Int

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Int -> Int

SubstituteSym Word

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Word -> Word

SubstituteSym a => SubstituteSym (Identity a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Identity a -> Identity a

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

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Default a -> Default a

(Mergeable a, SubstituteSym a) => SubstituteSym (UnionM a)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

substituteSym :: TypedSymbol b -> Sym b -> UnionM a -> UnionM a

SubstituteSym (Sym a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Sym a -> Sym a

SubstituteSym a => SubstituteSym (Maybe a)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> Maybe a -> Maybe a

SubstituteSym a => SubstituteSym [a]

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> [a] -> [a]

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

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b0 -> Sym b0 -> Either a b -> Either a b

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

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> MaybeT m a -> MaybeT m a

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

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b0 -> Sym b0 -> (a, b) -> (a, b)

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

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> ExceptT e m a -> ExceptT e m a

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

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> IdentityT m a -> IdentityT m a

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

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym :: TypedSymbol b -> Sym b -> 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 :: TypedSymbol b -> Sym b -> 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 :: TypedSymbol b0 -> Sym b0 -> (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 :: TypedSymbol b -> Sym b -> 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 :: TypedSymbol b0 -> Sym b0 -> (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 :: TypedSymbol b0 -> Sym b0 -> (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 :: TypedSymbol b0 -> Sym b0 -> (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 :: TypedSymbol b0 -> Sym b0 -> (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 :: TypedSymbol b0 -> Sym b0 -> (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' :: TypedSymbol b -> Sym b -> a c -> a c

Auxiliary function for substituteSym derivation

Instances

SubstituteSym' (U1 :: Type -> Type)

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym' :: TypedSymbol b -> Sym b -> U1 c -> U1 c

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

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym' :: TypedSymbol b0 -> Sym b0 -> (a :*: b) c -> (a :*: b) c

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

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym' :: TypedSymbol b0 -> Sym b0 -> (a :+: b) c -> (a :+: b) c

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

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym' :: TypedSymbol b -> Sym b -> K1 i c c0 -> K1 i c c0

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

Defined in Grisette.Core.Data.Class.Substitute

Methods

substituteSym' :: TypedSymbol b -> Sym b -> M1 i c a c0 -> M1 i c a c0