-- | Basic type-level arithmetic, using base two.
-- 
-- Copyright: (c) 2009 University of Kansas
-- License: BSD3
--
-- Maintainer: Andy Gill <andygill@ku.edu>
-- Stability: unstable
-- Portability: ghc


{-# LANGUAGE TypeFamilies, EmptyDataDecls, UndecidableInstances  #-}
module Data.Sized.Arith where

import Data.Ix

data N1

data X0 = X0
	deriving (Eq,Ord)

data X0_ a = X0_ Int
data X1_ a = X1_ Int


type family ADD a b
type instance ADD N1 N1 = APP0 N1
type instance ADD N1 X0 = N1
type instance ADD N1 (X0_ b) = APP1 (ADD N1 b)
type instance ADD N1 (X1_ b) = APP0 b
type instance ADD X0 N1 = N1					-- MIR
type instance ADD X0 X0 = X0
type instance ADD X0 (X0_ b) = X0_ b
type instance ADD X0 (X1_ b) = APP1 b
type instance ADD (X0_ a) N1 = APP1 (ADD a N1)			-- MIR
type instance ADD (X0_ a) X0 = APP0 a				-- MIR
type instance ADD (X0_ a) (X0_ b) = APP0 (ADD a b)
type instance ADD (X0_ a) (X1_ b) = APP1 (ADD a b)
type instance ADD (X1_ a) N1 = APP0 a				-- MIR
type instance ADD (X1_ a) X0 = APP1 a				-- MIR
type instance ADD (X1_ a) (X0_ b) = APP1 (ADD a b)		-- MIR
type instance ADD (X1_ a) (X1_ b) = APP0 (SUCC (ADD a b))

type family NOT a
type instance NOT N1 = X0
type instance NOT X0 = N1
type instance NOT (X0_ a) = APP1 (NOT a)  
type instance NOT (X1_ a) = APP0 (NOT a)


type SUB a b = ADD a (SUCC (NOT b))


type family SUCC a
type instance SUCC N1 = X0
type instance SUCC X0 = X1_ X0
type instance SUCC (X0_ a) = APP1 a
type instance SUCC (X1_ a) = APP0 (SUCC a)

type family APP1 a
type instance APP1 N1 = N1
type instance APP1 X0 = X1_ X0
type instance APP1 (X0_ a) = X1_ (X0_ a)
type instance APP1 (X1_ a) = X1_ (X1_ a)

type family APP0 a
type instance APP0 N1 = X0_ N1
type instance APP0 X0 = X0
type instance APP0 (X0_ a) = X0_ (X0_ a)
type instance APP0 (X1_ a) = X0_ (X1_ a)

--- instances


instance Eq (X0_ a) where
	(X0_ a) == (X0_ b) = a == b

instance Ord (X0_ a) where
	(X0_ a) `compare` (X0_ b) = a `compare` b


instance Ix (X0_ a) where
	range (X0_ a,X0_ b) = map X0_ (range (a,b))
	index (X0_ a,X0_ b) (X0_ i) = index (a,b) i
	inRange (X0_ a,X0_ b) (X0_ i) = inRange (a,b) i

instance Enum (X0_ a) where
	toEnum n = (X0_ n)
	fromEnum (X0_ n) = n

instance Num (X0_ a) where
	fromInteger n = X0_ (fromInteger n)	-- bounds checking needed!
	abs a = a 
	signum (X0_ a) = if a == 0 then 0 else 1
	(X0_ a) + (X0_ b) = X0_ (a + b)
	(X0_ a) - (X0_ b) = X0_ (a - b)
	(X0_ a) * (X0_ b) = X0_ (a * b)


instance Show (X0_ a) where
	show (X0_ a) = show a
	
instance Eq (X1_ a) where
	(X1_ a) == (X1_ b) = a == b

instance Ord (X1_ a) where
	(X1_ a) `compare` (X1_ b) = a `compare` b



instance Ix (X1_ a) where
	range (X1_ a,X1_ b) = map X1_ (range (a,b))
	index (X1_ a,X1_ b) (X1_ i) = index (a,b) i
	inRange (X1_ a,X1_ b) (X1_ i) = inRange (a,b) i

instance Enum (X1_ a) where
	toEnum n = (X1_ n)
	fromEnum (X1_ n) = n

instance Num (X1_ a) where
	fromInteger n = X1_ (fromInteger n)	-- bounds checking needed!
	abs a = a 
	signum (X1_ a) = if a == 0 then 0 else 1
	(X1_ a) + (X1_ b) = X1_ (a + b)
	(X1_ a) - (X1_ b) = X1_ (a - b)
	(X1_ a) * (X1_ b) = X1_ (a * b)

instance Show (X1_ a) where
	show (X1_ a) = show a

instance Bounded X0 where
	minBound = error "minBound not defined"
	maxBound = error "maxBound not defined"

instance Ix X0 where
	range (X0,X0) = []
	inRange (X0,X0) X0 = False


instance Show X0 where
	show X0 = "-"