-----------------------------------------------------------------------------
-- |
-- Module      :  Transform.Rules.PF.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 functions involving lists.
--
-----------------------------------------------------------------------------

module Transform.Rules.PF.Lists where

import Transform.Rewriting
import Transform.Rules.PF.Combinators
import Data.Type
import Data.Pf

import Control.Monad

map_id :: Rule
map_id _ (MAP ID) = success "map-Id" ID
map_id _ _ = mzero

map_wrap, map_wrap' :: Rule
map_wrap = comp map_wrap'
map_wrap' (Fun _ (List b)) (COMP _ (MAP f) WRAP) = success "map-Wrap" $ COMP b WRAP f
map_wrap' _ _ = mzero

map_fusion, map_fusion' :: Rule
map_fusion = comp map_fusion'
map_fusion' _ (COMP (List a) (MAP f) (MAP g)) = success "map-Fusion" $ MAP $ COMP a f g
map_fusion' _ _ = mzero

-- Monoids

fold_mapzero, fold_mapzero' :: Rule
fold_mapzero = comp fold_mapzero'
fold_mapzero' _ (COMP _ FOLD (MAP ZERO)) = success "fold-MapZero" ZERO
fold_mapzero' _ _ = mzero

fold_wrap, fold_wrap' :: Rule
fold_wrap = comp fold_wrap'
fold_wrap' _ (COMP _ FOLD WRAP) = success "fold-Wrap" ID
fold_wrap' _ _ = mzero

fold_mapwrap, fold_mapwrap' :: Rule
fold_mapwrap = comp fold_mapwrap'
fold_mapwrap' _ (COMP _ FOLD (MAP WRAP)) = success "fold-MapWrap" $ ID
fold_mapwrap' _ (COMP _ FOLD (MAP (COMP _ WRAP f))) = success "fold-MapWrap" $ MAP f
fold_mapwrap' _ _ = mzero

map_plus, map_plus' :: Rule
map_plus = comp map_plus'
map_plus' (Fun _ r) (COMP _ (MAP f) PLUS) = success "map-Plus" $ COMP (Prod r r) PLUS (MAP f `PROD` MAP f)
map_plus' _ _ = mzero

map_zero, map_zero' :: Rule
map_zero = comp map_zero'
map_zero' _ (COMP _ (MAP f) ZERO) = success "map-Zero" ZERO
map_zero' _ _ = mzero

map_fold, map_fold' :: Rule
map_fold = comp map_fold'
map_fold' (Fun _ r) (COMP _ (MAP f) FOLD) = success "map-Fold" $ COMP (List r) FOLD $ MAP (MAP f)
map_fold' _ _ = mzero

fold_foldmap, fold_foldmap' :: Rule
fold_foldmap = comp fold_foldmap'
fold_foldmap' (Fun _ r) (COMP _ FOLD (COMP (List a) FOLD (MAP f))) = success "fold-FoldMap" $ COMP (List r) FOLD $ MAP (COMP a FOLD f)
fold_foldmap' _ _ = mzero

length_zero, length_zero' :: Rule
length_zero = comp length_zero'
length_zero' (Fun _ _) (COMP _ LENGTH ZERO) = success "length-Zero" ZERO
length_zero' _ _ = mzero

length_wrap, length_wrap' :: Rule
length_wrap = comp length_wrap'
length_wrap' (Fun _ _) (COMP _ LENGTH WRAP) = success "length-Wrap" ONE
length_wrap' _ _ = mzero

fold_mapone, fold_mapone' :: Rule
fold_mapone = comp fold_mapone'
fold_mapone' (Fun _ _) (COMP _ FOLD (MAP ONE)) = success "length" LENGTH
fold_mapone' _ _ = mzero

length_plus = comp length_plus'
length_plus' :: Rule
length_plus' (Fun _ _) (COMP _ LENGTH PLUS) =
    success "length-Plus" $ COMP (Prod nat nat) PLUS $ LENGTH `PROD` LENGTH
length_plus' _ _ = mzero

length_map = comp length_map'
length_map' :: Rule
length_map' t@(Fun la@(List a) _) v@(COMP lb@(List b) LENGTH (MAP l1)) = do
    success "length-Map" LENGTH
length_map' _ _ = mzero

length_fold = comp length_fold'
length_fold' :: Rule
length_fold' (Fun _ _) (COMP _ LENGTH FOLD) =
    success "length-Fold" $ COMP (List nat) FOLD $ MAP LENGTH
length_fold' _ _ = mzero

one_fusion, one_fusion' :: Rule
one_fusion = comp one_fusion'
one_fusion' _ (COMP _ ONE f) = success "one-Fusion" ONE
one_fusion' _ _ = mzero

head_nil, head_nil' :: Rule
head_nil = comp head_nil'
head_nil' _ (COMP _ LHEAD ZERO) = success "head-Zero" ZERO
head_nil' _ _ = mzero

head_wrap, head_wrap' :: Rule
head_wrap = comp head_wrap'
head_wrap' _ (COMP _ LHEAD WRAP) = success "head-Wrap" WRAP
head_wrap' _ _ = mzero

tail_nil, head_nil' :: Rule
tail_nil = comp head_nil'
tail_nil' _ (COMP _ LTAIL ZERO) = success "tail-Zero" ZERO
tail_nil' _ _ = mzero

tail_wrap, head_wrap' :: Rule
tail_wrap = comp head_wrap'
tail_wrap' _ (COMP _ LTAIL WRAP) = success "tail-Wrap" ZERO
tail_wrap' _ _ = mzero

lists :: Rule
lists = top map_id ||| top map_wrap ||| top map_fusion
    ||| top map_plus ||| top map_zero ||| top map_fold
    ||| top fold_mapzero ||| top fold_wrap ||| top fold_mapwrap ||| top fold_foldmap
    ||| top length_zero ||| top length_plus ||| top length_map ||| top length_fold
    ||| top length_wrap ||| top fold_mapone ||| top one_fusion
    ||| top head_nil ||| top head_wrap ||| top tail_nil ||| top tail_wrap