-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Type
-- Copyright   :  (c) 2010 University of Minho
-- License     :  BSD3
--
-- Maintainer  :  hpacheco@di.uminho.pt
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Pointless Rewrite:
-- automatic transformation system for point-free programs
-- 
-- Type-safe representation of types and point-free expressions at the value level, including
-- representation of recursive types as fixpoints of functors.
--
-----------------------------------------------------------------------------

module Data.Type where

import Prelude hiding (Functor(..))
import Data.Monoid

import Generics.Pointless.Combinators
import Generics.Pointless.Functors
import Generics.Pointless.Lenses

-- * Representation of types

data Type a where

    -- Internal representations
    Any     :: Type a	  
    -- INTERNAL: denotes explicit recursivity, needed in some computations where F a c and c \= a 
    Id      :: Type a -> Type a

    -- Non-recursive
    Int     :: Type Int
    Bool    :: Type Bool
    Char    :: Type Char
    One     :: Type One
    Either  :: Type a -> Type b -> Type (Either a b)
    Prod    :: Type a -> Type b -> Type (a,b)
    Fun     :: Type a -> Type b -> Type (a -> b)
    Lns     :: Type a -> Type b -> Type (Lens a b)
    
    -- Recursive
    Data    :: (Mu a,Functor (PF a)) => String -> Fctr (PF a) -> Type a
    
    Pf      :: Type a -> Type (Pf a)
    Dynamic :: Type Dynamic
    
    -- Types for SYB generic programming
    TP      :: Type T
    TU      :: Type a -> Type (Q a)

instance Monoid Int where
   mempty = 0
   mappend = (+)
   mconcat = foldr (+) 0

data Dynamic where
    Dyn :: Type a -> a -> Dynamic

newtype T = T {unT :: GenericT}
type GenericT = forall a . Type a -> a -> a

newtype Q r = Q {unQ :: GenericQ r}
type GenericQ r = forall a . Type a -> a -> r

class Typeable a where
    typeof :: Type a

instance Typeable Int where
    typeof = Int
    
instance Typeable Bool where
    typeof = Bool
    
instance Typeable Char where
    typeof = Char
    
instance Typeable One where
    typeof = One

instance (Typeable a,Typeable b) => Typeable (Either a b) where
    typeof = Either typeof typeof
    
instance (Typeable a,Typeable b) => Typeable (a,b) where
    typeof = Prod typeof typeof

instance (Typeable a, Typeable b) => Typeable (a -> b) where
   typeof = Fun typeof typeof

instance (Typeable a,Typeable b) => Typeable (Lens a b) where
    typeof = Lns typeof typeof

instance Typeable a => Typeable (Pf a) where
   typeof = Pf typeof

instance Typeable T where
   typeof = TP

instance Typeable r => Typeable (Q r) where
   typeof = TU typeof

instance Typeable Nat where
    typeof = nat

instance Typeable a => Typeable [a] where
    typeof = list typeof

nat :: Type Nat
nat = Data "Nat" fctrof

list :: Type a -> Type [a]
list a = Data "List" $ K One :+!: (K a :*!: I)

unlist :: Type [a] -> Type a
unlist (Data "List" (K One :+!: (K a :*!: I))) = a

instance Typeable a => Typeable (Maybe a) where
    typeof = Data "Maybe" fctrof

instance (Fctrable f) => Typeable (Fix f) where
    typeof = fixof fctrof

-- | Functor GADT for polytypic recursive functions.
-- At the moment it does not rely on a @Typeable@ instance for constants.
data Fctr (f :: * -> *) where
    I :: Fctr Id
    K :: Type c -> Fctr (Const c)
    L :: Fctr []
    (:*!:) :: (Functor f,Functor g) => Fctr f -> Fctr g -> Fctr (f :*: g)
    (:+!:) :: (Functor f,Functor g) => Fctr f -> Fctr g -> Fctr (f :+: g)
    (:@!:) :: (Functor f,Functor g) => Fctr f -> Fctr g -> Fctr (f :@: g)

rep :: Fctr f -> Type a -> Type (Rep f a)
rep I a = a
rep (K c) a = c
rep (f:*!:g) a = Prod (rep f a) (rep g a)
rep (f:+!:g) a = Either (rep f a) (rep g a)
rep (f:@!:g) a = rep f (rep g a)
rep L a = list a

-- | Class of representable functors.
class (Functor f) => Fctrable (f :: * -> *) where
    fctrof :: Fctr f
instance Fctrable Id where
    fctrof = I
instance Typeable c => Fctrable (Const c) where
    fctrof = K typeof
instance Fctrable [] where
    fctrof = L
instance (Functor f,Fctrable f,Functor g,Fctrable g) => Fctrable (f :*: g) where
    fctrof = (:*!:) fctrof fctrof
instance (Functor f,Fctrable f,Functor g,Fctrable g) => Fctrable (f :+: g) where
    fctrof = (:+!:) fctrof fctrof
instance (Functor f,Fctrable f,Functor g,Fctrable g) => Fctrable (f :@: g) where
    fctrof = (:@!:) fctrof fctrof

fixof :: (Functor f) => Fctr f -> Type (Fix f)
fixof f = Data "" f

fixF :: Fctr f -> Fix f
fixF (_::Fctr f) = (_L :: Fix f)

fctrofF :: Fctrable f => Fix f -> Fctr f
fctrofF (_::Fix f) = fctrof :: Fctr f

showL :: [String] -> String
showL [x] = x
showL xs = "(" ++ init (Prelude.foldr (\a b -> a ++ " " ++ b) "" xs) ++ ")"

-- * Representation of point-free expressions

data Pf a where
    
    -- Variables and pointwise expressions
    VAR           :: String -> Pf a
    FUN           :: String -> (a -> b) -> Pf (a -> b)
    
    -- Internal combinators
    HOLE          :: Pf a
    TOP           :: Pf a
    CONV          :: Either One One -> Pf (a -> b) -> Pf (b -> a)
    CONV_LNS      :: Either One One -> Pf (Lens c a) -> Pf (Lens a c)
    LNS           :: String -> Lens c a -> Pf (Lens c a)
    COMPF         :: Functor f => Fctr f -> Type a -> Pf (Rep f a -> b) -> Pf (c -> Rep f a) -> Pf (c -> b)
    COMPF_LNS     :: Functor f => Fctr f -> Type a -> Pf (Lens (Rep f a) b) -> Pf (Lens c (Rep f a)) -> Pf (Lens c b)
    -- Internal encapsulators
    PROTECT       :: Pf (a -> b) -> Pf (a -> b)
    PROTECT_LNS   :: Pf (Lens a b) -> Pf (Lens a b)
    
    -- Non-recursive point-free combinators
    PNT           :: a -> Pf (One -> a)
    BANG          :: Pf (a -> One)
    COMP          :: Type b -> Pf (b -> c) -> Pf (a -> b) -> Pf (a -> c)
    FST           :: Pf ((a,b) -> a)
    SND           :: Pf ((a,b) -> b)
    SPLIT         :: Pf (a -> b) -> Pf (a -> c) -> Pf (a -> (b,c))
    PROD          :: Pf (a -> c) -> Pf (b -> d) -> Pf ((a,b) -> (c,d))
    INL           :: Pf (a -> Either a b)
    INR           :: Pf (b -> Either a b)
    EITHER        :: Pf (a -> c) -> Pf (b -> c) -> Pf (Either a b -> c)
    SUM           :: Pf (a -> c) -> Pf (b -> d) -> Pf (Either a b -> Either c d)
   
    -- Monoids
    ZERO          :: Monoid b => Pf (a -> b)
    PLUS          :: Monoid a => Pf ((a,a) -> a)
   
    -- Isomorphic point-free combinators
    ID            :: Pf (c -> c)
    SWAP          :: Pf ((a,b) -> (b,a))
    COSWAP        :: Pf ((Either a b) -> (Either b a))
    DISTL         :: Pf ((Either a b,c) -> (Either (a,c) (b,c)))
    UNDISTL       :: Pf ((Either (a,c) (b,c)) -> (Either a b, c))
    DISTR         :: Pf ((c, Either a b) -> (Either (c,a) (c,b)))
    UNDISTR       :: Pf ((Either (c,a) (c,b)) -> (c,Either a b))
    ASSOCL        :: Pf ((a,(b,c)) -> ((a,b),c))
    ASSOCR        :: Pf (((a,b),c) -> (a,(b,c)))
    COASSOCL      :: Pf ((Either a (Either b c)) -> (Either (Either a b) c))
    COASSOCR      :: Pf ((Either (Either a b) c) -> (Either a (Either b c)))

    -- Recursive point-free combinators
    INN           :: (Mu a,Functor (PF a)) => Pf (F a a -> a)
    OUT           :: (Mu a,Functor (PF a)) => Pf (a -> F a a)
    FMAP          :: Functor f => Fctr f -> Type (c -> a) -> Pf (c -> a) -> Pf (Rep f c -> Rep f a)
    FZIP          :: Functor f => Fctr f -> Type (a -> c) -> Pf (a -> c) -> Pf ((Rep f a,Rep f c) -> Rep f (a,c))
    ANA           :: (Mu b,Functor (PF b)) => Pf (a -> (F b a)) -> Pf (a -> b)
    CATA          :: (Mu a,Functor (PF a)) => Pf (F a b -> b) -> Pf (a -> b)
    PARA          :: (Mu a,Functor (PF a)) => Pf (F a (c,a) -> c) -> Pf (a -> c)
    
    -- Lens Point-free functions
    GET           :: Pf (Lens c a) -> Pf (c -> a)
    PUT           :: Pf (Lens c a) -> Pf ((a,c) -> c)
    CREATE        :: Pf (Lens c a) -> Pf (a -> c)
    
    -- Non-recursive lenses
    COMP_LNS      :: Type b -> Pf (Lens b a) -> Pf (Lens c b) -> Pf (Lens c a)
    FST_LNS       :: Pf (a -> b) -> Pf (Lens (a,b) a)
    SND_LNS       :: Pf (b -> a) -> Pf (Lens (a,b) b)
    PROD_LNS      :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (c,d) (a,b))
    EITHER_LNS    :: Pf (c -> Either One One) -> Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)
    SUM_LNS       :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))
    SUMW_LNS      :: Pf ((a,d) -> c) -> Pf ((b,c) -> d) -> Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))
    BANG_LNS      :: Pf (One -> c) -> Pf (Lens c One)
    BANGL_LNS     :: Pf (Lens c (One,c))
    BANGR_LNS     :: Pf (Lens c (c,One))
    
    -- Non-recursive isomorphisms
    ID_LNS        :: Pf (Lens c c)
    SWAP_LNS      :: Pf (Lens (a,b) (b,a))
    COSWAP_LNS    :: Pf (Lens (Either a b) (Either b a))
    DISTL_LNS     :: Pf (Lens (Either a b,c) (Either (a,c) (b,c)))
    UNDISTL_LNS   :: Pf (Lens (Either (a,c) (b,c)) (Either a b,c))
    DISTR_LNS     :: Pf (Lens (c, Either a b) (Either (c,a) (c,b)))
    UNDISTR_LNS   :: Pf (Lens (Either (c,a) (c,b)) (c,Either a b))
    ASSOCL_LNS    :: Pf (Lens (a,(b,c)) ((a,b),c))
    ASSOCR_LNS    :: Pf (Lens ((a,b),c) (a,(b,c)))
    COASSOCL_LNS  :: Pf (Lens (Either a (Either b c)) (Either (Either a b) c))
    COASSOCR_LNS  :: Pf (Lens (Either (Either a b) c) (Either a (Either b c)))
    
    -- Recursive lenses
    INN_LNS       :: (Mu a,Functor (PF a)) => Pf (Lens (F a a) a)
    OUT_LNS       :: (Mu a,Functor (PF a)) => Pf (Lens a (F a a))
    FMAP_LNS      :: Functor f => Fctr f -> Type (c -> a) -> Pf (Lens c a) -> Pf (Lens (Rep f c) (Rep f a))
    ANA_LNS       :: (Mu b,Functor (PF b)) => Pf (Lens a (F b a)) -> Pf (Lens a b)
    CATA_LNS      :: (Mu a,Functor (PF a)) => Pf ((Lens (F a b) b)) -> Pf (Lens a b)
    
    -- User-defined lenses
    MAP_LNS           :: Pf (Lens a b) -> Pf (Lens [a] [b])
    LENGTH_LNS        :: a -> Pf (Lens [a] Nat)
    FILTER_LEFT_LNS   :: Pf (Lens [Either a b] [a])
    FILTER_RIGHT_LNS  :: Pf (Lens [Either a b] [b])
    CAT_LNS           :: Pf (Lens ([a],[a]) [a])
    CONCAT_LNS        :: Pf (Lens [[a]] [a])
    SUML_LNS          :: Pf (Lens [Nat] Nat)
    PLUS_LNS          :: Pf (Lens (Nat,Nat) Nat)

    -- Type-preserving strategy combinators
    APPLY             :: Type a -> Pf T -> Pf (a -> a)
    MKT               :: Type a -> Pf (a -> a) -> Pf T
    NOP               :: Pf T
    SEQ               :: Pf T -> Pf T -> Pf T
    EXTT              :: Pf T -> Type b -> Pf (b -> b) -> Pf T
    ALL               :: Pf T -> Pf T
    EVERYWHERE        :: Pf T -> Pf T		-- bottom-up (catamorphism)
    EVERYWHERE'       :: Pf T -> Pf T		-- top-down (anamorphism)
    -- Type-unifying strategy combinators
    APPLYQ            :: Type a -> Pf (Q r) -> Pf (a -> r)
    MKQ               :: Monoid r => Type a -> Pf (a -> r) -> Pf (Q r)
    EMPTYQ            :: Monoid r => Pf (Q r)
    UNION             :: Monoid r => Pf (Q r) -> Pf (Q r) -> Pf (Q r)
    EXTQ              :: Pf (Q r) -> Type a -> Pf (a -> r) -> Pf (Q r)
    GMAPQ             :: Monoid r => Pf (Q r) -> Pf (Q r)
    EVERYTHING        :: Monoid r => Pf (Q r) -> Pf (Q r) -- bottom-up, right-to-left (paramorphism)

infix 5  ?=
(?=) :: Type a -> Pf (a -> Either One One) -> Pf (a -> Either a a)
(?=) a p = COMP (Either (Prod One a) (Prod One a)) (SND -|-= SND) $ COMP (Prod (Either One One) a) DISTL $ p /\= ID

infixr 9 .=
(.=) :: Typeable b => Pf (b -> a) -> Pf (c -> b) -> Pf (c -> a)
(.=) f g = COMP typeof f g

infix 6  /\=
(/\=) :: Pf (a -> b) -> Pf (a -> c) -> Pf (a -> (b,c))
(/\=) f g = SPLIT f g

infix 7 ><=
(><=) :: Pf (c -> a) -> Pf (d -> b) -> Pf ((c,d) -> (a,b))
(><=) f g = PROD f g

infix 4 \/=
(\/=) :: Pf (b -> a) -> Pf (c -> a) -> Pf (Either b c -> a)
(\/=) f g = EITHER f g

infix 5 -|-=
(-|-=) :: Pf (c -> a) -> Pf (d -> b) -> Pf ((Either c d) -> (Either a b))
(-|-=) f g = SUM f g

distp_pf :: Pf (((c,d),(a,b)) -> ((c,a),(d,b)))
distp_pf = FST ><= FST /\= SND ><= SND

dists_pf :: Type (Either a b,Either c d) -> Pf ((Either a b,Either c d) -> (Either (Either (a,c) (a,d)) (Either (b,c) (b,d))))
dists_pf (Prod (Either a b) (Either c d)) = COMP t (DISTR -|-= DISTR) DISTL
    where t = Either (Prod a (Either c d)) (Prod b (Either c d))

infixr 9 .<<
(.<<) :: Typeable b => Pf (Lens b a) -> Pf (Lens c b) -> Pf (Lens c a)
(.<<) f g = COMP_LNS typeof f g

infix 7 ><<<
(><<<) :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (c,d) (a,b))
(><<<) f g = PROD_LNS f g

infix 5 -|-<<
(-|-<<) :: Pf (Lens c a) -> Pf (Lens d b) -> Pf (Lens (Either c d) (Either a b))
(-|-<<) f g = SUM_LNS f g

infix 4 \/<<
(\/<<) :: Pf (c -> Either One One) -> Pf (Lens a c) -> Pf (Lens b c) -> Pf (Lens (Either a b) c)
(\/<<) x f g = EITHER_LNS x f g

dists_lns :: Type (Either a b,Either c d) -> Pf (Lens (Either a b,Either c d) (Either (Either (a,c) (a,d)) (Either (b,c) (b,d))))
dists_lns (Prod (Either a b) (Either c d)) = COMP_LNS t (DISTR_LNS -|-<< DISTR_LNS) DISTL_LNS
    where t = Either (Prod a (Either c d)) (Prod b (Either c d))

fmap_Lns :: (Functor f,Typeable (c -> a)) => Fctr f -> Pf (Lens c a) -> Pf (Lens (Rep f c) (Rep f a))
fmap_Lns fctr f = FMAP_LNS fctr typeof f