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

Description

Synopsis

type ValidFP (eb :: Nat) (sb :: Nat) = ValidFloat eb sb
newtype FP (eb :: Nat) (sb :: Nat) = FP {
- unFP :: FloatingPoint eb sb
}
type FP16 = FP 5 11
type FP32 = FP 8 24
type FP64 = FP 11 53
withValidFPProofs :: forall (eb :: Nat) (sb :: Nat) r. ValidFP eb sb => ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb), 1 <= eb, 1 <= sb) => r) -> r
data FPRoundingMode
- = RNE
- | RNA
- | RTP
- | RTN
- | RTZ
allFPRoundingMode :: [FPRoundingMode]
data NotRepresentableFPError
- = NaNError
- | FPUnderflowError
- | FPOverflowError
class ConvertibleBound (bv :: Nat -> Type) where
- convertibleLowerBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => bv n -> FPRoundingMode -> FP eb sb
- convertibleUpperBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => bv n -> FPRoundingMode -> FP eb sb
nextFP :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FP eb sb -> FP eb sb
prevFP :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FP eb sb -> FP eb sb
withUnsafeValidFP :: forall (eb :: Nat) (sb :: Nat) r. (KnownNat eb, KnownNat sb) => (ValidFP eb sb => r) -> r
checkDynamicValidFP :: Natural -> Natural -> Bool
invalidFPMessage :: String

Documentation

type ValidFP (eb :: Nat) (sb :: Nat) = ValidFloat eb sb Source #

A type-level proof that the given bit-widths are valid for a floating-point number.

newtype FP (eb :: Nat) (sb :: Nat) Source #

IEEE 754 floating-point number with eb exponent bits and sb significand bits.

>>> 1.0 + 2.0 :: FP 11 53
3.0

More operations are available. Please refer to Grisette.Core for more information.

Constructors

FP
Fields unFP :: FloatingPoint eb sb

Instances

Instances details

PEvalFPTerm FP Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFP

Methods

pevalFPTraitTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPTrait -> Term (FP eb sb) -> Term Bool Source #

pevalFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPUnaryOp -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPBinaryOp -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingUnaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingBinaryOp -> Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalFPFMATerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

sbvFPTraitTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPTrait -> SBVType (FP eb sb) -> SBVType Bool Source #

sbvFPUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPUnaryOp -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvFPBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPBinaryOp -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvFPRoundingUnaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingUnaryOp -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvFPRoundingBinaryTerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FPRoundingBinaryOp -> SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvFPFMATerm :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

BitCast Int16 FP16 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Int16 -> FP16 Source #

BitCast Int32 FP32 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Int32 -> FP32 Source #

BitCast Int64 FP64 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Int64 -> FP64 Source #

BitCast Word16 FP16 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Word16 -> FP16 Source #

BitCast Word32 FP32 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Word32 -> FP32 Source #

BitCast Word64 FP64 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Word64 -> FP64 Source #

BitCast Double FP64 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Double -> FP64 Source #

BitCast Float FP32 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: Float -> FP32 Source #

BitCastCanonical FP16 Int16 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastCanonicalValue :: proxy FP16 -> Int16 Source #

BitCastCanonical FP16 Word16 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastCanonicalValue :: proxy FP16 -> Word16 Source #

BitCastCanonical FP32 Int32 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastCanonicalValue :: proxy FP32 -> Int32 Source #

BitCastCanonical FP32 Word32 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastCanonicalValue :: proxy FP32 -> Word32 Source #

BitCastCanonical FP32 Float Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastCanonicalValue :: proxy FP32 -> Float Source #

BitCastCanonical FP64 Int64 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastCanonicalValue :: proxy FP64 -> Int64 Source #

BitCastCanonical FP64 Word64 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastCanonicalValue :: proxy FP64 -> Word64 Source #

BitCastCanonical FP64 Double Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastCanonicalValue :: proxy FP64 -> Double Source #

BitCastOr FP16 Int16 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastOr :: Int16 -> FP16 -> Int16 Source #

BitCastOr FP16 Word16 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastOr :: Word16 -> FP16 -> Word16 Source #

BitCastOr FP32 Int32 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastOr :: Int32 -> FP32 -> Int32 Source #

BitCastOr FP32 Word32 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastOr :: Word32 -> FP32 -> Word32 Source #

BitCastOr FP32 Float Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastOr :: Float -> FP32 -> Float Source #

BitCastOr FP64 Int64 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastOr :: Int64 -> FP64 -> Int64 Source #

BitCastOr FP64 Word64 Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastOr :: Word64 -> FP64 -> Word64 Source #

BitCastOr FP64 Double Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastOr :: Double -> FP64 -> Double Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP16 Int16 m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP16 -> m Int16 Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP16 Word16 m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP16 -> m Word16 Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP32 Int32 m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP32 -> m Int32 Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP32 Word32 m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP32 -> m Word32 Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP32 Float m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP32 -> m Float Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP64 Int64 m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP64 -> m Int64 Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP64 Word64 m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP64 -> m Word64 Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP64 Double m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP64 -> m Double Source #

ValidFP eb sb => UnifiedFPImpl 'C FP eb sb (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP

Associated Types

type GetFP 'C
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP type GetFP 'C = FP
type GetFPRoundingMode 'C
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP type GetFPRoundingMode 'C = FPRoundingMode

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb) => UnifiedSafeFromFP mode NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb) => UnifiedSafeFromFP mode NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m => r) -> r Source #

ValidFP eb sb => UnifiedFromIntegral 'C Integer (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral Integer, Num (FP eb sb)) (SymFromIntegral Integer (FP eb sb)) => r) -> r Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m AlgReal Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m Integer Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast mode NotRepresentableFPError (FP eb sb) (IntN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (FP eb sb) (IntN n) m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast mode NotRepresentableFPError (FP eb sb) (WordN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (FP eb sb) (WordN n) m => r) -> r Source #

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'C (IntN n') (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (IntN n'), Num (FP eb sb)) (SymFromIntegral (IntN n') (FP eb sb)) => r) -> r Source #

(KnownNat n', 1 <= n', ValidFP eb sb) => UnifiedFromIntegral 'C (WordN n') (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedFromIntegral

Methods

withBaseFromIntegral :: (If (IsConMode 'C) (Integral (WordN n'), Num (FP eb sb)) (SymFromIntegral (WordN n') (FP eb sb)) => r) -> r Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m (IntN n) Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m (WordN n) Source #

(DecideEvalMode mode, ValidFP a1 a2) => UnifiedSymEq mode (FP a1 a2) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymEq

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq (FP a1 a2)) (SymEq (FP a1 a2)) => r) -> r Source #

(DecideEvalMode mode, ValidFP a1 a2) => UnifiedSymOrd mode (FP a1 a2) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymOrd

Methods

withBaseSymOrd :: (If (IsConMode mode) (Ord (FP a1 a2)) (SymOrd (FP a1 a2)) => r) -> r Source #

ValidFP eb sb => PEvalFromIntegralTerm Integer (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term Integer -> Term (FP eb sb) Source #

sbvFromIntegralTerm :: SBVType Integer -> SBVType (FP eb sb) Source #

ValidFP eb sb => Lift (FP eb sb :: Type) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

lift :: Quote m => FP eb sb -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => FP eb sb -> Code m (FP eb sb) #

ValidFP eb sb => IEEEFPConvertible AlgReal (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fromFPOr :: AlgReal -> FPRoundingMode -> FP eb sb -> AlgReal Source #

toFP :: FPRoundingMode -> AlgReal -> FP eb sb Source #

ValidFP eb sb => IEEEFPConvertible Integer (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fromFPOr :: Integer -> FPRoundingMode -> FP eb sb -> Integer Source #

toFP :: FPRoundingMode -> Integer -> FP eb sb Source #

ValidFP eb sb => IEEEFPToAlgReal AlgReal (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fpToAlgReal :: AlgReal -> FP eb sb -> AlgReal Source #

(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, TryMerge m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (FP eb sb) (IntN r) m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP eb sb -> m (IntN r) Source #

(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, TryMerge m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (FP eb sb) (WordN r) m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP eb sb -> m (WordN r) Source #

ValidFP eb sb => UnifiedSolvable 'C (FP eb sb) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSolvable

Methods

withBaseSolvable :: (If (IsConMode 'C) (FP eb sb ~ FP eb sb) (Solvable (FP eb sb) (FP eb sb)) => r) -> r Source #

ValidFP eb sb => UnifiedSolvable 'S (SymFP eb sb) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSolvable

Methods

withBaseSolvable :: (If (IsConMode 'S) (SymFP eb sb ~ FP eb sb) (Solvable (FP eb sb) (SymFP eb sb)) => r) -> r Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCast (IntN r) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: IntN r -> FP eb sb Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCast (WordN r) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCast :: WordN r -> FP eb sb Source #

(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastTerm (IntN n) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm

Methods

pevalBitCastTerm :: Term (IntN n) -> Term (FP eb sb) Source #

sbvBitCast :: SBVType (IntN n) -> SBVType (FP eb sb) Source #

(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastTerm (WordN n) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm

Methods

pevalBitCastTerm :: Term (WordN n) -> Term (FP eb sb) Source #

sbvBitCast :: SBVType (WordN n) -> SBVType (FP eb sb) Source #

(KnownNat n, 1 <= n, ValidFP eb sb) => PEvalFromIntegralTerm (IntN n) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (IntN n) -> Term (FP eb sb) Source #

sbvFromIntegralTerm :: SBVType (IntN n) -> SBVType (FP eb sb) Source #

(KnownNat n, 1 <= n, ValidFP eb sb) => PEvalFromIntegralTerm (WordN n) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFromIntegralTerm

Methods

pevalFromIntegralTerm :: Term (WordN n) -> Term (FP eb sb) Source #

sbvFromIntegralTerm :: SBVType (WordN n) -> SBVType (FP eb sb) Source #

(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (IntN n) (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fromFPOr :: IntN n -> FPRoundingMode -> FP eb sb -> IntN n Source #

toFP :: FPRoundingMode -> IntN n -> FP eb sb Source #

(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (WordN n) (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fromFPOr :: WordN n -> FPRoundingMode -> FP eb sb -> WordN n Source #

toFP :: FPRoundingMode -> WordN n -> FP eb sb Source #

ValidFloat eb sb => Arbitrary (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

arbitrary :: Gen (FP eb sb) #

shrink :: FP eb sb -> [FP eb sb] #

ValidFP eb sb => Binary (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

put :: FP eb sb -> Put #

get :: Get (FP eb sb) #

putList :: [FP eb sb] -> Put #

ValidFP eb sb => Serial (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

serialize :: MonadPut m => FP eb sb -> m () #

deserialize :: MonadGet m => m (FP eb sb) #

ValidFP eb sb => Serialize (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

put :: Putter (FP eb sb) #

get :: Get (FP eb sb) #

NFData (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

rnf :: FP eb sb -> () #

ValidFloat eb sb => Floating (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

pi :: FP eb sb #

exp :: FP eb sb -> FP eb sb #

log :: FP eb sb -> FP eb sb #

sqrt :: FP eb sb -> FP eb sb #

(**) :: FP eb sb -> FP eb sb -> FP eb sb #

logBase :: FP eb sb -> FP eb sb -> FP eb sb #

sin :: FP eb sb -> FP eb sb #

cos :: FP eb sb -> FP eb sb #

tan :: FP eb sb -> FP eb sb #

asin :: FP eb sb -> FP eb sb #

acos :: FP eb sb -> FP eb sb #

atan :: FP eb sb -> FP eb sb #

sinh :: FP eb sb -> FP eb sb #

cosh :: FP eb sb -> FP eb sb #

tanh :: FP eb sb -> FP eb sb #

asinh :: FP eb sb -> FP eb sb #

acosh :: FP eb sb -> FP eb sb #

atanh :: FP eb sb -> FP eb sb #

log1p :: FP eb sb -> FP eb sb #

expm1 :: FP eb sb -> FP eb sb #

log1pexp :: FP eb sb -> FP eb sb #

log1mexp :: FP eb sb -> FP eb sb #

ValidFloat eb sb => RealFloat (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

floatRadix :: FP eb sb -> Integer #

floatDigits :: FP eb sb -> Int #

floatRange :: FP eb sb -> (Int, Int) #

decodeFloat :: FP eb sb -> (Integer, Int) #

encodeFloat :: Integer -> Int -> FP eb sb #

exponent :: FP eb sb -> Int #

significand :: FP eb sb -> FP eb sb #

scaleFloat :: Int -> FP eb sb -> FP eb sb #

isNaN :: FP eb sb -> Bool #

isInfinite :: FP eb sb -> Bool #

isDenormalized :: FP eb sb -> Bool #

isNegativeZero :: FP eb sb -> Bool #

isIEEE :: FP eb sb -> Bool #

atan2 :: FP eb sb -> FP eb sb -> FP eb sb #

ValidFloat eb sb => Num (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

(+) :: FP eb sb -> FP eb sb -> FP eb sb #

(-) :: FP eb sb -> FP eb sb -> FP eb sb #

(*) :: FP eb sb -> FP eb sb -> FP eb sb #

negate :: FP eb sb -> FP eb sb #

abs :: FP eb sb -> FP eb sb #

signum :: FP eb sb -> FP eb sb #

fromInteger :: Integer -> FP eb sb #

ValidFloat eb sb => Fractional (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

(/) :: FP eb sb -> FP eb sb -> FP eb sb #

recip :: FP eb sb -> FP eb sb #

fromRational :: Rational -> FP eb sb #

ValidFloat eb sb => Real (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

toRational :: FP eb sb -> Rational #

ValidFloat eb sb => RealFrac (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

properFraction :: Integral b => FP eb sb -> (b, FP eb sb) #

truncate :: Integral b => FP eb sb -> b #

round :: Integral b => FP eb sb -> b #

ceiling :: Integral b => FP eb sb -> b #

floor :: Integral b => FP eb sb -> b #

Show (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

showsPrec :: Int -> FP eb sb -> ShowS #

show :: FP eb sb -> String #

showList :: [FP eb sb] -> ShowS #

Eq (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

(==) :: FP eb sb -> FP eb sb -> Bool #

(/=) :: FP eb sb -> FP eb sb -> Bool #

ValidFP eb sb => Ord (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

compare :: FP eb sb -> FP eb sb -> Ordering #

(<) :: FP eb sb -> FP eb sb -> Bool #

(<=) :: FP eb sb -> FP eb sb -> Bool #

(>) :: FP eb sb -> FP eb sb -> Bool #

(>=) :: FP eb sb -> FP eb sb -> Bool #

max :: FP eb sb -> FP eb sb -> FP eb sb #

min :: FP eb sb -> FP eb sb -> FP eb sb #

Apply (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Associated Types

type FunType (FP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.FP type FunType (FP eb sb) = FP eb sb

Methods

apply :: FP eb sb -> FunType (FP eb sb) Source #

ValidFP eb sb => IEEEFPConstants (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fpPositiveInfinite :: FP eb sb Source #

fpNegativeInfinite :: FP eb sb Source #

fpNaN :: FP eb sb Source #

fpNegativeZero :: FP eb sb Source #

fpPositiveZero :: FP eb sb Source #

fpMinNormalized :: FP eb sb Source #

fpMinSubnormal :: FP eb sb Source #

fpMaxNormalized :: FP eb sb Source #

fpMaxSubnormal :: FP eb sb Source #

ValidFP eb sb => IEEEFPOp (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fpAbs :: FP eb sb -> FP eb sb Source #

fpNeg :: FP eb sb -> FP eb sb Source #

fpRem :: FP eb sb -> FP eb sb -> FP eb sb Source #

fpMinimum :: FP eb sb -> FP eb sb -> FP eb sb Source #

fpMinimumNumber :: FP eb sb -> FP eb sb -> FP eb sb Source #

fpMaximum :: FP eb sb -> FP eb sb -> FP eb sb Source #

fpMaximumNumber :: FP eb sb -> FP eb sb -> FP eb sb Source #

ValidFP eb sb => SymIEEEFPTraits (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SymIEEEFP

Methods

symFpIsNaN :: FP eb sb -> SymBool Source #

symFpIsPositive :: FP eb sb -> SymBool Source #

symFpIsNegative :: FP eb sb -> SymBool Source #

symFpIsPositiveInfinite :: FP eb sb -> SymBool Source #

symFpIsNegativeInfinite :: FP eb sb -> SymBool Source #

symFpIsInfinite :: FP eb sb -> SymBool Source #

symFpIsPositiveZero :: FP eb sb -> SymBool Source #

symFpIsNegativeZero :: FP eb sb -> SymBool Source #

symFpIsZero :: FP eb sb -> SymBool Source #

symFpIsNormal :: FP eb sb -> SymBool Source #

symFpIsSubnormal :: FP eb sb -> SymBool Source #

symFpIsPoint :: FP eb sb -> SymBool Source #

ValidFP eb fb => EvalSym (FP eb fb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> FP eb fb -> FP eb fb Source #

ValidFP eb sb => ExtractSym (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym

Methods

extractSym :: FP eb sb -> AnySymbolSet Source #

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => FP eb sb -> Maybe (SymbolSet knd) Source #

ValidFP eb sb => Mergeable (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy (FP eb sb) Source #

sortIndices :: FP eb sb -> [DynamicSortedIdx] Source #

ValidFP eb sb => PPrint (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint

Methods

pformat :: FP eb sb -> Doc ann Source #

pformatPrec :: Int -> FP eb sb -> Doc ann Source #

pformatList :: [FP eb sb] -> Doc ann Source #

ValidFP eb sb => SubstSym (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym

Methods

substSym :: forall cb sb0 (knd :: SymbolKind). (LinkedRep cb sb0, IsSymbolKind knd) => TypedSymbol knd cb -> sb0 -> FP eb sb -> FP eb sb Source #

ValidFP eb sb => SymEq (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq

Methods

(.==) :: FP eb sb -> FP eb sb -> SymBool Source #

(./=) :: FP eb sb -> FP eb sb -> SymBool Source #

symDistinct :: [FP eb sb] -> SymBool Source #

ValidFP eb sb => SymOrd (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd

Methods

(.<) :: FP eb sb -> FP eb sb -> SymBool Source #

(.<=) :: FP eb sb -> FP eb sb -> SymBool Source #

(.>) :: FP eb sb -> FP eb sb -> SymBool Source #

(.>=) :: FP eb sb -> FP eb sb -> SymBool Source #

symCompare :: FP eb sb -> FP eb sb -> Union Ordering Source #

ValidFP eb sb => AllSyms (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: FP eb sb -> [SomeSym] -> [SomeSym] Source #

allSyms :: FP eb sb -> [SomeSym] Source #

ValidFP eb sb => NonFuncSBVRep (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type NonFuncSBVBaseType (FP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type NonFuncSBVBaseType (FP eb sb) = FloatingPoint eb sb

ValidFP eb sb => PEvalFloatingTerm (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFloatingTerm

Methods

pevalFloatingUnaryTerm :: FloatingUnaryOp -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalPowerTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

withSbvFloatingTermConstraint :: (Floating (SBVType (FP eb sb)) => r) -> r Source #

sbvPowerTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvFloatingUnaryTerm :: FloatingUnaryOp -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

ValidFP eb sb => PEvalFractionalTerm (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalFractionalTerm

Methods

pevalFdivTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalRecipTerm :: Term (FP eb sb) -> Term (FP eb sb) Source #

withSbvFractionalTermConstraint :: (Fractional (SBVType (FP eb sb)) => r) -> r Source #

sbvFdivTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvRecipTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

ValidFP eb sb => PEvalIEEEFPConvertibleTerm (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm

Methods

pevalFromFPOrTerm :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFP eb0 sb0 => Term (FP eb sb) -> Term FPRoundingMode -> Term (FP eb0 sb0) -> Term (FP eb sb) Source #

pevalToFPTerm :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFP eb0 sb0 => Term FPRoundingMode -> Term (FP eb sb) -> Term (FP eb0 sb0) Source #

sbvFromFPOrTerm :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFP eb0 sb0 => SBVType (FP eb sb) -> SBVType FPRoundingMode -> SBVType (FP eb0 sb0) -> SBVType (FP eb sb) Source #

sbvToFPTerm :: forall (eb0 :: Nat) (sb0 :: Nat). ValidFP eb0 sb0 => SBVType FPRoundingMode -> SBVType (FP eb sb) -> SBVType (FP eb0 sb0) Source #

ValidFP eb sb => PEvalNumTerm (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalNumTerm

Methods

pevalAddNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalNegNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source #

pevalMulNumTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalAbsNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source #

pevalSignumNumTerm :: Term (FP eb sb) -> Term (FP eb sb) Source #

withSbvNumTermConstraint :: (Num (SBVType (FP eb sb)) => r) -> r Source #

sbvAddNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvNegNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvMulNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvAbsNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvSignumNumTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

ValidFP eb sb => PEvalOrdTerm (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm

Methods

pevalLtOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool Source #

pevalLeOrdTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool Source #

withSbvOrdTermConstraint :: (OrdSymbolic (SBVType (FP eb sb)) => r) -> r Source #

sbvLtOrdTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBV Bool Source #

sbvLeOrdTerm :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBV Bool Source #

ValidFP eb sb => SBVRep (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type SBVType (FP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type SBVType (FP eb sb) = SBV (FloatingPoint eb sb)

ValidFP eb sb => SupportedNonFuncPrim (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

conNonFuncSBVTerm :: FP eb sb -> SBV (NonFuncSBVBaseType (FP eb sb)) Source #

symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType (FP eb sb))) Source #

withNonFuncPrim :: (NonFuncPrimConstraint (FP eb sb) => r) -> r Source #

ValidFP eb sb => SupportedPrim (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

primTypeRep :: TypeRep (FP eb sb) Source #

sameCon :: FP eb sb -> FP eb sb -> Bool Source #

hashConWithSalt :: Int -> FP eb sb -> Int Source #

pformatCon :: FP eb sb -> String Source #

defaultValue :: FP eb sb Source #

pevalITETerm :: Term Bool -> Term (FP eb sb) -> Term (FP eb sb) -> Term (FP eb sb) Source #

pevalEqTerm :: Term (FP eb sb) -> Term (FP eb sb) -> Term Bool Source #

pevalDistinctTerm :: NonEmpty (Term (FP eb sb)) -> Term Bool Source #

conSBVTerm :: FP eb sb -> SBVType (FP eb sb) Source #

symSBVName :: TypedSymbol 'AnyKind (FP eb sb) -> Int -> String Source #

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType (FP eb sb)) Source #

withPrim :: ((PrimConstraint (FP eb sb), SMTDefinable (SBVType (FP eb sb)), Mergeable (SBVType (FP eb sb)), Typeable (SBVType (FP eb sb))) => a) -> a Source #

sbvIte :: SBV Bool -> SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBVType (FP eb sb) Source #

sbvEq :: SBVType (FP eb sb) -> SBVType (FP eb sb) -> SBV Bool Source #

sbvDistinct :: NonEmpty (SBVType (FP eb sb)) -> SBV Bool Source #

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FP eb sb Source #

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd (FP eb sb) -> Maybe (TypedSymbol knd' (FP eb sb)) Source #

funcDummyConstraint :: SBVType (FP eb sb) -> SBV Bool Source #

ValidFP eb sb => SupportedPrimConstraint (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type PrimConstraint (FP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type PrimConstraint (FP eb sb) = ValidFP eb sb

ValidFP eb sb => SymRep (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type SymType (FP eb sb)
Instance details Defined in Grisette.Internal.SymPrim.SymFP type SymType (FP eb sb) = SymFP eb sb

ValidFP eb sb => UnifiedConRep (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type ConType (FP eb sb)
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type ConType (FP eb sb) = FP eb sb

ValidFP eb sb => UnifiedSymRep (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

Associated Types

type SymType (FP eb sb)
Instance details Defined in Grisette.Internal.Unified.Class.UnifiedRep type SymType (FP eb sb) = SymFP eb sb

ValidFP eb sb => Hashable (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

hashWithSalt :: Int -> FP eb sb -> Int #

hash :: FP eb sb -> Int #

ValidFP eb sb => IEEEFPRoundingOp (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fpAdd :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source #

fpSub :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source #

fpMul :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source #

fpDiv :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source #

fpFMA :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb -> FP eb sb Source #

fpSqrt :: FPRoundingMode -> FP eb sb -> FP eb sb Source #

fpRoundToIntegral :: FPRoundingMode -> FP eb sb -> FP eb sb Source #

(ValidFP eb sb, n ~ (eb + sb)) => BitCastCanonical (FP eb sb) (IntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastCanonicalValue :: proxy (FP eb sb) -> IntN n Source #

(ValidFP eb sb, n ~ (eb + sb)) => BitCastCanonical (FP eb sb) (WordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastCanonicalValue :: proxy (FP eb sb) -> WordN n Source #

(ValidFP eb sb, n ~ (eb + sb)) => BitCastOr (FP eb sb) (IntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastOr :: IntN n -> FP eb sb -> IntN n Source #

(ValidFP eb sb, r ~ (eb + sb)) => BitCastOr (FP eb sb) (WordN r) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

bitCastOr :: WordN r -> FP eb sb -> WordN r Source #

(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastOrTerm (FP eb sb) (IntN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm

Methods

pevalBitCastOrTerm :: Term (IntN n) -> Term (FP eb sb) -> Term (IntN n) Source #

sbvBitCastOr :: SBVType (IntN n) -> SBVType (FP eb sb) -> SBVType (IntN n) Source #

(n ~ (eb + sb), ValidFP eb sb, KnownNat n, 1 <= n) => PEvalBitCastOrTerm (FP eb sb) (WordN n) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalBitCastTerm

Methods

pevalBitCastOrTerm :: Term (WordN n) -> Term (FP eb sb) -> Term (WordN n) Source #

sbvBitCastOr :: SBVType (WordN n) -> SBVType (FP eb sb) -> SBVType (WordN n) Source #

ValidFP eb sb => GenSym (FP eb sb) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => FP eb sb -> m (Union (FP eb sb)) Source #

ValidFP eb sb => GenSymSimple (FP eb sb) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => FP eb sb -> m (FP eb sb) Source #

ValidFP eb sb => Solvable (FP eb sb) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

con :: FP eb sb -> SymFP eb sb Source #

conView :: SymFP eb sb -> Maybe (FP eb sb) Source #

sym :: Symbol -> SymFP eb sb Source #

ssym :: Identifier -> SymFP eb sb Source #

isym :: Identifier -> Int -> SymFP eb sb Source #

ValidFP eb sb => ToCon (FP eb sb) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: FP eb sb -> Maybe (FP eb sb) Source #

ValidFP eb sb => ToCon (SymFP eb sb) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: SymFP eb sb -> Maybe (FP eb sb) Source #

ValidFP eb sb => ToSym (FP eb sb) (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: FP eb sb -> FP eb sb Source #

ValidFP eb sb => ToSym (FP eb sb) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: FP eb sb -> SymFP eb sb Source #

ValidFP eb sb => LinkedRep (FP eb sb) (SymFP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

underlyingTerm :: SymFP eb sb -> Term (FP eb sb) Source #

wrapTerm :: Term (FP eb sb) -> SymFP eb sb Source #

(ValidFP eb sb, ValidFP eb' sb') => IEEEFPConvertible (FP eb' sb') (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fromFPOr :: FP eb' sb' -> FPRoundingMode -> FP eb sb -> FP eb' sb' Source #

toFP :: FPRoundingMode -> FP eb' sb' -> FP eb sb Source #

type FunType (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

type FunType (FP eb sb) = FP eb sb

type NonFuncSBVBaseType (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type NonFuncSBVBaseType (FP eb sb) = FloatingPoint eb sb

type PrimConstraint (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type PrimConstraint (FP eb sb) = ValidFP eb sb

type SBVType (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type SBVType (FP eb sb) = SBV (FloatingPoint eb sb)

type SymType (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

type SymType (FP eb sb) = SymFP eb sb

type ConType (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type ConType (FP eb sb) = FP eb sb

type SymType (FP eb sb) Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedRep

type SymType (FP eb sb) = SymFP eb sb

type FP16 = FP 5 11 Source #

IEEE 754 half-precision floating-point number.

type FP32 = FP 8 24 Source #

IEEE 754 single-precision floating-point number.

type FP64 = FP 11 53 Source #

IEEE 754 double-precision floating-point number.

withValidFPProofs :: forall (eb :: Nat) (sb :: Nat) r. ValidFP eb sb => ((KnownNat (eb + sb), BVIsNonZero (eb + sb), 1 <= (eb + sb), 1 <= eb, 1 <= sb) => r) -> r Source #

Some type-level witnesses that could be derived from ValidFP.

data FPRoundingMode Source #

Rounding mode for floating-point operations.

Constructors

RNE	Round to nearest, ties to even.
RNA	Round to nearest, ties to away from zero.
RTP	Round towards positive infinity.
RTN	Round towards negative infinity.
RTZ	Round towards zero.

Instances

Instances details

Arbitrary FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

arbitrary :: Gen FPRoundingMode #

shrink :: FPRoundingMode -> [FPRoundingMode] #

Serial FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

serialize :: MonadPut m => FPRoundingMode -> m () #

deserialize :: MonadGet m => m FPRoundingMode #

NFData FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

rnf :: FPRoundingMode -> () #

Generic FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Associated Types

type Rep FPRoundingMode

Instance details

Defined in Grisette.Internal.SymPrim.FP

type Rep FPRoundingMode = D1 ('MetaData "FPRoundingMode" "Grisette.Internal.SymPrim.FP" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) ((C1 ('MetaCons "RNE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RNA" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RTP" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RTN" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RTZ" 'PrefixI 'False) (U1 :: Type -> Type))))

Methods

from :: FPRoundingMode -> Rep FPRoundingMode x #

to :: Rep FPRoundingMode x -> FPRoundingMode #

Show FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

showsPrec :: Int -> FPRoundingMode -> ShowS #

show :: FPRoundingMode -> String #

showList :: [FPRoundingMode] -> ShowS #

Eq FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

(==) :: FPRoundingMode -> FPRoundingMode -> Bool #

(/=) :: FPRoundingMode -> FPRoundingMode -> Bool #

Ord FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

compare :: FPRoundingMode -> FPRoundingMode -> Ordering #

(<) :: FPRoundingMode -> FPRoundingMode -> Bool #

(<=) :: FPRoundingMode -> FPRoundingMode -> Bool #

(>) :: FPRoundingMode -> FPRoundingMode -> Bool #

(>=) :: FPRoundingMode -> FPRoundingMode -> Bool #

max :: FPRoundingMode -> FPRoundingMode -> FPRoundingMode #

min :: FPRoundingMode -> FPRoundingMode -> FPRoundingMode #

Apply FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Associated Types

type FunType FPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.FP type FunType FPRoundingMode = FPRoundingMode

Methods

apply :: FPRoundingMode -> FunType FPRoundingMode Source #

IEEEFPRoundingMode FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

rne :: FPRoundingMode Source #

rna :: FPRoundingMode Source #

rtp :: FPRoundingMode Source #

rtn :: FPRoundingMode Source #

rtz :: FPRoundingMode Source #

EvalSym FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> FPRoundingMode -> FPRoundingMode Source #

ExtractSym FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym

Methods

extractSym :: FPRoundingMode -> AnySymbolSet Source #

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => FPRoundingMode -> Maybe (SymbolSet knd) Source #

Mergeable FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy FPRoundingMode Source #

sortIndices :: FPRoundingMode -> [DynamicSortedIdx] Source #

PPrint FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint

Methods

pformat :: FPRoundingMode -> Doc ann Source #

pformatPrec :: Int -> FPRoundingMode -> Doc ann Source #

pformatList :: [FPRoundingMode] -> Doc ann Source #

SubstSym FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym

Methods

substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> FPRoundingMode -> FPRoundingMode Source #

SymEq FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq

Methods

(.==) :: FPRoundingMode -> FPRoundingMode -> SymBool Source #

(./=) :: FPRoundingMode -> FPRoundingMode -> SymBool Source #

symDistinct :: [FPRoundingMode] -> SymBool Source #

SymOrd FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd

Methods

(.<) :: FPRoundingMode -> FPRoundingMode -> SymBool Source #

(.<=) :: FPRoundingMode -> FPRoundingMode -> SymBool Source #

(.>) :: FPRoundingMode -> FPRoundingMode -> SymBool Source #

(.>=) :: FPRoundingMode -> FPRoundingMode -> SymBool Source #

symCompare :: FPRoundingMode -> FPRoundingMode -> Union Ordering Source #

AllSyms FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.SymPrim.AllSyms

Methods

allSymsS :: FPRoundingMode -> [SomeSym] -> [SomeSym] Source #

allSyms :: FPRoundingMode -> [SomeSym] Source #

NonFuncSBVRep FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type NonFuncSBVBaseType FPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type NonFuncSBVBaseType FPRoundingMode = RoundingMode

PEvalOrdTerm FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalOrdTerm

Methods

pevalLtOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool Source #

pevalLeOrdTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool Source #

withSbvOrdTermConstraint :: (OrdSymbolic (SBVType FPRoundingMode) => r) -> r Source #

sbvLtOrdTerm :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool Source #

sbvLeOrdTerm :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool Source #

SBVRep FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type SBVType FPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type SBVType FPRoundingMode = SBV RoundingMode

SupportedNonFuncPrim FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

conNonFuncSBVTerm :: FPRoundingMode -> SBV (NonFuncSBVBaseType FPRoundingMode) Source #

symNonFuncSBVTerm :: SBVFreshMonad m => String -> m (SBV (NonFuncSBVBaseType FPRoundingMode)) Source #

withNonFuncPrim :: (NonFuncPrimConstraint FPRoundingMode => r) -> r Source #

SupportedPrim FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Methods

primTypeRep :: TypeRep FPRoundingMode Source #

sameCon :: FPRoundingMode -> FPRoundingMode -> Bool Source #

hashConWithSalt :: Int -> FPRoundingMode -> Int Source #

pformatCon :: FPRoundingMode -> String Source #

defaultValue :: FPRoundingMode Source #

pevalITETerm :: Term Bool -> Term FPRoundingMode -> Term FPRoundingMode -> Term FPRoundingMode Source #

pevalEqTerm :: Term FPRoundingMode -> Term FPRoundingMode -> Term Bool Source #

pevalDistinctTerm :: NonEmpty (Term FPRoundingMode) -> Term Bool Source #

conSBVTerm :: FPRoundingMode -> SBVType FPRoundingMode Source #

symSBVName :: TypedSymbol 'AnyKind FPRoundingMode -> Int -> String Source #

symSBVTerm :: SBVFreshMonad m => String -> m (SBVType FPRoundingMode) Source #

withPrim :: ((PrimConstraint FPRoundingMode, SMTDefinable (SBVType FPRoundingMode), Mergeable (SBVType FPRoundingMode), Typeable (SBVType FPRoundingMode)) => a) -> a Source #

sbvIte :: SBV Bool -> SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBVType FPRoundingMode Source #

sbvEq :: SBVType FPRoundingMode -> SBVType FPRoundingMode -> SBV Bool Source #

sbvDistinct :: NonEmpty (SBVType FPRoundingMode) -> SBV Bool Source #

parseSMTModelResult :: Int -> ([([CV], CV)], CV) -> FPRoundingMode Source #

castTypedSymbol :: forall (knd' :: SymbolKind) (knd :: SymbolKind). IsSymbolKind knd' => TypedSymbol knd FPRoundingMode -> Maybe (TypedSymbol knd' FPRoundingMode) Source #

funcDummyConstraint :: SBVType FPRoundingMode -> SBV Bool Source #

SupportedPrimConstraint FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

Associated Types

type PrimConstraint FPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim type PrimConstraint FPRoundingMode = ()

SymRep FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Associated Types

type SymType FPRoundingMode
Instance details Defined in Grisette.Internal.SymPrim.SymFP type SymType FPRoundingMode = SymFPRoundingMode

Hashable FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

hashWithSalt :: Int -> FPRoundingMode -> Int #

hash :: FPRoundingMode -> Int #

GenSym FPRoundingMode FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.GenSym

Methods

fresh :: MonadFresh m => FPRoundingMode -> m (Union FPRoundingMode) Source #

GenSymSimple FPRoundingMode FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.GenSym

Methods

simpleFresh :: MonadFresh m => FPRoundingMode -> m FPRoundingMode Source #

Solvable FPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

con :: FPRoundingMode -> SymFPRoundingMode Source #

conView :: SymFPRoundingMode -> Maybe FPRoundingMode Source #

sym :: Symbol -> SymFPRoundingMode Source #

ssym :: Identifier -> SymFPRoundingMode Source #

isym :: Identifier -> Int -> SymFPRoundingMode Source #

ToCon FPRoundingMode FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: FPRoundingMode -> Maybe FPRoundingMode Source #

ToCon SymFPRoundingMode FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: SymFPRoundingMode -> Maybe FPRoundingMode Source #

ToSym FPRoundingMode FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: FPRoundingMode -> FPRoundingMode Source #

ToSym FPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: FPRoundingMode -> SymFPRoundingMode Source #

DecideEvalMode mode => UnifiedSymEq mode FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymEq

Methods

withBaseSymEq :: (If (IsConMode mode) (Eq FPRoundingMode) (SymEq FPRoundingMode) => r) -> r Source #

DecideEvalMode mode => UnifiedSymOrd mode FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.Class.UnifiedSymOrd

Methods

withBaseSymOrd :: (If (IsConMode mode) (Ord FPRoundingMode) (SymOrd FPRoundingMode) => r) -> r Source #

LinkedRep FPRoundingMode SymFPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

Methods

underlyingTerm :: SymFPRoundingMode -> Term FPRoundingMode Source #

wrapTerm :: Term FPRoundingMode -> SymFPRoundingMode Source #

Lift FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

lift :: Quote m => FPRoundingMode -> m Exp #

liftTyped :: forall (m :: Type -> Type). Quote m => FPRoundingMode -> Code m FPRoundingMode #

ValidFP eb sb => UnifiedFPImpl 'C FP eb sb (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP

Associated Types

type GetFP 'C
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP type GetFP 'C = FP
type GetFPRoundingMode 'C
Instance details Defined in Grisette.Internal.Internal.Impl.Unified.UnifiedFP type GetFPRoundingMode 'C = FPRoundingMode

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb) => UnifiedSafeFromFP mode NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb) => UnifiedSafeFromFP mode NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m AlgReal Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m Integer Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m (IntN n) Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m (WordN n) Source #

ValidFP eb sb => IEEEFPConvertible AlgReal (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fromFPOr :: AlgReal -> FPRoundingMode -> FP eb sb -> AlgReal Source #

toFP :: FPRoundingMode -> AlgReal -> FP eb sb Source #

ValidFP eb sb => IEEEFPConvertible Integer (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fromFPOr :: Integer -> FPRoundingMode -> FP eb sb -> Integer Source #

toFP :: FPRoundingMode -> Integer -> FP eb sb Source #

ValidFP eb sb => IEEEFPToAlgReal AlgReal (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fpToAlgReal :: AlgReal -> FP eb sb -> AlgReal Source #

(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (IntN n) (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fromFPOr :: IntN n -> FPRoundingMode -> FP eb sb -> IntN n Source #

toFP :: FPRoundingMode -> IntN n -> FP eb sb Source #

(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (WordN n) (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fromFPOr :: WordN n -> FPRoundingMode -> FP eb sb -> WordN n Source #

toFP :: FPRoundingMode -> WordN n -> FP eb sb Source #

ValidFP eb sb => IEEEFPRoundingOp (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fpAdd :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source #

fpSub :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source #

fpMul :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source #

fpDiv :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb Source #

fpFMA :: FPRoundingMode -> FP eb sb -> FP eb sb -> FP eb sb -> FP eb sb Source #

fpSqrt :: FPRoundingMode -> FP eb sb -> FP eb sb Source #

fpRoundToIntegral :: FPRoundingMode -> FP eb sb -> FP eb sb Source #

(ValidFP eb sb, ValidFP eb' sb') => IEEEFPConvertible (FP eb' sb') (FP eb sb) FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

fromFPOr :: FP eb' sb' -> FPRoundingMode -> FP eb sb -> FP eb' sb' Source #

toFP :: FPRoundingMode -> FP eb' sb' -> FP eb sb Source #

type Rep FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

type Rep FPRoundingMode = D1 ('MetaData "FPRoundingMode" "Grisette.Internal.SymPrim.FP" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) ((C1 ('MetaCons "RNE" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RNA" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "RTP" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "RTN" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RTZ" 'PrefixI 'False) (U1 :: Type -> Type))))

type FunType FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

type FunType FPRoundingMode = FPRoundingMode

type NonFuncSBVBaseType FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type NonFuncSBVBaseType FPRoundingMode = RoundingMode

type PrimConstraint FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type PrimConstraint FPRoundingMode = ()

type SBVType FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.Prim.Internal.Instances.SupportedPrim

type SBVType FPRoundingMode = SBV RoundingMode

type SymType FPRoundingMode Source #

Instance details

Defined in Grisette.Internal.SymPrim.SymFP

type SymType FPRoundingMode = SymFPRoundingMode

allFPRoundingMode :: [FPRoundingMode] Source #

All IEEE 754 rounding modes.

data NotRepresentableFPError Source #

An error thrown when bitcasting or converting FP NaN to other types.

Constructors

NaNError
FPUnderflowError
FPOverflowError

Instances

Instances details

Exception NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

toException :: NotRepresentableFPError -> SomeException #

fromException :: SomeException -> Maybe NotRepresentableFPError #

displayException :: NotRepresentableFPError -> String #

backtraceDesired :: NotRepresentableFPError -> Bool #

Generic NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Associated Types

type Rep NotRepresentableFPError

Instance details

Defined in Grisette.Internal.SymPrim.FP

type Rep NotRepresentableFPError = D1 ('MetaData "NotRepresentableFPError" "Grisette.Internal.SymPrim.FP" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "NaNError" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPUnderflowError" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPOverflowError" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: NotRepresentableFPError -> Rep NotRepresentableFPError x #

to :: Rep NotRepresentableFPError x -> NotRepresentableFPError #

Show NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

showsPrec :: Int -> NotRepresentableFPError -> ShowS #

show :: NotRepresentableFPError -> String #

showList :: [NotRepresentableFPError] -> ShowS #

Eq NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

Methods

(==) :: NotRepresentableFPError -> NotRepresentableFPError -> Bool #

(/=) :: NotRepresentableFPError -> NotRepresentableFPError -> Bool #

Ord NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

EvalSym NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.EvalSym

Methods

evalSym :: Bool -> Model -> NotRepresentableFPError -> NotRepresentableFPError Source #

ExtractSym NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ExtractSym

Methods

extractSym :: NotRepresentableFPError -> AnySymbolSet Source #

extractSymMaybe :: forall (knd :: SymbolKind). IsSymbolKind knd => NotRepresentableFPError -> Maybe (SymbolSet knd) Source #

Mergeable NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.Mergeable

Methods

rootStrategy :: MergingStrategy NotRepresentableFPError Source #

sortIndices :: NotRepresentableFPError -> [DynamicSortedIdx] Source #

PPrint NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.PPrint

Methods

pformat :: NotRepresentableFPError -> Doc ann Source #

pformatPrec :: Int -> NotRepresentableFPError -> Doc ann Source #

pformatList :: [NotRepresentableFPError] -> Doc ann Source #

SubstSym NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SubstSym

Methods

substSym :: forall cb sb (knd :: SymbolKind). (LinkedRep cb sb, IsSymbolKind knd) => TypedSymbol knd cb -> sb -> NotRepresentableFPError -> NotRepresentableFPError Source #

SymEq NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymEq

Methods

(.==) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source #

(./=) :: NotRepresentableFPError -> NotRepresentableFPError -> SymBool Source #

symDistinct :: [NotRepresentableFPError] -> SymBool Source #

SymOrd NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.SymOrd

ToCon NotRepresentableFPError NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: NotRepresentableFPError -> Maybe NotRepresentableFPError Source #

ToSym NotRepresentableFPError NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: NotRepresentableFPError -> NotRepresentableFPError Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP16 Int16 m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP16 -> m Int16 Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP16 Word16 m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP16 -> m Word16 Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP32 Int32 m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP32 -> m Int32 Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP32 Word32 m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP32 -> m Word32 Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP32 Float m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP32 -> m Float Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP64 Int64 m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP64 -> m Int64 Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP64 Word64 m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP64 -> m Word64 Source #

(MonadError NotRepresentableFPError m, TryMerge m) => SafeBitCast NotRepresentableFPError FP64 Double m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP64 -> m Double Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb) => UnifiedSafeFromFP 'S NotRepresentableFPError SymAlgReal (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError SymAlgReal (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb) => UnifiedSafeFromFP 'S NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb) => UnifiedSafeFromFP mode NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb) => UnifiedSafeFromFP mode NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP 'S NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP 'S NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n) => UnifiedSafeFromFP mode NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeFromFP

Methods

withBaseSafeFromFP :: (SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m => r) -> r Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError AlgReal (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m AlgReal Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError SymAlgReal (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m SymAlgReal Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError SymInteger (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m SymInteger Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb) => SafeFromFP NotRepresentableFPError Integer (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m Integer Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast 'S NotRepresentableFPError (SymFP eb sb) (SymIntN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymIntN n) m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching 'S m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast 'S NotRepresentableFPError (SymFP eb sb) (SymWordN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymWordN n) m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast mode NotRepresentableFPError (FP eb sb) (IntN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (FP eb sb) (IntN n) m => r) -> r Source #

(MonadError NotRepresentableFPError m, UnifiedBranching mode m, ValidFP eb sb, KnownNat n, 1 <= n, n ~ (eb + sb)) => UnifiedSafeBitCast mode NotRepresentableFPError (FP eb sb) (WordN n) m Source #

Instance details

Defined in Grisette.Internal.Unified.Class.UnifiedSafeBitCast

Methods

withBaseSafeBitCast :: (SafeBitCast NotRepresentableFPError (FP eb sb) (WordN n) m => r) -> r Source #

ToSym NotRepresentableFPError (Union NotRepresentableFPError) Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToSym

Methods

toSym :: NotRepresentableFPError -> Union NotRepresentableFPError Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (IntN n) (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m (IntN n) Source #

(MonadError NotRepresentableFPError m, TryMerge m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (WordN n) (FP eb sb) FPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: FPRoundingMode -> FP eb sb -> m (WordN n) Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (SymIntN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymIntN n) Source #

(MonadError NotRepresentableFPError m, MonadUnion m, ValidFP eb sb, KnownNat n, 1 <= n) => SafeFromFP NotRepresentableFPError (SymWordN n) (SymFP eb sb) SymFPRoundingMode m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeFromFP

Methods

safeFromFP :: SymFPRoundingMode -> SymFP eb sb -> m (SymWordN n) Source #

(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, TryMerge m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (FP eb sb) (IntN r) m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP eb sb -> m (IntN r) Source #

(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, TryMerge m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (FP eb sb) (WordN r) m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: FP eb sb -> m (WordN r) Source #

(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, MonadUnion m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymIntN r) m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: SymFP eb sb -> m (SymIntN r) Source #

(ValidFP eb sb, r ~ (eb + sb), KnownNat r, 1 <= r, MonadUnion m, MonadError NotRepresentableFPError m) => SafeBitCast NotRepresentableFPError (SymFP eb sb) (SymWordN r) m Source #

Instance details

Defined in Grisette.Internal.Core.Data.Class.SafeBitCast

Methods

safeBitCast :: SymFP eb sb -> m (SymWordN r) Source #

ToCon (Union NotRepresentableFPError) NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.Internal.Impl.Core.Data.Class.ToCon

Methods

toCon :: Union NotRepresentableFPError -> Maybe NotRepresentableFPError Source #

type Rep NotRepresentableFPError Source #

Instance details

Defined in Grisette.Internal.SymPrim.FP

type Rep NotRepresentableFPError = D1 ('MetaData "NotRepresentableFPError" "Grisette.Internal.SymPrim.FP" "grisette-0.11.0.0-HndeEPlDvvDHSETLw6O8c" 'False) (C1 ('MetaCons "NaNError" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "FPUnderflowError" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "FPOverflowError" 'PrefixI 'False) (U1 :: Type -> Type)))

class ConvertibleBound (bv :: Nat -> Type) where Source #

Bounds for converting bit vectors to floating-point numbers. Out-of-range FP values cannot be converted to a representable bit-vector.

Methods

convertibleLowerBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => bv n -> FPRoundingMode -> FP eb sb Source #

convertibleUpperBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => bv n -> FPRoundingMode -> FP eb sb Source #

Instances

Instances details

ConvertibleBound IntN Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods convertibleLowerBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => IntN n -> FPRoundingMode -> FP eb sb Source # convertibleUpperBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => IntN n -> FPRoundingMode -> FP eb sb Source #
ConvertibleBound WordN Source #
Instance details Defined in Grisette.Internal.SymPrim.FP Methods convertibleLowerBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => WordN n -> FPRoundingMode -> FP eb sb Source # convertibleUpperBound :: forall (eb :: Nat) (sb :: Nat) (n :: Nat). (ValidFP eb sb, KnownNat n, 1 <= n) => WordN n -> FPRoundingMode -> FP eb sb Source #

nextFP :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FP eb sb -> FP eb sb Source #

Next representable floating-point number.

Note:

nextFP(+inf) = +inf
nextFP(-inf) = -maxNormalized
nextFP(NaN) = NaN

The function do not distinguish between -0 and +0.

prevFP :: forall (eb :: Nat) (sb :: Nat). ValidFP eb sb => FP eb sb -> FP eb sb Source #

Previous representable floating-point number.

Note:

prevFP(+inf) = +maxNormalized
prevFP(-inf) = -inf
prevFP(NaN) = NaN

The function do not distinguish between -0 and +0.

withUnsafeValidFP :: forall (eb :: Nat) (sb :: Nat) r. (KnownNat eb, KnownNat sb) => (ValidFP eb sb => r) -> r Source #

Provide an (unsafe) type-level proof that the given floating-point type is valid.

checkDynamicValidFP :: Natural -> Natural -> Bool Source #

Check if the given floating-point type is valid.

invalidFPMessage :: String Source #

A message thrown when the floating-point type is invalid.