{-# LANGUAGE RebindableSyntax #-}
{- |
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.Absolute             as Absolute
import qualified Algebra.Ring                 as Ring
import qualified Algebra.Additive             as Additive
import qualified Algebra.ZeroTestable         as ZeroTestable
import qualified Algebra.Indexable            as Indexable
import qualified Algebra.Monoid               as Monoid

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

import qualified Algebra.EqualityDecision as EqDec
import qualified Algebra.OrderDecision    as OrdDec

import Data.Maybe (catMaybes, )
import Data.Array(Ix(..))

import qualified Prelude     as P98
import qualified NumericPrelude.Base as P
import qualified NumericPrelude.Numeric as NP
import Data.List.HT (mapAdjacent, shearTranspose, )
import Data.Tuple.HT (mapFst, )

import NumericPrelude.Base
import NumericPrelude.Numeric


data T = Zero
       | Succ T
   deriving (Show, Read, Eq)

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
add Zero y = y
add (Succ x) y = Succ (add x y)

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


mul :: T -> T -> T
mul Zero _ = Zero
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)

instance Additive.C T where
   zero = Zero
   (+) = add
   (-) = 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
   fromEnum = toPosEnum
   enumFrom x = iterate Succ x
   enumFromThen x y =
      let (sign,d) = subNeg x y
      in  if sign
            then iterate (sub d) x
            else iterate (add d) x
   {-
   enumFromTo =
   enumFromThenTo =
   -}


{- |
If all values are completely defined,
then it holds

> if b then x else y == ifLazy b x y

However if @b@ is undefined,
then it is at least known that the result is larger than @min x y@.
-}
ifLazy :: Bool -> T -> T -> T
ifLazy b (Succ x) (Succ y) = Succ (ifLazy b x y)
ifLazy b x y = if b then x else y

instance EqDec.C T where
   (==?) x y = ifLazy (x==y)

instance OrdDec.C T where
   (<=?) x y le gt = ifLazy (x<=y) le gt

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

   {-
   This special implementation works also for undefined < Zero.
   Thanks to Peter Divianszky for the hint.
   -}
   _      < Zero   = False
   Zero   < _      = True
   Succ n < Succ m = n < m

   x > y  = y < x

   x <= y = not (y < x)

   x >= y = not (x < y)


{- | cf.
To how to find the shortest list in a list of lists efficiently,
this means, also in the presence of infinite lists.
<http://www.haskell.org/pipermail/haskell-cafe/2006-October/018753.html>
-}
argMinFull :: (T,a) -> (T,a) -> (T,a)
argMinFull (x0,xv) (y0,yv) =
   let recourse (Succ x) (Succ y) =
          let (z,zv) = recourse x y
          in  (Succ z, zv)
       recourse Zero _ = (Zero,xv)
       recourse _    _ = (Zero,yv)
   in  recourse 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 recourse (Succ x) (Succ y) =
          let (z,zv) = recourse x y
          in  (Succ z, zv)
       recourse x Zero = (x,xv)
       recourse _ y    = (y,yv)
   in  recourse 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



-- isAscending - naive implementations

{- |
@x0 <= x1 && x1 <= x2 ... @
for possibly infinite numbers in finite lists.
-}
isAscendingFiniteList :: [T] -> Bool
isAscendingFiniteList [] = True
isAscendingFiniteList (x:xs) =
   let decrement (Succ y) = Just y
       decrement _ = Nothing
   in  case x of
         Zero -> isAscendingFiniteList xs
         Succ xd ->
           case mapM decrement xs of
             Nothing -> False
             Just xsd -> isAscendingFiniteList (xd : xsd)

isAscendingFiniteNumbers :: [T] -> Bool
isAscendingFiniteNumbers = and . mapAdjacent (<=)


-- isAscending - sophisticated implementations - explicit

toListMaybe :: a -> T -> [Maybe a]
toListMaybe a =
   let recourse Zero     = [Just a]
       recourse (Succ x) = Nothing : recourse x
   in  recourse

{- |
In @glue x y == (z,(b,r))@
@z@ represents @min x y@,
@r@ represents @max x y - min x y@,
and @x<=y  ==  b@.

Cf. Numeric.NonNegative.Chunky
-}
glue :: T -> T -> (T, (Bool, T))
glue Zero ys = (Zero, (True, ys))
glue xs Zero = (Zero, (False, xs))
glue (Succ xs) (Succ ys) =
   mapFst Succ $ glue xs ys

{-
Implementation notes:
We check all pairs of adjacent numbers for correct order.
We obtain a set of booleans, which must all be True.
The order of checking these booleans is crucial.
Pairs of numbers that are infinitely big or infinitely far in the list
must be checked \"last\".
Thus we order the booleans according to their computation costs
(list position + magnitude of number)
using 'shearTranspose'.
-}
isAscending :: [T] -> Bool
isAscending =
   and . catMaybes . concat .
   shearTranspose .
   mapAdjacent (\x y ->
      let (costs0,(le,_)) = glue x y
      in  toListMaybe le costs0)


-- isAscending - use a cost measuring data type (could generalized to a monad, when considered as Writer monad, see htam and unique-logic packages

-- following an idea of vixy http://moonpatio.com:8080/fastcgi/hpaste.fcgi/view?id=562

data Valuable a = Valuable {costs :: T, value :: a}
   deriving (Show, Eq, Ord)


increaseCosts :: T -> Valuable a -> Valuable a
increaseCosts inc ~(Valuable c x) = Valuable (inc+c) x

{- |
Compute '(&&)' with minimal costs.
-}
infixr 3 &&~
(&&~) :: Valuable Bool -> Valuable Bool -> Valuable Bool
(&&~) (Valuable xc xb) (Valuable yc yb) =
   let (minc,~(le,difc)) = glue xc yc
       (bCheap,bExpensive) =
          if le
            then (xb,yb)
            else (yb,xb)
   in  increaseCosts minc $
       uncurry Valuable $
       if bCheap
         then (difc, bExpensive)
         else (Zero, False)

andW :: [Valuable Bool] -> Valuable Bool
andW =
   foldr
      (\b acc -> b &&~ increaseCosts one acc)
      (Valuable Zero True)

leW :: T -> T -> Valuable Bool
leW x y =
   let (minc,~(le,_difc)) = glue x y
   in  Valuable minc le

isAscendingW :: [T] -> Valuable Bool
isAscendingW =
   andW . mapAdjacent leW

{-
test with

*Number.Peano> isAscendingW [0,infinity,infinity,5]
False
-}


-- instances

instance Absolute.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 Monoid.C T where
   idt = zero
   (<*>) = add
   cumulate = foldr add Zero

instance NonNeg.C T where
   split = glue

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
   (+) = add
   (-) = 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