```{- |
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:

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

```