Compare commits

..

10 commits

4 changed files with 66 additions and 37 deletions

View file

@ -1,6 +1,6 @@
MIT License
Copyright (c) 2022 Kiana Sheibani
Copyright (c) 2024 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

View file

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

View file

@ -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 assert_total $ gcd y (x `mod` y)
else gcd y (assert_smaller y $ x `mod` y)
export IntegralGCD Integer where

View file

@ -1,5 +1,6 @@
module Data.Ratio
import Data.Bool.Xor
import Data.Maybe
import Data.So
import Data.IntegralGCD
@ -25,35 +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)
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
@ -78,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
@ -87,12 +99,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
@ -120,3 +132,18 @@ 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