```{-
Number.hs

This file is part of Session Types for Haskell.

Session Types for Haskell is free software: you can redistribute it
and/or modify it under the terms of the GNU General Public License

Session Types for Haskell is distributed in the hope that it will
be useful, but WITHOUT ANY WARRANTY; without even the implied
warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
See the GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with Session Types for Haskell.
-}

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances, OverlappingInstances #-}

-- | Type level Integers. These are all base 10.

module Control.Concurrent.Session.Number
( E (..)
, D0 (..)
, D1 (..)
, D2 (..)
, D3 (..)
, D4 (..)
, D5 (..)
, D6 (..)
, D7 (..)
, D8 (..)
, D9 (..)
, Succ (..)
, Pred (..)
, SmallerThan
, TyNum
, TypeNumberToInt (..)
) where

{-
This module provides basic arithmetic for numbers at the type level.
-}

data E = E deriving (Show)
data D0 n = D0 n deriving (Show)
data D1 n = D1 n deriving (Show)
data D2 n = D2 n deriving (Show)
data D3 n = D3 n deriving (Show)
data D4 n = D4 n deriving (Show)
data D5 n = D5 n deriving (Show)
data D6 n = D6 n deriving (Show)
data D7 n = D7 n deriving (Show)
data D8 n = D8 n deriving (Show)
data D9 n = D9 n deriving (Show)

class Reverse x y | x -> y, y -> x where
tyReverse :: x -> y
instance (Reverse' x E y) => Reverse x y where
tyReverse x = tyReverse' x E

class Reverse' x a z | x a -> z where
tyReverse' :: x -> a -> z
instance Reverse' E a a where
tyReverse' _ a = a
instance (Reverse' n (D0 a) r) => Reverse' (D0 n) a r where
tyReverse' (D0 n) a = tyReverse' n (D0 a)
instance (Reverse' n (D1 a) r) => Reverse' (D1 n) a r where
tyReverse' (D1 n) a = tyReverse' n (D1 a)
instance (Reverse' n (D2 a) r) => Reverse' (D2 n) a r where
tyReverse' (D2 n) a = tyReverse' n (D2 a)
instance (Reverse' n (D3 a) r) => Reverse' (D3 n) a r where
tyReverse' (D3 n) a = tyReverse' n (D3 a)
instance (Reverse' n (D4 a) r) => Reverse' (D4 n) a r where
tyReverse' (D4 n) a = tyReverse' n (D4 a)
instance (Reverse' n (D5 a) r) => Reverse' (D5 n) a r where
tyReverse' (D5 n) a = tyReverse' n (D5 a)
instance (Reverse' n (D6 a) r) => Reverse' (D6 n) a r where
tyReverse' (D6 n) a = tyReverse' n (D6 a)
instance (Reverse' n (D7 a) r) => Reverse' (D7 n) a r where
tyReverse' (D7 n) a = tyReverse' n (D7 a)
instance (Reverse' n (D8 a) r) => Reverse' (D8 n) a r where
tyReverse' (D8 n) a = tyReverse' n (D8 a)
instance (Reverse' n (D9 a) r) => Reverse' (D9 n) a r where
tyReverse' (D9 n) a = tyReverse' n (D9 a)

class IncrementRightToLeft x y | x -> y where
tyIncrementRightToLeft :: x -> y
instance IncrementRightToLeft E (D1 E) where
tyIncrementRightToLeft _ = (D1 E)
instance IncrementRightToLeft (D0 a) (D1 a) where
tyIncrementRightToLeft (D0 a) = (D1 a)
instance IncrementRightToLeft (D1 a) (D2 a) where
tyIncrementRightToLeft (D1 a) = (D2 a)
instance IncrementRightToLeft (D2 a) (D3 a) where
tyIncrementRightToLeft (D2 a) = (D3 a)
instance IncrementRightToLeft (D3 a) (D4 a) where
tyIncrementRightToLeft (D3 a) = (D4 a)
instance IncrementRightToLeft (D4 a) (D5 a) where
tyIncrementRightToLeft (D4 a) = (D5 a)
instance IncrementRightToLeft (D5 a) (D6 a) where
tyIncrementRightToLeft (D5 a) = (D6 a)
instance IncrementRightToLeft (D6 a) (D7 a) where
tyIncrementRightToLeft (D6 a) = (D7 a)
instance IncrementRightToLeft (D7 a) (D8 a) where
tyIncrementRightToLeft (D7 a) = (D8 a)
instance IncrementRightToLeft (D8 a) (D9 a) where
tyIncrementRightToLeft (D8 a) = (D9 a)
instance (IncrementRightToLeft a b) => IncrementRightToLeft (D9 a) (D0 b) where
tyIncrementRightToLeft (D9 a) = D0 (tyIncrementRightToLeft a)

class Succ x y | x -> y where
tySucc :: x -> y
instance (Reverse a a', IncrementRightToLeft a' b', Reverse b' b) => Succ a b where
tySucc = tyReverse . tyIncrementRightToLeft . tyReverse

class DecrementRightToLeft x y | x -> y where
tyDecrementRightToLeft :: x -> y
instance DecrementRightToLeft (D9 a) (D8 a) where
tyDecrementRightToLeft (D9 a) = (D8 a)
instance DecrementRightToLeft (D8 a) (D7 a) where
tyDecrementRightToLeft (D8 a) = (D7 a)
instance DecrementRightToLeft (D7 a) (D6 a) where
tyDecrementRightToLeft (D7 a) = (D6 a)
instance DecrementRightToLeft (D6 a) (D5 a) where
tyDecrementRightToLeft (D6 a) = (D5 a)
instance DecrementRightToLeft (D5 a) (D4 a) where
tyDecrementRightToLeft (D5 a) = (D4 a)
instance DecrementRightToLeft (D4 a) (D3 a) where
tyDecrementRightToLeft (D4 a) = (D3 a)
instance DecrementRightToLeft (D3 a) (D2 a) where
tyDecrementRightToLeft (D3 a) = (D2 a)
instance DecrementRightToLeft (D2 a) (D1 a) where
tyDecrementRightToLeft (D2 a) = (D1 a)
instance DecrementRightToLeft (D1 a) (D0 a) where
tyDecrementRightToLeft (D1 a) = (D0 a)
instance (DecrementRightToLeft a b) => DecrementRightToLeft (D0 a) (D9 b) where
tyDecrementRightToLeft (D0 a) = D9 (tyDecrementRightToLeft a)

class StripLeadingZeros x y | x -> y where
instance StripLeadingZeros (D0 E) (D0 E) where
instance StripLeadingZeros (D1 a) (D1 a) where
instance StripLeadingZeros (D2 a) (D2 a) where
instance StripLeadingZeros (D3 a) (D3 a) where
instance StripLeadingZeros (D4 a) (D4 a) where
instance StripLeadingZeros (D5 a) (D5 a) where
instance StripLeadingZeros (D6 a) (D6 a) where
instance StripLeadingZeros (D7 a) (D7 a) where
instance StripLeadingZeros (D8 a) (D8 a) where
instance StripLeadingZeros (D9 a) (D9 a) where

class Pred x y | x -> y where
tyPred :: x -> y
instance ( Reverse a a'
, DecrementRightToLeft a' b'
, Reverse b' b''
=> Pred a b where
tyPred = tyStripLeadingZeros . tyReverse . tyDecrementRightToLeft . tyReverse

class Add m n s | m n -> s where
tyAdd :: m -> n -> s
instance Add (D0 E) (D0 E) (D0 E) where
tyAdd _ _ = D0 E
instance (Pred m m') => Add m (D0 E) m where
tyAdd m (D0 E) = m
instance (Pred n n') => Add (D0 E) n n where
tyAdd (D0 E) n = n
instance (Add m' n' s, Pred m m', Pred n n', Succ s s', Succ s' s'') => Add m n s'' where
tyAdd m n = tySucc . tySucc \$ tyAdd (tyPred m) (tyPred n)

class SmallerThan x y -- x < y
instance (Pred y y') => SmallerThan (D0 E) y
instance (Pred x x', Pred y y', SmallerThan x' y') => SmallerThan x y

class TyNum n
instance TyNum (D0 E)
instance TyNum (D1 E)
instance TyNum (D2 E)
instance TyNum (D3 E)
instance TyNum (D4 E)
instance TyNum (D5 E)
instance TyNum (D6 E)
instance TyNum (D7 E)
instance TyNum (D8 E)
instance TyNum (D9 E)
instance (TyNum n) => TyNum (D0 n)
instance (TyNum n) => TyNum (D1 n)
instance (TyNum n) => TyNum (D2 n)
instance (TyNum n) => TyNum (D3 n)
instance (TyNum n) => TyNum (D4 n)
instance (TyNum n) => TyNum (D5 n)
instance (TyNum n) => TyNum (D6 n)
instance (TyNum n) => TyNum (D7 n)
instance (TyNum n) => TyNum (D8 n)
instance (TyNum n) => TyNum (D9 n)

-- | Convert a type-level number to an Int. Of course, we can only go this way...
class TypeNumberToInt ty where
tyNumToInt :: ty -> Int
instance TypeNumberToInt (D0 E) where
tyNumToInt _ = 0
instance (Pred a b, TypeNumberToInt b) => TypeNumberToInt a where
tyNumToInt n = 1 + (tyNumToInt (tyPred n))
```