An FP puzzle! Great!
q be your rational number of type
Q.t. Consider the FP number
f = Q.to_float q. The doc says that
q rounded to a nearest representable FP number. So there are three cases:
- No rounding:
q is exactly represented as
q \in [f, f]
- Rounded up:
f is “just above”
q \in [Float.pred f, f]
- Rounded down:
f is “just below”
q \in [f; Float.succ f]
To keep things simple you could pick
[Float.pred f, Float.succ f] as your interval. It contains
q and is only 2 ulp wide.
If you want the tightest interval, you need to determine which of the three cases above holds. Just convert
f back to a rational number (this is exact) and compare with
Q.compare q (Q.of_float f). If it’s 0 you’re in case 1; if it’s negative you’re in case 2; if it’s positive you’re in case 3.
I haven’t checked all the details, but I hope the above approach makes sense and is not too wrong.