-----------------------------------------------------------------------------
-- |
-- Module      :  Transform.Rules.PF.Products
-- 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 products.
--
-----------------------------------------------------------------------------

module Transform.Rules.PF.Products where
    
import Data.Type
import Data.Pf
import Data.Equal
import Transform.Rewriting
import Transform.Rules.PF.Combinators

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

-- ** Products

prod_def :: Rule
prod_def t@(Fun (Prod a b) _) (PROD f g) =
    success "prod-Def" $ (COMP a f FST) `SPLIT` (COMP b g SND)
prod_def _ _ = mzero

prod_undef :: Rule
prod_undef t@(Fun a (Prod b c)) (f `SPLIT` g) = do
    COMP _ f' FST <- rightmost (Fun a b) f
    COMP _ g' SND <- rightmost (Fun a c) g
    success "prod-UnDef" $ f' ><= g'
prod_undef _ _ = mzero

prod_eta :: Rule
prod_eta a (SPLIT (COMP b FST f) (COMP c SND g)) = do
    Eq <- teq b c
    guard (geq (Pf a) f g)
    success "prod-Eta" f
prod_eta _ _ = mzero

prod_functor_id :: Rule
prod_functor_id _ (SPLIT FST SND) =
    success "prod-Functor-Id" ID
prod_functor_id _ (PROD ID ID) =
    success "prod-Functor-Id" ID
prod_functor_id _ _ = mzero

prod_functor_comp = comp prod_functor_comp'
prod_functor_comp' :: Rule
prod_functor_comp' t@(Fun a b) v@(COMP (Prod c d) (f `PROD` g) (h `PROD` i)) = do
    success "prod-Functor-Comp" $ COMP c f h ><= COMP d g i
prod_functor_comp' _ _ = mzero

prod_cancel, prod_cancel' :: Rule
prod_cancel = comp prod_cancel'
prod_cancel' t (COMP _ FST (SPLIT f g)) =
    success "prod-Cancel" f
prod_cancel' (Fun (Prod a b) _) (COMP _ FST (f `PROD` g)) =
    success "prod-Cancel" $ COMP a f FST
prod_cancel' t (COMP _ SND (SPLIT f g)) =
    success "prod-Cancel" g
prod_cancel' (Fun (Prod a b) _) (COMP _ SND (f `PROD` g)) =
    success "prod-Cancel" $ COMP b g SND
prod_cancel' _ _ = mzero

prod_fusion = comp $ try (comp1 abides) >>> prod_fusion'
prod_fusion' :: Rule
prod_fusion' t v@(COMP c (SPLIT f g) h) = do
    success "prod-Fusion" $ (COMP c f h) `SPLIT` (COMP c g h)
prod_fusion' _ _ = mzero

prod_absor = comp prod_absor'
prod_absor' :: Rule
prod_absor' t@(Fun _ _) v@(COMP (Prod c d) (f `PROD` g) (h `SPLIT` i)) = do
    success "prod-Absor" $ (COMP c f h) /\= (COMP d g i)
prod_absor' _ _ = mzero

-- ** Isomorphisms

swap_def :: Rule
swap_def t@(Fun (Prod a b) _) v@SWAP = do
    success "swap-Def" $ SND /\= FST
swap_def _ _ = mzero

assocl_def :: Rule
assocl_def (Fun (Prod a (Prod b c)) _) ASSOCL =
    success "assocl-Def" $ (ID ><= FST) /\= (COMP (Prod b c) SND SND)
assocl_def _ _ = mzero

assocr_def :: Rule
assocr_def (Fun (Prod (Prod a b) c) _) ASSOCR =
    success "assocr-Def" $ (COMP (Prod a b) FST FST) /\= (SND ><= ID)
assocr_def _ _ = mzero

prods :: Rule
prods = top prod_functor_id ||| top prod_functor_comp
    ||| top prod_cancel ||| top prod_absor ||| top prod_eta
    ||| top swap_def ||| top assocl_def ||| top assocr_def