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

Rearrange sections of Data.Ratio module

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

84
src/Data/Ratio.idr
View file

@ -26,50 +26,6 @@ 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)
||| 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 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
@ -94,6 +50,46 @@ 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