{- |
Copyright    :   (c) Peter Divianszky 2008
Maintainer   :   divip@aszt.inf.elte.hu
Stability    :   experimental
Portability  :   portable

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:

* @1 + a > a@,  because @1 + infinity == infinity@.

-}
module Number.Peano.Inf
    ( Nat
    , infinity
    , inductive_infinity
    , diff
    , zeroDiff
    , infDiff
    , (-|)
    , minimum'
    ) where

import Data.Ratio ((%))
{-
Implementation Notes

The observable infinity value has many representatives:

> Inf
> Succ Inf
> Succ (Succ Inf)
> ...

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
the observable infinity, both @f n@ and @f m@ should be

* either @0@, @1@, @2@, ..., @bottom@, @Succ bottom@, @Succ (Succ bottom)@, ...

* or (maybe different) representatives of the observable infinity

The functions in this module obey this rule.
The abstract @Nat@ data type ensures that the users should not take care of this rule.
-}

-- | Natural numbers and infinity.
data Nat
    = Zero
    | Succ Nat
    | Inf           

{- | 
Observable infinity value.

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@.
-}
infinity :: Nat
infinity = Inf

{- |
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@.
-}
inductive_infinity :: Nat
inductive_infinity = let n = Succ n in n



instance Eq Nat where

    Zero   == Zero   = True
    Succ n == Succ m = n == m
    Inf    == Inf    = True
    Succ n == Inf    = n == Inf 
    Inf    == Succ m = Inf == m 
    _      == _      = False

instance Ord Nat where

    Zero   `compare` Zero   = EQ
    Zero   `compare` _      = LT
    _      `compare` Zero   = GT
    Succ n `compare` Succ m = n `compare` m
    Inf    `compare` Inf    = EQ
    Inf    `compare` Succ m = Inf `compare` m
    Succ n `compare` Inf    = n `compare` Inf

    _      < Zero   = False
    Zero   < _      = True
    Succ n < Succ m = n < m
    Inf    < Inf    = False
    Inf    < Succ m = Inf < m
    Succ n < Inf    = n < Inf

    n > m = m < n

    n <= m = not (m < n)

    n >= m = not (n < m)

    Zero   `max` m      = m
    n      `max` Zero   = n
    Succ n `max` Succ m = Succ (n `max` m)
    _      `max` _      = Inf

    Zero   `min` _      = Zero
    _      `min` Zero   = Zero
    Succ n `min` Succ m = Succ (n `min` m)
    Inf    `min` m      = m
    n      `min` Inf    = n


toInteger' :: Nat -> Maybe Integer
toInteger' n = f 0 n where

    f i Zero = Just i
    f i (Succ m) = i' `seq` f i' m  where i' = i+1
    f _ Inf = Nothing


instance Show Nat where

    show n = case toInteger' n of
        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@
-}
diff 
    :: Nat             -- ^ n
    -> Nat             -- ^ m
    -> Either Nat Nat  -- ^ n >= m: Left (n-m),  n < m: Right (m-n)

n      `diff` Zero   = Left  n 
Zero   `diff` m      = Right m
Succ n `diff` Succ m = n `diff` m
Inf    `diff` Inf    = error "Number.Peano.Inf: infinity - infinity."
Inf    `diff` Succ m = Inf `diff` m
Succ n `diff` Inf    = n `diff` Inf


{- | 
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@.
-}
infDiff
    :: Nat             -- ^ n
    -> Nat             -- ^ m
    -> Either Nat Nat  -- ^ n >= m: Left (n-m),  n < m: Right (m-n)

Inf    `infDiff` _      = Left Inf
Succ n `infDiff` Succ m = n `infDiff` m
Succ n `infDiff` Inf    = n `infDiff` Inf
n      `infDiff` Zero   = Left  n 
Zero   `infDiff` m      = Right m


{- | 
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@.
-}
zeroDiff
    :: Nat             -- ^ n
    -> Nat             -- ^ m
    -> Either Nat Nat  -- ^ n >= m: Left (n-m),  n < m: Right (m-n)

n      `zeroDiff` Zero   = Left  n 
Zero   `zeroDiff` m      = Right m
Succ n `zeroDiff` Succ m = n `zeroDiff` m
Inf    `zeroDiff` Inf    = Left Zero
Inf    `zeroDiff` Succ m = Inf `zeroDiff` m
Succ n `zeroDiff` Inf    = n `zeroDiff` Inf



-- | Non-negative subtraction. For example, @(5 -| 8  ==  0)@.

infixl 6 -|
(-|) :: Nat -> Nat -> Nat
n -| m = case n `diff` m of
    Left k  -> k
    Right _ -> Zero


instance Num Nat where

    n - m = case n `diff` m of
        Left k  -> k
        Right _ -> error "Number.Peano.Inf: 0 - succ n."

    Zero   + m      = m
    Succ n + m      = Succ (n + m)
    Inf    + _      = Inf

    Succ n * m = m + n * m
    Zero   * _ = Zero
    Inf    * _ = Inf

    fromInteger i | i < 0 = error "Number.Peano.Inf: fromInteger on negative value."
    fromInteger i = iterate Succ Zero !! fromInteger i

    abs n = n

    signum Zero = Zero
    signum _    = Succ Zero

instance Enum Nat where

    succ = Succ

    pred Inf = Inf
    pred (Succ n) = n
    pred Zero = error "Number.Peano.Inf: pred 0."

    toEnum i | i < 0 = error "Number.Peano.Inf: toEnum on negative value."
    toEnum i = iterate Succ Zero !! i

    enumFrom n = enumFromTo n Inf

    {- |
            @[inf.. inf] == [inf, inf, inf, ..@

        instead of 

            @[inf.. inf] == [inf]@

        Both have sense, but the second solution would make @enumfrom@ more eager.
    -}
    enumFromTo n m = case m `infDiff` n of

        Right _ -> []
        Left k  -> f k n  where

            f Zero     l  = [l]
            f (Succ j) l  = l: f j (Succ l)
            f Inf      l  = iterate Succ l
    
    enumFromThen n n' = case n `zeroDiff` n' of

        -- constant sequence
        Left Zero -> n: repeat n'

        -- decreasing sequence
        Left d -> n: n': f (n' `zeroDiff` d) where

            f (Right _)               = []
            f (Left j)                = j: f (j `zeroDiff` d)

        -- increasing sequence
        Right d  -> n: iterate (d +) n'


    enumFromThenTo n n' m = case n `zeroDiff` n' of     -- [n, n' .. m]

        -- constant sequence
        Left Zero -> n: repeat n'

        -- decreasing sequence
        Left d -> case m `compare` n of

            EQ  -> [n]
            GT  -> []
            LT  -> n: f (n' `zeroDiff` m) n'  where    -- n' >= m ?    n'-m = (-(m-n)) - (n-n'),  if n,m < inf

                f (Right _) _                 = []
                f (Left j)  l                 = l: f (j `zeroDiff` d) (l - d)

        -- increasing sequence
        Right d  -> case m `infDiff` n of

            Right _ -> []
            Left k  -> n: f (k `infDiff` d) n'  where

                f (Right _)   _  = []
                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 = fromIntegral n % 1

instance Integral Nat where

    toInteger n = case toInteger' n of
        Just i  -> i
        Nothing -> error "Number.Peano.Inf: toInteger infinity."

    quotRem _ _ = error "Number.Peano.Inf: quotRem not implemented."

instance Bounded Nat where

    minBound = Zero
    maxBound = Inf

{- |
Minimum of the list elements.
Works also for empty lists.
-}
minimum' :: [Nat] -> Nat
minimum' = foldr min infinity