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