{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Grisette.Internal.Core.Data.Class.ExtractSymbolics
(
ExtractSymbolics (..),
)
where
import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
( Identity (Identity),
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.TypeNats (KnownNat, type (<=))
import Generics.Deriving
( Default (Default, unDefault),
Generic (Rep, from),
K1 (unK1),
M1 (unM1),
U1,
V1,
type (:*:) ((:*:)),
type (:+:) (L1, R1),
)
import Grisette.Internal.Core.Control.Exception (AssertionError, VerificationConditions)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.GeneralFun (type (-->))
import Grisette.Internal.SymPrim.Prim.Model
( SymbolSet (SymbolSet),
)
import Grisette.Internal.SymPrim.Prim.Term
( LinkedRep,
SupportedPrim,
)
import Grisette.Internal.SymPrim.Prim.TermUtils (extractSymbolicsTerm)
import Grisette.Internal.SymPrim.SymBV
( SymIntN (SymIntN),
SymWordN (SymWordN),
)
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun))
import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))
import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))
import Grisette.Internal.SymPrim.TabularFun (type (=->))
class a where
:: a -> SymbolSet
#define CONCRETE_EXTRACT_SYMBOLICS(type) \
instance ExtractSymbolics type where \
extractSymbolics _ = mempty
#define CONCRETE_EXTRACT_SYMBOLICS_BV(type) \
instance (KnownNat n, 1 <= n) => ExtractSymbolics (type n) where \
extractSymbolics _ = mempty
#if 1
CONCRETE_EXTRACT_SYMBOLICS(Bool)
CONCRETE_EXTRACT_SYMBOLICS(Integer)
CONCRETE_EXTRACT_SYMBOLICS(Char)
CONCRETE_EXTRACT_SYMBOLICS(Int)
CONCRETE_EXTRACT_SYMBOLICS(Int8)
CONCRETE_EXTRACT_SYMBOLICS(Int16)
CONCRETE_EXTRACT_SYMBOLICS(Int32)
CONCRETE_EXTRACT_SYMBOLICS(Int64)
CONCRETE_EXTRACT_SYMBOLICS(Word)
CONCRETE_EXTRACT_SYMBOLICS(Word8)
CONCRETE_EXTRACT_SYMBOLICS(Word16)
CONCRETE_EXTRACT_SYMBOLICS(Word32)
CONCRETE_EXTRACT_SYMBOLICS(Word64)
CONCRETE_EXTRACT_SYMBOLICS(B.ByteString)
CONCRETE_EXTRACT_SYMBOLICS(T.Text)
CONCRETE_EXTRACT_SYMBOLICS_BV(WordN)
CONCRETE_EXTRACT_SYMBOLICS_BV(IntN)
#endif
instance ExtractSymbolics () where
extractSymbolics :: () -> SymbolSet
extractSymbolics ()
_ = SymbolSet
forall a. Monoid a => a
mempty
deriving via
(Default (Either a b))
instance
(ExtractSymbolics a, ExtractSymbolics b) =>
ExtractSymbolics (Either a b)
deriving via
(Default (Maybe a))
instance
(ExtractSymbolics a) => ExtractSymbolics (Maybe a)
deriving via
(Default [a])
instance
(ExtractSymbolics a) => ExtractSymbolics [a]
deriving via
(Default (a, b))
instance
(ExtractSymbolics a, ExtractSymbolics b) =>
ExtractSymbolics (a, b)
deriving via
(Default (a, b, c))
instance
(ExtractSymbolics a, ExtractSymbolics b, ExtractSymbolics c) =>
ExtractSymbolics (a, b, c)
deriving via
(Default (a, b, c, d))
instance
( ExtractSymbolics a,
ExtractSymbolics b,
ExtractSymbolics c,
ExtractSymbolics d
) =>
ExtractSymbolics (a, b, c, d)
deriving via
(Default (a, b, c, d, e))
instance
( ExtractSymbolics a,
ExtractSymbolics b,
ExtractSymbolics c,
ExtractSymbolics d,
ExtractSymbolics e
) =>
ExtractSymbolics (a, b, c, d, e)
deriving via
(Default (a, b, c, d, e, f))
instance
( ExtractSymbolics a,
ExtractSymbolics b,
ExtractSymbolics c,
ExtractSymbolics d,
ExtractSymbolics e,
ExtractSymbolics f
) =>
ExtractSymbolics (a, b, c, d, e, f)
deriving via
(Default (a, b, c, d, e, f, g))
instance
( ExtractSymbolics a,
ExtractSymbolics b,
ExtractSymbolics c,
ExtractSymbolics d,
ExtractSymbolics e,
ExtractSymbolics f,
ExtractSymbolics g
) =>
ExtractSymbolics (a, b, c, d, e, f, g)
deriving via
(Default (a, b, c, d, e, f, g, h))
instance
( ExtractSymbolics a,
ExtractSymbolics b,
ExtractSymbolics c,
ExtractSymbolics d,
ExtractSymbolics e,
ExtractSymbolics f,
ExtractSymbolics g,
ExtractSymbolics h
) =>
ExtractSymbolics (a, b, c, d, e, f, g, h)
instance (ExtractSymbolics (m (Maybe a))) => ExtractSymbolics (MaybeT m a) where
extractSymbolics :: MaybeT m a -> SymbolSet
extractSymbolics (MaybeT m (Maybe a)
v) = m (Maybe a) -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics m (Maybe a)
v
instance
(ExtractSymbolics (m (Either e a))) =>
ExtractSymbolics (ExceptT e m a)
where
extractSymbolics :: ExceptT e m a -> SymbolSet
extractSymbolics (ExceptT m (Either e a)
v) = m (Either e a) -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics m (Either e a)
v
deriving via
(Default (Sum f g a))
instance
(ExtractSymbolics (f a), ExtractSymbolics (g a)) =>
ExtractSymbolics (Sum f g a)
instance
(ExtractSymbolics (m (a, s))) =>
ExtractSymbolics (WriterLazy.WriterT s m a)
where
extractSymbolics :: WriterT s m a -> SymbolSet
extractSymbolics (WriterLazy.WriterT m (a, s)
f) = m (a, s) -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics m (a, s)
f
instance
(ExtractSymbolics (m (a, s))) =>
ExtractSymbolics (WriterStrict.WriterT s m a)
where
extractSymbolics :: WriterT s m a -> SymbolSet
extractSymbolics (WriterStrict.WriterT m (a, s)
f) = m (a, s) -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics m (a, s)
f
instance (ExtractSymbolics a) => ExtractSymbolics (Identity a) where
extractSymbolics :: Identity a -> SymbolSet
extractSymbolics (Identity a
a) = a -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics a
a
instance (ExtractSymbolics (m a)) => ExtractSymbolics (IdentityT m a) where
extractSymbolics :: IdentityT m a -> SymbolSet
extractSymbolics (IdentityT m a
a) = m a -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics m a
a
#define EXTRACT_SYMBOLICS_SIMPLE(symtype) \
instance ExtractSymbolics symtype where \
extractSymbolics (symtype t) = SymbolSet $ extractSymbolicsTerm t
#define EXTRACT_SYMBOLICS_BV(symtype) \
instance (KnownNat n, 1 <= n) => ExtractSymbolics (symtype n) where \
extractSymbolics (symtype t) = SymbolSet $ extractSymbolicsTerm t
#define EXTRACT_SYMBOLICS_FUN(cop, op, cons) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
ExtractSymbolics (op sa sb) where \
extractSymbolics (cons t) = SymbolSet $ extractSymbolicsTerm t
#if 1
EXTRACT_SYMBOLICS_SIMPLE(SymBool)
EXTRACT_SYMBOLICS_SIMPLE(SymInteger)
EXTRACT_SYMBOLICS_BV(SymIntN)
EXTRACT_SYMBOLICS_BV(SymWordN)
EXTRACT_SYMBOLICS_FUN((=->), (=~>), SymTabularFun)
EXTRACT_SYMBOLICS_FUN((-->), (-~>), SymGeneralFun)
#endif
deriving via (Default AssertionError) instance ExtractSymbolics AssertionError
deriving via (Default VerificationConditions) instance ExtractSymbolics VerificationConditions
instance (Generic a, ExtractSymbolics' (Rep a)) => ExtractSymbolics (Default a) where
extractSymbolics :: Default a -> SymbolSet
extractSymbolics = Rep a Any -> SymbolSet
forall c. Rep a c -> SymbolSet
forall (a :: * -> *) c. ExtractSymbolics' a => a c -> SymbolSet
extractSymbolics' (Rep a Any -> SymbolSet)
-> (Default a -> Rep a Any) -> Default a -> SymbolSet
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 (a -> Rep a Any) -> (Default a -> a) -> Default a -> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Default a -> a
forall a. Default a -> a
unDefault
class a where
:: a c -> SymbolSet
instance ExtractSymbolics' U1 where
extractSymbolics' :: forall c. U1 c -> SymbolSet
extractSymbolics' U1 c
_ = SymbolSet
forall a. Monoid a => a
mempty
instance ExtractSymbolics' V1 where
extractSymbolics' :: forall c. V1 c -> SymbolSet
extractSymbolics' V1 c
_ = SymbolSet
forall a. Monoid a => a
mempty
instance (ExtractSymbolics c) => ExtractSymbolics' (K1 i c) where
extractSymbolics' :: forall c. K1 i c c -> SymbolSet
extractSymbolics' = c -> SymbolSet
forall a. ExtractSymbolics a => a -> SymbolSet
extractSymbolics (c -> SymbolSet) -> (K1 i c c -> c) -> K1 i c c -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. K1 i c c -> c
forall k i c (p :: k). K1 i c p -> c
unK1
instance (ExtractSymbolics' a) => ExtractSymbolics' (M1 i c a) where
extractSymbolics' :: forall c. M1 i c a c -> SymbolSet
extractSymbolics' = a c -> SymbolSet
forall c. a c -> SymbolSet
forall (a :: * -> *) c. ExtractSymbolics' a => a c -> SymbolSet
extractSymbolics' (a c -> SymbolSet)
-> (M1 i c a c -> a c) -> M1 i c a c -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. M1 i c a c -> a c
forall k i (c :: Meta) (f :: k -> *) (p :: k). M1 i c f p -> f p
unM1
instance
(ExtractSymbolics' a, ExtractSymbolics' b) =>
ExtractSymbolics' (a :+: b)
where
extractSymbolics' :: forall c. (:+:) a b c -> SymbolSet
extractSymbolics' (L1 a c
l) = a c -> SymbolSet
forall c. a c -> SymbolSet
forall (a :: * -> *) c. ExtractSymbolics' a => a c -> SymbolSet
extractSymbolics' a c
l
extractSymbolics' (R1 b c
r) = b c -> SymbolSet
forall c. b c -> SymbolSet
forall (a :: * -> *) c. ExtractSymbolics' a => a c -> SymbolSet
extractSymbolics' b c
r
instance
(ExtractSymbolics' a, ExtractSymbolics' b) =>
ExtractSymbolics' (a :*: b)
where
extractSymbolics' :: forall c. (:*:) a b c -> SymbolSet
extractSymbolics' (a c
l :*: b c
r) = a c -> SymbolSet
forall c. a c -> SymbolSet
forall (a :: * -> *) c. ExtractSymbolics' a => a c -> SymbolSet
extractSymbolics' a c
l SymbolSet -> SymbolSet -> SymbolSet
forall a. Semigroup a => a -> a -> a
<> b c -> SymbolSet
forall c. b c -> SymbolSet
forall (a :: * -> *) c. ExtractSymbolics' a => a c -> SymbolSet
extractSymbolics' b c
r