cryptol-2.9.0: Cryptol: The Language of Cryptography

Safe HaskellNone
LanguageHaskell2010

Cryptol.Eval.What4.SFloat

Contents

Description

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

Synopsis

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 #

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 #

Arithmetic

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

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

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.

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