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 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 =.= /* Returns true for numbers that are not an infinity or NaN. */ primitive fpIsFinite : {e,p} ValidFloat e p => Float e p -> Bool /* ---------------------------------------------------------------------- * 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 /* ------------------------------------------------------------ * * 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