-----------------------------------------------------------------------------
-- |
-- 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 at the value level, including
-- representation of recursive types as fixpoints of functors.
--
-----------------------------------------------------------------------------

module Data.Type where

import Prelude hiding (Functor(..))
import Data.Monoid hiding (Any)
import Data.Char
import Data.List

import {-# SOURCE #-} Data.Pf
import Generics.Pointless.Combinators
import Generics.Pointless.Functors hiding (rep)
import Generics.Pointless.Lenses
import Generics.Pointless.Lenses.Examples.Examples

-- * Representation of types

data Type a where

    -- Internal representations
    Var     :: String -> Type a
    Any     :: Type 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)
    
    -- Built-in
    List    :: Type a -> Type [a]
    
    -- Recursive
    Data    :: (Mu a,Functor (PF a)) => String -> Fctr (PF a) -> Type a
    NewData :: Functor f => String -> Fctr f -> Type (Fix f)
    
    Pf      :: Type a -> Type (Pf a)
    Dynamic :: Type Dynamic
    
    -- Types for SYB generic programming
    TP      :: Type T
    TU      :: Type a -> Type (Q a)
    TypeRep  :: Type (Type a)
    FctrRep  :: Type (Fctr f)

isData :: Type a -> Bool
isData (Data _ _) = True
isData (NewData _ _) = True
isData _ = False

isAtt :: Type a -> Bool
isAtt (dataName -> Just s) = isPrefixOf "@" s
isAtt _ = False

isOne :: Type a -> Bool
isOne One = True
isOne _ = False

isBasic :: Type a -> Bool
isBasic (List Char) = True
isBasic (Data "Nat" _) = True
isBasic Int = True
isBasic Bool = True
isBasic _ = False

-- | Selects the name and functor of a non-based type
dataNameFctr :: Type a -> Maybe (String,Fctr (PF a))
dataNameFctr a = do
    s <- dataName a
    f <- dataFctr a
    return (s,f)

refname :: String -> String
refname s = aux $ span (/= '\'') s
	where aux (x,[]) = x
	      aux (x,'\'':y) = x ++ y

nodename  :: String -> String
nodename = takeWhile (/= '\'')

-- | Checks if two name strings are equal modulo an arbitrary sufix
sameName :: String -> String -> Bool
sameName n n' = map toLower (takeWhile (/= '\'') n) == map toLower (takeWhile (/= '\'') n')

-- | Selects the name of a non-based type
dataName  :: Type a -> Maybe String
dataName (Data s _) = Just s
dataName (NewData s _) = Just s
dataName (List a) = Just "List"
dataName _ = Nothing

-- | Selects the functor of a non-base type
dataFctr :: Type a -> Maybe (Fctr (PF a))
dataFctr (Data _ f) = Just f
dataFctr (NewData _ f) = Just f
dataFctr (List a) = Just $ listfctr a
dataFctr a = Nothing

instance Monoid Bool where
   mempty = False
   mappend = (||)

instance Monoid One where
   mempty = _L
   mappend _ _ = _L

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

instance Monoid Nat where
   mempty = nzero
   mappend = curry (get plus_lns)

-- | A generic type encapsulator.
data Dynamic where
    Dyn :: Type a -> a -> Dynamic

-- Convert a regular type to a dynamic type.
mkDyn :: Type a -> a -> Dynamic
mkDyn a v = Dyn a v

-- Apply a generic function to a dynamically typed value.
applyDyn :: (forall a . Type a -> a -> b) -> Dynamic -> b
applyDyn f (Dyn ta a) = f ta a

data DynType where
    DynT :: Type a -> DynType

applyDynT :: (forall a . Type a -> b) -> DynType -> b
applyDynT f (DynT t) = f t

applyDynT2 :: (forall a b . Type a -> Type b -> c) -> DynType -> DynType -> c
applyDynT2 f (DynT a) (DynT b) = f a b

data DynFctr where
    DynF :: Functor f => Fctr f -> DynFctr

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 Dynamic where
    typeof = Dynamic

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

listfctr :: Type a -> Fctr (Const One :+: Const a :*: Id)
listfctr a = K One :+!: (K a :*!: I)

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)
    AnyF :: Fctr a

rep :: Fctr f -> Type a -> Type (Rep f a)
rep I a = a
rep L a = List 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)

-- | 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 = NewData "Fix" f

annT :: Type a -> Ann a
annT (_::Type a) = ann

fixF :: Fctr f -> Ann (Fix f)
fixF (_::Fctr f) = ann

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) ++ ")"

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