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

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

import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
  ( Identity (Identity, runIdentity),
    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.Generics (Generic (Rep, from, to), K1 (K1), M1 (M1), U1, V1, type (:*:) ((:*:)), type (:+:) (L1, R1))
import GHC.TypeNats (KnownNat, type (<=))
import Generics.Deriving (Default (Default))
import Generics.Deriving.Instances ()
import Grisette.Internal.Core.Control.Exception (AssertionError, VerificationConditions)
import Grisette.Internal.Core.Data.Class.Solvable (Solvable (conView), pattern Con)
import Grisette.Internal.SymPrim.BV
  ( IntN (IntN),
    WordN (WordN),
  )
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.SymGeneralFun (type (-~>))
import Grisette.Internal.SymPrim.SymInteger (SymInteger)
import Grisette.Internal.SymPrim.SymTabularFun (type (=~>))
import Grisette.Internal.SymPrim.TabularFun (type (=->))

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

#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(B.ByteString)
CONCRETE_TOCON(T.Text)
CONCRETE_TOCON_BV(WordN)
CONCRETE_TOCON_BV(IntN)
#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

#define TO_CON_SYMID_SIMPLE(symtype) \
instance ToCon symtype symtype where \
  toCon = Just

#define TO_CON_SYMID_BV(symtype) \
instance (KnownNat n, 1 <= n) => ToCon (symtype n) (symtype n) where \
  toCon = Just

#define TO_CON_SYMID_FUN(op) \
instance (SupportedPrim a, SupportedPrim b) => ToCon (a op b) (a op b) where \
  toCon = Just

#if 1
TO_CON_SYMID_SIMPLE(SymBool)
TO_CON_SYMID_SIMPLE(SymInteger)
TO_CON_SYMID_BV(SymIntN)
TO_CON_SYMID_BV(SymWordN)
TO_CON_SYMID_FUN(=~>)
TO_CON_SYMID_FUN(-~>)

#endif

#define TO_CON_FROMSYM_SIMPLE(contype, symtype) \
instance ToCon symtype contype where \
  toCon = conView

#define TO_CON_FROMSYM_BV(contype, symtype) \
instance (KnownNat n, 1 <= n) => ToCon (symtype n) (contype n) where \
  toCon = conView

#define TO_CON_FROMSYM_FUN(conop, symop) \
instance (SupportedPrim (conop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
  ToCon (symop sa sb) (conop ca cb) where \
  toCon = conView

#if 1
TO_CON_FROMSYM_SIMPLE(Bool, SymBool)
TO_CON_FROMSYM_SIMPLE(Integer, SymInteger)
TO_CON_FROMSYM_BV(IntN, SymIntN)
TO_CON_FROMSYM_BV(WordN, SymWordN)
TO_CON_FROMSYM_FUN((=->), (=~>))
TO_CON_FROMSYM_FUN((-->), (-~>))
#endif

#define TOCON_MACHINE_INTEGER(sbvw, bvw, n, int) \
instance ToCon (sbvw n) int where \
  toCon (Con (bvw v :: bvw n)) = Just $ fromIntegral v; \
  toCon _ = Nothing

#if 1
TOCON_MACHINE_INTEGER(SymIntN, IntN, 8, Int8)
TOCON_MACHINE_INTEGER(SymIntN, IntN, 16, Int16)
TOCON_MACHINE_INTEGER(SymIntN, IntN, 32, Int32)
TOCON_MACHINE_INTEGER(SymIntN, IntN, 64, Int64)
TOCON_MACHINE_INTEGER(SymWordN, WordN, 8, Word8)
TOCON_MACHINE_INTEGER(SymWordN, WordN, 16, Word16)
TOCON_MACHINE_INTEGER(SymWordN, WordN, 32, Word32)
TOCON_MACHINE_INTEGER(SymWordN, WordN, 64, Word64)
TOCON_MACHINE_INTEGER(SymIntN, IntN, $intBitwidthQ, Int)
TOCON_MACHINE_INTEGER(SymWordN, WordN, $intBitwidthQ, Word)
#endif

deriving via
  (Default AssertionError)
  instance
    ToCon AssertionError AssertionError

deriving via
  (Default VerificationConditions)
  instance
    ToCon VerificationConditions VerificationConditions

-- Derivation of ToCon for generic types
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 a b. (a -> b) -> Maybe a -> Maybe 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
forall x. Rep b x -> b
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 c. Rep a c -> Maybe (Rep b c)
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 x. a -> Rep a x
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' V1 V1 where
  toCon' :: forall c. V1 c -> Maybe (V1 c)
toCon' = V1 c -> Maybe (V1 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 c. 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 c. 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 c. 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 c. 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 c. 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 a. a -> Maybe a
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