LICENSE

@@ -1,6 +1,6 @@
 MIT License
 
-Copyright (c) 2024 Kiana Sheibani
+Copyright (c) 2022 Kiana Sheibani
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

ratio.ipkg

@@ -1,5 +1,4 @@
 package ratio
-brief = "Arbitrary-precision ratio types"
 version = 1.0.0
 
 authors = "Kiana Sheibani"
@@ -8,5 +7,4 @@ license = "MIT"
 sourcedir = "src"
 readme = "README.md"
 
-modules = Data.Ratio,
-          Data.IntegralGCD
+modules = Data.Ratio

src/Data/IntegralGCD.idr

@@ -18,7 +18,7 @@ interface (Eq a, Integral a) => IntegralGCD a where
   gcd x y =
     if x == 0 then y
     else if y == 0 then x
-    else gcd y (assert_smaller y $ x `mod` y)
+    else assert_total $ gcd y (x `mod` y)
 
 
 export IntegralGCD Integer where

src/Data/Ratio.idr

@@ -1,6 +1,5 @@
 module Data.Ratio
 
-import Data.Bool.Xor
 import Data.Maybe
 import Data.So
 import Data.IntegralGCD
@@ -26,6 +25,35 @@ Rational : Type
 Rational = Ratio Integer
 
 
+||| Reduce a ratio by dividing both components by their common factor. Most
+||| operations automatically reduce the returned ratio, so explicitly calling
+||| this function is usually unnecessary.
+export
+reduce : IntegralGCD a => Ratio a -> Ratio a
+reduce (MkRatio n d) =
+  let g = gcd n d in MkRatio (n `div` g) (d `div` g)
+
+
+||| Construct a ratio of two values, returning `Nothing` if the denominator is
+||| zero.
+export
+mkRatioMaybe : IntegralGCD a => (n, d : a) -> Maybe (Ratio a)
+mkRatioMaybe n d = toMaybe (d /= 0) (reduce $ MkRatio n d)
+
+infix 9 //
+
+||| Construct a ratio of two values.
+export
+(//) : IntegralGCD a => (n, d : a) -> {auto 0 ok : So (d /= 0)} -> Ratio a
+(//) n d = reduce $ MkRatio n d
+
+
+||| Round a ratio down to a positive integer.
+export
+floor : Integral a => Ratio a -> a
+floor (MkRatio n d) = n `div` d
+
+
 namespace Ratio
   ||| Return the numerator of the ratio in reduced form.
   export %inline
@@ -50,46 +78,6 @@ namespace Ratio
   (.denom) = dn
 
 
-||| Reduce a ratio by dividing both components by their common factor. Most
-||| operations automatically reduce the returned ratio, so explicitly calling
-||| this function is usually unnecessary.
-export
-reduce : IntegralGCD a => Ratio a -> Ratio a
-reduce (MkRatio n d) =
-  let g = gcd n d in MkRatio (n `div` g) (d `div` g)
-
-||| Construct a ratio of two values, returning `Nothing` if the denominator is
-||| zero.
-export
-mkRatioMaybe : IntegralGCD a => (n, d : a) -> Maybe (Ratio a)
-mkRatioMaybe n d = toMaybe (d /= 0) (reduce $ MkRatio n d)
-
-||| Create a ratio of two values.
-export partial
-mkRatio : IntegralGCD a => (n, d : a) -> Ratio a
-mkRatio n d = case d /= 0 of
-  True => reduce $ MkRatio n d
-
-||| Create a ratio of two values, unsafely assuming that they are coprime and
-||| the denominator is non-zero.
-||| WARNING: This function will behave erratically and may crash your program
-||| if these conditions are not met!
-export %unsafe
-unsafeMkRatio : (n, d : a) -> Ratio a
-unsafeMkRatio = MkRatio
-
-infix 9 //
-
-||| Construct a ratio of two values.
-export
-(//) : IntegralGCD a => (n, d : a) -> {auto 0 ok : So (d /= 0)} -> Ratio a
-(//) n d = reduce $ MkRatio n d
-
-
-||| Round a ratio down to the nearest integer less than it.
-export
-floor : Integral a => Ratio a -> a
-floor (MkRatio n d) = n `div` d
 
 
 export
@@ -99,12 +87,12 @@ Eq a => Eq (Ratio a) where
 export
 (Ord a, Num a) => Ord (Ratio a) where
   compare (MkRatio n d) (MkRatio m b) =
-    flipIf (b >= 0 `xor` d >= 0) $ compare (n*b) (m*d)
+    flipIfNeg (b*d) $ compare (n*b) (m*d)
     where
-      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
+      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
 
 export
 Show a => Show (Ratio a) where
@@ -132,18 +120,3 @@ IntegralGCD a => Fractional (Ratio a) where
   recip (MkRatio n d) = case n /= 0 of True => MkRatio d n
   MkRatio n d / MkRatio m b = case m /= 0 of
     True => reduce $ MkRatio (n*b) (m*d)
-
--- ## Casting
-
-export
-Num a => Cast a (Ratio a) where
-  cast x = MkRatio x 1
-
-export
-Cast a b => Cast (Ratio a) (Ratio b) where
-  cast (MkRatio n d) = MkRatio (cast n) (cast d)
-
--- Special case: `Cast Rational Double`
-export
-(Cast a b, Fractional b) => Cast (Ratio a) b where
-  cast (MkRatio n d) = cast n / cast d