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

-- |
-- Module      :   Grisette.Internal.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.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 Control.Monad.Except (ExceptT (ExceptT), runExceptT)
import Control.Monad.Identity
  ( Identity (Identity),
    IdentityT (IdentityT),
  )
import Control.Monad.Trans.Maybe (MaybeT (MaybeT, runMaybeT))
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.Compose (Compose (Compose))
import Data.Functor.Const (Const)
import Data.Functor.Product (Product)
import Data.Functor.Sum (Sum)
import qualified Data.HashSet as HS
import Data.Int (Int16, Int32, Int64, Int8)
import Data.Kind (Type)
import Data.Maybe (fromJust)
import Data.Monoid (Alt, Ap)
import Data.Ord (Down)
import qualified Data.Text as T
import Data.Word (Word16, Word32, Word64, Word8)
import GHC.TypeNats (KnownNat, type (<=))
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 qualified Generics.Deriving.Monoid as Monoid
import Grisette.Internal.Core.Control.Exception
  ( AssertionError,
    VerificationConditions,
  )
import Grisette.Internal.Core.Data.Class.ToCon
  ( ToCon (toCon),
    ToCon1,
    ToCon2,
    toCon1,
    toCon2,
  )
import Grisette.Internal.SymPrim.AlgReal (AlgReal)
import Grisette.Internal.SymPrim.BV (IntN, WordN)
import Grisette.Internal.SymPrim.FP (FP, FPRoundingMode, NotRepresentableFPError, ValidFP)
import Grisette.Internal.SymPrim.GeneralFun (type (-->) (GeneralFun))
import Grisette.Internal.SymPrim.Prim.Model (Model, evalTerm)
import Grisette.Internal.SymPrim.Prim.Term
  ( LinkedRep,
    SupportedPrim,
    SymRep (SymType),
    someTypedSymbol,
  )
import Grisette.Internal.SymPrim.SymAlgReal (SymAlgReal (SymAlgReal))
import Grisette.Internal.SymPrim.SymBV
  ( SymIntN (SymIntN),
    SymWordN (SymWordN),
  )
import Grisette.Internal.SymPrim.SymBool (SymBool (SymBool))
import Grisette.Internal.SymPrim.SymFP
  ( SymFP (SymFP),
    SymFPRoundingMode (SymFPRoundingMode),
  )
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 (=->) (TabularFun))
import Grisette.Internal.TH.DeriveBuiltin (deriveBuiltins)
import Grisette.Internal.TH.DeriveInstanceProvider
  ( Strategy (ViaDefault, ViaDefault1),
  )
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 #-}

#define CONCRETE_EVALUATESYM(type) \
instance EvalSym type where \
  evalSym _ _ = id

#define CONCRETE_EVALUATESYM_BV(type) \
instance (KnownNat n, 1 <= n) => EvalSym (type n) where \
  evalSym _ _ = 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(Float)
CONCRETE_EVALUATESYM(Double)
CONCRETE_EVALUATESYM(B.ByteString)
CONCRETE_EVALUATESYM(T.Text)
CONCRETE_EVALUATESYM(FPRoundingMode)
CONCRETE_EVALUATESYM(Monoid.All)
CONCRETE_EVALUATESYM(Monoid.Any)
CONCRETE_EVALUATESYM(Ordering)
CONCRETE_EVALUATESYM_BV(IntN)
CONCRETE_EVALUATESYM_BV(WordN)
CONCRETE_EVALUATESYM(AlgReal)
#endif

instance (ValidFP eb fb) => EvalSym (FP eb fb) where
  evalSym :: Bool -> Model -> FP eb fb -> FP eb fb
evalSym Bool
_ Model
_ = FP eb fb -> FP eb fb
forall a. a -> a
id

-- Symbolic primitives
#define EVALUATE_SYM_SIMPLE(symtype) \
instance EvalSym symtype where \
  evalSym fillDefault model (symtype t) = \
    symtype $ evalTerm fillDefault model HS.empty t

#define EVALUATE_SYM_BV(symtype) \
instance (KnownNat n, 1 <= n) => EvalSym (symtype n) where \
  evalSym fillDefault model (symtype t) = \
    symtype $ evalTerm fillDefault model HS.empty t

#define EVALUATE_SYM_FUN(cop, op, cons) \
instance (SupportedPrim (cop ca cb), LinkedRep ca sa, LinkedRep cb sb) => \
  EvalSym (op sa sb) where \
  evalSym fillDefault model (cons t) = \
    cons $ evalTerm fillDefault model HS.empty t

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

instance (ValidFP eb sb) => EvalSym (SymFP eb sb) where
  evalSym :: Bool -> Model -> SymFP eb sb -> SymFP eb sb
evalSym Bool
fillDefault Model
model (SymFP Term (FP eb sb)
t) =
    Term (FP eb sb) -> SymFP eb sb
forall (eb :: Nat) (sb :: Nat). Term (FP eb sb) -> SymFP eb sb
SymFP (Term (FP eb sb) -> SymFP eb sb) -> Term (FP eb sb) -> SymFP eb sb
forall a b. (a -> b) -> a -> b
$ Bool
-> Model
-> HashSet SomeTypedConstantSymbol
-> Term (FP eb sb)
-> Term (FP eb sb)
forall a.
SupportedPrim a =>
Bool
-> Model -> HashSet SomeTypedConstantSymbol -> Term a -> Term a
evalTerm Bool
fillDefault Model
model HashSet SomeTypedConstantSymbol
forall a. HashSet a
HS.empty Term (FP eb sb)
t

-- Instances
deriveBuiltins
  (ViaDefault ''EvalSym)
  [''EvalSym]
  [ ''[],
    ''Maybe,
    ''Either,
    ''(),
    ''(,),
    ''(,,),
    ''(,,,),
    ''(,,,,),
    ''(,,,,,),
    ''(,,,,,,),
    ''(,,,,,,,),
    ''(,,,,,,,,),
    ''(,,,,,,,,,),
    ''(,,,,,,,,,,),
    ''(,,,,,,,,,,,),
    ''(,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,,),
    ''AssertionError,
    ''VerificationConditions,
    ''NotRepresentableFPError,
    ''Identity,
    ''Monoid.Dual,
    ''Monoid.Sum,
    ''Monoid.Product,
    ''Monoid.First,
    ''Monoid.Last,
    ''Down
  ]

deriveBuiltins
  (ViaDefault1 ''EvalSym1)
  [''EvalSym, ''EvalSym1]
  [ ''[],
    ''Maybe,
    ''Either,
    ''(,),
    ''(,,),
    ''(,,,),
    ''(,,,,),
    ''(,,,,,),
    ''(,,,,,,),
    ''(,,,,,,,),
    ''(,,,,,,,,),
    ''(,,,,,,,,,),
    ''(,,,,,,,,,,),
    ''(,,,,,,,,,,,),
    ''(,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,),
    ''(,,,,,,,,,,,,,,),
    ''Identity,
    ''Monoid.Dual,
    ''Monoid.Sum,
    ''Monoid.Product,
    ''Monoid.First,
    ''Monoid.Last,
    ''Down
  ]

-- ExceptT
instance
  (EvalSym1 m, EvalSym e, EvalSym a) =>
  EvalSym (ExceptT e m a)
  where
  evalSym :: Bool -> Model -> ExceptT e m a -> ExceptT e m a
evalSym = Bool -> Model -> ExceptT e m a -> ExceptT e m a
forall (f :: * -> *) a.
(EvalSym1 f, EvalSym a) =>
Bool -> Model -> f a -> f a
evalSym1
  {-# INLINE evalSym #-}

instance (EvalSym1 m, EvalSym e) => EvalSym1 (ExceptT e m) where
  liftEvalSym :: forall a.
(Bool -> Model -> a -> a)
-> Bool -> Model -> ExceptT e m a -> ExceptT e m a
liftEvalSym Bool -> Model -> a -> a
f Bool
fillDefault Model
model =
    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)
-> (ExceptT e m a -> m (Either e a))
-> ExceptT e m a
-> ExceptT e m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Model -> Either e a -> Either e a)
-> Bool -> Model -> m (Either e a) -> m (Either e a)
forall a. (Bool -> Model -> a -> a) -> Bool -> Model -> m a -> m a
forall (f :: * -> *) a.
EvalSym1 f =>
(Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
liftEvalSym ((Bool -> Model -> a -> a)
-> Bool -> Model -> Either e a -> Either e a
forall a.
(Bool -> Model -> a -> a)
-> Bool -> Model -> Either e a -> Either e 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 (m (Either e a) -> m (Either e a))
-> (ExceptT e m a -> m (Either e a))
-> ExceptT e m a
-> m (Either e a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExceptT e m a -> m (Either e a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT
  {-# INLINE liftEvalSym #-}

-- MaybeT
instance (EvalSym1 m, EvalSym a) => EvalSym (MaybeT m a) where
  evalSym :: Bool -> Model -> MaybeT m a -> MaybeT m a
evalSym = Bool -> Model -> MaybeT m a -> MaybeT m a
forall (f :: * -> *) a.
(EvalSym1 f, EvalSym a) =>
Bool -> Model -> f a -> f a
evalSym1
  {-# INLINE evalSym #-}

instance (EvalSym1 m) => EvalSym1 (MaybeT m) where
  liftEvalSym :: forall a.
(Bool -> Model -> a -> a)
-> Bool -> Model -> MaybeT m a -> MaybeT m a
liftEvalSym Bool -> Model -> a -> a
f Bool
fillDefault Model
model =
    m (Maybe a) -> MaybeT m a
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (m (Maybe a) -> MaybeT m a)
-> (MaybeT m a -> m (Maybe a)) -> MaybeT m a -> MaybeT m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Model -> Maybe a -> Maybe a)
-> Bool -> Model -> m (Maybe a) -> m (Maybe a)
forall a. (Bool -> Model -> a -> a) -> Bool -> Model -> m a -> m a
forall (f :: * -> *) a.
EvalSym1 f =>
(Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
liftEvalSym ((Bool -> Model -> a -> a) -> Bool -> Model -> Maybe a -> Maybe a
forall a.
(Bool -> Model -> a -> a) -> Bool -> Model -> Maybe a -> Maybe 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 (m (Maybe a) -> m (Maybe a))
-> (MaybeT m a -> m (Maybe a)) -> MaybeT m a -> m (Maybe a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MaybeT m a -> m (Maybe a)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT
  {-# INLINE liftEvalSym #-}

-- WriterT
instance
  (EvalSym1 m, EvalSym s, EvalSym a) =>
  EvalSym (WriterLazy.WriterT s m a)
  where
  evalSym :: Bool -> Model -> WriterT s m a -> WriterT s m a
evalSym = Bool -> Model -> WriterT s m a -> WriterT s m a
forall (f :: * -> *) a.
(EvalSym1 f, EvalSym a) =>
Bool -> Model -> f a -> f a
evalSym1
  {-# INLINE evalSym #-}

instance
  (EvalSym1 m, EvalSym s) =>
  EvalSym1 (WriterLazy.WriterT s m)
  where
  liftEvalSym :: forall a.
(Bool -> Model -> a -> a)
-> Bool -> Model -> WriterT s m a -> WriterT s m a
liftEvalSym Bool -> Model -> a -> a
f Bool
fillDefault Model
model =
    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)
-> (WriterT s m a -> m (a, s)) -> WriterT s m a -> WriterT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Model -> (a, s) -> (a, s))
-> Bool -> Model -> m (a, s) -> m (a, s)
forall a. (Bool -> Model -> a -> a) -> Bool -> Model -> m a -> m a
forall (f :: * -> *) a.
EvalSym1 f =>
(Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
liftEvalSym ((Bool -> Model -> a -> a)
-> (Bool -> Model -> s -> s) -> Bool -> Model -> (a, s) -> (a, s)
forall a b.
(Bool -> Model -> a -> a)
-> (Bool -> Model -> b -> b) -> Bool -> Model -> (a, b) -> (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
f Bool -> Model -> s -> s
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym) Bool
fillDefault Model
model
      (m (a, s) -> m (a, s))
-> (WriterT s m a -> m (a, s)) -> WriterT s m a -> m (a, s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT s m a -> m (a, s)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
WriterLazy.runWriterT
  {-# INLINE liftEvalSym #-}

instance
  (EvalSym1 m, EvalSym s, EvalSym a) =>
  EvalSym (WriterStrict.WriterT s m a)
  where
  evalSym :: Bool -> Model -> WriterT s m a -> WriterT s m a
evalSym = Bool -> Model -> WriterT s m a -> WriterT s m a
forall (f :: * -> *) a.
(EvalSym1 f, EvalSym a) =>
Bool -> Model -> f a -> f a
evalSym1
  {-# INLINE evalSym #-}

instance
  (EvalSym1 m, EvalSym s) =>
  EvalSym1 (WriterStrict.WriterT s m)
  where
  liftEvalSym :: forall a.
(Bool -> Model -> a -> a)
-> Bool -> Model -> WriterT s m a -> WriterT s m a
liftEvalSym Bool -> Model -> a -> a
f Bool
fillDefault Model
model =
    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)
-> (WriterT s m a -> m (a, s)) -> WriterT s m a -> WriterT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Model -> (a, s) -> (a, s))
-> Bool -> Model -> m (a, s) -> m (a, s)
forall a. (Bool -> Model -> a -> a) -> Bool -> Model -> m a -> m a
forall (f :: * -> *) a.
EvalSym1 f =>
(Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a
liftEvalSym ((Bool -> Model -> a -> a)
-> (Bool -> Model -> s -> s) -> Bool -> Model -> (a, s) -> (a, s)
forall a b.
(Bool -> Model -> a -> a)
-> (Bool -> Model -> b -> b) -> Bool -> Model -> (a, b) -> (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
f Bool -> Model -> s -> s
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym) Bool
fillDefault Model
model
      (m (a, s) -> m (a, s))
-> (WriterT s m a -> m (a, s)) -> WriterT s m a -> m (a, s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. WriterT s m a -> m (a, s)
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
WriterStrict.runWriterT
  {-# INLINE liftEvalSym #-}

-- IdentityT
instance (EvalSym1 m, EvalSym a) => EvalSym (IdentityT m a) where
  evalSym :: Bool -> Model -> IdentityT m a -> IdentityT m a
evalSym = Bool -> Model -> IdentityT m a -> IdentityT m a
forall (f :: * -> *) a.
(EvalSym1 f, EvalSym a) =>
Bool -> Model -> f a -> f a
evalSym1
  {-# INLINE evalSym #-}

instance (EvalSym1 m) => EvalSym1 (IdentityT m) where
  liftEvalSym :: forall a.
(Bool -> Model -> a -> a)
-> Bool -> Model -> IdentityT m a -> IdentityT m a
liftEvalSym Bool -> Model -> a -> a
f 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 -> a -> a) -> Bool -> Model -> m a -> m a
forall a. (Bool -> Model -> a -> a) -> Bool -> Model -> m a -> m 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 m a
a
  {-# INLINE liftEvalSym #-}

-- Product
deriving via
  (Default (Product l r a))
  instance
    (EvalSym (l a), EvalSym (r a)) => EvalSym (Product l r a)

deriving via
  (Default1 (Product l r))
  instance
    (EvalSym1 l, EvalSym1 r) => EvalSym1 (Product l r)

-- Sum
deriving via
  (Default (Sum l r a))
  instance
    (EvalSym (l a), EvalSym (r a)) => EvalSym (Sum l r a)

deriving via
  (Default1 (Sum l r))
  instance
    (EvalSym1 l, EvalSym1 r) => EvalSym1 (Sum l r)

-- Compose
deriving via
  (Default (Compose f g a))
  instance
    (EvalSym (f (g a))) => EvalSym (Compose f g a)

instance (EvalSym1 f, EvalSym1 g) => EvalSym1 (Compose f g) where
  liftEvalSym :: forall a.
(Bool -> Model -> a -> a)
-> Bool -> Model -> Compose f g a -> Compose f g a
liftEvalSym Bool -> Model -> a -> a
f Bool
fillDefault Model
m (Compose f (g a)
l) =
    f (g a) -> Compose f g a
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (g a) -> Compose f g a) -> f (g a) -> Compose 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 ((Bool -> Model -> a -> a) -> Bool -> Model -> g a -> g a
forall a. (Bool -> Model -> a -> a) -> Bool -> Model -> g a -> g 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
m f (g a)
l
  {-# INLINE liftEvalSym #-}

-- Const
deriving via (Default (Const a b)) instance (EvalSym a) => EvalSym (Const a b)

deriving via (Default1 (Const a)) instance (EvalSym a) => EvalSym1 (Const a)

-- Alt
deriving via (Default (Alt f a)) instance (EvalSym (f a)) => EvalSym (Alt f a)

deriving via (Default1 (Alt f)) instance (EvalSym1 f) => EvalSym1 (Alt f)

-- Ap
deriving via (Default (Ap f a)) instance (EvalSym (f a)) => EvalSym (Ap f a)

deriving via (Default1 (Ap f)) instance (EvalSym1 f) => EvalSym1 (Ap f)

-- Generic
deriving via (Default (U1 p)) instance EvalSym (U1 p)

deriving via (Default (V1 p)) instance EvalSym (V1 p)

deriving via
  (Default (K1 i c p))
  instance
    (EvalSym c) => EvalSym (K1 i c p)

deriving via
  (Default (M1 i c f p))
  instance
    (EvalSym (f p)) => EvalSym (M1 i c f p)

deriving via
  (Default ((f :+: g) p))
  instance
    (EvalSym (f p), EvalSym (g p)) => EvalSym ((f :+: g) p)

deriving via
  (Default ((f :*: g) p))
  instance
    (EvalSym (f p), EvalSym (g p)) => EvalSym ((f :*: g) p)

deriving via
  (Default (Par1 p))
  instance
    (EvalSym p) => EvalSym (Par1 p)

deriving via
  (Default (Rec1 f p))
  instance
    (EvalSym (f p)) => EvalSym (Rec1 f p)

deriving via
  (Default ((f :.: g) p))
  instance
    (EvalSym (f (g p))) => EvalSym ((f :.: g) p)

instance EvalSym2 Either where
  liftEvalSym2 :: forall a b.
(Bool -> Model -> a -> a)
-> (Bool -> Model -> b -> b)
-> Bool
-> Model
-> Either a b
-> Either a b
liftEvalSym2 Bool -> Model -> a -> a
f Bool -> Model -> b -> b
_ Bool
fillDefault Model
model (Left a
a) = a -> Either a b
forall a b. a -> Either a b
Left (a -> Either a b) -> a -> Either a b
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> a -> a
f Bool
fillDefault Model
model a
a
  liftEvalSym2 Bool -> Model -> a -> a
_ Bool -> Model -> b -> b
g Bool
fillDefault Model
model (Right b
a) =
    b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> b -> Either a b
forall a b. (a -> b) -> a -> b
$ Bool -> Model -> b -> b
g Bool
fillDefault Model
model b
a
  {-# INLINE liftEvalSym2 #-}

instance EvalSym2 (,) where
  liftEvalSym2 :: forall a b.
(Bool -> Model -> a -> a)
-> (Bool -> Model -> b -> b) -> Bool -> Model -> (a, b) -> (a, b)
liftEvalSym2 Bool -> Model -> a -> a
f Bool -> Model -> b -> b
g Bool
fillDefault Model
model (a
a, b
b) =
    (Bool -> Model -> a -> a
f Bool
fillDefault Model
model a
a, Bool -> Model -> b -> b
g Bool
fillDefault Model
model b
b)
  {-# INLINE liftEvalSym2 #-}

instance (EvalSym a) => EvalSym2 ((,,) a) where
  liftEvalSym2 :: forall a b.
(Bool -> Model -> a -> a)
-> (Bool -> Model -> b -> b)
-> Bool
-> Model
-> (a, a, b)
-> (a, a, b)
liftEvalSym2 Bool -> Model -> a -> a
f Bool -> Model -> b -> b
g Bool
fillDefault Model
model (a
a, a
b, b
c) =
    ( Bool -> Model -> a -> a
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym Bool
fillDefault Model
model a
a,
      Bool -> Model -> a -> a
f Bool
fillDefault Model
model a
b,
      Bool -> Model -> b -> b
g Bool
fillDefault Model
model b
c
    )
  {-# INLINE liftEvalSym2 #-}

instance (EvalSym a, EvalSym b) => EvalSym2 ((,,,) a b) where
  liftEvalSym2 :: forall a b.
(Bool -> Model -> a -> a)
-> (Bool -> Model -> b -> b)
-> Bool
-> Model
-> (a, b, a, b)
-> (a, b, a, b)
liftEvalSym2 Bool -> Model -> a -> a
f Bool -> Model -> b -> b
g Bool
fillDefault Model
model (a
a, b
b, a
c, b
d) =
    ( Bool -> Model -> a -> a
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym Bool
fillDefault Model
model a
a,
      Bool -> Model -> b -> b
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym Bool
fillDefault Model
model b
b,
      Bool -> Model -> a -> a
f Bool
fillDefault Model
model a
c,
      Bool -> Model -> b -> b
g Bool
fillDefault Model
model b
d
    )
  {-# INLINE liftEvalSym2 #-}

instance (EvalSym a, EvalSym b) => EvalSym (a =-> b) where
  evalSym :: Bool -> Model -> (a =-> b) -> a =-> b
evalSym Bool
fillDefault Model
model (TabularFun [(a, b)]
s b
t) =
    [(a, b)] -> b -> a =-> b
forall a b. [(a, b)] -> b -> a =-> b
TabularFun
      (Bool -> Model -> [(a, b)] -> [(a, b)]
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym Bool
fillDefault Model
model [(a, b)]
s)
      (Bool -> Model -> b -> b
forall a. EvalSym a => Bool -> Model -> a -> a
evalSym Bool
fillDefault Model
model b
t)

instance (EvalSym (SymType b)) => EvalSym (a --> b) where
  evalSym :: Bool -> Model -> (a --> b) -> a --> b
evalSym Bool
fillDefault Model
model (GeneralFun TypedConstantSymbol a
s Term b
t) =
    TypedConstantSymbol a -> Term b -> a --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedConstantSymbol a -> Term b -> a --> b
GeneralFun TypedConstantSymbol a
s (Term b -> a --> b) -> Term b -> a --> b
forall a b. (a -> b) -> a -> b
$
      Bool
-> Model -> HashSet SomeTypedConstantSymbol -> Term b -> Term b
forall a.
SupportedPrim a =>
Bool
-> Model -> HashSet SomeTypedConstantSymbol -> Term a -> Term a
evalTerm Bool
fillDefault Model
model (SomeTypedConstantSymbol -> HashSet SomeTypedConstantSymbol
forall a. Hashable a => a -> HashSet a
HS.singleton (SomeTypedConstantSymbol -> HashSet SomeTypedConstantSymbol)
-> SomeTypedConstantSymbol -> HashSet SomeTypedConstantSymbol
forall a b. (a -> b) -> a -> b
$ TypedConstantSymbol a -> SomeTypedConstantSymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedConstantSymbol a
s) Term b
t