-----------------------------------------------------------------------------
-- |
-- Module      :  Transform.Rules.Lenses.Lists
-- 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
-- 
-- Combinators for the rewriting of point-free lenses involving lists.
--
-----------------------------------------------------------------------------

module Transform.Rules.Lenses.Lists where

import Data.Type
import Data.Pf
import Data.Eval
import Data.Lens
import Transform.Rewriting
import Transform.Rules.Lenses.Combinators

import Prelude hiding (Functor(..))
import Control.Monad hiding (Functor(..))

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

-- ** List laws

map_id_lns :: Rule
map_id_lns (Lns _ _) (MAP_LNS ID_LNS) =
    success "map-Id-Lns" $ ID_LNS
map_id_lns _ _ = mzero

map_fusion_lns = comp_lns map_fusion_lns'
map_fusion_lns' :: Rule
map_fusion_lns' (Lns _ _) (COMP_LNS (List c) (MAP_LNS l1) (MAP_LNS l2)) =
    success "map-Fusion-Lns" $ MAP_LNS $ COMP_LNS c l1 l2
map_fusion_lns' _ _ = mzero

leftmost_map_lns :: Rule
leftmost_map_lns (Lns (List a) (List b)) (MAP_LNS l1) = do
    (COMP_LNS c f g) <- leftmost_lns' (Lns a b) l1
    return $ COMP_LNS (List c) (MAP_LNS f) (MAP_LNS g)
leftmost_map_lns _ _ = mzero

map_cat_lns = comp_lns map_cat_lns'
map_cat_lns' :: Rule
map_cat_lns' (Lns _ lb) (COMP_LNS _ (MAP_LNS l1) CAT_LNS) =
    success "map-Cat-Lns" $ COMP_LNS (Prod lb lb) CAT_LNS (MAP_LNS l1 ><<< MAP_LNS l1)
map_cat_lns' _ _ = mzero

map_concat_lns = comp_lns map_concat_lns'
map_concat_lns' :: Rule
map_concat_lns' (Lns _ lb) (COMP_LNS _ (MAP_LNS l1) CONCAT_LNS) =
    success "map-Concat-Lns" $ COMP_LNS (List lb) CONCAT_LNS $ MAP_LNS $ MAP_LNS l1
map_concat_lns' _ _ = mzero

filter_cat_lns = comp_lns filter_cat_lns'
filter_cat_lns' :: Rule
filter_cat_lns' (Lns _ la) (COMP_LNS _ FILTER_LEFT_LNS CAT_LNS) =
    success "filter-Cat-Lns" $ COMP_LNS (Prod la la) CAT_LNS (FILTER_LEFT_LNS ><<< FILTER_LEFT_LNS)
filter_cat_lns' (Lns _ lb) (COMP_LNS _ FILTER_RIGHT_LNS CAT_LNS) =
    success "filter-Cat-Lns" $ COMP_LNS (Prod lb lb) CAT_LNS (FILTER_RIGHT_LNS ><<< FILTER_RIGHT_LNS)
filter_cat_lns' _ _ = mzero

filter_map_lns = postcomp_lns leftmost_map_lns filter_map_lns'
filter_map_lns' :: Rule
filter_map_lns' (Lns (List (Either a b)) _) (COMP_LNS _ FILTER_LEFT_LNS (MAP_LNS (l1 `SUM_LNS` l2))) = do
    success "filter-Map-Lns" $ COMP_LNS (List a) (MAP_LNS l1) FILTER_LEFT_LNS
filter_map_lns' (Lns (List (Either a b)) _) (COMP_LNS _ FILTER_LEFT_LNS (MAP_LNS (SUMW_LNS _ _ l1 l2))) = do
    success "filter-Map-Lns" $ COMP_LNS (List a) (MAP_LNS l1) FILTER_LEFT_LNS
filter_map_lns' (Lns (List (Either a b)) _) (COMP_LNS _ FILTER_RIGHT_LNS (MAP_LNS (l1 `SUM_LNS` l2))) = do
    success "filter-Map-Lns" $ COMP_LNS (List b) (MAP_LNS l2) FILTER_RIGHT_LNS
filter_map_lns' (Lns (List (Either a b)) _) (COMP_LNS _ FILTER_RIGHT_LNS (MAP_LNS (SUMW_LNS _ _ l1 l2))) = do
    success "filter-Map-Lns" $ COMP_LNS (List b) (MAP_LNS l2) FILTER_RIGHT_LNS
filter_map_lns' _ _ = mzero

filter_concat_lns = comp_lns filter_concat_lns'
filter_concat_lns' :: Rule
filter_concat_lns' (Lns _ la) (COMP_LNS _ FILTER_LEFT_LNS CONCAT_LNS) =
    success "filter-Concat-Lns" $ COMP_LNS (List la) CONCAT_LNS $ MAP_LNS FILTER_LEFT_LNS
filter_concat_lns' (Lns _ lb) (COMP_LNS _ FILTER_RIGHT_LNS CONCAT_LNS) =
    success "filter-Concat-Lns" $ COMP_LNS (List lb) CONCAT_LNS $ MAP_LNS FILTER_RIGHT_LNS
filter_concat_lns' _ _ = mzero

sum_cat_lns = comp_lns sum_cat_lns'
sum_cat_lns' :: Rule
sum_cat_lns' (Lns _ _) (COMP_LNS _ SUMN_LNS CAT_LNS) =
    success "sum-Cat-Lns" $ COMP_LNS (Prod nat nat) PLUSN_LNS (SUMN_LNS ><<< SUMN_LNS)
sum_cat_lns' _ _ = mzero

sum_concat_lns = comp_lns sum_concat_lns'
sum_concat_lns' :: Rule
sum_concat_lns' (Lns _ _) (COMP_LNS _ SUMN_LNS CONCAT_LNS) =
    success "sum-Concat-Lns" $ COMP_LNS (List nat) SUMN_LNS (MAP_LNS SUMN_LNS)
sum_concat_lns' _ _ = mzero

length_cat_lns = comp_lns length_cat_lns'
length_cat_lns' :: Rule
length_cat_lns' (Lns _ _) (COMP_LNS _ (LENGTH_LNS f) CAT_LNS) =
    success "length-Cat-Lns" $ COMP_LNS (Prod nat nat) PLUSN_LNS $ LENGTH_LNS f ><<< LENGTH_LNS f
length_cat_lns' _ _ = mzero

length_map_lns = comp_lns length_map_lns'
length_map_lns' :: Rule
length_map_lns' t@(Lns la@(List a) _) v@(COMP_LNS lb@(List b) (LENGTH_LNS va) (MAP_LNS l1)) = do
    debug "length-Map-Lns" (Pf t) v
    let va' = (eval (Fun b a) (createof (Lns a b) l1)) va
    success "length-Map-Lns" $ LENGTH_LNS va'
length_map_lns' _ _ = mzero

length_concat_lns = comp_lns length_concat_lns'
length_concat_lns' :: Rule
length_concat_lns' (Lns _ _) (COMP_LNS _ (LENGTH_LNS f) CONCAT_LNS) =
    success "length-Concat-Lns" $ COMP_LNS (List nat) SUMN_LNS $ MAP_LNS $ LENGTH_LNS f
length_concat_lns' _ _ = mzero

cata_map_fusion_lns = comp_lns cata_map_fusion_lns'
cata_map_fusion_lns' :: Rule
cata_map_fusion_lns' (Lns la c) (COMP_LNS lb@(List b) (CATA_LNS l1) (MAP_LNS l2)) =
    success "cata-Map-Fusion-Lns" $ CATA_LNS $ COMP_LNS (Either One (Prod b c)) l1 $ ID_LNS -|-<< l2 ><<< ID_LNS
cata_map_fusion_lns' _ _ = mzero

ana_map_fusion_lns = comp_lns ana_map_fusion_lns'
ana_map_fusion_lns' :: Rule
ana_map_fusion_lns' (Lns a lc) (COMP_LNS lb@(List b) (MAP_LNS l2) (ANA_LNS l1)) =
    success "ana-Map-Fusion-Lns" $ ANA_LNS $ COMP_LNS (Either One (Prod b a)) (ID_LNS -|-<< l2 ><<< ID_LNS) l1
ana_map_fusion_lns' _ _ = mzero

-- ** Definitions

list_defs_lns :: Rule
list_defs_lns = list_catas_defs_lns ||| list_anas_defs_lns ||| list_hylos_defs_lns

list_catas_defs_lns :: Rule
list_catas_defs_lns = top map_cata_def_lns ||| top length_cata_def_lns
         ||| top concat_def_lns ||| top sum_def_lns ||| top filter_def_lns

list_anas_defs_lns :: Rule
list_anas_defs_lns = top map_ana_def_lns ||| top length_ana_def_lns

list_hylos_defs_lns :: Rule
list_hylos_defs_lns = top plus_def_lns ||| top cat_def_lns

inle :: Type a -> Type b -> Pf (Lens (Either a (Either a b)) (Either a b))
inle a b = COMP_LNS (Either (Either a a) b) ((EITHER_LNS (COMP One INL BANG) ID_LNS ID_LNS) -|-<< ID_LNS) COASSOCL_LNS

inre :: Type a -> Type b -> Pf (Lens (Either (Either a b) b) (Either a b))
inre a b = COMP_LNS (Either a (Either b b)) (ID_LNS -|-<< (EITHER_LNS (COMP One INR BANG) ID_LNS ID_LNS)) COASSOCR_LNS

map_cata_def_lns :: Rule
map_cata_def_lns (Lns _ lb@(List b)) (MAP_LNS l1) =
    success "map-Cata-Def-Lns" $ CATA_LNS $ COMP_LNS (Either One (Prod b lb)) INN_LNS (ID_LNS -|-<< l1 ><<< ID_LNS)
map_cata_def_lns _ _ = mzero

map_ana_def_lns :: Rule
map_ana_def_lns (Lns la@(List a) _) (MAP_LNS l1) =
    success "map-Ana-Def-Lns" $ ANA_LNS $ COMP_LNS (Either One (Prod a la)) (ID_LNS -|-<< l1 ><<< ID_LNS) OUT_LNS
map_ana_def_lns _ _ = mzero

filter_def_lns :: Rule
filter_def_lns (Lns (List (Either a b)) la) FILTER_LEFT_LNS = do
    let e = (\/<<) (COMP One INL BANG) INN_LNS (SND_LNS TOP)
        t = Either (Either One (Prod a la)) (Prod b la)
        t' = Either One (Either (Prod a la) (Prod b la))
    success "filter-Def-Lns" $ CATA_LNS $ COMP_LNS t e $ COMP_LNS t' COASSOCL_LNS (ID_LNS -|-<< DISTL_LNS)
filter_def_lns (Lns (List (Either a b)) lb) FILTER_RIGHT_LNS = do
    let e = (\/<<) (COMP One INL BANG) INN_LNS (SND_LNS TOP)
        t = Either (Either One (Prod b lb)) (Prod a lb)
        t' = Either One (Either (Prod b lb) (Prod a lb))
        t'' = Either (Prod a lb) (Prod b lb)
    success "filter-Def-Lns" $ CATA_LNS $ COMP_LNS t e $ COMP_LNS t' COASSOCL_LNS (ID_LNS -|-<< COMP_LNS t'' COSWAP_LNS DISTL_LNS)
filter_def_lns _ _ = mzero

length_cata_def_lns :: Rule
length_cata_def_lns (Lns _ _) (LENGTH_LNS v) = do
    let f = COMP One (PNT v) BANG
    success "length-Cata-Def-Lns" $ CATA_LNS $ COMP_LNS (Either One nat) INN_LNS (ID_LNS -|-<< SND_LNS f)
length_cata_def_lns _ _ = mzero

length_ana_def_lns :: Rule
length_ana_def_lns (Lns la@(List a) _) (LENGTH_LNS v) = do
    let f = COMP One (PNT v) BANG
    success "length-Ana-Def-Lns" $ ANA_LNS $ COMP_LNS (Either One (Prod a la)) (ID_LNS -|-<< SND_LNS f) OUT_LNS
length_ana_def_lns _ _ = mzero

cat_def_lns :: Rule
cat_def_lns (Lns _ la@(List a)) CAT_LNS = do
    let t = Prod (Either One (Prod a la)) la
        t' = Either (Prod One la) (Prod (Prod a la) la)
        t'' = Either (Either One (Prod a la)) (Prod a la)
        t''' = Either One (Prod a la)
        g = CATA_LNS $ COMP_LNS t''' INN_LNS $ COMP_LNS t'' (inre One (Prod a la)) (OUT_LNS -|-<< ID_LNS)
        h = ANA_LNS $ COMP_LNS t' (SND_LNS BANG -|-<< ASSOCR_LNS) $ COMP_LNS t DISTL_LNS (OUT_LNS ><<< ID_LNS)
        f = fixof (K la :+!: (K a :*!: I))
    success "cat-Def-Lns" $ COMP_LNS f g h
cat_def_lns _ _ = mzero

concat_def_lns :: Rule
concat_def_lns (Lns _ la@(List a)) CONCAT_LNS = do
    let aux = COMP_LNS (Either One (Either One (Prod a la))) (inle One (Prod a la)) (ID_LNS -|-<< (COMP_LNS la OUT_LNS CAT_LNS))
    success "concat-Def-Lns" $ CATA_LNS $ COMP_LNS (Either One (Prod a la)) INN_LNS aux
concat_def_lns _ _ = mzero

plus_def_lns :: Rule
plus_def_lns (Lns _ _) PLUSN_LNS = do
    let t = Prod (Either One nat) nat
        t' = Either (Prod One nat) (Prod nat nat)
        t'' = Either (Either One nat) nat
        l1 = COMP_LNS (Either One nat) INN_LNS $ COMP_LNS t'' (inre One nat) (OUT_LNS -|-<< ID_LNS)
        l2 = COMP_LNS t' (SND_LNS BANG -|-<< ID_LNS) $ COMP_LNS t DISTL_LNS (OUT_LNS ><<< ID_LNS)
        f = typeof :: Type (Fix (Const Nat :+: Id))
    success "plus-Def-Lns" $ COMP_LNS f (CATA_LNS l1) (ANA_LNS l2)
plus_def_lns _ _ = mzero

sum_def_lns :: Rule
sum_def_lns (Lns _ _) SUMN_LNS = do
    let t = Either One (Either One nat)
        aux = COMP_LNS t (inle One nat) (ID_LNS -|-<< (COMP_LNS nat OUT_LNS PLUSN_LNS))
    success "sum-Def-Lns" $ CATA_LNS $ COMP_LNS (Either One nat) INN_LNS aux
sum_def_lns _ _ = mzero

lists :: Rule
lists = top map_id_lns ||| top map_fusion_lns
    ||| top map_cat_lns ||| top map_concat_lns
    ||| top filter_cat_lns ||| top filter_map_lns ||| top filter_concat_lns
    ||| top sum_cat_lns ||| top sum_concat_lns
    ||| top length_cat_lns ||| top length_map_lns ||| top length_concat_lns