{-# LANGUAGE TypeFamilies, FlexibleContexts, MultiParamTypeClasses,
  FlexibleInstances, UndecidableInstances, QuasiQuotes, ScopedTypeVariables,
  Rank2Types #-}

{- |

Module      :  Type.Yoko.TFunA
Copyright   :  (c) The University of Kansas 2011
License     :  BSD3

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

The type-level functionality of "Type.Yoko.FunA" functions.

-}

module Type.Yoko.TFunA (TApp, CMap(..), CApp) where

import Type.Yoko.TSTSS

import Type.Yoko.Fun
import Type.Yoko.FunA

import Type.Yoko.Type
import Type.Yoko.Universe

import Data.Yoko.CoreTypes
import Data.Yoko.Generic

import Control.Applicative (Applicative(pure))
import Data.Traversable (Traversable(traverse))




-- | The @TApp@ type family encodes the type-level functionality of
-- "Type.Yoko.Fun" functions.
type family TApp (fn :: * -> *) t




-- | @CMap fn m c@ applies @fn@ to all recursive occurrences (i.e. 'R') in a
-- "Data.Yoko.Core" type @c@ that's mediated by @m@. The domain ('Dom') is @RM
-- m c@ and the range ('Rng') is @RM m (CApp (fn m) c)@. The 'Idiom' is @Idiom
-- (fn m)@.
newtype CMap fn m c = CMap (forall t. fn m t)

type instance Dom (CMap fn m) c = RM m c
type instance Rng (CMap fn m) c = RM m (CApp (fn m) c)
type instance Idiom (CMap fn m) = Idiom (fn m)

-- | @CApp fn c@ applies the type-function @fn@ to all recursive occurrences
-- (i.e. 'R') in the "Data.Yoko.Core" type @c@.
type family CApp (fn :: * -> *) c
type instance CApp fn (D a) = D a
type instance CApp fn (F f c) = F f (CApp fn c)
type instance CApp fn (FF ff c d) = FF ff (CApp fn c) (CApp fn d)
type instance CApp fn (M i c) = M i (CApp fn c)
type instance CApp fn (R t) = R (TApp fn t)
type instance CApp fn U = U
type instance CApp fn V = V

pureDomain :: (Dom fn t ~ Rng fn t) => Domain fn t
pureDomain = AppBy $ \_ -> id

instance D a ::: Domain (CMap fn m) where inhabits = pureDomain
instance (c ::: Domain (CMap fn m), Traversable f
         ) => F f c ::: Domain (CMap fn m) where
  inhabits = AppBy $ \(CMap fn) -> F . fmap (apply (CMap fn)) . unF
instance (c ::: Domain (CMap fn m), d ::: Domain (CMap fn m),
          FunctorTSTSS ff
         ) => FF ff c d ::: Domain (CMap fn m) where
  inhabits = AppBy $ \(CMap fn) -> FF .
               fmapTSTSS (apply (CMap fn)) (apply (CMap fn)) . unFF
instance (c ::: Domain (CMap fn m)) => M i c ::: Domain (CMap fn m) where
  inhabits = AppBy $ \(CMap fn) -> M . apply (CMap fn) . unM
instance (t ::: Domain (fn m), Wrapper (fn m),
          Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med m (TApp (fn m) t)
         ) => R t ::: Domain (CMap fn m) where
  inhabits = AppBy $ \(CMap fn) -> R . apply (fn :: fn m t) . unR
instance U ::: Domain (CMap fn m) where inhabits = pureDomain
instance V ::: Domain (CMap fn m) where inhabits = pureDomain

pureDomainA :: (Dom fn t ~ Rng fn t, Applicative (Idiom fn)) => DomainA fn t
pureDomainA = AppABy $ \_ -> pure

instance Applicative (Idiom (fn m)) => D a ::: DomainA (CMap fn m) where
  inhabits = pureDomainA
instance (c ::: DomainA (CMap fn m), Applicative (Idiom (fn m)),
          Traversable f) => F f c ::: DomainA (CMap fn m) where
  inhabits = AppABy $ \(CMap fn) -> fmap F . traverse (applyA (CMap fn)) . unF
instance (c ::: DomainA (CMap fn m), d ::: DomainA (CMap fn m),
          Applicative (Idiom (fn m)), TraversableTSTSS ff
         ) => FF ff c d ::: DomainA (CMap fn m) where
  inhabits = AppABy $ \(CMap fn) -> fmap FF .
               traverseTSTSS (applyA (CMap fn)) (applyA (CMap fn)) . unFF
instance (c ::: DomainA (CMap fn m), Functor (Idiom (fn m))
         ) => M i c ::: DomainA (CMap fn m) where
  inhabits = AppABy $ \(CMap fn) -> fmap M . applyA (CMap fn) . unM
instance (t ::: DomainA (fn m), Functor (Idiom (fn m)), Wrapper (fn m),
          Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med m (TApp (fn m) t)
         ) => R t ::: DomainA (CMap fn m) where
  inhabits = AppABy $ \(CMap fn) -> fmap R . applyA (fn :: fn m t) . unR
instance Applicative (Idiom (fn m)) => U ::: DomainA (CMap fn m) where
  inhabits = pureDomainA
instance Applicative (Idiom (fn m)) => V ::: DomainA (CMap fn m) where
  inhabits = pureDomainA