{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, FlexibleContexts, UndecidableInstances #-}

module Data.Typical where

import Data.Typical.Misc


-- the HCons and HNil datatype
--
data a :#: b = a :#: b

infixr :#:

data HNil = HNil

-- basic list operations

class HHead a h | a -> h where
        hHead :: a -> h

instance HHead (a :#: b) a where
        hHead (a :#: _) = a

class HTail a t | a -> t where
        hTail :: a -> t

instance HTail (a :#: b) b where
        hTail (_ :#: b) = b


class HSplitAt a n h t | a n -> h t where
	hSplitAt :: a -> n -> (h, t)

instance HSplitAt HNil n HNil HNil where
	hSplitAt HNil _ = (HNil, HNil)

instance HSplitAt (a :#: b) HNil (a :#: HNil) b where
	hSplitAt (a :#: b) HNil = (a :#: HNil, b)

instance (HSub (d :#: d') HNil predD, HSplitAt b predD a' b') 
	=> HSplitAt (a :#: b) (d :#: d') (a :#: a') b' where
	hSplitAt (a :#: b) d = let (a', b') = hSplitAt b (hSub d HNil) in (a :#: a' , b')


class HMergeBy f a b c | f a b -> c where
	hMergeBy :: f -> a -> b -> c

instance HMergeBy f HNil HNil HNil where
	hMergeBy _ HNil HNil = HNil

instance HMergeBy f HNil (a :#: b) (a :#: b) where
	hMergeBy _ HNil (a :#: b) = a :#: b

instance HMergeBy f (a :#: b) HNil (a :#: b) where
	hMergeBy _ (a :#: b) HNil = a :#: b

instance (HApply f (a, c) cmp, HOrd cmp (a :#: b) (c :#: d) h a' b', HMergeBy f a' b' e)
	=> HMergeBy f (a :#: b) (c :#: d) (h :#: e) where
	hMergeBy f (a :#: b) (c :#: d) = let 
		cmp = hApply f (a, c)
		(h, a', b') = hOrd cmp (a :#: b) (c :#: d)
		e = hMergeBy f a' b'
		in (h :#: e)

{-
class HSortBy f a b | f a -> b where
	hSortBy :: f -> a -> b

class HRunsBy f cmp a tmp tmp' res | f cmp a tmp -> tmp' res where
	hRunsBy :: f -> cmp -> a -> tmp -> (tmp', res)

instance (HRunsBy f cmp (b :#: c :#: d) tmp tmp' res, HApply f (b, c) cmp) 
	=> HRunsBy f HLT (a :#: b :#: c :#: d) tmp (a :#: tmp', res)

instance (HRunsBy f cmp (b :#: c :#: d) tmp tmp' res, HApply f (b, c) cmp) 
        => HRunsBy f HEQ (a :#: b :#: c :#: d) tmp (a :#: tmp', res)

instance (HRunsBy f cmp (b :#: c :#: d) tmp tmp' res, HApply f (b, c) cmp) 
        => HRunsBy f HGT (a :#: b :#: c :#: d) tmp (a :#: HNil, tmp :#: res)

-}

-- the apply class for function objects
--

class HApply f parameter result | f parameter -> result where
	hApply :: f -> parameter -> result


-- the atoms of numbers (binary digits)
--
data B0 = B0
data B1 = B1

-- the class of natural numbers
class HNat a

instance HNat (B1 :#: HNil)
instance HNat a => HNat (B1 :#: a)
instance HNat a => HNat (B0 :#: a)

type N1 = HNil
type N2 = B0 :#: HNil
type N3 = B1 :#: HNil
type N4 = B0 :#: N2

n1 :: N1
n1 = HNil

n2 :: N2
n2 = B0 :#: HNil

n3 :: N3
n3 = B1 :#: HNil

n4 :: N4
n4 = B0 :#: n2


-- addition

class HAdd n1 n2 r | n1 n2 -> r where
	hAdd :: n1 -> n2 -> r

instance HAdd HNil HNil (B0 :#: HNil) where
	hAdd HNil HNil = (B0 :#: HNil)

instance HAdd HNil (B0 :#: b) (B1 :#: b) where
	hAdd HNil (B0 :#: b) = B1 :#: b

instance HAdd (B0 :#: a) HNil (B1 :#: a) where
	hAdd (B0 :#: a) HNil = B1 :#: a

instance HAdd HNil b b' => HAdd HNil (B1 :#: b) (B0 :#: b') where
	hAdd HNil (B1 :#: b) = B0 :#: hAdd HNil b

instance HAdd HNil a a' => HAdd (B1 :#: a) HNil (B0 :#: a') where
	hAdd (B1 :#: a) HNil = B0 :#: hAdd HNil a

instance HAdd a b c => HAdd (B0 :#: a) (B0 :#: b) (B0 :#: c) where
	hAdd (B0 :#: a) (B0 :#: b) = B0 :#: hAdd a b

instance HAdd a b c => HAdd (B0 :#: a) (B1 :#: b) (B1 :#: c) where
        hAdd (B0 :#: a) (B1 :#: b) = B1 :#: hAdd a b

instance HAdd a b c => HAdd (B1 :#: a) (B0 :#: b) (B1 :#: c) where
        hAdd (B1 :#: a) (B0 :#: b) = B1 :#: hAdd a b

instance (HAdd a b c, HAdd HNil c c') => HAdd (B1 :#: a) (B1 :#: b) (B0 :#: c') where
        hAdd (B1 :#: a) (B1 :#: b) = B0 :#: hAdd HNil (hAdd a b)


-- substraction
--

class HSub n1 n2 r | n1 n2 -> r where
	hSub :: n1 -> n2 -> r

instance HSub (B1 :#: b) HNil (B0 :#: b) where
	hSub (B1 :#: b) HNil = B0 :#: b

instance HSub (B0 :#: HNil) HNil HNil where
	hSub (B0 :#: HNil) HNil = HNil

instance HSub (B1 :#: HNil) (B0 :#: HNil) HNil where
        hSub (B1 :#: HNil) (B0 :#: HNil) = HNil

instance HSub (b :#: c) HNil d => HSub (B0 :#: b :#: c) HNil (B1 :#: d) where
	hSub (B0 :#: b :#: c) HNil = B1 :#: hSub (b :#: c) HNil

instance HSub a b c => HSub (B0 :#: a) (B0 :#: b) (B0 :#: c) where
	hSub (B0 :#: a) (B0 :#: b) = B0 :#: hSub a b

instance HSub (a :#: b) c d => HSub (B1 :#: a :#: b) (B0 :#: c) (B1 :#: d) where
	hSub (B1 :#: a :#: b) (B0 :#: c) = B1 :#: hSub (a :#: b) c

instance (HAdd b N1 b', HSub a b' c) => HSub (B0 :#: a) (B1 :#: b) (B1 :#: c) where
	hSub (B0 :#: a) (B1 :#: b) = B1 :#: hSub a (hAdd b HNil)

instance HSub a b c => HSub (B1 :#: a) (B1 :#: b) (B0 :#: c) where
	hSub (B1 :#: a) (B1 :#: b) = B0 :#: hSub a b


-- multiplication
--

class HMul a b c | a b -> c where
	hMul :: a -> b -> c

class HMulSub a b c | a b -> c where
	hMulSub :: a -> b -> c

instance HMulSub HNil a (a :#: HNil) where
	hMulSub HNil a = (a :#: HNil)

instance HMulSub b (B0 :#: c) r => HMulSub (B0 :#: b) c r where
	hMulSub (B0 :#: b) c = hMulSub b (B0 :#: c)

instance HMulSub b (B0 :#: c) r => HMulSub (B1 :#: b) c (c :#: r) where
	hMulSub (B1 :#: b) c = let r = hMulSub b (B0 :#: c) in (c :#: r)

-- comparism

instance HCompare B0 B0 HEQ where
	hCompare B0 B0 = HEQ

instance HCompare B0 B1 HLT where
        hCompare B0 B1 = HLT

instance HCompare B1 B0 HGT where
        hCompare B1 B0 = HGT

instance HCompare B1 B1 HEQ where
        hCompare B1 B1 = HEQ


instance HCompare HNil HNil HEQ where
	hCompare HNil HNil = HEQ

instance HCompare HNil (c :#: d) HLT where
	hCompare HNil (_ :#: _) = HLT

instance HCompare (a :#: b) HNil HGT where
	hCompare (_ :#: _) HNil = HGT

instance (HCompare a c res1, HCompare b d res2, CalcRes res1 res2 res) 
	=> HCompare (a :#: b) (c :#: d) res where
	hCompare (a :#: b) (c :#: d) = calcRes (hCompare a c) (hCompare b d)

class CalcRes a b c | a b -> c where
	calcRes :: a -> b -> c

instance CalcRes a HLT HLT where
	calcRes _ HLT = HLT

instance CalcRes a HGT HGT where
	calcRes _ HGT = HGT

instance CalcRes HLT HEQ HLT where
	calcRes HLT HEQ = HLT

instance CalcRes HGT HEQ HGT where
	calcRes HGT HEQ = HGT

instance CalcRes HEQ HEQ HEQ where
	calcRes HEQ HEQ = HEQ


class HOrd cmp a b h a' b' | cmp a b -> h a' b' where
	hOrd :: cmp -> a -> b -> (h, a', b')

instance HOrd HLT (ha :#: ta) (hb :#: tb) ha ta (hb :#: tb) where
	hOrd HLT (ha :#: ta) (hb :#: tb) = (ha, ta, hb :#: tb)

instance HOrd HGT (ha :#: ta) (hb :#: tb) hb (ha :#: ta) tb where
	hOrd HGT (ha :#: ta) (hb :#: tb) = (hb, ha :#: ta, tb)

instance HOrd HEQ (ha :#: ta) (hb :#: tb) ha ta (hb :#: tb) where
	hOrd HEQ (ha :#: ta) (hb :#: tb) = (ha, ta, hb :#: tb)


-- simple math
--

class HDiv2 a b | a -> b where
	hDiv2 :: a -> b

instance HDiv2 HNil HNil where
	hDiv2 HNil = HNil

instance HDiv2 (a :#: b) b where
	hDiv2 (_ :#: b) = b



-- tests
--
--

data HCmpHNat = HCmpHNat
instance HCompare a b cmp => HApply HCmpHNat (a, b) cmp where
	hApply HCmpHNat (a, b) = hCompare a b

x :: (N2 :#: N2 :#: N3 :#: N4 :#: HNil)
x = hMergeBy HCmpHNat (n2 :#: n3 :#: HNil) ((n4 `hSub` n2) :#: n4 :#: HNil)