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

Contents

Substituting symbolic constants

Description

Synopsis

class SubstituteSym a where
- substituteSym :: TypedSymbol b -> Sym b -> a -> a
class SubstituteSym' a where
- substituteSym' :: TypedSymbol b -> Sym b -> 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 :: TypedSymbol b -> Sym b -> a -> a Source #

Instances

Instances details

SubstituteSym Int16 Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Int16 -> Int16 Source #
SubstituteSym Int32 Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Int32 -> Int32 Source #
SubstituteSym Int64 Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Int64 -> Int64 Source #
SubstituteSym Int8 Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Int8 -> Int8 Source #
SubstituteSym Word16 Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Word16 -> Word16 Source #
SubstituteSym Word32 Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Word32 -> Word32 Source #
SubstituteSym Word64 Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Word64 -> Word64 Source #
SubstituteSym ByteString Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> ByteString -> ByteString Source #
SubstituteSym Word8 Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Word8 -> Word8 Source #
SubstituteSym Integer Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Integer -> Integer Source #
SubstituteSym () Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> () -> () Source #
SubstituteSym Bool Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Bool -> Bool Source #
SubstituteSym Char Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Char -> Char Source #
SubstituteSym Int Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Int -> Int Source #
SubstituteSym Word Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Word -> Word Source #
SubstituteSym a => SubstituteSym (Identity a) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Identity a -> Identity a Source #
(Generic a, SubstituteSym' (Rep a)) => SubstituteSym (Default a) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Default a -> Default a Source #
(Mergeable a, SubstituteSym a) => SubstituteSym (UnionM a) Source #
Instance details Defined in Grisette.Core.Control.Monad.UnionM Methods substituteSym :: TypedSymbol b -> Sym b -> UnionM a -> UnionM a Source #
SubstituteSym (Sym a) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Sym a -> Sym a Source #
SubstituteSym a => SubstituteSym (Maybe a) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> Maybe a -> Maybe a Source #
SubstituteSym a => SubstituteSym [a] Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> [a] -> [a] Source #
(SubstituteSym a, SubstituteSym b) => SubstituteSym (Either a b) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b0 -> Sym b0 -> Either a b -> Either a b Source #
SubstituteSym (m (Maybe a)) => SubstituteSym (MaybeT m a) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> MaybeT m a -> MaybeT m a Source #
(SubstituteSym a, SubstituteSym b) => SubstituteSym (a, b) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b0 -> Sym b0 -> (a, b) -> (a, b) Source #
SubstituteSym (m (Either e a)) => SubstituteSym (ExceptT e m a) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> ExceptT e m a -> ExceptT e m a Source #
SubstituteSym (m a) => SubstituteSym (IdentityT m a) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> IdentityT m a -> IdentityT m a Source #
SubstituteSym (m (a, s)) => SubstituteSym (WriterT s m a) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> WriterT s m a -> WriterT s m a Source #
SubstituteSym (m (a, s)) => SubstituteSym (WriterT s m a) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> 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.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b0 -> Sym b0 -> (a, b, c) -> (a, b, c) Source #
(SubstituteSym (f a), SubstituteSym (g a)) => SubstituteSym (Sum f g a) Source #
Instance details Defined in Grisette.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b -> Sym b -> 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.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b0 -> Sym b0 -> (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.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b0 -> Sym b0 -> (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.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b0 -> Sym b0 -> (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.Core.Data.Class.Substitute Methods substituteSym :: TypedSymbol b0 -> Sym b0 -> (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.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) Source #

class SubstituteSym' a where Source #

Auxiliary class for SubstituteSym instance derivation

Methods

substituteSym' :: TypedSymbol b -> Sym b -> a c -> a c Source #

Auxiliary function for substituteSym derivation

Instances

Instances details

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