{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleContexts,
  MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, DataKinds #-}

{- |

Module      :  Data.Yoko.View
Copyright   :  (c) The University of Kansas 2012
License     :  BSD3

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

The @yoko@ generic view.

-}

module Data.Yoko.View
  (-- * Reflection
   -- ** Fields types
   Tag, Codomain, DC(..),
   -- ** Disbanded data types
   DCs, DT(..)
  ) where

import Data.Yoko.Representation
import Data.Yoko.TypeSums (Embed, Partition, (:-:))
import Data.Yoko.Each

import Type.Digits (Digit)



-- | @Tag@ returns a simulated type-level string that is the name of the
-- constructor that the @dc@ fields type represents.
type family Tag dc :: Digit

-- | @Codomain@ is the data type that contains the constructor that the fields
-- type @dc@ represents.  It can also be applied to sums of fields types, in
-- which case it just uses the left-most.
type family Codomain dc
type instance Codomain (N dc) = Codomain dc
type instance Codomain (l :+: r) = Codomain l

-- | Any fields type can be further represented as a product-of-fields and can
-- be injected back into the original data type.
class (Generic dc, DT (Codomain dc)) => DC dc where rejoin :: dc -> Codomain dc

-- | The @DCs@ of a data type is sum of all of its fields types.
type family DCs t
-- | @DT@ disbands a data type if all of its fields types have @DC@ instances.
class Each IsDCOf (DCs t) => DT t where disband :: t -> DCs t

class (Partition (DCs (Codomain dc)) (N dc) (DCs (Codomain dc) :-: N dc),
       Embed (N dc) (DCs (Codomain dc))) => IsDCOf dc
instance (Partition (DCs (Codomain dc)) (N dc) (DCs (Codomain dc) :-: N dc),
          Embed (N dc) (DCs (Codomain dc))) => IsDCOf dc