From 0c45513a4f44807e4828d40f0698c863495453ab Mon Sep 17 00:00:00 2001 From: Sirui Lu Date: Thu, 6 Jun 2024 13:40:39 -0700 Subject: [PATCH 1/2] Fix the Ord instance for FP and FloatingPoint --- Data/SBV/Core/SizedFloats.hs | 21 +++++++++++++++++++-- 1 file changed, 19 insertions(+), 2 deletions(-) diff --git a/Data/SBV/Core/SizedFloats.hs b/Data/SBV/Core/SizedFloats.hs index ba6b51e04..d6b2b0461 100644 --- a/Data/SBV/Core/SizedFloats.hs +++ b/Data/SBV/Core/SizedFloats.hs @@ -56,7 +56,13 @@ import qualified Data.Generics as G -- DP is @FloatingPoint 11 53@ -- etc. newtype FloatingPoint (eb :: Nat) (sb :: Nat) = FloatingPoint FP - deriving (Eq, Ord) + deriving (Eq) + +instance Ord (FloatingPoint eb sb) where + FloatingPoint f0 < FloatingPoint f1 = f0 < f1 + FloatingPoint f0 <= FloatingPoint f1 = f0 <= f1 + f0 > f1 = f1 < f0 + f0 >= f1 = f1 <= f0 -- | Abbreviation for IEEE half precision float, bit width 16 = 5 + 11. type FPHalf = FloatingPoint 5 11 @@ -87,7 +93,18 @@ data FP = FP { fpExponentSize :: Int , fpSignificandSize :: Int , fpValue :: BigFloat } - deriving (Ord, Eq, G.Data) + deriving (Eq, G.Data) + +-- Manually implemented instance as GHC generated a non-IEEE 754 compliant instance. +-- Note that we cannot pack the values in a tuple and then compare them as that will +-- also give non-IEEE 754 compilant results. +instance Ord FP where + FP eb0 sb0 v0 < FP eb1 sb1 v1 = + eb0 < eb1 || (eb0 == eb1 && (sb0 < sb1 || (sb0 == sb1 && v0 < v1))) + FP eb0 sb0 v0 <= FP eb1 sb1 v1 = + eb0 < eb1 || (eb0 == eb1 && (sb0 < sb1 || (sb0 == sb1 && v0 <= v1))) + f0 > f1 = f1 < f0 + f0 >= f1 = f1 <= f0 instance Show FP where show = bfRemoveRedundantExp . bfToString 10 False False From 5e4d0551f8b05f63e2acfd65176280b973ebcfc5 Mon Sep 17 00:00:00 2001 From: Sirui Lu Date: Thu, 6 Jun 2024 14:03:36 -0700 Subject: [PATCH 2/2] Throw error on comparing FPs with different precisions --- Data/SBV/Core/SizedFloats.hs | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/Data/SBV/Core/SizedFloats.hs b/Data/SBV/Core/SizedFloats.hs index d6b2b0461..3ec2de74b 100644 --- a/Data/SBV/Core/SizedFloats.hs +++ b/Data/SBV/Core/SizedFloats.hs @@ -99,10 +99,14 @@ data FP = FP { fpExponentSize :: Int -- Note that we cannot pack the values in a tuple and then compare them as that will -- also give non-IEEE 754 compilant results. instance Ord FP where - FP eb0 sb0 v0 < FP eb1 sb1 v1 = - eb0 < eb1 || (eb0 == eb1 && (sb0 < sb1 || (sb0 == sb1 && v0 < v1))) - FP eb0 sb0 v0 <= FP eb1 sb1 v1 = - eb0 < eb1 || (eb0 == eb1 && (sb0 < sb1 || (sb0 == sb1 && v0 <= v1))) + FP eb0 sb0 v0 < FP eb1 sb1 v1 + | eb0 /= eb1 || sb0 /= sb1 = + error $ "FP.<: comparing FPs with different precision: " <> show (eb0, sb0) <> show (eb1, sb1) + | otherwise = v0 < v1 + FP eb0 sb0 v0 <= FP eb1 sb1 v1 + | eb0 /= eb1 || sb0 /= sb1 = + error $ "FP.<=: comparing FPs with different precision: " <> show (eb0, sb0) <> show (eb1, sb1) + | otherwise = v0 <= v1 f0 > f1 = f1 < f0 f0 >= f1 = f1 <= f0