module Data.Sized.Arith where
import Data.Ix
data N1
data X0 = X0
deriving (Eq,Ord)
data X0_ a = X0_ Integer
data X1_ a = X1_ Integer
type family ADD a b
type instance ADD N1 N1 = APP0 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_ a) N1 = APP1 (ADD a N1)
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_ b) = APP1 (ADD a b)
type instance ADD (X1_ a) (X1_ b) = APP0 (SUCC (ADD a b))
type instance ADD a X0 = a
type instance ADD X0 a = a
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 MUL a b
type instance MUL x X0 = X0
type instance MUL x (X0_ b) = ADD x (MUL x (ADD (X0_ b) N1))
type instance MUL x (X1_ b) = ADD x (MUL x (ADD (X1_ b) N1))
type instance MUL x N1 = SUB X0 x
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 LOG a
type instance LOG X0 = X0
type instance LOG (X0_ a) = ADD (X1_ X0) (LOG a)
type instance LOG (X1_ a) = ADD (X1_ X0) (LOG 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)