Real.maxFinite bug

[Matthew Fluet]

> Anyways, please take a look at Real.c and see if you have any suggestions for
> Real_class, Real_qequal, and Real_isNormal, which are still implemented by hand
> instead of calling math.h functions.  They may be susceptible to similar bugs.

It wasn't clear to me from the start of this discussion why exactly
maxFinite, minPos, and minNormalPos are _computed_ values?  In particular,
what justifies the correctness of 

      local
         fun min (p: real -> bool): real =
            let
               fun loop (x: real): real =
                  let
                     val y = x / 2.0
                  in
                     if p y
                        then loop y
                     else x
                  end
            in loop 1.0
            end
      in
         val minNormalPos = min isNormal
         val minPos = min isPositive
      end

where minNormalPos and minPos will be of the form 1/(2^n) for some n (and
that's assuming infinite precision arithmetic).  It seems that this is
sensitive to the binary encoding of floating-point numbers; and if you're
depending on IEEE, then just construct the value as a pair of words (or a
packed real) and cast it.  maxFinite doesn't have the exact same issue; 
the resulting value will be of the form a_n*2^n + a_{n-1}*2^{n-1} + ... +
a_1*2 + a_0*2^0 + a_{-1}*2^{-1} + ...  where a_i \in {0,1} and there is an
I < n such that a_i = 1 for i > I and a_i = 0 for I <= I. But this again
assumes that the binary encoding of the maximum finite number is of this
form.