```{-# OPTIONS -fno-implicit-prelude #-}
{- |
Copyright    :   (c) Henning Thielemann 2007
Maintainer   :   numericprelude@henning-thielemann.de
Stability    :   provisional
Portability  :   portable

Lazy Peano numbers represent natural numbers inclusive infinity.
Since they are lazily evaluated,
they are optimally for use as number type of 'Data.List.genericLength' et.al.
-}
module Number.Peano where

import qualified Algebra.PrincipalIdealDomain as PID
import qualified Algebra.Units                as Units
import qualified Algebra.RealIntegral         as RealIntegral
import qualified Algebra.IntegralDomain       as Integral
import qualified Algebra.Real                 as Real
import qualified Algebra.Ring                 as Ring
import qualified Algebra.ZeroTestable         as ZeroTestable
import qualified Algebra.Indexable            as Indexable

import qualified Algebra.ToInteger            as ToInteger
import qualified Algebra.ToRational           as ToRational
import qualified Algebra.NonNegative          as NonNeg

import Data.Array(Ix(..))

import qualified Prelude     as P98
import qualified PreludeBase as P
import qualified NumericPrelude as NP

import PreludeBase
import NumericPrelude

data T = Zero
| Succ T

infinity :: T
infinity = Succ infinity

err :: String -> String -> a
err func msg = error ("Number.Peano."++func++": "++msg)

instance ZeroTestable.C T where
isZero Zero     = True
isZero (Succ _) = False

add :: T -> T -> T

sub :: T -> T -> T
sub x y =
let (sign,z) = subNeg y x
in  if sign
then err "sub" "negative difference"
else z

subNeg :: T -> T -> (Bool, T)
subNeg Zero y = (False, y)
subNeg x Zero = (True,  x)
subNeg (Succ x) (Succ y) = subNeg x y

{- efficient implementation of x0 <= x1 && x1 <= x2 ... -}
isAscending :: [T] -> Bool
isAscending [] = True
isAscending (x:xs) =
if isZero x
then isAscending xs
else not (any isZero xs) &&
isAscending (map pred xs)

mul :: T -> T -> T
mul Zero _ = Zero
mul (Succ x) y = add y (mul x y)

fromPosEnum :: (ZeroTestable.C a, Enum a) => a -> T
fromPosEnum n =
if isZero n
then Zero
else Succ (fromPosEnum (pred n))

toPosEnum :: (Additive.C a, Enum a) => T -> a
toPosEnum Zero = zero
toPosEnum (Succ x) = succ (toPosEnum x)

zero = Zero
(-) = sub
negate Zero     = Zero
negate (Succ _) = err "negate" "cannot negate positive number"

instance Ring.C T where
one = Succ Zero
(*) = mul
fromInteger n =
if n<0
then err "fromInteger" "Peano numbers are always non-negative"
else fromPosEnum n

instance Enum T where
pred Zero = err "pred" "Zero has no predecessor"
pred (Succ x) = x
succ = Succ
toEnum n =
if n<0
then err "toEnum" "Peano numbers are always non-negative"
else fromPosEnum n
enumFrom x = iterate Succ x
enumFromThen x y =
let (sign,d) = subNeg x y
in  if sign
then iterate (sub d) x
{-
enumFromTo =
enumFromThenTo =
-}

{-
The default instance is good for compare,
but fails for min and max.
-}
instance Ord T where
compare (Succ x) (Succ y) = compare x y
compare Zero     (Succ _) = LT
compare (Succ _) Zero     = GT
compare Zero     Zero     = EQ

min (Succ x) (Succ y) = Succ (min x y)
min _        _        = Zero

max (Succ x) (Succ y) = Succ (max x y)
max Zero     y        = y
max x        Zero     = x

{- | cf.
To how to find the shortest list in a list of lists efficiently,
this means, also in the presence of infinite lists.
-}
argMinFull :: (T,a) -> (T,a) -> (T,a)
argMinFull (x0,xv) (y0,yv) =
let recurse (Succ x) (Succ y) =
let (z,zv) = recurse x y
in  (Succ z, zv)
recurse Zero _ = (Zero,xv)
recurse _    _ = (Zero,yv)
in  recurse x0 y0

{- |
On equality the first operand is returned.
-}
argMin :: (T,a) -> (T,a) -> a
argMin x y = snd \$ argMinFull x y

argMinimum :: [(T,a)] -> a
argMinimum = snd . foldl1 argMinFull

argMaxFull :: (T,a) -> (T,a) -> (T,a)
argMaxFull (x0,xv) (y0,yv) =
let recurse (Succ x) (Succ y) =
let (z,zv) = recurse x y
in  (Succ z, zv)
recurse x Zero = (x,xv)
recurse _ y    = (y,yv)
in  recurse x0 y0

{- |
On equality the first operand is returned.
-}
argMax :: (T,a) -> (T,a) -> a
argMax x y = snd \$ argMaxFull x y

argMaximum :: [(T,a)] -> a
argMaximum = snd . foldl1 argMaxFull

instance Real.C T where
signum Zero     = zero
signum (Succ _) = one
abs             = id

instance ToInteger.C T where
toInteger = toPosEnum

instance ToRational.C T where
toRational = toRational . toInteger

instance RealIntegral.C T where
quot = div
rem  = mod
quotRem = divMod

instance Integral.C T where
div x y = fst (divMod x y)
mod x y = snd (divMod x y)
divMod x y =
let (isNeg,d) = subNeg y x
in  if isNeg
then (zero,x)
else let (q,r) = divMod d y in (succ q,r)

instance NonNeg.C T where
(-|) x y =
let (isNeg,d) = subNeg y x
in  if isNeg
then zero
else d

instance Ix T where
range = uncurry enumFromTo
index (lower,_) i =
let (sign,offset) = subNeg lower i
in  if sign
then err "index" "index out of range"
else toPosEnum offset
inRange (lower,upper) i =
isAscending [lower, i, upper]
rangeSize (lower,upper) =
toPosEnum (sub lower (succ upper))

instance Indexable.C T where
compare = Indexable.ordCompare

instance Units.C T where
isUnit x  =  x == one
stdAssociate  =  id
stdUnit    _ = one
stdUnitInv _ = one

instance PID.C T where
gcd = PID.euclid mod
extendedGCD = PID.extendedEuclid divMod

instance Bounded T where
minBound = Zero
maxBound = infinity

legacyInstance :: a
legacyInstance =
error "legacy Ring.C instance for simple input of numeric literals"

instance P98.Num T where
fromInteger = Ring.fromInteger
negate = Additive.negate -- for unary minus
(-) = sub
(*) = mul
signum = legacyInstance
abs = legacyInstance

-- for use with genericLength et.al.
instance P98.Real T where
toRational = P98.toRational . toInteger

instance P98.Integral T where
rem  = div
quot = mod
quotRem = divMod
div x y = fst (divMod x y)
mod x y = snd (divMod x y)
divMod x y =
let (sign,d) = subNeg y x
in  if sign
then (0,x)
else let (q,r) = divMod d y in (succ q,r)
toInteger = toPosEnum
```