{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.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.Core.Data.Class.ToSym
  ( -- * Converting to symbolic values
    ToSym (..),
  )
where

import Control.Monad.Identity
import Control.Monad.Reader
import qualified Control.Monad.State.Lazy as StateLazy
import qualified Control.Monad.State.Strict as StateStrict
import Control.Monad.Trans.Except
import Control.Monad.Trans.Maybe
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
import Data.Int
import Data.Word
import GHC.TypeNats
import Generics.Deriving
import Grisette.Core.Data.BV

-- $setup
-- >>> import Grisette.IR.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

instance (Generic a, Generic b, ToSym' (Rep a) (Rep b)) => ToSym a (Default b) where
  toSym :: a -> Default b
toSym = forall a. a -> Default a
Default forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a x. Generic a => Rep a x -> a
to forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> *) (b :: * -> *) c. ToSym' a b => a c -> b c
toSym' forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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' = 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) = forall k i c (p :: k). c -> K1 i c p
K1 forall 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) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall a b. (a -> b) -> a -> b
$ 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) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall a b. (a -> b) -> a -> b
$ forall (a :: * -> *) (b :: * -> *) c. ToSym' a b => a c -> b c
toSym' a1 c
a
  toSym' (R1 b1 c
b) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall a b. (a -> b) -> a -> b
$ 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) = forall (a :: * -> *) (b :: * -> *) c. ToSym' a b => a c -> b c
toSym' a1 c
a forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (a :: * -> *) (b :: * -> *) c. ToSym' a b => a c -> b c
toSym' b1 c
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_BV(IntN)
CONCRETE_TOSYM_BV(WordN)
#endif

-- 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 = forall a b. ToSym a b => a -> b
toSym 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) = forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> 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) = forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall a b. (a -> b) -> a -> 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) = forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateLazy.StateT forall a b. (a -> b) -> a -> b
$ 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) = forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateStrict.StateT forall a b. (a -> b) -> a -> b
$ 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) = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterLazy.WriterT forall a b. (a -> b) -> a -> b
$ 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) = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterStrict.WriterT forall a b. (a -> b) -> a -> b
$ 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) = forall r (m :: * -> *) a. (r -> m a) -> ReaderT r m a
ReaderT forall a b. (a -> b) -> a -> b
$ 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) = forall a. a -> Identity a
Identity forall 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) = forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT forall a b. (a -> b) -> a -> b
$ forall a b. ToSym a b => a -> b
toSym m a
v