Grisette.Core.Data.Class.ToCon

Converting to concrete values

class ToCon a b where

Convert a symbolic value to concrete value if possible.

Methods

toCon :: a -> Maybe b

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

ToCon Int16 Int16

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Int16 -> Maybe Int16

ToCon Int32 Int32

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Int32 -> Maybe Int32

ToCon Int64 Int64

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Int64 -> Maybe Int64

ToCon Int8 Int8

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Int8 -> Maybe Int8

ToCon Word16 Word16

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Word16 -> Maybe Word16

ToCon Word32 Word32

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Word32 -> Maybe Word32

ToCon Word64 Word64

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Word64 -> Maybe Word64

ToCon Word8 Word8

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Word8 -> Maybe Word8

ToCon ByteString ByteString

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: ByteString -> Maybe ByteString

ToCon AssertionError AssertionError

Defined in Grisette.Core.Control.Exception

Methods

toCon :: AssertionError -> Maybe AssertionError

ToCon VerificationConditions VerificationConditions

Defined in Grisette.Core.Control.Exception

Methods

toCon :: VerificationConditions -> Maybe VerificationConditions

ToCon SomeIntN SomeIntN

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: SomeIntN -> Maybe SomeIntN

ToCon SomeWordN SomeWordN

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: SomeWordN -> Maybe SomeWordN

ToCon SomeSymIntN SomeIntN

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SomeSymIntN -> Maybe SomeIntN

ToCon SomeSymIntN SomeSymIntN

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SomeSymIntN -> Maybe SomeSymIntN

ToCon SomeSymWordN SomeWordN

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SomeSymWordN -> Maybe SomeWordN

ToCon SomeSymWordN SomeSymWordN

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SomeSymWordN -> Maybe SomeSymWordN

ToCon SymBool SymBool

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymBool -> Maybe SymBool

ToCon SymBool Bool

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymBool -> Maybe Bool

ToCon SymInteger SymInteger

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymInteger -> Maybe SymInteger

ToCon SymInteger Integer

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymInteger -> Maybe Integer

ToCon Integer Integer

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Integer -> Maybe Integer

ToCon () ()

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: () -> Maybe ()

ToCon Bool Bool

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Bool -> Maybe Bool

ToCon Char Char

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Char -> Maybe Char

ToCon Int Int

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Int -> Maybe Int

ToCon Word Word

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Word -> Maybe Word

(Generic a, Generic b, ToCon' (Rep a) (Rep b)) => ToCon a (Default b)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: a -> Maybe (Default b)

ToCon v (Identity v)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: v -> Maybe (Identity v)

ToCon (Identity v) v

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Identity v -> Maybe v

ToCon a b => ToCon (UnionM a) b

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toCon :: UnionM a -> Maybe b

ToCon (SymIntN 8) Int8

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymIntN 8 -> Maybe Int8

ToCon (SymIntN 16) Int16

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymIntN 16 -> Maybe Int16

ToCon (SymIntN 32) Int32

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymIntN 32 -> Maybe Int32

ToCon (SymIntN 64) Int64

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymIntN 64 -> Maybe Int64

ToCon (SymIntN 64) Int

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymIntN 64 -> Maybe Int

ToCon (SymWordN 8) Word8

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymWordN 8 -> Maybe Word8

ToCon (SymWordN 16) Word16

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymWordN 16 -> Maybe Word16

ToCon (SymWordN 32) Word32

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymWordN 32 -> Maybe Word32

ToCon (SymWordN 64) Word64

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymWordN 64 -> Maybe Word64

ToCon (SymWordN 64) Word

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymWordN 64 -> Maybe Word

ToCon a b => ToCon (Identity a) (Identity b)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Identity a -> Maybe (Identity b)

(ToCon a b, Mergeable b) => ToCon (UnionM a) (UnionM b)

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toCon :: UnionM a -> Maybe (UnionM b)

(KnownNat n, 1 <= n) => ToCon (IntN n) (IntN n)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: IntN n -> Maybe (IntN n)

(KnownNat n, 1 <= n) => ToCon (WordN n) (WordN n)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: WordN n -> Maybe (WordN n)

(KnownNat n, 1 <= n) => ToCon (SymIntN n) (IntN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymIntN n -> Maybe (IntN n)

(KnownNat n, 1 <= n) => ToCon (SymIntN n) (SymIntN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymIntN n -> Maybe (SymIntN n)

(KnownNat n, 1 <= n) => ToCon (SymWordN n) (WordN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymWordN n -> Maybe (WordN n)

(KnownNat n, 1 <= n) => ToCon (SymWordN n) (SymWordN n)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymWordN n -> Maybe (SymWordN n)

ToCon a1 a2 => ToCon (Maybe a1) (Maybe a2)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Maybe a1 -> Maybe (Maybe a2)

ToCon a b => ToCon [a] [b]

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: [a] -> Maybe [b]

(ToCon e1 e2, ToCon a1 a2) => ToCon (Either e1 a1) (Either e2 a2)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Either e1 a1 -> Maybe (Either e2 a2)

(ToCon e1 e2, ToCon a1 a2) => ToCon (Either e1 a1) (CBMCEither e2 a2)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toCon :: Either e1 a1 -> Maybe (CBMCEither e2 a2)

(ToCon e1 e2, ToCon a1 a2) => ToCon (CBMCEither e1 a1) (Either e2 a2)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toCon :: CBMCEither e1 a1 -> Maybe (Either e2 a2)

(ToCon e1 e2, ToCon a1 a2) => ToCon (CBMCEither e1 a1) (CBMCEither e2 a2)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toCon :: CBMCEither e1 a1 -> Maybe (CBMCEither e2 a2)

(SupportedPrim a, SupportedPrim b) => ToCon (a -~> b) (a -~> b)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: (a -~> b) -> Maybe (a -~> b)

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa -~> sb) (ca --> cb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: (sa -~> sb) -> Maybe (ca --> cb)

(SupportedPrim a, SupportedPrim b) => ToCon (a =~> b) (a =~> b)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: (a =~> b) -> Maybe (a =~> b)

(SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToCon (sa =~> sb) (ca =-> cb)

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: (sa =~> sb) -> Maybe (ca =-> cb)

ToCon (m1 (Maybe a)) (m2 (Maybe b)) => ToCon (MaybeT m1 a) (MaybeT m2 b)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: MaybeT m1 a -> Maybe (MaybeT m2 b)

(ToCon a1 a2, ToCon b1 b2) => ToCon (a1, b1) (a2, b2)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: (a1, b1) -> Maybe (a2, b2)

ToCon (m1 (CBMCEither e1 a)) (Either e2 b) => ToCon (CBMCExceptT e1 m1 a) (Either e2 b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toCon :: CBMCExceptT e1 m1 a -> Maybe (Either e2 b)

ToCon (m1 (Either e1 a)) (Either e2 b) => ToCon (ExceptT e1 m1 a) (Either e2 b)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: ExceptT e1 m1 a -> Maybe (Either e2 b)

ToCon (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b)) => ToCon (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b)

Defined in Grisette.Core.Control.Monad.CBMCExcept

Methods

toCon :: CBMCExceptT e1 m1 a -> Maybe (CBMCExceptT e2 m2 b)

ToCon (m1 (Either e1 a)) (m2 (Either e2 b)) => ToCon (ExceptT e1 m1 a) (ExceptT e2 m2 b)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: ExceptT e1 m1 a -> Maybe (ExceptT e2 m2 b)

ToCon (m a) (m1 b) => ToCon (IdentityT m a) (IdentityT m1 b)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: IdentityT m a -> Maybe (IdentityT m1 b)

ToCon (m1 (a, s1)) (m2 (b, s2)) => ToCon (WriterT s1 m1 a) (WriterT s2 m2 b)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: WriterT s1 m1 a -> Maybe (WriterT s2 m2 b)

ToCon (m1 (a, s1)) (m2 (b, s2)) => ToCon (WriterT s1 m1 a) (WriterT s2 m2 b)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: WriterT s1 m1 a -> Maybe (WriterT s2 m2 b)

(ToCon a1 a2, ToCon b1 b2, ToCon c1 c2) => ToCon (a1, b1, c1) (a2, b2, c2)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: (a1, b1, c1) -> Maybe (a2, b2, c2)

(ToCon (f a) (f1 a1), ToCon (g a) (g1 a1)) => ToCon (Sum f g a) (Sum f1 g1 a1)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Sum f g a -> Maybe (Sum f1 g1 a1)

(ToCon a1 a2, ToCon b1 b2, ToCon c1 c2, ToCon d1 d2) => ToCon (a1, b1, c1, d1) (a2, b2, c2, d2)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: (a1, b1, c1, d1) -> Maybe (a2, b2, c2, d2)

(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)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: (a1, b1, c1, d1, e1) -> Maybe (a2, b2, c2, d2, e2)

(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)

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: (a1, b1, c1, d1, e1, f1) -> Maybe (a2, b2, c2, d2, e2, f2)

(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)

Defined in Grisette.Core.Data.Class.ToCon

Methods

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

(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)

Defined in Grisette.Core.Data.Class.ToCon

Methods

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