Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix the Ord instance for FP and FloatingPoint #701

Merged
merged 2 commits into from
Jun 6, 2024
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 23 additions & 2 deletions Data/SBV/Core/SizedFloats.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -87,7 +93,22 @@ 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 || 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

instance Show FP where
show = bfRemoveRedundantExp . bfToString 10 False False
Expand Down
Loading