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

Description

Synopsis

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

Documentation

type family GetWordN mode = (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.

Instances

Instances details

type GetWordN 'C Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedBV type GetWordN 'C = WordN
type GetWordN 'S Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedBV type GetWordN 'S = SymWordN

type family GetIntN mode = (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

type GetIntN 'C Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedBV type GetIntN 'C = IntN
type GetIntN 'S Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedBV type GetIntN 'S = SymIntN

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)) => 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.

Instances

Instances details

(KnownNat n, 1 <= n) => UnifiedBVImpl 'C WordN IntN n (WordN n) (IntN n) Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedBV Associated Types type GetWordN 'C = (w :: Nat -> Type) Source # type GetIntN 'C = (i :: Nat -> Type) Source #
(KnownNat n, 1 <= n) => UnifiedBVImpl 'S SymWordN SymIntN n (SymWordN n) (SymIntN n) Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedBV Associated Types type GetWordN 'S = (w :: Nat -> Type) Source # type GetIntN 'S = (i :: Nat -> Type) Source #

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

Instances details

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

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)

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

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.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

Instances details

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

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

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