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

Description

 
Synopsis

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

Methods

toSym :: Int16 -> Int16 Source #

ToSym Int32 Int32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int32 -> Int32 Source #

ToSym Int64 Int64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int64 -> Int64 Source #

ToSym Int8 Int8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int8 -> Int8 Source #

ToSym Word16 Word16 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word16 -> Word16 Source #

ToSym Word32 Word32 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word32 -> Word32 Source #

ToSym Word64 Word64 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word64 -> Word64 Source #

ToSym ByteString ByteString Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

ToSym AssertionError AssertionError Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ToSym VerificationConditions VerificationConditions Source # 
Instance details

Defined in Grisette.Core.Control.Exception

ToSym Word8 Word8 Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word8 -> Word8 Source #

ToSym Integer Integer Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

ToSym () () Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: () -> () Source #

ToSym Bool Bool Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Bool -> Bool Source #

ToSym Char Char Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Char -> Char Source #

ToSym Int Int Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Int -> Int Source #

ToSym Word Word Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Word -> Word Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int16 -> Sym (IntN 16) Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int32 -> Sym (IntN 32) Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int64 -> Sym (IntN 64) Source #

ToSym Int8 (Sym (IntN 8)) Source # 
Instance details

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int8 -> Sym (IntN 8) Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word16 -> Sym (WordN 16) Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word32 -> Sym (WordN 32) Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word64 -> Sym (WordN 64) Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word8 -> Sym (WordN 8) Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Int -> Sym (IntN 64) Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Word -> Sym (WordN 64) Source #

(Generic a, Generic b, ToSym' (Rep a) (Rep b)) => ToSym a (Default b) Source # 
Instance details

Defined in Grisette.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.Core.Control.Monad.UnionM

Methods

toSym :: a -> UnionM b Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: a -> Sym a Source #

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

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Identity a -> Identity b Source #

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

Defined in Grisette.Core.Control.Monad.UnionM

Methods

toSym :: UnionM a -> UnionM b Source #

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

Defined in Grisette.IR.SymPrim.Data.SymPrim

Methods

toSym :: Sym a -> Sym a Source #

ToSym a b => ToSym (Maybe a) (Maybe b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: Maybe a -> Maybe b Source #

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

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: [a] -> [b] Source #

(ToSym e1 e2, ToSym a1 a2) => ToSym (Either e1 a1) (Either e2 a2) Source # 
Instance details

Defined in Grisette.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.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.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.Core.Control.Monad.CBMCExcept

Methods

toSym :: CBMCEither e1 a1 -> CBMCEither e2 a2 Source #

ToSym (m1 (Maybe a)) (m2 (Maybe b)) => ToSym (MaybeT m1 a) (MaybeT m2 b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: MaybeT m1 a -> MaybeT m2 b Source #

ToSym a b => ToSym (v -> a) (v -> b) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (v -> a) -> v -> b Source #

(ToSym a1 b1, ToSym a2 b2) => ToSym (a1, a2) (b1, b2) Source # 
Instance details

Defined in Grisette.Core.Data.Class.ToSym

Methods

toSym :: (a1, a2) -> (b1, b2) 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.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.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.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.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.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.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.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.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.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.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.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.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.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.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.Core.Data.Class.ToSym

Methods

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