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

Contents

Converting to concrete values

Description

Synopsis

class ToCon a b where
- toCon :: a -> Maybe b

Converting to concrete values

class ToCon a b where Source #

Convert a symbolic value to concrete value if possible.

Methods

toCon :: a -> Maybe b Source #

Convert a symbolic value to concrete value if possible. If the symbolic value cannot be converted to concrete, the result will be Nothing.

>>> toCon (ssym "a" :: SymInteger) :: Maybe Integer
Nothing

>>> toCon (con 1 :: SymInteger) :: Maybe Integer
Just 1

toCon works on complex types too.

>>> toCon ([con 1, con 2] :: [SymInteger]) :: Maybe [Integer]
Just [1,2]

>>> toCon ([con 1, ssym "a"] :: [SymInteger]) :: Maybe [Integer]
Nothing

Instances

Instances details

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