{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE GADTs                 #-}

module Generics.MultiRec.LR where

import Generics.MultiRec

-----------------------------------------------------------------------------
-- Functions for generating values that are different on top-level.
-----------------------------------------------------------------------------

-- | The @LRBase@ class defines two functions, @leftb@ and @rightb@, which 
-- should produce different values.
class LRBase a where
  leftb  :: a
  rightb :: a

instance LRBase Int where
  leftb  = 0
  rightb = 1

instance LRBase Integer where
  leftb  = 0
  rightb = 1

instance LRBase Char where
  leftb  = 'L'
  rightb = 'R'
 
instance LRBase Bool where
  leftb  = True
  rightb = False

instance LRBase a => LRBase [a] where
  leftb  = []
  rightb = [rightb]

-- | The @LR@ class defines two functions, @leftf@ and @rightf@, which should 
-- produce different functorial values.
class LR phi (f :: (* -> *) -> * -> *) where
--    leftf  :: s ix -> (forall ix . Ix s ix => s ix -> r ix) -> [f s r ix]
  leftf  :: phi ix -> (forall ix'. El phi ix' => phi ix' -> r ix') -> [f r ix]
  rightf :: phi ix -> (forall ix'. El phi ix' => phi ix' -> r ix') -> [f r ix]
 
instance El phi xi => LR phi (I xi) where
  leftf  _ f = [I (f proof)]
  rightf _ f = [I (f proof)]

instance LRBase a => LR phi (K a) where
  leftf  _ _ = [K leftb]
  rightf _ _ = [K rightb]

instance LR phi U where
  leftf  _ _ = [U]
  rightf _ _ = [U]

instance (LR phi f, LR phi g) => LR phi (f :+: g) where
  leftf  p f = map L (leftf  p f) ++ map R (leftf  p f)
  rightf p f = map R (rightf p f) ++ map L (rightf p f)

instance (LR phi f, LR phi g) => LR phi (f :*: g) where
  leftf  p f = zipWith (:*:) (leftf  p f) (leftf  p f)
  rightf p f = zipWith (:*:) (rightf p f) (rightf p f)

instance LR phi f => LR phi (C c f) where
  leftf  p f = map C (leftf  p f)
  rightf p f = map C (rightf p f)

instance (El phi ix, LR phi f, EqS phi) => LR phi (f :>: ix) where
  leftf  p f = case eqS (proof :: phi ix) p of
    Just Refl -> map Tag (leftf  p f)
    Nothing   -> []
  rightf p f = case eqS (proof :: phi ix) p of
    Just Refl -> map Tag (rightf  p f)
    Nothing   -> []

instance LR phi f => LR phi ([] :.: f) where
  leftf  p f = [D []]
  rightf p f = map (\v -> D [v]) $ rightf p f

left :: (Fam phi, LR phi (PF phi)) => phi ix -> ix
left p = to p $ safeHead $ leftf p (I0 . left)

right :: (Fam phi, LR phi (PF phi)) => phi ix -> ix
right p = to p $ safeHead $ rightf p (I0 . right)

safeHead [] = error "Internal error, left or right returned []"
safeHead (x:xs) = x