packages feed

kind-rational 0.1 → 0.2

raw patch · 4 files changed

+138/−232 lines, 4 files

Files

CHANGELOG.md view
@@ -1,3 +1,10 @@+# Version 0.2++* COMPILER ASSISTED BREAKING CHANGE: Removed `Mod`, `DivMod`, `mod`, `divMod`.++* COMPILER ASSISTED BREAKING CHANGE: Renamed `Dif` to `Rem`, `DivDif` to+  `DivRem`, `mod` to `rem`, `divDif` to `divRem`.+ # Version 0.1  * Initial version.
kind-rational.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: kind-rational-version: 0.1+version: 0.2 license: BSD-3-Clause license-file: LICENSE extra-source-files: README.md CHANGELOG.md
lib/KindRational.hs view
@@ -52,14 +52,10 @@   , Recip   , Div   , div-  , Mod-  , mod-  , Dif-  , dif-  , DivMod-  , divMod-  , DivDif-  , divDif+  , Rem+  , rem+  , DivRem+  , divRem   , I.Round(..)      -- * Decimals@@ -97,7 +93,7 @@ import KindInteger (type (==?), type (==), type (/=?), type (/=)) import KindInteger qualified as I import Numeric.Natural (Natural)-import Prelude hiding (Rational, Integer, Num, div, mod, divMod)+import Prelude hiding (Rational, Integer, Num, div, rem) import Prelude qualified as P import Text.ParserCombinators.ReadPrec as Read import Text.Read.Lex qualified as Read@@ -162,7 +158,7 @@  -- | Shows the 'Rational' as it appears literally at the type-level. ----- This is different from normal 'show' for 'Rational', which shows+-- This is remerent from normal 'show' for 'Rational', which shows -- the term-level value. -- -- @@@ -211,6 +207,10 @@     max_ :: P.Integer -- Some big enough number. TODO: Pick good number.     max_ = 10 ^ (1000 :: Int) +-- | Like 'unsafeFromPrelude', but returns a "Prelude" 'P.Rational'.+unsafeCheckPrelude :: P.Rational -> P.Rational+unsafeCheckPrelude = toPrelude . unsafeFromPrelude+ -- | Convert a term-level "KindRational" 'Rational' into a term-level -- "Prelude" 'P.Rational'. --@@ -364,116 +364,70 @@ -- @ -- forall (r :: 'I.Round') (a :: 'Rational'). --   ('Den' a '/=' 0) =>---     'Mod' r a  '=='  'Num' a 'I.-' 'P' ('Den' a) 'I.*' 'Div' r a+--     'Rem' r a  '=='  a '-' 'Div' r a '%' 1 -- @+--+-- Use this to approximate a type-level 'Rational' to an 'Integer'. type Div (r :: I.Round) (a :: Rational) =   Div_ r (Normalize a) :: Integer type Div_ (r :: I.Round) (a :: Rational) =   I.Div r (Num_ a) (P (Den_ a)) :: Integer --- | 'Mod'ulus of the division of the 'Num'erator of type-level 'Rational'+-- | 'Rem'ainder from 'Div'iding the 'Num'erator of the type-level 'Rational' -- @a@ by its 'Den'ominator, using the specified 'I.Round'ing @r@. -- -- @ -- forall (r :: 'I.Round') (a :: 'Rational'). --   ('Den' a '/=' 0) =>---     'Mod' r a  '=='  'Num' a 'I.-' 'P' ('Den' a) 'I.*' 'Div' r a--- @-type Mod (r :: I.Round) (a :: Rational) = Snd (DivMod r a) :: Integer---- | Get both the quotient and the 'Mod'ulus of the 'Div'ision of the--- 'Num'erator of type-level 'Rational' @a@ by its 'Den'ominator,--- using the specified 'I.Round'ing @r@.------ @--- forall (r :: 'I.Round') (a :: 'Rational').---   ('Den' a '/=' 0) =>---     'DivMod' r a  '=='  '('Div' r a, 'Mod' r a)--- @-type DivMod (r :: I.Round) (a :: Rational) =-  DivMod_ r (Normalize a) :: (Integer, Integer)-type DivMod_ (r :: I.Round) (a :: Rational) =-  I.DivMod r (Num_ a) (P (Den_ a)) :: (Integer, Integer)---- | 'Dif'ference of the type-level 'Rational' @a@ and the 'Div'ision of--- its 'Num'erator by its 'Den'ominator, using the specified 'I.Round'ing @r@.------ @--- forall (r :: 'I.Round') (a :: 'Rational').---   ('Den' a '/=' 0) =>---     'Dif' r a  '=='  a '-' 'Div' r a '%' 1+--     'Rem' r a  '=='  a '-' 'Div' r a '%' 1 -- @------ Note: We use the word /difference/ because talking about /remainder/ in this--- context can be confusing, considering "Prelude"'s `rem`ainder function.--- However, strictly speaking, @`Dif` r a@ is the 'Rational' that /remiains/--- after performing the 'I.Round'ed 'Div'ision. So, yes, 'Dif' could potentially--- have been called @Rem@ instead.-type Dif (r :: I.Round) (a :: Rational) = Snd (DivDif r a) :: Rational+type Rem (r :: I.Round) (a :: Rational) = Snd (DivRem r a) :: Rational --- | Get both the quotient and the 'Dif'ference of the 'Div'ision of the+-- | Get both the quotient and the 'Rem'ainder of the 'Div'ision of the -- 'Num'erator of type-level 'Rational' @a@ by its 'Den'ominator, -- using the specified 'I.Round'ing @r@. -- -- @ -- forall (r :: 'I.Round') (a :: 'Rational'). --   ('Den' a '/=' 0) =>---     'DivDif' r a  '=='  '('Div' r a, 'Dif' r a)+--     'DivRem' r a  '=='  '('Div' r a, 'Rem' r a) -- @-type DivDif (r :: I.Round) (a :: Rational) =-  DivDif_ r (Normalize a) :: (Integer, Rational)-type DivDif_ (r :: I.Round) (a :: Rational) =-  DivDif__ a (Div_ r a) :: (Integer, Rational)-type DivDif__ (a :: Rational) (q :: Integer) =-  '(q, a - q :% 1) :: (Integer, Rational)+type DivRem (r :: I.Round) (a :: Rational) =+  DivRem_ r (Normalize a) :: (Integer, Rational)+type DivRem_ (r :: I.Round) (a :: Rational) =+  DivRem__ (Den_ a) (I.DivRem r (Num_ a) (P (Den_ a))) :: (Integer, Rational)+type DivRem__ (d :: Natural) (qm :: (Integer, Integer)) =+  '(Fst qm, Normalize (Snd qm % d)) :: (Integer, Rational)  -- | Term-level version of 'Div'. -- -- Takes a "Prelude" 'P.Rational' as input, returns a "Prelude" 'P.Integer'. div :: I.Round -> P.Rational -> P.Integer-div r = \(n P.:% d) -> f n d-  where f = I.div r---- | Term-level version of 'Div'.------ Takes a "Prelude" 'P.Rational' as input, returns a "Prelude" 'P.Integer'.-mod :: I.Round -> P.Rational -> P.Integer-mod r = \(n P.:% d) -> f n d-  where f = I.mod r---- | Term-level version of 'DivMod'.--- Takes a "Prelude" 'P.Rational' as input, returns a pair of "Prelude"--- 'P.Integer's /(quotient, modulus)/.------ @--- forall ('r' :: 'I.Round') (a :: 'P.Rational').---   ('P.denominator' a 'P./=' 0) =>---     'divMod' r a  'P.=='  ('div' r a, 'mod' r a)--- @-divMod :: I.Round -> P.Rational -> (P.Integer, P.Integer)-divMod r = \(n P.:% d) -> f n d-  where f = I.divMod r+div r = let f = I.div r+        in \a -> let (n P.:% d) = unsafeCheckPrelude a+                 in  f n d --- | Term-level version of 'Dif'.+-- | Term-level version of 'Rem'. -- -- Takes a "Prelude" 'P.Rational' as input, returns a "Prelude" 'P.Rational'.-dif :: I.Round -> P.Rational -> P.Rational-dif r = \a -> a - toRational (f a)-  where f = div r+rem :: I.Round -> P.Rational -> P.Rational+rem r = snd . divRem r --- | Term-level version of 'DivDif'.+-- | Term-level version of 'DivRem'. -- -- Takes a "Prelude" 'P.Rational' as input, returns a pair of "Prelude"--- 'P.Rational's /(quotient, difference)/.+-- 'P.Rational's /(quotient, remerence)/. -- -- @ -- forall ('r' :: 'I.Round') (a :: 'P.Rational'). --   ('P.denominator' a 'P./=' 0) =>---     'divDif' r a  'P.=='  ('div' r a, 'dif' r a)+--     'divRem' r a  'P.=='  ('div' r a, 'rem' r a) -- @-divDif :: I.Round -> P.Rational -> (P.Integer, P.Rational)-divDif r = \a -> let q = f a in (q, a - toRational q)-  where f = div r+divRem :: I.Round -> P.Rational -> (P.Integer, P.Rational)+divRem r = let f = I.divRem r+           in \a -> let (n P.:% d) = unsafeCheckPrelude a+                        (q, m) = f n d+                    in  (q, m P.% d) -- (m % d) == (a - q)  -------------------------------------------------------------------------------- @@ -713,5 +667,6 @@  data Dict c where Dict :: c => Dict c +type family Fst (ab :: (a, b)) :: a where Fst '(a, b) = a type family Snd (ab :: (a, b)) :: b where Snd '(a, b) = b
test/Main.hs view
@@ -213,32 +213,6 @@   , (N 4 / 3) ~ K.Recip (N 3 / 4)   ) --- Most tests for these are in kind-integer.-_testDivMod =  Dict-_testDivMod :: Dict-  ( '(P 1, P 1) ~ K.DivMod 'K.RoundDown (3 / 2)-  , '(P 2, N 1) ~ K.DivMod 'K.RoundUp (3 / 2)-  , '(P 1, P 1) ~ K.DivMod 'K.RoundZero (3 / 2)-  , '(P 2, N 1) ~ K.DivMod 'K.RoundAway (3 / 2)-  , '(P 1, P 1) ~ K.DivMod 'K.RoundHalfDown (3 / 2)-  , '(P 2, N 1) ~ K.DivMod 'K.RoundHalfUp (3 / 2)-  , '(P 1, P 1) ~ K.DivMod 'K.RoundHalfZero (3 / 2)-  , '(P 2, N 1) ~ K.DivMod 'K.RoundHalfAway (3 / 2)-  , '(P 2, N 1) ~ K.DivMod 'K.RoundHalfEven (3 / 2)-  , '(P 1, P 1) ~ K.DivMod 'K.RoundHalfOdd (3 / 2)--  , '(N 2, P 1) ~ K.DivMod 'K.RoundDown (N 3 / 2)-  , '(N 1, N 1) ~ K.DivMod 'K.RoundUp (N 3 / 2)-  , '(N 1, N 1) ~ K.DivMod 'K.RoundZero (N 3 / 2)-  , '(N 2, P 1) ~ K.DivMod 'K.RoundAway (N 3 / 2)-  , '(N 2, P 1) ~ K.DivMod 'K.RoundHalfDown (N 3 / 2)-  , '(N 1, N 1) ~ K.DivMod 'K.RoundHalfUp (N 3 / 2)-  , '(N 1, N 1) ~ K.DivMod 'K.RoundHalfZero (N 3 / 2)-  , '(N 2, P 1) ~ K.DivMod 'K.RoundHalfAway (N 3 / 2)-  , '(N 2, P 1) ~ K.DivMod 'K.RoundHalfEven (N 3 / 2)-  , '(N 1, N 1) ~ K.DivMod 'K.RoundHalfOdd (N 3 / 2)-  )- _testDiv =  Dict _testDiv :: Dict   ( P 1 ~ K.Div 'K.RoundDown (3 / 2)@@ -286,123 +260,98 @@   , N 1 ~ K.Div 'K.RoundHalfOdd (N 3 / 4)   ) -_testMod =  Dict-_testMod :: Dict-  ( P 1 ~ K.Mod 'K.RoundDown (3 / 2)-  , N 1 ~ K.Mod 'K.RoundUp (3 / 2)-  , P 1 ~ K.Mod 'K.RoundZero (3 / 2)-  , N 1 ~ K.Mod 'K.RoundAway (3 / 2)-  , P 1 ~ K.Mod 'K.RoundHalfDown (3 / 2)-  , N 1 ~ K.Mod 'K.RoundHalfUp (3 / 2)-  , P 1 ~ K.Mod 'K.RoundHalfZero (3 / 2)-  , N 1 ~ K.Mod 'K.RoundHalfAway (3 / 2)-  , N 1 ~ K.Mod 'K.RoundHalfEven (3 / 2)-  , P 1 ~ K.Mod 'K.RoundHalfOdd (3 / 2)--  , P 1 ~ K.Mod 'K.RoundDown (N 3 / 2)-  , N 1 ~ K.Mod 'K.RoundUp (N 3 / 2)-  , N 1 ~ K.Mod 'K.RoundZero (N 3 / 2)-  , P 1 ~ K.Mod 'K.RoundAway (N 3 / 2)-  , P 1 ~ K.Mod 'K.RoundHalfDown (N 3 / 2)-  , N 1 ~ K.Mod 'K.RoundHalfUp (N 3 / 2)-  , N 1 ~ K.Mod 'K.RoundHalfZero (N 3 / 2)-  , P 1 ~ K.Mod 'K.RoundHalfAway (N 3 / 2)-  , P 1 ~ K.Mod 'K.RoundHalfEven (N 3 / 2)-  , N 1 ~ K.Mod 'K.RoundHalfOdd (N 3 / 2)-  )--_testDif =  Dict-_testDif :: Dict-  ( P 1 / 2 ~ K.Dif 'K.RoundDown (3 / 2)-  , N 1 / 2 ~ K.Dif 'K.RoundUp (3 / 2)-  , P 1 / 2 ~ K.Dif 'K.RoundZero (3 / 2)-  , N 1 / 2 ~ K.Dif 'K.RoundAway (3 / 2)-  , P 1 / 2 ~ K.Dif 'K.RoundHalfDown (3 / 2)-  , N 1 / 2 ~ K.Dif 'K.RoundHalfUp (3 / 2)-  , P 1 / 2 ~ K.Dif 'K.RoundHalfZero (3 / 2)-  , N 1 / 2 ~ K.Dif 'K.RoundHalfAway (3 / 2)-  , N 1 / 2 ~ K.Dif 'K.RoundHalfEven (3 / 2)-  , P 1 / 2 ~ K.Dif 'K.RoundHalfOdd (3 / 2)+_testRem =  Dict+_testRem :: Dict+  ( P 1 / 2 ~ K.Rem 'K.RoundDown (3 / 2)+  , N 1 / 2 ~ K.Rem 'K.RoundUp (3 / 2)+  , P 1 / 2 ~ K.Rem 'K.RoundZero (3 / 2)+  , N 1 / 2 ~ K.Rem 'K.RoundAway (3 / 2)+  , P 1 / 2 ~ K.Rem 'K.RoundHalfDown (3 / 2)+  , N 1 / 2 ~ K.Rem 'K.RoundHalfUp (3 / 2)+  , P 1 / 2 ~ K.Rem 'K.RoundHalfZero (3 / 2)+  , N 1 / 2 ~ K.Rem 'K.RoundHalfAway (3 / 2)+  , N 1 / 2 ~ K.Rem 'K.RoundHalfEven (3 / 2)+  , P 1 / 2 ~ K.Rem 'K.RoundHalfOdd (3 / 2) -  , P 1 / 2 ~ K.Dif 'K.RoundDown (N 3 / 2)-  , N 1 / 2 ~ K.Dif 'K.RoundUp (N 3 / 2)-  , N 1 / 2 ~ K.Dif 'K.RoundZero (N 3 / 2)-  , P 1 / 2 ~ K.Dif 'K.RoundAway (N 3 / 2)-  , P 1 / 2 ~ K.Dif 'K.RoundHalfDown (N 3 / 2)-  , N 1 / 2 ~ K.Dif 'K.RoundHalfUp (N 3 / 2)-  , N 1 / 2 ~ K.Dif 'K.RoundHalfZero (N 3 / 2)-  , P 1 / 2 ~ K.Dif 'K.RoundHalfAway (N 3 / 2)-  , P 1 / 2 ~ K.Dif 'K.RoundHalfEven (N 3 / 2)-  , N 1 / 2 ~ K.Dif 'K.RoundHalfOdd (N 3 / 2)+  , P 1 / 2 ~ K.Rem 'K.RoundDown (N 3 / 2)+  , N 1 / 2 ~ K.Rem 'K.RoundUp (N 3 / 2)+  , N 1 / 2 ~ K.Rem 'K.RoundZero (N 3 / 2)+  , P 1 / 2 ~ K.Rem 'K.RoundAway (N 3 / 2)+  , P 1 / 2 ~ K.Rem 'K.RoundHalfDown (N 3 / 2)+  , N 1 / 2 ~ K.Rem 'K.RoundHalfUp (N 3 / 2)+  , N 1 / 2 ~ K.Rem 'K.RoundHalfZero (N 3 / 2)+  , P 1 / 2 ~ K.Rem 'K.RoundHalfAway (N 3 / 2)+  , P 1 / 2 ~ K.Rem 'K.RoundHalfEven (N 3 / 2)+  , N 1 / 2 ~ K.Rem 'K.RoundHalfOdd (N 3 / 2) -  , P 3 / 4 ~ K.Dif 'K.RoundDown (3 / 4)-  , N 1 / 4 ~ K.Dif 'K.RoundUp (3 / 4)-  , P 3 / 4 ~ K.Dif 'K.RoundZero (3 / 4)-  , N 1 / 4 ~ K.Dif 'K.RoundAway (3 / 4)-  , N 1 / 4 ~ K.Dif 'K.RoundHalfDown (3 / 4)-  , N 1 / 4 ~ K.Dif 'K.RoundHalfUp (3 / 4)-  , N 1 / 4 ~ K.Dif 'K.RoundHalfZero (3 / 4)-  , N 1 / 4 ~ K.Dif 'K.RoundHalfAway (3 / 4)-  , N 1 / 4 ~ K.Dif 'K.RoundHalfEven (3 / 4)-  , N 1 / 4 ~ K.Dif 'K.RoundHalfOdd (3 / 4)+  , P 3 / 4 ~ K.Rem 'K.RoundDown (3 / 4)+  , N 1 / 4 ~ K.Rem 'K.RoundUp (3 / 4)+  , P 3 / 4 ~ K.Rem 'K.RoundZero (3 / 4)+  , N 1 / 4 ~ K.Rem 'K.RoundAway (3 / 4)+  , N 1 / 4 ~ K.Rem 'K.RoundHalfDown (3 / 4)+  , N 1 / 4 ~ K.Rem 'K.RoundHalfUp (3 / 4)+  , N 1 / 4 ~ K.Rem 'K.RoundHalfZero (3 / 4)+  , N 1 / 4 ~ K.Rem 'K.RoundHalfAway (3 / 4)+  , N 1 / 4 ~ K.Rem 'K.RoundHalfEven (3 / 4)+  , N 1 / 4 ~ K.Rem 'K.RoundHalfOdd (3 / 4) -  , P 1 / 4 ~ K.Dif 'K.RoundDown (N 3 / 4)-  , N 3 / 4 ~ K.Dif 'K.RoundUp (N 3 / 4)-  , N 3 / 4 ~ K.Dif 'K.RoundZero (N 3 / 4)-  , P 1 / 4 ~ K.Dif 'K.RoundAway (N 3 / 4)-  , P 1 / 4 ~ K.Dif 'K.RoundHalfDown (N 3 / 4)-  , P 1 / 4 ~ K.Dif 'K.RoundHalfUp (N 3 / 4)-  , P 1 / 4 ~ K.Dif 'K.RoundHalfZero (N 3 / 4)-  , P 1 / 4 ~ K.Dif 'K.RoundHalfAway (N 3 / 4)-  , P 1 / 4 ~ K.Dif 'K.RoundHalfEven (N 3 / 4)-  , P 1 / 4 ~ K.Dif 'K.RoundHalfOdd (N 3 / 4)+  , P 1 / 4 ~ K.Rem 'K.RoundDown (N 3 / 4)+  , N 3 / 4 ~ K.Rem 'K.RoundUp (N 3 / 4)+  , N 3 / 4 ~ K.Rem 'K.RoundZero (N 3 / 4)+  , P 1 / 4 ~ K.Rem 'K.RoundAway (N 3 / 4)+  , P 1 / 4 ~ K.Rem 'K.RoundHalfDown (N 3 / 4)+  , P 1 / 4 ~ K.Rem 'K.RoundHalfUp (N 3 / 4)+  , P 1 / 4 ~ K.Rem 'K.RoundHalfZero (N 3 / 4)+  , P 1 / 4 ~ K.Rem 'K.RoundHalfAway (N 3 / 4)+  , P 1 / 4 ~ K.Rem 'K.RoundHalfEven (N 3 / 4)+  , P 1 / 4 ~ K.Rem 'K.RoundHalfOdd (N 3 / 4)   ) -_testDivDif =  Dict-_testDivDif :: Dict-  ( '(P 1, P 1 / 2) ~ K.DivDif 'K.RoundDown (3 / 2)-  , '(P 2, N 1 / 2) ~ K.DivDif 'K.RoundUp (3 / 2)-  , '(P 1, P 1 / 2) ~ K.DivDif 'K.RoundZero (3 / 2)-  , '(P 2, N 1 / 2) ~ K.DivDif 'K.RoundAway (3 / 2)-  , '(P 1, P 1 / 2) ~ K.DivDif 'K.RoundHalfDown (3 / 2)-  , '(P 2, N 1 / 2) ~ K.DivDif 'K.RoundHalfUp (3 / 2)-  , '(P 1, P 1 / 2) ~ K.DivDif 'K.RoundHalfZero (3 / 2)-  , '(P 2, N 1 / 2) ~ K.DivDif 'K.RoundHalfAway (3 / 2)-  , '(P 2, N 1 / 2) ~ K.DivDif 'K.RoundHalfEven (3 / 2)-  , '(P 1, P 1 / 2) ~ K.DivDif 'K.RoundHalfOdd (3 / 2)+_testDivRem =  Dict+_testDivRem :: Dict+  ( '(P 1, P 1 / 2) ~ K.DivRem 'K.RoundDown (3 / 2)+  , '(P 2, N 1 / 2) ~ K.DivRem 'K.RoundUp (3 / 2)+  , '(P 1, P 1 / 2) ~ K.DivRem 'K.RoundZero (3 / 2)+  , '(P 2, N 1 / 2) ~ K.DivRem 'K.RoundAway (3 / 2)+  , '(P 1, P 1 / 2) ~ K.DivRem 'K.RoundHalfDown (3 / 2)+  , '(P 2, N 1 / 2) ~ K.DivRem 'K.RoundHalfUp (3 / 2)+  , '(P 1, P 1 / 2) ~ K.DivRem 'K.RoundHalfZero (3 / 2)+  , '(P 2, N 1 / 2) ~ K.DivRem 'K.RoundHalfAway (3 / 2)+  , '(P 2, N 1 / 2) ~ K.DivRem 'K.RoundHalfEven (3 / 2)+  , '(P 1, P 1 / 2) ~ K.DivRem 'K.RoundHalfOdd (3 / 2) -  , '(N 2, P 1 / 2) ~ K.DivDif 'K.RoundDown (N 3 / 2)-  , '(N 1, N 1 / 2) ~ K.DivDif 'K.RoundUp (N 3 / 2)-  , '(N 1, N 1 / 2) ~ K.DivDif 'K.RoundZero (N 3 / 2)-  , '(N 2, P 1 / 2) ~ K.DivDif 'K.RoundAway (N 3 / 2)-  , '(N 2, P 1 / 2) ~ K.DivDif 'K.RoundHalfDown (N 3 / 2)-  , '(N 1, N 1 / 2) ~ K.DivDif 'K.RoundHalfUp (N 3 / 2)-  , '(N 1, N 1 / 2) ~ K.DivDif 'K.RoundHalfZero (N 3 / 2)-  , '(N 2, P 1 / 2) ~ K.DivDif 'K.RoundHalfAway (N 3 / 2)-  , '(N 2, P 1 / 2) ~ K.DivDif 'K.RoundHalfEven (N 3 / 2)-  , '(N 1, N 1 / 2) ~ K.DivDif 'K.RoundHalfOdd (N 3 / 2)+  , '(N 2, P 1 / 2) ~ K.DivRem 'K.RoundDown (N 3 / 2)+  , '(N 1, N 1 / 2) ~ K.DivRem 'K.RoundUp (N 3 / 2)+  , '(N 1, N 1 / 2) ~ K.DivRem 'K.RoundZero (N 3 / 2)+  , '(N 2, P 1 / 2) ~ K.DivRem 'K.RoundAway (N 3 / 2)+  , '(N 2, P 1 / 2) ~ K.DivRem 'K.RoundHalfDown (N 3 / 2)+  , '(N 1, N 1 / 2) ~ K.DivRem 'K.RoundHalfUp (N 3 / 2)+  , '(N 1, N 1 / 2) ~ K.DivRem 'K.RoundHalfZero (N 3 / 2)+  , '(N 2, P 1 / 2) ~ K.DivRem 'K.RoundHalfAway (N 3 / 2)+  , '(N 2, P 1 / 2) ~ K.DivRem 'K.RoundHalfEven (N 3 / 2)+  , '(N 1, N 1 / 2) ~ K.DivRem 'K.RoundHalfOdd (N 3 / 2) -  , '(P 0, P 3 / 4) ~ K.DivDif 'K.RoundDown (3 / 4)-  , '(P 1, N 1 / 4) ~ K.DivDif 'K.RoundUp (3 / 4)-  , '(P 0, P 3 / 4) ~ K.DivDif 'K.RoundZero (3 / 4)-  , '(P 1, N 1 / 4) ~ K.DivDif 'K.RoundAway (3 / 4)-  , '(P 1, N 1 / 4) ~ K.DivDif 'K.RoundHalfDown (3 / 4)-  , '(P 1, N 1 / 4) ~ K.DivDif 'K.RoundHalfUp (3 / 4)-  , '(P 1, N 1 / 4) ~ K.DivDif 'K.RoundHalfZero (3 / 4)-  , '(P 1, N 1 / 4) ~ K.DivDif 'K.RoundHalfAway (3 / 4)-  , '(P 1, N 1 / 4) ~ K.DivDif 'K.RoundHalfEven (3 / 4)-  , '(P 1, N 1 / 4) ~ K.DivDif 'K.RoundHalfOdd (3 / 4)+  , '(P 0, P 3 / 4) ~ K.DivRem 'K.RoundDown (3 / 4)+  , '(P 1, N 1 / 4) ~ K.DivRem 'K.RoundUp (3 / 4)+  , '(P 0, P 3 / 4) ~ K.DivRem 'K.RoundZero (3 / 4)+  , '(P 1, N 1 / 4) ~ K.DivRem 'K.RoundAway (3 / 4)+  , '(P 1, N 1 / 4) ~ K.DivRem 'K.RoundHalfDown (3 / 4)+  , '(P 1, N 1 / 4) ~ K.DivRem 'K.RoundHalfUp (3 / 4)+  , '(P 1, N 1 / 4) ~ K.DivRem 'K.RoundHalfZero (3 / 4)+  , '(P 1, N 1 / 4) ~ K.DivRem 'K.RoundHalfAway (3 / 4)+  , '(P 1, N 1 / 4) ~ K.DivRem 'K.RoundHalfEven (3 / 4)+  , '(P 1, N 1 / 4) ~ K.DivRem 'K.RoundHalfOdd (3 / 4) -  , '(N 1, P 1 / 4) ~ K.DivDif 'K.RoundDown (N 3 / 4)-  , '(P 0, N 3 / 4) ~ K.DivDif 'K.RoundUp (N 3 / 4)-  , '(P 0, N 3 / 4) ~ K.DivDif 'K.RoundZero (N 3 / 4)-  , '(N 1, P 1 / 4) ~ K.DivDif 'K.RoundAway (N 3 / 4)-  , '(N 1, P 1 / 4) ~ K.DivDif 'K.RoundHalfDown (N 3 / 4)-  , '(N 1, P 1 / 4) ~ K.DivDif 'K.RoundHalfUp (N 3 / 4)-  , '(N 1, P 1 / 4) ~ K.DivDif 'K.RoundHalfZero (N 3 / 4)-  , '(N 1, P 1 / 4) ~ K.DivDif 'K.RoundHalfAway (N 3 / 4)-  , '(N 1, P 1 / 4) ~ K.DivDif 'K.RoundHalfEven (N 3 / 4)-  , '(N 1, P 1 / 4) ~ K.DivDif 'K.RoundHalfOdd (N 3 / 4)+  , '(N 1, P 1 / 4) ~ K.DivRem 'K.RoundDown (N 3 / 4)+  , '(P 0, N 3 / 4) ~ K.DivRem 'K.RoundUp (N 3 / 4)+  , '(P 0, N 3 / 4) ~ K.DivRem 'K.RoundZero (N 3 / 4)+  , '(N 1, P 1 / 4) ~ K.DivRem 'K.RoundAway (N 3 / 4)+  , '(N 1, P 1 / 4) ~ K.DivRem 'K.RoundHalfDown (N 3 / 4)+  , '(N 1, P 1 / 4) ~ K.DivRem 'K.RoundHalfUp (N 3 / 4)+  , '(N 1, P 1 / 4) ~ K.DivRem 'K.RoundHalfZero (N 3 / 4)+  , '(N 1, P 1 / 4) ~ K.DivRem 'K.RoundHalfAway (N 3 / 4)+  , '(N 1, P 1 / 4) ~ K.DivRem 'K.RoundHalfEven (N 3 / 4)+  , '(N 1, P 1 / 4) ~ K.DivRem 'K.RoundHalfOdd (N 3 / 4)   )  _testTerminates =  Dict@@ -533,24 +482,19 @@             == fmap (\(K.SomeRational p) -> K.rationalVal p)                     (readMaybe @K.SomeRational str) -  ] <> testsDivModDif <> testsTerminating+  ] <> testsDivRem <> testsTerminating -testsDivModDif :: [IO Bool]-testsDivModDif = do+testsDivRem :: [IO Bool]+testsDivRem = do   a@(n P.:% d) <- rats 4   r :: K.Round <- [minBound .. maxBound]   let tname :: String -> ShowS       tname t = showString t . showChar ' ' . shows r . showChar ' '               . shows n . showChar ' ' . shows d-  [ assert (tname "divMod" "") $ case K.divMod r a of-                                   (q, m) -> m == n - d * q-    , assert (tname "divMod/div" "") $ fst (K.divMod r a) == K.div r a-    , assert (tname "divMod/mod" "") $ snd (K.divMod r a) == K.mod r a--    , assert (tname "divDif" "") $ case K.divDif r a of-                                     (q, x) -> a == toRational q + x-    , assert (tname "divDif/div" "") $ fst (K.divDif r a) == K.div r a-    , assert (tname "divDif/dif" "") $ snd (K.divDif r a) == K.dif r a+  [   assert (tname "divRem" "") $ case K.divRem r a of+                                        (q, x) -> a == toRational q + x+    , assert (tname "divRem/div" "") $ fst (K.divRem r a) == K.div r a+    , assert (tname "divRem/rem" "") $ snd (K.divRem r a) == K.rem r a     ]  testsTerminating  :: [IO Bool]