-----------------------------------------------------------------------------
-- |
-- 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.Equal

import Data.Monoid

import Generics.Pointless.Combinators
import Generics.Pointless.RecursionPatterns
import Generics.Pointless.Functors
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.Recs

fctrT :: Functor f => Fctr f -> F.Fctr f
fctrT I = F.I
fctrT (K c) = F.K
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 (fctrT f) (create l)
          create' = fmap fix (create l)
          fix = fixF f

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

cata_lnsF :: (Mu a,Functor (PF a)) => a -> Fctr (PF a) -> (Lens (F a b) b) -> Lens a b
cata_lnsF (a::a) f l = Lens get' put' create'
    where get' = cata a (get l)
          put' = ana a (fzip (fctrT 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 _ HOLE = error "hole"
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 c a) (COMPF fctr x f g) = eval (Fun c a) (COMP (rep fctr x) f g)
eval (Lns c a) (COMPF_LNS fctr x f g) = eval (Lns c a) (COMP_LNS (rep fctr x) f g)
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 _ ZERO = const mempty
eval _ PLUS = uncurry mappend

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 (fctrT fctr) $ eval t f
eval (Fun a b@(Data _ fctr)) (ANA f) = ana _L (eval (Fun a (rep fctr a)) f)
eval (Fun a@(Data _ fctr) b) (CATA f) = cata _L (eval (Fun (rep fctr b) b) f)
eval (Fun a@(Data _ fctr) b) (PARA f) = para _L (eval (Fun (rep fctr (Prod b a)) b) f)

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 _ a@(Data _ fctr)) INN_LNS = inn_lnsF fctr
eval (Lns a@(Data _ 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 b@(Data _ fctr)) (ANA_LNS f) = ana_lnsF _L fctr (eval (Lns a (rep fctr a)) f)
eval (Lns a@(Data _ fctr) b) (CATA_LNS f) = cata_lnsF _L fctr (eval (Lns (rep fctr b) b) f)

eval (Lns la lb) (MAP_LNS l1) = map_pf (eval (Lns (unlist la) (unlist lb)) l1)
eval (Lns la _) (LENGTH_LNS v) = length_pf 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 _ _) SUML_LNS = suml_pf
eval (Lns _ _) PLUS_LNS = plus_pf

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 a r)(APPLYQ _ (GMAPQ f)) = eval q (gmapQ r a f)
eval q (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

everywhereEval t f = APPLY t (f `SEQ` ALL (EVERYWHERE f))
everywhereEval' t f = APPLY t (ALL (EVERYWHERE' f) `SEQ` f)
everythingEval t f = APPLYQ t (f `UNION` GMAPQ (EVERYTHING f))

-- ** Type-preserving specialization

allT :: Type a -> Pf T -> Pf (a -> a)
allT t@(Data _ fctr) g = let f = rep fctr t in COMP f INN $ COMP f (allTN f g) OUT
allT (Either a b) f = (APPLY a f) `SUM` (APPLY b f)
allT (Prod a b) f = (APPLY a f) `PROD` (APPLY b f)
allT _ _ = ID
-- | We do not want it to recurse inside Datas, otherwise we get a full traversal
allTN :: Type a -> Pf T -> Pf (a -> a)
allTN (Either a b) f = (allTN a f) `SUM` (allTN b f)
allTN (Prod a b) f = (allTN a f) `PROD` (allTN b f)
allTN a f = APPLY a f

-- | bottom-up (cata)
everywhereT :: Type a -> Pf T -> Pf (a -> a)
everywhereT t@(Data _ fctr) g = let f = rep fctr t
                                    boxf = rep fctr (Id t)
                                in CATA $ COMP t (APPLY t g) $ COMP f INN $ APPLY boxf $ EVERYWHERE g
everywhereT (Id t) f = ID
everywhereT t f = APPLY t (ALL (EVERYWHERE f) `SEQ` f)

-- | top-down (ana)
everywhereT' :: Type a -> Pf T -> Pf (a -> a)
everywhereT' t@(Data _ fctr) g = let f = rep fctr t
                                     boxf = rep fctr (Id t)
                                 in ANA $ COMP f (APPLY boxf $ EVERYWHERE' g) $ COMP t OUT $ APPLY t g
everywhereT' t f = APPLY t (f `SEQ` ALL (EVERYWHERE' f))

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

gmapQProd :: (Monoid r) => Type r -> Pf (a -> (r,r)) -> Pf (a -> r)
gmapQProd r (p::Pf (a -> (r,r))) = COMP (Prod r r) PLUS p

gmapQId :: (Monoid r) => Type r -> Type r' -> Pf (Q r) -> Pf (r' -> r)
gmapQId r r' (f :: Pf (Q r)) = case teq r' r of {Just Eq -> ID; otherwise -> ZERO}

gmapQ :: (Monoid r) => Type r -> Type a -> Pf (Q r) -> Pf (a -> r)
gmapQ r t@(Data _ fctr) g = let f = rep fctr t in COMP f (gmapQN r f g) OUT
gmapQ r (Either a b) f = (APPLYQ a f) `EITHER` (APPLYQ b f)
gmapQ r (Prod a b) f = gmapQProd r $ (APPLYQ a f) `PROD` (APPLYQ b f)
gmapQ r (Id a) f = gmapQId r a f
gmapQ r t f = ZERO

-- | We do not want it to recurse inside Datas, otherwise we get a full traversal
gmapQN :: (Monoid r) => Type r -> Type a -> Pf (Q r) -> Pf (a -> r)
gmapQN r (Either a b) f = (gmapQN r a f) `EITHER` (gmapQN r b f)
gmapQN r (Prod a b) f = gmapQProd r $ (gmapQN r a f) `PROD` (gmapQN r b f)
gmapQN r a f = APPLYQ a f

everythingQ :: (Monoid r) => Type r -> Type a -> Pf (Q r) -> Pf (a -> r)
everythingQ r t@(Data _ fctr::Type t) (g::Pf (Q r)) = let fr = rep fctr r
                                                          boxfr = rep fctr (Id r)
                                                          ft = rep fctr t
                                                      in PARA $ gmapQProd r $ COMP (Prod fr ft) ((APPLYQ boxfr $ EVERYTHING g) `PROD` (COMP t (APPLYQ t g) INN)) (FMAP fctr (Fun (Prod r t) r) FST `SPLIT` FMAP fctr (Fun (Prod r t) t) SND)
everythingQ r t f = APPLYQ t (f `UNION` GMAPQ (EVERYTHING f))


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}