mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-11 14:06:13 +03:00
0909120a68
Expose some additional primitives, such as FMA, abs, sqrt, and more classification predicates. Refactor the primitives table for floating-point values into a single generic table that uses methods from the `Backend` class.
229 lines
6.5 KiB
Plaintext
229 lines
6.5 KiB
Plaintext
module Float where
|
|
|
|
primitive type ValidFloat : # -> # -> Prop
|
|
|
|
/** IEEE-754 floating point numbers. */
|
|
primitive type { exponent : #, precision : #}
|
|
ValidFloat exponent precision => Float exponent precision : *
|
|
|
|
/** An abbreviation for common 16-bit floating point numbers. */
|
|
type Float16 = Float 5 11
|
|
|
|
/** An abbreviation for common 32-bit floating point numbers. */
|
|
type Float32 = Float 8 24
|
|
|
|
/** An abbreviation for common 64-bit floating point numbers. */
|
|
type Float64 = Float 11 53
|
|
|
|
/** An abbreviation for common 128-bit floating point numbers. */
|
|
type Float128 = Float 15 113
|
|
|
|
/** An abbreviation for common 256-bit floating point numbers. */
|
|
type Float256 = Float 19 237
|
|
|
|
|
|
|
|
/* ----------------------------------------------------------------------
|
|
* Rounding modes (this should be an enumeration type, when we add these)
|
|
*---------------------------------------------------------------------- */
|
|
|
|
/**
|
|
* A 'RoundingMode' is used to specify the precise behavior of some
|
|
* floating point primitives.
|
|
*
|
|
* There are five valid 'RoundingMode' values:
|
|
* * roundNearestEven
|
|
* * roundNearestAway
|
|
* * roundPositive
|
|
* * roundNegative
|
|
* * roundZero
|
|
*/
|
|
type RoundingMode = [3]
|
|
|
|
/** Round toward nearest, ties go to even. */
|
|
roundNearestEven, rne : RoundingMode
|
|
roundNearestEven = 0
|
|
rne = roundNearestEven
|
|
|
|
/** Round toward nearest, ties away from zero. */
|
|
roundNearestAway, rna : RoundingMode
|
|
roundNearestAway = 1
|
|
rna = roundNearestAway
|
|
|
|
/** Round toward positive infinity. */
|
|
roundPositive, rtp : RoundingMode
|
|
roundPositive = 2
|
|
rtp = roundPositive
|
|
|
|
/** Round toward negative infinity. */
|
|
roundNegative, rtn : RoundingMode
|
|
roundNegative = 3
|
|
rtn = roundNegative
|
|
|
|
/** Round toward zero. */
|
|
roundZero, rtz : RoundingMode
|
|
roundZero = 4
|
|
rtz = roundZero
|
|
|
|
|
|
|
|
/* ----------------------------------------------------------------------
|
|
* Constants
|
|
* ---------------------------------------------------------------------- */
|
|
|
|
/** Not a number. */
|
|
primitive
|
|
fpNaN : {e,p} ValidFloat e p => Float e p
|
|
|
|
/** Positive infinity. */
|
|
primitive
|
|
fpPosInf : {e,p} ValidFloat e p => Float e p
|
|
|
|
/** Negative infinity. */
|
|
fpNegInf : {e,p} ValidFloat e p => Float e p
|
|
fpNegInf = - fpPosInf
|
|
|
|
/** Positive zero. */
|
|
fpPosZero : {e,p} ValidFloat e p => Float e p
|
|
fpPosZero = zero
|
|
|
|
/** Negative zero. */
|
|
fpNegZero : {e,p} ValidFloat e p => Float e p
|
|
fpNegZero = - fpPosZero
|
|
|
|
|
|
// Binary representations
|
|
|
|
/** A floating point number using the exact bit pattern,
|
|
in IEEE interchange format with layout:
|
|
|
|
(sign : [1]) # (biased_exponent : [e]) # (significand : [p-1])
|
|
*/
|
|
primitive
|
|
fpFromBits : {e,p} ValidFloat e p => [e + p] -> Float e p
|
|
|
|
/** Export a floating point number in IEEE interchange format with layout:
|
|
|
|
(sign : [1]) # (biased_exponent : [e]) # (significand : [p-1])
|
|
|
|
NaN is represented as:
|
|
* positive: sign == 0
|
|
* quiet with no info: significand == 0b1 # 0
|
|
*/
|
|
primitive
|
|
fpToBits : {e,p} ValidFloat e p => Float e p -> [e + p]
|
|
|
|
|
|
|
|
|
|
|
|
/* ----------------------------------------------------------------------
|
|
* Predicates
|
|
* ----------------------------------------------------------------------
|
|
*/
|
|
|
|
// Operations in `Cmp` use IEEE reasoning.
|
|
|
|
/** Check if two floating point numbers are representationally the same.
|
|
In particular, the following hold:
|
|
* NaN =.= NaN
|
|
* ~ (pfNegZero =.= fpPosZero)
|
|
*/
|
|
primitive
|
|
(=.=) : {e,p} ValidFloat e p => Float e p -> Float e p -> Bool
|
|
|
|
infix 20 =.=
|
|
|
|
/** Test if this value is not-a-number (NaN). */
|
|
primitive fpIsNaN : {e,p} ValidFloat e p => Float e p -> Bool
|
|
|
|
/** Test if this value is positive or negative infinity. */
|
|
primitive fpIsInf : {e,p} ValidFloat e p => Float e p -> Bool
|
|
|
|
/** Test if this value is positive or negative zero. */
|
|
primitive fpIsZero : {e,p} ValidFloat e p => Float e p -> Bool
|
|
|
|
/** Test if this value is negative. */
|
|
primitive fpIsNeg : {e,p} ValidFloat e p => Float e p -> Bool
|
|
|
|
/** Test if this value is normal (not NaN, not infinite, not zero, and not subnormal). */
|
|
primitive fpIsNormal : {e,p} ValidFloat e p => Float e p -> Bool
|
|
|
|
/**
|
|
* Test if this value is subnormal. Subnormal values are nonzero
|
|
* values with magnitudes smaller than can be represented with the
|
|
* normal implicit leading bit convention.
|
|
*/
|
|
primitive fpIsSubnormal : {e,p} ValidFloat e p => Float e p -> Bool
|
|
|
|
/* Returns true for numbers that are not an infinity or NaN. */
|
|
fpIsFinite : {e,p} ValidFloat e p => Float e p -> Bool
|
|
fpIsFinite f = ~ (fpIsNaN f \/ fpIsInf f )
|
|
|
|
|
|
/* ----------------------------------------------------------------------
|
|
* Arithmetic
|
|
* ---------------------------------------------------------------------- */
|
|
|
|
|
|
/** Add floating point numbers using the given rounding mode. */
|
|
primitive
|
|
fpAdd : {e,p} ValidFloat e p =>
|
|
RoundingMode -> Float e p -> Float e p -> Float e p
|
|
|
|
/** Subtract floating point numbers using the given rounding mode. */
|
|
primitive
|
|
fpSub : {e,p} ValidFloat e p =>
|
|
RoundingMode -> Float e p -> Float e p -> Float e p
|
|
|
|
/** Multiply floating point numbers using the given rounding mode. */
|
|
primitive
|
|
fpMul : {e,p} ValidFloat e p =>
|
|
RoundingMode -> Float e p -> Float e p -> Float e p
|
|
|
|
/** Divide floating point numbers using the given rounding mode. */
|
|
primitive
|
|
fpDiv : {e,p} ValidFloat e p =>
|
|
RoundingMode -> Float e p -> Float e p -> Float e p
|
|
|
|
/**
|
|
* Fused-multiply-add. 'fpFMA r x y z' computes the value '(x*y)+z',
|
|
* rounding the result according to mode 'r' only after performing both
|
|
* operations.
|
|
*/
|
|
primitive
|
|
fpFMA : {e,p} ValidFloat e p =>
|
|
RoundingMode -> Float e p -> Float e p -> Float e p -> Float e p
|
|
|
|
/**
|
|
* Absolute value of a floating-point value.
|
|
*/
|
|
primitive
|
|
fpAbs : {e,p} ValidFloat e p =>
|
|
Float e p -> Float e p
|
|
|
|
/**
|
|
* Square root of a floating-point value. The square root of
|
|
* a negative value yiels NaN, except that the sqaure root of
|
|
* '-0.0' is '-0.0'.
|
|
*/
|
|
primitive
|
|
fpSqrt : {e,p} ValidFloat e p =>
|
|
RoundingMode -> Float e p -> Float e p
|
|
|
|
/* ------------------------------------------------------------ *
|
|
* Rationals *
|
|
* ------------------------------------------------------------ */
|
|
|
|
/** Convert a floating point number to a rational.
|
|
It is an error to use this with infinity or NaN **/
|
|
primitive
|
|
fpToRational : {e,p} ValidFloat e p =>
|
|
Float e p -> Rational
|
|
|
|
/** Convert a rational to a floating point number, using the
|
|
given rounding mode, if the number cannot be represented exactly. */
|
|
primitive
|
|
fpFromRational : {e,p} ValidFloat e p =>
|
|
RoundingMode -> Rational -> Float e p
|