{-# OPTIONS -fno-implicit-prelude #-} {- | 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.Array(Ix(..)) import qualified Prelude as P98 import qualified PreludeBase as P import qualified NumericPrelude as NP 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 {- efficient implementation of x0 <= x1 && x1 <= x2 ... -} isAscending :: [T] -> Bool isAscending [] = True isAscending (x:xs) = if isZero x then isAscending xs else not (any isZero xs) && isAscending (map pred xs) mul :: T -> T -> T 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 {- | 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 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