peano-inf 0.6 → 0.6.1
raw patch · 4 files changed
+244/−70 lines, 4 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- Number/Peano/Inf.hs +26/−31
- Number/Peano/Inf/Functions.hs +11/−0
- Number/Peano/Inf/Test.hs +206/−36
- peano-inf.cabal +1/−3
Number/Peano/Inf.hs view
@@ -6,10 +6,7 @@ Lazy Peano numbers including observable infinity value. -Properties of @Num@ can be found in the source of 'Number.Peano.Inf.Test'.--The lazy operations of @Num@ makes it ideal for lazy list length computation. For example, @(genericLength [1..] :: Nat) > 100@ is @True@.-+Properties of @Nat@ can be found in the source of "Number.Peano.Inf.Test". -} module Number.Peano.Inf ( Nat@@ -67,26 +64,14 @@ {- | Traditional infinity value: @let n = Succ n in n@. -For every function @f :: Nat -> Bool@, @f infinity@ and @f inductive_infinity@ gives the same result, provided that-the results are not bottom.--Use @infinity@ instead. Lots of the given properties of @infinity@ is not true for @inductive_infinity@. For example,--* @inductive_infinity == inductive_infinity@ is an endless computation instead of @True@.--However, the following values are @True@:--* @n < inductive_infinity@, @n@ = 0, 1, 2,...--Note also:--* @inductive_infinity == infinity@ is an endless computation instead of @True@.+@infinity@ is equal to @inductive_infinity@ but @infinity@ is lazier.+In other words:+For every function @f :: Nat -> Bool@, either @f inductive_infinity@ is bottom or @f inductive_infinity@ is equal to @f infinity@. -} inductive_infinity :: Nat inductive_infinity = let n = Succ n in n - instance Eq Nat where Zero == Zero = True@@ -96,6 +81,7 @@ Inf == Succ m = Inf == m _ == _ = False + instance Ord Nat where Zero `compare` Zero = EQ@@ -145,15 +131,16 @@ Just i -> show i Nothing -> "infinity" + {- | Difference of two natural numbers: the result is either positive or negative. -implementation of @(-)@ is based on @diff@.- The following value is undefined: * @diff infinity infinity@ -}+infix 6 `diff`+ diff :: Nat -- ^ n -> Nat -- ^ m@@ -171,13 +158,16 @@ Variant of @diff@: * @infDiff infinity infinity == Left infinity@.-+-}+{- Note that if the implementation of @(-)@ would be based on @infDiff@, the following equations would not hold: * @(a - b) - (a - c) == c - b@, @a >= c >= b@, because @(infininty - 5) - (infinity - 10) == infinity /= 10 - 5@. * @a - (a - b) == b@, @a >= b@, because @infininty - (infinity - 5) == infinity /= 5@. -}+infixl 6 `infDiff`+ infDiff :: Nat -- ^ n -> Nat -- ^ m@@ -194,13 +184,16 @@ Variant of @diff@: * @zeroDiff infinity infinity == Left 0@.-+-}+{- Note that if the implementation of @(-)@ would be based on @zeroDiff@, the following equations would not hold: * @(a - b) - (a - c) == c - b@, @a >= c >= b@, because @(infininty - 5) - (infinity - 10) == 0 /= 10 - 5@. * @a - (a - b) == b@, @a >= b@, because @infininty - (infinity - 5) == 0 /= 5@. -}+infixl 6 `zeroDiff`+ zeroDiff :: Nat -- ^ n -> Nat -- ^ m@@ -215,7 +208,7 @@ --- | Non-negative subtraction. For example, @(5 -| 8 == 0)@.+-- | Non-negative subtraction. For example, @5 -| 8 == 0@. infixl 6 -| (-|) :: Nat -> Nat -> Nat@@ -247,6 +240,7 @@ signum Zero = Zero signum _ = Succ Zero + instance Enum Nat where succ = Succ@@ -258,6 +252,12 @@ toEnum i | i < 0 = error "Number.Peano.Inf: toEnum on negative value." toEnum i = iterate Succ Zero !! i + fromEnum n = f 0 n where++ f i Zero = i+ f i (Succ m) = i' `seq` f i' m where i' = i+1+ f _ Inf = error "Number.Peano.Inf: fromEnum infinity."+ enumFrom n = enumFromTo n Inf {- |@@ -318,17 +318,11 @@ f (Left j) l = l: f (j `infDiff` d) (d + l) - fromEnum n = f 0 n where-- f i Zero = i- f i (Succ m) = i' `seq` f i' m where i' = i+1- f _ Inf = error "Number.Peano.Inf: fromEnum infinity."-- instance Real Nat where toRational n = toRational (fromIntegral n :: Integer) + instance Integral Nat where toInteger n = case toInteger' n of@@ -336,6 +330,7 @@ Nothing -> error "Number.Peano.Inf: toInteger infinity." quotRem _ _ = error "Number.Peano.Inf: quotRem not implemented."+ instance Bounded Nat where
Number/Peano/Inf/Functions.hs view
@@ -24,6 +24,17 @@ maximum :: [Nat] -> Nat maximum = foldr max 0 +{- | +Lazyness properties of @Nat@ makes it ideal for lazy list length computation. +Examples:++> length [1..] > 100++> length undefined >= 0++> length (undefined: undefined) >= 1+-}+ length :: [a] -> Nat length [] = 0 length (_:t) = succ (length t)
Number/Peano/Inf/Test.hs view
@@ -1,3 +1,6 @@+{- |+You can find the properties in the source code.+-} {-# LANGUAGE ScopedTypeVariables #-} @@ -6,79 +9,246 @@ ) where import Number.Peano.Inf- import Test.LazySmallCheck hiding (test)+import Data.List default (Nat) +------ helper functions++sm :: Testable a => a -> IO ()+sm = smallCheck 10++(=~=) :: Eq a => [a] -> [a] -> Bool+as =~= bs = take 15 as == take 15 bs++infix 1 <=>+(<=>) :: Bool -> Bool -> Bool+(<=>) = (==)+++----------- Properties of Nat ------------++-- Note that (n::Nat) means that @n = 0, 1, 2..@ or @n = infinity@, but @inductive_infinity@ will not appear.+ test :: IO () test = do --- Several lazyness properties+-- Eq - smallCheck 10 $+ sm $ \(n::Nat) -> n == n - undefined >= (0::Nat) + sm $ \(n::Nat) (m::Nat) -> n == m <=> m == n - smallCheck 10 $ \(n::Nat) -> and+ sm $ \(n::Nat) (m::Nat) (k::Nat) -> n == m && m == k ==> n == k - [ n + undefined >= n -- but @undefined + n@ raises an error. - , n /= infinity ==> (1 + n + undefined) `compare` n == GT -- but @compare (n + undefined) n@ raises an error.+-- (<=) - , n `min` (n + undefined) == n+ sm $ \(n::Nat) (m::Nat) (k::Nat) -> n <= m && m <= k ==> n <= k - , (1 + n + undefined) `min` n == n -- but @min (n + undefined) n@ raises an error.- ]+ sm $ \(n::Nat) (m::Nat) -> n <= m && m <= n <=> n == m - smallCheck 10 $ \(m::Nat) (n::Nat) -> and+ sm $ \(n::Nat) (m::Nat) -> n <= m || m <= n - [ (m + n) `min` (m + undefined) >= m+-- sm $ \(n::Nat) (m::Nat) -> xor [n < m, n == m, m < n] - , (m + undefined) `min` (m + n) >= m - , n `max` (m + undefined) >= m+-- (<), (>), (>=), compare - , (m + undefined) `max` n >= m+ sm $ \(n::Nat) (m::Nat) -> n < m <=> n <= m && n /= m - ]+ sm $ \(n::Nat) (m::Nat) -> n > m <=> m < n --- Properties of infinity+ sm $ \(n::Nat) (m::Nat) -> n >= m <=> m <= n - smallCheck 10 $ and + sm $ \(n::Nat) (m::Nat) -> n `compare` m == case () of+ _ | n < m -> LT+ | n == m -> EQ+ | n > m -> GT - [ infinity == infinity+-- min, max - , 0 * infinity == 0+ sm $ \(n::Nat) (m::Nat) -> (n `min` m, n `max` m) `elem` [(n, m), (m, n)] - , infinity * 0 == 0+ sm $ \(n::Nat) (m::Nat) -> n `min` m <= n && n `min` m <= m - ]+ sm $ \(n::Nat) (m::Nat) -> n `max` m >= n && n `max` m >= m - smallCheck 10 $ \(n::Nat) -> and - [ n /= infinity ==> n < infinity+-- (+) - , n + infinity == infinity+ sm $ \(n::Nat) (m::Nat) -> n + m == m + n - , infinity + n == infinity+ sm $ \(n::Nat) (m::Nat) (k::Nat) -> n + (m + k) == (n + m) + k - , n /= 0 ==> n * infinity == infinity+ sm $ \(n::Nat) -> 0 + n == n - , n /= 0 ==> infinity * n == infinity+ sm $ \(n::Nat) -> infinity + n == infinity - , n /= infinity ==> infinity - n == infinity+ sm $ \(n::Nat) -> n == infinity || n `elem` iterate (1+) 0 - ]+ sm $ \(n::Nat) -> n /= infinity ==> n < 1 + n -{--The following values raise error messages:+-- diff -* @infinity - infinity@,+ sm $ \(n::Nat) (d::Nat) -> n /= infinity ==> (d + n) `diff` n == Left d -* @fromEnum infinity@,+ sm $ \(n::Nat) (d::Nat) -> n /= infinity ==> n `diff` (1 + d + n) == Right (1 + d) -* @toInteger infinity@.--}+ -- infinity `diff` infinity is undefined+++-- zeroDiff, infDiff, (-), (-|)++ sm $ \(n::Nat) (m::Nat) -> m /= infinity ==> n `zeroDiff` m == n `diff` m++ sm $ infinity `zeroDiff` infinity == Left 0++ sm $ \(n::Nat) (m::Nat) -> m /= infinity ==> n `infDiff` m == n `diff` m++ sm $ infinity `infDiff` infinity == Left infinity++ sm $ \(n::Nat) (m::Nat) -> n >= m && m /= infinity ==> Left (n - m) == n `diff` m++ sm $ \(n::Nat) (m::Nat) -> n >= m && m /= infinity ==> n -| m == n - m++ sm $ \(n::Nat) (m::Nat) -> n <= m && m /= infinity ==> n -| m == 0+++-- (*)++ sm $ \(n::Nat) -> 0 * n == 0++ sm $ \(n::Nat) (m::Nat) -> (1 + n) * m == m + n * m++-- sm $ \(n::Nat) -> n /= 0 ==> infinity * n == infinity++-- sm $ \(n::Nat) (m::Nat) -> n * m == m * n++-- sm $ \(n::Nat) (m::Nat) (k::Nat) -> n * (m * k) == (n * m) * k++++-- minBound, maxBound++ sm $ minBound == (0::Nat) && maxBound == infinity++ sm $ \(n::Nat) -> minBound <= n++ sm $ \(n::Nat) -> n <= maxBound+++-- toInteger, fromInteger++ sm $ toInteger (0::Nat) == 0++ sm $ \(n::Nat) -> n /= infinity ==> toInteger (1 + n) == 1 + toInteger n++ -- toInteger infinity is undefined++ sm $ \(n::Nat) -> n /= infinity ==> fromInteger (toInteger n) == n++ sm $ \(n::Integer) -> n >= 0 ==> toInteger (fromInteger n :: Nat) == n+++-- toEnum, fromEnum++ sm $ \(n::Int) -> n >= 0 ==> (toEnum n :: Nat) == fromInteger (toInteger n)++ sm $ \(n::Nat) -> n /= infinity ==> toInteger (fromEnum n) == toInteger n+++-- succ, pred++ sm $ \(n::Nat) -> succ n == 1 + n++ sm $ \(n::Nat) -> pred (1 + n) == n+++-- enumFrom++ sm $ \(n::Nat) -> head [n.. ] == n++ sm $ \(n::Nat) -> tail [n.. ] =~= [1+n.. ]++-- sm $ \(n::Nat) -> [n.. ] =~= [n, 1+n.. ]+++-- enumFromTo++ sm $ \(n::Nat) (m::Nat) -> [n.. m] =~= takeWhile (<= m) [n..]+++-- enumFromThen (non-decreasing)++ sm $ \(n::Nat) (m::Nat) -> take 2 [n, m.. ] == [n, m]++ sm $ \(n::Nat) (d::Nat) -> tail [n, d+n.. ] =~= [d+n, d+d+n.. ]+++-- enumFromThen (non-increasing)++ sm $ \(n::Nat) (d::Nat) -> d /= infinity ==> tail [d+d+n, d+n.. ] =~= [d+n, n.. ]++-- sm $ \(n::Nat) (d::Nat) -> tail [d+d+d+n, d+d+n.. ] =~= [d+d+n, d+n.. ]++ sm $ \(n::Nat) (d::Nat) -> n < d ==> tail [d+n, n.. ] == [n]+++-- enumFromThenTo++ sm $ \(n::Nat) (m::Nat) (k::Nat) -> [n, m.. k] =~= case n `compare` m of++ LT -> takeWhile (<= k) [n, m..]+ EQ -> [n, m..]+ GT -> takeWhile (>= k) [n, m..]+++-- inductive_infininty++ sm $ \(n::Nat) -> n /= infinity ==> n < inductive_infinity++++------- Lazyness properties of Nat ----------++++ sm $ (0::Nat) <= undefined+++ sm $ infinity + undefined == infinity++ sm $ \(n::Nat) -> n /= infinity ==> inductive_infinity + undefined > n++ sm $ \(n::Nat) -> n + undefined >= n++-- sm $ \(n::Nat) -> undefined + n >= n -- raises an error++ sm $ \(n::Nat) -> n /= infinity ==> 1 + n + undefined > n+++ sm $ \(n::Nat) -> n `min` (n + undefined) == n++ sm $ \(n::Nat) -> (1 + n + undefined) `min` n == n++-- sm $ \(n::Nat) -> (n + undefined) `min` n == n -- raises an error++ sm $ \(n::Nat) (m::Nat) -> (n + undefined) `min` (m + undefined) >= n `min` m+++ sm $ \(n::Nat) (m::Nat) -> n `max` (m + undefined) >= m++ sm $ \(n::Nat) (m::Nat) -> (m + undefined) `max` n >= m++ sm $ \(n::Nat) (m::Nat) -> (n + undefined) `max` (m + undefined) >= n `min` m+++ sm $ \(n::Nat) -> (1 + undefined) * n >= n++ sm $ \(n::Nat) -> n /= infinity ==> (1 + undefined) * inductive_infinity > n++
peano-inf.cabal view
@@ -1,10 +1,8 @@ name: peano-inf-version: 0.6+version: 0.6.1 synopsis: Lazy Peano numbers including observable infinity value. description: Lazy Peano numbers including observable infinity value.- .- This data type was needed in a graph traversing algorithm. . This data type is ideal for lazy list length computation (the infinite value is not needed in this case). For a comparison with other Peano number implementation, see <http://people.inf.elte.hu/divip/peano/>