| 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 ...
- class (Typeable mode, UnifiedBool mode, UnifiedPrimitive mode (GetBool mode), UnifiedInteger mode, AllUnifiedBV mode, AllUnifiedData mode, Monad (BaseMonad mode), TryMerge (BaseMonad mode), UnifiedBranching mode (BaseMonad mode)) => EvalMode mode
- type MonadWithMode mode m = (EvalMode 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
- 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
- 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 UnifiedSafeDivision (mode :: EvalModeTag) e a m where
- withBaseSafeDivision :: (SafeDivision e a m => r) -> r
- safeDiv :: forall mode e a m. (MonadError e m, UnifiedSafeDivision mode e a m) => a -> a -> m a
- safeMod :: forall mode e a m. (MonadError e m, UnifiedSafeDivision mode e a m) => a -> a -> m a
- safeDivMod :: forall mode e a m. (MonadError e m, UnifiedSafeDivision mode e a m) => a -> a -> m (a, a)
- safeQuot :: forall mode e a m. (MonadError e m, UnifiedSafeDivision mode e a m) => a -> a -> m a
- safeRem :: forall mode e a m. (MonadError e m, UnifiedSafeDivision mode e a m) => a -> a -> m a
- safeQuotRem :: forall mode e a m. (MonadError e m, UnifiedSafeDivision 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
- 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 GetData 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
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
class (Typeable mode, UnifiedBool mode, UnifiedPrimitive mode (GetBool mode), UnifiedInteger mode, AllUnifiedBV mode, AllUnifiedData mode, Monad (BaseMonad mode), TryMerge (BaseMonad mode), UnifiedBranching mode (BaseMonad mode)) => EvalMode 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
| EvalMode 'Con Source # | |
Defined in Grisette.Unified.Internal.EvalMode | |
| EvalMode 'Sym Source # | |
Defined in Grisette.Unified.Internal.EvalMode | |
type MonadWithMode mode m = (EvalMode 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 EvalMode.
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.
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 | |
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
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 safe ops
class UnifiedSafeDivision (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 SafeDivision.
Methods
withBaseSafeDivision :: (SafeDivision e a m => r) -> r Source #
Instances
safeDiv :: forall mode e a m. (MonadError e m, UnifiedSafeDivision 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, UnifiedSafeDivision 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, UnifiedSafeDivision 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, UnifiedSafeDivision 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, UnifiedSafeDivision 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, UnifiedSafeDivision 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
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.
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 | |
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.