{-# 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 @HasTagRepU tag c@ if @t@ is a 'DT' and there exists a @t@
-- constructor satisfying @'TagRepIs' tag c@.
data HasTagRepU tag c t where
  HasTagRepU :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) ->
                HasTagRepU tag c t
instance (DT t, DCs t ::: Exists (DCOf t :&& TagRepIs tag c)
         ) => t ::: HasTagRepU tag c where inhabits = HasTagRepU inhabits

-- | Given @HasTagRepU tag c t@, a trivially-mediated @c@ value can be embedded into
-- @t@.
hasTagRepU :: HasTagRepU tag c t -> RMI c -> t
hasTagRepU (HasTagRepU 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 HasTagRepImageU fn dc = HasTagRepU (Tag dc) (CApp fn (Rep dc))

-- | A constructor type @dc@ inhabits @ImageHasTagRepU 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 ImageInDTU t fn dc where
  ImageInDTU :: (Generic dc, Rep dc ::: Domain (CMap fn IdM)
                ) => HasTagRepImageU (fn IdM) dc t -> ImageInDTU t fn dc
instance (Generic dc, Rep dc ::: Domain (CMap fn IdM), t ::: HasTagRepImageU (fn IdM) dc
         ) => dc ::: ImageInDTU t fn where
  inhabits = ImageInDTU inhabits

-- | Given @ImageInDTU t fn dc@, a trivially-mediated @dc@ value can be
-- embedded into @t@.
imageInDTU :: (forall t. fn IdM t) -> ImageInDTU t fn dc -> RMNI dc -> t
imageInDTU fn (ImageInDTU d) = hasTagRepU 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)
                 ) => HasTagRepImageU (fn IdM) dc t -> ImageInDTDA t fn dc
instance (Generic dc, Rep dc ::: DomainA (CMap fn IdM), t ::: HasTagRepImageU (fn IdM) dc
         ) => dc ::: ImageInDTDA t fn where
  inhabits = ImageInDTDA inhabits

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