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
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)
type instance ADD (X0_ a) X0 = APP0 a
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
type instance ADD (X1_ a) X0 = APP1 a
type instance ADD (X1_ a) (X0_ b) = APP1 (ADD a b)
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)
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)
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)
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 = "-"