{-# 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.ToCon
-- 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.ToCon
  ( -- * Converting to concrete values
    ToCon (..),
  )
where

import Control.Monad.Except
import Control.Monad.Identity
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.Generics
import GHC.TypeNats
import Generics.Deriving
import Generics.Deriving.Instances ()
import Grisette.Core.Data.BV

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

-- | Convert a symbolic value to concrete value if possible.
class ToCon a b where
  -- | Convert a symbolic value to concrete value if possible.
  -- If the symbolic value cannot be converted to concrete, the result will be 'Nothing'.
  --
  -- >>> toCon (ssym "a" :: SymInteger) :: Maybe Integer
  -- Nothing
  --
  -- >>> toCon (con 1 :: SymInteger) :: Maybe Integer
  -- Just 1
  --
  -- 'toCon' works on complex types too.
  --
  -- >>> toCon ([con 1, con 2] :: [SymInteger]) :: Maybe [Integer]
  -- Just [1,2]
  --
  -- >>> toCon ([con 1, ssym "a"] :: [SymInteger]) :: Maybe [Integer]
  -- Nothing
  toCon :: a -> Maybe b

instance (Generic a, Generic b, ToCon' (Rep a) (Rep b)) => ToCon a (Default b) where
  toCon :: a -> Maybe (Default b)
toCon a
v = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (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 a b. (a -> b) -> a -> b
$ forall (a :: * -> *) (b :: * -> *) c.
ToCon' a b =>
a c -> Maybe (b c)
toCon' forall a b. (a -> b) -> a -> b
$ 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' = 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) = forall k i c (p :: k). c -> K1 i c p
K1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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) = forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (a :: * -> *) (b :: * -> *) c.
ToCon' a b =>
a c -> Maybe (b c)
toCon' a1 c
a
  toCon' (R1 b1 c
a) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall (a :: * -> *) (b :: * -> *) c.
ToCon' a b =>
a c -> Maybe (b c)
toCon' a1 c
a
    b2 c
bc <- forall (a :: * -> *) (b :: * -> *) c.
ToCon' a b =>
a c -> Maybe (b c)
toCon' b1 c
b
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a2 c
ac forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: b2 c
bc

#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(SomeWordN)
CONCRETE_TOCON(SomeIntN)
CONCRETE_TOCON(B.ByteString)
CONCRETE_TOCON_BV(WordN)
CONCRETE_TOCON_BV(IntN)
#endif

-- Unit
instance ToCon () () where
  toCon :: () -> Maybe ()
toCon = forall a. a -> Maybe a
Just

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

-- Maybe
deriving via (Default (Maybe a2)) instance (ToCon a1 a2) => ToCon (Maybe a1) (Maybe a2)

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

-- MaybeT
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) = forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. ToCon a b => a -> Maybe b
toCon m1 (Maybe a)
v

-- ExceptT
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) = forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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) = forall a b. ToCon a b => a -> Maybe b
toCon m1 (Either e1 a)
v

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

-- WriterT
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) = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterLazy.WriterT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterStrict.WriterT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. ToCon a b => a -> Maybe b
toCon m1 (a, s1)
v

-- Identity
instance ToCon a b => ToCon (Identity a) (Identity b) where
  toCon :: Identity a -> Maybe (Identity b)
toCon (Identity a
a) = forall a. a -> Identity a
Identity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Identity a -> a
runIdentity

instance ToCon v (Identity v) where
  toCon :: v -> Maybe (Identity v)
toCon = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Identity a
Identity

-- IdentityT
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) = forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a b. ToCon a b => a -> Maybe b
toCon m a
a