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.ToSym

Description

 
Synopsis

Converting to symbolic values

class ToSym a b where Source #

Convert a concrete value to symbolic value.

Methods

toSym :: a -> b Source #

Convert a concrete value to symbolic value.

>>> toSym False :: SymBool
false
>>> toSym [False, True] :: [SymBool]
[false,true]

Instances

Instances details
ToSym Int16 Int16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int16 -> Int16 Source #

ToSym Int16 SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym Int32 Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int32 -> Int32 Source #

ToSym Int32 SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym Int64 Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int64 -> Int64 Source #

ToSym Int64 SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym Int8 Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int8 -> Int8 Source #

ToSym Int8 SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym Word16 Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word16 -> Word16 Source #

ToSym Word16 SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym Word32 Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word32 -> Word32 Source #

ToSym Word32 SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym Word64 Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word64 -> Word64 Source #

ToSym Word64 SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym Word8 Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word8 -> Word8 Source #

ToSym Word8 SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym ByteString ByteString Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

ToSym AssertionError AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ToSym VerificationConditions VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ToSym SomeIntN SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

ToSym SomeIntN SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym SomeWordN SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

ToSym SomeWordN SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym SomeSymIntN SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym SomeSymWordN SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym SymBool SymBool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym SymInteger SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym Integer SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym Integer Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

ToSym () () Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: () -> () Source #

ToSym Bool SymBool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Bool -> SymBool Source #

ToSym Bool Bool Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Bool -> Bool Source #

ToSym Char Char Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Char -> Char Source #

ToSym Int SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym Int Int Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int -> Int Source #

ToSym Word SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym Word Word Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word -> Word Source #

ToSym Int16 (SymIntN 16) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int16 -> SymIntN 16 Source #

ToSym Int32 (SymIntN 32) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int32 -> SymIntN 32 Source #

ToSym Int64 (SymIntN 64) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int64 -> SymIntN 64 Source #

ToSym Int8 (SymIntN 8) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int8 -> SymIntN 8 Source #

ToSym Word16 (SymWordN 16) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word16 -> SymWordN 16 Source #

ToSym Word32 (SymWordN 32) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word32 -> SymWordN 32 Source #

ToSym Word64 (SymWordN 64) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word64 -> SymWordN 64 Source #

ToSym Word8 (SymWordN 8) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word8 -> SymWordN 8 Source #

ToSym Int (SymIntN 64) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int -> SymIntN 64 Source #

ToSym Word (SymWordN 64) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word -> SymWordN 64 Source #

(Generic a, Generic b, ToSym' (Rep a) (Rep b)) => ToSym a (Default b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: a -> Default b Source #

(ToSym a b, Mergeable b) => ToSym a (UnionM b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: a -> UnionM b Source #

ToSym (UnionM SomeIntN) SomeSymIntN Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

ToSym (UnionM SomeWordN) SomeSymWordN Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

ToSym (UnionM Integer) SymInteger Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

ToSym (UnionM Bool) SymBool Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: IntN n -> SomeSymIntN Source #

(KnownNat n, 1 <= n) => ToSym (WordN n) SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToSym a b => ToSym (Identity a) (Identity b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Identity a -> Identity b Source #

(KnownNat n, 1 <= n) => ToSym (UnionM (IntN n)) (SymIntN n) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: UnionM (IntN n) -> SymIntN n Source #

(KnownNat n, 1 <= n) => ToSym (UnionM (WordN n)) (SymWordN n) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: UnionM (WordN n) -> SymWordN n Source #

(ToSym a b, Mergeable b) => ToSym (UnionM a) (UnionM b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: UnionM a -> UnionM b Source #

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

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: IntN n -> IntN n Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: IntN n -> SymIntN n Source #

(KnownNat n, 1 <= n) => ToSym (WordN n) (WordN n) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: WordN n -> WordN n Source #

(KnownNat n, 1 <= n) => ToSym (WordN n) (SymWordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: WordN n -> SymWordN n Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: SymIntN n -> SymIntN n Source #

(KnownNat n, 1 <= n) => ToSym (SymWordN n) (SymWordN n) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: SymWordN n -> SymWordN n Source #

ToSym a b => ToSym (Maybe a) (Maybe b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Maybe a -> Maybe b Source #

ToSym a b => ToSym [a] [b] Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: [a] -> [b] Source #

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

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: UnionM (ca --> cb) -> sa -~> sb Source #

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

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: UnionM (ca =-> cb) -> sa =~> sb Source #

(ToSym e1 e2, ToSym a1 a2) => ToSym (Either e1 a1) (Either e2 a2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Either e1 a1 -> Either e2 a2 Source #

(ToSym e1 e2, ToSym a1 a2) => ToSym (Either e1 a1) (CBMCEither e2 a2) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toSym :: Either e1 a1 -> CBMCEither e2 a2 Source #

(ToSym e1 e2, ToSym a1 a2) => ToSym (CBMCEither e1 a1) (Either e2 a2) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toSym :: CBMCEither e1 a1 -> Either e2 a2 Source #

(ToSym e1 e2, ToSym a1 a2) => ToSym (CBMCEither e1 a1) (CBMCEither e2 a2) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toSym :: CBMCEither e1 a1 -> CBMCEither e2 a2 Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: (ca --> cb) -> sa -~> sb Source #

(SupportedPrim a, SupportedPrim b) => ToSym (a -~> b) (a -~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: (a -~> b) -> a -~> b Source #

(SupportedPrim a, SupportedPrim b) => ToSym (a =~> b) (a =~> b) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: (a =~> b) -> a =~> b Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: (ca =-> cb) -> sa =~> sb Source #

ToSym (m1 (Maybe a)) (m2 (Maybe b)) => ToSym (MaybeT m1 a) (MaybeT m2 b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: MaybeT m1 a -> MaybeT m2 b Source #

ToSym a b => ToSym (v -> a) (v -> b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (v -> a) -> v -> b Source #

(ToSym a1 b1, ToSym a2 b2) => ToSym (a1, a2) (b1, b2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, a2) -> (b1, b2) Source #

ToSym (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b)) => ToSym (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b) Source # 
Instance details

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toSym :: CBMCExceptT e1 m1 a -> CBMCExceptT e2 m2 b Source #

ToSym (m1 (Either e1 a)) (m2 (Either e2 b)) => ToSym (ExceptT e1 m1 a) (ExceptT e2 m2 b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: ExceptT e1 m1 a -> ExceptT e2 m2 b Source #

ToSym (m a) (m1 b) => ToSym (IdentityT m a) (IdentityT m1 b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: IdentityT m a -> IdentityT m1 b Source #

ToSym (s1 -> m1 a1) (s2 -> m2 a2) => ToSym (ReaderT s1 m1 a1) (ReaderT s2 m2 a2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: ReaderT s1 m1 a1 -> ReaderT s2 m2 a2 Source #

ToSym (s1 -> m1 (a1, s1)) (s2 -> m2 (a2, s2)) => ToSym (StateT s1 m1 a1) (StateT s2 m2 a2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: StateT s1 m1 a1 -> StateT s2 m2 a2 Source #

ToSym (s1 -> m1 (a1, s1)) (s2 -> m2 (a2, s2)) => ToSym (StateT s1 m1 a1) (StateT s2 m2 a2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: StateT s1 m1 a1 -> StateT s2 m2 a2 Source #

ToSym (m1 (a1, s1)) (m2 (a2, s2)) => ToSym (WriterT s1 m1 a1) (WriterT s2 m2 a2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: WriterT s1 m1 a1 -> WriterT s2 m2 a2 Source #

ToSym (m1 (a1, s1)) (m2 (a2, s2)) => ToSym (WriterT s1 m1 a1) (WriterT s2 m2 a2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: WriterT s1 m1 a1 -> WriterT s2 m2 a2 Source #

(ToSym a1 b1, ToSym a2 b2, ToSym a3 b3) => ToSym (a1, a2, a3) (b1, b2, b3) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, a2, a3) -> (b1, b2, b3) Source #

(ToSym (f a) (f1 a1), ToSym (g a) (g1 a1)) => ToSym (Sum f g a) (Sum f1 g1 a1) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Sum f g a -> Sum f1 g1 a1 Source #

(ToSym a1 a2, ToSym b1 b2, ToSym c1 c2, ToSym d1 d2) => ToSym (a1, b1, c1, d1) (a2, b2, c2, d2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, b1, c1, d1) -> (a2, b2, c2, d2) Source #

(ToSym a1 a2, ToSym b1 b2, ToSym c1 c2, ToSym d1 d2, ToSym e1 e2) => ToSym (a1, b1, c1, d1, e1) (a2, b2, c2, d2, e2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, b1, c1, d1, e1) -> (a2, b2, c2, d2, e2) Source #

(ToSym a1 a2, ToSym b1 b2, ToSym c1 c2, ToSym d1 d2, ToSym e1 e2, ToSym f1 f2) => ToSym (a1, b1, c1, d1, e1, f1) (a2, b2, c2, d2, e2, f2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, b1, c1, d1, e1, f1) -> (a2, b2, c2, d2, e2, f2) Source #

(ToSym a1 a2, ToSym b1 b2, ToSym c1 c2, ToSym d1 d2, ToSym e1 e2, ToSym f1 f2, ToSym g1 g2) => ToSym (a1, b1, c1, d1, e1, f1, g1) (a2, b2, c2, d2, e2, f2, g2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, b1, c1, d1, e1, f1, g1) -> (a2, b2, c2, d2, e2, f2, g2) Source #

(ToSym a1 a2, ToSym b1 b2, ToSym c1 c2, ToSym d1 d2, ToSym e1 e2, ToSym f1 f2, ToSym g1 g2, ToSym h1 h2) => ToSym (a1, b1, c1, d1, e1, f1, g1, h1) (a2, b2, c2, d2, e2, f2, g2, h2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, b1, c1, d1, e1, f1, g1, h1) -> (a2, b2, c2, d2, e2, f2, g2, h2) Source #