{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Core.Data.Class.ToSym
(
ToSym (..),
)
where
import Control.Monad.Identity
( Identity (Identity),
IdentityT (IdentityT),
)
import Control.Monad.Reader (ReaderT (ReaderT))
import qualified Control.Monad.State.Lazy as StateLazy
import qualified Control.Monad.State.Strict as StateStrict
import Control.Monad.Trans.Except (ExceptT (ExceptT))
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.TypeNats (KnownNat, type (<=))
import Generics.Deriving
( Default (Default),
Generic (Rep, from, to),
K1 (K1),
M1 (M1),
U1,
type (:*:) ((:*:)),
type (:+:) (L1, R1),
)
import Grisette.Core.Control.Exception (AssertionError, VerificationConditions)
import Grisette.Core.Data.BV
( IntN,
SomeIntN (SomeIntN),
SomeWordN (SomeWordN),
WordN,
)
import Grisette.Core.Data.Class.Solvable (Solvable (con))
import Grisette.IR.SymPrim.Data.IntBitwidth (intBitwidthQ)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
( LinkedRep,
SupportedPrim,
type (-->),
)
import Grisette.IR.SymPrim.Data.SymPrim
( SomeSymIntN (SomeSymIntN),
SomeSymWordN (SomeSymWordN),
SymBool,
SymIntN,
SymInteger,
SymWordN,
type (-~>),
type (=~>),
)
import Grisette.IR.SymPrim.Data.TabularFun (type (=->))
class ToSym a b where
toSym :: a -> b
#define CONCRETE_TOSYM(type) \
instance ToSym type type where \
toSym = id
#define CONCRETE_TOSYM_BV(type) \
instance (KnownNat n, 1 <= n) => ToSym (type n) (type n) where \
toSym = id
#if 1
CONCRETE_TOSYM(Bool)
CONCRETE_TOSYM(Integer)
CONCRETE_TOSYM(Char)
CONCRETE_TOSYM(Int)
CONCRETE_TOSYM(Int8)
CONCRETE_TOSYM(Int16)
CONCRETE_TOSYM(Int32)
CONCRETE_TOSYM(Int64)
CONCRETE_TOSYM(Word)
CONCRETE_TOSYM(Word8)
CONCRETE_TOSYM(Word16)
CONCRETE_TOSYM(Word32)
CONCRETE_TOSYM(Word64)
CONCRETE_TOSYM(SomeIntN)
CONCRETE_TOSYM(SomeWordN)
CONCRETE_TOSYM(B.ByteString)
CONCRETE_TOSYM(T.Text)
CONCRETE_TOSYM_BV(IntN)
CONCRETE_TOSYM_BV(WordN)
#endif
instance ToSym () () where
toSym :: () -> ()
toSym = () -> ()
forall a. a -> a
id
deriving via (Default (Either e2 a2)) instance (ToSym e1 e2, ToSym a1 a2) => ToSym (Either e1 a1) (Either e2 a2)
deriving via (Default (Maybe b)) instance (ToSym a b) => ToSym (Maybe a) (Maybe b)
deriving via (Default [b]) instance (ToSym a b) => ToSym [a] [b]
deriving via (Default (b1, b2)) instance (ToSym a1 b1, ToSym a2 b2) => ToSym (a1, a2) (b1, b2)
deriving via (Default (b1, b2, b3)) instance (ToSym a1 b1, ToSym a2 b2, ToSym a3 b3) => ToSym (a1, a2, a3) (b1, b2, b3)
deriving via
(Default (a2, b2, c2, d2))
instance
(ToSym a1 a2, ToSym b1 b2, ToSym c1 c2, ToSym d1 d2) => ToSym (a1, b1, c1, d1) (a2, b2, c2, d2)
deriving via
(Default (a2, b2, c2, d2, e2))
instance
(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)
deriving via
(Default (a2, b2, c2, d2, e2, f2))
instance
(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)
deriving via
(Default (a2, b2, c2, d2, e2, f2, g2))
instance
(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)
deriving via
(Default (a2, b2, c2, d2, e2, f2, g2, h2))
instance
(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)
instance (ToSym a b) => ToSym (v -> a) (v -> b) where
toSym :: (v -> a) -> v -> b
toSym v -> a
f = a -> b
forall a b. ToSym a b => a -> b
toSym (a -> b) -> (v -> a) -> v -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> a
f
instance
(ToSym (m1 (Maybe a)) (m2 (Maybe b))) =>
ToSym (MaybeT m1 a) (MaybeT m2 b)
where
toSym :: MaybeT m1 a -> MaybeT m2 b
toSym (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) -> m2 (Maybe b) -> MaybeT m2 b
forall a b. (a -> b) -> a -> b
$ m1 (Maybe a) -> m2 (Maybe b)
forall a b. ToSym a b => a -> b
toSym m1 (Maybe a)
v
instance
(ToSym (m1 (Either e1 a)) (m2 (Either e2 b))) =>
ToSym (ExceptT e1 m1 a) (ExceptT e2 m2 b)
where
toSym :: ExceptT e1 m1 a -> ExceptT e2 m2 b
toSym (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)
-> m2 (Either e2 b) -> ExceptT e2 m2 b
forall a b. (a -> b) -> a -> b
$ m1 (Either e1 a) -> m2 (Either e2 b)
forall a b. ToSym a b => a -> b
toSym m1 (Either e1 a)
v
instance (ToSym (s1 -> m1 (a1, s1)) (s2 -> m2 (a2, s2))) => ToSym (StateLazy.StateT s1 m1 a1) (StateLazy.StateT s2 m2 a2) where
toSym :: StateT s1 m1 a1 -> StateT s2 m2 a2
toSym (StateLazy.StateT s1 -> m1 (a1, s1)
f1) = (s2 -> m2 (a2, s2)) -> StateT s2 m2 a2
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateLazy.StateT ((s2 -> m2 (a2, s2)) -> StateT s2 m2 a2)
-> (s2 -> m2 (a2, s2)) -> StateT s2 m2 a2
forall a b. (a -> b) -> a -> b
$ (s1 -> m1 (a1, s1)) -> s2 -> m2 (a2, s2)
forall a b. ToSym a b => a -> b
toSym s1 -> m1 (a1, s1)
f1
instance (ToSym (s1 -> m1 (a1, s1)) (s2 -> m2 (a2, s2))) => ToSym (StateStrict.StateT s1 m1 a1) (StateStrict.StateT s2 m2 a2) where
toSym :: StateT s1 m1 a1 -> StateT s2 m2 a2
toSym (StateStrict.StateT s1 -> m1 (a1, s1)
f1) = (s2 -> m2 (a2, s2)) -> StateT s2 m2 a2
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateStrict.StateT ((s2 -> m2 (a2, s2)) -> StateT s2 m2 a2)
-> (s2 -> m2 (a2, s2)) -> StateT s2 m2 a2
forall a b. (a -> b) -> a -> b
$ (s1 -> m1 (a1, s1)) -> s2 -> m2 (a2, s2)
forall a b. ToSym a b => a -> b
toSym s1 -> m1 (a1, s1)
f1
instance (ToSym (m1 (a1, s1)) (m2 (a2, s2))) => ToSym (WriterLazy.WriterT s1 m1 a1) (WriterLazy.WriterT s2 m2 a2) where
toSym :: WriterT s1 m1 a1 -> WriterT s2 m2 a2
toSym (WriterLazy.WriterT m1 (a1, s1)
f1) = m2 (a2, s2) -> WriterT s2 m2 a2
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterLazy.WriterT (m2 (a2, s2) -> WriterT s2 m2 a2)
-> m2 (a2, s2) -> WriterT s2 m2 a2
forall a b. (a -> b) -> a -> b
$ m1 (a1, s1) -> m2 (a2, s2)
forall a b. ToSym a b => a -> b
toSym m1 (a1, s1)
f1
instance (ToSym (m1 (a1, s1)) (m2 (a2, s2))) => ToSym (WriterStrict.WriterT s1 m1 a1) (WriterStrict.WriterT s2 m2 a2) where
toSym :: WriterT s1 m1 a1 -> WriterT s2 m2 a2
toSym (WriterStrict.WriterT m1 (a1, s1)
f1) = m2 (a2, s2) -> WriterT s2 m2 a2
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterStrict.WriterT (m2 (a2, s2) -> WriterT s2 m2 a2)
-> m2 (a2, s2) -> WriterT s2 m2 a2
forall a b. (a -> b) -> a -> b
$ m1 (a1, s1) -> m2 (a2, s2)
forall a b. ToSym a b => a -> b
toSym m1 (a1, s1)
f1
instance (ToSym (s1 -> m1 a1) (s2 -> m2 a2)) => ToSym (ReaderT s1 m1 a1) (ReaderT s2 m2 a2) where
toSym :: ReaderT s1 m1 a1 -> ReaderT s2 m2 a2
toSym (ReaderT s1 -> m1 a1
f1) = (s2 -> m2 a2) -> ReaderT s2 m2 a2
forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT ((s2 -> m2 a2) -> ReaderT s2 m2 a2)
-> (s2 -> m2 a2) -> ReaderT s2 m2 a2
forall a b. (a -> b) -> a -> b
$ (s1 -> m1 a1) -> s2 -> m2 a2
forall a b. ToSym a b => a -> b
toSym s1 -> m1 a1
f1
deriving via
(Default (Sum f1 g1 a1))
instance
(ToSym (f a) (f1 a1), ToSym (g a) (g1 a1)) => ToSym (Sum f g a) (Sum f1 g1 a1)
instance (ToSym a b) => ToSym (Identity a) (Identity b) where
toSym :: Identity a -> Identity b
toSym (Identity a
a) = b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> b -> Identity b
forall a b. (a -> b) -> a -> b
$ a -> b
forall a b. ToSym a b => a -> b
toSym a
a
instance (ToSym (m a) (m1 b)) => ToSym (IdentityT m a) (IdentityT m1 b) where
toSym :: IdentityT m a -> IdentityT m1 b
toSym (IdentityT m a
v) = m1 b -> IdentityT m1 b
forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (m1 b -> IdentityT m1 b) -> m1 b -> IdentityT m1 b
forall a b. (a -> b) -> a -> b
$ m a -> m1 b
forall a b. ToSym a b => a -> b
toSym m a
v
#define TO_SYM_SYMID_SIMPLE(symtype) \
instance ToSym symtype symtype where \
toSym = id
#define TO_SYM_SYMID_BV(symtype) \
instance (KnownNat n, 1 <= n) => ToSym (symtype n) (symtype n) where \
toSym = id
#define TO_SYM_SYMID_FUN(op) \
instance (SupportedPrim a, SupportedPrim b) => ToSym (a op b) (a op b) where \
toSym = id
#if 1
TO_SYM_SYMID_SIMPLE(SymBool)
TO_SYM_SYMID_SIMPLE(SymInteger)
TO_SYM_SYMID_BV(SymIntN)
TO_SYM_SYMID_BV(SymWordN)
TO_SYM_SYMID_FUN(=~>)
TO_SYM_SYMID_FUN(-~>)
TO_SYM_SYMID_SIMPLE(SomeSymIntN)
TO_SYM_SYMID_SIMPLE(SomeSymWordN)
#endif
#define TO_SYM_FROMCON_SIMPLE(contype, symtype) \
instance ToSym contype symtype where \
toSym = con
#define TO_SYM_FROMCON_BV(contype, symtype) \
instance (KnownNat n, 1 <= n) => ToSym (contype n) (symtype n) where \
toSym = con
#define TO_SYM_FROMCON_FUN(conop, symop) \
instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ToSym (conop ca cb) (symop sa sb) where \
toSym = con
#define TO_SYM_FROMCON_BV_SOME(contype, symtype) \
instance ToSym contype symtype where \
toSym (contype v) = symtype (con v)
#if 1
TO_SYM_FROMCON_SIMPLE(Bool, SymBool)
TO_SYM_FROMCON_SIMPLE(Integer, SymInteger)
TO_SYM_FROMCON_BV(IntN, SymIntN)
TO_SYM_FROMCON_BV(WordN, SymWordN)
TO_SYM_FROMCON_FUN((=->), (=~>))
TO_SYM_FROMCON_FUN((-->), (-~>))
TO_SYM_FROMCON_BV_SOME(SomeIntN, SomeSymIntN)
TO_SYM_FROMCON_BV_SOME(SomeWordN, SomeSymWordN)
#endif
#define TO_SYM_FROMBV_SOME(somesymbv, bv) \
instance (KnownNat n, 1 <= n) => ToSym (bv n) somesymbv where \
toSym = somesymbv . con
#if 1
TO_SYM_FROMBV_SOME(SomeSymIntN, IntN)
TO_SYM_FROMBV_SOME(SomeSymWordN, WordN)
#endif
#define TOSYM_MACHINE_INTEGER(int, bv) \
instance ToSym int (bv) where \
toSym = fromIntegral
#define TOSYM_MACHINE_INTEGER_SOME(int, somesymbv, bv, bitwidth) \
instance ToSym int somesymbv where \
toSym v = somesymbv (con (fromIntegral v :: bv bitwidth))
#if 1
TOSYM_MACHINE_INTEGER(Int8, SymIntN 8)
TOSYM_MACHINE_INTEGER(Int16, SymIntN 16)
TOSYM_MACHINE_INTEGER(Int32, SymIntN 32)
TOSYM_MACHINE_INTEGER(Int64, SymIntN 64)
TOSYM_MACHINE_INTEGER(Word8, SymWordN 8)
TOSYM_MACHINE_INTEGER(Word16, SymWordN 16)
TOSYM_MACHINE_INTEGER(Word32, SymWordN 32)
TOSYM_MACHINE_INTEGER(Word64, SymWordN 64)
TOSYM_MACHINE_INTEGER(Int, SymIntN $intBitwidthQ)
TOSYM_MACHINE_INTEGER(Word, SymWordN $intBitwidthQ)
TOSYM_MACHINE_INTEGER_SOME(Int8, SomeSymIntN, IntN, 8)
TOSYM_MACHINE_INTEGER_SOME(Int16, SomeSymIntN, IntN, 16)
TOSYM_MACHINE_INTEGER_SOME(Int32, SomeSymIntN, IntN, 32)
TOSYM_MACHINE_INTEGER_SOME(Int64, SomeSymIntN, IntN, 64)
TOSYM_MACHINE_INTEGER_SOME(Word8, SomeSymWordN, WordN, 8)
TOSYM_MACHINE_INTEGER_SOME(Word16, SomeSymWordN, WordN, 16)
TOSYM_MACHINE_INTEGER_SOME(Word32, SomeSymWordN, WordN, 32)
TOSYM_MACHINE_INTEGER_SOME(Word64, SomeSymWordN, WordN, 64)
TOSYM_MACHINE_INTEGER_SOME(Int, SomeSymIntN, IntN, $intBitwidthQ)
TOSYM_MACHINE_INTEGER_SOME(Word, SomeSymWordN, WordN, $intBitwidthQ)
#endif
deriving via
(Default AssertionError)
instance
ToSym AssertionError AssertionError
deriving via
(Default VerificationConditions)
instance
ToSym VerificationConditions VerificationConditions
instance (Generic a, Generic b, ToSym' (Rep a) (Rep b)) => ToSym a (Default b) where
toSym :: a -> Default b
toSym = b -> Default b
forall a. a -> Default a
Default (b -> Default b) -> (a -> b) -> a -> 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 (Rep b Any -> b) -> (a -> Rep b Any) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> Rep b Any
forall c. Rep a c -> Rep b c
forall (a :: * -> *) (b :: * -> *) c. ToSym' a b => a c -> b c
toSym' (Rep a Any -> Rep b Any) -> (a -> Rep a Any) -> a -> Rep b Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from
class ToSym' a b where
toSym' :: a c -> b c
instance ToSym' U1 U1 where
toSym' :: forall c. U1 c -> U1 c
toSym' = U1 c -> U1 c
forall a. a -> a
id
instance (ToSym a b) => ToSym' (K1 i a) (K1 i b) where
toSym' :: forall c. K1 i a c -> K1 i b c
toSym' (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) -> b -> K1 i b c
forall a b. (a -> b) -> a -> b
$ a -> b
forall a b. ToSym a b => a -> b
toSym a
a
instance (ToSym' a b) => ToSym' (M1 i c1 a) (M1 i c2 b) where
toSym' :: forall c. M1 i c1 a c -> M1 i c2 b c
toSym' (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) -> b c -> M1 i c2 b c
forall a b. (a -> b) -> a -> b
$ a c -> b c
forall c. a c -> b c
forall (a :: * -> *) (b :: * -> *) c. ToSym' a b => a c -> b c
toSym' a c
a
instance (ToSym' a1 a2, ToSym' b1 b2) => ToSym' (a1 :+: b1) (a2 :+: b2) where
toSym' :: forall c. (:+:) a1 b1 c -> (:+:) a2 b2 c
toSym' (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) -> a2 c -> (:+:) a2 b2 c
forall a b. (a -> b) -> a -> b
$ a1 c -> a2 c
forall c. a1 c -> a2 c
forall (a :: * -> *) (b :: * -> *) c. ToSym' a b => a c -> b c
toSym' a1 c
a
toSym' (R1 b1 c
b) = b2 c -> (:+:) a2 b2 c
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (b2 c -> (:+:) a2 b2 c) -> b2 c -> (:+:) a2 b2 c
forall a b. (a -> b) -> a -> b
$ b1 c -> b2 c
forall c. b1 c -> b2 c
forall (a :: * -> *) (b :: * -> *) c. ToSym' a b => a c -> b c
toSym' b1 c
b
instance (ToSym' a1 a2, ToSym' b1 b2) => ToSym' (a1 :*: b1) (a2 :*: b2) where
toSym' :: forall c. (:*:) a1 b1 c -> (:*:) a2 b2 c
toSym' (a1 c
a :*: b1 c
b) = a1 c -> a2 c
forall c. a1 c -> a2 c
forall (a :: * -> *) (b :: * -> *) c. ToSym' a b => a c -> b c
toSym' a1 c
a a2 c -> b2 c -> (:*:) a2 b2 c
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b1 c -> b2 c
forall c. b1 c -> b2 c
forall (a :: * -> *) (b :: * -> *) c. ToSym' a b => a c -> b c
toSym' b1 c
b