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 :: SymBool
false
>>>
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 # | |