{-# 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.Internal.Core.Data.Class.ToSym
-- Copyright   :   (c) Sirui Lu 2021-2023
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Core.Data.Class.ToSym
  ( -- * Converting to symbolic values
    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,
    V1,
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
  )
import Grisette.Internal.Core.Control.Exception (AssertionError, VerificationConditions)
import Grisette.Internal.Core.Data.Class.BitCast (BitCast (bitCast))
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (con))
import Grisette.Internal.SymPrim.BV
  ( IntN,
    WordN,
  )
import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, ValidFP)
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.SymFP (SymFP, SymFP32, SymFP64, SymFPRoundingMode)
import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>))
import Grisette.Internal.SymPrim.SymInteger (SymInteger)
import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))
import Grisette.Internal.SymPrim.TabularFun (type (=->))

-- $setup
-- >>> import Grisette.SymPrim

-- | Convert a concrete value to symbolic value.
class ToSym a b where
  -- | Convert a concrete value to symbolic value.
  --
  -- >>> toSym False :: SymBool
  -- false
  --
  -- >>> toSym [False, True] :: [SymBool]
  -- [false,true]
  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(Float)
CONCRETE_TOSYM(Double)
CONCRETE_TOSYM(B.ByteString)
CONCRETE_TOSYM(T.Text)
CONCRETE_TOSYM(FPRoundingMode)
CONCRETE_TOSYM_BV(IntN)
CONCRETE_TOSYM_BV(WordN)
#endif

instance (ValidFP eb sb) => ToSym (FP eb sb) (FP eb sb) where
  toSym :: FP eb sb -> FP eb sb
toSym = FP eb sb -> FP eb sb
forall a. a -> a
id

-- Unit
instance ToSym () () where
  toSym :: () -> ()
toSym = () -> ()
forall a. a -> a
id

-- Either
deriving via (Default (Either e2 a2)) instance (ToSym e1 e2, ToSym a1 a2) => ToSym (Either e1 a1) (Either e2 a2)

-- Maybe
deriving via (Default (Maybe b)) instance (ToSym a b) => ToSym (Maybe a) (Maybe b)

-- List
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)

-- function
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

-- MaybeT
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

-- ExceptT
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

-- StateT
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

-- WriterT
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

-- ReaderT
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

-- Sum
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)

-- Identity
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

-- IdentityT
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(SymFPRoundingMode)
#endif

instance (ValidFP eb sb) => ToSym (SymFP eb sb) (SymFP eb sb) where
  toSym :: SymFP eb sb -> SymFP eb sb
toSym = SymFP eb sb -> SymFP eb sb
forall a. a -> a
id

#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 (conop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
  ToSym (conop ca cb) (symop sa sb) where \
  toSym = con

#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_SIMPLE(FPRoundingMode, SymFPRoundingMode)
#endif

instance (ValidFP eb sb) => ToSym (FP eb sb) (SymFP eb sb) where
  toSym :: FP eb sb -> SymFP eb sb
toSym = FP eb sb -> SymFP eb sb
forall c t. Solvable c t => c -> t
con

#define TOSYM_MACHINE_INTEGER(int, bv) \
instance ToSym int (bv) where \
  toSym = fromIntegral

#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)
#endif

instance ToSym Float SymFP32 where
  toSym :: Float -> SymFP32
toSym = FP 8 24 -> SymFP32
forall c t. Solvable c t => c -> t
con (FP 8 24 -> SymFP32) -> (Float -> FP 8 24) -> Float -> SymFP32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Float -> FP 8 24
forall from to. BitCast from to => from -> to
bitCast
  {-# INLINE toSym #-}

instance ToSym Double SymFP64 where
  toSym :: Double -> SymFP64
toSym = FP 11 53 -> SymFP64
forall c t. Solvable c t => c -> t
con (FP 11 53 -> SymFP64) -> (Double -> FP 11 53) -> Double -> SymFP64
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Double -> FP 11 53
forall from to. BitCast from to => from -> to
bitCast
  {-# INLINE toSym #-}

-- Exception
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' V1 V1 where
  toSym' :: forall c. V1 c -> V1 c
toSym' = V1 c -> V1 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