{-# OPTIONS -fglasgow-exts #-}
{-# OPTIONS -fallow-overlapping-instances #-}
{-# OPTIONS -fallow-undecidable-instances #-}

module Joy where

import MainGhcGeneric1

data Lit a = Lit a 
instance Apply (Lit a) s (HCons a s) where
	apply (Lit a) s = HCons a s

data If = If
instance Apply t s s' => Apply If (HCons f (HCons t (HCons HTrue s))) s' where
	apply _ (HCons _ (HCons t (HCons _ s))) = apply t s
instance Apply f s s' => Apply If (HCons f (HCons t (HCons HFalse s))) s' where
	apply _ (HCons f (HCons _ (HCons _ s))) = apply f s

data Eq = Eq
instance TypeEq a b t => Apply Eq (HCons a (HCons b s)) (HCons t s) where
	apply _ (HCons a (HCons b s)) = HCons (typeEq a b) s

data Dip = Dip
instance Apply a s s' => Apply Dip (HCons a (HCons b s)) (HCons b s') where
	apply _ (HCons a (HCons b s)) = HCons b (apply a s)

data Dup = Dup
instance Apply Dup (HCons a s) (HCons a (HCons a s)) where
	apply _ s@(HCons a _) = HCons a s

data Pop = Pop
instance Apply Pop (HCons a s) s where
	apply _ (HCons _ s) = s

data Swap = Swap
instance Apply Swap (HCons a (HCons b s)) (HCons b (HCons a s)) where
	apply _ (HCons a (HCons b s)) = HCons b (HCons a s)

class (HNat a,HNat b) => HAdd a b c | a -> b -> c where
	hadd :: a -> b -> c
instance HAdd HZero HZero HZero where
	hadd _ _ = hZero
instance HAdd HZero (HSucc b) (HSucc b) where
	hadd _ b = b
instance HAdd a b c => HAdd (HSucc a) (HSucc b) (HSucc (HSucc c))
	hadd _ _ = hadd (undefined::a) (undefined::b)

data Add = Add
instance HAdd a b c => Apply Add (HCons a (HCons b s)) (HCons c s) where
	apply _ (HCons _ (HCons _ s)) = HCons (hadd (undefined::a) (undefined::b)) s

data Mult = Mult
instance HMult a b c => Apply Mult (HCons a (HCons b s)) (HCons c s) where
	apply _ (HCons _ (HCons _ s)) = HCons (hadd (undefined::a) (undefined::b)) s

data a @ b = a @ b
instance (Apply a s s',Apply b s' s'') => Apply (a @ b) s'' where
	apply (O a b) s = apply b (apply a s :: s')

type Square = Dup @ Mult
type Cube = Dup @ Dup @ Mult

data I = I
instance Apply a s s' => Apply I (HCons a s) s' where
	apply _ (HCons a s) = apply a s

data Times = Times
instance Apply Times (HCons p (HCons HZero s)) s where
	apply _ (HCons _ s) = s
instance Apply p s s' => Apply Times (HCons p (HCons (HSucc n) s) (HCons p (HCons n s')) where
	apply _ (HCons p (HCons _ s)) = HCons p (HCons (undefined::n) (apply p s))