module Data.PeanoNat where

import GHC.TypeNats
import Import
import Numeric.Natural

-- | Inductive natural numbers.
data PeanoNat
    = Zero
    | Succ PeanoNat

addPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat
addPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat
addPeanoNat PeanoNat
Zero PeanoNat
b = PeanoNat
b
addPeanoNat (Succ PeanoNat
a) PeanoNat
b = PeanoNat -> PeanoNat
Succ forall a b. (a -> b) -> a -> b
$ PeanoNat -> PeanoNat -> PeanoNat
addPeanoNat PeanoNat
a PeanoNat
b

type Add :: PeanoNat -> PeanoNat -> PeanoNat
type family Add a b where
    Add 'Zero b = b
    Add ('Succ a) b = 'Succ (Add a b)

-- | subtractFromPeanoNat a b = b - a
subtractFromPeanoNat :: PeanoNat -> PeanoNat -> Maybe PeanoNat
subtractFromPeanoNat :: PeanoNat -> PeanoNat -> Maybe PeanoNat
subtractFromPeanoNat PeanoNat
Zero PeanoNat
b = forall a. a -> Maybe a
Just PeanoNat
b
subtractFromPeanoNat (Succ PeanoNat
a) (Succ PeanoNat
b) = PeanoNat -> PeanoNat -> Maybe PeanoNat
subtractFromPeanoNat PeanoNat
a PeanoNat
b
subtractFromPeanoNat (Succ PeanoNat
_) PeanoNat
Zero = forall a. Maybe a
Nothing

multiplyPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat
multiplyPeanoNat :: PeanoNat -> PeanoNat -> PeanoNat
multiplyPeanoNat PeanoNat
Zero PeanoNat
_ = PeanoNat
Zero
multiplyPeanoNat (Succ PeanoNat
a) PeanoNat
b = PeanoNat -> PeanoNat -> PeanoNat
addPeanoNat (PeanoNat -> PeanoNat -> PeanoNat
multiplyPeanoNat PeanoNat
a PeanoNat
b) PeanoNat
b

peanoToNatural :: PeanoNat -> Natural
peanoToNatural :: PeanoNat -> Natural
peanoToNatural PeanoNat
Zero = Natural
0
peanoToNatural (Succ PeanoNat
n) = forall a. Enum a => a -> a
succ forall a b. (a -> b) -> a -> b
$ PeanoNat -> Natural
peanoToNatural PeanoNat
n

naturalToPeano :: Natural -> PeanoNat
naturalToPeano :: Natural -> PeanoNat
naturalToPeano Natural
0 = PeanoNat
Zero
naturalToPeano Natural
n = PeanoNat -> PeanoNat
Succ forall a b. (a -> b) -> a -> b
$ Natural -> PeanoNat
naturalToPeano forall a b. (a -> b) -> a -> b
$ forall a. Enum a => a -> a
pred Natural
n

type PeanoToNatural :: PeanoNat -> Nat
type family PeanoToNatural pn where
    PeanoToNatural 'Zero = 0
    PeanoToNatural ('Succ pn) = PeanoToNatural pn + 1

type ListLength :: forall k. [k] -> PeanoNat
type family ListLength l where
    ListLength '[] = 'Zero
    ListLength (a ': aa) = 'Succ (ListLength aa)