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

Description

Synopsis

class UnifiedFiniteBits (mode :: EvalModeTag) a where
- withBaseFiniteBits :: (If (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) => r) -> r
symTestBit :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> Int -> GetBool mode
symSetBitTo :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> Int -> GetBool mode -> a
symFromBits :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => [GetBool mode] -> a
symBitBlast :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> [GetBool mode]
symLsb :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> GetBool mode
symMsb :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> GetBool mode
symPopCount :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) => a -> a
symCountLeadingZeros :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) => a -> a
symCountTrailingZeros :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) => a -> a

Documentation

class UnifiedFiniteBits (mode :: EvalModeTag) a where Source #

A class that provides unified equality comparison.

We use this type class to help resolve the constraints for FiniteBits, FromBits and SymFiniteBits.

Methods

withBaseFiniteBits :: (If (IsConMode mode) (FiniteBits a, FromBits a) (SymFiniteBits a) => r) -> r Source #

Instances

Instances details

UnifiedFiniteBits 'C SomeIntN Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'C) (FiniteBits SomeIntN, FromBits SomeIntN) (SymFiniteBits SomeIntN) => r) -> r Source #
UnifiedFiniteBits 'C SomeWordN Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'C) (FiniteBits SomeWordN, FromBits SomeWordN) (SymFiniteBits SomeWordN) => r) -> r Source #
UnifiedFiniteBits 'S SomeSymIntN Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits SomeSymIntN, FromBits SomeSymIntN) (SymFiniteBits SomeSymIntN) => r) -> r Source #
UnifiedFiniteBits 'S SomeSymWordN Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits SomeSymWordN, FromBits SomeSymWordN) (SymFiniteBits SomeSymWordN) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedFiniteBits 'C (IntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'C) (FiniteBits (IntN n), FromBits (IntN n)) (SymFiniteBits (IntN n)) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedFiniteBits 'C (WordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'C) (FiniteBits (WordN n), FromBits (WordN n)) (SymFiniteBits (WordN n)) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedFiniteBits 'S (SymIntN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits (SymIntN n), FromBits (SymIntN n)) (SymFiniteBits (SymIntN n)) => r) -> r Source #
(KnownNat n, 1 <= n) => UnifiedFiniteBits 'S (SymWordN n) Source #
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedFiniteBits Methods withBaseFiniteBits :: (If (IsConMode 'S) (FiniteBits (SymWordN n), FromBits (SymWordN n)) (SymFiniteBits (SymWordN n)) => r) -> r Source #

symTestBit :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> Int -> GetBool mode Source #

Unified symTestBit.

symSetBitTo :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> Int -> GetBool mode -> a Source #

Unified symSetBitTo.

symFromBits :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => [GetBool mode] -> a Source #

Unified symFromBits.

symBitBlast :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> [GetBool mode] Source #

Unified symBitBlast.

symLsb :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> GetBool mode Source #

Unified symLsb.

symMsb :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a) => a -> GetBool mode Source #

Unified symMsb.

symPopCount :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) => a -> a Source #

Unified symPopCount.

symCountLeadingZeros :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) => a -> a Source #

Unified symCountLeadingZeros.

symCountTrailingZeros :: forall (mode :: EvalModeTag) a. (DecideEvalMode mode, UnifiedFiniteBits mode a, Num a, UnifiedITEOp mode a) => a -> a Source #

Unified symCountTrailingZeros.