[MLton-user] IEEEReal rounding not working

[Matthew Fluet]

On Fri, 27 Jul 2007, Sean McLaughlin wrote:
> As for interval arithmetic, a main concern of mine is that
> the sqrt function rounds correctly given the rounding mode, as specified
> in IEEE754.

The other aspect that I was wondering about was floating-point constants.
That is, what should the following program do:

val mtenth_lo = (down(); 0.1)
val mtenth_hi = (up(); 0.1)
val mtenth_near = (near(); 0.1)
val mtenth_zero = (zero(); 0.1)

val _ = print(word8vectorToString (P.toBytes mtenth_lo) ^ "\n")
val _ = print(word8vectorToString (P.toBytes mtenth_hi) ^ "\n")
val _ = print(word8vectorToString (P.toBytes mtenth_near) ^ "\n")
val _ = print(word8vectorToString (P.toBytes mtenth_zero) ^ "\n")


A very strict reading of The Definition says that special constants are 
evaluated as part of the dynamic semantics, yielding "a value according to 
normal mathematical conventions".  However, the function from special 
constants to values is:
   val : SCon -> Val
and the evaluation rule is:
   E |- scon => val(scon)   (90)
which suggests that the meaning of the special constants are not dependent 
upon the dynamic state.  On the other hand, the function from primitive 
functions and arguments to values is:
   APPLY : BasVal * Val -> Val + Pack
and the evaluation rule is:
   E |- exp => b  E |- atexp => v  APPLY(b,v) = v'/p
  ---------------------------------------------------
   E |- exp atexp => v'/p
which also suggests that primitives are pure functions, not dependent upon 
the dynamic state.  Since Real<N> arithmetic already steps outside of 
this, the question arises as to whether the evaluation of real constants 
should also step outside this.