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 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 BitwidthMismatch ArithException) m) => SafeUnifiedSomeBV mode m, forall n. (KnownNat n, 1 <= n) => UnifiedBV mode n, SomeBVPair mode (GetSomeWordN mode) (GetSomeIntN 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 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 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 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 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

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

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

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

Evaluation mode with unified bit vector types.

Instances details

Instance details