| Copyright | (c) Sirui Lu 2024 |
|---|---|
| License | BSD-3-Clause (see the LICENSE file) |
| Maintainer | siruilu@cs.washington.edu |
| Stability | Experimental |
| Portability | GHC only |
| Safe Haskell | None |
| Language | Haskell2010 |
Grisette.Unified
Description
Synopsis
- data EvalModeTag
- type family IsConMode (mode :: EvalModeTag) = (r :: Bool) | r -> mode where ...
- type family BaseMonad (mode :: EvalModeTag) = (r :: Type -> Type) | r -> mode where ...
- genEvalMode :: String -> [TheoryToUnify] -> DecsQ
- data TheoryToUnify
- class (DecideEvalMode mode, UnifiedBool mode, UnifiedBasicPrim mode (GetBool mode), Monad (BaseMonad mode), TryMerge (BaseMonad mode), UnifiedBranching mode (BaseMonad mode), AllUnifiedData mode) => EvalModeBase (mode :: EvalModeTag)
- type EvalModeInteger = UnifiedInteger
- class (AllUnifiedBV mode, AllUnifiedBVBVConversion mode) => EvalModeBV (mode :: EvalModeTag)
- class (AllUnifiedFP mode, AllUnifiedFPFPConversion mode, AllUnifiedBVFPConversion mode) => EvalModeFP (mode :: EvalModeTag)
- type EvalModeAlgReal = UnifiedAlgReal
- class (EvalModeBase mode, EvalModeInteger mode, EvalModeAlgReal mode, EvalModeBV mode, EvalModeFP mode) => EvalModeAll (mode :: EvalModeTag)
- type MonadEvalModeAll (mode :: EvalModeTag) (m :: Type -> Type) = (EvalModeAll mode, Monad m, TryMerge m, UnifiedBranching mode m)
- class DecideEvalMode (mode :: EvalModeTag) where
- withMode :: forall (mode :: EvalModeTag) r. DecideEvalMode mode => (mode ~ 'C => r) -> (mode ~ 'S => r) -> r
- class (DecideEvalMode c, DecideEvalMode s) => EvalModeConvertible (c :: EvalModeTag) (s :: EvalModeTag) where
- class (DecideEvalMode mode, TryMerge m) => UnifiedBranching (mode :: EvalModeTag) (m :: Type -> Type) where
- withBaseBranching :: (If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
- class Mergeable a => UnifiedSimpleMergeable (mode :: EvalModeTag) a where
- withBaseSimpleMergeable :: (If (IsConMode mode) () (SimpleMergeable a) => r) -> r
- class UnifiedSimpleMergeable1 (mode :: EvalModeTag) (f :: Type -> Type) where
- withBaseSimpleMergeable1 :: (If (IsConMode mode) () (SimpleMergeable1 f) => r) -> r
- class UnifiedSimpleMergeable2 (mode :: EvalModeTag) (f :: Type -> Type -> Type) where
- withBaseSimpleMergeable2 :: (If (IsConMode mode) () (SimpleMergeable2 f) => r) -> r
- mrgIf :: forall (mode :: EvalModeTag) a m. (DecideEvalMode mode, Mergeable a, UnifiedBranching mode m) => GetBool mode -> m a -> m a -> m a
- liftBaseMonad :: forall (mode :: EvalModeTag) a m. (Applicative m, UnifiedBranching mode m, Mergeable a) => BaseMonad mode a -> m a
- mrgIte :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSimpleMergeable mode a) => GetBool mode -> a -> a -> a
- mrgIte1 :: forall (mode :: EvalModeTag) f a. (DecideEvalMode mode, UnifiedSimpleMergeable1 mode f, UnifiedSimpleMergeable mode a) => GetBool mode -> f a -> f a -> f a
- liftMrgIte :: forall (mode :: EvalModeTag) f a. (DecideEvalMode mode, UnifiedSimpleMergeable1 mode f) => (GetBool mode -> a -> a -> a) -> GetBool mode -> f a -> f a -> f a
- mrgIte2 :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSimpleMergeable2 mode f, UnifiedSimpleMergeable mode a, UnifiedSimpleMergeable mode b) => GetBool mode -> f a b -> f a b -> f a b
- liftMrgIte2 :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSimpleMergeable2 mode f) => (GetBool mode -> a -> a -> a) -> (GetBool mode -> b -> b -> b) -> GetBool mode -> f a b -> f a b -> f a b
- simpleMerge :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSimpleMergeable mode a) => BaseMonad mode a -> a
- class UnifiedITEOp (mode :: EvalModeTag) v where
- withBaseITEOp :: (If (IsConMode mode) () (ITEOp v) => r) -> r
- symIte :: forall (mode :: EvalModeTag) v. (DecideEvalMode mode, UnifiedITEOp mode v) => GetBool mode -> v -> v -> v
- symIteMerge :: forall (mode :: EvalModeTag) v. (DecideEvalMode mode, UnifiedITEOp mode v, Mergeable v) => BaseMonad mode v -> v
- class UnifiedSymEq (mode :: EvalModeTag) a where
- withBaseSymEq :: (If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
- class (forall a. UnifiedSymEq mode a => UnifiedSymEq mode (f a)) => UnifiedSymEq1 (mode :: EvalModeTag) (f :: Type -> Type) where
- withBaseSymEq1 :: (If (IsConMode mode) (Eq1 f) (SymEq1 f) => r) -> r
- class (forall a. UnifiedSymEq mode a => UnifiedSymEq1 mode (f a)) => UnifiedSymEq2 (mode :: EvalModeTag) (f :: Type -> Type -> Type) where
- withBaseSymEq2 :: (If (IsConMode mode) (Eq2 f) (SymEq2 f) => r) -> r
- (.==) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymEq mode a) => a -> a -> GetBool mode
- (./=) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymEq mode a) => a -> a -> GetBool mode
- symDistinct :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymEq mode a) => [a] -> GetBool mode
- liftSymEq :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymEq1 mode f) => (a -> b -> GetBool mode) -> f a -> f b -> GetBool mode
- symEq1 :: forall (mode :: EvalModeTag) f a. (DecideEvalMode mode, UnifiedSymEq mode a, UnifiedSymEq1 mode f) => f a -> f a -> GetBool mode
- liftSymEq2 :: forall (mode :: EvalModeTag) f a b c d. (DecideEvalMode mode, UnifiedSymEq2 mode f) => (a -> b -> GetBool mode) -> (c -> d -> GetBool mode) -> f a c -> f b d -> GetBool mode
- symEq2 :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymEq mode a, UnifiedSymEq mode b, UnifiedSymEq2 mode f) => f a b -> f a b -> GetBool mode
- class UnifiedSymOrd (mode :: EvalModeTag) a where
- withBaseSymOrd :: (If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
- class UnifiedSymOrd1 (mode :: EvalModeTag) (f :: Type -> Type) where
- withBaseSymOrd1 :: (If (IsConMode mode) (Ord1 f) (SymOrd1 f) => r) -> r
- class UnifiedSymOrd2 (mode :: EvalModeTag) (f :: Type -> Type -> Type) where
- withBaseSymOrd2 :: (If (IsConMode mode) (Ord2 f) (SymOrd2 f) => r) -> r
- (.<=) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode
- (.<) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode
- (.>=) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode
- (.>) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode
- symCompare :: forall (mode :: EvalModeTag) a (ctx :: Type -> Type). (DecideEvalMode mode, UnifiedSymOrd mode a, Monad ctx) => a -> a -> BaseMonad mode Ordering
- liftSymCompare :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymOrd1 mode f) => (a -> b -> BaseMonad mode Ordering) -> f a -> f b -> BaseMonad mode Ordering
- symCompare1 :: forall (mode :: EvalModeTag) f a. (DecideEvalMode mode, UnifiedSymOrd mode a, UnifiedSymOrd1 mode f) => f a -> f a -> BaseMonad mode Ordering
- liftSymCompare2 :: forall (mode :: EvalModeTag) f a b c d. (DecideEvalMode mode, UnifiedSymOrd2 mode f) => (a -> b -> BaseMonad mode Ordering) -> (c -> d -> BaseMonad mode Ordering) -> f a c -> f b d -> BaseMonad mode Ordering
- symCompare2 :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymOrd mode a, UnifiedSymOrd mode b, UnifiedSymOrd2 mode f) => f a b -> f a b -> BaseMonad mode Ordering
- symMax :: forall (mode :: EvalModeTag) a. (UnifiedSymOrd mode a, UnifiedITEOp mode a, DecideEvalMode mode) => a -> a -> a
- symMin :: forall (mode :: EvalModeTag) a. (UnifiedSymOrd mode a, UnifiedITEOp mode a, DecideEvalMode mode) => a -> a -> a
- mrgMax :: forall (mode :: EvalModeTag) a m. (UnifiedSymOrd mode a, UnifiedBranching mode m, DecideEvalMode mode, Applicative m, Mergeable a) => a -> a -> m a
- mrgMin :: forall (mode :: EvalModeTag) a m. (UnifiedSymOrd mode a, UnifiedBranching mode m, DecideEvalMode mode, Applicative m, Mergeable a) => a -> a -> m a
- class UnifiedFiniteBits (mode :: EvalModeTag) a where
- withBaseFiniteBits :: (If (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) => r) -> r
- symTestBit :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> Int -> GetBool mode
- symSetBitTo :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> Int -> GetBool mode -> a
- symFromBits :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => [GetBool mode] -> a
- symBitBlast :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> [GetBool mode]
- symLsb :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> GetBool mode
- symMsb :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> GetBool mode
- symPopCount :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) => a -> a
- symCountLeadingZeros :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) => a -> a
- symCountTrailingZeros :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) => a -> a
- class UnifiedFromIntegral (mode :: EvalModeTag) a b where
- withBaseFromIntegral :: (If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) => r) -> r
- symFromIntegral :: forall (mode :: EvalModeTag) a b. (DecideEvalMode mode, UnifiedFromIntegral mode a b) => a -> b
- class UnifiedSafeBitCast (mode :: EvalModeTag) e a b (m :: Type -> Type) where
- withBaseSafeBitCast :: (SafeBitCast e a b m => r) -> r
- safeBitCast :: forall (mode :: EvalModeTag) e a b m. (MonadError e m, UnifiedSafeBitCast mode e a b m) => a -> m b
- class UnifiedSafeFromFP (mode :: EvalModeTag) e a fp fprd (m :: Type -> Type) where
- withBaseSafeFromFP :: (SafeFromFP e a fp fprd m => r) -> r
- safeFromFP :: forall (mode :: EvalModeTag) e a fp fprd m. (UnifiedSafeFromFP mode e a fp fprd m, MonadError e m) => fprd -> fp -> m a
- class UnifiedSafeDiv (mode :: EvalModeTag) e a (m :: Type -> Type) where
- withBaseSafeDiv :: (SafeDiv e a m => r) -> r
- safeDiv :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m a
- safeMod :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m a
- safeDivMod :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m (a, a)
- safeQuot :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m a
- safeRem :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m a
- safeQuotRem :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m (a, a)
- class UnifiedSafeLinearArith (mode :: EvalModeTag) e a (m :: Type -> Type) where
- withBaseSafeLinearArith :: (SafeLinearArith e a m => r) -> r
- safeAdd :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeLinearArith mode e a m) => a -> a -> m a
- safeNeg :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeLinearArith mode e a m) => a -> m a
- safeSub :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeLinearArith mode e a m) => a -> a -> m a
- class UnifiedSafeSymRotate (mode :: EvalModeTag) e a (m :: Type -> Type) where
- withBaseSafeSymRotate :: (SafeSymRotate e a m => r) -> r
- safeSymRotateL :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeSymRotate mode e a m) => a -> a -> m a
- safeSymRotateR :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeSymRotate mode e a m) => a -> a -> m a
- class UnifiedSafeSymShift (mode :: EvalModeTag) e a (m :: Type -> Type) where
- withBaseSafeSymShift :: (SafeSymShift e a m => r) -> r
- safeSymShiftL :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeSymShift mode e a m) => a -> a -> m a
- safeSymShiftR :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeSymShift mode e a m) => a -> a -> m a
- safeSymStrictShiftL :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeSymShift mode e a m) => a -> a -> m a
- safeSymStrictShiftR :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeSymShift mode e a m) => a -> a -> m a
- class UnifiedSafeFdiv (mode :: EvalModeTag) e a (m :: Type -> Type) where
- withBaseUnifiedSafeFdiv :: (SafeFdiv e a m => r) -> r
- safeFdiv :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeFdiv mode e a m) => a -> a -> m a
- type UnifiedPrim (mode :: EvalModeTag) a = (Prim a, UnifiedITEOp mode a, UnifiedSymEq mode a, UnifiedSymOrd mode a)
- type UnifiedBasicPrim (mode :: EvalModeTag) a = (UnifiedPrim mode a, UnifiedSimpleMergeable mode a, UnifiedConRep a, UnifiedSymRep a, UnifiedSolvable mode a (ConType a), ConSymConversion (ConType a) (SymType a) a)
- type family GetBool (mode :: EvalModeTag) = (bool :: Type) | bool -> mode
- type family GetIntN (mode :: EvalModeTag) = (i :: Nat -> Type) | i -> mode
- type family GetWordN (mode :: EvalModeTag) = (w :: Nat -> Type) | w -> mode
- type family GetSomeWordN (mode :: EvalModeTag) = (sw :: Type) | sw -> mode where ...
- type family GetSomeIntN (mode :: EvalModeTag) = (sw :: Type) | sw -> mode where ...
- class UnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) => UnifiedBV (mode :: EvalModeTag) (n :: Nat)
- class SafeUnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) m => SafeUnifiedBV (mode :: EvalModeTag) (n :: Nat) (m :: Type -> Type)
- class SafeUnifiedSomeBVImpl mode (SomeBV (GetWordN mode)) (SomeBV (GetIntN mode)) m => SafeUnifiedSomeBV (mode :: EvalModeTag) (m :: Type -> Type)
- type family GetInteger (mode :: EvalModeTag) = (int :: Type) | int -> mode
- class UnifiedIntegerImpl mode (GetInteger mode) => UnifiedInteger (mode :: EvalModeTag)
- type family GetFP (mode :: EvalModeTag) = (f :: Nat -> Nat -> Type) | f -> mode
- type family GetFPRoundingMode (mode :: EvalModeTag) = (r :: Type) | r -> mode
- class UnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) => UnifiedFP (mode :: EvalModeTag) (eb :: Nat) (sb :: Nat)
- class (SafeUnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) m, UnifiedSafeFromFP mode NotRepresentableFPError (GetInteger mode) (GetFP mode eb sb) (GetFPRoundingMode mode) m) => SafeUnifiedFP (mode :: EvalModeTag) (eb :: Nat) (sb :: Nat) (m :: Type -> Type)
- type family GetAlgReal (mode :: EvalModeTag) = (real :: Type) | real -> mode
- class UnifiedAlgRealImpl mode (GetAlgReal mode) => UnifiedAlgReal (mode :: EvalModeTag)
- type family GetData (mode :: EvalModeTag) v = (r :: Type) | r -> mode v
- class UnifiedDataImpl mode v (GetData mode v) => UnifiedData (mode :: EvalModeTag) v
- extractData :: (UnifiedDataImpl mode v u, Mergeable v, Monad m, UnifiedBranching mode m) => u -> m v
- wrapData :: UnifiedDataImpl mode v u => v -> u
- type family GetFun (mode :: EvalModeTag) = (fun :: Type -> Type -> Type) | fun -> mode
- type GetFun2 (mode :: EvalModeTag) a b = GetFun mode a b
- type GetFun3 (mode :: EvalModeTag) a b c = GetFun mode a (GetFun mode b c)
- type GetFun4 (mode :: EvalModeTag) a b c d = GetFun mode a (GetFun mode b (GetFun mode c d))
- type GetFun5 (mode :: EvalModeTag) a b c d e = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d e)))
- type GetFun6 (mode :: EvalModeTag) a b c d e f = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d (GetFun mode e f))))
- type GetFun7 (mode :: EvalModeTag) a b c d e f g = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d (GetFun mode e (GetFun mode f g)))))
- type GetFun8 (mode :: EvalModeTag) a b c d e f g h = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d (GetFun mode e (GetFun mode f (GetFun mode g h))))))
- class UnifiedFun (mode :: EvalModeTag)
- type UnifiedFunConstraint (mode :: EvalModeTag) a b ca cb sa sb = (Show (GetFun mode a b), Binary (GetFun mode a b), Serial (GetFun mode a b), Serialize (GetFun mode a b), NFData (GetFun mode a b), Eq (GetFun mode a b), EvalSym (GetFun mode a b), ExtractSym (GetFun mode a b), Mergeable (GetFun mode a b), PPrint (GetFun mode a b), SubstSym (GetFun mode a b), Hashable (GetFun mode a b), Lift (GetFun mode a b), Typeable (GetFun mode a b), ToCon (GetFun mode a b) (ca =-> cb), ToCon (sa =~> sb) (GetFun mode a b), ToSym (GetFun mode a b) (sa =~> sb), ToSym (ca =-> cb) (GetFun mode a b), Function (GetFun mode a b) a b, Apply (GetFun mode a b), FunType (GetFun mode a b) ~ (a -> b))
- unifiedFunInstanceName :: String -> [TheoryToUnify] -> String
- genUnifiedFunInstance :: String -> [TheoryToUnify] -> DecsQ
- class (UnifiedBVBVConversionImpl mode (GetWordN mode) (GetWordN mode) n0 n1 (GetWordN mode n0) (GetWordN mode n1), UnifiedBVBVConversionImpl mode (GetWordN mode) (GetIntN mode) n0 n1 (GetWordN mode n0) (GetIntN mode n1), UnifiedBVBVConversionImpl mode (GetIntN mode) (GetWordN mode) n0 n1 (GetIntN mode n0) (GetWordN mode n1), UnifiedBVBVConversionImpl mode (GetIntN mode) (GetIntN mode) n0 n1 (GetIntN mode n0) (GetIntN mode n1)) => UnifiedBVBVConversion (mode :: EvalModeTag) (n0 :: Nat) (n1 :: Nat)
- class UnifiedBVFPConversionImpl mode (GetWordN mode) (GetIntN mode) (GetFP mode) n eb sb (GetWordN mode n) (GetIntN mode n) (GetFP mode eb sb) (GetFPRoundingMode mode) => UnifiedBVFPConversion (mode :: EvalModeTag) (n :: Nat) (eb :: Nat) (sb :: Nat)
- class SafeUnifiedBVFPConversionImpl mode (GetWordN mode) (GetIntN mode) (GetFP mode) n eb sb (GetWordN mode n) (GetIntN mode n) (GetFP mode eb sb) (GetFPRoundingMode mode) m => SafeUnifiedBVFPConversion (mode :: EvalModeTag) (n :: Nat) (eb :: Nat) (sb :: Nat) (m :: Type -> Type)
- class UnifiedFPFPConversionImpl mode (GetFP mode) eb0 sb0 eb1 sb1 (GetFP mode eb0 sb0) (GetFP mode eb1 sb1) (GetFPRoundingMode mode) => UnifiedFPFPConversion (mode :: EvalModeTag) (eb0 :: Nat) (sb0 :: Nat) (eb1 :: Nat) (sb1 :: Nat)
Evaluation mode
data EvalModeTag Source #
Instances
| Show EvalModeTag Source # | |
Defined in Grisette.Internal.Unified.EvalModeTag Methods showsPrec :: Int -> EvalModeTag -> ShowS # show :: EvalModeTag -> String # showList :: [EvalModeTag] -> ShowS # | |
| Eq EvalModeTag Source # | |
Defined in Grisette.Internal.Unified.EvalModeTag | |
| Lift EvalModeTag Source # | |
Defined in Grisette.Internal.Unified.EvalModeTag Methods lift :: Quote m => EvalModeTag -> m Exp # liftTyped :: forall (m :: Type -> Type). Quote m => EvalModeTag -> Code m EvalModeTag # | |
type family IsConMode (mode :: EvalModeTag) = (r :: Bool) | r -> mode where ... Source #
Type family to check if a mode is C.
type family BaseMonad (mode :: EvalModeTag) = (r :: Type -> Type) | r -> mode where ... Source #
A type family that specifies the base monad for the evaluation mode.
Aggregated constraints
genEvalMode :: String -> [TheoryToUnify] -> DecsQ Source #
This template haskell function generates an EvalMode constraint on demand.
For example, if in your system, you are only working on bit-vectors and booleans, but not floating points, integers, or real numbers, you can use this function to generate a constraint that only includes the necessary constraints:
genEvalMode "MyEvalMode" [UWordN, UIntN, UBool] f :: MyEvalMode mode => GetBool mode -> GetWordN mode 8 -> GetWordN mode 8 f = ...
This may help with faster compilation times.
Another usage of this custom constraint is to working with uninterpreted
functions. The uninterpreted functions aren't available even with
EvalModeAll, and is only available with the constraint generated by this
function. Note that you need to explicitly list all the uninterpreted
function types you need in your system.
genEvalMode "MyEvalModeUF" [UFun [UWordN, UIntN], UFun [UBool, UBool, UWordN]]
This will give us a constraint that allows us to work with booleans and bit-vectors, and also the uninterpreted functions that
- maps an unsigned bit-vector (any bitwidth) to an unsigned integer (any bitwidth), and
- maps two booleans to an unsigned bit-vector (any bitwidth).
You can then use them in your code like this:
f :: MyEvalModeUF mode => GetFun mode (GetWordN mode 8) (GetIntN mode 8) -> GetIntN mode 8 f fun = f # 1
The function will also provide the constraint MonadMyEvalModeUF, which
includes the constraints for the monad and the unified branching, similar to
MonadEvalModeAll.
For compilers older than GHC 9.2.1, see the notes for EvalModeAll. This
function will also generate constraints like MyEvalModeUFFunUWordNUIntN,
which can be used to resolve the constraints for older compilers.
The naming conversion is the concatenation of the three parts:
- The base name provided by the user (i.e.,
MyEvalModeUF), Fun,- The concatenation of all the types in the uninterpreted function (i.e.,
UWordNUIntN).
The arguments to the type class is as follows:
- The first argument is the mode,
- The second to the end arguments are the natural number arguments for all the types. Here the second argument is the bitwidth of the unsigned bit-vector argument, and the third argument is the bitwidth of the signed bit-vector result.
data TheoryToUnify Source #
This data type is used to represent the theories that is unified.
The UFun constructor is used to represent a specific uninterpreted function
type. The type is uncurried.
Instances
| Show TheoryToUnify Source # | |
Defined in Grisette.Internal.Unified.Theories Methods showsPrec :: Int -> TheoryToUnify -> ShowS # show :: TheoryToUnify -> String # showList :: [TheoryToUnify] -> ShowS # | |
| Eq TheoryToUnify Source # | |
Defined in Grisette.Internal.Unified.Theories Methods (==) :: TheoryToUnify -> TheoryToUnify -> Bool # (/=) :: TheoryToUnify -> TheoryToUnify -> Bool # | |
class (DecideEvalMode mode, UnifiedBool mode, UnifiedBasicPrim mode (GetBool mode), Monad (BaseMonad mode), TryMerge (BaseMonad mode), UnifiedBranching mode (BaseMonad mode), AllUnifiedData mode) => EvalModeBase (mode :: EvalModeTag) Source #
Provide the constraint that the mode is a valid evaluation mode, and
provides the support for GetBool and GetData.
For compilers prior to GHC 9.2.1, see the notes for EvalModeAll.
Instances
type EvalModeInteger = UnifiedInteger Source #
Provide the support for GetInteger.
For compilers prior to GHC 9.2.1, see the notes for EvalModeAll.
class (AllUnifiedBV mode, AllUnifiedBVBVConversion mode) => EvalModeBV (mode :: EvalModeTag) Source #
Provide the support for GetIntN,
GetWordN, GetSomeIntN, and
GetSomeWordN.
For compilers prior to GHC 9.2.1, see the notes for EvalModeAll.
Instances
| EvalModeBV 'C Source # | |
| EvalModeBV 'S Source # | |
class (AllUnifiedFP mode, AllUnifiedFPFPConversion mode, AllUnifiedBVFPConversion mode) => EvalModeFP (mode :: EvalModeTag) Source #
Provide the support for GetFP and
GetFPRoundingMode.
For compilers prior to GHC 9.2.1, see the notes for EvalModeAll.
Instances
| EvalModeFP 'C Source # | |
| EvalModeFP 'S Source # | |
type EvalModeAlgReal = UnifiedAlgReal Source #
Provide the support for GetAlgReal.
For compilers prior to GHC 9.2.1, see the notes for EvalModeAll.
class (EvalModeBase mode, EvalModeInteger mode, EvalModeAlgReal mode, EvalModeBV mode, EvalModeFP mode) => EvalModeAll (mode :: EvalModeTag) Source #
A constraint that specifies that the mode is valid, and provide all the corresponding constraints for the operaions for the types.
Note for users with GHC prior to 9.2.1: the GHC compiler isn't able to
resolve the operations for sized bitvectors and data types. In this case,
you may need to provide UnifiedBV,
SafeUnifiedBV,
SafeUnifiedSomeBV, and
UnifiedData constraints manually.
For example, the following code is valid for GHC 9.2.1 and later:
fbv ::
forall mode n.
(EvalMode mode, KnownNat n, 1 <= n) =>
GetIntN mode n ->
GetIntN mode n ->
GetIntN mode n
fbv l r =
mrgIte @mode
(l .== r)
(l + r)
(symIte @mode (l .< r) l r)But with older GHCs, you need to write:
fbv ::
forall mode n.
(EvalMode mode, KnownNat n, 1 <= n, UnifiedBV mode n) =>
GetIntN mode n ->
GetIntN mode n ->
GetIntN mode n
fbv l r =
mrgIte @mode
(l .== r)
(l + r)
(symIte @mode (l .< r) l r)Instances
type MonadEvalModeAll (mode :: EvalModeTag) (m :: Type -> Type) = (EvalModeAll mode, Monad m, TryMerge m, UnifiedBranching mode m) Source #
A constraint that specifies that the mode is valid, and provide all the corresponding constraints for the operations for the types.
This also provide the branching constraints for the monad, and the safe
operations: for example, SafeUnifiedInteger provides
safeDiv for the integer type with in ExceptT ArithException m.
For users with GHC prior to 9.2.1, see notes in EvalModeAll.
class DecideEvalMode (mode :: EvalModeTag) where Source #
A class that provides the mode tag at runtime.
Methods
Instances
| DecideEvalMode 'C Source # | |
Defined in Grisette.Internal.Unified.Util Methods | |
| DecideEvalMode 'S Source # | |
Defined in Grisette.Internal.Unified.Util Methods | |
withMode :: forall (mode :: EvalModeTag) r. DecideEvalMode mode => (mode ~ 'C => r) -> (mode ~ 'S => r) -> r Source #
Case analysis on the mode.
class (DecideEvalMode c, DecideEvalMode s) => EvalModeConvertible (c :: EvalModeTag) (s :: EvalModeTag) where Source #
A class saying that we can convert a value with one mode to another mode.
Allowed conversions:
Conversion from left to right uses ToSym class, and conversion
from right to left uses ToCon class.
Methods
withModeConvertible :: (c ~ 'C => r) -> (s ~ 'S => r) -> r Source #
withModeConvertible' :: ((c ~ 'C, s ~ 'C) => r) -> ((c ~ 'C, s ~ 'S) => r) -> ((c ~ 'S, s ~ 'S) => r) -> r Source #
Instances
| DecideEvalMode s => EvalModeConvertible 'C s Source # | |
| DecideEvalMode c => EvalModeConvertible c 'S Source # | |
| DecideEvalMode c => EvalModeConvertible c c Source # | |
Unified operations
Unified simple mergeable
class (DecideEvalMode mode, TryMerge m) => UnifiedBranching (mode :: EvalModeTag) (m :: Type -> Type) where Source #
A class that provides a unified branching operation.
We use this type class to help resolve the constraints for
SymBranching.
Methods
withBaseBranching :: (If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r Source #
Instances
class Mergeable a => UnifiedSimpleMergeable (mode :: EvalModeTag) a where Source #
A class that provides a unified simple merging.
We use this type class to help resolve the constraints for SimpleMergeable.
Methods
withBaseSimpleMergeable :: (If (IsConMode mode) () (SimpleMergeable a) => r) -> r Source #
Instances
class UnifiedSimpleMergeable1 (mode :: EvalModeTag) (f :: Type -> Type) where Source #
A class that provides lifting of unified simple merging.
We use this type class to help resolve the constraints for
SimpleMergeable1.
Methods
withBaseSimpleMergeable1 :: (If (IsConMode mode) () (SimpleMergeable1 f) => r) -> r Source #
Instances
class UnifiedSimpleMergeable2 (mode :: EvalModeTag) (f :: Type -> Type -> Type) where Source #
A class that provides lifting of unified simple merging.
We use this type class to help resolve the constraints for
SimpleMergeable2.
Methods
withBaseSimpleMergeable2 :: (If (IsConMode mode) () (SimpleMergeable2 f) => r) -> r Source #
Instances
mrgIf :: forall (mode :: EvalModeTag) a m. (DecideEvalMode mode, Mergeable a, UnifiedBranching mode m) => GetBool mode -> m a -> m a -> m a Source #
Unified mrgIf.
This function isn't able to infer the mode of the boolean variable, so you need to provide the mode explicitly. For example:
mrgIf @mode (a .== b) ... mrgIf (a .== b :: SymBool) ... mrgIf (a .== b :: GetBool mode) ...
liftBaseMonad :: forall (mode :: EvalModeTag) a m. (Applicative m, UnifiedBranching mode m, Mergeable a) => BaseMonad mode a -> m a Source #
Unified lifting of a base monad.
mrgIte :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSimpleMergeable mode a) => GetBool mode -> a -> a -> a Source #
Unified mrgIte.
mrgIte1 :: forall (mode :: EvalModeTag) f a. (DecideEvalMode mode, UnifiedSimpleMergeable1 mode f, UnifiedSimpleMergeable mode a) => GetBool mode -> f a -> f a -> f a Source #
Unified mrgIte1.
liftMrgIte :: forall (mode :: EvalModeTag) f a. (DecideEvalMode mode, UnifiedSimpleMergeable1 mode f) => (GetBool mode -> a -> a -> a) -> GetBool mode -> f a -> f a -> f a Source #
Unified liftMrgIte.
mrgIte2 :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSimpleMergeable2 mode f, UnifiedSimpleMergeable mode a, UnifiedSimpleMergeable mode b) => GetBool mode -> f a b -> f a b -> f a b Source #
Unified mrgIte2.
liftMrgIte2 :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSimpleMergeable2 mode f) => (GetBool mode -> a -> a -> a) -> (GetBool mode -> b -> b -> b) -> GetBool mode -> f a b -> f a b -> f a b Source #
Unified liftMrgIte2.
simpleMerge :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSimpleMergeable mode a) => BaseMonad mode a -> a Source #
Unified merge of simply mergeable values in the base monad.
Unified ITE operator
class UnifiedITEOp (mode :: EvalModeTag) v where Source #
A class that provides unified equality comparison.
We use this type class to help resolve the constraints for ITEOp.
Instances
| (DecideEvalMode mode, If (IsConMode mode) () (ITEOp a)) => UnifiedITEOp mode a Source # | |
| (UnifiedITEOp 'S v, Mergeable v) => UnifiedITEOp 'S (Union v) Source # | |
symIte :: forall (mode :: EvalModeTag) v. (DecideEvalMode mode, UnifiedITEOp mode v) => GetBool mode -> v -> v -> v Source #
Unified symIte operation.
This function isn't able to infer the mode of the boolean variable, so you need to provide the mode explicitly. For example:
symIte @mode (a .== b) ... symIte (a .== b :: SymBool) ... symIte (a .== b :: GetBool mode) ...
symIteMerge :: forall (mode :: EvalModeTag) v. (DecideEvalMode mode, UnifiedITEOp mode v, Mergeable v) => BaseMonad mode v -> v Source #
Unified symIteMerge
operation.
This function isn't able to infer the mode of the base monad from the result, so you need to provide the mode explicitly. For example:
symIteMerge @mode ... symIteMerge (... :: BaseMonad mode v) ...
Unified SymEq
class UnifiedSymEq (mode :: EvalModeTag) a where Source #
A class that provides unified equality comparison.
We use this type class to help resolve the constraints for Eq and SymEq.
Instances
class (forall a. UnifiedSymEq mode a => UnifiedSymEq mode (f a)) => UnifiedSymEq1 (mode :: EvalModeTag) (f :: Type -> Type) where Source #
A class that provides unified lifting of equality comparison.
We use this type class to help resolve the constraints for Eq1 and
SymEq1.
Instances
class (forall a. UnifiedSymEq mode a => UnifiedSymEq1 mode (f a)) => UnifiedSymEq2 (mode :: EvalModeTag) (f :: Type -> Type -> Type) where Source #
A class that provides unified lifting of equality comparison.
We use this type class to help resolve the constraints for Eq2 and
SymEq2.
Instances
| DecideEvalMode mode => UnifiedSymEq2 mode Either Source # | |
| DecideEvalMode mode => UnifiedSymEq2 mode (,) Source # | |
| (DecideEvalMode mode, If (IsConMode mode) (Eq2 f) (SymEq2 f), forall a. UnifiedSymEq mode a => UnifiedSymEq1 mode (f a)) => UnifiedSymEq2 mode f Source # | |
| (DecideEvalMode mode, UnifiedSymEq mode a) => UnifiedSymEq2 mode ((,,) a) Source # | |
| (DecideEvalMode mode, UnifiedSymEq mode a1, UnifiedSymEq mode a2) => UnifiedSymEq2 mode ((,,,) a1 a2) Source # | |
(.==) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymEq mode a) => a -> a -> GetBool mode Source #
(./=) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymEq mode a) => a -> a -> GetBool mode Source #
symDistinct :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymEq mode a) => [a] -> GetBool mode Source #
Unified symDistinct.
Note that you may sometimes need to write type annotations for the result when the mode isn't clear:
symDistinct l :: GetBool mode
One example when it isn't clear is when this is used in unified
mrgIf.
liftSymEq :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymEq1 mode f) => (a -> b -> GetBool mode) -> f a -> f b -> GetBool mode Source #
Unified liftSymEq.
symEq1 :: forall (mode :: EvalModeTag) f a. (DecideEvalMode mode, UnifiedSymEq mode a, UnifiedSymEq1 mode f) => f a -> f a -> GetBool mode Source #
Unified symEq1.
liftSymEq2 :: forall (mode :: EvalModeTag) f a b c d. (DecideEvalMode mode, UnifiedSymEq2 mode f) => (a -> b -> GetBool mode) -> (c -> d -> GetBool mode) -> f a c -> f b d -> GetBool mode Source #
Unified liftSymEq2.
symEq2 :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymEq mode a, UnifiedSymEq mode b, UnifiedSymEq2 mode f) => f a b -> f a b -> GetBool mode Source #
Unified symEq2.
Unified SymOrd
class UnifiedSymOrd (mode :: EvalModeTag) a where Source #
A class that provides unified comparison.
We use this type class to help resolve the constraints for Ord and
SymOrd.
Instances
class UnifiedSymOrd1 (mode :: EvalModeTag) (f :: Type -> Type) where Source #
A class that provides unified lifting of comparison.
We use this type class to help resolve the constraints for Ord1 and
SymOrd1.
Instances
class UnifiedSymOrd2 (mode :: EvalModeTag) (f :: Type -> Type -> Type) where Source #
A class that provides unified lifting of comparison.
We use this type class to help resolve the constraints for Ord2 and
SymOrd2.
Instances
| DecideEvalMode mode => UnifiedSymOrd2 mode Either Source # | |
| DecideEvalMode mode => UnifiedSymOrd2 mode (,) Source # | |
| (DecideEvalMode mode, If (IsConMode mode) (Ord2 f) (SymOrd2 f), forall a. UnifiedSymOrd mode a => UnifiedSymOrd1 mode (f a)) => UnifiedSymOrd2 mode f Source # | |
| (DecideEvalMode mode, UnifiedSymOrd mode a) => UnifiedSymOrd2 mode ((,,) a) Source # | |
| (DecideEvalMode mode, UnifiedSymOrd mode a1, UnifiedSymOrd mode a2) => UnifiedSymOrd2 mode ((,,,) a1 a2) Source # | |
(.<=) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode Source #
(.<) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode Source #
Unified (.<).
(.>=) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode Source #
Unified (.>=).
(.>) :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode Source #
Unified (.>).
symCompare :: forall (mode :: EvalModeTag) a (ctx :: Type -> Type). (DecideEvalMode mode, UnifiedSymOrd mode a, Monad ctx) => a -> a -> BaseMonad mode Ordering Source #
Unified symCompare.
liftSymCompare :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymOrd1 mode f) => (a -> b -> BaseMonad mode Ordering) -> f a -> f b -> BaseMonad mode Ordering Source #
Unified liftSymCompare.
symCompare1 :: forall (mode :: EvalModeTag) f a. (DecideEvalMode mode, UnifiedSymOrd mode a, UnifiedSymOrd1 mode f) => f a -> f a -> BaseMonad mode Ordering Source #
Unified symCompare1.
liftSymCompare2 :: forall (mode :: EvalModeTag) f a b c d. (DecideEvalMode mode, UnifiedSymOrd2 mode f) => (a -> b -> BaseMonad mode Ordering) -> (c -> d -> BaseMonad mode Ordering) -> f a c -> f b d -> BaseMonad mode Ordering Source #
Unified liftSymCompare2.
symCompare2 :: forall (mode :: EvalModeTag) f a b. (DecideEvalMode mode, UnifiedSymOrd mode a, UnifiedSymOrd mode b, UnifiedSymOrd2 mode f) => f a b -> f a b -> BaseMonad mode Ordering Source #
Unified symCompare2.
symMax :: forall (mode :: EvalModeTag) a. (UnifiedSymOrd mode a, UnifiedITEOp mode a, DecideEvalMode mode) => a -> a -> a Source #
Unified symMax.
symMin :: forall (mode :: EvalModeTag) a. (UnifiedSymOrd mode a, UnifiedITEOp mode a, DecideEvalMode mode) => a -> a -> a Source #
Unified symMin.
mrgMax :: forall (mode :: EvalModeTag) a m. (UnifiedSymOrd mode a, UnifiedBranching mode m, DecideEvalMode mode, Applicative m, Mergeable a) => a -> a -> m a Source #
Unified mrgMax.
mrgMin :: forall (mode :: EvalModeTag) a m. (UnifiedSymOrd mode a, UnifiedBranching mode m, DecideEvalMode mode, Applicative m, Mergeable a) => a -> a -> m a Source #
Unified mrgMin.
Unified finite bits
class UnifiedFiniteBits (mode :: EvalModeTag) a where Source #
A class that provides unified equality comparison.
We use this type class to help resolve the constraints for FiniteBits,
FromBits and SymFiniteBits.
Methods
withBaseFiniteBits :: (If (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) => r) -> r Source #
Instances
symTestBit :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> Int -> GetBool mode Source #
Unified symTestBit.
symSetBitTo :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> Int -> GetBool mode -> a Source #
Unified symSetBitTo.
symFromBits :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => [GetBool mode] -> a Source #
Unified symFromBits.
symBitBlast :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> [GetBool mode] Source #
Unified symBitBlast.
symLsb :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> GetBool mode Source #
Unified symLsb.
symMsb :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> GetBool mode Source #
Unified symMsb.
symPopCount :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) => a -> a Source #
Unified symPopCount.
symCountLeadingZeros :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) => a -> a Source #
Unified
symCountLeadingZeros.
symCountTrailingZeros :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) => a -> a Source #
Unified
symCountTrailingZeros.
Unified conversions
class UnifiedFromIntegral (mode :: EvalModeTag) a b where Source #
A class that provides unified conversion from integral types.
We use this type class to help resolve the constraints for SymFromIntegral.
Methods
withBaseFromIntegral :: (If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) => r) -> r Source #
Instances
symFromIntegral :: forall (mode :: EvalModeTag) a b. (DecideEvalMode mode, UnifiedFromIntegral mode a b) => a -> b Source #
Unified symFromIntegral
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
symFromIntegral @mode a
class UnifiedSafeBitCast (mode :: EvalModeTag) e a b (m :: Type -> Type) where Source #
A class that provides unified safe bitcast operations.
We use this type class to help resolve the constraints for SafeBitCast.
Methods
withBaseSafeBitCast :: (SafeBitCast e a b m => r) -> r Source #
Instances
safeBitCast :: forall (mode :: EvalModeTag) e a b m. (MonadError e m, UnifiedSafeBitCast mode e a b m) => a -> m b Source #
Unified safeSub
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeSub @mode a b
class UnifiedSafeFromFP (mode :: EvalModeTag) e a fp fprd (m :: Type -> Type) where Source #
A class that provides unified safe conversion from floating points.
We use this type class to help resolve the constraints for SafeFromFP.
Methods
withBaseSafeFromFP :: (SafeFromFP e a fp fprd m => r) -> r Source #
Instances
safeFromFP :: forall (mode :: EvalModeTag) e a fp fprd m. (UnifiedSafeFromFP mode e a fp fprd m, MonadError e m) => fprd -> fp -> m a Source #
Unified safeFromFP
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeFromFP @mode mode fp
Unified safe ops
class UnifiedSafeDiv (mode :: EvalModeTag) e a (m :: Type -> Type) where Source #
A class that provides unified division operations.
We use this type class to help resolve the constraints for SafeDiv.
Methods
withBaseSafeDiv :: (SafeDiv e a m => r) -> r Source #
Instances
safeDiv :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m a Source #
Unified safeDiv operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeDiv @mode a b
safeMod :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m a Source #
Unified safeMod operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeMod @mode a b
safeDivMod :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m (a, a) Source #
Unified safeDivMod
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeDivMod @mode a b
safeQuot :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m a Source #
Unified safeQuot
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeQuot @mode a b
safeRem :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m a Source #
Unified safeRem operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeRem @mode a b
safeQuotRem :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m (a, a) Source #
Unified safeQuotRem
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeQuotRem @mode a b
class UnifiedSafeLinearArith (mode :: EvalModeTag) e a (m :: Type -> Type) where Source #
A class that provides unified linear arithmetic operations.
We use this type class to help resolve the constraints for SafeLinearArith.
Methods
withBaseSafeLinearArith :: (SafeLinearArith e a m => r) -> r Source #
Instances
safeAdd :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeLinearArith mode e a m) => a -> a -> m a Source #
Unified safeAdd
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeAdd @mode a b
safeNeg :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeLinearArith mode e a m) => a -> m a Source #
Unified safeNeg
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeNeg @mode a
safeSub :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeLinearArith mode e a m) => a -> a -> m a Source #
Unified safeSub
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeSub @mode a b
class UnifiedSafeSymRotate (mode :: EvalModeTag) e a (m :: Type -> Type) where Source #
A class that provides unified safe symbolic rotation operations.
We use this type class to help resolve the constraints for SafeSymRotate.
Methods
withBaseSafeSymRotate :: (SafeSymRotate e a m => r) -> r Source #
Instances
safeSymRotateL :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeSymRotate mode e a m) => a -> a -> m a Source #
Unified safeSymRotateL
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeSymRotateL @mode a b
safeSymRotateR :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeSymRotate mode e a m) => a -> a -> m a Source #
Unified safeSymRotateR
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeSymRotateR @mode a b
class UnifiedSafeSymShift (mode :: EvalModeTag) e a (m :: Type -> Type) where Source #
A class that provides unified safe symbolic rotation operations.
We use this type class to help resolve the constraints for SafeSymShift.
Methods
withBaseSafeSymShift :: (SafeSymShift e a m => r) -> r Source #
Instances
safeSymShiftL :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeSymShift mode e a m) => a -> a -> m a Source #
Unified safeSymShiftL
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeSymShiftL @mode a b
safeSymShiftR :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeSymShift mode e a m) => a -> a -> m a Source #
Unified safeSymShiftR
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeSymShiftR @mode a b
safeSymStrictShiftL :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeSymShift mode e a m) => a -> a -> m a Source #
Unified
safeSymStrictShiftL
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeSymStrictShiftL @mode a b
safeSymStrictShiftR :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeSymShift mode e a m) => a -> a -> m a Source #
Unified
safeSymStrictShiftR
operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeSymStrictShiftR @mode a b
class UnifiedSafeFdiv (mode :: EvalModeTag) e a (m :: Type -> Type) where Source #
A class that provides unified floating division operations.
We use this type class to help resolve the constraints for SafeFdiv.
Methods
withBaseUnifiedSafeFdiv :: (SafeFdiv e a m => r) -> r Source #
Instances
| (MonadError ArithException m, UnifiedBranching 'S m) => UnifiedSafeFdiv 'S ArithException SymAlgReal m Source # | |
Defined in Grisette.Internal.Unified.Class.UnifiedSafeFdiv Methods withBaseUnifiedSafeFdiv :: (SafeFdiv ArithException SymAlgReal m => r) -> r Source # | |
| (MonadError ArithException m, UnifiedBranching mode m) => UnifiedSafeFdiv mode ArithException AlgReal m Source # | |
Defined in Grisette.Internal.Unified.Class.UnifiedSafeFdiv Methods withBaseUnifiedSafeFdiv :: (SafeFdiv ArithException AlgReal m => r) -> r Source # | |
| (UnifiedBranching mode m, SafeFdiv e a m) => UnifiedSafeFdiv mode e a m Source # | |
Defined in Grisette.Internal.Unified.Class.UnifiedSafeFdiv Methods withBaseUnifiedSafeFdiv :: (SafeFdiv e a m => r) -> r Source # | |
safeFdiv :: forall (mode :: EvalModeTag) e a m. (MonadError e m, UnifiedSafeFdiv mode e a m) => a -> a -> m a Source #
Unified safeFdiv operation.
This function isn't able to infer the mode, so you need to provide the mode explicitly. For example:
safeFdiv @mode a b
Shared constraints
type UnifiedPrim (mode :: EvalModeTag) a = (Prim a, UnifiedITEOp mode a, UnifiedSymEq mode a, UnifiedSymOrd mode a) Source #
A type that is used as a constraint for all the (unified) primitive types in Grisette.
type UnifiedBasicPrim (mode :: EvalModeTag) a = (UnifiedPrim mode a, UnifiedSimpleMergeable mode a, UnifiedConRep a, UnifiedSymRep a, UnifiedSolvable mode a (ConType a), ConSymConversion (ConType a) (SymType a) a) Source #
A type that is used as a constraint for all the basic (unified) primitive types in Grisette.
GetSomeWordN is not considered as a basic (unified)
primitive type.
Unified types
Boolean
type family GetBool (mode :: EvalModeTag) = (bool :: Type) | bool -> mode Source #
Bit-vector
type family GetIntN (mode :: EvalModeTag) = (i :: Nat -> Type) | i -> mode Source #
type family GetWordN (mode :: EvalModeTag) = (w :: Nat -> Type) | w -> mode Source #
type family GetSomeWordN (mode :: EvalModeTag) = (sw :: Type) | sw -> mode where ... Source #
Get a unified unsigned dynamic bit width bit vector type. Resolves to
SomeWordN in C mode, and SomeSymWordN in
S mode.
Equations
| GetSomeWordN mode = SomeBV (GetWordN mode) |
type family GetSomeIntN (mode :: EvalModeTag) = (sw :: Type) | sw -> mode where ... Source #
Get a unified signed dynamic bit width bit vector type. Resolves to
SomeIntN in C mode, and SomeSymIntN in
S mode.
Equations
| GetSomeIntN mode = SomeBV (GetIntN mode) |
class UnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) => UnifiedBV (mode :: EvalModeTag) (n :: Nat) Source #
This class is needed as constraint in user code prior to GHC 9.2.1.
See the notes in EvalMode.
class SafeUnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) m => SafeUnifiedBV (mode :: EvalModeTag) (n :: Nat) (m :: Type -> Type) Source #
This class is needed as constraint in user code prior to GHC 9.2.1.
See the notes in EvalMode.
class SafeUnifiedSomeBVImpl mode (SomeBV (GetWordN mode)) (SomeBV (GetIntN mode)) m => SafeUnifiedSomeBV (mode :: EvalModeTag) (m :: Type -> Type) Source #
This class is needed as constraint in user code prior to GHC 9.2.1.
See the notes in EvalMode.
Integer
type family GetInteger (mode :: EvalModeTag) = (int :: Type) | int -> mode Source #
Get a unified Integer type. Resolves to Integer in C mode, and
SymInteger in S mode.
Instances
| type GetInteger 'C Source # | |
Defined in Grisette.Internal.Unified.UnifiedInteger | |
| type GetInteger 'S Source # | |
Defined in Grisette.Internal.Unified.UnifiedInteger | |
class UnifiedIntegerImpl mode (GetInteger mode) => UnifiedInteger (mode :: EvalModeTag) Source #
Evaluation mode with unified Integer type.
Instances
| UnifiedInteger 'C Source # | |
Defined in Grisette.Internal.Unified.UnifiedInteger | |
| UnifiedInteger 'S Source # | |
Defined in Grisette.Internal.Unified.UnifiedInteger | |
FP
type family GetFPRoundingMode (mode :: EvalModeTag) = (r :: Type) | r -> mode Source #
Get a unified floating point rounding mode type. Resolves to
FPRoundingMode in C mode, and
SymFPRoundingMode in S mode.
Instances
| type GetFPRoundingMode 'C Source # | |
| type GetFPRoundingMode 'S Source # | |
class UnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) => UnifiedFP (mode :: EvalModeTag) (eb :: Nat) (sb :: Nat) Source #
Evaluation mode with unified FP type.
Instances
| UnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) => UnifiedFP mode eb sb Source # | |
class (SafeUnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) m, UnifiedSafeFromFP mode NotRepresentableFPError (GetInteger mode) (GetFP mode eb sb) (GetFPRoundingMode mode) m) => SafeUnifiedFP (mode :: EvalModeTag) (eb :: Nat) (sb :: Nat) (m :: Type -> Type) Source #
This class is needed as constraint in user code prior to GHC 9.2.1.
See the notes in EvalMode.
Instances
| (SafeUnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) m, UnifiedSafeFromFP mode NotRepresentableFPError (GetInteger mode) (GetFP mode eb sb) (GetFPRoundingMode mode) m) => SafeUnifiedFP mode eb sb m Source # | |
AlgReal
type family GetAlgReal (mode :: EvalModeTag) = (real :: Type) | real -> mode Source #
Get a unified algebraic real type. Resolves to AlgReal in C mode,
and SymAlgReal in S mode.
Floating, LogBaseOr and SafeLogBase for
SymAlgReal are not provided as they are not available for AlgReal.
Instances
| type GetAlgReal 'C Source # | |
Defined in Grisette.Internal.Unified.UnifiedAlgReal | |
| type GetAlgReal 'S Source # | |
Defined in Grisette.Internal.Unified.UnifiedAlgReal | |
class UnifiedAlgRealImpl mode (GetAlgReal mode) => UnifiedAlgReal (mode :: EvalModeTag) Source #
Evaluation mode with unified AlgReal type.
Instances
| UnifiedAlgReal 'C Source # | |
Defined in Grisette.Internal.Unified.UnifiedAlgReal | |
| UnifiedAlgReal 'S Source # | |
Defined in Grisette.Internal.Unified.UnifiedAlgReal | |
Data
type family GetData (mode :: EvalModeTag) v = (r :: Type) | r -> mode v Source #
class UnifiedDataImpl mode v (GetData mode v) => UnifiedData (mode :: EvalModeTag) v Source #
This class is needed as constraint in user code prior to GHC 9.2.1.
See the notes in IsMode.
Instances
| UnifiedDataImpl bool v (GetData bool v) => UnifiedData bool v Source # | |
Defined in Grisette.Internal.Unified.UnifiedData | |
extractData :: (UnifiedDataImpl mode v u, Mergeable v, Monad m, UnifiedBranching mode m) => u -> m v Source #
Extracts a value from the unified data type.
Functions
type GetFun2 (mode :: EvalModeTag) a b = GetFun mode a b Source #
The unified function type with 2 arguments.
type GetFun3 (mode :: EvalModeTag) a b c = GetFun mode a (GetFun mode b c) Source #
The unified function type with 3 arguments.
type GetFun4 (mode :: EvalModeTag) a b c d = GetFun mode a (GetFun mode b (GetFun mode c d)) Source #
The unified function type with 4 arguments.
type GetFun5 (mode :: EvalModeTag) a b c d e = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d e))) Source #
The unified function type with 5 arguments.
type GetFun6 (mode :: EvalModeTag) a b c d e f = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d (GetFun mode e f)))) Source #
The unified function type with 6 arguments.
type GetFun7 (mode :: EvalModeTag) a b c d e f g = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d (GetFun mode e (GetFun mode f g))))) Source #
The unified function type with 7 arguments.
type GetFun8 (mode :: EvalModeTag) a b c d e f g h = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d (GetFun mode e (GetFun mode f (GetFun mode g h)))))) Source #
The unified function type with 8 arguments.
class UnifiedFun (mode :: EvalModeTag) Source #
Provide unified function types.
Instances
| UnifiedFun 'C Source # | |
Defined in Grisette.Internal.Unified.UnifiedFun | |
| UnifiedFun 'S Source # | |
Defined in Grisette.Internal.Unified.UnifiedFun | |
type UnifiedFunConstraint (mode :: EvalModeTag) a b ca cb sa sb = (Show (GetFun mode a b), Binary (GetFun mode a b), Serial (GetFun mode a b), Serialize (GetFun mode a b), NFData (GetFun mode a b), Eq (GetFun mode a b), EvalSym (GetFun mode a b), ExtractSym (GetFun mode a b), Mergeable (GetFun mode a b), PPrint (GetFun mode a b), SubstSym (GetFun mode a b), Hashable (GetFun mode a b), Lift (GetFun mode a b), Typeable (GetFun mode a b), ToCon (GetFun mode a b) (ca =-> cb), ToCon (sa =~> sb) (GetFun mode a b), ToSym (GetFun mode a b) (sa =~> sb), ToSym (ca =-> cb) (GetFun mode a b), Function (GetFun mode a b) a b, Apply (GetFun mode a b), FunType (GetFun mode a b) ~ (a -> b)) Source #
The constraint for a unified function.
unifiedFunInstanceName :: String -> [TheoryToUnify] -> String Source #
Generate unified function instance names.
genUnifiedFunInstance :: String -> [TheoryToUnify] -> DecsQ Source #
Generate unified function instances.
Supplemental conversions
class (UnifiedBVBVConversionImpl mode (GetWordN mode) (GetWordN mode) n0 n1 (GetWordN mode n0) (GetWordN mode n1), UnifiedBVBVConversionImpl mode (GetWordN mode) (GetIntN mode) n0 n1 (GetWordN mode n0) (GetIntN mode n1), UnifiedBVBVConversionImpl mode (GetIntN mode) (GetWordN mode) n0 n1 (GetIntN mode n0) (GetWordN mode n1), UnifiedBVBVConversionImpl mode (GetIntN mode) (GetIntN mode) n0 n1 (GetIntN mode n0) (GetIntN mode n1)) => UnifiedBVBVConversion (mode :: EvalModeTag) (n0 :: Nat) (n1 :: Nat) Source #
Unified constraints for conversion between bit-vectors.
Instances
| (UnifiedBVBVConversionImpl mode (GetWordN mode) (GetWordN mode) n0 n1 (GetWordN mode n0) (GetWordN mode n1), UnifiedBVBVConversionImpl mode (GetWordN mode) (GetIntN mode) n0 n1 (GetWordN mode n0) (GetIntN mode n1), UnifiedBVBVConversionImpl mode (GetIntN mode) (GetWordN mode) n0 n1 (GetIntN mode n0) (GetWordN mode n1), UnifiedBVBVConversionImpl mode (GetIntN mode) (GetIntN mode) n0 n1 (GetIntN mode n0) (GetIntN mode n1)) => UnifiedBVBVConversion mode n0 n1 Source # | |
Defined in Grisette.Internal.Unified.BVBVConversion | |
class UnifiedBVFPConversionImpl mode (GetWordN mode) (GetIntN mode) (GetFP mode) n eb sb (GetWordN mode n) (GetIntN mode n) (GetFP mode eb sb) (GetFPRoundingMode mode) => UnifiedBVFPConversion (mode :: EvalModeTag) (n :: Nat) (eb :: Nat) (sb :: Nat) Source #
Unified constraints for conversion from bit-vectors to floating point numbers.
Instances
| UnifiedBVFPConversionImpl mode (GetWordN mode) (GetIntN mode) (GetFP mode) n eb sb (GetWordN mode n) (GetIntN mode n) (GetFP mode eb sb) (GetFPRoundingMode mode) => UnifiedBVFPConversion mode n eb sb Source # | |
class SafeUnifiedBVFPConversionImpl mode (GetWordN mode) (GetIntN mode) (GetFP mode) n eb sb (GetWordN mode n) (GetIntN mode n) (GetFP mode eb sb) (GetFPRoundingMode mode) m => SafeUnifiedBVFPConversion (mode :: EvalModeTag) (n :: Nat) (eb :: Nat) (sb :: Nat) (m :: Type -> Type) Source #
Unified constraints for safe conversion from bit-vectors to floating point numbers.
Instances
| SafeUnifiedBVFPConversionImpl mode (GetWordN mode) (GetIntN mode) (GetFP mode) n eb sb (GetWordN mode n) (GetIntN mode n) (GetFP mode eb sb) (GetFPRoundingMode mode) m => SafeUnifiedBVFPConversion mode n eb sb m Source # | |
class UnifiedFPFPConversionImpl mode (GetFP mode) eb0 sb0 eb1 sb1 (GetFP mode eb0 sb0) (GetFP mode eb1 sb1) (GetFPRoundingMode mode) => UnifiedFPFPConversion (mode :: EvalModeTag) (eb0 :: Nat) (sb0 :: Nat) (eb1 :: Nat) (sb1 :: Nat) Source #
Unified constraints for conversion from floating point numbers to floating point numbers.
Instances
| UnifiedFPFPConversionImpl mode (GetFP mode) eb0 sb0 eb1 sb1 (GetFP mode eb0 sb0) (GetFP mode eb1 sb1) (GetFPRoundingMode mode) => UnifiedFPFPConversion mode eb0 sb0 eb1 sb1 Source # | |