toki/idris2-ratio
1
0
Fork 0
Code Issues Pull requests Activity

Make inequality comparison slightly more efficient

Browse source
This commit is contained in:
Kiana Sheibani 2024-06-07 02:08:02 -04:00
parent 80e43be8fc
commit e21b81b965
Signed by: toki
GPG key ID: 6CB106C25E86A9F7
1 changed files with 6 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/Data/Ratio.idr
View file

@ -1,5 +1,6 @@
module Data.Ratio
import Data.Bool.Xor
import Data.Maybe
import Data.So
import Data.IntegralGCD
@ -102,12 +103,12 @@ Eq a => Eq (Ratio a) where
export
(Ord a, Num a) => Ord (Ratio a) where
compare (MkRatio n d) (MkRatio m b) =
flipIfNeg (b*d) $ compare (n*b) (m*d)
flipIf (b >= 0 `xor` d >= 0) $ compare (n*b) (m*d)
where
flipIfNeg : a -> Ordering -> Ordering
flipIfNeg x EQ = EQ
flipIfNeg x LT = if x >= 0 then LT else GT
flipIfNeg x GT = if x >= 0 then GT else LT
flipIf : Bool -> Ordering -> Ordering
flipIf _ EQ = EQ
flipIf b LT = if b then GT else LT
flipIf b GT = if b then LT else GT
export
Show a => Show (Ratio a) where