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

Lazy Peano numbers including observable infinity value.
-}
module Number.Peano.Inf
    ( Nat (Zero, Succ)
    , infinity
    , isInfinity
    , (-|)
    ) where

import Data.Ratio ((%))

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

-- | Observable infinity value.

infinity :: Nat
infinity = Inf

-- | True for @(infinity)@, @(5 + 4 * infinity)@ etc. Evaluates to bottom for @(genericLength [1..])@.

isInfinity :: Nat -> Bool
isInfinity Zero = False
isInfinity Inf  = True
isInfinity (Succ n) = isInfinity n

instance Eq Nat where

    Zero   == Zero   = True
    Succ n == Succ m = n == m
    Inf    == Inf    = error "Nat: infinity == infinity"
    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    = error "Nat: infinity `compare` infinity"
    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    = error "Nat: infinity < infinity"
    Inf    < Succ m = Inf < m
    Succ n < Inf    = n < Inf

    x > y = y < x

    x <= y = not (y < x)

    x >= y = not (x < y)

    Zero   `max` x      = x
    x      `max` Zero   = x
    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

instance Show Nat where

    show Inf = "infinity"
    show x   = show $ toInteger x

-- | Subtraction maximized to 0. For example, @(5 -| 8  ==  0)@.

infixl 6 -|
(-|) :: Nat -> Nat -> Nat
Inf    -| Inf    = error "Nat: infinity -| infinity"
Inf    -| _      = Inf
Succ n -| Succ m = n -| m
n      -| Zero   = n
_      -| _      = Zero


instance Num Nat where

    Inf    - Inf    = error "Nat: infinity - infinity"
    Inf    - _      = Inf
    Succ n - Succ m = n - m
    n      - Zero   = n
    _      - Inf    = error "Nat: n - inifinty"
    Zero   - Succ _ = error "Nat: 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 "Nat: fromInteger on negative value."
    fromInteger i = iterate Succ Zero !! fromInteger i

    abs x = x

    signum Zero = Zero
    signum _    = Succ Zero

instance Enum Nat where

    toEnum i | i < 0 = error "Nat: 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

instance Real Nat where

    toRational n = fromIntegral n % 1

instance Integral Nat where

    toInteger n = f 0 n where

        f i Zero = i
        f i (Succ m) = i' `seq` f i' m  where i' = i+1

    quotRem _ _ = error "Nat: quotRem not implemented."