{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE Trustworthy #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- |
-- Module      :   Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Internal.Decl.Core.Data.Class.EvalSym
  ( -- * Evaluating symbolic values with model
    EvalSym (..),
    evalSymToCon,
    EvalSym1 (..),
    evalSym1,
    evalSymToCon1,
    EvalSym2 (..),
    evalSym2,
    evalSymToCon2,

    -- * Generic 'EvalSym'
    EvalSymArgs (..),
    GEvalSym (..),
    genericEvalSym,
    genericLiftEvalSym,
  )
where

import Data.Kind (Type)
import Data.Maybe (fromJust)
import Generics.Deriving
  ( Default (Default, unDefault),
    Default1 (Default1, unDefault1),
    Generic (Rep, from, to),
    Generic1 (Rep1, from1, to1),
    K1 (K1),
    M1 (M1),
    Par1 (Par1),
    Rec1 (Rec1),
    U1,
    V1,
    (:.:) (Comp1),
    type (:*:) ((:*:)),
    type (:+:) (L1, R1),
  )
import Generics.Deriving.Instances ()
import Grisette.Internal.Internal.Decl.Core.Data.Class.ToCon
  ( ToCon (toCon),
    ToCon1,
    ToCon2,
    toCon1,
    toCon2,
  )
import Grisette.Internal.SymPrim.Prim.Model (Model)
import Grisette.Internal.Utils.Derive (Arity0, Arity1)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim
-- >>> import Data.Proxy

-- | Evaluating symbolic values with some model. This would substitute the
-- symbols (symbolic constants) with the values in the model.
--
-- >>> let model = insertValue "a" (1 :: Integer) emptyModel :: Model
-- >>> evalSym False model ([ssym "a", ssym "b"] :: [SymInteger])
-- [1,b]
--
-- If we set the first argument true, the missing symbols will be filled in
-- with some default values:
--
-- >>> evalSym 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 EvalSym via (Default X)
class EvalSym a where
  -- | Evaluate a symbolic value with some model, possibly fill in values for
  -- the missing symbols.
  evalSym :: Bool -> Model -> a -> a

-- | Evaluate a symbolic value with some model, fill in values for the missing
-- symbols, and convert the result to a concrete value.
--
-- >>> let model = insertValue "a" (1 :: Integer) emptyModel :: Model
-- >>> evalSymToCon model ([ssym "a", ssym "b"] :: [SymInteger]) :: [Integer]
-- [1,0]
evalSymToCon :: (ToCon a b, EvalSym a) => Model -> a -> b
evalSymToCon :: forall a b. (ToCon a b, EvalSym a) => Model -> a -> b
evalSymToCon 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. EvalSym a => Bool -> Model -> a -> a
evalSym Bool
True Model
model a
a

-- | Lifting of 'EvalSym' to unary type constructors.
class (forall a. (EvalSym a) => EvalSym (f a)) => EvalSym1 f where
  -- | Lift the 'evalSym' function to unary type constructors.
  liftEvalSym :: (Bool -> Model -> a -> a) -> (Bool -> Model -> f a -> f a)

-- | Lifting the standard 'evalSym' to unary type constructors.
evalSym1 :: (EvalSym1 f, EvalSym a) => Bool -> Model -> f a -> f a
evalSym1 :: forall (f :: * -> *) a.
(EvalSym1 f, EvalSym a) =>
Bool -> Model -> f a -> f a
evalSym1 = (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
forall a. (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
forall (f :: * -> *) a.
EvalSym1 f =>
(Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
liftEvalSym Bool -> Model -> a -> a
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym
{-# INLINE evalSym1 #-}

-- | Evaluate and convert to concrete values with lifted standard 'evalSym' for
-- unary type constructors. See 'evalSymToCon'.
evalSymToCon1 ::
  (EvalSym1 f, EvalSym a, ToCon1 f g, ToCon a b) =>
  Model ->
  f a ->
  g b
evalSymToCon1 :: forall (f :: * -> *) a (g :: * -> *) b.
(EvalSym1 f, EvalSym a, ToCon1 f g, ToCon a b) =>
Model -> f a -> g b
evalSymToCon1 Model
model f a
a = Maybe (g b) -> g b
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (g b) -> g b) -> Maybe (g b) -> g b
forall a b. (a -> b) -> a -> b
$ f a -> Maybe (g b)
forall (f1 :: * -> *) (f2 :: * -> *) a b.
(ToCon1 f1 f2, ToCon a b) =>
f1 a -> Maybe (f2 b)
toCon1 (f a -> Maybe (g b)) -> f a -> Maybe (g b)
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> f a -> f a
forall (f :: * -> *) a.
(EvalSym1 f, EvalSym a) =>
Bool -> Model -> f a -> f a
evalSym1 Bool
True Model
model f a
a
{-# INLINE evalSymToCon1 #-}

-- | Lifting of 'EvalSym1' to binary type constructors.
class (forall a. (EvalSym a) => EvalSym1 (f a)) => EvalSym2 f where
  -- | Lift the 'evalSym' function to binary type constructors.
  liftEvalSym2 ::
    (Bool -> Model -> a -> a) ->
    (Bool -> Model -> b -> b) ->
    (Bool -> Model -> f a b -> f a b)

-- | Lifting the standard 'evalSym' to binary type constructors.
evalSym2 ::
  (EvalSym2 f, EvalSym a, EvalSym b) =>
  Bool ->
  Model ->
  f a b ->
  f a b
evalSym2 :: forall (f :: * -> * -> *) a b.
(EvalSym2 f, EvalSym a, EvalSym b) =>
Bool -> Model -> f a b -> f a b
evalSym2 = (Bool -> Model -> a -> a)
-> (Bool -> Model -> b -> b) -> Bool -> Model -> f a b -> f a b
forall a b.
(Bool -> Model -> a -> a)
-> (Bool -> Model -> b -> b) -> Bool -> Model -> f a b -> f a b
forall (f :: * -> * -> *) a b.
EvalSym2 f =>
(Bool -> Model -> a -> a)
-> (Bool -> Model -> b -> b) -> Bool -> Model -> f a b -> f a b
liftEvalSym2 Bool -> Model -> a -> a
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym Bool -> Model -> b -> b
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym
{-# INLINE evalSym2 #-}

-- | Evaluate and convert to concrete values with lifted standard 'evalSym' for
-- binary type constructors. See 'evalSymToCon'.
evalSymToCon2 ::
  ( EvalSym2 f,
    EvalSym a,
    EvalSym c,
    ToCon2 f g,
    ToCon a b,
    ToCon c d
  ) =>
  Model ->
  f a c ->
  g b d
evalSymToCon2 :: forall (f :: * -> * -> *) a c (g :: * -> * -> *) b d.
(EvalSym2 f, EvalSym a, EvalSym c, ToCon2 f g, ToCon a b,
 ToCon c d) =>
Model -> f a c -> g b d
evalSymToCon2 Model
model f a c
a = Maybe (g b d) -> g b d
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (g b d) -> g b d) -> Maybe (g b d) -> g b d
forall a b. (a -> b) -> a -> b
$ f a c -> Maybe (g b d)
forall (f1 :: * -> * -> *) (f2 :: * -> * -> *) a b c d.
(ToCon2 f1 f2, ToCon a b, ToCon c d) =>
f1 a c -> Maybe (f2 b d)
toCon2 (f a c -> Maybe (g b d)) -> f a c -> Maybe (g b d)
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> f a c -> f a c
forall (f :: * -> * -> *) a b.
(EvalSym2 f, EvalSym a, EvalSym b) =>
Bool -> Model -> f a b -> f a b
evalSym2 Bool
True Model
model f a c
a
{-# INLINE evalSymToCon2 #-}

-- Derivations

-- | The arguments to the generic 'evalSym' function.
data family EvalSymArgs arity a :: Type

data instance EvalSymArgs Arity0 _ = EvalSymArgs0

newtype instance EvalSymArgs Arity1 a
  = EvalSymArgs1 (Bool -> Model -> a -> a)

-- | The class of types that can be generically evaluated.
class GEvalSym arity f where
  gevalSym :: EvalSymArgs arity a -> Bool -> Model -> f a -> f a

instance GEvalSym arity V1 where
  gevalSym :: forall a. EvalSymArgs arity a -> Bool -> Model -> V1 a -> V1 a
gevalSym EvalSymArgs arity a
_ Bool
_ Model
_ = V1 a -> V1 a
forall a. a -> a
id
  {-# INLINE gevalSym #-}

instance GEvalSym arity U1 where
  gevalSym :: forall a. EvalSymArgs arity a -> Bool -> Model -> U1 a -> U1 a
gevalSym EvalSymArgs arity a
_ Bool
_ Model
_ = U1 a -> U1 a
forall a. a -> a
id
  {-# INLINE gevalSym #-}

instance
  (GEvalSym arity a, GEvalSym arity b) =>
  GEvalSym arity (a :*: b)
  where
  gevalSym :: forall a.
EvalSymArgs arity a -> Bool -> Model -> (:*:) a b a -> (:*:) a b a
gevalSym EvalSymArgs arity a
args Bool
fillDefault Model
model (a a
a :*: b a
b) =
    EvalSymArgs arity a -> Bool -> Model -> a a -> a a
forall a. EvalSymArgs arity a -> Bool -> Model -> a a -> a a
forall arity (f :: * -> *) a.
GEvalSym arity f =>
EvalSymArgs arity a -> Bool -> Model -> f a -> f a
gevalSym EvalSymArgs arity a
args Bool
fillDefault Model
model a a
a
      a a -> b a -> (:*:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: EvalSymArgs arity a -> Bool -> Model -> b a -> b a
forall a. EvalSymArgs arity a -> Bool -> Model -> b a -> b a
forall arity (f :: * -> *) a.
GEvalSym arity f =>
EvalSymArgs arity a -> Bool -> Model -> f a -> f a
gevalSym EvalSymArgs arity a
args Bool
fillDefault Model
model b a
b
  {-# INLINE gevalSym #-}

instance
  (GEvalSym arity a, GEvalSym arity b) =>
  GEvalSym arity (a :+: b)
  where
  gevalSym :: forall a.
EvalSymArgs arity a -> Bool -> Model -> (:+:) a b a -> (:+:) a b a
gevalSym EvalSymArgs arity a
args Bool
fillDefault Model
model (L1 a a
l) =
    a a -> (:+:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k). f p -> (:+:) f g p
L1 (a a -> (:+:) a b a) -> a a -> (:+:) a b a
forall a b. (a -> b) -> a -> b
$ EvalSymArgs arity a -> Bool -> Model -> a a -> a a
forall a. EvalSymArgs arity a -> Bool -> Model -> a a -> a a
forall arity (f :: * -> *) a.
GEvalSym arity f =>
EvalSymArgs arity a -> Bool -> Model -> f a -> f a
gevalSym EvalSymArgs arity a
args Bool
fillDefault Model
model a a
l
  gevalSym EvalSymArgs arity a
args Bool
fillDefault Model
model (R1 b a
r) =
    b a -> (:+:) a b a
forall k (f :: k -> *) (g :: k -> *) (p :: k). g p -> (:+:) f g p
R1 (b a -> (:+:) a b a) -> b a -> (:+:) a b a
forall a b. (a -> b) -> a -> b
$ EvalSymArgs arity a -> Bool -> Model -> b a -> b a
forall a. EvalSymArgs arity a -> Bool -> Model -> b a -> b a
forall arity (f :: * -> *) a.
GEvalSym arity f =>
EvalSymArgs arity a -> Bool -> Model -> f a -> f a
gevalSym EvalSymArgs arity a
args Bool
fillDefault Model
model b a
r
  {-# INLINE gevalSym #-}

instance (GEvalSym arity a) => GEvalSym arity (M1 i c a) where
  gevalSym :: forall a.
EvalSymArgs arity a -> Bool -> Model -> M1 i c a a -> M1 i c a a
gevalSym EvalSymArgs arity a
args Bool
fillDefault Model
model (M1 a a
x) =
    a a -> M1 i c a a
forall k i (c :: Meta) (f :: k -> *) (p :: k). f p -> M1 i c f p
M1 (a a -> M1 i c a a) -> a a -> M1 i c a a
forall a b. (a -> b) -> a -> b
$ EvalSymArgs arity a -> Bool -> Model -> a a -> a a
forall a. EvalSymArgs arity a -> Bool -> Model -> a a -> a a
forall arity (f :: * -> *) a.
GEvalSym arity f =>
EvalSymArgs arity a -> Bool -> Model -> f a -> f a
gevalSym EvalSymArgs arity a
args Bool
fillDefault Model
model a a
x
  {-# INLINE gevalSym #-}

instance (EvalSym a) => GEvalSym arity (K1 i a) where
  gevalSym :: forall a.
EvalSymArgs arity a -> Bool -> Model -> K1 i a a -> K1 i a a
gevalSym EvalSymArgs arity a
_ Bool
fillDefault Model
model (K1 a
x) = a -> K1 i a a
forall k i c (p :: k). c -> K1 i c p
K1 (a -> K1 i a a) -> a -> K1 i a a
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> a -> a
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym Bool
fillDefault Model
model a
x
  {-# INLINE gevalSym #-}

instance GEvalSym Arity1 Par1 where
  gevalSym :: forall a. EvalSymArgs Arity1 a -> Bool -> Model -> Par1 a -> Par1 a
gevalSym (EvalSymArgs1 Bool -> Model -> a -> a
f) Bool
fillDefault Model
model (Par1 a
x) =
    a -> Par1 a
forall p. p -> Par1 p
Par1 (a -> Par1 a) -> a -> Par1 a
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> a -> a
f Bool
fillDefault Model
model a
x
  {-# INLINE gevalSym #-}

instance (EvalSym1 a) => GEvalSym Arity1 (Rec1 a) where
  gevalSym :: forall a.
EvalSymArgs Arity1 a -> Bool -> Model -> Rec1 a a -> Rec1 a a
gevalSym (EvalSymArgs1 Bool -> Model -> a -> a
f) Bool
fillDefault Model
model (Rec1 a a
x) =
    a a -> Rec1 a a
forall k (f :: k -> *) (p :: k). f p -> Rec1 f p
Rec1 (a a -> Rec1 a a) -> a a -> Rec1 a a
forall a b. (a -> b) -> a -> b
$ (Bool -> Model -> a -> a) -> Bool -> Model -> a a -> a a
forall a. (Bool -> Model -> a -> a) -> Bool -> Model -> a a -> a a
forall (f :: * -> *) a.
EvalSym1 f =>
(Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
liftEvalSym Bool -> Model -> a -> a
f Bool
fillDefault Model
model a a
x
  {-# INLINE gevalSym #-}

instance
  (EvalSym1 f, GEvalSym Arity1 g) =>
  GEvalSym Arity1 (f :.: g)
  where
  gevalSym :: forall a.
EvalSymArgs Arity1 a -> Bool -> Model -> (:.:) f g a -> (:.:) f g a
gevalSym EvalSymArgs Arity1 a
targs Bool
fillDefault Model
model (Comp1 f (g a)
x) =
    f (g a) -> (:.:) f g a
forall k2 k1 (f :: k2 -> *) (g :: k1 -> k2) (p :: k1).
f (g p) -> (:.:) f g p
Comp1 (f (g a) -> (:.:) f g a) -> f (g a) -> (:.:) f g a
forall a b. (a -> b) -> a -> b
$ (Bool -> Model -> g a -> g a)
-> Bool -> Model -> f (g a) -> f (g a)
forall a. (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
forall (f :: * -> *) a.
EvalSym1 f =>
(Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
liftEvalSym (EvalSymArgs Arity1 a -> Bool -> Model -> g a -> g a
forall a. EvalSymArgs Arity1 a -> Bool -> Model -> g a -> g a
forall arity (f :: * -> *) a.
GEvalSym arity f =>
EvalSymArgs arity a -> Bool -> Model -> f a -> f a
gevalSym EvalSymArgs Arity1 a
targs) Bool
fillDefault Model
model f (g a)
x
  {-# INLINE gevalSym #-}

-- | Generic 'evalSym' function.
genericEvalSym ::
  (Generic a, GEvalSym Arity0 (Rep a)) => Bool -> Model -> a -> a
genericEvalSym :: forall a.
(Generic a, GEvalSym Arity0 (Rep a)) =>
Bool -> Model -> a -> a
genericEvalSym Bool
fillDefault Model
model =
  Rep a Any -> a
forall a x. Generic a => Rep a x -> a
forall x. Rep a x -> a
to (Rep a Any -> a) -> (a -> Rep a Any) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvalSymArgs Arity0 Any -> Bool -> Model -> Rep a Any -> Rep a Any
forall a.
EvalSymArgs Arity0 a -> Bool -> Model -> Rep a a -> Rep a a
forall arity (f :: * -> *) a.
GEvalSym arity f =>
EvalSymArgs arity a -> Bool -> Model -> f a -> f a
gevalSym EvalSymArgs Arity0 Any
forall _. EvalSymArgs Arity0 _
EvalSymArgs0 Bool
fillDefault Model
model (Rep a Any -> Rep a Any) -> (a -> Rep a Any) -> 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
{-# INLINE genericEvalSym #-}

-- | Generic 'liftEvalSym' function.
genericLiftEvalSym ::
  (Generic1 f, GEvalSym Arity1 (Rep1 f)) =>
  (Bool -> Model -> a -> a) ->
  Bool ->
  Model ->
  f a ->
  f a
genericLiftEvalSym :: forall (f :: * -> *) a.
(Generic1 f, GEvalSym Arity1 (Rep1 f)) =>
(Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
genericLiftEvalSym Bool -> Model -> a -> a
f Bool
fillDefault Model
model =
  Rep1 f a -> f a
forall a. Rep1 f a -> f a
forall k (f :: k -> *) (a :: k). Generic1 f => Rep1 f a -> f a
to1 (Rep1 f a -> f a) -> (f a -> Rep1 f a) -> f a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EvalSymArgs Arity1 a -> Bool -> Model -> Rep1 f a -> Rep1 f a
forall a.
EvalSymArgs Arity1 a -> Bool -> Model -> Rep1 f a -> Rep1 f a
forall arity (f :: * -> *) a.
GEvalSym arity f =>
EvalSymArgs arity a -> Bool -> Model -> f a -> f a
gevalSym ((Bool -> Model -> a -> a) -> EvalSymArgs Arity1 a
forall a. (Bool -> Model -> a -> a) -> EvalSymArgs Arity1 a
EvalSymArgs1 Bool -> Model -> a -> a
f) Bool
fillDefault Model
model (Rep1 f a -> Rep1 f a) -> (f a -> Rep1 f a) -> f a -> Rep1 f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Rep1 f a
forall a. f a -> Rep1 f a
forall k (f :: k -> *) (a :: k). Generic1 f => f a -> Rep1 f a
from1
{-# INLINE genericLiftEvalSym #-}

instance
  (Generic a, GEvalSym Arity0 (Rep a)) =>
  EvalSym (Default a)
  where
  evalSym :: Bool -> Model -> Default a -> Default a
evalSym 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
. Bool -> Model -> a -> a
forall a.
(Generic a, GEvalSym Arity0 (Rep a)) =>
Bool -> Model -> a -> a
genericEvalSym Bool
fillDefault Model
model (a -> a) -> (Default a -> a) -> Default a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Default a -> a
forall a. Default a -> a
unDefault
  {-# INLINE evalSym #-}

instance
  (Generic1 f, GEvalSym Arity1 (Rep1 f), EvalSym a) =>
  EvalSym (Default1 f a)
  where
  evalSym :: Bool -> Model -> Default1 f a -> Default1 f a
evalSym = Bool -> Model -> Default1 f a -> Default1 f a
forall (f :: * -> *) a.
(EvalSym1 f, EvalSym a) =>
Bool -> Model -> f a -> f a
evalSym1
  {-# INLINE evalSym #-}

instance
  (Generic1 f, GEvalSym Arity1 (Rep1 f)) =>
  EvalSym1 (Default1 f)
  where
  liftEvalSym :: forall a.
(Bool -> Model -> a -> a)
-> Bool -> Model -> Default1 f a -> Default1 f a
liftEvalSym Bool -> Model -> a -> a
f Bool
fillDefault Model
model =
    f a -> Default1 f a
forall (f :: * -> *) a. f a -> Default1 f a
Default1 (f a -> Default1 f a)
-> (Default1 f a -> f a) -> Default1 f a -> Default1 f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
forall (f :: * -> *) a.
(Generic1 f, GEvalSym Arity1 (Rep1 f)) =>
(Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
genericLiftEvalSym Bool -> Model -> a -> a
f Bool
fillDefault Model
model (f a -> f a) -> (Default1 f a -> f a) -> Default1 f a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Default1 f a -> f a
forall (f :: * -> *) a. Default1 f a -> f a
unDefault1
  {-# INLINE liftEvalSym #-}