| Copyright | (c) Sirui Lu 2021-2024 |
|---|---|
| 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.ToSym
Description
Synopsis
- class ToSym a b where
- toSym :: a -> b
- class (forall a b. ToSym a b => ToSym (f1 a) (f2 b)) => ToSym1 f1 f2 where
- liftToSym :: (a -> b) -> f1 a -> f2 b
- toSym1 :: (ToSym1 f1 f2, ToSym a b) => f1 a -> f2 b
- class (forall a b. ToSym a b => ToSym1 (f1 a) (f2 b)) => ToSym2 f1 f2 where
- liftToSym2 :: (a -> b) -> (c -> d) -> f1 a c -> f2 b d
- toSym2 :: (ToSym2 f1 f2, ToSym a b, ToSym c d) => f1 a c -> f2 b d
- data family ToSymArgs arity a b :: Type
- class GToSym arity f1 f2 where
- genericToSym :: (Generic a, Generic b, GToSym Arity0 (Rep a) (Rep b)) => a -> b
- genericLiftToSym :: (Generic1 f1, Generic1 f2, GToSym Arity1 (Rep1 f1) (Rep1 f2)) => (a -> b) -> f1 a -> f2 b
Converting to symbolic values
class ToSym a b where Source #
Convert a concrete value to symbolic value.
Methods
Convert a concrete value to symbolic value.
>>>toSym False :: SymBoolfalse
>>>toSym [False, True] :: [SymBool][false,true]
Instances
| ToSym All All Source # | |
| ToSym Any Any Source # | |
| ToSym Int16 Int16 Source # | |
| ToSym Int32 Int32 Source # | |
| ToSym Int64 Int64 Source # | |
| ToSym Int8 Int8 Source # | |
| ToSym Word16 Word16 Source # | |
| ToSym Word32 Word32 Source # | |
| ToSym Word64 Word64 Source # | |
| ToSym Word8 Word8 Source # | |
| ToSym ByteString ByteString Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: ByteString -> ByteString Source # | |
| ToSym Ordering Ordering Source # | |
| ToSym AssertionError AssertionError Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: AssertionError -> AssertionError Source # | |
| ToSym VerificationConditions VerificationConditions Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: VerificationConditions -> VerificationConditions Source # | |
| ToSym FPRoundingMode FPRoundingMode Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: FPRoundingMode -> FPRoundingMode Source # | |
| ToSym FPRoundingMode SymFPRoundingMode Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods | |
| ToSym SymBool SymBool Source # | |
| ToSym SymFPRoundingMode SymFPRoundingMode Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods | |
| ToSym SymInteger SymInteger Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: SymInteger -> SymInteger Source # | |
| ToSym Text Text Source # | |
| ToSym Integer SymInteger Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods toSym :: Integer -> SymInteger Source # | |
| ToSym Integer Integer Source # | |
| ToSym () () Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| ToSym Bool SymBool Source # | |
| ToSym Bool Bool Source # | |
| ToSym Char Char Source # | |
| ToSym Double SymFP64 Source # | |
| ToSym Double Double Source # | |
| ToSym Float SymFP32 Source # | |
| ToSym Float Float Source # | |
| ToSym Int Int Source # | |
| ToSym Word Word Source # | |
| ToSym a a Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| ToSym Int16 (SymIntN 16) Source # | |
| ToSym Int32 (SymIntN 32) Source # | |
| ToSym Int64 (SymIntN 64) Source # | |
| ToSym Int8 (SymIntN 8) Source # | |
| ToSym Word16 (SymWordN 16) Source # | |
| ToSym Word32 (SymWordN 32) Source # | |
| ToSym Word64 (SymWordN 64) Source # | |
| ToSym Word8 (SymWordN 8) Source # | |
| ToSym Int (SymIntN 64) Source # | |
| ToSym Word (SymWordN 64) Source # | |
| ToSym a b => ToSym a (Identity b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (Generic a, Generic b, GToSym Arity0 (Rep a) (Rep b)) => ToSym a (Default b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a b, Mergeable b) => ToSym a (Union b) Source # | |
Defined in Grisette.Internal.Core.Control.Monad.Union | |
| ToSym a b => ToSym (Identity a) b Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| ToSym (Union Integer) SymInteger Source # | |
Defined in Grisette.Internal.Core.Control.Monad.Union | |
| ToSym (Union Bool) SymBool Source # | |
| ToSym a b => ToSym (Identity a) (Identity b) Source # | |
| ToSym a_1 a_2 => ToSym (First a_1) (First a_2) Source # | |
| ToSym a_1 a_2 => ToSym (Last a_1) (Last a_2) Source # | |
| ToSym a_1 a_2 => ToSym (Down a_1) (Down a_2) Source # | |
| ToSym a_1 a_2 => ToSym (Dual a_1) (Dual a_2) Source # | |
| ToSym a_1 a_2 => ToSym (Product a_1) (Product a_2) Source # | |
| ToSym a_1 a_2 => ToSym (Sum a_1) (Sum a_2) Source # | |
| ToSym p0 p => ToSym (Par1 p0) (Par1 p) Source # | |
| (KnownNat n, 1 <= n) => ToSym (Union (IntN n)) (SymIntN n) Source # | |
| (KnownNat n, 1 <= n) => ToSym (Union (WordN n)) (SymWordN n) Source # | |
| ToSym a b => ToSym (Union a) (Union b) Source # | |
| (KnownNat n, 1 <= n) => ToSym (IntN n) (IntN n) Source # | |
| (KnownNat n, 1 <= n) => ToSym (IntN n) (SymIntN n) Source # | |
| (KnownNat n, 1 <= n) => ToSym (WordN n) (WordN n) Source # | |
| (KnownNat n, 1 <= n) => ToSym (WordN n) (SymWordN n) Source # | |
| (forall (n :: Nat). (KnownNat n, 1 <= n) => ToSym (cbv n) (sbv n)) => ToSym (SomeBV cbv) (SomeBV sbv) Source # | |
| (KnownNat n, 1 <= n) => ToSym (SymIntN n) (SymIntN n) Source # | |
| (KnownNat n, 1 <= n) => ToSym (SymWordN n) (SymWordN n) Source # | |
| ToSym a_1 a_2 => ToSym (Maybe a_1) (Maybe a_2) Source # | |
| ToSym a_1 a_2 => ToSym [a_1] [a_2] Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (Union (ca --> cb)) (sa -~> sb) Source # | |
| (SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (Union (ca =-> cb)) (sa =~> sb) Source # | |
| (Generic1 f1, Generic1 f2, GToSym Arity1 (Rep1 f1) (Rep1 f2), ToSym a b) => ToSym (f1 a) (Default1 f2 b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2) => ToSym (Either a_1 b_1) (Either a_2 b_2) Source # | |
| (ToSym e1 e2, ToSym a1 a2) => ToSym (Either e1 a1) (CBMCEither e2 a2) Source # | |
Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods toSym :: Either e1 a1 -> CBMCEither e2 a2 Source # | |
| ToSym (U1 p0) (U1 p) Source # | |
| ToSym (V1 p0) (V1 p) Source # | |
| (ToSym e1 e2, ToSym a1 a2) => ToSym (CBMCEither e1 a1) (Either e2 a2) Source # | |
Defined in Grisette.Internal.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 # | |
Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods toSym :: CBMCEither e1 a1 -> CBMCEither e2 a2 Source # | |
| ValidFP eb sb => ToSym (FP eb sb) (FP eb sb) Source # | |
| ValidFP eb sb => ToSym (FP eb sb) (SymFP eb sb) Source # | |
| (SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca --> cb) (sa -~> sb) Source # | |
| ValidFP eb sb => ToSym (SymFP eb sb) (SymFP eb sb) Source # | |
| (SupportedPrim a, SupportedPrim b) => ToSym (a -~> b) (a -~> b) Source # | |
| (SupportedPrim a, SupportedPrim b) => ToSym (a =~> b) (a =~> b) Source # | |
| (SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => ToSym (ca =-> cb) (sa =~> sb) Source # | |
| (ToSym1 m1 m2, ToSym a b) => ToSym (MaybeT m1 a) (MaybeT m2 b) Source # | |
| (ToSym a_1 a_2, ToSym b_1 b_2) => ToSym (a_1, b_1) (a_2, b_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym b d, ToSym c a) => ToSym (a -> b) (c -> d) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| ToSym a0 a => ToSym (Const a0 b0) (Const a b) Source # | |
| ToSym (f0 a0) (f a) => ToSym (Ap f0 a0) (Ap f a) Source # | |
| ToSym (f0 a0) (f a) => ToSym (Alt f0 a0) (Alt f a) Source # | |
| ToSym (f0 p0) (f p) => ToSym (Rec1 f0 p0) (Rec1 f p) Source # | |
| ToSym (m1 (CBMCEither e1 a)) (m2 (CBMCEither e2 b)) => ToSym (CBMCExceptT e1 m1 a) (CBMCExceptT e2 m2 b) Source # | |
Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept Methods toSym :: CBMCExceptT e1 m1 a -> CBMCExceptT e2 m2 b Source # | |
| (ToSym1 m1 m2, ToSym e1 e2, ToSym a b) => ToSym (ExceptT e1 m1 a) (ExceptT e2 m2 b) Source # | |
| (ToSym1 m m1, ToSym a b) => ToSym (IdentityT m a) (IdentityT m1 b) Source # | |
| (ToSym s2 s1, ToSym1 m1 m2, ToSym a1 a2) => ToSym (ReaderT s1 m1 a1) (ReaderT s2 m2 a2) Source # | |
| (ToSym1 m1 m2, ToSym a1 a2) => ToSym (StateT s m1 a1) (StateT s m2 a2) Source # | |
| (ToSym1 m1 m2, ToSym a1 a2) => ToSym (StateT s m1 a1) (StateT s m2 a2) Source # | |
| (ToSym1 m1 m2, ToSym a b, ToSym s1 s2) => ToSym (WriterT s1 m1 a) (WriterT s2 m2 b) Source # | |
| (ToSym1 m1 m2, ToSym a b, ToSym s1 s2) => ToSym (WriterT s1 m1 a) (WriterT s2 m2 b) Source # | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2) => ToSym (a_1, b_1, c_1) (a_2, b_2, c_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym (l0 a0) (l a), ToSym (r0 a0) (r a)) => ToSym (Product l0 r0 a0) (Product l r a) Source # | |
| (ToSym (l0 a0) (l a), ToSym (r0 a0) (r a)) => ToSym (Sum l0 r0 a0) (Sum l r a) Source # | |
| (ToSym (f0 p0) (f p), ToSym (g0 p0) (g p)) => ToSym ((f0 :*: g0) p0) ((f :*: g) p) Source # | |
| (ToSym (f0 p0) (f p), ToSym (g0 p0) (g p)) => ToSym ((f0 :+: g0) p0) ((f :+: g) p) Source # | |
| ToSym c0 c => ToSym (K1 i0 c0 p0) (K1 i c p) Source # | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2) => ToSym (a_1, b_1, c_1, d_1) (a_2, b_2, c_2, d_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| ToSym (f0 (g0 a0)) (f (g a)) => ToSym (Compose f0 g0 a0) (Compose f g a) Source # | |
| ToSym (f0 (g0 p0)) (f (g p)) => ToSym ((f0 :.: g0) p0) ((f :.: g) p) Source # | |
| ToSym (f0 p0) (f p) => ToSym (M1 i0 c0 f0 p0) (M1 i c f p) Source # | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2) => ToSym (a_1, b_1, c_1, d_1, e_1) (a_2, b_2, c_2, d_2, e_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2) => ToSym (a_1, b_1, c_1, d_1, e_1, f_1) (a_2, b_2, c_2, d_2, e_2, f_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2) => ToSym (a_1, b_1, c_1, d_1, e_1, f_1, g_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2) => ToSym (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2) => ToSym (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2) => ToSym (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1, j_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2, j_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2, ToSym k_1 k_2) => ToSym (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1, j_1, k_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2, j_2, k_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2, ToSym k_1 k_2, ToSym l_1 l_2) => ToSym (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1, j_1, k_1, l_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2, j_2, k_2, l_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2, ToSym k_1 k_2, ToSym l_1 l_2, ToSym m_1 m_2) => ToSym (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1, j_1, k_1, l_1, m_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2, j_2, k_2, l_2, m_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2, ToSym k_1 k_2, ToSym l_1 l_2, ToSym m_1 m_2, ToSym n_1 n_2) => ToSym (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1, j_1, k_1, l_1, m_1, n_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2, j_2, k_2, l_2, m_2, n_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2, ToSym k_1 k_2, ToSym l_1 l_2, ToSym m_1 m_2, ToSym n_1 n_2, ToSym o_1 o_2) => ToSym (a_1, b_1, c_1, d_1, e_1, f_1, g_1, h_1, i_1, j_1, k_1, l_1, m_1, n_1, o_1) (a_2, b_2, c_2, d_2, e_2, f_2, g_2, h_2, i_2, j_2, k_2, l_2, m_2, n_2, o_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
class (forall a b. ToSym a b => ToSym (f1 a) (f2 b)) => ToSym1 f1 f2 where Source #
Lifting of ToSym to unary type constructors.
Methods
liftToSym :: (a -> b) -> f1 a -> f2 b Source #
Lift a conversion to symbolic function to unary type constructors.
Instances
| ToSym1 Identity Identity Source # | |
| ToSym1 First First Source # | |
| ToSym1 Last Last Source # | |
| ToSym1 Down Down Source # | |
| ToSym1 Dual Dual Source # | |
| ToSym1 Product Product Source # | |
| ToSym1 Sum Sum Source # | |
| ToSym1 Union Union Source # | |
| ToSym1 Maybe Maybe Source # | |
| ToSym1 List List Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (Generic1 f1, Generic1 f2, GToSym Arity1 (Rep1 f1) (Rep1 f2)) => ToSym1 f1 (Default1 f2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| ToSym a_1 a_2 => ToSym1 (Either a_1) (Either a_2) Source # | |
| ToSym1 m1 m2 => ToSym1 (MaybeT m1) (MaybeT m2) Source # | |
| ToSym a_1 a_2 => ToSym1 ((,) a_1) ((,) a_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| ToSym a0 a => ToSym1 (Const a0 :: Type -> Type) (Const a :: Type -> Type) Source # | |
| ToSym1 f0 f => ToSym1 (Ap f0) (Ap f) Source # | |
| ToSym1 f0 f => ToSym1 (Alt f0) (Alt f) Source # | |
| (ToSym1 m1 m2, ToSym e1 e2) => ToSym1 (ExceptT e1 m1) (ExceptT e2 m2) Source # | |
| ToSym1 m m1 => ToSym1 (IdentityT m) (IdentityT m1) Source # | |
| (ToSym s2 s1, ToSym1 m1 m2) => ToSym1 (ReaderT s1 m1) (ReaderT s2 m2) Source # | |
| ToSym1 m1 m2 => ToSym1 (StateT s m1) (StateT s m2) Source # | |
| ToSym1 m1 m2 => ToSym1 (StateT s m1) (StateT s m2) Source # | |
| (ToSym1 m1 m2, ToSym s1 s2) => ToSym1 (WriterT s1 m1) (WriterT s2 m2) Source # | |
| (ToSym1 m1 m2, ToSym s1 s2) => ToSym1 (WriterT s1 m1) (WriterT s2 m2) Source # | |
| (ToSym a_1 a_2, ToSym b_1 b_2) => ToSym1 ((,,) a_1 b_1) ((,,) a_2 b_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym1 l0 l, ToSym1 r0 r) => ToSym1 (Product l0 r0) (Product l r) Source # | |
| (ToSym1 l0 l, ToSym1 r0 r) => ToSym1 (Sum l0 r0) (Sum l r) Source # | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2) => ToSym1 ((,,,) a_1 b_1 c_1) ((,,,) a_2 b_2 c_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| ToSym c a => ToSym1 ((->) a) ((->) c) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym1 f0 f, ToSym1 g0 g) => ToSym1 (Compose f0 g0) (Compose f g) Source # | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2) => ToSym1 ((,,,,) a_1 b_1 c_1 d_1) ((,,,,) a_2 b_2 c_2 d_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2) => ToSym1 ((,,,,,) a_1 b_1 c_1 d_1 e_1) ((,,,,,) a_2 b_2 c_2 d_2 e_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2) => ToSym1 ((,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1) ((,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2) => ToSym1 ((,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1) ((,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2) => ToSym1 ((,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1) ((,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2) => ToSym1 ((,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1) ((,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2) => ToSym1 ((,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1) ((,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2, ToSym k_1 k_2) => ToSym1 ((,,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1 k_1) ((,,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2 k_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2, ToSym k_1 k_2, ToSym l_1 l_2) => ToSym1 ((,,,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1 k_1 l_1) ((,,,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2 k_2 l_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2, ToSym k_1 k_2, ToSym l_1 l_2, ToSym m_1 m_2) => ToSym1 ((,,,,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1 k_1 l_1 m_1) ((,,,,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2 k_2 l_2 m_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| (ToSym a_1 a_2, ToSym b_1 b_2, ToSym c_1 c_2, ToSym d_1 d_2, ToSym e_1 e_2, ToSym f_1 f_2, ToSym g_1 g_2, ToSym h_1 h_2, ToSym i_1 i_2, ToSym j_1 j_2, ToSym k_1 k_2, ToSym l_1 l_2, ToSym m_1 m_2, ToSym n_1 n_2) => ToSym1 ((,,,,,,,,,,,,,,) a_1 b_1 c_1 d_1 e_1 f_1 g_1 h_1 i_1 j_1 k_1 l_1 m_1 n_1) ((,,,,,,,,,,,,,,) a_2 b_2 c_2 d_2 e_2 f_2 g_2 h_2 i_2 j_2 k_2 l_2 m_2 n_2) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
toSym1 :: (ToSym1 f1 f2, ToSym a b) => f1 a -> f2 b Source #
Lift the standard toSym to unary type constructors.
class (forall a b. ToSym a b => ToSym1 (f1 a) (f2 b)) => ToSym2 f1 f2 where Source #
Lifting of ToSym to binary type constructors.
Methods
liftToSym2 :: (a -> b) -> (c -> d) -> f1 a c -> f2 b d Source #
Lift conversion to symbolic functions to binary type constructors.
Instances
| ToSym2 Either Either Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods liftToSym2 :: (a -> b) -> (c -> d) -> Either a c -> Either b d Source # | |
| ToSym2 (,) (,) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods liftToSym2 :: (a -> b) -> (c -> d) -> (a, c) -> (b, d) Source # | |
| ToSym a b => ToSym2 ((,,) a) ((,,) b) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods liftToSym2 :: (a0 -> b0) -> (c -> d) -> (a, a0, c) -> (b, b0, d) Source # | |
| (ToSym a c, ToSym b d) => ToSym2 ((,,,) a b) ((,,,) c d) Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym Methods liftToSym2 :: (a0 -> b0) -> (c0 -> d0) -> (a, b, a0, c0) -> (c, d, b0, d0) Source # | |
toSym2 :: (ToSym2 f1 f2, ToSym a b, ToSym c d) => f1 a c -> f2 b d Source #
Lift the standard toSym to binary type constructors.
Generic ToSym
data family ToSymArgs arity a b :: Type Source #
The arguments to the generic toSym function.
Instances
| data ToSymArgs Arity0 _ _1 Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
| newtype ToSymArgs Arity1 a b Source # | |
Defined in Grisette.Internal.Core.Data.Class.ToSym | |
class GToSym arity f1 f2 where Source #
The class of types that can be generically converted to symbolic values.
Instances
| GToSym Arity1 Par1 Par1 Source # | |
| GToSym arity (U1 :: Type -> Type) (U1 :: Type -> Type) Source # | |
| GToSym arity (V1 :: Type -> Type) (V1 :: Type -> Type) Source # | |
| ToSym1 f1 f2 => GToSym Arity1 (Rec1 f1) (Rec1 f2) Source # | |
| (GToSym arity a b, GToSym arity c d) => GToSym arity (a :*: c) (b :*: d) Source # | |
| (GToSym arity a b, GToSym arity c d) => GToSym arity (a :+: c) (b :+: d) Source # | |
| ToSym a b => GToSym arity (K1 i a :: Type -> Type) (K1 i b :: Type -> Type) Source # | |
| (ToSym1 f1 f2, GToSym Arity1 g1 g2) => GToSym Arity1 (f1 :.: g1) (f2 :.: g2) Source # | |
| GToSym arity f1 f2 => GToSym arity (M1 i c1 f1) (M1 i c2 f2) Source # | |