{-# LANGUAGE NoImplicitPrelude #-} {- | Copyright : (c) Henning Thielemann 2007 Maintainer : numericprelude@henning-thielemann.de Stability : provisional Portability : portable Lazy Peano numbers represent natural numbers inclusive infinity. Since they are lazily evaluated, they are optimally for use as number type of 'Data.List.genericLength' et.al. -} module Number.Peano where import qualified Algebra.PrincipalIdealDomain as PID import qualified Algebra.Units as Units import qualified Algebra.RealIntegral as RealIntegral import qualified Algebra.IntegralDomain as Integral import qualified Algebra.Real as Real import qualified Algebra.Ring as Ring import qualified Algebra.Additive as Additive import qualified Algebra.ZeroTestable as ZeroTestable import qualified Algebra.Indexable as Indexable import qualified Algebra.ToInteger as ToInteger import qualified Algebra.ToRational as ToRational import qualified Algebra.NonNegative as NonNeg import Data.Maybe (catMaybes, ) import Data.Array(Ix(..)) import qualified Prelude as P98 import qualified PreludeBase as P import qualified NumericPrelude as NP import Data.List.HT (mapAdjacent, shearTranspose, ) import PreludeBase import NumericPrelude data T = Zero | Succ T deriving (Show, Read, Eq) infinity :: T infinity = Succ infinity err :: String -> String -> a err func msg = error ("Number.Peano."++func++": "++msg) instance ZeroTestable.C T where isZero Zero = True isZero (Succ _) = False add :: T -> T -> T add Zero y = y add (Succ x) y = Succ (add x y) sub :: T -> T -> T sub x y = let (sign,z) = subNeg y x in if sign then err "sub" "negative difference" else z subNeg :: T -> T -> (Bool, T) subNeg Zero y = (False, y) subNeg x Zero = (True, x) subNeg (Succ x) (Succ y) = subNeg x y mul :: T -> T -> T mul Zero _ = Zero mul _ Zero = Zero mul (Succ x) y = add y (mul x y) fromPosEnum :: (ZeroTestable.C a, Enum a) => a -> T fromPosEnum n = if isZero n then Zero else Succ (fromPosEnum (pred n)) toPosEnum :: (Additive.C a, Enum a) => T -> a toPosEnum Zero = zero toPosEnum (Succ x) = succ (toPosEnum x) instance Additive.C T where zero = Zero (+) = add (-) = sub negate Zero = Zero negate (Succ _) = err "negate" "cannot negate positive number" instance Ring.C T where one = Succ Zero (*) = mul fromInteger n = if n<0 then err "fromInteger" "Peano numbers are always non-negative" else fromPosEnum n instance Enum T where pred Zero = err "pred" "Zero has no predecessor" pred (Succ x) = x succ = Succ toEnum n = if n<0 then err "toEnum" "Peano numbers are always non-negative" else fromPosEnum n fromEnum = toPosEnum enumFrom x = iterate Succ x enumFromThen x y = let (sign,d) = subNeg x y in if sign then iterate (sub d) x else iterate (add d) x {- enumFromTo = enumFromThenTo = -} {- The default instance is good for compare, but fails for min and max. -} instance Ord T where compare (Succ x) (Succ y) = compare x y compare Zero (Succ _) = LT compare (Succ _) Zero = GT compare Zero Zero = EQ min (Succ x) (Succ y) = Succ (min x y) min _ _ = Zero max (Succ x) (Succ y) = Succ (max x y) max Zero y = y max x Zero = x {- This special implementation works also for undefined < Zero. Thanks to Peter Divianszky for the hint. -} _ < Zero = False Zero < _ = True Succ n < Succ m = n < m x > y = y < x x <= y = not (y < x) x >= y = not (x < y) {- | cf. To how to find the shortest list in a list of lists efficiently, this means, also in the presence of infinite lists. -} argMinFull :: (T,a) -> (T,a) -> (T,a) argMinFull (x0,xv) (y0,yv) = let recurse (Succ x) (Succ y) = let (z,zv) = recurse x y in (Succ z, zv) recurse Zero _ = (Zero,xv) recurse _ _ = (Zero,yv) in recurse x0 y0 {- | On equality the first operand is returned. -} argMin :: (T,a) -> (T,a) -> a argMin x y = snd \$ argMinFull x y argMinimum :: [(T,a)] -> a argMinimum = snd . foldl1 argMinFull argMaxFull :: (T,a) -> (T,a) -> (T,a) argMaxFull (x0,xv) (y0,yv) = let recurse (Succ x) (Succ y) = let (z,zv) = recurse x y in (Succ z, zv) recurse x Zero = (x,xv) recurse _ y = (y,yv) in recurse x0 y0 {- | On equality the first operand is returned. -} argMax :: (T,a) -> (T,a) -> a argMax x y = snd \$ argMaxFull x y argMaximum :: [(T,a)] -> a argMaximum = snd . foldl1 argMaxFull -- isAscending - naive implementations {- | @x0 <= x1 && x1 <= x2 ... @ for possibly infinite numbers in finite lists. -} isAscendingFiniteList :: [T] -> Bool isAscendingFiniteList [] = True isAscendingFiniteList (x:xs) = let decrement (Succ y) = Just y decrement _ = Nothing in case x of Zero -> isAscendingFiniteList xs Succ xd -> case mapM decrement xs of Nothing -> False Just xsd -> isAscendingFiniteList (xd : xsd) isAscendingFiniteNumbers :: [T] -> Bool isAscendingFiniteNumbers = and . mapAdjacent (<=) -- isAscending - sophisticated implementations - explicit toListMaybe :: a -> T -> [Maybe a] toListMaybe a = let recurse Zero = [Just a] recurse (Succ x) = Nothing : recurse x in recurse {- | In @glue x y == (z,r,b)@ @z@ represents @min x y@, @r@ represents @max x y - min x y@, and @x<=y == b@. Cf. Numeric.NonNegative.Chunky -} glue :: T -> T -> (T, T, Bool) glue Zero ys = (Zero, ys, True) glue xs Zero = (Zero, xs, False) glue (Succ xs) (Succ ys) = let (common, difference, sign) = glue xs ys in (Succ common, difference, sign) {- Implementation notes: We check all pairs of adjacent numbers for correct order. We obtain a set of booleans, which must all be True. The order of checking these booleans is crucial. Pairs of numbers that are infinitely big or infinitely far in the list must be checked \"last\". Thus we order the booleans according to their computation costs (list position + magnitude of number) using 'shearTranspose'. -} isAscending :: [T] -> Bool isAscending = and . catMaybes . concat . shearTranspose . mapAdjacent (\x y -> let (costs0,_,le) = glue x y in toListMaybe le costs0) -- isAscending - use a cost measuring data type (could generalized to a monad, when considered as Writer monad, see htam and unique-logic packages -- following an idea of vixy http://moonpatio.com:8080/fastcgi/hpaste.fcgi/view?id=562 data Valuable a = Valuable {costs :: T, value :: a} deriving (Show, Eq, Ord) increaseCosts :: T -> Valuable a -> Valuable a increaseCosts inc ~(Valuable c x) = Valuable (inc+c) x {- | Compute '(&&)' with minimal costs. -} infixr 3 &&~ (&&~) :: Valuable Bool -> Valuable Bool -> Valuable Bool (&&~) (Valuable xc xb) (Valuable yc yb) = let (minc,difc,le) = glue xc yc (bCheap,bExpensive) = if le then (xb,yb) else (yb,xb) in increaseCosts minc \$ uncurry Valuable \$ if bCheap then (difc, bExpensive) else (Zero, False) andW :: [Valuable Bool] -> Valuable Bool andW = foldr (\b acc -> b &&~ increaseCosts one acc) (Valuable Zero True) leW :: T -> T -> Valuable Bool leW x y = let (minc,_difc,le) = glue x y in Valuable minc le isAscendingW :: [T] -> Valuable Bool isAscendingW = andW . mapAdjacent leW {- test with *Number.Peano> isAscendingW [0,infinity,infinity,5] False -} -- instances instance Real.C T where signum Zero = zero signum (Succ _) = one abs = id instance ToInteger.C T where toInteger = toPosEnum instance ToRational.C T where toRational = toRational . toInteger instance RealIntegral.C T where quot = div rem = mod quotRem = divMod instance Integral.C T where div x y = fst (divMod x y) mod x y = snd (divMod x y) divMod x y = let (isNeg,d) = subNeg y x in if isNeg then (zero,x) else let (q,r) = divMod d y in (succ q,r) instance NonNeg.C T where (-|) x y = let (isNeg,d) = subNeg y x in if isNeg then zero else d instance Ix T where range = uncurry enumFromTo index (lower,_) i = let (sign,offset) = subNeg lower i in if sign then err "index" "index out of range" else toPosEnum offset inRange (lower,upper) i = isAscending [lower, i, upper] rangeSize (lower,upper) = toPosEnum (sub lower (succ upper)) instance Indexable.C T where compare = Indexable.ordCompare instance Units.C T where isUnit x = x == one stdAssociate = id stdUnit _ = one stdUnitInv _ = one instance PID.C T where gcd = PID.euclid mod extendedGCD = PID.extendedEuclid divMod instance Bounded T where minBound = Zero maxBound = infinity legacyInstance :: a legacyInstance = error "legacy Ring.C instance for simple input of numeric literals" instance P98.Num T where fromInteger = Ring.fromInteger negate = Additive.negate -- for unary minus (+) = add (-) = sub (*) = mul signum = legacyInstance abs = legacyInstance -- for use with genericLength et.al. instance P98.Real T where toRational = P98.toRational . toInteger instance P98.Integral T where rem = div quot = mod quotRem = divMod div x y = fst (divMod x y) mod x y = snd (divMod x y) divMod x y = let (sign,d) = subNeg y x in if sign then (0,x) else let (q,r) = divMod d y in (succ q,r) toInteger = toPosEnum