[ base ] Add bindings for ieee Double number consts
#3116
Conversation
Racket provides a builtin for the epsilon `epsilon.0`. Chez Scheme does not, but we can calculate it manually. The (machine-)epsilon is the minimum distance between floating-point numbers. The rounding unit is the smallest number which does not move a float (iiuc), typically defined as eps/2 (or rather, eps is sometimes 2ru).
With accompanying tests for schemes and node
Seems to be the technical term; I'd just misremembered what it was.
Combined, the IEEE-related commits close idris-lang#29
There was a problem hiding this comment.
I think our standard approach has been to call the naked foreign primitive
something like prim__xxx and then defining an xxx toplevel function.
We can attach documentation to that xxx.
Then again this may be because we typically have PrimIO involved and we
use these toplevel definitions to wrap the call into a nicer IO...
That was almost exactly my rationale; don't wrap the names with |
For SOME reason, using `epsilon.0` in `support.rkt` trips the totality checker but only on `libs/papers/Data/Description/Regular.idr` ??? Idk man, computers were a mistake...
|
(Copying from Discord so it doesn't get lost in the aether): Issue 1 is that the new bindings require Now why that causes the totality checker of all things to trip, and why it only trips it on papers' |
For some reason, having `epsilon.0` from `(require math/flonum)` anywhere in the Racket support library trips the totality checker, regardless of whether the code is used or not. Operations from `math/flonum` (e.g. `fl/`) do not reproduce this behaviour. See idris-lang#3116 for the full context.
MVP (afaict) for having these constants available to those who want it, along with some tests that I think check they behave as expected
Closes #29
Should this change go in the CHANGELOG?
implementation, I have updated
CHANGELOG.md(and potentially alsoCONTRIBUTORS.md).