{-# LANGUAGE CPP #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# 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 Generics.Deriving
import Generics.Deriving.Instances ()

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

#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(B.ByteString)
#endif

-- Unit
instance ToCon () () where
  toCon :: () -> Maybe ()
toCon = () -> Maybe ()
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) = m2 (Maybe b) -> MaybeT m2 b
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m2 (Maybe b) -> MaybeT m2 b)
-> Maybe (m2 (Maybe b)) -> Maybe (MaybeT m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m1 (Maybe a) -> Maybe (m2 (Maybe 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) = 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)
-> Maybe (m2 (Either e2 b)) -> Maybe (ExceptT e2 m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m1 (Either e1 a) -> Maybe (m2 (Either e2 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) = m1 (Either e1 a) -> Maybe (Either e2 b)
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) = m2 (b, s2) -> WriterT s2 m2 b
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterLazy.WriterT (m2 (b, s2) -> WriterT s2 m2 b)
-> Maybe (m2 (b, s2)) -> Maybe (WriterT s2 m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m1 (a, s1) -> Maybe (m2 (b, s2))
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) = m2 (b, s2) -> WriterT s2 m2 b
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterStrict.WriterT (m2 (b, s2) -> WriterT s2 m2 b)
-> Maybe (m2 (b, s2)) -> Maybe (WriterT s2 m2 b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m1 (a, s1) -> Maybe (m2 (b, s2))
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) = b -> Identity b
forall a. a -> Identity a
Identity (b -> Identity b) -> Maybe b -> Maybe (Identity b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Maybe 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 = v -> Maybe v
forall a. a -> Maybe a
Just (v -> Maybe v) -> (Identity v -> v) -> Identity v -> Maybe v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Identity v -> v
forall a. Identity a -> a
runIdentity

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