| 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.Internal.Unified.UnifiedBV
Description
Synopsis
- class UnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) => UnifiedBV mode n
- class (UnifiedConRep word, UnifiedSymRep int, ConType word ~ WordN n, SymType word ~ SymWordN n, ConType int ~ IntN n, SymType int ~ SymIntN n, UnifiedBasicPrim mode word, UnifiedBasicPrim mode int, BVConstraint mode word int, wordn ~ GetWordN mode, intn ~ GetIntN mode, word ~ wordn n, int ~ intn n, BitCast word int, BitCast int word, DivOr word, DivOr int, UnifiedFromIntegral mode (GetInteger mode) word, UnifiedFromIntegral mode (GetInteger mode) int, UnifiedFromIntegral mode word (GetInteger mode), UnifiedFromIntegral mode word (GetAlgReal mode), UnifiedFromIntegral mode int (GetInteger mode), UnifiedFromIntegral mode int (GetAlgReal mode), ConSymConversion (WordN n) (SymWordN n) word, ConSymConversion (IntN n) (SymIntN n) int) => UnifiedBVImpl (mode :: EvalModeTag) wordn intn n word int | wordn -> intn, intn -> wordn, wordn n -> word, word -> wordn n, intn n -> int, int -> intn n where
- class (forall n m. (UnifiedBranching mode m, MonadError ArithException m, KnownNat n, 1 <= n) => SafeUnifiedBV mode n m, forall m. (UnifiedBranching mode m, MonadError (Either SomeBVException ArithException) m) => SafeUnifiedSomeBV mode m, forall n. (KnownNat n, 1 <= n) => UnifiedBV mode n, SomeBVPair mode (GetSomeWordN mode) (GetSomeIntN mode), SizedBV (GetWordN mode), SizedBV (GetIntN mode)) => AllUnifiedBV mode
- 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 GetSomeWordN mode = sw | sw -> mode where ...
- type family GetSomeIntN mode = sw | sw -> mode where ...
- type SomeBVPair mode word int = (UnifiedPrim mode word, UnifiedPrim mode int, BVConstraint mode word int, BV word, BV int, DivOr word, DivOr int, ConSymConversion SomeWordN SomeSymWordN word, ConSymConversion SomeIntN SomeSymIntN int) :: Constraint
Documentation
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 (UnifiedConRep word, UnifiedSymRep int, ConType word ~ WordN n, SymType word ~ SymWordN n, ConType int ~ IntN n, SymType int ~ SymIntN n, UnifiedBasicPrim mode word, UnifiedBasicPrim mode int, BVConstraint mode word int, wordn ~ GetWordN mode, intn ~ GetIntN mode, word ~ wordn n, int ~ intn n, BitCast word int, BitCast int word, DivOr word, DivOr int, UnifiedFromIntegral mode (GetInteger mode) word, UnifiedFromIntegral mode (GetInteger mode) int, UnifiedFromIntegral mode word (GetInteger mode), UnifiedFromIntegral mode word (GetAlgReal mode), UnifiedFromIntegral mode int (GetInteger mode), UnifiedFromIntegral mode int (GetAlgReal mode), ConSymConversion (WordN n) (SymWordN n) word, ConSymConversion (IntN n) (SymIntN n) int) => UnifiedBVImpl (mode :: EvalModeTag) wordn intn n word int | wordn -> intn, intn -> wordn, wordn n -> word, word -> wordn n, intn n -> int, int -> intn n Source #
Implementation for UnifiedBV.
Associated Types
type GetWordN mode = (w :: Nat -> Type) | w -> mode Source #
class (forall n m. (UnifiedBranching mode m, MonadError ArithException m, KnownNat n, 1 <= n) => SafeUnifiedBV mode n m, forall m. (UnifiedBranching mode m, MonadError (Either SomeBVException ArithException) m) => SafeUnifiedSomeBV mode m, forall n. (KnownNat n, 1 <= n) => UnifiedBV mode n, SomeBVPair mode (GetSomeWordN mode) (GetSomeIntN mode), SizedBV (GetWordN mode), SizedBV (GetIntN mode)) => AllUnifiedBV mode Source #
Evaluation mode with unified bit vector types.
Instances
| (forall (n :: Nat) (m :: Type -> Type). (UnifiedBranching mode m, MonadError ArithException m, KnownNat n, 1 <= n) => SafeUnifiedBV mode n m, forall (m :: Type -> Type). (UnifiedBranching mode m, MonadError (Either SomeBVException ArithException) m) => SafeUnifiedSomeBV mode m, forall (n :: Nat). (KnownNat n, 1 <= n) => UnifiedBV mode n, SomeBVPair mode (GetSomeWordN mode) (GetSomeIntN mode), SizedBV (GetWordN mode), SizedBV (GetIntN mode)) => AllUnifiedBV mode Source # | |
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.
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.
type family GetSomeWordN mode = sw | 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 = sw | 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) |
type SomeBVPair mode word int = (UnifiedPrim mode word, UnifiedPrim mode int, BVConstraint mode word int, BV word, BV int, DivOr word, DivOr int, ConSymConversion SomeWordN SomeSymWordN word, ConSymConversion SomeIntN SomeSymIntN int) :: Constraint Source #
Constraints for a pair of non-sized-tagged bit vector types.