grisette-0.1.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 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 Word8 Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToCon

Methods

toCon :: Word8 -> Maybe Word8 Source #

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 (Sym (IntN 8)) Int8 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 8) -> Maybe Int8 Source #

ToCon (Sym (IntN 16)) Int16 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 16) -> Maybe Int16 Source #

ToCon (Sym (IntN 32)) Int32 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 32) -> Maybe Int32 Source #

ToCon (Sym (IntN 64)) Int64 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 64) -> Maybe Int64 Source #

ToCon (Sym (IntN 64)) Int Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (IntN 64) -> Maybe Int Source #

ToCon (Sym (WordN 8)) Word8 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 8) -> Maybe Word8 Source #

ToCon (Sym (WordN 16)) Word16 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 16) -> Maybe Word16 Source #

ToCon (Sym (WordN 32)) Word32 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 32) -> Maybe Word32 Source #

ToCon (Sym (WordN 64)) Word64 Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 64) -> Maybe Word64 Source #

ToCon (Sym (WordN 64)) Word Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym (WordN 64) -> Maybe Word Source #

SupportedPrim a => ToCon (Sym a) a Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym a -> Maybe a 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 #

SupportedPrim a => ToCon (Sym a) (Sym a) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toCon :: Sym a -> Maybe (Sym a) 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 #

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 #