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

module LeftRight where

import Control.Monad

import Base
import TEq
import Repr

-- * Generation of left/right values
-- Ugly implementation for now.
-- Should be improved!

class LR (f :: (* -> *) -> (* -> *) -> * -> *) s where
  leftf  :: s ix -> (forall ix . Ix s ix => s ix -> r ix) -> [f s r ix]
  rightf :: s ix -> (forall ix . Ix s ix => s ix -> r ix) -> [f s r ix]

instance (LR a s,LR b s) => LR (a :+: b) s where
  leftf  w f = map L (leftf  w f) ++ map R (leftf  w f)
  rightf w f = map R (rightf w f) ++ map L (rightf w f)

instance (LR a s, LR b s) => LR (a :*: b) s where
  leftf  w f = zipWith (:*:) (leftf w f) (leftf w f)
  rightf w f = zipWith (:*:) (rightf w f) (rightf w f)

instance Ix s ixr => LR (I ixr) s where
  leftf   _ f = [I (f index)]
  rightf  _ f = [I (f index)]

instance LRA a => LR (K a) s where
  leftf  w f = [K lefta]
  rightf w f = [K righta]

class LRA a where
  lefta  :: a
  righta :: a


{-
 - This should be more efficient (compile time checking of Tag ls)

instance (Zero (f r s ix)) => LR (Tag ix f r s ix) where
  left  = [Tag zero]
  right = [Tag zero]

instance LR (Tag ix' f r s ix) where
  left  = []
  right = []
-}

-- The instance below can be used when no undecidable instances are desired.
-- In that case type comparisons are carried out at runtime

instance (Repr s,Ix s ixt,LR f s) => LR (f :>: ixt) s where
  leftf w f
    = case ixeq (index::s ixt) w of
        Nothing   -> []
        Just Refl -> map Tag (leftf w f)
  rightf w f
    = case ixeq (index::s ixt) w of
        Nothing   -> []
        Just Refl -> map Tag (rightf w f)

-- Ad-hoc left/right
instance LRA Char where
  lefta  = 'L'
  righta = 'R'

instance LRA a => LRA [a] where
  lefta  = []
  righta = [righta]

instance LRA Int where
  lefta  = 0
  righta = 1

-- Not very good for distinguishing constructors
instance LRA () where
  lefta  = ()
  righta = ()

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


left :: (Ix s ix, LR (PF s) s) => s ix -> ix
left w = to $ safeHead $ leftf w (I0 . left)

right :: (Ix s ix, LR (PF s) s) => s ix -> ix
right w = to $ safeHead $ rightf w (I0 . right)