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

Contents

Converting to symbolic values

Description

Synopsis

class ToSym a b where
- toSym :: a -> b

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.Internal.Core.Data.Class.ToSym Methods toSym :: Int16 -> Int16 Source #
ToSym Int32 Int32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int32 -> Int32 Source #
ToSym Int64 Int64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int64 -> Int64 Source #
ToSym Int8 Int8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int8 -> Int8 Source #
ToSym Word16 Word16 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word16 -> Word16 Source #
ToSym Word32 Word32 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word32 -> Word32 Source #
ToSym Word64 Word64 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word64 -> Word64 Source #
ToSym Word8 Word8 Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word8 -> Word8 Source #
ToSym ByteString ByteString Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: ByteString -> ByteString Source #
ToSym AssertionError AssertionError Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: AssertionError -> AssertionError Source #
ToSym VerificationConditions VerificationConditions Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: VerificationConditions -> VerificationConditions Source #
ToSym SymBool SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: SymBool -> SymBool Source #
ToSym SymInteger SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: SymInteger -> SymInteger Source #
ToSym Text Text Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Text -> Text Source #
ToSym Integer SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Integer -> SymInteger Source #
ToSym Integer Integer Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Integer -> Integer Source #
ToSym () () Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: () -> () Source #
ToSym Bool SymBool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Bool -> SymBool Source #
ToSym Bool Bool Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Bool -> Bool Source #
ToSym Char Char Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Char -> Char Source #
ToSym Int Int Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int -> Int Source #
ToSym Word Word Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word -> Word Source #
ToSym Int16 (SymIntN 16) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int16 -> SymIntN 16 Source #
ToSym Int32 (SymIntN 32) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int32 -> SymIntN 32 Source #
ToSym Int64 (SymIntN 64) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int64 -> SymIntN 64 Source #
ToSym Int8 (SymIntN 8) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int8 -> SymIntN 8 Source #
ToSym Word16 (SymWordN 16) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word16 -> SymWordN 16 Source #
ToSym Word32 (SymWordN 32) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word32 -> SymWordN 32 Source #
ToSym Word64 (SymWordN 64) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word64 -> SymWordN 64 Source #
ToSym Word8 (SymWordN 8) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Word8 -> SymWordN 8 Source #
ToSym Int (SymIntN 64) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Int -> SymIntN 64 Source #
ToSym Word (SymWordN 64) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym 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.Internal.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.Internal.Core.Control.Monad.UnionM Methods toSym :: a -> UnionM b Source #
ToSym (UnionM Integer) SymInteger Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods toSym :: UnionM Integer -> SymInteger Source #
ToSym (UnionM Bool) SymBool Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods toSym :: UnionM Bool -> SymBool Source #
ToSym a b => ToSym (Identity a) (Identity b) Source #
Instance details Defined in Grisette.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.Core.Data.Class.ToSym Methods toSym :: IntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => ToSym (WordN n) (WordN n) Source #
Instance details Defined in Grisette.Internal.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.Internal.Core.Data.Class.ToSym Methods toSym :: WordN n -> SymWordN n Source #
(forall (n :: Nat). (KnownNat n, 1 <= n) => ToSym (cbv n) (sbv n)) => ToSym (SomeBV cbv) (SomeBV sbv) Source #
Instance details Defined in Grisette.Internal.SymPrim.SomeBV Methods toSym :: SomeBV cbv -> SomeBV sbv Source #
(KnownNat n, 1 <= n) => ToSym (SymIntN n) (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: SymIntN n -> SymIntN n Source #
(KnownNat n, 1 <= n) => ToSym (SymWordN n) (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: SymWordN n -> SymWordN n Source #
ToSym a b => ToSym (Maybe a) (Maybe b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Maybe a -> Maybe b Source #
ToSym a b => ToSym [a] [b] Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: [a] -> [b] Source #
(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (ca --> cb)) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Control.Monad.UnionM Methods toSym :: UnionM (ca --> cb) -> sa -~> sb Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (UnionM (ca =-> cb)) (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.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.Internal.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.Internal.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.Internal.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.Internal.Core.Control.Monad.CBMCExcept Methods toSym :: CBMCEither e1 a1 -> CBMCEither e2 a2 Source #
(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca --> cb) (sa -~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: (ca --> cb) -> sa -~> sb Source #
(SupportedPrim a, SupportedPrim b) => ToSym (a -~> b) (a -~> b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: (a -~> b) -> a -~> b Source #
(SupportedPrim a, SupportedPrim b) => ToSym (a =~> b) (a =~> b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: (a =~> b) -> a =~> b Source #
(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca =-> cb) (sa =~> sb) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym 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.Internal.Core.Data.Class.ToSym Methods toSym :: MaybeT m1 a -> MaybeT m2 b Source #
(ToSym a1 b1, ToSym a2 b2) => ToSym (a1, a2) (b1, b2) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: (a1, a2) -> (b1, b2) Source #
ToSym a b => ToSym (v -> a) (v -> b) Source #
Instance details Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: (v -> a) -> v -> b 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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.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.Internal.Core.Data.Class.ToSym Methods toSym :: (a1, b1, c1, d1, e1, f1, g1, h1) -> (a2, b2, c2, d2, e2, f2, g2, h2) Source #