Add more functionality to floating point number type

[oskarabrahamsson]

Currently, the only way to create floating point numbers is to parse them from string. Pretty much the only useful things I can do with these floating point numbers is arithmetic (addition, multiplication, subtraction and division), as well as turning them back into strings. In this sense they're a finite precision alternative to the built-in rational type, albeit with less operations.

I propose adding the following (at the very least):

• Double.exp and Double.log
• Double.floor (and/or truncate, or something)
• Double.toInt

Here is a related issue: https://github.com/CakeML/cakeml/issues/824.

[michael-roe]

At the moment, I can't get floating point arithmetic to work at all. But assuming I get past that issue, CakeML is missing several important operations that are in IEEE 754 and in the Standard ML basis library:

val copySign : real * real -> real

This is needed to extract the sign bit from a floating point value that can't simply be compared against zero. (-0.0 is "equal" to 0.0, NaN is unordered with respect to 0.0)

val unordered : real * real -> bool

Comparison operation that is true if either of them is a NaN.

val isNan : real -> bool (isInfinite would be good, too)

=======

I don't understand the cakeml code well enough to be sure, but it looks to me as though adding these might require adding some of them to Isabelle's theory of IEEE 754 arithmetic.

=====

Rationale for why these operations are needed: ideally, Double.toString would be implemented in the language, rather than with a foreign function interface call that eventually calls the C library's snprintf(). Which means that you need a rich enough set of floating point operations that you can implement Double.toString.

[michael-roe]

I'd don't entirely understand how HOL4's IEEE 754 theory works, but looking at https://github.com/HOL-Theorem-Prover/HOL/blob/62a0f78a20c8e8202d35e4cbbd397c8d70a3ad00/src/float/ieeeScript.sml it looks like is_nan and is_infinity are defined, but copysign and unordered aren't.

[michael-roe]

On floating point comparison operators: the result of a comparison can be less than, greater than, equal or unordered (4 possibilities). That gives 2**4 = 16 possible binary operators. You can reduce this to 8 if you leave out the ones that are the negation of an existing operator. You further reduce it to 7 is you leave out the "always false" operator.

HOL4's theory defines 5 of them, leaving out "unordered" and "equal or unordered (?=)", both of which are in the Standard ML basis library.

[michael-roe]

The L3 language lacks FP64_Unordered too, so in the L3 model of MIPS floating point I had to provide a definition for it:

(https://github.com/acjf3/l3mips/blob/master/src/l3/fpu/instructions.spec)

[michael-roe]

By way of illustration, here is a rough attempt at a double to hexadecimal string function, written in Standard ML of New Jersey rather than CakeML. It doesn't handle denormalised numbers, but don't worry about that. The issue here is that I want to be able to write a function like this in CakeML, so CakeML should have something equivalent for the floating point operations that it uses. (Which are copySign, class, toManExp, trunc, realTrunc).

fun mantissa_to_hex_1(x) = if Real.==(x, 0.0) then "" else let val v = 16.0*x in (Int.fmt StringCvt.HEX (Real.trunc(v))) ^ mantissa_to_hex_1(v - Real.realTrunc(v)) end;

fun mantissa_to_hex(x) = if Real.==(x, 0.0) then "0" else let val v = 16.0*x in (Int.fmt StringCvt.HEX (Real.trunc(v))) ^ mantissa_to_hex_1(v - Real.realTrunc(v)) end;

fun nonnegative_real_to_hex(x) = let val c = Real.class(x) in case c of IEEEReal.ZERO => "0x0p+0" | IEEEReal.NORMAL => let val y = Real.toManExp(x) in "0x1." ^ mantissa_to_hex(2.0*(#man y) - 1.0) ^ "p" ^ Int.toString((#exp y) - 1) end | IEEEReal.SUBNORMAL => "subnormal" | IEEEReal.INF => "inf" | IEEEReal.NAN p => "nan" end;

fun real_to_hex(x) = if Real.copySign(1.0, x) < 0.0 then "~"^nonnegative_real_to_hex(Real.abs(x)) else nonnegative_real_to_hex(x);