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

Lazy Peano numbers including observable infinity value.

Properties of @Num@ can be found in the source of 'Number.Peano.Inf.Test'.

The lazy operations of @Num@ makes it ideal for lazy list length computation. For example, @(genericLength [1..] :: Nat) > 100@ is @True@.

-}
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

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

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
_      * 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, ..@

@[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 = 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

```