Safe Haskell	None
Language	Haskell2010

What4.SFloat

Contents

Interface
Constants
Interchange formats
Relations
Arithmetic
Conversions
Queries
Exceptions

Description

Working with floats of dynamic sizes.

Synopsis

data SFloat sym where
- SFloat :: IsExpr (SymExpr sym) => SymFloat sym fpp -> SFloat sym
fpReprOf :: IsExpr (SymExpr sym) => sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp
fpSize :: SFloat sym -> (Integer, Integer)
fpRepr :: Integer -> Integer -> Maybe (Some FloatPrecisionRepr)
fpAsLit :: SFloat sym -> Maybe BigFloat
fpIte :: IsExprBuilder sym => sym -> Pred sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpFresh :: IsSymExprBuilder sym => sym -> Integer -> Integer -> IO (SFloat sym)
fpNaN :: IsExprBuilder sym => sym -> Integer -> Integer -> IO (SFloat sym)
fpPosInf :: IsExprBuilder sym => sym -> Integer -> Integer -> IO (SFloat sym)
fpNegInf :: IsExprBuilder sym => sym -> Integer -> Integer -> IO (SFloat sym)
fpFromLit :: IsExprBuilder sym => sym -> Integer -> Integer -> BigFloat -> IO (SFloat sym)
fpFromRationalLit :: IsExprBuilder sym => sym -> Integer -> Integer -> Rational -> IO (SFloat sym)
fpFromBinary :: IsExprBuilder sym => sym -> Integer -> Integer -> SWord sym -> IO (SFloat sym)
fpToBinary :: IsExprBuilder sym => sym -> SFloat sym -> IO (SWord sym)
type SFloatRel sym = sym -> SFloat sym -> SFloat sym -> IO (Pred sym)
fpEq :: IsExprBuilder sym => SFloatRel sym
fpEqIEEE :: IsExprBuilder sym => SFloatRel sym
fpLtIEEE :: IsExprBuilder sym => SFloatRel sym
fpGtIEEE :: IsExprBuilder sym => SFloatRel sym
type SFloatBinArith sym = sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym)
fpAbs :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym)
fpSqrt :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
fpAdd :: IsExprBuilder sym => SFloatBinArith sym
fpSub :: IsExprBuilder sym => SFloatBinArith sym
fpMul :: IsExprBuilder sym => SFloatBinArith sym
fpDiv :: IsExprBuilder sym => SFloatBinArith sym
fpMin :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpMax :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpFMA :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> SFloat sym -> SFloat sym -> IO (SFloat sym)
fpRound :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym)
fpToReal :: IsExprBuilder sym => sym -> SFloat sym -> IO (SymReal sym)
fpFromReal :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SymReal sym -> IO (SFloat sym)
fpFromRational :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> SymInteger sym -> IO (SFloat sym)
fpToRational :: IsSymExprBuilder sym => sym -> SFloat sym -> IO (Pred sym, SymInteger sym, SymInteger sym)
fpFromInteger :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> IO (SFloat sym)
fpIsInf :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsNaN :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsZero :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsSubnorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
fpIsNorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym)
data UnsupportedFloat = UnsupportedFloat {
- fpWho :: String
- exponentBits, precisionBits :: Integer
}
data FPTypeError = FPTypeError {
- fpExpected :: Some BaseTypeRepr
- fpActual :: Some BaseTypeRepr
}

Interface

data SFloat sym where Source #

Symbolic floating point numbers.

Constructors

SFloat :: IsExpr (SymExpr sym) => SymFloat sym fpp -> SFloat sym

fpReprOf :: IsExpr (SymExpr sym) => sym -> SymFloat sym fpp -> FloatPrecisionRepr fpp Source #

fpSize :: SFloat sym -> (Integer, Integer) Source #

fpRepr Source #

Arguments

:: Integer	Exponent width
-> Integer	Precision width
-> Maybe (Some FloatPrecisionRepr)

Construct the FloatPrecisionRepr with the given parameters.

fpAsLit :: SFloat sym -> Maybe BigFloat Source #

fpIte :: IsExprBuilder sym => sym -> Pred sym -> SFloat sym -> SFloat sym -> IO (SFloat sym) Source #

Constants

fpFresh :: IsSymExprBuilder sym => sym -> Integer -> Integer -> IO (SFloat sym) Source #

A fresh variable of the given type.

fpNaN Source #

Arguments

:: IsExprBuilder sym
=> sym
-> Integer	Exponent width
-> Integer	Precision width
-> IO (SFloat sym)

Not a number

fpPosInf Source #

Arguments

:: IsExprBuilder sym
=> sym
-> Integer	Exponent width
-> Integer	Precision width
-> IO (SFloat sym)

Positive infinity

fpNegInf Source #

Arguments

:: IsExprBuilder sym
=> sym
-> Integer	Exponent width
-> Integer	Precision width
-> IO (SFloat sym)

Negative infinity

fpFromLit Source #

Arguments

:: IsExprBuilder sym
=> sym
-> Integer	Exponent width
-> Integer	Precision width
-> BigFloat
-> IO (SFloat sym)

A floating point number corresponding to the given BigFloat.

fpFromRationalLit Source #

Arguments

:: IsExprBuilder sym
=> sym
-> Integer	Exponent width
-> Integer	Precision width
-> Rational
-> IO (SFloat sym)

A floating point number corresponding to the given rational.

Interchange formats

fpFromBinary Source #

Arguments

:: IsExprBuilder sym
=> sym
-> Integer	Exponent width
-> Integer	Precision width
-> SWord sym
-> IO (SFloat sym)

Make a floating point number with the given bit representation.

fpToBinary :: IsExprBuilder sym => sym -> SFloat sym -> IO (SWord sym) Source #

Relations

type SFloatRel sym = sym -> SFloat sym -> SFloat sym -> IO (Pred sym) Source #

fpEq :: IsExprBuilder sym => SFloatRel sym Source #

fpEqIEEE :: IsExprBuilder sym => SFloatRel sym Source #

fpLtIEEE :: IsExprBuilder sym => SFloatRel sym Source #

fpGtIEEE :: IsExprBuilder sym => SFloatRel sym Source #

Arithmetic

type SFloatBinArith sym = sym -> RoundingMode -> SFloat sym -> SFloat sym -> IO (SFloat sym) Source #

fpNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym) Source #

fpAbs :: IsExprBuilder sym => sym -> SFloat sym -> IO (SFloat sym) Source #

fpSqrt :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym) Source #

fpAdd :: IsExprBuilder sym => SFloatBinArith sym Source #

fpSub :: IsExprBuilder sym => SFloatBinArith sym Source #

fpMul :: IsExprBuilder sym => SFloatBinArith sym Source #

fpDiv :: IsExprBuilder sym => SFloatBinArith sym Source #

fpMin :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym) Source #

fpMax :: IsExprBuilder sym => sym -> SFloat sym -> SFloat sym -> IO (SFloat sym) Source #

fpFMA :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> SFloat sym -> SFloat sym -> IO (SFloat sym) Source #

Conversions

fpRound :: IsExprBuilder sym => sym -> RoundingMode -> SFloat sym -> IO (SFloat sym) Source #

fpToReal :: IsExprBuilder sym => sym -> SFloat sym -> IO (SymReal sym) Source #

This is undefined on "special" values (NaN,infinity)

fpFromReal :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SymReal sym -> IO (SFloat sym) Source #

fpFromRational :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> SymInteger sym -> IO (SFloat sym) Source #

fpToRational :: IsSymExprBuilder sym => sym -> SFloat sym -> IO (Pred sym, SymInteger sym, SymInteger sym) Source #

Returns a predicate and two integers, x and y. If the the predicate holds, then x / y is a rational representing the floating point number. Assumes the FP number is not one of the special ones that has no real representation.

fpFromInteger :: IsExprBuilder sym => sym -> Integer -> Integer -> RoundingMode -> SymInteger sym -> IO (SFloat sym) Source #

Queries

fpIsInf :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) Source #

fpIsNaN :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) Source #

fpIsZero :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) Source #

fpIsNeg :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) Source #

fpIsSubnorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) Source #

fpIsNorm :: IsExprBuilder sym => sym -> SFloat sym -> IO (Pred sym) Source #

Exceptions

data UnsupportedFloat Source #

This exception is thrown if the operations try to create a floating point value we do not support

Constructors

UnsupportedFloat
Fields fpWho :: String exponentBits, precisionBits :: Integer

Instances

Instances details

Show UnsupportedFloat Source #
Instance details Defined in What4.SFloat Methods showsPrec :: Int -> UnsupportedFloat -> ShowS # show :: UnsupportedFloat -> String # showList :: [UnsupportedFloat] -> ShowS #
Exception UnsupportedFloat Source #
Instance details Defined in What4.SFloat Methods toException :: UnsupportedFloat -> SomeException # fromException :: SomeException -> Maybe UnsupportedFloat # displayException :: UnsupportedFloat -> String #

data FPTypeError Source #

This exceptoin is throws if the types don't match.

Constructors

FPTypeError
Fields fpExpected :: Some BaseTypeRepr fpActual :: Some BaseTypeRepr

Instances

Instances details

Show FPTypeError Source #
Instance details Defined in What4.SFloat Methods showsPrec :: Int -> FPTypeError -> ShowS # show :: FPTypeError -> String # showList :: [FPTypeError] -> ShowS #
Exception FPTypeError Source #
Instance details Defined in What4.SFloat Methods toException :: FPTypeError -> SomeException # fromException :: SomeException -> Maybe FPTypeError # displayException :: FPTypeError -> String #