{-# 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
(
EvalSym (..),
evalSymToCon,
EvalSym1 (..),
evalSym1,
evalSymToCon1,
EvalSym2 (..),
evalSym2,
evalSymToCon2,
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)
class EvalSym a where
evalSym :: Bool -> Model -> a -> a
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
class (forall a. (EvalSym a) => EvalSym (f a)) => EvalSym1 f where
liftEvalSym :: (Bool -> Model -> a -> a) -> (Bool -> Model -> f a -> f a)
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 #-}
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 #-}
class (forall a. (EvalSym a) => EvalSym1 (f a)) => EvalSym2 f where
liftEvalSym2 ::
(Bool -> Model -> a -> a) ->
(Bool -> Model -> b -> b) ->
(Bool -> Model -> f a b -> f a b)
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 #-}
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 #-}
data family EvalSymArgs arity a :: Type
data instance EvalSymArgs Arity0 _ = EvalSymArgs0
newtype instance EvalSymArgs Arity1 a
= EvalSymArgs1 (Bool -> Model -> a -> a)
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 #-}
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 #-}
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
#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
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
]
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 #-}
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 #-}
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 #-}
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 #-}
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)
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)
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 #-}
deriving via (Default (Const a b)) instance (EvalSym a) => EvalSym (Const a b)
deriving via (Default1 (Const a)) instance (EvalSym a) => EvalSym1 (Const a)
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)
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)
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