From fdbc5b9d69c0dcb17d26c589d81eebfc8543acde Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Sun, 6 Aug 2023 22:10:47 -0400 Subject: [PATCH 01/10] Add unsafe ratio constructor --- src/Data/Ratio.idr | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/Data/Ratio.idr b/src/Data/Ratio.idr index 5487f5c..4caa1c4 100644 --- a/src/Data/Ratio.idr +++ b/src/Data/Ratio.idr @@ -40,6 +40,14 @@ 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. +||| WARNING: This is only safe if the denominator is not zero! +export %unsafe +unsafeMkRatio : (n, d : a) -> Ratio a +unsafeMkRatio = MkRatio + + infix 9 // ||| Construct a ratio of two values. From c1bfc2f042af394da7f9106f79f9bd3fed6d8731 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Sun, 6 Aug 2023 22:18:11 -0400 Subject: [PATCH 02/10] Add partial ratio constructor --- src/Data/Ratio.idr | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/Data/Ratio.idr b/src/Data/Ratio.idr index 4caa1c4..d0a0602 100644 --- a/src/Data/Ratio.idr +++ b/src/Data/Ratio.idr @@ -40,9 +40,16 @@ 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. -||| WARNING: This is only safe if the denominator is not zero! +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 denomindator 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 From 5a6b7cad3f5e213fed8b4cdcedd9d9cfb8dfd7f5 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Sun, 6 Aug 2023 22:19:40 -0400 Subject: [PATCH 03/10] Typo --- src/Data/Ratio.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/Ratio.idr b/src/Data/Ratio.idr index d0a0602..3da1861 100644 --- a/src/Data/Ratio.idr +++ b/src/Data/Ratio.idr @@ -47,7 +47,7 @@ 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 denomindator is non-zero. +||| the denominator is non-zero. ||| WARNING: This function will behave erratically and may crash your program ||| if these conditions are not met! export %unsafe From 42d216fb9890e0b2d78c05ab5394907a3341ce85 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Thu, 6 Jun 2024 20:47:45 -0400 Subject: [PATCH 04/10] Bump copyright year --- LICENSE | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/LICENSE b/LICENSE index 4d48a87..712386e 100644 --- a/LICENSE +++ b/LICENSE @@ -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 From 0dbd3e6bc89decf9c50cef9fc5d1d66a75f1818c Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Thu, 6 Jun 2024 20:51:11 -0400 Subject: [PATCH 05/10] Use assert_smaller instead of assert_total --- src/Data/IntegralGCD.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Data/IntegralGCD.idr b/src/Data/IntegralGCD.idr index 0e2d65d..cd1449b 100644 --- a/src/Data/IntegralGCD.idr +++ b/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 assert_total $ gcd y (x `mod` y) + else gcd y (assert_smaller y $ x `mod` y) export IntegralGCD Integer where From 80e43be8fc348abb5450ce77715be2e6a0144a3f Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 7 Jun 2024 02:07:25 -0400 Subject: [PATCH 06/10] Add casting implementations --- src/Data/Ratio.idr | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/Data/Ratio.idr b/src/Data/Ratio.idr index 3da1861..a2ed86e 100644 --- a/src/Data/Ratio.idr +++ b/src/Data/Ratio.idr @@ -135,3 +135,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 From e21b81b965461e62c04120b5ec39f905058321d1 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 7 Jun 2024 02:08:02 -0400 Subject: [PATCH 07/10] Make inequality comparison slightly more efficient --- src/Data/Ratio.idr | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/Data/Ratio.idr b/src/Data/Ratio.idr index a2ed86e..0c63e27 100644 --- a/src/Data/Ratio.idr +++ b/src/Data/Ratio.idr @@ -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 From 52eb83594b53d23fd388763a74a4cb3ae61540fa Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 7 Jun 2024 02:08:31 -0400 Subject: [PATCH 08/10] Rearrange sections of Data.Ratio module --- src/Data/Ratio.idr | 84 ++++++++++++++++++++++------------------------ 1 file changed, 40 insertions(+), 44 deletions(-) diff --git a/src/Data/Ratio.idr b/src/Data/Ratio.idr index 0c63e27..56dba9f 100644 --- a/src/Data/Ratio.idr +++ b/src/Data/Ratio.idr @@ -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 From d19ae136f7244f8a9463bdc7cf06741c554d3a5d Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Fri, 7 Jun 2024 02:18:53 -0400 Subject: [PATCH 09/10] Add brief description --- ratio.ipkg | 1 + 1 file changed, 1 insertion(+) diff --git a/ratio.ipkg b/ratio.ipkg index 1f426b3..3f97be0 100644 --- a/ratio.ipkg +++ b/ratio.ipkg @@ -1,4 +1,5 @@ package ratio +brief = "Arbitrary-precision ratio types" version = 1.0.0 authors = "Kiana Sheibani" From 1bdfde80d70c1dc63df186e32f7c86ba6545dff2 Mon Sep 17 00:00:00 2001 From: Kiana Sheibani Date: Sat, 8 Jun 2024 14:44:26 -0400 Subject: [PATCH 10/10] Fix module not added to ipkg --- ratio.ipkg | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ratio.ipkg b/ratio.ipkg index 3f97be0..8258a02 100644 --- a/ratio.ipkg +++ b/ratio.ipkg @@ -8,4 +8,5 @@ license = "MIT" sourcedir = "src" readme = "README.md" -modules = Data.Ratio +modules = Data.Ratio, + Data.IntegralGCD