{-# 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.Serialize (decode, encode) 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 ), KeyEq (keyEq), 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 keyEq, unaryOpComplianceWithFloat "symFpIsPositive" symFpIsPositive symFpIsPositive keyEq, unaryOpComplianceWithFloat "symFpIsNegative" symFpIsNegative symFpIsNegative keyEq, unaryOpComplianceWithFloat "symFpIsPositiveInfinite" symFpIsPositiveInfinite symFpIsPositiveInfinite keyEq, unaryOpComplianceWithFloat "symFpIsNegativeInfinite" symFpIsNegativeInfinite symFpIsNegativeInfinite keyEq, unaryOpComplianceWithFloat "symFpIsInfinite" symFpIsInfinite symFpIsInfinite keyEq, unaryOpComplianceWithFloat "symFpIsPositiveZero" symFpIsPositiveZero symFpIsPositiveZero keyEq, unaryOpComplianceWithFloat "symFpIsNegativeZero" symFpIsNegativeZero symFpIsNegativeZero keyEq, unaryOpComplianceWithFloat "symFpIsZero" symFpIsZero symFpIsZero keyEq, unaryOpComplianceWithFloat "symFpIsNormal" symFpIsNormal symFpIsNormal keyEq, unaryOpComplianceWithFloat "symFpIsSubnormal" symFpIsSubnormal symFpIsSubnormal keyEq, unaryOpComplianceWithFloat "symFpIsPoint" symFpIsPoint symFpIsPoint keyEq ], 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.SymVal (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 "ebnn-1,12/4/16" 100 [-256, -256, -255, -256, -255] [256, 256, 255, 255, 256], boundTest0 @IntN @12 @4 @12 "ebnn-1,12/4/12" 100 [-256, -256, -255, -256, -255] [256, 256, 255, 255, 256], boundTest0 @IntN @12 @4 @11 "ebnn-1,10/4/16" 100 [-256, -256, -255, -256, -255] [256, 256, 255, 255, 256], boundTest0 @IntN @10 @4 @11 "ebnn-1,10/4/10" 100 [-256, -256, -255, -256, -255] [256, 256, 255, 255, 256], boundTest0 @IntN @10 @4 @10 "ebnn-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&&sbn-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&&sbn-1&&sbn-1&&sbn-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&&sbn-1&&sbn-1&&sbn-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&&sbn-1&&sb (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 "ebnn,12/4/16" 100 [0, 0, 0, 0, 0] [256, 256, 255, 255, 256], boundTest0 @WordN @12 @4 @13 "ebnn,12/4/13" 100 [0, 0, 0, 0, 0] [256, 256, 255, 255, 256], boundTest0 @WordN @12 @4 @12 "ebnn,9/4/16" 100 [0, 0, 0, 0, 0] [256, 256, 255, 255, 256], boundTest0 @WordN @9 @4 @10 "ebnn,9/4/10" 100 [0, 0, 0, 0, 0] [256, 256, 255, 255, 256], boundTest0 @WordN @9 @4 @9 "ebnn,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&&sbn&&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&&sbn&&sbn&&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&&sbn&&sb (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 ] ] ], testProperty "Serialize" $ \(x :: FP 8 24) -> ioProperty $ if isNaN x then case (decode . encode) x of Right (v :: FP 8 24) -> assertBool "Should be NaN" $ fpIsNaN v Left err -> fail err else Right x @?= (decode . encode) x ] 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