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

Lazy Peano numbers including observable infinity value.

Properties of @Nat@ can be found in the source of "Number.Peano.Inf.Test".
-}
module Number.Peano.Inf
    ( Nat
    , infinity
    , inductive_infinity
    , diff
    , zeroDiff
    , infDiff
    , (-|)
    ) where

import Test.LazySmallCheck (Serial(..), cons0, cons1, (\/))

{-
Implementation Notes

The observable infinity value has many representatives:

> Inf
> Succ Inf
> 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
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           

-- Serial instance needed for testing
instance Serial Nat where
    series = cons0 Zero \/ cons1 Succ \/ cons0 Inf


-- | Observable infinity value.
infinity :: Nat
infinity = Inf

{- |
Traditional infinity value: @let n = Succ n in n@.

@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
    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.

The following value is undefined:

* @diff infinity infinity@
-}
infix 6 `diff`

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@.
-}
infixl 6 `infDiff`

infDiff :: Nat -> Nat -> Either Nat Nat

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@.
-}
infixl 6 `zeroDiff`

zeroDiff :: Nat -> Nat -> Either Nat Nat

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
    _      * 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

    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 = iterate Succ

    {- |
            @[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)


instance Real Nat where

    toRational n = toRational (fromIntegral n :: Integer)


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