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

module Generics.MultiRec.Rewriting.LeftRight where

import Generics.MultiRec.Base

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

class Single (s :: * -> *) (f :: (* -> *) -> * -> *) where
  singlef :: s ix -> (forall ix'. Fam s => s ix' -> r ix') -> Bool -> [f r ix]

instance (Single s a, Single s b) => Single s (a :+: b) where
  singlef w f True  = map L (singlef w f True ) ++ map R (singlef w f True)
  singlef w f False = map R (singlef w f False) ++ map L (singlef w f False)

instance (Single s a) => Single s (C c a) where
  singlef w f b = map C (singlef w f b)

instance (Single s a, Single s b) => Single s (a :*: b) where
  singlef w f b = zipWith (:*:) (singlef w f b) (singlef w f b)

instance (Fam s, El s ixr) => Single s (I ixr) where
  singlef _ f _ = [I (f proof)]

instance LRA a => Single s (K a) where
  singlef _ _ True  = [K lefta]
  singlef _ _ False = [K righta]

instance Single s U where
  singlef _ _ _ = [U]

instance (EqS s, El s ixt, Single s f) => Single s (f :>: ixt) where
  singlef w f b = case eqS (proof :: s ixt) w of
                    Nothing   -> []
                    Just Refl -> map Tag (singlef w f b)


-- Ad-hoc left/right
class LRA a where
  lefta  :: a
  righta :: a

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

instance LRA Integer where
  lefta  = 0
  righta = 1

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

safeHead :: [a] -> a
safeHead []    = error "Internal error, left or right returned []"
safeHead (x:_) = x


left :: (Fam s, Single s (PF s)) => s ix -> ix
left w = to w . safeHead $ singlef w (I0 . left) True

right :: (Fam s, Single s (PF s)) => s ix -> ix
right w = to w . safeHead $ singlef w (I0 . right) False