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

-- |
-- Module      :   Grisette.Internal.Core.Data.Class.EvaluateSym
-- 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.EvaluateSym
  ( -- * Evaluating symbolic values with model
    EvaluateSym (..),
    evaluateSymToCon,
  )
where

import Control.Monad.Except (ExceptT (ExceptT))
import Control.Monad.Identity
  ( Identity (Identity),
    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 Data.Maybe (fromJust)
import qualified Data.Text as T
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeNats (KnownNat, type (<=))
import Generics.Deriving
  ( Default (Default, unDefault),
    Generic (Rep, from, to),
    K1 (K1),
    M1 (M1),
    U1,
    V1,
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
  )
import Generics.Deriving.Instances ()
import Grisette.Internal.Core.Control.Exception (AssertionError, VerificationConditions)
import Grisette.Internal.Core.Data.Class.ToCon (ToCon (toCon))
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.GeneralFun (type (-->))
import Grisette.Internal.SymPrim.Prim.Model (Model, evaluateTerm)
import Grisette.Internal.SymPrim.Prim.Term (LinkedRep, SupportedPrim)
import Grisette.Internal.SymPrim.SymBV
  ( SymIntN (SymIntN),
    SymWordN (SymWordN),
  )
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
import Grisette.Internal.SymPrim.SymGeneralFun (type (-~>) (SymGeneralFun))
import Grisette.Internal.SymPrim.SymInteger (SymInteger (SymInteger))
import Grisette.Internal.SymPrim.SymTabularFun (type (=~>) (SymTabularFun))
import Grisette.Internal.SymPrim.TabularFun (type (=->))

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Data.Proxy
-- >>> :set -XTypeApplications

-- | Evaluating symbolic values with some model.
--
-- >>> let model = insertValue "a" (1 :: Integer) emptyModel :: Model
-- >>> evaluateSym False model ([ssym "a", ssym "b"] :: [SymInteger])
-- [1,b]
--
-- If we set the first argument true, the missing variables will be filled in with
-- some default values:
--
-- >>> evaluateSym True model ([ssym "a", ssym "b"] :: [SymInteger])
-- [1,0]
--
-- __Note 1:__ This type class can be derived for algebraic data types.
-- You may need the @DerivingVia@ and @DerivingStrategies@ extensions.
--
-- > data X = ... deriving Generic deriving EvaluateSym via (Default X)
class EvaluateSym a where
  -- | Evaluate a symbolic variable with some model, possibly fill in values for the missing variables.
  evaluateSym :: Bool -> Model -> a -> a

-- | Evaluate a symbolic variable with some model, fill in values for the missing variables,
-- and transform to concrete ones
--
-- >>> let model = insertValue "a" (1 :: Integer) emptyModel :: Model
-- >>> evaluateSymToCon model ([ssym "a", ssym "b"] :: [SymInteger]) :: [Integer]
-- [1,0]
evaluateSymToCon :: (ToCon a b, EvaluateSym a) => Model -> a -> b
evaluateSymToCon :: forall a b. (ToCon a b, EvaluateSym a) => Model -> a -> b
evaluateSymToCon Model
model a
a = Maybe b -> b
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe b -> b) -> Maybe b -> b
forall a b. (a -> b) -> a -> b
$ a -> Maybe b
forall a b. ToCon a b => a -> Maybe b
toCon (a -> Maybe b) -> a -> Maybe b
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> a -> a
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
True Model
model a
a

-- instances

#define CONCRETE_EVALUATESYM(type) \
instance EvaluateSym type where \
  evaluateSym _ _ = id

#define CONCRETE_EVALUATESYM_BV(type) \
instance (KnownNat n, 1 <= n) => EvaluateSym (type n) where \
  evaluateSym _ _ = id

#if 1
CONCRETE_EVALUATESYM(Bool)
CONCRETE_EVALUATESYM(Integer)
CONCRETE_EVALUATESYM(Char)
CONCRETE_EVALUATESYM(Int)
CONCRETE_EVALUATESYM(Int8)
CONCRETE_EVALUATESYM(Int16)
CONCRETE_EVALUATESYM(Int32)
CONCRETE_EVALUATESYM(Int64)
CONCRETE_EVALUATESYM(Word)
CONCRETE_EVALUATESYM(Word8)
CONCRETE_EVALUATESYM(Word16)
CONCRETE_EVALUATESYM(Word32)
CONCRETE_EVALUATESYM(Word64)
CONCRETE_EVALUATESYM(B.ByteString)
CONCRETE_EVALUATESYM(T.Text)
CONCRETE_EVALUATESYM_BV(IntN)
CONCRETE_EVALUATESYM_BV(WordN)
#endif

-- ()
instance EvaluateSym () where
  evaluateSym :: Bool -> Model -> () -> ()
evaluateSym Bool
_ Model
_ = () -> ()
forall a. a -> a
id

-- Either
deriving via (Default (Either a b)) instance (EvaluateSym a, EvaluateSym b) => EvaluateSym (Either a b)

-- Maybe
deriving via (Default (Maybe a)) instance (EvaluateSym a) => EvaluateSym (Maybe a)

-- List
deriving via (Default [a]) instance (EvaluateSym a) => EvaluateSym [a]

-- (,)
deriving via (Default (a, b)) instance (EvaluateSym a, EvaluateSym b) => EvaluateSym (a, b)

-- (,,)
deriving via (Default (a, b, c)) instance (EvaluateSym a, EvaluateSym b, EvaluateSym c) => EvaluateSym (a, b, c)

-- (,,,)
deriving via
  (Default (a, b, c, d))
  instance
    (EvaluateSym a, EvaluateSym b, EvaluateSym c, EvaluateSym d) => EvaluateSym (a, b, c, d)

-- (,,,,)
deriving via
  (Default (a, b, c, d, e))
  instance
    (EvaluateSym a, EvaluateSym b, EvaluateSym c, EvaluateSym d, EvaluateSym e) =>
    EvaluateSym (a, b, c, d, e)

-- (,,,,,)
deriving via
  (Default (a, b, c, d, e, f))
  instance
    (EvaluateSym a, EvaluateSym b, EvaluateSym c, EvaluateSym d, EvaluateSym e, EvaluateSym f) =>
    EvaluateSym (a, b, c, d, e, f)

-- (,,,,,,)
deriving via
  (Default (a, b, c, d, e, f, g))
  instance
    ( EvaluateSym a,
      EvaluateSym b,
      EvaluateSym c,
      EvaluateSym d,
      EvaluateSym e,
      EvaluateSym f,
      EvaluateSym g
    ) =>
    EvaluateSym (a, b, c, d, e, f, g)

-- (,,,,,,,)
deriving via
  (Default (a, b, c, d, e, f, g, h))
  instance
    ( EvaluateSym a,
      EvaluateSym b,
      EvaluateSym c,
      EvaluateSym d,
      EvaluateSym e,
      EvaluateSym f,
      EvaluateSym g,
      EvaluateSym h
    ) =>
    EvaluateSym ((,,,,,,,) a b c d e f g h)

-- MaybeT
instance (EvaluateSym (m (Maybe a))) => EvaluateSym (MaybeT m a) where
  evaluateSym :: Bool -> Model -> MaybeT m a -> MaybeT m a
evaluateSym Bool
fillDefault Model
model (MaybeT m (Maybe a)
v) = m (Maybe a) -> MaybeT m a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe a) -> MaybeT m a) -> m (Maybe a) -> MaybeT m a
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> m (Maybe a) -> m (Maybe a)
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model m (Maybe a)
v

-- ExceptT
instance (EvaluateSym (m (Either e a))) => EvaluateSym (ExceptT e m a) where
  evaluateSym :: Bool -> Model -> ExceptT e m a -> ExceptT e m a
evaluateSym Bool
fillDefault Model
model (ExceptT m (Either e a)
v) = m (Either e a) -> ExceptT e m a
forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT (m (Either e a) -> ExceptT e m a)
-> m (Either e a) -> ExceptT e m a
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> m (Either e a) -> m (Either e a)
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model m (Either e a)
v

-- Sum
deriving via
  (Default (Sum f g a))
  instance
    (EvaluateSym (f a), EvaluateSym (g a)) => EvaluateSym (Sum f g a)

-- WriterT
instance (EvaluateSym (m (a, s))) => EvaluateSym (WriterLazy.WriterT s m a) where
  evaluateSym :: Bool -> Model -> WriterT s m a -> WriterT s m a
evaluateSym Bool
fillDefault Model
model (WriterLazy.WriterT m (a, s)
v) = m (a, s) -> WriterT s m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterLazy.WriterT (m (a, s) -> WriterT s m a) -> m (a, s) -> WriterT s m a
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> m (a, s) -> m (a, s)
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model m (a, s)
v

instance (EvaluateSym (m (a, s))) => EvaluateSym (WriterStrict.WriterT s m a) where
  evaluateSym :: Bool -> Model -> WriterT s m a -> WriterT s m a
evaluateSym Bool
fillDefault Model
model (WriterStrict.WriterT m (a, s)
v) = m (a, s) -> WriterT s m a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterStrict.WriterT (m (a, s) -> WriterT s m a) -> m (a, s) -> WriterT s m a
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> m (a, s) -> m (a, s)
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model m (a, s)
v

-- Identity
instance (EvaluateSym a) => EvaluateSym (Identity a) where
  evaluateSym :: Bool -> Model -> Identity a -> Identity a
evaluateSym Bool
fillDefault Model
model (Identity a
a) = a -> Identity a
forall a. a -> Identity a
Identity (a -> Identity a) -> a -> Identity a
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> a -> a
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model a
a

-- IdentityT
instance (EvaluateSym (m a)) => EvaluateSym (IdentityT m a) where
  evaluateSym :: Bool -> Model -> IdentityT m a -> IdentityT m a
evaluateSym Bool
fillDefault Model
model (IdentityT m a
a) = m a -> IdentityT m a
forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT (m a -> IdentityT m a) -> m a -> IdentityT m a
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> m a -> m a
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model m a
a

-- Symbolic primitives
#define EVALUATE_SYM_SIMPLE(symtype) \
instance EvaluateSym symtype where \
  evaluateSym fillDefault model (symtype t) = symtype $ evaluateTerm fillDefault model t

#define EVALUATE_SYM_BV(symtype) \
instance (KnownNat n, 1 <= n) => EvaluateSym (symtype n) where \
  evaluateSym fillDefault model (symtype t) = symtype $ evaluateTerm fillDefault model t

#define EVALUATE_SYM_FUN(cop, op, cons) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
  EvaluateSym (op sa sb) where \
  evaluateSym fillDefault model (cons t) = \
    cons $ evaluateTerm fillDefault model t

#if 1
EVALUATE_SYM_SIMPLE(SymBool)
EVALUATE_SYM_SIMPLE(SymInteger)
EVALUATE_SYM_BV(SymIntN)
EVALUATE_SYM_BV(SymWordN)
EVALUATE_SYM_FUN((=->), (=~>), SymTabularFun)
EVALUATE_SYM_FUN((-->), (-~>), SymGeneralFun)
#endif

-- Exception
deriving via (Default AssertionError) instance EvaluateSym AssertionError

deriving via (Default VerificationConditions) instance EvaluateSym VerificationConditions

instance (Generic a, EvaluateSym' (Rep a)) => EvaluateSym (Default a) where
  evaluateSym :: Bool -> Model -> Default a -> Default a
evaluateSym Bool
fillDefault Model
model =
    a -> Default a
forall a. a -> Default a
Default (a -> Default a) -> (Default a -> a) -> Default a -> Default a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> (Default a -> Rep a Any) -> Default a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> Model -> Rep a Any -> Rep a Any
forall c. Bool -> Model -> Rep a c -> Rep a c
forall (a :: * -> *) c.
EvaluateSym' a =>
Bool -> Model -> a c -> a c
evaluateSym' Bool
fillDefault Model
model (Rep a Any -> Rep a Any)
-> (Default a -> Rep a Any) -> Default a -> Rep a 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 (a -> Rep a Any) -> (Default a -> a) -> Default a -> Rep a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Default a -> a
forall a. Default a -> a
unDefault

class EvaluateSym' a where
  evaluateSym' :: Bool -> Model -> a c -> a c

instance EvaluateSym' U1 where
  evaluateSym' :: forall c. Bool -> Model -> U1 c -> U1 c
evaluateSym' Bool
_ Model
_ = U1 c -> U1 c
forall a. a -> a
id
  {-# INLINE evaluateSym' #-}

instance EvaluateSym' V1 where
  evaluateSym' :: forall c. Bool -> Model -> V1 c -> V1 c
evaluateSym' Bool
_ Model
_ = V1 c -> V1 c
forall a. a -> a
id
  {-# INLINE evaluateSym' #-}

instance (EvaluateSym c) => EvaluateSym' (K1 i c) where
  evaluateSym' :: forall c. Bool -> Model -> K1 i c c -> K1 i c c
evaluateSym' Bool
fillDefault Model
model (K1 c
v) = c -> K1 i c c
forall k i c (p :: k). c -> K1 i c p
K1 (c -> K1 i c c) -> c -> K1 i c c
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> c -> c
forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model c
v
  {-# INLINE evaluateSym' #-}

instance (EvaluateSym' a) => EvaluateSym' (M1 i c a) where
  evaluateSym' :: forall c. Bool -> Model -> M1 i c a c -> M1 i c a c
evaluateSym' Bool
fillDefault Model
model (M1 a c
v) = a c -> M1 i c a c
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a c -> M1 i c a c) -> a c -> M1 i c a c
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> a c -> a c
forall c. Bool -> Model -> a c -> a c
forall (a :: * -> *) c.
EvaluateSym' a =>
Bool -> Model -> a c -> a c
evaluateSym' Bool
fillDefault Model
model a c
v
  {-# INLINE evaluateSym' #-}

instance (EvaluateSym' a, EvaluateSym' b) => EvaluateSym' (a :+: b) where
  evaluateSym' :: forall c. Bool -> Model -> (:+:) a b c -> (:+:) a b c
evaluateSym' Bool
fillDefault Model
model (L1 a c
l) = a c -> (:+:) a b c
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (a c -> (:+:) a b c) -> a c -> (:+:) a b c
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> a c -> a c
forall c. Bool -> Model -> a c -> a c
forall (a :: * -> *) c.
EvaluateSym' a =>
Bool -> Model -> a c -> a c
evaluateSym' Bool
fillDefault Model
model a c
l
  evaluateSym' Bool
fillDefault Model
model (R1 b c
r) = b c -> (:+:) a b c
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (b c -> (:+:) a b c) -> b c -> (:+:) a b c
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> b c -> b c
forall c. Bool -> Model -> b c -> b c
forall (a :: * -> *) c.
EvaluateSym' a =>
Bool -> Model -> a c -> a c
evaluateSym' Bool
fillDefault Model
model b c
r
  {-# INLINE evaluateSym' #-}

instance (EvaluateSym' a, EvaluateSym' b) => EvaluateSym' (a :*: b) where
  evaluateSym' :: forall c. Bool -> Model -> (:*:) a b c -> (:*:) a b c
evaluateSym' Bool
fillDefault Model
model (a c
a :*: b c
b) =
    Bool -> Model -> a c -> a c
forall c. Bool -> Model -> a c -> a c
forall (a :: * -> *) c.
EvaluateSym' a =>
Bool -> Model -> a c -> a c
evaluateSym' Bool
fillDefault Model
model a c
a a c -> b c -> (:*:) a b c
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Bool -> Model -> b c -> b c
forall c. Bool -> Model -> b c -> b c
forall (a :: * -> *) c.
EvaluateSym' a =>
Bool -> Model -> a c -> a c
evaluateSym' Bool
fillDefault Model
model b c
b
  {-# INLINE evaluateSym' #-}