-- |Value-level Peano arithmetic.
module Numeric.Peano where

import Prelude hiding (foldr)
import Data.Foldable (Foldable(foldr))
import Data.Ratio ((%))

-- |Lazy Peano numbers. Allow calculation with infinite values.
data Nat = Z -- ^Zero
           | S Nat -- ^Successor
   deriving (Show)

-- |Sign for whole numbers.
data Sign = Pos | Neg deriving (Show, Eq, Ord, Enum, Read, Bounded)

-- |Whole numbers (Z).
data Whole = Whole Nat Sign -- ^Construct a whole number out of a magnitue and a sign.

-- |The class of Peano-like constructions (i.e. Nat and Whole).
class Enum a => Peano a where
   -- |Test for zero.
   isZero :: a -> Bool
   -- |An unobservable infinity. For all finite numbers @n@, @n < infinity@ must
   --  hold, but there need not be a total function that tests whether a number
   --  is infinite.
   infinity :: a
   -- |Converts the number to an Integer.
   fromPeano :: a -> Integer
   -- |Reduces the absolute value of the number by 1. If @isZero n@, then
   --  @decr n = n@ and vice versa.
   decr :: a -> a

-- |Negation of 'isZero'.
isSucc :: Peano n => n -> Bool
isSucc = not . isZero

instance Peano Nat where
   isZero Z = True
   isZero _ = False
   infinity = S infinity
   fromPeano Z = 0
   fromPeano (S n) = succ $ fromPeano n
   decr = pred

instance Peano Whole where
   isZero (Whole n _) = isZero n
   infinity = Whole infinity Pos
   fromPeano (Whole n Pos) = fromPeano n
   fromPeano (Whole n Neg) = negate $ fromPeano n
   decr (Whole n s) = Whole (pred n) s

-- |Removes at most 'S' constructors from a Peano number.
--  Outputs the number of removed constructors and the remaining number.
takeNat :: (Num a, Enum a, Ord a, Peano n) => a -> n -> (a, n)
takeNat = takeNat' 0
   where
      takeNat' c i n | i <= 0    = (c, n)
                     | isZero n  = (c, n)
                     | otherwise = takeNat' (succ c) (pred i) (decr n)


-- |The lower bound is zero, the upper bound is infinity.
instance Bounded Nat where
   minBound = Z
   maxBound = infinity

-- |The bounds are negative and positive infinity.
instance Bounded Whole where
   minBound = Whole infinity Neg
   maxBound = infinity

-- |The 'pred' function is bounded at Zero.
instance Enum Nat where
   toEnum = fromInteger . fromIntegral
   fromEnum = fromInteger . fromPeano
   succ = S
   pred Z = Z
   pred (S n) = n

-- |'succ' and 'pred' work according to the total
--  order on the whole numbers, i.e. @succ n = n+1@ and @pred n = n-1@.
instance Enum Whole where
   toEnum i | i < 0     = Whole (toEnum i) Neg
            | otherwise = Whole (toEnum i) Pos
   fromEnum = fromInteger . fromPeano
   succ (Whole (S n) Neg) = Whole n Neg
   succ (Whole n Pos) = Whole (S n) Pos
   succ (Whole Z _) = Whole (S Z) Pos
   pred (Whole (S n) Pos) = Whole n Pos
   pred (Whole n Neg) = Whole (S n) Neg
   pred (Whole Z _) = Whole (S Z) Neg

-- |Addition, multiplication, and subtraction are
--  lazy in both arguments, meaning that, in the case of infinite values,
--  they can produce an infinite stream of S-constructors. As long as
--  the callers of these functions only consume a finite amount of these,
--  the program will not hang.
--
--  @fromInteger@ is not injective in case of 'Nat', since negative integers
--  are all converted to zero ('Z').
instance Num Nat where
   (+) Z n = n
   (+) n Z = n
   (+) (S n) (S m) = S $ S $ (+) n m

   (*) Z n = Z
   (*) n Z = Z
   (*) (S n) (S m) = S Z + n + m + (n * m)

   abs = id

   signum _ = S Z

   fromInteger i | i <= 0    = Z
                 | otherwise = S $ fromInteger $ i - 1

   (-) Z n = Z
   (-) n Z = n
   (-) (S n) (S m) = n - m

instance Num Whole where
   (+) (Whole n Pos) (Whole m Pos) = Whole (n+m) Pos
   (+) (Whole n Neg) (Whole m Neg) = Whole (n+m) Neg
   (+) (Whole n Pos) (Whole m Neg) | n >= m    = Whole (n-m) Pos
                                   | otherwise = Whole (m-n) Neg
   (+) (Whole n Neg) (Whole m Pos) = Whole m Pos + Whole n Neg

   (*) (Whole n s) (Whole m t) | s == t    = Whole (n*m) Pos
                               | otherwise = Whole (n*m) Neg

   (-) n (Whole m Neg) = n + (Whole m Pos)
   (-) n (Whole m Pos) = n + (Whole m Neg)

   abs (Whole n s) = Whole n Pos

   signum (Whole Z _) = Whole Z Pos
   signum (Whole _ Pos) = Whole (S Z) Pos
   signum (Whole _ Neg) = Whole (S Z) Neg

   fromInteger i | i < 0     = Whole (fromInteger $ negate i) Neg
                 | otherwise = Whole (fromInteger i) Pos


-- |'==' and '/=' work as long as at least one operand is finite.
instance Eq Nat where
   (==) Z Z = True
   (==) Z (S _) = False
   (==) (S _) Z = False
   (==) (S n) (S m) = n == m

-- |Positive and negative zero are considered equal.
instance Eq Whole where
   (==) (Whole Z _) (Whole Z _) = True
   (==) (Whole n s) (Whole m t) = s == t && n == m

-- |All methods work as long as at least one operand is finite.
instance Ord Nat where
   compare Z Z = EQ
   compare Z (S _) = LT
   compare (S _) Z = GT
   compare (S n) (S m) = compare n m

-- |The ordering is the standard total order on Z. Positive and negative zero
--  are equal.
instance Ord Whole where
   compare (Whole Z _) (Whole Z _) = EQ
   compare (Whole _ Neg) (Whole _ Pos) = LT
   compare (Whole _ Pos) (Whole _ Neg) = GT
   compare (Whole n Pos) (Whole m Pos) = compare n m
   compare (Whole n Neg) (Whole m Neg) = compare m n

-- |Returns the length of a foldable container as 'Nat'. The number is generated
--  lazily and thus, infinitely large containers are supported.
natLength :: Foldable f => f a -> Nat
natLength = foldr (const S) Z

-- |Since 'toRational' returns a @Ratio Integer@, it WILL NOT terminate on infinities.
instance Real Nat where
   toRational = flip (%) 1 . fromPeano

-- |Since negative numbers are not allowed,
--  @'quot' = 'div'@ and @'rem' = 'mod'@. The methods 'quot', 'rem', 'div', 'mod',
--  'quotRem' and 'divMod' will terminate as long as their first argument is
--  finite. Infinities in their second arguments are permitted and are handled
--  as follows:
--
--  @
--  n `quot` infinity   =   n `div` infinity   =   0
--  n `rem`  infinity   =   n `mod` infinity   =   n@
instance Integral Nat where
   quotRem _ Z = error "divide by zero"
   quotRem n (S m) = quotRem' Z n (S m)
      where
         quotRem' q n m | n >= m    = quotRem' (S q) (n-m) m
                        | otherwise = (q,n)

   divMod = quotRem
   toInteger = fromPeano