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 (BVConstraint mode (GetWordN mode n) (GetIntN mode n), ConSymConversion (WordN n) (SymWordN n) (GetWordN mode n), UnifiedSimpleMergeable mode (GetWordN mode n), ConSymConversion (IntN n) (SymIntN n) (GetIntN mode n), UnifiedSimpleMergeable mode (GetIntN mode n), 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 Con mode, and SymWordN in Sym mode.

Instances

Instances details

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

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

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

Instances

Instances details

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

class (BVConstraint mode (GetWordN mode n) (GetIntN mode n), ConSymConversion (WordN n) (SymWordN n) (GetWordN mode n), UnifiedSimpleMergeable mode (GetWordN mode n), ConSymConversion (IntN n) (SymIntN n) (GetIntN mode n), UnifiedSimpleMergeable mode (GetIntN mode n), 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 'Con WordN IntN n (WordN n) (IntN n) Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedBV Associated Types type GetWordN 'Con = (w :: Nat -> Type) Source # type GetIntN 'Con = (i :: Nat -> Type) Source #
(KnownNat n, 1 <= n) => UnifiedBVImpl 'Sym SymWordN SymIntN n (SymWordN n) (SymIntN n) Source #
Instance details Defined in Grisette.Unified.Internal.UnifiedBV Associated Types type GetWordN 'Sym = (w :: Nat -> Type) Source # type GetIntN 'Sym = (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 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 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