{-# LANGUAGE TypeOperators, GADTs, FlexibleInstances, MultiParamTypeClasses,
  FlexibleContexts, UndecidableInstances, Rank2Types #-}

{- |

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

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

Various universes determined by a data constructor type's suitability to be
embedded in a data type.

-}
module Data.Yoko.InDT where

import Type.Yoko

import Data.Yoko.Generic
import Data.Yoko.Reflect



-- | A type @t@ inhabits @HasTagRepDCD tag c@ if @t@ is a 'DT' and there exists a @t@
-- constructor satisfying @'TagRepIs' tag c@.
data HasTagRepDCD tag c t where
  HasTagRepDCD :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) ->
           HasTagRepDCD tag c t
instance (DT t, DCs t ::: Exists (DCOf t :&& TagRepIs tag c)
         ) => t ::: HasTagRepDCD tag c where inhabits = HasTagRepDCD inhabits

-- | Given @HasTagRepDCD tag c t@, a trivially-mediated @c@ value can be embedded into
-- @t@.
hasTagRepDCD :: HasTagRepDCD tag c t -> RMI c -> t
hasTagRepDCD (HasTagRepDCD d) = w d where
  w :: Exists (DCOf t :&& TagRepIs tag c) dcs -> RMI c -> t
  w (Here (x@(DCOf _) :&& TagRepIs)) = fr_DCOf x . obj
  w (OnLeft u) = w u; w (OnRight u) = w u





-- | Often times, we're interested in the universe of types accomodating a data
-- constructor's image under some type-function.
type HasTagRepDCImageD fn dc = HasTagRepDCD (Tag dc) (CApp fn (Rep dc))

-- | A constructor type @dc@ inhabits @ImageHasTagRepDCD t fn@ if
--
-- 1. @fn@ can be mapped across the recursive occurrences in @dc@, and
--
-- 2. @t@ has a constructor isomorphic to the @fn@-image of @dc@ 
data ImageInDTD t fn dc where
  ImageInDTD :: (Generic dc, Rep dc ::: Domain (CMap fn IdM)
                ) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTD t fn dc
instance (Generic dc, Rep dc ::: Domain (CMap fn IdM), t ::: HasTagRepDCImageD (fn IdM) dc
         ) => dc ::: ImageInDTD t fn where
  inhabits = ImageInDTD inhabits

-- | Given @ImageInDTD t fn dc@, a trivially-mediated @dc@ value can be
-- embedded into @t@.
imageInDTD :: (forall t. fn IdM t) -> ImageInDTD t fn dc -> RMNI dc -> t
imageInDTD fn (ImageInDTD d) = hasTagRepDCD d . apply (CMap fn) . rep

-- | Same as @ImageInDTD@, but uses an implicitly applicative function.
data ImageInDTDA t fn dc where
  ImageInDTDA :: (Generic dc, Rep dc ::: DomainA (CMap fn IdM)
                 ) => HasTagRepDCImageD (fn IdM) dc t -> ImageInDTDA t fn dc
instance (Generic dc, Rep dc ::: DomainA (CMap fn IdM), t ::: HasTagRepDCImageD (fn IdM) dc
         ) => dc ::: ImageInDTDA t fn where
  inhabits = ImageInDTDA inhabits

imageInDTAD :: Functor (Idiom (fn IdM)) =>
               (forall t. fn IdM t) -> ImageInDTDA t fn dc -> RMNI dc -> Idiom (fn IdM) t
imageInDTAD fn (ImageInDTDA d) = fmap (hasTagRepDCD d) . applyA (CMap fn) . rep