-----------------------------------------------------------------------------
-- |
-- 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.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_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' (Fun _ _) (COMP (Prod c d) (f `PROD` g) (h `PROD` i)) =
    success "prod-Functor-Comp" $ COMP c f h ><= COMP d g i
prod_functor_comp' _ _ = mzero

prod_cancel = comp prod_cancel'
prod_cancel' :: Rule
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 prod_fusion'
prod_fusion' :: Rule
prod_fusion' t (COMP c (SPLIT f g) h) =
    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' (Fun _ _) (COMP (Prod c d) (f `PROD` g) (h `SPLIT` i)) =
    success "prod-Absor" $ (COMP c f h) /\= (COMP d g i)
prod_absor' _ _ = mzero

-- ** Isomorphisms

swap_def :: Rule
swap_def (Fun (Prod a b) _) SWAP =
    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