Grisette.Internal.Core.Data.Class.EvalSym

Evaluating symbolic values with model

class EvalSym a where

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)

Methods

evalSym :: Bool -> Model -> a -> a

Evaluate a symbolic value with some model, possibly fill in values for the missing symbols.

Instances

EvalSym All

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> All -> All

EvalSym Any

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Any -> Any

EvalSym Int16

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Int16 -> Int16

EvalSym Int32

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Int32 -> Int32

EvalSym Int64

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Int64 -> Int64

EvalSym Int8

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Int8 -> Int8

EvalSym Word16

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Word16 -> Word16

EvalSym Word32

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Word32 -> Word32

EvalSym Word64

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Word64 -> Word64

EvalSym Word8

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Word8 -> Word8

EvalSym ByteString

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> ByteString -> ByteString

EvalSym Ordering

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Ordering -> Ordering

EvalSym AssertionError

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> AssertionError -> AssertionError

EvalSym VerificationConditions

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> VerificationConditions -> VerificationConditions

EvalSym CEGISCondition

Defined in Grisette.Internal.Core.Data.Class.CEGISSolver

Methods

evalSym :: Bool -> Model -> CEGISCondition -> CEGISCondition

EvalSym FPRoundingMode

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> FPRoundingMode -> FPRoundingMode

EvalSym SymBool

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> SymBool -> SymBool

EvalSym SymFPRoundingMode

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> SymFPRoundingMode -> SymFPRoundingMode

EvalSym SymInteger

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> SymInteger -> SymInteger

EvalSym Text

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Text -> Text

EvalSym Integer

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Integer -> Integer

EvalSym ()

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> () -> ()

EvalSym Bool

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Bool -> Bool

EvalSym Char

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Char -> Char

EvalSym Double

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Double -> Double

EvalSym Float

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Float -> Float

EvalSym Int

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Int -> Int

EvalSym Word

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Word -> Word

EvalSym a => EvalSym (Identity a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Identity a -> Identity a

EvalSym a => EvalSym (First a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> First a -> First a

EvalSym a => EvalSym (Last a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Last a -> Last a

EvalSym a => EvalSym (Down a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Down a -> Down a

EvalSym a => EvalSym (Dual a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Dual a -> Dual a

EvalSym a => EvalSym (Product a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Product a -> Product a

EvalSym a => EvalSym (Sum a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Sum a -> Sum a

EvalSym p => EvalSym (Par1 p)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Par1 p -> Par1 p

(Generic a, GEvalSym Arity0 (Rep a)) => EvalSym (Default a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Default a -> Default a

EvalSym a => EvalSym (Union a)

Defined in Grisette.Internal.Core.Control.Monad.Union

Methods

evalSym :: Bool -> Model -> Union a -> Union a

(KnownNat n, 1 <= n) => EvalSym (IntN n)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> IntN n -> IntN n

(KnownNat n, 1 <= n) => EvalSym (WordN n)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> WordN n -> WordN n

(forall (n :: Nat). (KnownNat n, 1 <= n) => EvalSym (bv n)) => EvalSym (SomeBV bv)

Defined in Grisette.Internal.SymPrim.SomeBV

Methods

evalSym :: Bool -> Model -> SomeBV bv -> SomeBV bv

(KnownNat n, 1 <= n) => EvalSym (SymIntN n)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> SymIntN n -> SymIntN n

(KnownNat n, 1 <= n) => EvalSym (SymWordN n)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> SymWordN n -> SymWordN n

EvalSym a => EvalSym (Maybe a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Maybe a -> Maybe a

EvalSym a => EvalSym [a]

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> [a] -> [a]

(EvalSym a, EvalSym b) => EvalSym (Either a b)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Either a b -> Either a b

EvalSym (U1 p)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> U1 p -> U1 p

EvalSym (V1 p)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> V1 p -> V1 p

(Generic1 f, GEvalSym Arity1 (Rep1 f), EvalSym a) => EvalSym (Default1 f a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Default1 f a -> Default1 f a

(EvalSym a, EvalSym b) => EvalSym (CBMCEither a b)

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

evalSym :: Bool -> Model -> CBMCEither a b -> CBMCEither a b

ValidFP eb fb => EvalSym (FP eb fb)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> FP eb fb -> FP eb fb

ValidFP eb sb => EvalSym (SymFP eb sb)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> SymFP eb sb -> SymFP eb sb

(SupportedPrim (ca --> cb), LinkedRep ca sa, LinkedRep cb sb) => EvalSym (sa -~> sb)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (sa -~> sb) -> sa -~> sb

(SupportedPrim (ca =-> cb), LinkedRep ca sa, LinkedRep cb sb) => EvalSym (sa =~> sb)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (sa =~> sb) -> sa =~> sb

(EvalSym1 m, EvalSym a) => EvalSym (MaybeT m a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> MaybeT m a -> MaybeT m a

(EvalSym a, EvalSym b) => EvalSym (a, b)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b) -> (a, b)

EvalSym a => EvalSym (Const a b)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Const a b -> Const a b

EvalSym (f a) => EvalSym (Ap f a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Ap f a -> Ap f a

EvalSym (f a) => EvalSym (Alt f a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Alt f a -> Alt f a

EvalSym (f p) => EvalSym (Rec1 f p)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Rec1 f p -> Rec1 f p

EvalSym (m (CBMCEither e a)) => EvalSym (CBMCExceptT e m a)

Defined in Grisette.Internal.Core.Control.Monad.CBMCExcept

Methods

evalSym :: Bool -> Model -> CBMCExceptT e m a -> CBMCExceptT e m a

(EvalSym1 m, EvalSym e, EvalSym a) => EvalSym (ExceptT e m a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> ExceptT e m a -> ExceptT e m a

(EvalSym1 m, EvalSym a) => EvalSym (IdentityT m a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> IdentityT m a -> IdentityT m a

(EvalSym1 m, EvalSym s, EvalSym a) => EvalSym (WriterT s m a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> WriterT s m a -> WriterT s m a

(EvalSym1 m, EvalSym s, EvalSym a) => EvalSym (WriterT s m a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> WriterT s m a -> WriterT s m a

(EvalSym a, EvalSym b, EvalSym c) => EvalSym (a, b, c)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b, c) -> (a, b, c)

(EvalSym (l a), EvalSym (r a)) => EvalSym (Product l r a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Product l r a -> Product l r a

(EvalSym (l a), EvalSym (r a)) => EvalSym (Sum l r a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Sum l r a -> Sum l r a

(EvalSym (f p), EvalSym (g p)) => EvalSym ((f :*: g) p)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (f :*: g) p -> (f :*: g) p

(EvalSym (f p), EvalSym (g p)) => EvalSym ((f :+: g) p)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (f :+: g) p -> (f :+: g) p

EvalSym c => EvalSym (K1 i c p)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> K1 i c p -> K1 i c p

(EvalSym a, EvalSym b, EvalSym c, EvalSym d) => EvalSym (a, b, c, d)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b, c, d) -> (a, b, c, d)

EvalSym (f (g a)) => EvalSym (Compose f g a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> Compose f g a -> Compose f g a

EvalSym (f (g p)) => EvalSym ((f :.: g) p)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (f :.: g) p -> (f :.: g) p

EvalSym (f p) => EvalSym (M1 i c f p)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> M1 i c f p -> M1 i c f p

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e) => EvalSym (a, b, c, d, e)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b, c, d, e) -> (a, b, c, d, e)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f) => EvalSym (a, b, c, d, e, f)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b, c, d, e, f) -> (a, b, c, d, e, f)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g) => EvalSym (a, b, c, d, e, f, g)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b, c, d, e, f, g) -> (a, b, c, d, e, f, g)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h) => EvalSym (a, b, c, d, e, f, g, h)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b, c, d, e, f, g, h) -> (a, b, c, d, e, f, g, h)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h, EvalSym i) => EvalSym (a, b, c, d, e, f, g, h, i)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b, c, d, e, f, g, h, i) -> (a, b, c, d, e, f, g, h, i)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h, EvalSym i, EvalSym j) => EvalSym (a, b, c, d, e, f, g, h, i, j)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b, c, d, e, f, g, h, i, j) -> (a, b, c, d, e, f, g, h, i, j)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h, EvalSym i, EvalSym j, EvalSym k) => EvalSym (a, b, c, d, e, f, g, h, i, j, k)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b, c, d, e, f, g, h, i, j, k) -> (a, b, c, d, e, f, g, h, i, j, k)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h, EvalSym i, EvalSym j, EvalSym k, EvalSym l) => EvalSym (a, b, c, d, e, f, g, h, i, j, k, l)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b, c, d, e, f, g, h, i, j, k, l) -> (a, b, c, d, e, f, g, h, i, j, k, l)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h, EvalSym i, EvalSym j, EvalSym k, EvalSym l, EvalSym m) => EvalSym (a, b, c, d, e, f, g, h, i, j, k, l, m)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b, c, d, e, f, g, h, i, j, k, l, m) -> (a, b, c, d, e, f, g, h, i, j, k, l, m)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h, EvalSym i, EvalSym j, EvalSym k, EvalSym l, EvalSym m, EvalSym n) => EvalSym (a, b, c, d, e, f, g, h, i, j, k, l, m, n)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h, EvalSym i, EvalSym j, EvalSym k, EvalSym l, EvalSym m, EvalSym n, EvalSym o) => EvalSym (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o)

evalSymToCon :: (ToCon a b, EvalSym a) => Model -> a -> b

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]

class (forall a. EvalSym a => EvalSym (f a)) => EvalSym1 f where

Lifting of EvalSym to unary type constructors.

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a

Lift the evalSym function to unary type constructors.

Instances

EvalSym1 Identity

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Identity a -> Identity a

EvalSym1 First

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> First a -> First a

EvalSym1 Last

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Last a -> Last a

EvalSym1 Down

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Down a -> Down a

EvalSym1 Dual

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Dual a -> Dual a

EvalSym1 Product

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Product a -> Product a

EvalSym1 Sum

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Sum a -> Sum a

EvalSym1 Union

Defined in Grisette.Internal.Core.Control.Monad.Union

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Union a -> Union a

EvalSym1 Maybe

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Maybe a -> Maybe a

EvalSym1 List

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> [a] -> [a]

EvalSym a => EvalSym1 (Either a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> Either a a0 -> Either a a0

(Generic1 f, GEvalSym Arity1 (Rep1 f)) => EvalSym1 (Default1 f)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Default1 f a -> Default1 f a

EvalSym1 m => EvalSym1 (MaybeT m)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> MaybeT m a -> MaybeT m a

EvalSym a => EvalSym1 ((,) a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, a0) -> (a, a0)

EvalSym a => EvalSym1 (Const a :: Type -> Type)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> Const a a0 -> Const a a0

EvalSym1 f => EvalSym1 (Ap f)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Ap f a -> Ap f a

EvalSym1 f => EvalSym1 (Alt f)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Alt f a -> Alt f a

(EvalSym1 m, EvalSym e) => EvalSym1 (ExceptT e m)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> ExceptT e m a -> ExceptT e m a

EvalSym1 m => EvalSym1 (IdentityT m)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> IdentityT m a -> IdentityT m a

(EvalSym1 m, EvalSym s) => EvalSym1 (WriterT s m)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> WriterT s m a -> WriterT s m a

(EvalSym1 m, EvalSym s) => EvalSym1 (WriterT s m)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> WriterT s m a -> WriterT s m a

(EvalSym a, EvalSym b) => EvalSym1 ((,,) a b)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, b, a0) -> (a, b, a0)

(EvalSym1 l, EvalSym1 r) => EvalSym1 (Product l r)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Product l r a -> Product l r a

(EvalSym1 l, EvalSym1 r) => EvalSym1 (Sum l r)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Sum l r a -> Sum l r a

(EvalSym a, EvalSym b, EvalSym c) => EvalSym1 ((,,,) a b c)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, b, c, a0) -> (a, b, c, a0)

(EvalSym1 f, EvalSym1 g) => EvalSym1 (Compose f g)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a -> a) -> Bool -> Model -> Compose f g a -> Compose f g a

(EvalSym a, EvalSym b, EvalSym c, EvalSym d) => EvalSym1 ((,,,,) a b c d)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, b, c, d, a0) -> (a, b, c, d, a0)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e) => EvalSym1 ((,,,,,) a b c d e)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, b, c, d, e, a0) -> (a, b, c, d, e, a0)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f) => EvalSym1 ((,,,,,,) a b c d e f)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, b, c, d, e, f, a0) -> (a, b, c, d, e, f, a0)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g) => EvalSym1 ((,,,,,,,) a b c d e f g)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, b, c, d, e, f, g, a0) -> (a, b, c, d, e, f, g, a0)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h) => EvalSym1 ((,,,,,,,,) a b c d e f g h)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, b, c, d, e, f, g, h, a0) -> (a, b, c, d, e, f, g, h, a0)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h, EvalSym i) => EvalSym1 ((,,,,,,,,,) a b c d e f g h i)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, b, c, d, e, f, g, h, i, a0) -> (a, b, c, d, e, f, g, h, i, a0)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h, EvalSym i, EvalSym j) => EvalSym1 ((,,,,,,,,,,) a b c d e f g h i j)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, b, c, d, e, f, g, h, i, j, a0) -> (a, b, c, d, e, f, g, h, i, j, a0)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h, EvalSym i, EvalSym j, EvalSym k) => EvalSym1 ((,,,,,,,,,,,) a b c d e f g h i j k)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, b, c, d, e, f, g, h, i, j, k, a0) -> (a, b, c, d, e, f, g, h, i, j, k, a0)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h, EvalSym i, EvalSym j, EvalSym k, EvalSym l) => EvalSym1 ((,,,,,,,,,,,,) a b c d e f g h i j k l)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, b, c, d, e, f, g, h, i, j, k, l, a0) -> (a, b, c, d, e, f, g, h, i, j, k, l, a0)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h, EvalSym i, EvalSym j, EvalSym k, EvalSym l, EvalSym m) => EvalSym1 ((,,,,,,,,,,,,,) a b c d e f g h i j k l m)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, b, c, d, e, f, g, h, i, j, k, l, m, a0) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, a0)

(EvalSym a, EvalSym b, EvalSym c, EvalSym d, EvalSym e, EvalSym f, EvalSym g, EvalSym h, EvalSym i, EvalSym j, EvalSym k, EvalSym l, EvalSym m, EvalSym n) => EvalSym1 ((,,,,,,,,,,,,,,) a b c d e f g h i j k l m n)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym :: (Bool -> Model -> a0 -> a0) -> Bool -> Model -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, a0) -> (a, b, c, d, e, f, g, h, i, j, k, l, m, n, a0)

evalSym1 :: (EvalSym1 f, EvalSym a) => Bool -> Model -> f a -> f a

Lifting the standard evalSym to unary type constructors.

evalSymToCon1 :: (EvalSym1 f, EvalSym a, ToCon1 f g, ToCon a b) => Model -> f a -> g b

Evaluate and convert to concrete values with lifted standard evalSym for unary type constructors. See evalSymToCon.

class (forall a. EvalSym a => EvalSym1 (f a)) => EvalSym2 f where

Lifting of EvalSym1 to binary type constructors.

Methods

liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> f a b -> f a b

Lift the evalSym function to binary type constructors.

Instances

EvalSym2 Either

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> Either a b -> Either a b

EvalSym2 (,)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym2 :: (Bool -> Model -> a -> a) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a, b) -> (a, b)

EvalSym a => EvalSym2 ((,,) a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym2 :: (Bool -> Model -> a0 -> a0) -> (Bool -> Model -> b -> b) -> Bool -> Model -> (a, a0, b) -> (a, a0, b)

(EvalSym a, EvalSym b) => EvalSym2 ((,,,) a b)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

liftEvalSym2 :: (Bool -> Model -> a0 -> a0) -> (Bool -> Model -> b0 -> b0) -> Bool -> Model -> (a, b, a0, b0) -> (a, b, a0, b0)

evalSym2 :: (EvalSym2 f, EvalSym a, EvalSym b) => Bool -> Model -> f a b -> f a b

Lifting the standard evalSym to binary type constructors.

evalSymToCon2 :: (EvalSym2 f, EvalSym a, EvalSym c, ToCon2 f g, ToCon a b, ToCon c d) => Model -> f a c -> g b d

Evaluate and convert to concrete values with lifted standard evalSym for binary type constructors. See evalSymToCon.

Generic EvalSym

data family EvalSymArgs arity a :: Type

The arguments to the generic evalSym function.

Instances

data EvalSymArgs Arity0 _

Defined in Grisette.Internal.Core.Data.Class.EvalSym

data EvalSymArgs Arity0 _ = EvalSymArgs0

newtype EvalSymArgs Arity1 a

Defined in Grisette.Internal.Core.Data.Class.EvalSym

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

class GEvalSym arity f where

The class of types that can be generically evaluated.

Methods

gevalSym :: EvalSymArgs arity a -> Bool -> Model -> f a -> f a

Instances

GEvalSym Arity1 Par1

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

gevalSym :: EvalSymArgs Arity1 a -> Bool -> Model -> Par1 a -> Par1 a

GEvalSym arity (U1 :: Type -> Type)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

gevalSym :: EvalSymArgs arity a -> Bool -> Model -> U1 a -> U1 a

GEvalSym arity (V1 :: Type -> Type)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

gevalSym :: EvalSymArgs arity a -> Bool -> Model -> V1 a -> V1 a

EvalSym1 a => GEvalSym Arity1 (Rec1 a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

gevalSym :: EvalSymArgs Arity1 a0 -> Bool -> Model -> Rec1 a a0 -> Rec1 a a0

(GEvalSym arity a, GEvalSym arity b) => GEvalSym arity (a :*: b)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

gevalSym :: EvalSymArgs arity a0 -> Bool -> Model -> (a :*: b) a0 -> (a :*: b) a0

(GEvalSym arity a, GEvalSym arity b) => GEvalSym arity (a :+: b)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

gevalSym :: EvalSymArgs arity a0 -> Bool -> Model -> (a :+: b) a0 -> (a :+: b) a0

EvalSym a => GEvalSym arity (K1 i a :: Type -> Type)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

gevalSym :: EvalSymArgs arity a0 -> Bool -> Model -> K1 i a a0 -> K1 i a a0

(EvalSym1 f, GEvalSym Arity1 g) => GEvalSym Arity1 (f :.: g)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

gevalSym :: EvalSymArgs Arity1 a -> Bool -> Model -> (f :.: g) a -> (f :.: g) a

GEvalSym arity a => GEvalSym arity (M1 i c a)

Defined in Grisette.Internal.Core.Data.Class.EvalSym

Methods

gevalSym :: EvalSymArgs arity a0 -> Bool -> Model -> M1 i c a a0 -> M1 i c a a0

genericEvalSym :: (Generic a, GEvalSym Arity0 (Rep a)) => Bool -> Model -> a -> a

Generic evalSym function.

genericLiftEvalSym :: (Generic1 f, GEvalSym Arity1 (Rep1 f)) => (Bool -> Model -> a -> a) -> Bool -> Model -> f a -> f a

Generic liftEvalSym function.