peano-inf 0.5 → 0.6

raw patch · 4 files changed

+138/−76 lines, 4 filesdep +lazysmallcheckPVP ok

version bump matches the API change (PVP)

Dependencies added: lazysmallcheck

API changes (from Hackage documentation)

Files

• Number/Peano/Inf.hs +15/−73
• Number/Peano/Inf/Functions.hs +33/−0
• Number/Peano/Inf/Test.hs +84/−0
• peano-inf.cabal +6/−3

@@ -6,37 +6,9 @@  Lazy Peano numbers including observable infinity value. -Several lazyness properties:--* @undefined >= 0@,--* @n + undefined >= n@, if @n@ = 0, 1, 2, ...--but @undefined + n@ raises an error.--* @compare (n + undefined) (n-1) == GT@, if @n@ = 0, 1, 2, ...--but @compare (n + undefined) n@ raises an error.--* @min n (n + undefined)@ results @n@, if @n@ = 0, 1, 2, ...--* @min (n + undefined) (n - 1)@ results @n - 1@, if @n@ = 0, 1, 2, ...--but @min (n + undefined) n@ raises an error.--* @min n (m + undefined) >= m@, if @n@, @m@ = 0, 1, 2, ... For example, @min 10 (5 + undefined) >= 5@.--* @min (m + undefined) n >= m@, if @n@, @m@ = 0, 1, 2, ...--* @max n (m + undefined) >= m@, if @n@, @m@ = 0, 1, 2, ... For example, @max 10 (5 + undefined) >= 5@.--* @max (m + undefined) n >= m@, if @n@, @m@ = 0, 1, 2, ...--These properties makes the @Num@ data type ideal for lazy list length computation. For example, @(genericLength [1..] :: Nat) > 100@ is @True@.--Note that the following equation does /not/ hold for this number type:+Properties of @Num@ can be found in the source of 'Number.Peano.Inf.Test'. -* @1 + a > a@,  because @1 + infinity == infinity@.+The lazy operations of @Num@ makes it ideal for lazy list length computation. For example, @(genericLength [1..] :: Nat) > 100@ is @True@.  -} module Number.Peano.Inf@@ -47,10 +19,10 @@     , zeroDiff     , infDiff     , (-|)-    , minimum'     ) where -import Data.Ratio ((%))+import Test.LazySmallCheck (Serial(..), cons0, cons1, (\/))+ {- Implementation Notes @@ -61,6 +33,8 @@ > Succ (Succ Inf) > ... +The representatives are needed to keep (+) lazy in its second argument.+ Multiple representatives need extra caretaking: Every function on @Nat@ must be well defined.  A function @f :: Nat -> Nat@ is well defined if for all @n@ and @m@ which are representatives of@@ -80,38 +54,12 @@     | Succ Nat     | Inf            -{- | -Observable infinity value.+instance Serial Nat where+    series = cons0 Zero \/ cons1 Succ \/ cons0 Inf -The following values are @True@ for @n@ = 0, 1, 2,... : -* @infinity == infinity@,--* @n < infinity@,--* @n + infinity == infinity@,--* @infinity + infinity == infinity@,--* @infinity + n == infinity@,--* @n * infinity == infinity@,--* @infinity * n == infinity@,--* @infinity * infinity == infinity@,--* @n - infinity == 0@,--* @infinity - n == infinity@.--The following values raise error messages:--* @infinity - infinity@,--* @fromEnum infinity@,--* @toInteger infinity@.+{- | +Observable infinity value. -} infinity :: Nat infinity = Inf@@ -286,9 +234,10 @@     Succ n + m      = Succ (n + m)     Inf    + _      = Inf -    Succ n * m = m + n * m-    Zero   * _ = Zero-    Inf    * _ = Inf+    Succ n * m      = m + n * m+    Zero   * _      = Zero+    _      * Zero   = Zero+    Inf    * _      = Inf      fromInteger i | i < 0 = error "Number.Peano.Inf: fromInteger on negative value."     fromInteger i = iterate Succ Zero !! fromInteger i@@ -378,7 +327,7 @@  instance Real Nat where -    toRational n = fromIntegral n % 1+    toRational n = toRational (fromIntegral n :: Integer)  instance Integral Nat where @@ -392,13 +341,6 @@      minBound = Zero     maxBound = Inf--{- |-Minimum of the list elements.-Works also for empty lists.--}-minimum' :: [Nat] -> Nat-minimum' = foldr min infinity   

@@ -0,0 +1,33 @@+module Number.Peano.Inf.Functions +    ( minimum+    , maximum+    , length+    ) where++import Number.Peano.Inf++import qualified Prelude as P+import Prelude hiding (minimum, maximum, length)++{- |+Minimum of the list elements.+Works also for empty lists.+-}+minimum :: [Nat] -> Nat+minimum = foldr min infinity+++{- |+Maximum of the list elements.+Works also for empty lists.+-}+maximum :: [Nat] -> Nat+maximum = foldr max 0++length :: [a] -> Nat+length [] = 0+length (_:t) = succ (length t)++++

@@ -0,0 +1,84 @@++{-# LANGUAGE ScopedTypeVariables #-}++module Number.Peano.Inf.Test +    ( test+    ) where++import Number.Peano.Inf++import Test.LazySmallCheck hiding (test)++default (Nat)++test :: IO ()+test = do++-- Several lazyness properties++    smallCheck 10 $++        undefined >= (0::Nat)        ++    smallCheck 10 $ \(n::Nat) -> and++        [   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++        ,   (1 + n + undefined) `min` n == n    -- but @min (n + undefined) n@ raises an error.+        ]++    smallCheck 10 $ \(m::Nat) (n::Nat) -> and++        [   (m + n) `min` (m + undefined) >= m++        ,   (m + undefined) `min` (m + n) >= m++        ,   n `max` (m + undefined) >= m++        ,   (m + undefined) `max` n >= m++        ]++-- Properties of infinity++    smallCheck 10 $ and ++        [   infinity == infinity++        ,   0 * infinity == 0++        ,   infinity * 0 == 0++        ]++    smallCheck 10 $ \(n::Nat) -> and++        [   n /= infinity ==>  n < infinity++        ,   n + infinity == infinity++        ,   infinity + n == infinity++        ,   n /= 0 ==>  n * infinity == infinity++        ,   n /= 0 ==>  infinity * n == infinity++        ,   n /= infinity ==>  infinity - n == infinity++        ]+++{-+The following values raise error messages:++* @infinity - infinity@,++* @fromEnum infinity@,++* @toInteger infinity@.+-}+

@@ -1,5 +1,5 @@ name:           peano-inf-version:        0.5+version:        0.6 synopsis:       Lazy Peano numbers including observable infinity value. description:         Lazy Peano numbers including observable infinity value.@@ -21,9 +21,12 @@ library     ghc-options:    -Wall -fno-warn-overlapping-patterns -fno-warn-incomplete-patterns     build-depends:-        base+        base,+        lazysmallcheck      exposed-modules:-        Number.Peano.Inf+        Number.Peano.Inf,+        Number.Peano.Inf.Test,+        Number.Peano.Inf.Functions