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.Internal.Unified.UnifiedBV

Description

Synopsis

class UnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) => UnifiedBV (mode :: EvalModeTag) (n :: Nat)
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 :: Nat -> Type) (intn :: Nat -> Type) (n :: Nat) word int | wordn -> intn, intn -> wordn, wordn n -> word, word -> wordn n, intn n -> int, int -> intn n where
- type GetWordN (mode :: EvalModeTag) = (w :: Nat -> Type) | w -> mode
- type GetIntN (mode :: EvalModeTag) = (i :: Nat -> Type) | i -> mode
class (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 :: EvalModeTag)
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 GetSomeWordN (mode :: EvalModeTag) = (sw :: Type) | sw -> mode where ...
type family GetSomeIntN (mode :: EvalModeTag) = (sw :: Type) | sw -> mode where ...
type SomeBVPair (mode :: EvalModeTag) 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)

Documentation

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.

Instances

Instances details

UnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) => UnifiedBV mode n Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV

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 :: Nat -> Type) (intn :: Nat -> Type) (n :: Nat) 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 :: EvalModeTag) = (w :: Nat -> Type) | w -> mode Source #

Get a unified unsigned size-tagged bit vector type. Resolves to WordN in C mode, and SymWordN in S mode.

type GetIntN (mode :: EvalModeTag) = (i :: Nat -> Type) | i -> mode Source #

Get a unified signed size-tagged bit vector type. Resolves to IntN in C mode, and SymIntN in S mode.

Instances

Instances details

(KnownNat n, 1 <= n) => UnifiedBVImpl 'C WordN IntN n (WordN n) (IntN n) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV

Associated Types

type GetWordN 'C
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV type GetWordN 'C = WordN
type GetIntN 'C
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV type GetIntN 'C = IntN

(KnownNat n, 1 <= n) => UnifiedBVImpl 'S SymWordN SymIntN n (SymWordN n) (SymIntN n) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV

Associated Types

type GetWordN 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV type GetWordN 'S = SymWordN
type GetIntN 'S
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV type GetIntN 'S = SymIntN

class (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 :: EvalModeTag) Source #

Evaluation mode with unified bit vector types.

Instances

Instances details

(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 #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV

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.

Instances

Instances details

SafeUnifiedBVImpl mode (GetWordN mode) (GetIntN mode) n (GetWordN mode n) (GetIntN mode n) m => SafeUnifiedBV mode n m Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV

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.

Instances

Instances details

SafeUnifiedSomeBVImpl mode (SomeBV (GetWordN mode)) (SomeBV (GetIntN mode)) m => SafeUnifiedSomeBV mode m Source #
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedBV

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)

type SomeBVPair (mode :: EvalModeTag) 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) Source #

Constraints for a pair of non-sized-tagged bit vector types.