module TypeFun.Data.Peano
  ( N(..)
  , KnownPeano(..)
  , ToNat
  , FromNat
  , (:+:)
  , (:-:)
  , (:*:)
  ) where

import           Data.Typeable
import           GHC.Generics  (Generic)
import           GHC.TypeLits

data N = Z | S N
         deriving ( Eq, Ord, Read, Show
                  , Generic, Typeable )

-- | @since 0.1.2
class KnownPeano (p :: N) where
  peanoVal :: proxy p -> Integer

instance KnownPeano Z where
  peanoVal _ = 0

instance (KnownPeano n) => KnownPeano (S n) where
  peanoVal _ = succ $ peanoVal (Proxy :: Proxy n)

type family ToNat (a :: N) :: Nat where
  ToNat Z = 0
  ToNat (S a) = 1 + (ToNat a)

type family FromNat (a :: Nat) :: N where
  FromNat 0 = Z
  FromNat a = S (FromNat (a - 1))

type family (:+:) (a :: N) (b :: N) :: N where
  Z :+: b = b
  (S a) :+: b = a :+: (S b)

type family (:-:) (a :: N) (b :: N) :: N where
  a :-: Z = a
  (S a) :-: (S b) = a :-: b

type family (:*:) (a :: N) (b :: N) :: N where
  Z :*: b = Z
  a :*: Z = Z
  (S a) :*: b = b :+: (a :*: b)