{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Internal.Core.Data.Class.ToCon
(
ToCon (..),
)
where
import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
( Identity (Identity, runIdentity),
IdentityT (IdentityT),
)
import Control.Monad.Trans.Maybe (MaybeT (MaybeT))
import qualified Control.Monad.Writer.Lazy as WriterLazy
import qualified Control.Monad.Writer.Strict as WriterStrict
import qualified Data.ByteString as B
import Data.Functor.Sum (Sum)
import Data.Int (Int16, Int32, Int64, Int8)
import qualified Data.Text as T
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.Generics (Generic (Rep, from, to), K1 (K1), M1 (M1), U1, V1, type (:*:) ((:*:)), type (:+:) (L1, R1))
import GHC.TypeNats (KnownNat, type (<=))
import Generics.Deriving (Default (Default))
import Generics.Deriving.Instances ()
import Grisette.Internal.Core.Control.Exception (AssertionError, VerificationConditions)
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (conView), pattern Con)
import Grisette.Internal.SymPrim.BV
( IntN (IntN),
WordN (WordN),
)
import Grisette.Internal.SymPrim.GeneralFun (type (-->))
import Grisette.Internal.SymPrim.IntBitwidth (intBitwidthQ)
import Grisette.Internal.SymPrim.Prim.Term
( LinkedRep,
SupportedPrim,
)
import Grisette.Internal.SymPrim.SymBV
( SymIntN,
SymWordN,
)
import Grisette.Internal.SymPrim.SymBool (SymBool)
import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>))
import Grisette.Internal.SymPrim.SymInteger (SymInteger)
import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))
import Grisette.Internal.SymPrim.TabularFun (type (=->))
class ToCon a b where
toCon :: a -> Maybe b
#define CONCRETE_TOCON(type) \
instance ToCon type type where \
toCon = Just
#define CONCRETE_TOCON_BV(type) \
instance (KnownNat n, 1 <= n) => ToCon (type n) (type n) where \
toCon = Just
#if 1
CONCRETE_TOCON(Bool)
CONCRETE_TOCON(Integer)
CONCRETE_TOCON(Char)
CONCRETE_TOCON(Int)
CONCRETE_TOCON(Int8)
CONCRETE_TOCON(Int16)
CONCRETE_TOCON(Int32)
CONCRETE_TOCON(Int64)
CONCRETE_TOCON(Word)
CONCRETE_TOCON(Word8)
CONCRETE_TOCON(Word16)
CONCRETE_TOCON(Word32)
CONCRETE_TOCON(Word64)
CONCRETE_TOCON(B.ByteString)
CONCRETE_TOCON(T.Text)
CONCRETE_TOCON_BV(WordN)
CONCRETE_TOCON_BV(IntN)
#endif
instance ToCon () () where
toCon :: () -> Maybe ()
toCon = () -> Maybe ()
forall a. a -> Maybe a
Just
deriving via (Default (Either e2 a2)) instance (ToCon e1 e2, ToCon a1 a2) => ToCon (Either e1 a1) (Either e2 a2)
deriving via (Default (Maybe a2)) instance (ToCon a1 a2) => ToCon (Maybe a1) (Maybe a2)
deriving via (Default [b]) instance (ToCon a b) => ToCon [a] [b]
deriving via (Default (a2, b2)) instance (ToCon a1 a2, ToCon b1 b2) => ToCon (a1, b1) (a2, b2)
deriving via (Default (a2, b2, c2)) instance (ToCon a1 a2, ToCon b1 b2, ToCon c1 c2) => ToCon (a1, b1, c1) (a2, b2, c2)
deriving via
(Default (a2, b2, c2, d2))
instance
(ToCon a1 a2, ToCon b1 b2, ToCon c1 c2, ToCon d1 d2) => ToCon (a1, b1, c1, d1) (a2, b2, c2, d2)
deriving via
(Default (a2, b2, c2, d2, e2))
instance
(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)
deriving via
(Default (a2, b2, c2, d2, e2, f2))
instance
(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)
deriving via
(Default (a2, b2, c2, d2, e2, f2, g2))
instance
(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)
deriving via
(Default (a2, b2, c2, d2, e2, f2, g2, h2))
instance
(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)
instance
(ToCon (m1 (Maybe a)) (m2 (Maybe b))) =>
ToCon (MaybeT m1 a) (MaybeT m2 b)
where
toCon :: MaybeT m1 a -> Maybe (MaybeT m2 b)
toCon (MaybeT m1 (Maybe a)
v) = m2 (Maybe b) -> MaybeT m2 b
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m2 (Maybe b) -> MaybeT m2 b)
-> Maybe (m2 (Maybe b)) -> Maybe (MaybeT m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m1 (Maybe a) -> Maybe (m2 (Maybe b))
forall a b. ToCon a b => a -> Maybe b
toCon m1 (Maybe a)
v
instance
(ToCon (m1 (Either e1 a)) (m2 (Either e2 b))) =>
ToCon (ExceptT e1 m1 a) (ExceptT e2 m2 b)
where
toCon :: ExceptT e1 m1 a -> Maybe (ExceptT e2 m2 b)
toCon (ExceptT m1 (Either e1 a)
v) = m2 (Either e2 b) -> ExceptT e2 m2 b
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (m2 (Either e2 b) -> ExceptT e2 m2 b)
-> Maybe (m2 (Either e2 b)) -> Maybe (ExceptT e2 m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m1 (Either e1 a) -> Maybe (m2 (Either e2 b))
forall a b. ToCon a b => a -> Maybe b
toCon m1 (Either e1 a)
v
instance
(ToCon (m1 (Either e1 a)) (Either e2 b)) =>
ToCon (ExceptT e1 m1 a) (Either e2 b)
where
toCon :: ExceptT e1 m1 a -> Maybe (Either e2 b)
toCon (ExceptT m1 (Either e1 a)
v) = m1 (Either e1 a) -> Maybe (Either e2 b)
forall a b. ToCon a b => a -> Maybe b
toCon m1 (Either e1 a)
v
deriving via
(Default (Sum f1 g1 a1))
instance
(ToCon (f a) (f1 a1), ToCon (g a) (g1 a1)) => ToCon (Sum f g a) (Sum f1 g1 a1)
instance
(ToCon (m1 (a, s1)) (m2 (b, s2))) =>
ToCon (WriterLazy.WriterT s1 m1 a) (WriterLazy.WriterT s2 m2 b)
where
toCon :: WriterT s1 m1 a -> Maybe (WriterT s2 m2 b)
toCon (WriterLazy.WriterT m1 (a, s1)
v) = m2 (b, s2) -> WriterT s2 m2 b
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterLazy.WriterT (m2 (b, s2) -> WriterT s2 m2 b)
-> Maybe (m2 (b, s2)) -> Maybe (WriterT s2 m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m1 (a, s1) -> Maybe (m2 (b, s2))
forall a b. ToCon a b => a -> Maybe b
toCon m1 (a, s1)
v
instance
(ToCon (m1 (a, s1)) (m2 (b, s2))) =>
ToCon (WriterStrict.WriterT s1 m1 a) (WriterStrict.WriterT s2 m2 b)
where
toCon :: WriterT s1 m1 a -> Maybe (WriterT s2 m2 b)
toCon (WriterStrict.WriterT m1 (a, s1)
v) = m2 (b, s2) -> WriterT s2 m2 b
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterStrict.WriterT (m2 (b, s2) -> WriterT s2 m2 b)
-> Maybe (m2 (b, s2)) -> Maybe (WriterT s2 m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m1 (a, s1) -> Maybe (m2 (b, s2))
forall a b. ToCon a b => a -> Maybe b
toCon m1 (a, s1)
v
instance (ToCon a b) => ToCon (Identity a) (Identity b) where
toCon :: Identity a -> Maybe (Identity b)
toCon (Identity a
a) = b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> Maybe b -> Maybe (Identity b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon a
a
instance ToCon (Identity v) v where
toCon :: Identity v -> Maybe v
toCon = v -> Maybe v
forall a. a -> Maybe a
Just (v -> Maybe v) -> (Identity v -> v) -> Identity v -> Maybe v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity v -> v
forall a. Identity a -> a
runIdentity
instance ToCon v (Identity v) where
toCon :: v -> Maybe (Identity v)
toCon = Identity v -> Maybe (Identity v)
forall a. a -> Maybe a
Just (Identity v -> Maybe (Identity v))
-> (v -> Identity v) -> v -> Maybe (Identity v)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> Identity v
forall a. a -> Identity a
Identity
instance (ToCon (m a) (m1 b)) => ToCon (IdentityT m a) (IdentityT m1 b) where
toCon :: IdentityT m a -> Maybe (IdentityT m1 b)
toCon (IdentityT m a
a) = m1 b -> IdentityT m1 b
forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (m1 b -> IdentityT m1 b) -> Maybe (m1 b) -> Maybe (IdentityT m1 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> Maybe (m1 b)
forall a b. ToCon a b => a -> Maybe b
toCon m a
a
#define TO_CON_SYMID_SIMPLE(symtype) \
instance ToCon symtype symtype where \
toCon = Just
#define TO_CON_SYMID_BV(symtype) \
instance (KnownNat n, 1 <= n) => ToCon (symtype n) (symtype n) where \
toCon = Just
#define TO_CON_SYMID_FUN(op) \
instance (SupportedPrim a, SupportedPrim b) => ToCon (a op b) (a op b) where \
toCon = Just
#if 1
TO_CON_SYMID_SIMPLE(SymBool)
TO_CON_SYMID_SIMPLE(SymInteger)
TO_CON_SYMID_BV(SymIntN)
TO_CON_SYMID_BV(SymWordN)
TO_CON_SYMID_FUN(=~>)
TO_CON_SYMID_FUN(-~>)
#endif
#define TO_CON_FROMSYM_SIMPLE(contype, symtype) \
instance ToCon symtype contype where \
toCon = conView
#define TO_CON_FROMSYM_BV(contype, symtype) \
instance (KnownNat n, 1 <= n) => ToCon (symtype n) (contype n) where \
toCon = conView
#define TO_CON_FROMSYM_FUN(conop, symop) \
instance (SupportedPrim (conop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
ToCon (symop sa sb) (conop ca cb) where \
toCon = conView
#if 1
TO_CON_FROMSYM_SIMPLE(Bool, SymBool)
TO_CON_FROMSYM_SIMPLE(Integer, SymInteger)
TO_CON_FROMSYM_BV(IntN, SymIntN)
TO_CON_FROMSYM_BV(WordN, SymWordN)
TO_CON_FROMSYM_FUN((=->), (=~>))
TO_CON_FROMSYM_FUN((-->), (-~>))
#endif
#define TOCON_MACHINE_INTEGER(sbvw, bvw, n, int) \
instance ToCon (sbvw n) int where \
toCon (Con (bvw v :: bvw n)) = Just $ fromIntegral v; \
toCon _ = Nothing
#if 1
TOCON_MACHINE_INTEGER(SymIntN, IntN, 8, Int8)
TOCON_MACHINE_INTEGER(SymIntN, IntN, 16, Int16)
TOCON_MACHINE_INTEGER(SymIntN, IntN, 32, Int32)
TOCON_MACHINE_INTEGER(SymIntN, IntN, 64, Int64)
TOCON_MACHINE_INTEGER(SymWordN, WordN, 8, Word8)
TOCON_MACHINE_INTEGER(SymWordN, WordN, 16, Word16)
TOCON_MACHINE_INTEGER(SymWordN, WordN, 32, Word32)
TOCON_MACHINE_INTEGER(SymWordN, WordN, 64, Word64)
TOCON_MACHINE_INTEGER(SymIntN, IntN, $intBitwidthQ, Int)
TOCON_MACHINE_INTEGER(SymWordN, WordN, $intBitwidthQ, Word)
#endif
deriving via
(Default AssertionError)
instance
ToCon AssertionError AssertionError
deriving via
(Default VerificationConditions)
instance
ToCon VerificationConditions VerificationConditions
instance (Generic a, Generic b, ToCon' (Rep a) (Rep b)) => ToCon a (Default b) where
toCon :: a -> Maybe (Default b)
toCon a
v = (Rep b Any -> Default b) -> Maybe (Rep b Any) -> Maybe (Default b)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (b -> Default b
forall a. a -> Default a
Default (b -> Default b) -> (Rep b Any -> b) -> Rep b Any -> Default b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep b Any -> b
forall a x. Generic a => Rep a x -> a
forall x. Rep b x -> b
to) (Maybe (Rep b Any) -> Maybe (Default b))
-> Maybe (Rep b Any) -> Maybe (Default b)
forall a b. (a -> b) -> a -> b
$ Rep a Any -> Maybe (Rep b Any)
forall c. Rep a c -> Maybe (Rep b c)
forall (a :: * -> *) (b :: * -> *) c.
ToCon' a b =>
a c -> Maybe (b c)
toCon' (Rep a Any -> Maybe (Rep b Any)) -> Rep a Any -> Maybe (Rep b Any)
forall a b. (a -> b) -> a -> b
$ a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from a
v
class ToCon' a b where
toCon' :: a c -> Maybe (b c)
instance ToCon' U1 U1 where
toCon' :: forall c. U1 c -> Maybe (U1 c)
toCon' = U1 c -> Maybe (U1 c)
forall a. a -> Maybe a
Just
instance ToCon' V1 V1 where
toCon' :: forall c. V1 c -> Maybe (V1 c)
toCon' = V1 c -> Maybe (V1 c)
forall a. a -> Maybe a
Just
instance (ToCon a b) => ToCon' (K1 i a) (K1 i b) where
toCon' :: forall c. K1 i a c -> Maybe (K1 i b c)
toCon' (K1 a
a) = b -> K1 i b c
forall k i c (p :: k). c -> K1 i c p
K1 (b -> K1 i b c) -> Maybe b -> Maybe (K1 i b c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon a
a
instance (ToCon' a b) => ToCon' (M1 i c1 a) (M1 i c2 b) where
toCon' :: forall c. M1 i c1 a c -> Maybe (M1 i c2 b c)
toCon' (M1 a c
a) = b c -> M1 i c2 b c
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (b c -> M1 i c2 b c) -> Maybe (b c) -> Maybe (M1 i c2 b c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a c -> Maybe (b c)
forall c. a c -> Maybe (b c)
forall (a :: * -> *) (b :: * -> *) c.
ToCon' a b =>
a c -> Maybe (b c)
toCon' a c
a
instance (ToCon' a1 a2, ToCon' b1 b2) => ToCon' (a1 :+: b1) (a2 :+: b2) where
toCon' :: forall c. (:+:) a1 b1 c -> Maybe ((:+:) a2 b2 c)
toCon' (L1 a1 c
a) = a2 c -> (:+:) a2 b2 c
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (a2 c -> (:+:) a2 b2 c) -> Maybe (a2 c) -> Maybe ((:+:) a2 b2 c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a1 c -> Maybe (a2 c)
forall c. a1 c -> Maybe (a2 c)
forall (a :: * -> *) (b :: * -> *) c.
ToCon' a b =>
a c -> Maybe (b c)
toCon' a1 c
a
toCon' (R1 b1 c
a) = b2 c -> (:+:) a2 b2 c
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (b2 c -> (:+:) a2 b2 c) -> Maybe (b2 c) -> Maybe ((:+:) a2 b2 c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> b1 c -> Maybe (b2 c)
forall c. b1 c -> Maybe (b2 c)
forall (a :: * -> *) (b :: * -> *) c.
ToCon' a b =>
a c -> Maybe (b c)
toCon' b1 c
a
instance (ToCon' a1 a2, ToCon' b1 b2) => ToCon' (a1 :*: b1) (a2 :*: b2) where
toCon' :: forall c. (:*:) a1 b1 c -> Maybe ((:*:) a2 b2 c)
toCon' (a1 c
a :*: b1 c
b) = do
a2 c
ac <- a1 c -> Maybe (a2 c)
forall c. a1 c -> Maybe (a2 c)
forall (a :: * -> *) (b :: * -> *) c.
ToCon' a b =>
a c -> Maybe (b c)
toCon' a1 c
a
b2 c
bc <- b1 c -> Maybe (b2 c)
forall c. b1 c -> Maybe (b2 c)
forall (a :: * -> *) (b :: * -> *) c.
ToCon' a b =>
a c -> Maybe (b c)
toCon' b1 c
b
(:*:) a2 b2 c -> Maybe ((:*:) a2 b2 c)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return ((:*:) a2 b2 c -> Maybe ((:*:) a2 b2 c))
-> (:*:) a2 b2 c -> Maybe ((:*:) a2 b2 c)
forall a b. (a -> b) -> a -> b
$ a2 c
ac a2 c -> b2 c -> (:*:) a2 b2 c
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b2 c
bc