module Data.Peano (Peano (..), infinity) where

import Data.Data
import Data.Function (on)
import Data.Ix (Ix (..))
import Data.Typeable

data Peano = Zero | Succ Peano deriving (Eq, Ord, Read, Show, Typeable, Data)

instance Enum Peano where
    succ = Succ

    pred (Succ n) = n
    pred Zero = error "pred Zero"

    toEnum   = fromInteger . toEnum

    fromEnum = fromEnum . toInteger

instance Bounded Peano where
    minBound = Zero
    maxBound = infinity

instance Ix Peano where
    range = uncurry enumFromTo
    index (l, u) n = fromEnum (n - l)
    inRange (l, u) n = l <= n && u >= n
    rangeSize (l, u) = fromEnum (Succ u - l)

instance Num Peano where
    Zero   + n = n
    Succ m + n = Succ (m + n)

    m      - Zero   = m
    Succ m - Succ n = m - n

    Zero   * n = Zero
    Succ m * n = n + m * n

    abs = id

    signum Zero = Zero
    signum _    = Succ Zero

    fromInteger n | n <  0 = error "fromInteger n | n < 0"
                  | n == 0 = Zero
                  | n >  0 = Succ (fromInteger (n - 1))

instance Real Peano where
    toRational = toRational . toInteger

instance Integral Peano where
    toInteger Zero = 0
    toInteger (Succ n) = toInteger n + 1

    Zero `quotRem` Zero   = error "0/0"
    m    `quotRem` n      = case compare m n
                            of LT -> (Zero, m)
                               _  -> let (q, r) = quotRem (m - n) n in (Succ q, r)

    divMod = quotRem

infinity :: Peano
infinity = Succ infinity