Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[ base ] Add bindings for ieee Double number consts #3116

Merged
merged 11 commits into from
Nov 9, 2023
3 changes: 3 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -239,6 +239,9 @@

* Adds `Semigroup`, `Applicative`, `Traversable` and `Zippable` for `Data.These`.

* Adds bindings for IEEE floating point constants NaN and (+/-) Inf, as well as
machine epsilon and unit roundoff. Speeds vary depending on backend.

#### System

* Changes `getNProcessors` to return the number of online processors rather than
Expand Down
34 changes: 34 additions & 0 deletions libs/base/Data/Double.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,34 @@
||| Various IEEE floating-point number constants
module Data.Double

||| Largest number that can be added to a floating-point number without changing
||| its value, i.e. `1.0 + unitRoundoff == 1.0`.
%foreign "scheme:blodwen-calcFlonumUnitRoundoff"
"node:lambda:()=>Number.EPSILON / 2"
export
unitRoundoff : Double

||| Machine epsilon is the smallest floating-point number that distinguishes two
||| floating-point numbers; the step size on the floating-point number line.
-- /!\ See `support/racket/support.rkt:42-45`
-- %foreign "scheme,chez:blodwen-calcFlonumEpsilon"
-- "scheme,racket:blodwen-flonumEpsilon"
%foreign "scheme:blodwen-calcFlonumEpsilon"
"node:lambda:()=>Number.EPSILON"
export
epsilon : Double


||| Not a number, e.g. `0.0 / 0.0`. Never equal to anything, including itself.
%foreign "scheme:blodwen-flonumNaN"
"node:lambda:()=>Number.NaN"
export
nan : Double


||| Positive Infinity. Can be negated to obtain Negative Infinity.
%foreign "scheme:blodwen-flonumInf"
"node:lambda:()=>Infinity"
export
inf : Double

1 change: 1 addition & 0 deletions libs/base/base.ipkg
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,7 @@ modules = Control.App,
Data.Colist,
Data.Colist1,
Data.Contravariant,
Data.Double,
Data.DPair,
Data.Either,
Data.Fin,
Expand Down
1 change: 1 addition & 0 deletions src/Compiler/Scheme/Racket.idr
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ schHeader prof libs = fromString """
(require ffi/unsafe ffi/unsafe/define) ; for calling C
\{ ifThenElse prof "(require profile)" "" }
(require racket/flonum) ; for float-typed transcendental functions
(require math/flonum) ; for flonum constants

""" ++ libs ++ """

Expand Down
19 changes: 19 additions & 0 deletions support/chez/support.ss
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,25 @@
(if (> b 0) (+ r b) (- r b))
r)))

; flonum constants

(define (blodwen-calcFlonumUnitRoundoff)
(let loop [(uro 1.0)]
(if (fl= 1.0 (fl+ 1.0 uro))
uro
(loop (fl/ uro 2.0)))))

(define (blodwen-calcFlonumEpsilon)
(fl* (blodwen-calcFlonumUnitRoundoff) 2.0))

(define (blodwen-flonumNaN)
+nan.0)

(define (blodwen-flonumInf)
+inf.0)

; Bits

(define bu+ (lambda (x y bits) (blodwen-toUnsignedInt (+ x y) bits)))
(define bu- (lambda (x y bits) (blodwen-toUnsignedInt (- x y) bits)))
(define bu* (lambda (x y bits) (blodwen-toUnsignedInt (* x y) bits)))
Expand Down
25 changes: 25 additions & 0 deletions support/racket/support.rkt
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,31 @@
(if (> b 0) (+ r b) (- r b))
r)))

; flonum constants

;; /!\ this code is cursed for some reason?...
;;
;; (define (blodwen-flonumEpsilon)
;; epsilon.0)

(define (blodwen-calcFlonumUnitRoundoff)
;; (fl/ (blodwen-flonumEpsilon) 2.0))
(let loop [(uro 1.0)]
(if (fl= 1.0 (fl+ 1.0 uro))
uro
(loop (fl/ uro 2.0)))))

(define (blodwen-calcFlonumEpsilon)
(fl* (blodwen-calcFlonumUnitRoundoff) 2.0))

(define (blodwen-flonumNaN)
+nan.0)

(define (blodwen-flonumInf)
+inf.0)

; Bits

(define bu+ (lambda (x y bits) (blodwen-toUnsignedInt (+ x y) bits)))
(define bu- (lambda (x y bits) (blodwen-toUnsignedInt (- x y) bits)))
(define bu* (lambda (x y bits) (blodwen-toUnsignedInt (* x y) bits)))
Expand Down
19 changes: 19 additions & 0 deletions tests/allschemes/double001/URandEpsilon.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
import Data.Double

-- adding the unit roundoff to a Double should not modify it

testOnePlusUR : Bool
testOnePlusUR = 1.0 + unitRoundoff == 1.0

testURPlusOne : Bool
testURPlusOne = unitRoundoff + 1.0 == 1.0

testURComm : Bool
testURComm = testOnePlusUR == testURPlusOne


-- the machine epsilon should be double the unit roundoff

testEps2UR : Bool
testEps2UR = epsilon == unitRoundoff * 2.0

7 changes: 7 additions & 0 deletions tests/allschemes/double001/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
1/1: Building URandEpsilon (URandEpsilon.idr)
Main> Main> True
Main> True
Main> True
Main> True
Main>
Bye for now!
5 changes: 5 additions & 0 deletions tests/allschemes/double001/input
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
-- we need to exec to get the prim__* functions to disappear
:exec printLn testOnePlusUR
:exec printLn testURPlusOne
:exec printLn testURComm
:exec printLn testEps2UR
3 changes: 3 additions & 0 deletions tests/allschemes/double001/run
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
. ../../testutils.sh

idris2 URandEpsilon.idr < input
28 changes: 28 additions & 0 deletions tests/allschemes/double002/NaN.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
import Data.Double

-- undefined things are NaN
divZeroZero : Double
divZeroZero = 0.0 / 0.0

-- NaN with anything is NaN

nanPlus : Double
nanPlus = 1.0 + nan

nanSub : Double
nanSub = 1.0 - nan

nanMult : Double
nanMult = 2.0 * nan

nanDiv : Double
nanDiv = nan / 2.0

-- neg NaN is still NaN
negNaN : Double
negNaN = negate nan

-- NaNs are never equal
nansNotEq : Bool
nansNotEq = nan == nan

10 changes: 10 additions & 0 deletions tests/allschemes/double002/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
1/1: Building NaN (NaN.idr)
Main> Main> +nan.0
Main> +nan.0
Main> +nan.0
Main> +nan.0
Main> +nan.0
Main> +nan.0
Main> False
Main>
Bye for now!
8 changes: 8 additions & 0 deletions tests/allschemes/double002/input
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
-- we need to exec to get the prim__* functions to disappear
:exec printLn divZeroZero
:exec printLn nanPlus
:exec printLn nanSub
:exec printLn nanMult
:exec printLn nanDiv
:exec printLn negNaN
:exec printLn nansNotEq
3 changes: 3 additions & 0 deletions tests/allschemes/double002/run
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
. ../../testutils.sh

idris2 NaN.idr < input
52 changes: 52 additions & 0 deletions tests/allschemes/double003/Inf.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
import Data.Double

-- negating positive inf (should give negative inf)
negInf : Double
negInf = negate inf

-- dividing non-zero by zero tends to infinity
divNZbyZero : Bool
divNZbyZero = 1.0 / 0.0 == inf

-- adding pos-inf to pos-inf gives pos-inf
addPosInfs : Bool
addPosInfs = inf + inf == inf

-- subbing inf from neg-inf gives neg-inf
subNegInfs : Bool
subNegInfs = -inf - inf == -inf

-- subtracting pos-inf from pos-inf is nan
-- (can't use `==` because no nans are equal)
subPosInf : Double
subPosInf = inf - inf

-- adding pos-inf to neg-inf is nan
-- (can't use `==` because no nans are equal)
addNegInf : Double
addNegInf = -inf + inf

-- neg-inf by neg-inf gives pos-inf
squareNegInfIsPosInf : Bool
squareNegInfIsPosInf = pow (-inf) 2 == inf

-- pos-inf by pos-inf gives pos-inf
squarePosInfIsPosInf : Bool
squarePosInfIsPosInf = pow inf 2 == inf

-- pos-inf by neg-inf is neg-inf
multInfSignFlip : Bool
multInfSignFlip = inf * (-inf) == -inf

-- pos-inf is equal to some other pos-inf
posInfIsPosInf : Bool
posInfIsPosInf = inf == pow inf 2

-- neg-inf is equal to some other neg-inf
negInfIsNegInf : Bool
negInfIsNegInf = -inf == pow (-inf) 3

-- pos-inf is not neg-inf
posInfEqNegInf : Bool
posInfEqNegInf = inf == -inf

15 changes: 15 additions & 0 deletions tests/allschemes/double003/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
1/1: Building Inf (Inf.idr)
Main> Main> -inf.0
Main> True
Main> True
Main> True
Main> +nan.0
Main> +nan.0
Main> True
Main> True
Main> True
Main> True
Main> True
Main> False
Main>
Bye for now!
13 changes: 13 additions & 0 deletions tests/allschemes/double003/input
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
-- we need to exec to get the prim__* functions to disappear
:exec printLn negInf
:exec printLn divNZbyZero
:exec printLn addPosInfs
:exec printLn subNegInfs
:exec printLn subPosInf
:exec printLn addNegInf
:exec printLn squareNegInfIsPosInf
:exec printLn squarePosInfIsPosInf
:exec printLn multInfSignFlip
:exec printLn posInfIsPosInf
:exec printLn negInfIsNegInf
:exec printLn posInfEqNegInf
3 changes: 3 additions & 0 deletions tests/allschemes/double003/run
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
. ../../testutils.sh

idris2 Inf.idr < input
19 changes: 19 additions & 0 deletions tests/node/double001/URandEpsilon.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
import Data.Double

-- adding the rounding unit to a Double should not modify it

testOnePlusUR : Bool
testOnePlusUR = 1.0 + unitRoundoff == 1.0

testURPlusOne : Bool
testURPlusOne = unitRoundoff + 1.0 == 1.0

testURComm : Bool
testURComm = testOnePlusUR == testURPlusOne


-- the machine epsilon should be double the rounding unit

testEps2UR : Bool
testEps2UR = epsilon == unitRoundoff * 2.0

7 changes: 7 additions & 0 deletions tests/node/double001/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
1/1: Building URandEpsilon (URandEpsilon.idr)
Main> Main> True
Main> True
Main> True
Main> True
Main>
Bye for now!
5 changes: 5 additions & 0 deletions tests/node/double001/input
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
-- we need to exec to get the prim__* functions to disappear
:exec printLn testOnePlusUR
:exec printLn testURPlusOne
:exec printLn testURComm
:exec printLn testEps2UR
3 changes: 3 additions & 0 deletions tests/node/double001/run
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
. ../../testutils.sh

idris2 URandEpsilon.idr < input
28 changes: 28 additions & 0 deletions tests/node/double002/NaN.idr
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
import Data.Double

-- undefined things are NaN
divZeroZero : Double
divZeroZero = 0.0 / 0.0

-- NaN with anything is NaN

nanPlus : Double
nanPlus = 1.0 + nan

nanSub : Double
nanSub = 1.0 - nan

nanMult : Double
nanMult = 2.0 * nan

nanDiv : Double
nanDiv = nan / 2.0

-- neg NaN is still NaN
negNaN : Double
negNaN = negate nan

-- NaNs are never equal
nansNotEq : Bool
nansNotEq = nan == nan

10 changes: 10 additions & 0 deletions tests/node/double002/expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
1/1: Building NaN (NaN.idr)
Main> Main> NaN
Main> NaN
Main> NaN
Main> NaN
Main> NaN
Main> NaN
Main> False
Main>
Bye for now!
8 changes: 8 additions & 0 deletions tests/node/double002/input
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
-- we need to exec to get the prim__* functions to disappear
:exec printLn divZeroZero
:exec printLn nanPlus
:exec printLn nanSub
:exec printLn nanMult
:exec printLn nanDiv
:exec printLn negNaN
:exec printLn nansNotEq
3 changes: 3 additions & 0 deletions tests/node/double002/run
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
. ../../testutils.sh

idris2 NaN.idr < input
Loading
Loading