-----------------------------------------------------------------------------
-- |
-- Module      :  Data.Eval
-- 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
-- 
-- Evaluation of point-free representations.
--
-----------------------------------------------------------------------------

module Data.Eval where
    
import Prelude hiding (Functor(..))
import Data.Type
import Data.Pf
import Data.Spine
import Data.Equal

import Data.Monoid
import Data.Char
import Data.List

import Generics.Pointless.Combinators
import Generics.Pointless.RecursionPatterns
import Generics.Pointless.Functors hiding (rep)
import qualified Generics.Pointless.Fctrable as F
import Generics.Pointless.Lenses
import Generics.Pointless.Lenses.Combinators
import Generics.Pointless.Lenses.RecursionPatterns
import Generics.Pointless.Lenses.Examples.Examples
import Generics.Pointless.Lenses.Examples.Recs

wrap :: a -> [a]
wrap a = [a]

fctrT :: Functor f => Fctr f -> F.Fctr f
fctrT I = F.I
fctrT (K c) = F.K
fctrT L = F.L
fctrT (f :*!: g) = fctrT f F.:*!: fctrT g
fctrT (f :+!: g) = fctrT f F.:+!: fctrT g
fctrT (f :@!: g) = fctrT f F.:@!: fctrT g

inn_lnsF :: Mu a => Fctr f -> Lens (F a a) a
inn_lnsF f = Lens inn (out . fst) out

out_lnsF :: Mu a => Fctr f -> Lens a (F a a)
out_lnsF f = Lens out (inn . fst) inn

fmap_lnsF :: Functor f => Fctr f -> Lens c a -> Lens (Rep f c) (Rep f a)
fmap_lnsF (f::Fctr f) l = Lens get' put' create'
    where get' = fmap fix (get l)
          put' = fmap fix (put l) . fzip (fixF f) (create l)
          create' = fmap fix (create l)
          fix = fixF f

ana_lnsF :: (Mu b,Functor (PF b)) => Ann b -> Fctr (PF b) -> Lens a (F b a) -> Lens a b
ana_lnsF (b::Ann b) f l = Lens get' put' create'
    where get' = ana b (get l)
          put' = accum b  (put l) (fzip (fixF g) create' . (id >< get l))
          create' = cata b (create l)
          g = f :: Fctr (PF b)

cata_lnsF :: (Mu a,Functor (PF a)) => Ann a -> Fctr (PF a) -> (Lens (F a b) b) -> Lens a b
cata_lnsF (a::Ann a) f l = Lens get' put' create'
    where get' = cata a (get l)
          put' = ana a (fzip (fixF g) create' . (put l . (id >< fmap (fixF f) get') /\ snd) . (id >< out))
          create' = ana a (create l)
          g = f :: Fctr (PF a)

eval :: Type a -> Pf a -> a
eval _ BOT = error "_L"
eval _ TOP = error "top"
eval (Fun _ _) (FUN _ f) = f
eval (Fun _ _) (CONV _ f) = error "converse evaluation"
eval (Lns _ _) (CONV_LNS _ f) = error "converse evaluation"
eval (Lns _ _) (LNS _ l) = l
eval (Fun a b) (PROTECT f) = eval (Fun a b) f
eval (Lns a b) (PROTECT_LNS f) = eval (Lns a b) f
eval _ (VAR s) = error s

eval (Fun a b) (PNT v) = const v
eval (Fun _ _) BANG = bang
eval (Fun a c) (COMP b f g) = eval (Fun b c) f . eval (Fun a b) g
eval (Fun _ _) FST = fst
eval (Fun _ _) SND = snd
eval (Fun a (Prod b c)) (SPLIT f g) = eval (Fun a b) f /\ eval (Fun a c) g
eval (Fun (Prod a b) (Prod c d)) (PROD f g) = eval (Fun a c) f >< eval (Fun b d) g
eval (Fun _ _) INL = inl
eval (Fun _ _) INR = inr
eval (Fun (Either a b) c) (EITHER f g) = eval (Fun a c) f \/ eval (Fun b c) g
eval (Fun (Either a b) (Either c d)) (SUM f g) = eval (Fun a c) f -|- eval (Fun b d) g

eval _ (MKDYN a) = Dyn a
eval _ (UNDYN a) = unDyn a
eval (Fun b _) (CAST a) = cast a b

eval _ ZERO = const mempty
eval _ PLUS = uncurry mappend
eval _ FOLD = mconcat

eval (Fun _ _) ID = id
eval (Fun _ _) SWAP = swap
eval (Fun _ _) COSWAP = coswap
eval (Fun _ _) DISTL = distl
eval (Fun _ _) UNDISTL = undistl
eval (Fun _ _) DISTR = distr
eval (Fun _ _) UNDISTR = undistr
eval (Fun _ _) ASSOCL = assocl
eval (Fun _ _) ASSOCR = assocr
eval (Fun _ _) COASSOCL = coassocl
eval (Fun _ _) COASSOCR = coassocr

eval (Fun _ _) INN = inn
eval (Fun _ _) OUT = out
eval (Fun _ _) (FMAP fctr (Fun c a) f) = fmap (fixF fctr) (eval (Fun c a) f)
eval (Fun _ _) (FZIP fctr t f) = fzip (fixF fctr) $ eval t f
eval (Fun a b@(dataFctr -> Just fctr)) (ANA f) = ana _L (eval (Fun a (rep fctr a)) f)
eval (Fun a@(dataFctr -> Just fctr) b) (CATA f) = cata _L (eval (Fun (rep fctr b) b) f)
eval (Fun a@(dataFctr -> Just fctr) b) (PARA f) = para _L (eval (Fun (rep fctr (Prod b a)) b) f)
eval (Fun a (List b)) (ANA f) = ana _L (eval (Fun a (rep (listfctr b) a)) f)
eval (Fun (List a) b) (CATA f) = cata _L (eval (Fun (rep (listfctr a) b) b) f)
eval (Fun la@(List a) b) (PARA f) = para _L (eval (Fun (rep (listfctr a) (Prod b la)) b) f)

eval (Fun (List a) (List b)) (MAP f) = map (eval (Fun a b) f)
eval (Fun _ _) LHEAD = \l -> if (null l) then [] else [head l]
eval (Fun _ _) LTAIL = \l -> if (null l) then [] else tail l
eval (Fun _ _) WRAP = wrap
eval (Fun _ _) LENGTH = get (length_lns _L)
eval (Fun _ _) ONE = const (Nat 1)

eval (Fun c a) (GET l) = get (eval (Lns c a) l)
eval (Fun (Prod a c) _) (PUT l) = put (eval (Lns c a) l)
eval (Fun a c) (CREATE l) = create (eval (Lns c a) l)

eval (Lns c a) (COMP_LNS b f g) = eval (Lns b a) f .< eval (Lns c b) g
eval (Lns (Prod a b) _) (FST_LNS f) = fst_lns $ eval (Fun a b) f
eval (Lns (Prod a b) _) (SND_LNS f) = snd_lns $ eval (Fun b a) f
eval (Lns (Prod a b) (Prod c d)) (PROD_LNS f g) = eval (Lns a c) f ><< eval (Lns b d) g
eval (Lns (Either a b) c) (EITHER_LNS x f g) = (\/<) (eval (Fun c (Either One One)) x) (eval (Lns a c) f) (eval (Lns b c) g)
eval (Lns (Either a b) (Either c d)) (SUM_LNS f g) = eval (Lns a c) f -|-< eval (Lns b d) g
eval (Lns (Either a b) (Either c d)) (SUMW_LNS f g l1 l2) = sum_lns f' g' (eval (Lns a c) l1) (eval (Lns b d) l2)
    where f' = eval (Fun (Prod c b) a) f
          g' = eval (Fun (Prod d a) b) g
eval (Lns a One) (BANG_LNS f) = (!<) (eval (Fun One a) f)
eval (Lns c _) BANGL_LNS = (!/\<) id_lns
eval (Lns c _) BANGR_LNS = (/\!<) id_lns

eval (Lns _ _) ID_LNS = id_lns
eval (Lns _ _) SWAP_LNS = swap_lns
eval (Lns _ _) COSWAP_LNS = coswap_lns
eval (Lns _ _) DISTL_LNS = distl_lns
eval (Lns _ _) UNDISTL_LNS = undistl_lns
eval (Lns _ _) DISTR_LNS = distr_lns
eval (Lns _ _) UNDISTR_LNS = undistr_lns
eval (Lns _ _) ASSOCL_LNS = assocl_lns
eval (Lns _ _) ASSOCR_LNS = assocr_lns
eval (Lns _ _) COASSOCL_LNS = coassocl_lns
eval (Lns _ _) COASSOCR_LNS = coassocr_lns

eval (Lns _ (List a)) INN_LNS = inn_lnsF (listfctr a)
eval (Lns (List a) _) OUT_LNS = out_lnsF (listfctr a)
eval (Lns _ a@(dataFctr -> Just fctr)) INN_LNS = inn_lnsF fctr
eval (Lns a@(dataFctr -> Just fctr) _) OUT_LNS = out_lnsF fctr
eval (Lns _ _) (FMAP_LNS fctr (Fun c a) f) = fmap_lnsF fctr (eval (Lns c a) f)
eval (Lns a (List b)) (ANA_LNS f) = ana_lnsF _L (listfctr b) (eval (Lns a (rep (listfctr b) a)) f)
eval (Lns (List a) b) (CATA_LNS f) = cata_lnsF _L (listfctr a) (eval (Lns (rep (listfctr a) b) b) f)
eval (Lns a b@(dataFctr -> Just fctr)) (ANA_LNS f) = ana_lnsF _L fctr (eval (Lns a (rep fctr a)) f)
eval (Lns a@(dataFctr -> Just fctr) b) (CATA_LNS f) = cata_lnsF _L fctr (eval (Lns (rep fctr b) b) f)

eval (Lns (List a) (List b)) (MAP_LNS l1) = map_pf (eval (Lns a b) l1)
eval (Lns (List a) _) (LENGTH_LNS v) = length_lns v
eval (Lns _ _) FILTER_LEFT_LNS = filter_left_pf
eval (Lns _ _) FILTER_RIGHT_LNS = filter_right_pf
eval (Lns _ _) CAT_LNS = cat_pf
eval (Lns _ _) CONCAT_LNS = concat_pf
eval (Lns _ _) SUMN_LNS = sum_pf
eval (Lns _ _) PLUSN_LNS = plus_lns

eval p (APPLY Dynamic t) = applyDyn $ \a -> mkDyn a . eval (Fun a a) (APPLY a t)
eval p (APPLY a (ALL f)) = eval p (allT a f)
eval p (APPLY a (EVERYWHERE f)) = eval p (everywhereEval a f)
eval p (APPLY a (EVERYWHERE' f)) = eval p (everywhereEval' a f)
eval p (APPLY a (EXTT f t g)) = eval p (extT a f t g)
eval p (APPLY a (SEQ f g)) = eval p (APPLY a g) . eval p (APPLY a f)
eval p (APPLY a (MKT t f)) = eval p (mkT a t f)
eval p (APPLY a NOP) = id

eval q@(Fun _ r) (APPLYQ Dynamic f) = applyDyn $ \a -> eval (Fun a r) (APPLYQ a f)
eval q@(Fun a r)(APPLYQ _ (GMAPQ f)) = eval q (gmapQ r a f)
eval q@(Fun _ r) (APPLYQ a (EVERYTHING f)) = eval q (everythingEval a f)
eval q (APPLYQ a (EXTQ f t g)) = eval q (extQ a f t g)
eval q (APPLYQ t (UNION f g)) = eval q (APPLYQ t f) `mappend` eval q (APPLYQ t g)
eval q (APPLYQ a (MKQ t f)) = eval q (mkQ a t f)
eval q (APPLYQ a EMPTYQ) = mempty
eval (Fun _ s) (APPLYQ a (SEQQ (q :: Pf (Q r)) f)) = let r = typeof :: Type r in eval (Fun r s) f . eval (Fun a r) (APPLYQ a q)
eval _ (f :?: p) = Q (\t x -> let y = unQ (eval (TU (List Dynamic)) f) t x
		               in filter (unQ (eval (TU Bool) p) Dynamic) y)
eval (Fun _ _) NONEMPTY = not . null

eval q (APPLYQ a SELF) = if isAtt a then mempty else wrap . mkDyn a
eval q (APPLYQ a ATT) = if isAtt a then wrap . mkDyn a else mempty
eval q (APPLYQ a CHILD) = eval q $ APPLYQ a $ GMAPQ SELF
eval q (APPLYQ a ATTRIBUTE) = eval q $ APPLYQ a $ GMAPQ ATT
eval q (APPLYQ a DESCENDANT) = eval q $ APPLYQ a $ EVERYTHING CHILD
eval q (APPLYQ a DESCSELF) = eval q $ APPLYQ a $ EVERYTHING SELF
eval q (APPLYQ a@(dataName -> Just name) (NAME n)) | sameName name n = eval q (APPLYQ a SELF)
eval q (APPLYQ a@(dataName -> Just name) (NAME n)) | sameName name ("@"++n) = eval q (APPLYQ a ATT)
eval q (APPLYQ a (NAME n)) = mempty
eval (Fun t r) (APPLYQ a (f :/: g)) = mconcat . map (eval (Fun Dynamic r) (APPLYQ Dynamic g)) . eval (Fun t (List Dynamic)) (APPLYQ a f)
eval (TU (Prod a b)) (f :/\: g) = Q (\t x -> (unQ (eval (TU a) f) t x,unQ (eval (TU b) g) t x))

eval t f = error $ "eval undefined for: " ++ show t
everywhereEval t f = APPLY t (ALL (EVERYWHERE f) `SEQ` f)
everywhereEval' t f = APPLY t (f `SEQ` ALL (EVERYWHERE' f))
everythingEval t f = APPLYQ t (f `UNION` GMAPQ (EVERYTHING f))

-- ** Type-preserving specialization

allTF :: Fctr f -> Type a -> Pf T -> Pf (Rep f a -> Rep f a)
allTF I a t = APPLY a t
allTF L a t = MAP $ APPLY a t
allTF (K c) a t = APPLY c t
allTF (f :*!: g) a t = allTF f a t `PROD` allTF g a t
allTF (f :+!: g) a t = allTF f a t `SUM` allTF g a t
allTF (f :@!: g) a t = let ga = rep g a
                       in COMP (rep f ga) (allTKF f ga t) (FMAP f (Fun ga ga) (allTF g a t))

allTKF :: Fctr f -> Type a -> Pf T -> Pf (Rep f a -> Rep f a)
allTKF I a t = ID
allTKF L a t = ID
allTKF (K c) a t = APPLY c t
allTKF (f :*!: g) a t = allTKF f a t `PROD` allTKF g a t
allTKF (f :+!: g) a t = allTKF f a t `SUM` allTKF g a t
allTKF (f :@!: g) a t = let ga = rep g a
                       in COMP (rep f ga) (allTKF f ga t) (FMAP f (Fun ga ga) (allTKF g a t))

allT :: Type a -> Pf T -> Pf (a -> a)
allT a@(Data s fctr) t = allTRec a fctr t
allT a@(NewData s fctr) t = allTRec a fctr t
allT (List a) t = MAP (APPLY a t)
allT (Either a b) t = (APPLY a t) `SUM` (APPLY b t)
allT (Prod a b) t = (APPLY a t) `PROD` (APPLY b t)
--allT Dynamic 
allT a t = ID

allTRec :: (Functor (PF a),Mu a) => Type a -> Fctr (PF a) -> Pf T -> Pf (a -> a)
allTRec a fctr t = let f = rep fctr a
                       in COMP f INN $ COMP f (allTF fctr a t) OUT

-- | bottom-up (cata)
everywhereT :: Type a -> Pf T -> Pf (a -> a)
everywhereT t@(Data n fctr) g = everywhereTRec t fctr g
everywhereT t@(NewData n fctr) g = everywhereTRec t fctr g
everywhereT t g = APPLY t (ALL (EVERYWHERE g) `SEQ` g)

everywhereTRec :: (Functor (PF a),Mu a) => Type a -> Fctr (PF a) -> Pf T -> Pf (a -> a)
everywhereTRec t fctr g = let f = rep fctr t
                              in CATA $ COMP t (APPLY t g) $ COMP f INN (allTKF fctr t $ EVERYWHERE g)

-- | top-down (ana)
everywhereT' :: Type a -> Pf T -> Pf (a -> a)
everywhereT' t@(Data n fctr) g = everywhereTRec' t fctr g
everywhereT' t@(NewData n fctr) g = everywhereTRec' t fctr g
everywhereT' t g = APPLY t (g `SEQ` ALL (EVERYWHERE' g))

everywhereTRec' :: (Functor (PF a),Mu a) => Type a -> Fctr (PF a) -> Pf T -> Pf (a -> a)
everywhereTRec' t fctr g = let f = rep fctr t
                               in ANA $ COMP f (allTKF fctr t $ EVERYWHERE' g) $ COMP t OUT $ APPLY t g

mkT :: Type a -> Type x -> Pf (x -> x) -> Pf (a -> a)
mkT t t' f = case teq t t' of {Just Eq -> f; otherwise -> ID}

extT :: Type x -> Pf T -> Type a -> Pf (a -> a) -> Pf (x -> x)
extT t f x g = case teq t x of {Just Eq -> g; otherwise -> APPLY t f}

-- ** Type-unifying specialization

gmapQF :: Monoid r => Type r -> Fctr f -> Type a -> Pf (Q r) -> Pf (Rep f a -> r)
gmapQF r I a q = case teq r a of { Just Eq -> ID; otherwise -> APPLYQ a q }
gmapQF r L a q = case teq r a of { Just Eq -> FOLD; otherwise -> COMP (List r) FOLD $ MAP $ APPLYQ a q }
gmapQF r (K c) a q = APPLYQ c q
gmapQF r (f :+!: g) a q = gmapQF r f a q `EITHER` gmapQF r g a q
gmapQF r (f :*!: g) a q = COMP (Prod r r) PLUS $ gmapQF r f a q `PROD` gmapQF r g a q
gmapQF r (f :@!: g) a q = let ga = rep g a
                          in COMP (rep f r) (gmapQKF r f r q) $ FMAP f (Fun ga r) (gmapQF r g a q)

gmapQKF :: Monoid r => Type r -> Fctr f -> Type a -> Pf (Q r) -> Pf (Rep f a -> r)
gmapQKF r I a q = case teq r a of { Just Eq -> ID; otherwise -> ZERO }
gmapQKF r L a q = case teq r a of { Just Eq -> FOLD; otherwise -> ZERO }
gmapQKF r (K c) a q = APPLYQ c q
gmapQKF r (f :+!: g) a q = gmapQKF r f a q `EITHER` gmapQKF r g a q
gmapQKF r (f :*!: g) a q = COMP (Prod r r) PLUS $ gmapQKF r f a q `PROD` gmapQKF r g a q
gmapQKF r (f :@!: g) a q = let ga = rep g a
                          in COMP (rep f r) (gmapQKF r f r q) $ FMAP f (Fun ga r) (gmapQKF r g a q)

gmapQ :: (Monoid r) => Type r -> Type a -> Pf (Q r) -> Pf (a -> r)
gmapQ r t@(Data _ fctr) g = gmapQRec r t fctr g
gmapQ r t@(NewData _ fctr) g = gmapQRec r t fctr g
gmapQ r (List a) f = COMP (List r) FOLD $ MAP $ APPLYQ a f
gmapQ r (Either a b) f = (APPLYQ a f) `EITHER` (APPLYQ b f)
gmapQ r (Prod a b) f = COMP (Prod r r) PLUS $ APPLYQ a f `PROD` APPLYQ b f
gmapQ r t f = ZERO

gmapQRec :: (Functor (PF a), Mu a,Monoid r) => Type r -> Type a -> Fctr (PF a) -> Pf (Q r) -> Pf (a -> r)
gmapQRec r t fctr g = COMP (rep fctr t) (gmapQF r fctr t g) OUT

everythingQ :: (Monoid r) => Type r -> Type a -> Pf (Q r) -> Pf (a -> r)
everythingQ r t@(Data _ fctr) g = everythingQRec r t fctr g
everythingQ r t@(NewData _ fctr) g = everythingQRec r t fctr g
--everythingQ r t@(List a) g = everythingQRec r t (listfctr a) g
everythingQ r t g = APPLYQ t (g `UNION` GMAPQ (EVERYTHING g))

everythingQRec :: (Functor (PF a), Mu a,Monoid r) => Type r -> Type a -> Fctr (PF a) -> Pf (Q r) -> Pf (a -> r)
everythingQRec r t fctr g = let (fr,ft) = (rep fctr r,rep fctr t)
                                (rr,rt) = (Prod r r,Prod r t)
                            in PARA $ COMP rr PLUS
                                    $ COMP (Prod fr t) (gmapQKF r fctr r (EVERYTHING g) `PROD` APPLYQ t g)
                                    $ FMAP fctr (Fun rt r) FST `SPLIT` (COMP ft INN $ FMAP fctr (Fun rt t) SND)


mkQ :: Monoid r => Type a -> Type x -> Pf (x -> r) -> Pf (a -> r)
mkQ a x f = case teq a x of {Just Eq -> f; otherwise -> ZERO}

extQ :: Type x -> Pf (Q r) -> Type a -> Pf (a -> r) -> Pf (x -> r)
extQ t f x g = case teq t x of {Just Eq -> g; otherwise -> APPLYQ t f}