{-# LANGUAGE DataKinds, PolyKinds, KindSignatures, TypeFamilies #-}

module Prelude.Type.Integer (
  -- | Two's complement integers
  -- 
  -- (One Ones) and (Zero Zeros) are malformed Integers. They can cause
  -- bugs if passed as a paramter and they are never returned.
  -- IntegerCons builds integers that are well formed and should be used
  -- instead of One or Zero
  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)