grisette-0.8.0.0: test/Grisette/SymPrim/FPTests.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# HLINT ignore "Unused LANGUAGE pragma" #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
module Grisette.SymPrim.FPTests (fpTests) where
import Data.Foldable (traverse_)
import Data.Kind (Type)
import Data.Ratio ((%))
import Data.SBV (SMTResult (Satisfiable, Unsatisfiable))
import qualified Data.SBV as SBV
import Data.Word (Word32, Word64)
import GHC.TypeLits (KnownNat, Nat, type (<=))
import Grisette
( AlgReal (AlgExactRational),
FP,
FPRoundingMode (RTP),
IEEEFPConstants
( fpMaxNormalized,
fpMaxSubnormal,
fpMinNormalized,
fpMinSubnormal
),
IEEEFPOp
( fpAbs,
fpMaximum,
fpMaximumNumber,
fpMinimum,
fpMinimumNumber,
fpNeg,
fpRem
),
IEEEFPRoundingMode (rna, rne, rtn, rtp, rtz),
IEEEFPRoundingOp
( fpAdd,
fpDiv,
fpFMA,
fpMul,
fpRoundToIntegral,
fpSqrt,
fpSub
),
WordN,
bitCastOrCanonical,
)
import Grisette.Internal.Core.Data.Class.BitCast (BitCast (bitCast))
import Grisette.Internal.Core.Data.Class.IEEEFP
( IEEEFPConstants
( fpNaN,
fpNegativeInfinite,
fpNegativeZero,
fpPositiveInfinite,
fpPositiveZero
),
IEEEFPConvertible (fromFPOr, toFP),
fpIsNaN,
fpIsNegativeInfinite,
fpIsNegativeZero,
fpIsPositiveInfinite,
fpIsPositiveZero,
)
import Grisette.Internal.Core.Data.Class.SafeFromFP (SafeFromFP (safeFromFP))
import Grisette.Internal.Core.Data.Class.SymIEEEFP
( SymIEEEFPTraits
( symFpIsInfinite,
symFpIsNaN,
symFpIsNegative,
symFpIsNegativeInfinite,
symFpIsNegativeZero,
symFpIsNormal,
symFpIsPoint,
symFpIsPositive,
symFpIsPositiveInfinite,
symFpIsPositiveZero,
symFpIsSubnormal,
symFpIsZero
),
)
import Grisette.Internal.SymPrim.BV (IntN)
import Grisette.Internal.SymPrim.FP
( ConvertibleBound (convertibleLowerBound, convertibleUpperBound),
FP32,
NotRepresentableFPError,
ValidFP,
nextFP,
prevFP,
)
import Grisette.Internal.SymPrim.Prim.Internal.Instances.PEvalIEEEFPConvertibleTerm
( genericFPCast,
)
import Grisette.Internal.SymPrim.Prim.Internal.Term
( SupportedPrim (conSBVTerm),
)
import Test.Framework (Test, testGroup)
import Test.Framework.Providers.HUnit (testCase)
import Test.Framework.Providers.QuickCheck2 (testProperty)
import Test.HUnit (assertBool, (@?=))
import Test.QuickCheck (Arbitrary, ioProperty)
import Type.Reflection (Typeable, typeRep)
sameFP :: forall a b. (RealFloat a, RealFloat b) => a -> b -> Bool
sameFP x y
| isNaN x && isNaN y = True
| isInfinite x && isInfinite y =
(x < 0 && y < 0) || (x > 0 && y > 0)
-- \| GHC's floating point support doesn't conform to IEEE754.
| otherwise = (uncurry encodeFloat (decodeFloat x) :: b) == y
fp32ConversionTest :: (Word32 -> IO ()) -> [Test]
fp32ConversionTest testFun =
[ testProperty "property" $ ioProperty . testFun,
testCase "NaN" $ testFun 0x7f800100,
testCase "+inf" $ testFun 0x7f800000,
testCase "-inf" $ testFun 0xFf800000,
testCase "0" $ testFun 0,
testCase "-0" $ testFun 0x80000000
]
fp64ConversionTest :: (Word64 -> IO ()) -> [Test]
fp64ConversionTest testFun =
[ testProperty "property" $ ioProperty . testFun,
testCase "NaN" $ testFun 0x7ff8000010000000,
testCase "+inf" $ testFun 0x7FF0000000000000,
testCase "-inf" $ testFun 0xFFF0000000000000,
testCase "0" $ testFun 0,
testCase "-0" $ testFun 0x8000000000000000
]
unaryOpComplianceWithFloat ::
String ->
(FP32 -> a) ->
(Float -> b) ->
(a -> b -> Bool) ->
Test
unaryOpComplianceWithFloat name fpOp floatOp cmp =
testProperty name $ \x ->
let x' = bitCastOrCanonical x
actual = fpOp x
expected = floatOp x'
in cmp actual expected
binOpComplianceWithFloat ::
String ->
(FP32 -> FP32 -> a) ->
(Float -> Float -> b) ->
(a -> b -> Bool) ->
Test
binOpComplianceWithFloat name fpOp floatOp cmp =
testProperty name $ \x y ->
let x' = bitCastOrCanonical x
y' = bitCastOrCanonical y
actual = fpOp x y
expected = floatOp x' y'
in cmp actual expected
fpTests :: Test
fpTests =
testGroup
"FP"
[ testGroup
"bitcast"
[ testGroup "WordN -> FP" $
fp32ConversionTest $ \(x :: Word32) -> do
let fp = bitCast x :: FP32
let float = bitCast x :: Float
assertBool "Must be the same FP" $ sameFP fp float,
testGroup "FP -> WordN" $ do
fp32ConversionTest $ \(x :: Word32) -> do
let fp = bitCast x :: FP32
let regulated =
if isNaN fp
then 0x7fc00000
else bitCastOrCanonical fp :: WordN 32
let actual = bitCastOrCanonical (bitCast regulated :: FP32)
actual @?= regulated
],
testGroup
"Eq"
[ binOpComplianceWithFloat "==" (==) (==) (==),
binOpComplianceWithFloat "/=" (/=) (/=) (==)
],
testGroup
"Ord"
[ binOpComplianceWithFloat "<" (<) (<) (==),
binOpComplianceWithFloat "<=" (<=) (<=) (==),
binOpComplianceWithFloat ">" (>) (>) (==),
binOpComplianceWithFloat ">=" (>=) (>=) (==)
],
testGroup
"Num"
[ binOpComplianceWithFloat "+" (+) (+) sameFP,
binOpComplianceWithFloat "-" (-) (-) sameFP,
binOpComplianceWithFloat "*" (*) (*) sameFP,
unaryOpComplianceWithFloat "negate" negate negate sameFP,
unaryOpComplianceWithFloat "abs" abs abs sameFP,
unaryOpComplianceWithFloat "signum" signum signum sameFP,
testProperty "fromInteger" $ \x ->
let fp = fromInteger x :: FP32
float = fromInteger x :: Float
in sameFP fp float
],
testCase "Lift" $ do
let x = bitCast (0x12345678 :: WordN 32) :: FP32
$$([||x||]) @?= x,
testGroup
"Fractional"
[ binOpComplianceWithFloat "/" (/) (/) sameFP,
unaryOpComplianceWithFloat "recip" recip recip sameFP,
testProperty "fromRational" $ \x ->
let fp = fromRational x :: FP32
float = fromRational x :: Float
in sameFP fp float
],
testGroup
"Floating"
[ -- Only the following operations are supported in SBV
unaryOpComplianceWithFloat "sqrt" sqrt sqrt sameFP,
binOpComplianceWithFloat "(**)" (**) (**) sameFP
],
-- Real instantce is not compliant with Float.
-- testGroup
-- "Real"
-- [ unaryOpComplianceWithFloat "toRational" toRational toRational (==)
-- ]
-- RealFrac instance is not compliant with Float.
-- testGroup
-- "RealFrac"
-- [ unaryOpComplianceWithFloat
-- "truncate"
-- truncate
-- truncate
-- ((==) @Integer),
-- unaryOpComplianceWithFloat "round" round round ((==) @Integer),
-- unaryOpComplianceWithFloat "ceiling" ceiling ceiling ((==) @Integer),
-- unaryOpComplianceWithFloat "floor" floor floor ((==) @Integer)
-- ]
testGroup
"RealFloat"
[ unaryOpComplianceWithFloat "floatRadix" floatRadix floatRadix (==),
unaryOpComplianceWithFloat "floatDigits" floatDigits floatDigits (==),
unaryOpComplianceWithFloat "floatRange" floatRange floatRange (==),
-- decodeFloat is not compliant with Float
-- unaryOpComplianceWithFloat "decodeFloat" decodeFloat decodeFloat (==)
-- encodeFloat isn't tested
-- exponent is not compliant with Float
-- unaryOpComplianceWithFloat "exponent" exponent exponent (==)
-- significand is not compliant with Float
-- unaryOpComplianceWithFloat "significand" significand significand sameFP
testProperty "scaleFloat" $ \i (x :: FP32) ->
let x' = bitCastOrCanonical x :: Float
actual = scaleFloat i x
expected = scaleFloat i x'
in sameFP actual expected,
testProperty "isNaN" $ \(x :: FP32) ->
let x' = bitCastOrCanonical x :: Float
in isNaN x == isNaN x',
unaryOpComplianceWithFloat "isInfinite" isInfinite isInfinite (==),
unaryOpComplianceWithFloat
"isDenormalized"
isDenormalized
isDenormalized
(==),
unaryOpComplianceWithFloat
"isNegativeZero"
isNegativeZero
isNegativeZero
(==),
unaryOpComplianceWithFloat "isIEEE" isIEEE isIEEE (==) -- ,
-- atan2 is not supported
-- binOpComplianceWithFloat "atan2" atan2 atan2 sameFP
],
testGroup
"SymIEEEFPTraits"
[ unaryOpComplianceWithFloat "symFpIsNaN" symFpIsNaN symFpIsNaN (==),
unaryOpComplianceWithFloat
"symFpIsPositive"
symFpIsPositive
symFpIsPositive
(==),
unaryOpComplianceWithFloat
"symFpIsNegative"
symFpIsNegative
symFpIsNegative
(==),
unaryOpComplianceWithFloat
"symFpIsPositiveInfinite"
symFpIsPositiveInfinite
symFpIsPositiveInfinite
(==),
unaryOpComplianceWithFloat
"symFpIsNegativeInfinite"
symFpIsNegativeInfinite
symFpIsNegativeInfinite
(==),
unaryOpComplianceWithFloat
"symFpIsInfinite"
symFpIsInfinite
symFpIsInfinite
(==),
unaryOpComplianceWithFloat
"symFpIsPositiveZero"
symFpIsPositiveZero
symFpIsPositiveZero
(==),
unaryOpComplianceWithFloat
"symFpIsNegativeZero"
symFpIsNegativeZero
symFpIsNegativeZero
(==),
unaryOpComplianceWithFloat "symFpIsZero" symFpIsZero symFpIsZero (==),
unaryOpComplianceWithFloat
"symFpIsNormal"
symFpIsNormal
symFpIsNormal
(==),
unaryOpComplianceWithFloat
"symFpIsSubnormal"
symFpIsSubnormal
symFpIsSubnormal
(==),
unaryOpComplianceWithFloat
"symFpIsPoint"
symFpIsPoint
symFpIsPoint
(==)
],
testGroup
"IEEEFPConstants"
[ testCase "fpPositiveInfinite" $
fpIsPositiveInfinite (fpPositiveInfinite :: FP32) @?= True,
testCase "fpNegativeInfinite" $
fpIsNegativeInfinite (fpNegativeInfinite :: FP32) @?= True,
testCase "fpNaN" $
fpIsNaN (fpNaN :: FP32) @?= True,
testCase "fpPositiveZero" $
fpIsPositiveZero (fpPositiveZero :: FP32) @?= True,
testCase "fpNegativeZero" $
fpIsNegativeZero (fpNegativeZero :: FP32) @?= True,
testCase "fpMinNormalized" $
fpMinNormalized @?= (1.5625e-2 :: FP 4 4),
testCase "fpMaxNormalized" $
fpMaxNormalized @?= (2.4e2 :: FP 4 4),
testCase "fpMinSubnormal" $
fpMinSubnormal @?= (1.953125e-3 :: FP 4 4),
testCase "fpMaxSubnormal" $
fpMaxSubnormal @?= (1.3671875e-2 :: FP 4 4)
],
testGroup
"IEEEFPOp"
[ testCase "fpAbs" $ do
SameFPObj (fpAbs (0 :: FP32)) @?= 0
SameFPObj (fpAbs (fpNegativeZero :: FP32)) @?= 0
SameFPObj (fpAbs (fpPositiveInfinite :: FP32))
@?= fpPositiveInfinite
SameFPObj (fpAbs (fpNegativeInfinite :: FP32))
@?= fpPositiveInfinite
SameFPObj (fpAbs (1 :: FP32)) @?= 1
SameFPObj (fpAbs (-1 :: FP32)) @?= 1
SameFPObj (fpAbs (fpNaN :: FP32)) @?= fpNaN,
testCase "fpNeg" $ do
SameFPObj (fpNeg (0 :: FP32)) @?= -0
SameFPObj (fpNeg (fpNegativeZero :: FP32)) @?= 0
SameFPObj (fpNeg (fpPositiveInfinite :: FP32))
@?= fpNegativeInfinite
SameFPObj (fpNeg (fpNegativeInfinite :: FP32))
@?= fpPositiveInfinite
SameFPObj (fpNeg (1 :: FP32)) @?= -1
SameFPObj (fpNeg (-1 :: FP32)) @?= 1
SameFPObj (fpNeg (fpNaN :: FP32)) @?= fpNaN,
testGroup
"fpRem"
[ testCase "inf or nan / x" $ do
let lhs =
[fpPositiveInfinite :: FP32, fpNegativeInfinite, fpNaN]
let rhs =
[ 0,
-0,
1,
-1,
fpPositiveInfinite,
fpNegativeInfinite,
fpNaN
]
traverse_ (\(l, r) -> SameFPObj (fpRem l r) @?= fpNaN) $
zip lhs rhs,
testCase "0 / neither 0 nor nan" $ do
let lhs = [fpPositiveZero :: FP32, fpNegativeZero]
let rhs =
[1, -1, fpPositiveInfinite, fpNegativeInfinite]
traverse_ (\(l, r) -> SameFPObj (fpRem l r) @?= SameFPObj l) $
[(l, r) | l <- lhs, r <- rhs],
testCase "0 / 0 or nan" $ do
let lhs = [fpPositiveZero :: FP32, fpNegativeZero]
let rhs = [fpPositiveZero, fpNegativeZero, fpNaN]
traverse_ (\(l, r) -> SameFPObj (fpRem l r) @?= fpNaN) $
[(l, r) | l <- lhs, r <- rhs],
testCase "normal" $ do
SameFPObj (fpRem (5 :: FP32) 4) @?= 1
SameFPObj (fpRem (6 :: FP32) 4) @?= -2
SameFPObj (fpRem (7 :: FP32) 4) @?= -1
SameFPObj (fpRem (8 :: FP32) 4) @?= 0
SameFPObj (fpRem (9 :: FP32) 4) @?= 1
SameFPObj (fpRem (10 :: FP32) 4) @?= 2
],
testCase "fpMinimum" $ do
SameFPObj (fpMinimum (0 :: FP32) 0) @?= 0
SameFPObj (fpMinimum (0 :: FP32) (-0)) @?= -0
SameFPObj (fpMinimum (-0 :: FP32) 0) @?= -0
SameFPObj (fpMinimum (-0 :: FP32) (-0)) @?= -0
SameFPObj (fpMinimum (fpNaN :: FP32) fpNaN) @?= fpNaN
SameFPObj (fpMinimum (fpNaN :: FP32) 1) @?= fpNaN
SameFPObj (fpMinimum (1 :: FP32) fpNaN) @?= fpNaN
SameFPObj (fpMinimum (fpNaN :: FP32) fpPositiveInfinite) @?= fpNaN
SameFPObj (fpMinimum (fpNegativeInfinite :: FP32) fpNaN) @?= fpNaN
SameFPObj (fpMinimum (1 :: FP32) 2) @?= 1,
testCase "fpMinimumNumber" $ do
SameFPObj (fpMinimumNumber (0 :: FP32) 0) @?= 0
SameFPObj (fpMinimumNumber (0 :: FP32) (-0)) @?= -0
SameFPObj (fpMinimumNumber (-0 :: FP32) 0) @?= -0
SameFPObj (fpMinimumNumber (-0 :: FP32) (-0)) @?= -0
SameFPObj (fpMinimumNumber (fpNaN :: FP32) fpNaN) @?= fpNaN
SameFPObj (fpMinimumNumber (fpNaN :: FP32) 1) @?= 1
SameFPObj (fpMinimumNumber (1 :: FP32) fpNaN) @?= 1
SameFPObj (fpMinimumNumber (fpNaN :: FP32) fpPositiveInfinite)
@?= fpPositiveInfinite
SameFPObj (fpMinimumNumber (fpNegativeInfinite :: FP32) fpNaN)
@?= fpNegativeInfinite
SameFPObj (fpMinimumNumber (1 :: FP32) 2) @?= 1,
testCase "fpMaximum" $ do
SameFPObj (fpMaximum (0 :: FP32) 0) @?= 0
SameFPObj (fpMaximum (0 :: FP32) (-0)) @?= 0
SameFPObj (fpMaximum (-0 :: FP32) 0) @?= 0
SameFPObj (fpMaximum (-0 :: FP32) (-0)) @?= -0
SameFPObj (fpMaximum (fpNaN :: FP32) fpNaN) @?= fpNaN
SameFPObj (fpMaximum (fpNaN :: FP32) 1) @?= fpNaN
SameFPObj (fpMaximum (1 :: FP32) fpNaN) @?= fpNaN
SameFPObj (fpMaximum (fpNaN :: FP32) fpPositiveInfinite) @?= fpNaN
SameFPObj (fpMaximum (fpNegativeInfinite :: FP32) fpNaN) @?= fpNaN
SameFPObj (fpMaximum (1 :: FP32) 2) @?= 2,
testCase "fpMaximumNumber" $ do
SameFPObj (fpMaximumNumber (0 :: FP32) 0) @?= 0
SameFPObj (fpMaximumNumber (0 :: FP32) (-0)) @?= 0
SameFPObj (fpMaximumNumber (-0 :: FP32) 0) @?= 0
SameFPObj (fpMaximumNumber (-0 :: FP32) (-0)) @?= -0
SameFPObj (fpMaximumNumber (fpNaN :: FP32) fpNaN) @?= fpNaN
SameFPObj (fpMaximumNumber (fpNaN :: FP32) 1) @?= 1
SameFPObj (fpMaximumNumber (1 :: FP32) fpNaN) @?= 1
SameFPObj (fpMaximumNumber (fpNaN :: FP32) fpPositiveInfinite)
@?= fpPositiveInfinite
SameFPObj (fpMaximumNumber (fpNegativeInfinite :: FP32) fpNaN)
@?= fpNegativeInfinite
SameFPObj (fpMaximumNumber (1 :: FP32) 2) @?= 2
],
testGroup
"IEEEFPRoundingOp"
[ testCase "unop nan" $ do
let op = [fpRoundToIntegral, fpSqrt]
let roundingMode = [rne, rna, rtz, rtn, rtp]
traverse_ (\(o, rd) -> SameFPObj (o rd fpNaN) @?= fpNaN) $
[(op, rd) | op <- op, rd <- roundingMode],
testCase "binop nan" $ do
let op = [fpAdd, fpSub, fpMul, fpDiv]
let roundingMode = [rne, rna, rtz, rtn, rtp]
let operands =
[(fpNaN :: FP32, 1 :: FP32), (1, fpNaN), (fpNaN, fpNaN)]
traverse_ (\(o, r, (a, b)) -> SameFPObj (o r a b) @?= fpNaN) $
[(o, r, (a, b)) | o <- op, r <- roundingMode, (a, b) <- operands],
testCase "ternop nan" $ do
let op = [fpFMA]
let roundingMode = [rne, rna, rtz, rtn, rtp]
let operand = [fpNaN :: FP32, 1]
let operands =
[ (a, b, c)
| a <- operand,
b <- operand,
c <- operand,
fpIsNaN a || fpIsNaN b || fpIsNaN c
]
traverse_ (\(o, r, (a, b, c)) -> SameFPObj (o r a b c) @?= fpNaN) $
[ (o, r, (a, b, c))
| o <- op,
r <- roundingMode,
(a, b, c) <- operands
],
testCase "fpAdd" $ do
let v = 60 :: FP 4 4
fpAdd rne 2 v @?= 64
fpAdd rna 2 v @?= 64
fpAdd rne (-2) v @?= 56
fpAdd rna (-2) v @?= 60
fpAdd rtz 2 v @?= 60
fpAdd rtn 2 v @?= 60
fpAdd rtp 2 v @?= 64
fpAdd rne (-2) (-v) @?= -64
fpAdd rna (-2) (-v) @?= -64
fpAdd rtz (-2) (-v) @?= -60
fpAdd rtn (-2) (-v) @?= -64
fpAdd rtp (-2) (-v) @?= -60
fpAdd rne 1 v @?= 60
fpAdd rna 1 v @?= 60
fpAdd rtz 1 v @?= 60
fpAdd rtn 1 v @?= 60
fpAdd rtp 1 v @?= 64
fpAdd rne (-1) (-v) @?= -60
fpAdd rna (-1) (-v) @?= -60
fpAdd rtz (-1) (-v) @?= -60
fpAdd rtn (-1) (-v) @?= -64
fpAdd rtp (-1) (-v) @?= -60
fpAdd rne 3 v @?= 64
fpAdd rna 3 v @?= 64
fpAdd rtz 3 v @?= 60
fpAdd rtn 3 v @?= 60
fpAdd rtp 3 v @?= 64
fpAdd rne (-3) (-v) @?= -64
fpAdd rna (-3) (-v) @?= -64
fpAdd rtz (-3) (-v) @?= -60
fpAdd rtn (-3) (-v) @?= -64
fpAdd rtp (-3) (-v) @?= -60
],
testGroup "ConvertibleBound" $ do
let test ::
forall n eb sb.
( ValidFP eb sb,
KnownNat n,
1 <= n,
SBV.BVIsNonZero n
) =>
Test
test =
testGroup
( "n="
<> show (typeRep @n)
<> ",eb="
<> show (typeRep @eb)
<> ",sb="
<> show (typeRep @sb)
)
$ do
let tcase ::
forall (bv :: Nat -> Type) (sbvbv :: Nat -> Type).
( ConvertibleBound bv,
Num (bv n),
SBV.HasKind (sbvbv n),
Num (SBV.SBV (sbvbv n)),
Typeable bv
) =>
Test
tcase = testCase (show $ typeRep @bv) $ do
let lb =
convertibleLowerBound (0 :: bv n) RTP :: FP eb sb
let rb =
convertibleUpperBound (0 :: bv n) RTP :: FP eb sb
let lbad = prevFP lb
let rbad = nextFP rb
let sbvlb = conSBVTerm lb
let sbvrb = conSBVTerm rb
let sbvlbad = conSBVTerm lbad
let sbvrbad = conSBVTerm rbad
let sbvlbbv =
genericFPCast SBV.sRTP sbvlb :: SBV.SBV (sbvbv n)
let sbvrbbv =
genericFPCast SBV.sRTP sbvrb :: SBV.SBV (sbvbv n)
let sbvlbadbv =
genericFPCast
SBV.sRTP
sbvlbad ::
SBV.SBV (sbvbv n)
let sbvrbadbv =
genericFPCast
SBV.sRTP
sbvrbad ::
SBV.SBV (sbvbv n)
SBV.SatResult (Unsatisfiable {}) <-
SBV.sat (sbvlbbv SBV..== 1)
SBV.SatResult (Unsatisfiable {}) <-
SBV.sat (sbvrbbv SBV..== 1)
SBV.SatResult (Satisfiable {}) <-
SBV.sat (sbvlbadbv SBV..== 1)
SBV.SatResult (Satisfiable {}) <-
SBV.sat (sbvrbadbv SBV..== 1)
return ()
[tcase @IntN @SBV.IntN, tcase @WordN @SBV.WordN]
[ test @12 @4 @16,
test @12 @4 @14,
test @12 @4 @13,
test @12 @4 @12,
test @12 @4 @11,
test @12 @4 @10,
test @12 @4 @9,
test @12 @4 @2,
test @10 @4 @16,
test @10 @4 @12,
test @10 @4 @11,
test @10 @4 @10,
test @10 @4 @9,
test @10 @4 @8,
test @10 @4 @7,
test @10 @4 @2,
test @9 @4 @16,
test @9 @4 @11,
test @9 @4 @10,
test @9 @4 @9,
test @9 @4 @8,
test @9 @4 @7,
test @9 @4 @6,
test @9 @4 @2,
test @8 @4 @16,
test @8 @4 @10,
test @8 @4 @9,
test @8 @4 @8,
test @8 @4 @7,
test @8 @4 @6,
test @8 @4 @5,
test @8 @4 @2,
test @7 @4 @16,
test @7 @4 @9,
test @7 @4 @8,
test @7 @4 @7,
test @7 @4 @6,
test @7 @4 @5,
test @7 @4 @3,
test @7 @4 @2,
test @6 @4 @16,
test @6 @4 @8,
test @6 @4 @7,
test @6 @4 @6,
test @6 @4 @5,
test @6 @4 @3,
test @6 @4 @2,
test @5 @4 @16,
test @5 @4 @7,
test @5 @4 @6,
test @5 @4 @5,
test @5 @4 @3,
test @5 @4 @2
],
testGroup "IEEEFPConvertible" $ do
let safeFromFPComplianceTest ::
forall v.
( Show v,
Eq v,
Arbitrary v,
SafeFromFP
NotRepresentableFPError
v
(FP 4 4)
FPRoundingMode
(Either NotRepresentableFPError)
) =>
Test
safeFromFPComplianceTest = testProperty "safeFromFP" $
\(d :: v) (md :: FPRoundingMode) (v :: FP 4 4) -> do
let s = safeFromFP md v :: Either NotRepresentableFPError v
case s of
Left _ -> fromFPOr d md v == d
Right r -> fromFPOr d md v == r
[ testGroup
"AlgReal"
[ testCase "fromFPOr" $ do
fromFPOr (1 :: AlgReal) rne (fpPositiveZero :: FP 4 4) @?= 0
fromFPOr (1 :: AlgReal) rne (fpNegativeZero :: FP 4 4) @?= 0
fromFPOr (1 :: AlgReal) rne (fpPositiveInfinite :: FP 4 4) @?= 1
fromFPOr (1 :: AlgReal) rne (fpNegativeInfinite :: FP 4 4) @?= 1
fromFPOr (1 :: AlgReal) rne (fpNaN :: FP 4 4) @?= 1
fromFPOr (1 :: AlgReal) rne (3.75 :: FP 4 4)
@?= AlgExactRational (15 % 4),
safeFromFPComplianceTest @AlgReal,
testCase "toFP" $ do
toFP rne (AlgExactRational (15 % 4)) @?= (3.75 :: FP 4 4)
toFP rne (AlgExactRational (15 % 8)) @?= (1.875 :: FP 4 4)
toFP rne (AlgExactRational (17 % 8)) @?= (2 :: FP 4 4)
toFP rna (AlgExactRational (17 % 8)) @?= (2.25 :: FP 4 4)
toFP rtz (AlgExactRational (17 % 8)) @?= (2 :: FP 4 4)
toFP rtp (AlgExactRational (17 % 8)) @?= (2.25 :: FP 4 4)
toFP rtn (AlgExactRational (17 % 8)) @?= (2 :: FP 4 4)
toFP rne (AlgExactRational (-(17 % 8))) @?= (-2 :: FP 4 4)
toFP rna (AlgExactRational (-(17 % 8))) @?= (-2.25 :: FP 4 4)
toFP rtz (AlgExactRational (-(17 % 8))) @?= (-2 :: FP 4 4)
toFP rtp (AlgExactRational (-(17 % 8))) @?= (-2 :: FP 4 4)
toFP rtn (AlgExactRational (-(17 % 8))) @?= (-2.25 :: FP 4 4)
],
testGroup "FP" $ do
let tcase name func = testCase name $ do
mapM_
( \rm -> do
assertBool "+0" $
fpIsPositiveZero
(func rm (fpPositiveZero :: FP 6 6) :: FP 4 4)
assertBool "-0" $
fpIsNegativeZero (func rm (fpNegativeZero :: FP 6 6))
assertBool "+oo" $
fpIsPositiveInfinite
(func rm (fpPositiveInfinite :: FP 6 6))
assertBool "-oo" $
fpIsNegativeInfinite
(func rm (fpNegativeInfinite :: FP 6 6))
assertBool "nan" $
fpIsNaN (func rm (fpNaN :: FP 6 6))
)
[rna, rne, rtz, rtn, rtp]
let posfps = (/ 16) . fromIntegral <$> [48 .. 56] :: [FP 6 6]
let fps = (negate <$> posfps) <> posfps
let rnaExpected =
[3, 3, 3.25, 3.25, 3.25, 3.25, 3.5, 3.5, 3.5]
func rna <$> fps @?= (negate <$> rnaExpected) <> rnaExpected
let rneExpected =
[3, 3, 3, 3.25, 3.25, 3.25, 3.5, 3.5, 3.5]
func rne <$> fps @?= (negate <$> rneExpected) <> rneExpected
let rtzExpected =
[3, 3, 3, 3, 3.25, 3.25, 3.25, 3.25, 3.5]
func rtz <$> fps @?= (negate <$> rtzExpected) <> rtzExpected
let rtnExpected =
[3, 3, 3, 3, 3.25, 3.25, 3.25, 3.25, 3.5]
let rtpExpected =
[3, 3.25, 3.25, 3.25, 3.25, 3.5, 3.5, 3.5, 3.5]
func rtn <$> fps @?= (negate <$> rtpExpected) <> rtnExpected
func rtp <$> fps @?= (negate <$> rtnExpected) <> rtpExpected
[ tcase "fromFPOr" (fromFPOr 2),
tcase "toFP" toFP
],
testGroup "Integrals" $ do
let fps = (/ 4) . fromIntegral <$> [-7 .. 7] :: [FP 4 4]
let rneFromExpected :: (Num a) => [a]
rneFromExpected =
[-2, -2, -1, -1, -1, 0, 0, 0, 0, 0, 1, 1, 1, 2, 2]
rnaFromExpected :: (Num a) => [a]
rnaFromExpected =
[-2, -2, -1, -1, -1, -1, 0, 0, 0, 1, 1, 1, 1, 2, 2]
rtpFromExpected :: (Num a) => [a]
rtpFromExpected =
[-1, -1, -1, -1, 0, 0, 0, 0, 1, 1, 1, 1, 2, 2, 2]
rtnFromExpected :: (Num a) => [a]
rtnFromExpected =
[-2, -2, -2, -1, -1, -1, -1, 0, 0, 0, 0, 1, 1, 1, 1]
rtzFromExpected :: (Num a) => [a]
rtzFromExpected =
[-1, -1, -1, -1, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1]
let posints :: (Num a, Enum a) => [a]
posints = [30 .. 40]
ints :: (Num a, Enum a) => [a]
ints = (negate <$> posints) <> posints
let rnePosToFPExpected =
[30 :: FP 4 4, 32, 32, 32, 32, 36, 36, 36, 40, 40, 40]
let rnaPosToFPExpected =
[30 :: FP 4 4, 32, 32, 32, 36, 36, 36, 36, 40, 40, 40]
let rtzPosToFPExpected =
[30 :: FP 4 4, 30, 32, 32, 32, 32, 36, 36, 36, 36, 40]
let rtnPosToFPExpected =
[30 :: FP 4 4, 30, 32, 32, 32, 32, 36, 36, 36, 36, 40]
let rtpPosToFPExpected =
[30 :: FP 4 4, 32, 32, 36, 36, 36, 36, 40, 40, 40, 40]
let rneToFPExpected =
fmap negate rnePosToFPExpected <> rnePosToFPExpected
let rnaToFPExpected =
fmap negate rnaPosToFPExpected <> rnaPosToFPExpected
let rtzToFPExpected =
fmap negate rtzPosToFPExpected <> rtzPosToFPExpected
let rtnToFPExpected =
fmap negate rtpPosToFPExpected <> rtnPosToFPExpected
let rtpToFPExpected =
fmap negate rtnPosToFPExpected <> rtpPosToFPExpected
let boundTest0 ::
forall bv n eb sb.
( ValidFP eb sb,
KnownNat n,
1 <= n,
ConvertibleBound bv,
IEEEFPConvertible (bv n) (FP eb sb) FPRoundingMode,
Eq (bv n),
Show (bv n)
) =>
String ->
bv n ->
[bv n] ->
[bv n] ->
Test
boundTest0 name d lbvs rbvs = testGroup name $ do
(rm, lbv, rbv) <- zip3 [rne, rna, rtz, rtn, rtp] lbvs rbvs
return $ testCase (show rm) $ do
let (lb :: FP eb sb) = convertibleLowerBound d rm
let (rb :: FP eb sb) = convertibleUpperBound d rm
let lbad = prevFP lb
let rbad = nextFP rb
fromFPOr d rm lbad @?= d
fromFPOr d rm rbad @?= d
fromFPOr d rm lb @?= lbv
fromFPOr d rm rb @?= rbv
let boundTest ::
forall bv n eb sb.
( ValidFP eb sb,
KnownNat n,
1 <= n,
ConvertibleBound bv,
IEEEFPConvertible (bv n) (FP eb sb) FPRoundingMode,
Eq (bv n),
Show (bv n)
) =>
String ->
bv n ->
bv n ->
bv n ->
Test
boundTest name d lbv rbv =
boundTest0 @bv @n @eb @sb
name
d
(replicate 5 lbv)
(replicate 5 rbv)
[ testGroup
"Integer"
[ testCase "fromFPOr" $ do
fromFPOr (1 :: Integer) rne (fpPositiveZero :: FP 4 4) @?= 0
fromFPOr (1 :: Integer) rne (fpNegativeZero :: FP 4 4) @?= 0
fromFPOr (1 :: Integer) rne (fpPositiveInfinite :: FP 4 4)
@?= 1
fromFPOr (1 :: Integer) rne (fpNegativeInfinite :: FP 4 4)
@?= 1
fromFPOr (1 :: Integer) rne (fpNaN :: FP 4 4) @?= 1
fromFPOr (100 :: Integer) rne <$> fps @?= rneFromExpected
fromFPOr (100 :: Integer) rna <$> fps @?= rnaFromExpected
fromFPOr (100 :: Integer) rtp <$> fps @?= rtpFromExpected
fromFPOr (100 :: Integer) rtn <$> fps @?= rtnFromExpected
fromFPOr (100 :: Integer) rtz <$> fps @?= rtzFromExpected,
safeFromFPComplianceTest @Integer,
testCase "toFP" $ do
toFP rne (15 :: Integer) @?= (15 :: FP 4 4)
toFP rne <$> (ints :: [Integer]) @?= rneToFPExpected
toFP rna <$> (ints :: [Integer]) @?= rnaToFPExpected
toFP rtz <$> (ints :: [Integer]) @?= rtzToFPExpected
toFP rtn <$> (ints :: [Integer]) @?= rtnToFPExpected
toFP rtp <$> (ints :: [Integer]) @?= rtpToFPExpected
],
testGroup
"IntN"
[ testCase "fromFPOr" $ do
fromFPOr (1 :: IntN 32) rne (fpPositiveZero :: FP 4 4) @?= 0
fromFPOr (1 :: IntN 32) rne (fpNegativeZero :: FP 4 4) @?= 0
fromFPOr (1 :: IntN 32) rne (fpPositiveInfinite :: FP 4 4)
@?= 1
fromFPOr (1 :: IntN 32) rne (fpNegativeInfinite :: FP 4 4)
@?= 1
fromFPOr (1 :: IntN 32) rne (fpNaN :: FP 4 4) @?= 1
fromFPOr (100 :: IntN 32) rne <$> fps @?= rneFromExpected
fromFPOr (100 :: IntN 32) rna <$> fps @?= rnaFromExpected
fromFPOr (100 :: IntN 32) rtp <$> fps @?= rtpFromExpected
fromFPOr (100 :: IntN 32) rtn <$> fps @?= rtnFromExpected
fromFPOr (100 :: IntN 32) rtz <$> fps @?= rtzFromExpected
fromFPOr (0 :: IntN 3) rne (-3.5 :: FP 4 4) @?= -4
fromFPOr (0 :: IntN 3) rne (3.5 :: FP 4 4) @?= 0
fromFPOr (0 :: IntN 3) rna (-3.5 :: FP 4 4) @?= -4
fromFPOr (0 :: IntN 3) rna (3.5 :: FP 4 4) @?= 0
fromFPOr (0 :: IntN 3) rne (-4.5 :: FP 4 4) @?= -4
fromFPOr (0 :: IntN 3) rne (4.5 :: FP 4 4) @?= 0
fromFPOr (0 :: IntN 3) rna (-4.5 :: FP 4 4) @?= 0
fromFPOr (0 :: IntN 3) rna (4.5 :: FP 4 4) @?= 0,
safeFromFPComplianceTest @(IntN 3),
testGroup "ConvertibleBound" $ do
[ boundTest0 @IntN @12 @4 @16
"ebn<n-1&&sb>n-1,12/4/16"
100
[-256, -256, -255, -256, -255]
[256, 256, 255, 255, 256],
boundTest0 @IntN @12 @4 @12
"ebn<n-1&&sb>n-1,12/4/12"
100
[-256, -256, -255, -256, -255]
[256, 256, 255, 255, 256],
boundTest0 @IntN @12 @4 @11
"ebn<n-1&&sb==n-1,12/4/11"
100
[-256, -256, -255, -256, -255]
[256, 256, 255, 255, 256],
boundTest0 @IntN @12 @4 @10
"ebn<n-1&&sb<n-1,12/4/10"
100
[-256, -256, -255, -256, -255]
[256, 256, 255, 255, 256],
boundTest0 @IntN @12 @4 @9
"ebn<n-1&&sb<n-1,12/4/9"
100
[-256, -256, -255, -256, -255]
[256, 256, 255, 255, 256],
boundTest @IntN @12 @4 @2
"ebn<n-1&&sb<n-1,12/4/2"
100
(-192)
192,
boundTest0 @IntN @10 @4 @16
"ebn<n-1&&sb>n-1,10/4/16"
100
[-256, -256, -255, -256, -255]
[256, 256, 255, 255, 256],
boundTest0 @IntN @10 @4 @11
"ebn<n-1&&sb>n-1,10/4/10"
100
[-256, -256, -255, -256, -255]
[256, 256, 255, 255, 256],
boundTest0 @IntN @10 @4 @10
"ebn<n-1&&sb==n-1,10/4/9"
100
[-256, -256, -255, -256, -255]
[256, 256, 255, 255, 256],
boundTest @IntN @10 @4 @8
"ebn<n-1&&sb<n-1,10/4/8"
100
(-255)
255,
boundTest @IntN @10 @4 @7
"ebn<n-1&&sb<n-1,10/4/7"
100
(-254)
254,
boundTest @IntN @10 @4 @2
"ebn<n-1&&sb<n-1,10/4/2"
100
(-192)
192,
boundTest0 @IntN @9 @4 @16
"ebn==n-1&&sb>n-1,9/4/16"
100
[-256, -256, -255, -256, -255]
[255, 255, 255, 255, 255],
boundTest0 @IntN @9 @4 @9
"ebn==n-1&&sb>n-1,9/4/9"
100
[-256, -256, -255, -256, -255]
[255, 255, 255, 255, 255],
boundTest @IntN @9 @4 @8
"ebn==n-1&&sb==n-1,9/4/8"
100
(-255)
255,
boundTest @IntN @9 @4 @7
"ebn==n-1&&sb<n-1,9/4/7"
100
(-254)
254,
boundTest @IntN @9 @4 @2
"ebn==n-1&&sb<n-1,9/4/2"
100
(-192)
192,
boundTest @IntN @8 @4 @16
"ebn>n-1&&sb>n-1,8/4/16"
100
(-128)
127,
boundTest @IntN @8 @4 @8
"ebn>n-1&&sb>n-1,8/4/8"
100
(-128)
127,
boundTest @IntN @8 @4 @7
"ebn>n-1&&sb==n-1,8/4/7"
100
(-128)
127,
boundTest @IntN @8 @4 @6
"ebn>n-1&&sb<n-1,8/4/6"
100
(-128)
126,
boundTest @IntN @8 @4 @5
"ebn>n-1&&sb<n-1,8/4/5"
100
(-128)
124,
boundTest @IntN @8 @4 @2
"ebn>n-1&&sb<n-1,8/4/2"
100
(-128)
96,
boundTest @IntN @7 @4 @16
"ebn>n-1&&sb>n-1,7/4/16"
100
(-64)
63,
boundTest @IntN @7 @4 @7
"ebn>n-1&&sb>n-1,7/4/7"
100
(-64)
63,
boundTest @IntN @7 @4 @6
"ebn>n-1&&sb==n-1,7/4/6"
100
(-64)
63,
boundTest @IntN @7 @4 @5
"ebn>n-1&&sb<n-1,7/4/5"
100
(-64)
62,
boundTest @IntN @7 @4 @4
"ebn>n-1&&sb<n-1,7/4/4"
100
(-64)
60,
boundTest @IntN @7 @4 @2
"ebn>n-1&&sb<n-1,7/4/2"
100
(-64)
48,
boundTest @IntN @5 @4 @16
"ebn>n-1&&sb>n-1,5/4/16"
100
(-16)
15,
boundTest @IntN @5 @4 @5
"ebn>n-1&&sb>n-1,5/4/5"
100
(-16)
15,
boundTest @IntN @5 @4 @4
"ebn>n-1&&sb==n-1,5/4/4"
100
(-16)
15,
boundTest @IntN @5 @4 @3
"ebn>n-1&&sb<n-1,5/4/3"
100
(-16)
14,
boundTest @IntN @5 @4 @2
"ebn>n-1&&sb<n-1,5/4/2"
100
(-16)
12
],
testCase "toFP" $ do
toFP rne (15 :: IntN 32) @?= (15 :: FP 4 4)
toFP rne <$> (ints :: [IntN 32]) @?= rneToFPExpected
toFP rna <$> (ints :: [IntN 32]) @?= rnaToFPExpected
toFP rtz <$> (ints :: [IntN 32]) @?= rtzToFPExpected
toFP rtn <$> (ints :: [IntN 32]) @?= rtnToFPExpected
toFP rtp <$> (ints :: [IntN 32]) @?= rtpToFPExpected
],
testGroup
"WordN"
[ testCase "fromFPOr" $ do
fromFPOr (1 :: WordN 32) rne (fpPositiveZero :: FP 4 4)
@?= 0
fromFPOr (1 :: WordN 32) rne (fpNegativeZero :: FP 4 4)
@?= 0
fromFPOr (1 :: WordN 32) rne (fpPositiveInfinite :: FP 4 4)
@?= 1
fromFPOr (1 :: WordN 32) rne (fpNegativeInfinite :: FP 4 4)
@?= 1
fromFPOr (1 :: WordN 32) rne (fpNaN :: FP 4 4) @?= 1
let m = fmap (min 100)
fromFPOr (100 :: WordN 32) rne <$> fps @?= m rneFromExpected
fromFPOr (100 :: WordN 32) rna <$> fps @?= m rnaFromExpected
fromFPOr (100 :: WordN 32) rtp <$> fps @?= m rtpFromExpected
fromFPOr (100 :: WordN 32) rtn <$> fps @?= m rtnFromExpected
fromFPOr (100 :: WordN 32) rtz
<$> fps
@?= m rtzFromExpected
fromFPOr (4 :: WordN 3) rne (-0.5 :: FP 4 4) @?= 0
fromFPOr (4 :: WordN 3) rne (0.5 :: FP 4 4) @?= 0
fromFPOr (4 :: WordN 3) rna (-0.5 :: FP 4 4) @?= 4
fromFPOr (4 :: WordN 3) rna (0.5 :: FP 4 4) @?= 1
fromFPOr (4 :: WordN 3) rne (6.5 :: FP 4 4) @?= 6
fromFPOr (4 :: WordN 3) rne (7.5 :: FP 4 4) @?= 4
fromFPOr (4 :: WordN 3) rna (6.5 :: FP 4 4) @?= 7
fromFPOr (4 :: WordN 3) rna (7.5 :: FP 4 4) @?= 4,
safeFromFPComplianceTest @(WordN 3),
testGroup "ConvertibleBound" $ do
[ boundTest0 @WordN @12 @4 @16
"ebn<n&&sb>n,12/4/16"
100
[0, 0, 0, 0, 0]
[256, 256, 255, 255, 256],
boundTest0 @WordN @12 @4 @13
"ebn<n&&sb>n,12/4/13"
100
[0, 0, 0, 0, 0]
[256, 256, 255, 255, 256],
boundTest0 @WordN @12 @4 @12
"ebn<n&&sb==n,12/4/12"
100
[0, 0, 0, 0, 0]
[256, 256, 255, 255, 256],
boundTest0 @WordN @12 @4 @11
"ebn<n&&sb<n,12/4/11"
100
[0, 0, 0, 0, 0]
[256, 256, 255, 255, 256],
boundTest @WordN @12 @4 @2 "ebn<n&&sb<n,12/4/2" 100 0 192,
boundTest0 @WordN @9 @4 @16
"ebn<n&&sb>n,9/4/16"
100
[0, 0, 0, 0, 0]
[256, 256, 255, 255, 256],
boundTest0 @WordN @9 @4 @10
"ebn<n&&sb>n,9/4/10"
100
[0, 0, 0, 0, 0]
[256, 256, 255, 255, 256],
boundTest0 @WordN @9 @4 @9
"ebn<n&&sb==n,9/4/9"
100
[0, 0, 0, 0, 0]
[256, 256, 255, 255, 256],
boundTest @WordN @9 @4 @8 "ebn<n&&sb<n,9/4/8" 100 0 255,
boundTest @WordN @9 @4 @2 "ebn<n&&sb<n,9/4/2" 100 0 192,
boundTest @WordN @8 @4 @16
"ebn==n&&sb>n,8/4/16"
100
0
255,
boundTest @WordN @8 @4 @9 "ebn==n&&sb>n,8/4/16" 100 0 255,
boundTest @WordN @8 @4 @9 "ebn==n&&sb>n,8/4/9" 100 0 255,
boundTest @WordN @8 @4 @8 "ebn==n&&sb==n,8/4/8" 100 0 255,
boundTest @WordN @8 @4 @7 "ebn==n&&sb<n,8/4/7" 100 0 254,
boundTest @WordN @8 @4 @2 "ebn==n&&sb<n,8/4/2" 100 0 192,
boundTest @WordN @7 @4 @16 "ebn>n&&sb>n,7/4/16" 100 0 127,
boundTest @WordN @7 @4 @8 "ebn>n&&sb>n,7/4/8" 100 0 127,
boundTest @WordN @7 @4 @7 "ebn>n&&sb==n,7/4/7" 100 0 127,
boundTest @WordN @7 @4 @6 "ebn>n&&sb<n,7/4/6" 100 0 126,
boundTest @WordN @7 @4 @2 "ebn>n&&sb<n,7/4/2" 100 0 96,
boundTest @WordN @5 @4 @16 "ebn>n&&sb>n,7/4/16" 100 0 31,
boundTest @WordN @5 @4 @6 "ebn>n&&sb>n,5/4/6" 100 0 31,
boundTest @WordN @5 @4 @5 "ebn>n&&sb==n,5/4/5" 100 0 31,
boundTest @WordN @5 @4 @4 "ebn>n&&sb<n,5/4/4" 100 0 30,
boundTest @WordN @5 @4 @2 "ebn>n&&sb<n,5/4/2" 100 0 24
],
testCase "toFP" $ do
toFP rne (15 :: WordN 32) @?= (15 :: FP 4 4)
toFP rne <$> (posints :: [WordN 32]) @?= rnePosToFPExpected
toFP rna <$> (posints :: [WordN 32]) @?= rnaPosToFPExpected
toFP rtz <$> (posints :: [WordN 32]) @?= rtzPosToFPExpected
toFP rtn <$> (posints :: [WordN 32]) @?= rtnPosToFPExpected
toFP rtp <$> (posints :: [WordN 32]) @?= rtpPosToFPExpected
]
]
]
]
newtype SameFPObj = SameFPObj FP32 deriving newtype (Show, Num, IEEEFPConstants)
instance Eq SameFPObj where
SameFPObj a == SameFPObj b
| a == 0 && b == 0 =
fpIsPositiveZero a == fpIsPositiveZero b
SameFPObj a == SameFPObj b | fpIsNaN a && fpIsNaN b = True
SameFPObj a == SameFPObj b = a == b