module Prelude.Type.Integer (
Integer(..), I,
IntegerCons, IntegerHead, IntegerTail
) where
import Prelude (Bool(..))
import GHC.TypeLits
data Integer = One Integer | Zero Integer | Ones | Zeros
type family I (a :: Nat) :: Integer
type instance I 0 = Zeros
type instance I 1 = One Zeros
type instance I 2 = Zero (One (Zeros))
type instance I 3 = One (One Zeros)
type instance I 4 = Zero (Zero (One Zeros))
type instance I 5 = One (Zero (One Zeros))
type instance I 6 = Zero (One (One Zeros))
type instance I 7 = One (One (One Zeros))
type instance I 8 = Zero (Zero (Zero (One Zeros)))
type instance I 9 = One (Zero (Zero (One Zeros)))
type instance I 10 = Zero (One (Zero (One Zeros)))
type instance I 11 = One (One (Zero (One Zeros)))
type instance I 12 = Zero (Zero (One (One Zeros)))
type instance I 13 = One (Zero (One (One Zeros)))
type instance I 14 = Zero (One (One (One Zeros)))
type instance I 15 = One (One (One (One Zeros)))
type family IntegerHead (i :: Integer) :: Bool
type instance IntegerHead Zeros = False
type instance IntegerHead Ones = True
type instance IntegerHead (One i) = True
type instance IntegerHead (Zero i) = False
type family IntegerTail (i :: Integer) :: Integer
type instance IntegerTail Zeros = Zeros
type instance IntegerTail Ones = Ones
type instance IntegerTail (One i) = i
type instance IntegerTail (Zero i) = i
type family IntegerCons (b :: Bool) (i :: Integer) :: Integer
type instance IntegerCons False Zeros = Zeros
type instance IntegerCons True Zeros = One Zeros
type instance IntegerCons False Ones = Zero Ones
type instance IntegerCons True Ones = Ones
type instance IntegerCons False (Zero i) = Zero (Zero i)
type instance IntegerCons True (Zero i) = One (Zero i)
type instance IntegerCons False (One i) = Zero (One i)
type instance IntegerCons True (One i) = One (One i)