Safe Haskell	None
Language	Haskell2010

Cryptol.Backend.What4.SFloat

Contents

Interface
Constants
Interchange formats
Relations
Arithmetic
Conversions
Queries
Exceptions

Description

Working with floats of dynamic sizes. This should probably be moved to What4 one day.

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)
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)
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)
fpAdd :: IsExprBuilder sym => SFloatBinArith sym
fpSub :: IsExprBuilder sym => SFloatBinArith sym
fpMul :: IsExprBuilder sym => SFloatBinArith sym
fpDiv :: IsExprBuilder sym => SFloatBinArith 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)
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.

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

fpFromRationalLit Source #

Arguments

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

A floating point number corresponding to the given rations.

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 #

fpAdd :: IsExprBuilder sym => SFloatBinArith sym Source #

fpSub :: IsExprBuilder sym => SFloatBinArith sym Source #

fpMul :: IsExprBuilder sym => SFloatBinArith sym Source #

fpDiv :: IsExprBuilder sym => SFloatBinArith 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 #

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 Cryptol.Backend.What4.SFloat Methods showsPrec :: Int -> UnsupportedFloat -> ShowS # show :: UnsupportedFloat -> String # showList :: [UnsupportedFloat] -> ShowS #
Exception UnsupportedFloat Source #
Instance details Defined in Cryptol.Backend.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 Cryptol.Backend.What4.SFloat Methods showsPrec :: Int -> FPTypeError -> ShowS # show :: FPTypeError -> String # showList :: [FPTypeError] -> ShowS #
Exception FPTypeError Source #
Instance details Defined in Cryptol.Backend.What4.SFloat Methods toException :: FPTypeError -> SomeException # fromException :: SomeException -> Maybe FPTypeError # displayException :: FPTypeError -> String #