grisette-0.2.0.0: Symbolic evaluation as a library
Copyright(c) Sirui Lu 2021-2023
LicenseBSD-3-Clause (see the LICENSE file)
Maintainersiruilu@cs.washington.edu
StabilityExperimental
PortabilityGHC only
Safe HaskellTrustworthy
LanguageHaskell2010

Grisette.Core.Data.Class.Substitute

Description

 
Synopsis

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

Methods

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

SubstituteSym Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym ByteString Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SubstituteSym SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

SubstituteSym SymBool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

SubstituteSym SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

SubstituteSym Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym () Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym Bool Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym Char Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym Int Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym Word Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym a => SubstituteSym (Identity a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

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

Methods

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

(KnownNat n, 1 <= n) => SubstituteSym (IntN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

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

Methods

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

(KnownNat n, 1 <= n) => SubstituteSym (SymIntN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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.IR.SymPrim.Data.SymPrim

Methods

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

SubstituteSym a => SubstituteSym (Maybe a) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

Methods

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

SubstituteSym a => SubstituteSym [a] Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

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

Methods

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

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => SubstituteSym (sa -~> sb) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => SubstituteSym (sa =~> sb) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

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

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

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

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

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

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

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

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

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

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

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

Methods

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

(SubstituteSym' a, SubstituteSym' b) => SubstituteSym' (a :*: b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.Substitute

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

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

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

Methods

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