0 | module Data.Ratio
  1 |
  2 | import Data.Bool.Xor
  3 | import Data.Maybe
  4 | import Data.So
  5 | import Data.IntegralGCD
  6 |
  7 | %default total
  8 |
  9 |
 10 | ||| Ratio types, represented by a numerator and denominator of type `a`.
 11 | |||
 12 | ||| Most numeric operations require an instance `Integral a` in order to
 13 | ||| simplify the returned ratio and reduce storage space.
 14 | export
 15 | record Ratio a where
 16 |   constructor MkRatio
 17 |   nm, dn : a
 18 |
 19 | ||| Rational numbers, represented as a ratio between
 20 | ||| two arbitrary-precision integers.
 21 | |||
 22 | ||| Rationals can be constructed using `//`.
 23 | public export
 24 | Rational : Type
 25 | Rational = Ratio Integer
 26 |
 27 |
 28 | namespace Ratio
 29 |   ||| Return the numerator of the ratio in reduced form.
 30 |   export %inline
 31 |   numer : Ratio a -> a
 32 |   numer = nm
 33 |
 34 |   ||| Return the numerator of the ratio in reduced form.
 35 |   export %inline
 36 |   (.numer) : Ratio a -> a
 37 |   (.numer) = nm
 38 |
 39 |   ||| Return the denominator of the ratio in reduced form.
 40 |   ||| This value is guaranteed to always be positive.
 41 |   export %inline
 42 |   denom : Ratio a -> a
 43 |   denom = dn
 44 |
 45 |   ||| Return the denominator of the ratio in reduced form.
 46 |   ||| This value is guaranteed to always be positive.
 47 |   export %inline
 48 |   (.denom) : Ratio a -> a
 49 |   (.denom) = dn
 50 |
 51 |
 52 | ||| Reduce a ratio by dividing both components by their common factor. Most
 53 | ||| operations automatically reduce the returned ratio, so explicitly calling
 54 | ||| this function is usually unnecessary.
 55 | export
 56 | reduce : IntegralGCD a => Ratio a -> Ratio a
 57 | reduce (MkRatio n d) =
 58 |   let g = gcd n d in MkRatio (n `div` g) (d `div` g)
 59 |
 60 | ||| Construct a ratio of two values, returning `Nothing` if the denominator is
 61 | ||| zero.
 62 | export
 63 | mkRatioMaybe : IntegralGCD a => (n, d : a) -> Maybe (Ratio a)
 64 | mkRatioMaybe n d = toMaybe (d /= 0) (reduce $ MkRatio n d)
 65 |
 66 | ||| Create a ratio of two values.
 67 | export partial
 68 | mkRatio : IntegralGCD a => (n, d : a) -> Ratio a
 69 | mkRatio n d = case d /= 0 of
 70 |   True => reduce $ MkRatio n d
 71 |
 72 | ||| Create a ratio of two values, unsafely assuming that they are coprime and
 73 | ||| the denominator is non-zero.
 74 | ||| WARNING: This function will behave erratically and may crash your program
 75 | ||| if these conditions are not met!
 76 | export %unsafe
 77 | unsafeMkRatio : (n, d : a) -> Ratio a
 78 | unsafeMkRatio = MkRatio
 79 |
 80 | infix 9 //
 81 |
 82 | ||| Construct a ratio of two values.
 83 | export
 84 | (//) : IntegralGCD a => (n, d : a) -> {auto 0 ok : So (d /= 0)} -> Ratio a
 85 | (//) n d = reduce $ MkRatio n d
 86 |
 87 |
 88 | ||| Round a ratio down to the nearest integer less than it.
 89 | export
 90 | floor : Integral a => Ratio a -> a
 91 | floor (MkRatio n d) = n `div` d
 92 |
 93 |
 94 | export
 95 | Eq a => Eq (Ratio a) where
 96 |   MkRatio n d == MkRatio m b = n == m && d == b
 97 |
 98 | export
 99 | (Ord a, Num a) => Ord (Ratio a) where
100 |   compare (MkRatio n d) (MkRatio m b) =
101 |     flipIf (b >= 0 `xor` d >= 0) $ compare (n*b) (m*d)
102 |     where
103 |       flipIf : Bool -> Ordering -> Ordering
104 |       flipIf _ EQ = EQ
105 |       flipIf b LT = if b then GT else LT
106 |       flipIf b GT = if b then LT else GT
107 |
108 | export
109 | Show a => Show (Ratio a) where
110 |   showPrec p (MkRatio n d) =
111 |     let p' = User 10
112 |     in  showParens (p >= p') (showPrec p' n ++ " // " ++ showPrec p' d)
113 |
114 | export
115 | IntegralGCD a => Num (Ratio a) where
116 |   MkRatio n d + MkRatio m b = reduce $ MkRatio (n*b + m*d) (d*b)
117 |   MkRatio n d * MkRatio m b = reduce $ MkRatio (n*m) (d*b)
118 |   fromInteger x = MkRatio (fromInteger x) 1
119 |
120 | export
121 | (IntegralGCD a, Neg a) => Neg (Ratio a) where
122 |   negate (MkRatio n d) = MkRatio (-n) d
123 |   MkRatio n d - MkRatio m b = reduce $ MkRatio (n*b - m*d) (d*b)
124 |
125 | export
126 | (IntegralGCD a, Abs a) => Abs (Ratio a) where
127 |   abs (MkRatio n d) = MkRatio (abs n) (abs d)
128 |
129 | export
130 | IntegralGCD a => Fractional (Ratio a) where
131 |   recip (MkRatio n d) = case n /= 0 of True => MkRatio d n
132 |   MkRatio n d / MkRatio m b = case m /= 0 of
133 |     True => reduce $ MkRatio (n*b) (m*d)
134 |
135 | -- ## Casting
136 |
137 | export
138 | Num a => Cast a (Ratio a) where
139 |   cast x = MkRatio x 1
140 |
141 | export
142 | Cast a b => Cast (Ratio a) (Ratio b) where
143 |   cast (MkRatio n d) = MkRatio (cast n) (cast d)
144 |
145 | -- Special case: `Cast Rational Double`
146 | export
147 | (Cast a b, Fractional b) => Cast (Ratio a) b where
148 |   cast (MkRatio n d) = cast n / cast d
149 |