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

Lazy Peano numbers including observable infinity value.

Note that the following equation does /not/ hold for this number type:

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

The following operation is undefined:

* @infinity - infinity@

There are variants of @(-)@ with different behaviour regarding this, see below.

The following operations are naturally undefined:

* @fromEnum infinity@

* @toInteger infinity@

* @0 - n@, if @n > 0@

* @fromInteger n@, if @n < 0@

* @toEnum n@, if @n < 0@

* @pred 0@

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

import Data.Ratio ((%))

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

-- | Observable infinity value.

infinity :: Nat
infinity = Inf


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

    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