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.Core.Data.Class.IEEEFP

Description

Synopsis

fpIsNaN :: RealFloat a => a -> Bool
fpIsPositiveZero :: RealFloat a => a -> Bool
fpIsNegativeZero :: RealFloat a => a -> Bool
fpIsPositiveInfinite :: RealFloat a => a -> Bool
fpIsNegativeInfinite :: RealFloat a => a -> Bool
fpIsPositive :: RealFloat a => a -> Bool
fpIsNegative :: RealFloat a => a -> Bool
fpIsInfinite :: RealFloat a => a -> Bool
fpIsZero :: RealFloat a => a -> Bool
fpIsNormal :: RealFloat a => a -> Bool
fpIsSubnormal :: RealFloat a => a -> Bool
fpIsPoint :: RealFloat a => a -> Bool
class IEEEFPConstants a where
- fpPositiveInfinite :: a
- fpNegativeInfinite :: a
- fpNaN :: a
- fpNegativeZero :: a
- fpPositiveZero :: a
- fpMinNormalized :: a
- fpMinSubnormal :: a
- fpMaxNormalized :: a
- fpMaxSubnormal :: a
class IEEEFPRoundingMode mode where
- rne :: mode
- rna :: mode
- rtp :: mode
- rtn :: mode
- rtz :: mode
class IEEEFPOp a where
- fpAbs :: a -> a
- fpNeg :: a -> a
- fpRem :: a -> a -> a
- fpMinimum :: a -> a -> a
- fpMinimumNumber :: a -> a -> a
- fpMaximum :: a -> a -> a
- fpMaximumNumber :: a -> a -> a
class IEEEFPRoundingMode mode => IEEEFPRoundingOp a mode | a -> mode where
- fpAdd :: mode -> a -> a -> a
- fpSub :: mode -> a -> a -> a
- fpMul :: mode -> a -> a -> a
- fpDiv :: mode -> a -> a -> a
- fpFMA :: mode -> a -> a -> a -> a
- fpSqrt :: mode -> a -> a
- fpRoundToIntegral :: mode -> a -> a
class IEEEFPConvertible a fp mode | fp -> mode where
- fromFPOr :: a -> mode -> fp -> a
- toFP :: mode -> a -> fp
class (IEEEFPConvertible a fp mode, IEEEFPRoundingMode mode) => IEEEFPToAlgReal a fp mode | fp -> mode where
- fpToAlgReal :: a -> fp -> a

Documentation

fpIsNaN :: RealFloat a => a -> Bool Source #

Check if a floating-point number is not-a-number.

fpIsPositiveZero :: RealFloat a => a -> Bool Source #

Check if a floating-point number is positive zero.

fpIsNegativeZero :: RealFloat a => a -> Bool Source #

Check if a floating-point number is negative zero.

fpIsPositiveInfinite :: RealFloat a => a -> Bool Source #

Check if a floating-point number is positive infinite.

fpIsNegativeInfinite :: RealFloat a => a -> Bool Source #

Check if a floating-point number is negative infinite.

fpIsPositive :: RealFloat a => a -> Bool Source #

Check if a floating-point number is positive. +0, +inf are considered positive. nan, -0, -inf are not positive.

fpIsNegative :: RealFloat a => a -> Bool Source #

Check if a floating-point number is negative. -0, -inf are considered negative. nan, +0, +inf are not negative.

fpIsInfinite :: RealFloat a => a -> Bool Source #

Check if a floating-point number is infinite.

fpIsZero :: RealFloat a => a -> Bool Source #

Check if a floating-point number is zero.

fpIsNormal :: RealFloat a => a -> Bool Source #

Check if a floating-point number is normal, i.e., not 0, not inf, not nan, and not denormalized.

fpIsSubnormal :: RealFloat a => a -> Bool Source #

Check if a floating-point number is subnormal, i.e., denormalized. 0, inf, or nan are not subnormal.

fpIsPoint :: RealFloat a => a -> Bool Source #

Check if a floating-point number is a point, i.e., not inf, not nan.

class IEEEFPConstants a where Source #

Constants for IEEE floating-point numbers.

Methods

fpPositiveInfinite :: a Source #

Positive infinity.

fpNegativeInfinite :: a Source #

Negative infinity.

fpNaN :: a Source #

Not-a-number.

fpNegativeZero :: a Source #

Negative zero.

fpPositiveZero :: a Source #

Positive zero.

fpMinNormalized :: a Source #

Smallest positive normalized number.

fpMinSubnormal :: a Source #

Smallest positive subnormal number.

fpMaxNormalized :: a Source #

Largest positive normalized number.

fpMaxSubnormal :: a Source #

Largest positive subnormal number.

Instances

Instances details

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 => IEEEFPConstants (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods fpPositiveInfinite :: SymFP eb sb Source # fpNegativeInfinite :: SymFP eb sb Source # fpNaN :: SymFP eb sb Source # fpNegativeZero :: SymFP eb sb Source # fpPositiveZero :: SymFP eb sb Source # fpMinNormalized :: SymFP eb sb Source # fpMinSubnormal :: SymFP eb sb Source # fpMaxNormalized :: SymFP eb sb Source # fpMaxSubnormal :: SymFP eb sb Source #

class IEEEFPRoundingMode mode where Source #

Rounding modes for floating-point operations.

Methods

rne :: mode Source #

Round to nearest, ties to even.

rna :: mode Source #

Round to nearest, ties to away from zero.

rtp :: mode Source #

Round towards positive infinity.

rtn :: mode Source #

Round towards negative infinity.

rtz :: mode Source #

Round towards zero.

Instances

Instances details

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 #
IEEEFPRoundingMode SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods rne :: SymFPRoundingMode Source # rna :: SymFPRoundingMode Source # rtp :: SymFPRoundingMode Source # rtn :: SymFPRoundingMode Source # rtz :: SymFPRoundingMode Source #

class IEEEFPOp a where Source #

Operations on IEEE floating-point numbers, without rounding mode.

Methods

fpAbs :: a -> a Source #

IEEE754-2019 abs operation.

fpNeg :: a -> a Source #

IEEE754-2019 negate operation.

fpRem :: a -> a -> a Source #

IEEE754-2019 remainder operation.

fpMinimum :: a -> a -> a Source #

IEEE754-2019 minimum operation.

The comparison for zeros follows -0 < 0
Returns NaN if one operand is NaN.

fpMinimumNumber :: a -> a -> a Source #

IEEE754-2019 minimumNumber operation.

The comparison for zeros follows -0 < 0
Returns the other operand if one operand is NaN.

fpMaximum :: a -> a -> a Source #

IEEE754-2019 maximum operation.

The comparison for zeros follows -0 < 0
Returns NaN if one operand is NaN.

fpMaximumNumber :: a -> a -> a Source #

IEEE754-2019 maximumNumber operation.

The comparison for zeros follows -0 < 0
Returns the other operand if one operand is NaN.

Instances

Instances details

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 => IEEEFPOp (SymFP eb sb) Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods fpAbs :: SymFP eb sb -> SymFP eb sb Source # fpNeg :: SymFP eb sb -> SymFP eb sb Source # fpRem :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # fpMinimum :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # fpMinimumNumber :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # fpMaximum :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # fpMaximumNumber :: SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source #

class IEEEFPRoundingMode mode => IEEEFPRoundingOp a mode | a -> mode where Source #

Operations on IEEE floating-point numbers, with rounding mode.

Methods

fpAdd :: mode -> a -> a -> a Source #

fpSub :: mode -> a -> a -> a Source #

fpMul :: mode -> a -> a -> a Source #

fpDiv :: mode -> a -> a -> a Source #

fpFMA :: mode -> a -> a -> a -> a Source #

fpSqrt :: mode -> a -> a Source #

fpRoundToIntegral :: mode -> a -> a Source #

Instances

Instances details

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 => IEEEFPRoundingOp (SymFP eb sb) SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods fpAdd :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # fpSub :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # fpMul :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # fpDiv :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # fpFMA :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb -> SymFP eb sb Source # fpSqrt :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb Source # fpRoundToIntegral :: SymFPRoundingMode -> SymFP eb sb -> SymFP eb sb Source #

class IEEEFPConvertible a fp mode | fp -> mode where Source #

Conversion from and to FPs.

Methods

fromFPOr Source #

Arguments

:: a	Default value when converting non-representable FPs. For example, when converting to non-FP types, the NaN and infinities are not representable. Additionally, when converting to bit-vectors, out-of-bound FPs are not representable. Note that out-of-bound means that the value after conversion is out of bound, not the value before conversion, meaning that converting from 3.5 to 2-bit unsigned bit-vector is out-of-bound when rounding to positive, but not when rounding to negative.
-> mode	Rounding mode. Ignored when converting to `AlgReal` because every representable FP value is converted to an exact `AlgReal`.
-> fp	FP value.
-> a

toFP :: mode -> a -> fp Source #

Instances

Instances details

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 SymAlgReal (SymFP eb sb) SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods fromFPOr :: SymAlgReal -> SymFPRoundingMode -> SymFP eb sb -> SymAlgReal Source # toFP :: SymFPRoundingMode -> SymAlgReal -> SymFP eb sb Source #
ValidFP eb sb => IEEEFPConvertible SymInteger (SymFP eb sb) SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods fromFPOr :: SymInteger -> SymFPRoundingMode -> SymFP eb sb -> SymInteger Source # toFP :: SymFPRoundingMode -> SymInteger -> SymFP 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, 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, KnownNat n, 1 <= n) => IEEEFPConvertible (SymIntN n) (SymFP eb sb) SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods fromFPOr :: SymIntN n -> SymFPRoundingMode -> SymFP eb sb -> SymIntN n Source # toFP :: SymFPRoundingMode -> SymIntN n -> SymFP eb sb Source #
(ValidFP eb sb, KnownNat n, 1 <= n) => IEEEFPConvertible (SymWordN n) (SymFP eb sb) SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods fromFPOr :: SymWordN n -> SymFPRoundingMode -> SymFP eb sb -> SymWordN n Source # toFP :: SymFPRoundingMode -> SymWordN n -> 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 #
(ValidFP eb sb, ValidFP eb' sb') => IEEEFPConvertible (SymFP eb' sb') (SymFP eb sb) SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods fromFPOr :: SymFP eb' sb' -> SymFPRoundingMode -> SymFP eb sb -> SymFP eb' sb' Source # toFP :: SymFPRoundingMode -> SymFP eb' sb' -> SymFP eb sb Source #

class (IEEEFPConvertible a fp mode, IEEEFPRoundingMode mode) => IEEEFPToAlgReal a fp mode | fp -> mode where Source #

Converting FP to real numbers.

Minimal complete definition

Nothing

Methods

fpToAlgReal :: a -> fp -> a Source #

Similar to fromFPOr for AlgReal, but dropped the ignored rounding mode.

Instances

Instances details

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 => IEEEFPToAlgReal SymAlgReal (SymFP eb sb) SymFPRoundingMode Source #
Instance details Defined in Grisette.Internal.SymPrim.SymFP Methods fpToAlgReal :: SymAlgReal -> SymFP eb sb -> SymAlgReal Source #