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

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

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
+

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,

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 ++ """
 

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)))

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)))

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
+

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!

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

tests/allschemes/double001/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+idris2 URandEpsilon.idr < input

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
+

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!

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

tests/allschemes/double002/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+idris2 NaN.idr < input

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
+

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!

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

tests/allschemes/double003/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+idris2 Inf.idr < input

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
+

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!

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

tests/node/double001/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+idris2 URandEpsilon.idr < input

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
+

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!

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

tests/node/double002/run

@@ -0,0 +1,3 @@
+. ../../testutils.sh
+
+idris2 NaN.idr < input