| 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 | Safe-Inferred |
| 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 (Typeable mode, UnifiedBool mode, UnifiedPrimitive mode (GetBool mode), Monad (BaseMonad mode), TryMerge (BaseMonad mode), UnifiedBranching mode (BaseMonad mode), AllUnifiedData mode) => EvalModeBase mode
- type EvalModeInteger = UnifiedInteger
- class (AllUnifiedBV mode, AllUnifiedBVBVConversion mode) => EvalModeBV mode
- class (AllUnifiedFP mode, AllUnifiedFPFPConversion mode, AllUnifiedBVFPConversion mode) => EvalModeFP mode
- type EvalModeAlgReal = UnifiedAlgReal
- class (EvalModeBase mode, EvalModeInteger mode, EvalModeAlgReal mode, EvalModeBV mode, EvalModeFP mode) => EvalModeAll mode
- type MonadEvalModeAll mode m = (EvalModeAll mode, Monad m, TryMerge m, UnifiedBranching mode m)
- class Typeable mode => UnifiedBranching (mode :: EvalModeTag) m where
- withBaseBranching :: (If (IsConMode mode) (TryMerge m) (SymBranching m) => r) -> r
- class UnifiedSimpleMergeable mode a where
- withBaseSimpleMergeable :: (If (IsConMode mode) (() :: Constraint) (SimpleMergeable a) => r) -> r
- class UnifiedSimpleMergeable1 mode f where
- withBaseSimpleMergeable1 :: (If (IsConMode mode) (() :: Constraint) (SimpleMergeable1 f) => r) -> r
- class UnifiedSimpleMergeable2 mode f where
- withBaseSimpleMergeable2 :: (If (IsConMode mode) (() :: Constraint) (SimpleMergeable2 f) => r) -> r
- mrgIf :: forall mode a m. (Typeable mode, Mergeable a, UnifiedBranching mode m) => GetBool mode -> m a -> m a -> m a
- liftBaseMonad :: forall mode a m. (Applicative m, UnifiedBranching mode m, Mergeable a) => BaseMonad mode a -> m a
- mrgIte :: forall mode a. (Typeable mode, UnifiedSimpleMergeable mode a) => GetBool mode -> a -> a -> a
- mrgIte1 :: forall mode f a. (Typeable mode, UnifiedSimpleMergeable1 mode f, UnifiedSimpleMergeable mode a) => GetBool mode -> f a -> f a -> f a
- liftMrgIte :: forall mode f a. (Typeable mode, UnifiedSimpleMergeable1 mode f) => (GetBool mode -> a -> a -> a) -> GetBool mode -> f a -> f a -> f a
- mrgIte2 :: forall mode f a b. (Typeable mode, UnifiedSimpleMergeable2 mode f, UnifiedSimpleMergeable mode a, UnifiedSimpleMergeable mode b) => GetBool mode -> f a b -> f a b -> f a b
- liftMrgIte2 :: forall mode f a b. (Typeable 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 a. (Typeable mode, UnifiedSimpleMergeable mode a) => BaseMonad mode a -> a
- class UnifiedITEOp mode v where
- withBaseITEOp :: (If (IsConMode mode) (() :: Constraint) (ITEOp v) => r) -> r
- symIte :: forall mode v. (Typeable mode, UnifiedITEOp mode v) => GetBool mode -> v -> v -> v
- symIteMerge :: forall mode v. (Typeable mode, UnifiedITEOp mode v, Mergeable v) => BaseMonad mode v -> v
- class UnifiedSymEq mode a where
- withBaseSymEq :: (If (IsConMode mode) (Eq a) (SymEq a) => r) -> r
- (.==) :: forall mode a. (Typeable mode, UnifiedSymEq mode a) => a -> a -> GetBool mode
- (./=) :: forall mode a. (Typeable mode, UnifiedSymEq mode a) => a -> a -> GetBool mode
- symDistinct :: forall mode a. (Typeable mode, UnifiedSymEq mode a) => [a] -> GetBool mode
- liftSymEq :: forall mode f a b. (Typeable mode, UnifiedSymEq1 mode f) => (a -> b -> GetBool mode) -> f a -> f b -> GetBool mode
- symEq1 :: forall mode f a. (Typeable mode, UnifiedSymEq mode a, UnifiedSymEq1 mode f) => f a -> f a -> GetBool mode
- liftSymEq2 :: forall mode f a b c d. (Typeable mode, UnifiedSymEq2 mode f) => (a -> b -> GetBool mode) -> (c -> d -> GetBool mode) -> f a c -> f b d -> GetBool mode
- symEq2 :: forall mode f a b. (Typeable mode, UnifiedSymEq mode a, UnifiedSymEq mode b, UnifiedSymEq2 mode f) => f a b -> f a b -> GetBool mode
- class UnifiedSymOrd mode a where
- withBaseSymOrd :: (If (IsConMode mode) (Ord a) (SymOrd a) => r) -> r
- (.<=) :: forall mode a. (Typeable mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode
- (.<) :: forall mode a. (Typeable mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode
- (.>=) :: forall mode a. (Typeable mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode
- (.>) :: forall mode a. (Typeable mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode
- symCompare :: forall mode a ctx. (Typeable mode, UnifiedSymOrd mode a, Monad ctx) => a -> a -> BaseMonad mode Ordering
- liftSymCompare :: forall mode f a b. (Typeable mode, UnifiedSymOrd1 mode f) => (a -> b -> BaseMonad mode Ordering) -> f a -> f b -> BaseMonad mode Ordering
- symCompare1 :: forall mode f a. (Typeable mode, UnifiedSymOrd mode a, UnifiedSymOrd1 mode f) => f a -> f a -> BaseMonad mode Ordering
- liftSymCompare2 :: forall mode f a b c d. (Typeable 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 f a b. (Typeable mode, UnifiedSymOrd mode a, UnifiedSymOrd mode b, UnifiedSymOrd2 mode f) => f a b -> f a b -> BaseMonad mode Ordering
- symMax :: forall mode a. (UnifiedSymOrd mode a, UnifiedITEOp mode a, Typeable mode) => a -> a -> a
- symMin :: forall mode a. (UnifiedSymOrd mode a, UnifiedITEOp mode a, Typeable mode) => a -> a -> a
- mrgMax :: forall mode a m. (UnifiedSymOrd mode a, UnifiedBranching mode m, Typeable mode, Applicative m, Mergeable a) => a -> a -> m a
- mrgMin :: forall mode a m. (UnifiedSymOrd mode a, UnifiedBranching mode m, Typeable mode, Applicative m, Mergeable a) => a -> a -> m a
- class UnifiedFiniteBits mode a where
- withBaseFiniteBits :: (If (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) => r) -> r
- symTestBit :: forall mode a. (Typeable mode, UnifiedFiniteBits mode a) => a -> Int -> GetBool mode
- symSetBitTo :: forall mode a. (Typeable mode, UnifiedFiniteBits mode a) => a -> Int -> GetBool mode -> a
- symFromBits :: forall mode a. (Typeable mode, UnifiedFiniteBits mode a) => [GetBool mode] -> a
- symBitBlast :: forall mode a. (Typeable mode, UnifiedFiniteBits mode a) => a -> [GetBool mode]
- symLsb :: forall mode a. (Typeable mode, UnifiedFiniteBits mode a) => a -> GetBool mode
- symMsb :: forall mode a. (Typeable mode, UnifiedFiniteBits mode a) => a -> GetBool mode
- symPopCount :: forall mode a b. (Typeable mode, UnifiedFiniteBits mode a, Num b, UnifiedITEOp mode b) => a -> b
- symCountLeadingZeros :: forall mode a b. (Typeable mode, UnifiedFiniteBits mode a, Num b, UnifiedITEOp mode b) => a -> b
- symCountTrailingZeros :: forall mode a b. (Typeable mode, UnifiedFiniteBits mode a, Num b, UnifiedITEOp mode b) => a -> b
- class UnifiedFromIntegral (mode :: EvalModeTag) a b where
- withBaseFromIntegral :: (If (IsConMode mode) (Integral a, Num b) (SymFromIntegral a b) => r) -> r
- symFromIntegral :: forall mode a b. (Typeable mode, UnifiedFromIntegral mode a b) => a -> b
- class UnifiedSafeBitCast (mode :: EvalModeTag) e a b m where
- withBaseSafeBitCast :: (SafeBitCast e a b m => r) -> r
- safeBitCast :: forall mode 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 where
- withBaseSafeFromFP :: (SafeFromFP e a fp fprd m => r) -> r
- safeFromFP :: forall mode 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 where
- withBaseSafeDiv :: (SafeDiv e a m => r) -> r
- safeDiv :: forall mode e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m a
- safeMod :: forall mode e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m a
- safeDivMod :: forall mode e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m (a, a)
- safeQuot :: forall mode e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m a
- safeRem :: forall mode e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m a
- safeQuotRem :: forall mode e a m. (MonadError e m, UnifiedSafeDiv mode e a m) => a -> a -> m (a, a)
- class UnifiedSafeLinearArith (mode :: EvalModeTag) e a m where
- withBaseSafeLinearArith :: (SafeLinearArith e a m => r) -> r
- safeAdd :: forall mode e a m. (MonadError e m, UnifiedSafeLinearArith mode e a m) => a -> a -> m a
- safeNeg :: forall mode e a m. (MonadError e m, UnifiedSafeLinearArith mode e a m) => a -> m a
- safeSub :: forall mode e a m. (MonadError e m, UnifiedSafeLinearArith mode e a m) => a -> a -> m a
- class UnifiedSafeSymRotate (mode :: EvalModeTag) e a m where
- withBaseSafeSymRotate :: (SafeSymRotate e a m => r) -> r
- safeSymRotateL :: forall mode e a m. (MonadError e m, UnifiedSafeSymRotate mode e a m) => a -> a -> m a
- safeSymRotateR :: forall mode e a m. (MonadError e m, UnifiedSafeSymRotate mode e a m) => a -> a -> m a
- class UnifiedSafeSymShift (mode :: EvalModeTag) e a m where
- withBaseSafeSymShift :: (SafeSymShift e a m => r) -> r
- safeSymShiftL :: forall mode e a m. (MonadError e m, UnifiedSafeSymShift mode e a m) => a -> a -> m a
- safeSymShiftR :: forall mode e a m. (MonadError e m, UnifiedSafeSymShift mode e a m) => a -> a -> m a
- safeSymStrictShiftL :: forall mode e a m. (MonadError e m, UnifiedSafeSymShift mode e a m) => a -> a -> m a
- safeSymStrictShiftR :: forall mode e a m. (MonadError e m, UnifiedSafeSymShift mode e a m) => a -> a -> m a
- class UnifiedSafeFdiv (mode :: EvalModeTag) e a m where
- withBaseUnifiedSafeFdiv :: (SafeFdiv e a m => r) -> r
- safeFdiv :: forall mode e a m. (MonadError e m, UnifiedSafeFdiv mode e a m) => a -> a -> m a
- type family GetBool mode = bool | bool -> mode
- type family GetIntN mode = (i :: Nat -> Type) | i -> mode
- type family GetWordN mode = (w :: Nat -> Type) | w -> mode
- type family GetSomeWordN mode = sw | sw -> mode where ...
- type family GetSomeIntN mode = sw | sw -> mode where ...
- class UnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) => UnifiedBV mode n
- class SafeUnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) m => SafeUnifiedBV mode n m
- class SafeUnifiedSomeBVImpl mode (SomeBV (GetWordN mode)) (SomeBV (GetIntN mode)) m => SafeUnifiedSomeBV mode m
- type family GetInteger mode = int | int -> mode
- class UnifiedIntegerImpl mode (GetInteger mode) => UnifiedInteger (mode :: EvalModeTag)
- type family GetFP mode = (f :: Nat -> Nat -> Type) | f -> mode
- type family GetFPRoundingMode mode = r | r -> mode
- class UnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) => UnifiedFP mode eb sb
- 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 eb sb m
- type family GetAlgReal mode = real | real -> mode
- class UnifiedAlgRealImpl mode (GetAlgReal mode) => UnifiedAlgReal (mode :: EvalModeTag)
- type family GetData mode v = r | r -> mode v
- class UnifiedDataImpl mode v (GetData mode v) => UnifiedData mode v
- extractData :: (UnifiedDataImpl mode v u, Monad m, UnifiedBranching mode m) => u -> m v
- wrapData :: UnifiedDataImpl mode v u => v -> u
- type family GetFun mode = (fun :: Type -> Type -> Type) | fun -> mode
- type GetFun2 mode a b = GetFun mode a b
- type GetFun3 mode a b c = GetFun mode a (GetFun mode b c)
- type GetFun4 mode a b c d = GetFun mode a (GetFun mode b (GetFun mode c d))
- type GetFun5 mode a b c d e = GetFun mode a (GetFun mode b (GetFun mode c (GetFun mode d e)))
- type GetFun6 mode 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 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 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 a b ca cb sa sb = (Eq (GetFun mode a b), EvalSym (GetFun mode a b), ExtractSym (GetFun mode a b), PPrint (GetFun mode a b), Hashable (GetFun mode a b), Lift (GetFun mode a b), Mergeable (GetFun mode a b), NFData (GetFun mode a b), Show (GetFun mode a b), SubstSym (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 n1
- class UnifiedBVFPConversionImpl (mode :: EvalModeTag) (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
- 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 n eb sb m
- class UnifiedFPFPConversionImpl (mode :: EvalModeTag) (GetFP mode) eb0 sb0 eb1 sb1 (GetFP mode eb0 sb0) (GetFP mode eb1 sb1) (GetFPRoundingMode mode) => UnifiedFPFPConversion mode eb0 sb0 eb1 sb1
Evaluation mode
data EvalModeTag Source #
Instances
| Lift EvalModeTag Source # | |
Defined in Grisette.Unified.Internal.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 Con.
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.Unified.Internal.Theories Methods showsPrec :: Int -> TheoryToUnify -> ShowS # show :: TheoryToUnify -> String # showList :: [TheoryToUnify] -> ShowS # | |
| Eq TheoryToUnify Source # | |
Defined in Grisette.Unified.Internal.Theories Methods (==) :: TheoryToUnify -> TheoryToUnify -> Bool # (/=) :: TheoryToUnify -> TheoryToUnify -> Bool # | |
class (Typeable mode, UnifiedBool mode, UnifiedPrimitive mode (GetBool mode), Monad (BaseMonad mode), TryMerge (BaseMonad mode), UnifiedBranching mode (BaseMonad mode), AllUnifiedData mode) => EvalModeBase mode 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
| EvalModeBase 'Con Source # | |
Defined in Grisette.Unified.Internal.EvalMode | |
| EvalModeBase 'Sym Source # | |
Defined in Grisette.Unified.Internal.EvalMode | |
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 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 'Con Source # | |
Defined in Grisette.Unified.Internal.EvalMode | |
| EvalModeBV 'Sym Source # | |
Defined in Grisette.Unified.Internal.EvalMode | |
class (AllUnifiedFP mode, AllUnifiedFPFPConversion mode, AllUnifiedBVFPConversion mode) => EvalModeFP mode Source #
Provide the support for GetFP and
GetFPRoundingMode.
For compilers prior to GHC 9.2.1, see the notes for EvalModeAll.
Instances
| EvalModeFP 'Con Source # | |
Defined in Grisette.Unified.Internal.EvalMode | |
| EvalModeFP 'Sym Source # | |
Defined in Grisette.Unified.Internal.EvalMode | |
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 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
| EvalModeAll 'Con Source # | |
Defined in Grisette.Unified.Internal.EvalMode | |
| EvalModeAll 'Sym Source # | |
Defined in Grisette.Unified.Internal.EvalMode | |
type MonadEvalModeAll mode m = (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.
Unified operations
Unified simple mergeable
class Typeable mode => UnifiedBranching (mode :: EvalModeTag) m 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 UnifiedSimpleMergeable mode 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) (() :: Constraint) (SimpleMergeable a) => r) -> r Source #
Instances
class UnifiedSimpleMergeable1 mode f 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) (() :: Constraint) (SimpleMergeable1 f) => r) -> r Source #
Instances
class UnifiedSimpleMergeable2 mode f 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) (() :: Constraint) (SimpleMergeable2 f) => r) -> r Source #
Instances
mrgIf :: forall mode a m. (Typeable 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 a m. (Applicative m, UnifiedBranching mode m, Mergeable a) => BaseMonad mode a -> m a Source #
Unified lifting of a base monad.
mrgIte :: forall mode a. (Typeable mode, UnifiedSimpleMergeable mode a) => GetBool mode -> a -> a -> a Source #
Unified mrgIte.
mrgIte1 :: forall mode f a. (Typeable mode, UnifiedSimpleMergeable1 mode f, UnifiedSimpleMergeable mode a) => GetBool mode -> f a -> f a -> f a Source #
Unified mrgIte1.
liftMrgIte :: forall mode f a. (Typeable mode, UnifiedSimpleMergeable1 mode f) => (GetBool mode -> a -> a -> a) -> GetBool mode -> f a -> f a -> f a Source #
Unified liftMrgIte.
mrgIte2 :: forall mode f a b. (Typeable 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 f a b. (Typeable 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 a. (Typeable 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 v where Source #
A class that provides unified equality comparison.
We use this type class to help resolve the constraints for ITEOp.
Methods
withBaseITEOp :: (If (IsConMode mode) (() :: Constraint) (ITEOp v) => r) -> r Source #
Instances
| (Typeable mode, If (IsConMode mode) () (ITEOp a)) => UnifiedITEOp mode a Source # | |
Defined in Grisette.Unified.Internal.Class.UnifiedITEOp | |
| (Mergeable v, UnifiedITEOp 'Sym v) => UnifiedITEOp 'Sym (Union v) Source # | |
Defined in Grisette.Unified.Internal.Class.UnifiedITEOp | |
symIte :: forall mode v. (Typeable 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 v. (Typeable 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 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
symDistinct :: forall mode a. (Typeable 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 f a b. (Typeable mode, UnifiedSymEq1 mode f) => (a -> b -> GetBool mode) -> f a -> f b -> GetBool mode Source #
Unified liftSymEq.
symEq1 :: forall mode f a. (Typeable mode, UnifiedSymEq mode a, UnifiedSymEq1 mode f) => f a -> f a -> GetBool mode Source #
Unified symEq1.
liftSymEq2 :: forall mode f a b c d. (Typeable 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 f a b. (Typeable 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 a where Source #
A class that provides unified comparison.
We use this type class to help resolve the constraints for Ord and
SymOrd.
Instances
(.<) :: forall mode a. (Typeable mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode Source #
Unified (.<).
(.>=) :: forall mode a. (Typeable mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode Source #
Unified (.>=).
(.>) :: forall mode a. (Typeable mode, UnifiedSymOrd mode a) => a -> a -> GetBool mode Source #
Unified (.>).
symCompare :: forall mode a ctx. (Typeable mode, UnifiedSymOrd mode a, Monad ctx) => a -> a -> BaseMonad mode Ordering Source #
Unified symCompare.
liftSymCompare :: forall mode f a b. (Typeable mode, UnifiedSymOrd1 mode f) => (a -> b -> BaseMonad mode Ordering) -> f a -> f b -> BaseMonad mode Ordering Source #
Unified liftSymCompare.
symCompare1 :: forall mode f a. (Typeable mode, UnifiedSymOrd mode a, UnifiedSymOrd1 mode f) => f a -> f a -> BaseMonad mode Ordering Source #
Unified symCompare1.
liftSymCompare2 :: forall mode f a b c d. (Typeable 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 f a b. (Typeable 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 a. (UnifiedSymOrd mode a, UnifiedITEOp mode a, Typeable mode) => a -> a -> a Source #
Unified symMax.
symMin :: forall mode a. (UnifiedSymOrd mode a, UnifiedITEOp mode a, Typeable mode) => a -> a -> a Source #
Unified symMin.
mrgMax :: forall mode a m. (UnifiedSymOrd mode a, UnifiedBranching mode m, Typeable mode, Applicative m, Mergeable a) => a -> a -> m a Source #
Unified mrgMax.
mrgMin :: forall mode a m. (UnifiedSymOrd mode a, UnifiedBranching mode m, Typeable mode, Applicative m, Mergeable a) => a -> a -> m a Source #
Unified mrgMin.
Unified finite bits
class UnifiedFiniteBits mode 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 a. (Typeable mode, UnifiedFiniteBits mode a) => a -> Int -> GetBool mode Source #
Unified symTestBit.
symSetBitTo :: forall mode a. (Typeable mode, UnifiedFiniteBits mode a) => a -> Int -> GetBool mode -> a Source #
Unified symSetBitTo.
symFromBits :: forall mode a. (Typeable mode, UnifiedFiniteBits mode a) => [GetBool mode] -> a Source #
Unified symFromBits.
symBitBlast :: forall mode a. (Typeable mode, UnifiedFiniteBits mode a) => a -> [GetBool mode] Source #
Unified symBitBlast.
symLsb :: forall mode a. (Typeable mode, UnifiedFiniteBits mode a) => a -> GetBool mode Source #
Unified symLsb.
symMsb :: forall mode a. (Typeable mode, UnifiedFiniteBits mode a) => a -> GetBool mode Source #
Unified symMsb.
symPopCount :: forall mode a b. (Typeable mode, UnifiedFiniteBits mode a, Num b, UnifiedITEOp mode b) => a -> b Source #
Unified symPopCount.
symCountLeadingZeros :: forall mode a b. (Typeable mode, UnifiedFiniteBits mode a, Num b, UnifiedITEOp mode b) => a -> b Source #
Unified
symCountLeadingZeros.
symCountTrailingZeros :: forall mode a b. (Typeable mode, UnifiedFiniteBits mode a, Num b, UnifiedITEOp mode b) => a -> b 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 a b. (Typeable 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 'Sym m) => UnifiedSafeFdiv 'Sym ArithException SymAlgReal m Source # | |
Defined in Grisette.Unified.Internal.Class.UnifiedSafeFdiv Methods withBaseUnifiedSafeFdiv :: (SafeFdiv ArithException SymAlgReal m => r) -> r Source # | |
| (Typeable mode, MonadError ArithException m, UnifiedBranching mode m) => UnifiedSafeFdiv mode ArithException AlgReal m Source # | |
Defined in Grisette.Unified.Internal.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.Unified.Internal.Class.UnifiedSafeFdiv Methods withBaseUnifiedSafeFdiv :: (SafeFdiv e a m => r) -> r Source # | |
safeFdiv :: forall mode 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
Unified types
Boolean
Bit-vector
type family GetIntN mode = (i :: Nat -> Type) | i -> mode Source #
type family GetWordN mode = (w :: Nat -> Type) | w -> mode Source #
type family GetSomeWordN mode = sw | sw -> mode where ... Source #
Get a unified unsigned dynamic bit width bit vector type. Resolves to
SomeWordN in Con mode, and SomeSymWordN in Sym mode.
Equations
| GetSomeWordN mode = SomeBV (GetWordN mode) |
type family GetSomeIntN mode = sw | sw -> mode where ... Source #
Get a unified signed dynamic bit width bit vector type. Resolves to
SomeIntN in Con mode, and SomeSymIntN in Sym mode.
Equations
| GetSomeIntN mode = SomeBV (GetIntN mode) |
class UnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) => UnifiedBV mode n Source #
This class is needed as constraint in user code prior to GHC 9.2.1.
See the notes in EvalMode.
Instances
| UnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) => UnifiedBV mode n Source # | |
Defined in Grisette.Unified.Internal.UnifiedBV | |
class SafeUnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) m => SafeUnifiedBV mode n m Source #
This class is needed as constraint in user code prior to GHC 9.2.1.
See the notes in EvalMode.
Instances
| SafeUnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) m => SafeUnifiedBV mode n m Source # | |
Defined in Grisette.Unified.Internal.UnifiedBV | |
class SafeUnifiedSomeBVImpl mode (SomeBV (GetWordN mode)) (SomeBV (GetIntN mode)) m => SafeUnifiedSomeBV mode m Source #
This class is needed as constraint in user code prior to GHC 9.2.1.
See the notes in EvalMode.
Instances
| SafeUnifiedSomeBVImpl mode (SomeBV (GetWordN mode)) (SomeBV (GetIntN mode)) m => SafeUnifiedSomeBV mode m Source # | |
Defined in Grisette.Unified.Internal.UnifiedBV | |
Integer
type family GetInteger mode = int | int -> mode Source #
Get a unified Integer type. Resolves to Integer in Con mode, and
SymInteger in Sym mode.
Instances
| type GetInteger 'Con Source # | |
Defined in Grisette.Unified.Internal.UnifiedInteger | |
| type GetInteger 'Sym Source # | |
Defined in Grisette.Unified.Internal.UnifiedInteger | |
class UnifiedIntegerImpl mode (GetInteger mode) => UnifiedInteger (mode :: EvalModeTag) Source #
Evaluation mode with unified Integer type.
Instances
| UnifiedInteger 'Con Source # | |
Defined in Grisette.Unified.Internal.UnifiedInteger | |
| UnifiedInteger 'Sym Source # | |
Defined in Grisette.Unified.Internal.UnifiedInteger | |
FP
type family GetFPRoundingMode mode = r | r -> mode Source #
Get a unified floating point rounding mode type. Resolves to
FPRoundingMode in Con mode, and SymFPRoundingMode in Sym mode.
Instances
| type GetFPRoundingMode 'Con Source # | |
Defined in Grisette.Unified.Internal.UnifiedFP | |
| type GetFPRoundingMode 'Sym Source # | |
Defined in Grisette.Unified.Internal.UnifiedFP | |
class UnifiedFPImpl mode (GetFP mode) eb sb (GetFP mode eb sb) (GetFPRoundingMode mode) => UnifiedFP mode eb sb 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 # | |
Defined in Grisette.Unified.Internal.UnifiedFP | |
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 eb sb m 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 # | |
Defined in Grisette.Unified.Internal.UnifiedFP | |
AlgReal
type family GetAlgReal mode = real | real -> mode Source #
Get a unified algebraic real type. Resolves to AlgReal in Con mode,
and SymAlgReal in Sym mode.
Floating, LogBaseOr and SafeLogBase for
SymAlgReal are not provided as they are not available for AlgReal.
Instances
| type GetAlgReal 'Con Source # | |
Defined in Grisette.Unified.Internal.UnifiedAlgReal | |
| type GetAlgReal 'Sym Source # | |
Defined in Grisette.Unified.Internal.UnifiedAlgReal | |
class UnifiedAlgRealImpl mode (GetAlgReal mode) => UnifiedAlgReal (mode :: EvalModeTag) Source #
Evaluation mode with unified AlgReal type.
Instances
| UnifiedAlgReal 'Con Source # | |
Defined in Grisette.Unified.Internal.UnifiedAlgReal | |
| UnifiedAlgReal 'Sym Source # | |
Defined in Grisette.Unified.Internal.UnifiedAlgReal | |
Data
class UnifiedDataImpl mode v (GetData mode v) => UnifiedData mode 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.Unified.Internal.UnifiedData | |
extractData :: (UnifiedDataImpl mode v u, Monad m, UnifiedBranching mode m) => u -> m v Source #
Extracts a value from the unified data type.
Functions
type GetFun3 mode a b c = GetFun mode a (GetFun mode b c) Source #
The unified function type with 3 arguments.
type GetFun4 mode 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 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 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 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 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.
type UnifiedFunConstraint mode a b ca cb sa sb = (Eq (GetFun mode a b), EvalSym (GetFun mode a b), ExtractSym (GetFun mode a b), PPrint (GetFun mode a b), Hashable (GetFun mode a b), Lift (GetFun mode a b), Mergeable (GetFun mode a b), NFData (GetFun mode a b), Show (GetFun mode a b), SubstSym (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 n1 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.Unified.Internal.BVBVConversion | |
class UnifiedBVFPConversionImpl (mode :: EvalModeTag) (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 #
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 # | |
Defined in Grisette.Unified.Internal.BVFPConversion | |
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 n eb sb m 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 # | |
Defined in Grisette.Unified.Internal.BVFPConversion | |
class UnifiedFPFPConversionImpl (mode :: EvalModeTag) (GetFP mode) eb0 sb0 eb1 sb1 (GetFP mode eb0 sb0) (GetFP mode eb1 sb1) (GetFPRoundingMode mode) => UnifiedFPFPConversion mode eb0 sb0 eb1 sb1 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 # | |
Defined in Grisette.Unified.Internal.FPFPConversion | |