diff --git a/CHANGELOG.md b/CHANGELOG.md index 3429a191a..cc9317afe 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/libs/base/Data/Double.idr b/libs/base/Data/Double.idr new file mode 100644 index 000000000..588a8f2e4 --- /dev/null +++ b/libs/base/Data/Double.idr @@ -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 + diff --git a/libs/base/base.ipkg b/libs/base/base.ipkg index 9e30fc829..299c1c0a2 100644 --- a/libs/base/base.ipkg +++ b/libs/base/base.ipkg @@ -42,6 +42,7 @@ modules = Control.App, Data.Colist, Data.Colist1, Data.Contravariant, + Data.Double, Data.DPair, Data.Either, Data.Fin, diff --git a/src/Compiler/Scheme/Racket.idr b/src/Compiler/Scheme/Racket.idr index 67f04f681..06989b175 100644 --- a/src/Compiler/Scheme/Racket.idr +++ b/src/Compiler/Scheme/Racket.idr @@ -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 ++ """ diff --git a/support/chez/support.ss b/support/chez/support.ss index a12d220bd..075b4efac 100644 --- a/support/chez/support.ss +++ b/support/chez/support.ss @@ -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))) diff --git a/support/racket/support.rkt b/support/racket/support.rkt index 63b7b8d68..e321c4b65 100644 --- a/support/racket/support.rkt +++ b/support/racket/support.rkt @@ -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))) diff --git a/tests/allschemes/double001/URandEpsilon.idr b/tests/allschemes/double001/URandEpsilon.idr new file mode 100644 index 000000000..9b19c8b4b --- /dev/null +++ b/tests/allschemes/double001/URandEpsilon.idr @@ -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 + diff --git a/tests/allschemes/double001/expected b/tests/allschemes/double001/expected new file mode 100644 index 000000000..4655c8dd3 --- /dev/null +++ b/tests/allschemes/double001/expected @@ -0,0 +1,7 @@ +1/1: Building URandEpsilon (URandEpsilon.idr) +Main> Main> True +Main> True +Main> True +Main> True +Main> +Bye for now! diff --git a/tests/allschemes/double001/input b/tests/allschemes/double001/input new file mode 100644 index 000000000..dea813ac8 --- /dev/null +++ b/tests/allschemes/double001/input @@ -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 diff --git a/tests/allschemes/double001/run b/tests/allschemes/double001/run new file mode 100755 index 000000000..63121119c --- /dev/null +++ b/tests/allschemes/double001/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +idris2 URandEpsilon.idr < input diff --git a/tests/allschemes/double002/NaN.idr b/tests/allschemes/double002/NaN.idr new file mode 100644 index 000000000..13a093161 --- /dev/null +++ b/tests/allschemes/double002/NaN.idr @@ -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 + diff --git a/tests/allschemes/double002/expected b/tests/allschemes/double002/expected new file mode 100644 index 000000000..775d48ef3 --- /dev/null +++ b/tests/allschemes/double002/expected @@ -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! diff --git a/tests/allschemes/double002/input b/tests/allschemes/double002/input new file mode 100644 index 000000000..8931efec3 --- /dev/null +++ b/tests/allschemes/double002/input @@ -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 diff --git a/tests/allschemes/double002/run b/tests/allschemes/double002/run new file mode 100755 index 000000000..f8bad68ec --- /dev/null +++ b/tests/allschemes/double002/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +idris2 NaN.idr < input diff --git a/tests/allschemes/double003/Inf.idr b/tests/allschemes/double003/Inf.idr new file mode 100644 index 000000000..4549f432e --- /dev/null +++ b/tests/allschemes/double003/Inf.idr @@ -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 + diff --git a/tests/allschemes/double003/expected b/tests/allschemes/double003/expected new file mode 100644 index 000000000..7bec1523f --- /dev/null +++ b/tests/allschemes/double003/expected @@ -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! diff --git a/tests/allschemes/double003/input b/tests/allschemes/double003/input new file mode 100644 index 000000000..dd7ffff42 --- /dev/null +++ b/tests/allschemes/double003/input @@ -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 diff --git a/tests/allschemes/double003/run b/tests/allschemes/double003/run new file mode 100755 index 000000000..71cd04e9e --- /dev/null +++ b/tests/allschemes/double003/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +idris2 Inf.idr < input diff --git a/tests/node/double001/URandEpsilon.idr b/tests/node/double001/URandEpsilon.idr new file mode 100644 index 000000000..6b6f285e3 --- /dev/null +++ b/tests/node/double001/URandEpsilon.idr @@ -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 + diff --git a/tests/node/double001/expected b/tests/node/double001/expected new file mode 100644 index 000000000..4655c8dd3 --- /dev/null +++ b/tests/node/double001/expected @@ -0,0 +1,7 @@ +1/1: Building URandEpsilon (URandEpsilon.idr) +Main> Main> True +Main> True +Main> True +Main> True +Main> +Bye for now! diff --git a/tests/node/double001/input b/tests/node/double001/input new file mode 100644 index 000000000..dea813ac8 --- /dev/null +++ b/tests/node/double001/input @@ -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 diff --git a/tests/node/double001/run b/tests/node/double001/run new file mode 100755 index 000000000..63121119c --- /dev/null +++ b/tests/node/double001/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +idris2 URandEpsilon.idr < input diff --git a/tests/node/double002/NaN.idr b/tests/node/double002/NaN.idr new file mode 100644 index 000000000..13a093161 --- /dev/null +++ b/tests/node/double002/NaN.idr @@ -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 + diff --git a/tests/node/double002/expected b/tests/node/double002/expected new file mode 100644 index 000000000..e0ac132a7 --- /dev/null +++ b/tests/node/double002/expected @@ -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! diff --git a/tests/node/double002/input b/tests/node/double002/input new file mode 100644 index 000000000..8931efec3 --- /dev/null +++ b/tests/node/double002/input @@ -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 diff --git a/tests/node/double002/run b/tests/node/double002/run new file mode 100755 index 000000000..f8bad68ec --- /dev/null +++ b/tests/node/double002/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +idris2 NaN.idr < input diff --git a/tests/node/double003/Inf.idr b/tests/node/double003/Inf.idr new file mode 100644 index 000000000..4549f432e --- /dev/null +++ b/tests/node/double003/Inf.idr @@ -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 + diff --git a/tests/node/double003/expected b/tests/node/double003/expected new file mode 100644 index 000000000..95dd83d3e --- /dev/null +++ b/tests/node/double003/expected @@ -0,0 +1,15 @@ +1/1: Building Inf (Inf.idr) +Main> Main> -Infinity +Main> True +Main> True +Main> True +Main> NaN +Main> NaN +Main> True +Main> True +Main> True +Main> True +Main> True +Main> False +Main> +Bye for now! diff --git a/tests/node/double003/input b/tests/node/double003/input new file mode 100644 index 000000000..dd7ffff42 --- /dev/null +++ b/tests/node/double003/input @@ -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 diff --git a/tests/node/double003/run b/tests/node/double003/run new file mode 100755 index 000000000..71cd04e9e --- /dev/null +++ b/tests/node/double003/run @@ -0,0 +1,3 @@ +. ../../testutils.sh + +idris2 Inf.idr < input