{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE KindSignatures        #-}
{-# LANGUAGE EmptyDataDecls        #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types            #-}

-----------------------------------------------------------------------------
-- |
-- Module      :  Generics.Regular.Base
-- Copyright   :  (c) 2008 Universiteit Utrecht
-- License     :  BSD3
--
-- Maintainer  :  generics@haskell.org
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Summary: Types for structural representation.
-----------------------------------------------------------------------------

module Generics.Regular.Base {- (

    -- * Functorial structural representation types.
    K(..),
    I(..),
    E(..),
    U(..),
    (:+:)(..),
    (:*:)(..),
    (:.:)(..),

    -- * Fixed-point type.
    Fix (..),

    -- * Type class capturing the structural representation of a type and the corresponding embedding-projection pairs.
    Regular (..), PF,
    
    Regular1 (..), PF1,
    
    dft_fmap
    
  ) -} where


-----------------------------------------------------------------------------
-- Functorial structural representation types.
-----------------------------------------------------------------------------

-- | Structure type for constant values.
data K a       (es :: * -> *) r = K { unK :: a }

-- | Structure type for recursive values.
data I         (es :: * -> *) r = I { unI :: r }

-- | Structure type for parameters.
data E e       (es :: * -> *) r = E { unE :: es e }

-- | Structure type for empty constructors.
data U         (es :: * -> *) r = U

-- | Structure type for alternatives in a type.
data (f :+: g) (es :: * -> *) r = L (f es r) | R (g es r)

-- | Structure type for fields of a constructor.
data (f :*: g) (es :: * -> *) r = f es r :*: g es r

infixr 6 :+:
infixr 7 :*:

-----------------------------------------------------------------------------
-- Fixed-point type.
-----------------------------------------------------------------------------

-- | The well-known fixed-point type.
newtype Fix f = In (f (Fix f))


-----------------------------------------------------------------------------
-- Type class capturing the structural representation of a type and the
-- corresponding embedding-projection pairs.
-----------------------------------------------------------------------------

-- | The type class @Regular@ captures the structural representation of a 
-- type and the corresponding embedding-projection pairs.
--
-- To be able to use the rewriting functions, the user is required to provide
-- an instance of this type class.
type family PF a :: (* -> *) -> * -> *
type family Es a :: * -> *

class Regular a where
  from      :: a -> PF a (Es a) a
  to        :: PF a (Es a) a -> a


type family PF1 (f :: (* -> *) -> * -> *) :: (* -> *) -> * -> *
class Regular1 (f :: (* -> *) -> * -> *) where
  from1      :: f es a -> PF1 f es a
  to1        :: PF1 f es a -> f es a


data Zero
data Succ a

infixr 8 :|:

data Nil a = Nil { magic :: forall b. b }
data (t :|: ts) :: * -> * where
  Z :: t     -> (t :|: ts) Zero
  S :: ts n  -> (t :|: ts) (Succ n)

data NatPrf :: * -> * where
  PZ :: NatPrf Zero
  PS :: NatPrf n -> NatPrf (Succ n)

class El prf ix where
  proof :: prf ix

instance El NatPrf Zero where
  proof = PZ

instance El NatPrf n => El NatPrf (Succ n) where
  proof = PS proof

-----------------------------------------------------------------------------
-- Functorial map function.
-----------------------------------------------------------------------------

instance Functor (I es) where
  fmap f (I r) = I (f r)

instance Functor (E e es) where
  fmap _ (E e) = E e

instance Functor (K a es) where
  fmap _ (K a) = K a

instance Functor (U es) where
  fmap _ U = U

instance (Functor (f es), Functor (g es)) => Functor ((f :+: g) es) where
  fmap f (L x) = L (fmap f x)
  fmap f (R y) = R (fmap f y)

instance (Functor (f es), Functor (g es)) => Functor ((f :*: g) es) where
  fmap f (x :*: y) = fmap f x :*: fmap f y


dft_fmap :: (Regular1 f, Functor (PF1 f es)) => (a -> b) -> f es a -> f es b
dft_fmap f = to1 . fmap f . from1