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 ( N -> N -> Bool
(N -> N -> Bool) -> (N -> N -> Bool) -> Eq N
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: N -> N -> Bool
$c/= :: N -> N -> Bool
== :: N -> N -> Bool
$c== :: N -> N -> Bool
Eq, Eq N
Eq N
-> (N -> N -> Ordering)
-> (N -> N -> Bool)
-> (N -> N -> Bool)
-> (N -> N -> Bool)
-> (N -> N -> Bool)
-> (N -> N -> N)
-> (N -> N -> N)
-> Ord N
N -> N -> Bool
N -> N -> Ordering
N -> N -> N
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: N -> N -> N
$cmin :: N -> N -> N
max :: N -> N -> N
$cmax :: N -> N -> N
>= :: N -> N -> Bool
$c>= :: N -> N -> Bool
> :: N -> N -> Bool
$c> :: N -> N -> Bool
<= :: N -> N -> Bool
$c<= :: N -> N -> Bool
< :: N -> N -> Bool
$c< :: N -> N -> Bool
compare :: N -> N -> Ordering
$ccompare :: N -> N -> Ordering
$cp1Ord :: Eq N
Ord, ReadPrec [N]
ReadPrec N
Int -> ReadS N
ReadS [N]
(Int -> ReadS N)
-> ReadS [N] -> ReadPrec N -> ReadPrec [N] -> Read N
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [N]
$creadListPrec :: ReadPrec [N]
readPrec :: ReadPrec N
$creadPrec :: ReadPrec N
readList :: ReadS [N]
$creadList :: ReadS [N]
readsPrec :: Int -> ReadS N
$creadsPrec :: Int -> ReadS N
Read, Int -> N -> ShowS
[N] -> ShowS
N -> String
(Int -> N -> ShowS) -> (N -> String) -> ([N] -> ShowS) -> Show N
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [N] -> ShowS
$cshowList :: [N] -> ShowS
show :: N -> String
$cshow :: N -> String
showsPrec :: Int -> N -> ShowS
$cshowsPrec :: Int -> N -> ShowS
Show
                  , (forall x. N -> Rep N x) -> (forall x. Rep N x -> N) -> Generic N
forall x. Rep N x -> N
forall x. N -> Rep N x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep N x -> N
$cfrom :: forall x. N -> Rep N x
Generic, Typeable )

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

instance KnownPeano Z where
  peanoVal :: proxy 'Z -> Integer
peanoVal proxy 'Z
_ = Integer
0

instance (KnownPeano n) => KnownPeano (S n) where
  peanoVal :: proxy ('S n) -> Integer
peanoVal proxy ('S n)
_ = Integer -> Integer
forall a. Enum a => a -> a
succ (Integer -> Integer) -> Integer -> Integer
forall a b. (a -> b) -> a -> b
$ Proxy n -> Integer
forall (p :: N) (proxy :: N -> *).
KnownPeano p =>
proxy p -> Integer
peanoVal (Proxy n
forall k (t :: k). Proxy t
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)