{-# LANGUAGE TemplateHaskell, TypeFamilies, QuasiQuotes, StandaloneDeriving,
  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,
  MultiParamTypeClasses, TypeOperators, EmptyDataDecls  #-}

{- |

Module      :  Data.Yoko.Generic
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

Maintainer  :  nicolas.frisby@gmail.com
Stability   :  experimental
Portability :  see LANGUAGE pragmas (... GHC)

Representations of many Haskell types as compositions of "Data.Yoko.Core"
types.

-}

module Data.Yoko.Generic
  (module Data.Yoko.Generic, module Data.Yoko.CoreTypes) where

import Data.Yoko.CoreTypes
--import qualified Data.Yoko.Core as Core

import Type.Yoko.Type
--import Type.Yoko.Universe ((:::)(..))

--import qualified Control.Arrow as Arrow
                       

{- | @RM@ stands is for \"recursively mediated\", and @m@ is the \"mediator (of
recursive occurrences)\".

@
  data instance RM m V
  data instance RM m U = U
  newtype instance RM m (D a) = D a
  newtype instance RM m (R t) = R (Med m t)
  newtype instance RM m (F f c) = F (f (RM m c))
  newtype instance RM m (FF ff c d) = FF (ff (RM m c) (RM m d))
  newtype instance RM m (M i c) = M (RM m c)
@

-}
data family RM m c
data instance RM m V
data instance RM m U = U
newtype instance RM m (D a) = D a
newtype instance RM m (R t) = R (Med m t)
newtype instance RM m (F f c) = F (f (RM m c))
newtype instance RM m (FF ff c d) =
  FF (ff (RM m c) (RM m d))
newtype instance RM m (M i c) = M (RM m c)

-- | In @yoko@, the 'N' core type is used for a lightweight representation of
-- constructor types -- each will define its own instance of @RM (N _)@.
type RMN m dc = RM m (N dc)

type RMI = RM IdM
type RMNI dc = RMN IdM dc



-- | @Generic@ represents a recursion-mediated type @N a@ as a
-- recursion-mediated @Rep a@. The opposite of \"representation\" is (the
-- represented) \"object\".
class Generic a where
  rep :: RM m (N a) -> RM m (Rep a)
  obj :: RM m (Rep a) -> RM m (N a)

{-asRep :: (Generic a, Generic b) => (RM m (Rep a) -> RM m (Rep b)) -> RM m (N a) -> RM m (N b)
asRep f = obj . f . rep

asGist :: (Gist c, Gist d) => (Gst c m -> Gst d n) -> RM m c -> RM n d
asGist f = frip . f . gist

convertR :: (Gist c, Gst c m ~ Gst c n) => RM m c -> RM n c
convertR = asGist id-}


{-
-- @gist@ folds the mediator @m@ into the type and forgets all the frippery of
-- the core representation. (The opposite of \"gist\" is \"frippery\".)
type family Gst c m
class Gist c where
  gist :: RM m c -> Gst c m
  frip :: Gst c m -> RM m c

data AsRep u t where AsRep :: u (Rep t) -> AsRep u t
instance (Rep t ::: u) => t ::: AsRep u where inhabits = AsRep inhabits

data GistD c where GistD :: Gist c => GistD c
instance Gist c => c ::: GistD where inhabits = GistD
gistD :: GistD c -> RM m c -> Gst c m; gistD GistD = gist
fripD :: GistD c -> Gst c m -> RM m c; fripD GistD = frip



type instance Gst (F f c) m = f (Gst c m)
instance (Functor f, Gist c) => Gist (F f c) where
  gist (F x) = fmap gist x
  frip = F . fmap frip
type instance Gst (FF Either c d) m = Either (Gst c m) (Gst d m)
instance (Gist c, Gist d) => Gist (FF Either c d) where
  gist = (gist Arrow.+++ gist) . unFF
  frip = FF . (frip Arrow.+++ frip)
type instance Gst (FF (,) c d) m = (,) (Gst c m) (Gst d m)
instance (Gist c, Gist d) => Gist (FF (,) c d) where
  gist = (gist Arrow.*** gist) . unFF
  frip = FF . (frip Arrow.*** frip)
type instance Gst (D a) m = a
instance Gist (D a) where gist (D x) = x; frip = D
type instance Gst (M i c) m = Gst c m
instance Gist c => Gist (M i c) where
  gist = gist . unM; frip = M . frip
type instance Gst (R t) m = Med m t
instance Gist (R t) where gist (R x) = x; frip = R
type instance Gst U m = ()
instance Gist U where gist _ = (); frip _ = U
type instance Gst V m = Core.V
instance Gist V where gist = absurd "gist[V]"; frip _ = void "gist[V]"
type instance Gst (N n) m = Gst (Rep n) m
instance (Generic t, Gist (Rep t)) => Gist (N t) where
  gist = gist . rep; frip = obj . frip
-}


unD :: RM m (D a) -> a
unD (D x) = x

unM :: RM m (M i c) -> RM m c
unM (M x) = x

unR :: RM m (R t) -> Med m t
unR (R x) = x
deriving instance Eq (Med m t) => Eq (RM m (R t))
deriving instance Show (Med m t) => Show (RM m (R t))

instance Eq (RM m V) where _ == _ = True -- undefined?
instance Show (RM m V) where show _ = "<void>"
void :: String -> RM m V
void n = error $ "GenericR.void: " ++ n
absurd :: String -> RM m V -> a
absurd n = error $ "GenericR.absurd: " ++ n

unF (F x) = x
unFF (FF x) = x
deriving instance Eq (ff (RM m c) (RM m d)) => Eq (RM m (FF ff c d))
deriving instance Show (ff (RM m c) (RM m d)) => Show (RM m (FF ff c d))





concat `fmap` mapM derive [''RM]