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

Description

 
Synopsis

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

Methods

toCon :: Int16 -> Maybe Int16 Source #

ToCon Int32 Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Int32 -> Maybe Int32 Source #

ToCon Int64 Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Int64 -> Maybe Int64 Source #

ToCon Int8 Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Int8 -> Maybe Int8 Source #

ToCon Word16 Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

ToCon Word32 Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

ToCon Word64 Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

ToCon Word8 Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Word8 -> Maybe Word8 Source #

ToCon ByteString ByteString Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

ToCon AssertionError AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ToCon VerificationConditions VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ToCon SomeIntN SomeIntN Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

ToCon SomeWordN SomeWordN Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

ToCon SomeSymIntN SomeIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToCon SomeSymIntN SomeSymIntN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToCon SomeSymWordN SomeWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToCon SomeSymWordN SomeSymWordN Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToCon SymBool SymBool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToCon SymBool Bool Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToCon SymInteger SymInteger Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToCon SymInteger Integer Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

ToCon Integer Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

ToCon () () Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: () -> Maybe () Source #

ToCon Bool Bool Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Bool -> Maybe Bool Source #

ToCon Char Char Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Char -> Maybe Char Source #

ToCon Int Int Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Int -> Maybe Int Source #

ToCon Word Word Source # 
Instance details

Defined in Grisette.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.Core.Data.Class.ToCon

Methods

toCon :: a -> Maybe (Default b) Source #

ToCon v (Identity v) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: v -> Maybe (Identity v) Source #

ToCon (Identity v) v Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Identity v -> Maybe v Source #

ToCon a b => ToCon (UnionM a) b Source # 
Instance details

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toCon :: UnionM a -> Maybe b Source #

ToCon (SymIntN 8) Int8 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymIntN 8 -> Maybe Int8 Source #

ToCon (SymIntN 16) Int16 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymIntN 16 -> Maybe Int16 Source #

ToCon (SymIntN 32) Int32 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymIntN 32 -> Maybe Int32 Source #

ToCon (SymIntN 64) Int64 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymIntN 64 -> Maybe Int64 Source #

ToCon (SymIntN 64) Int Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymIntN 64 -> Maybe Int Source #

ToCon (SymWordN 8) Word8 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymWordN 8 -> Maybe Word8 Source #

ToCon (SymWordN 16) Word16 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymWordN 16 -> Maybe Word16 Source #

ToCon (SymWordN 32) Word32 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymWordN 32 -> Maybe Word32 Source #

ToCon (SymWordN 64) Word64 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymWordN 64 -> Maybe Word64 Source #

ToCon (SymWordN 64) Word Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: SymWordN 64 -> Maybe Word Source #

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

Defined in Grisette.Core.Data.Class.ToCon

Methods

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

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

Defined in Grisette.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.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.Core.Data.Class.ToCon

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

ToCon a1 a2 => ToCon (Maybe a1) (Maybe a2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

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

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

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

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

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

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

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

Methods

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