-----------------------------------------------------------------------------
-- |
-- Module      :  Transform.Rules.PF.Monoids
-- 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 monoids.
--
-----------------------------------------------------------------------------

module Transform.Rules.PF.Monoids where

import Generics.Pointless.Functors hiding (rep)
import Transform.Rewriting
import {-# SOURCE #-} Transform.Rules.PF
import Transform.Rules.PF.Combinators
import Transform.Rules.PF.Products
import Transform.Rules.PF.Sums
import Data.Type
import Data.Pf
import Data.Equal

import Control.Monad hiding (Functor)
import Data.Monoid hiding (Any)
import Prelude hiding (Functor)

cata_zero :: Rule
cata_zero (Fun a r@(isList -> Just Eq)) (CATA f) = cata_zero' (Fun a r) (CATA f)
cata_zero (Fun a r@(isInt -> Just Eq)) (CATA f) = cata_zero' (Fun a r) (CATA f)
cata_zero (Fun a r@(isNat -> Just Eq)) (CATA f) = cata_zero' (Fun a r) (CATA f)
cata_zero _ _ = mzero

cata_zero' :: (Mu a,Functor (PF a),Monoid r) => Type (a -> r) -> Pf (a -> r) -> Rewrite (Pf (a -> r))
cata_zero' (Fun a@(dataFctr -> Just fctr) r) (CATA f) = do
    let (fa,fr) = (rep fctr a,rep fctr r)
        g' = COMP fr f (FMAP fctr (Fun a r) ZERO)
    g <- optimise_pf (Fun fa r) g'
    guard $ geq (Pf $ Fun fa r) ZERO g
    success "cata-Zero" ZERO

plus_zero, plus_zero' :: Rule
plus_zero = comp plus_zero'
plus_zero' _ (COMP _ PLUS (ZERO `SPLIT` f)) = success "plus-Zero" f
plus_zero' (Fun (Prod a b) _) (COMP _ PLUS (ZERO `PROD` f)) = success "plus-Zero" $ COMP b f SND
plus_zero' _ (COMP _ PLUS (f `SPLIT` ZERO)) = success "plus-Zero" f
plus_zero' (Fun (Prod a b) _) (COMP _ PLUS (f `PROD` ZERO)) = success "plus-Zero" $ COMP a f FST
plus_zero' _ _ = mzero

zero_fusion, zero_fusion' :: Rule
zero_fusion = comp zero_fusion'
zero_fusion' _ (COMP _ ZERO f) = success "zero-Fusion" ZERO
zero_fusion' _ _ = mzero

zero_either :: Rule
zero_either _ (ZERO `EITHER` ZERO) = success "zero-Either" ZERO
zero_either _ _ = mzero

fold_plus, fold_plus' :: Rule
fold_plus = comp fold_plus'
fold_plus' (Fun _ r) (COMP _ FOLD PLUS) = success "fold-Plus" $ COMP (Prod r r) PLUS (FOLD `PROD` FOLD)
fold_plus' _ _ = mzero

fold_zero, fold_zero' :: Rule
fold_zero = comp fold_zero'
fold_zero' _ (COMP _ FOLD ZERO) = success "fold-Zero" ZERO
fold_zero' _ _ = mzero

monoids :: Rule
monoids = top plus_zero ||| top zero_fusion ||| top fold_plus ||| top fold_zero ||| top zero_either