{-# 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.Evaluate
-- 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.Evaluate
  ( -- * Evaluating symbolic values with model
    EvaluateSym (..),
    evaluateSymToCon,
  )
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.Maybe
import Data.Word
import GHC.TypeNats
import Generics.Deriving
import Generics.Deriving.Instances ()
import Grisette.Core.Data.BV
import Grisette.Core.Data.Class.ModelOps
import Grisette.Core.Data.Class.ToCon
import Grisette.IR.SymPrim.Data.Prim.Model

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

-- | Evaluating symbolic values with some model.
--
-- >>> let model = insertValue (SimpleSymbol "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

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

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) = forall k i c (p :: k). c -> K1 i c p
K1 forall a b. (a -> b) -> a -> b
$ forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model c
v

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) = 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 :: * -> *) c.
EvaluateSym' a =>
Bool -> Model -> a c -> a c
evaluateSym' Bool
fillDefault Model
model a c
v

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) = forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 forall a b. (a -> b) -> a -> b
$ 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) = forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 forall a b. (a -> b) -> a -> b
$ forall (a :: * -> *) c.
EvaluateSym' a =>
Bool -> Model -> a c -> a c
evaluateSym' Bool
fillDefault Model
model b c
r

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) = forall (a :: * -> *) c.
EvaluateSym' a =>
Bool -> Model -> a c -> a c
evaluateSym' Bool
fillDefault Model
model a c
a forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (a :: * -> *) c.
EvaluateSym' a =>
Bool -> Model -> a c -> a c
evaluateSym' Bool
fillDefault Model
model b c
b

-- | Evaluate a symbolic variable with some model, fill in values for the missing variables,
-- and transform to concrete ones
--
-- >>> let model = insertValue (SimpleSymbol "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 = forall a. HasCallStack => Maybe a -> a
fromJust forall a b. (a -> b) -> a -> b
$ forall a b. ToCon a b => a -> Maybe b
toCon forall a b. (a -> b) -> a -> b
$ 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(SomeIntN)
CONCRETE_EVALUATESYM(SomeWordN)
CONCRETE_EVALUATESYM(B.ByteString)
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) = forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT forall a b. (a -> b) -> a -> b
$ 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) = forall e (m :: * -> *) a. m (Either e a) -> ExceptT e m a
ExceptT forall a b. (a -> b) -> a -> b
$ 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) = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterLazy.WriterT forall a b. (a -> b) -> a -> b
$ 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) = forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterStrict.WriterT forall a b. (a -> b) -> a -> b
$ 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) = forall a. a -> Identity a
Identity forall a b. (a -> b) -> a -> b
$ 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) = forall {k} (f :: k -> *) (a :: k). f a -> IdentityT f a
IdentityT forall a b. (a -> b) -> a -> b
$ forall a. EvaluateSym a => Bool -> Model -> a -> a
evaluateSym Bool
fillDefault Model
model m a
a