-----------------------------------------------------------------------------
-- |
-- Module      :  Transform.Rules.PF.Sums
-- 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 sums.
--
-----------------------------------------------------------------------------

module Transform.Rules.PF.Sums where

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

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

-- ** Sums

sum_def :: Rule
sum_def t@(Fun _ (Either a b)) (SUM f g) =
    success "sum-Def" $ (EITHER (COMP a INL f) (COMP b INR g))
sum_def _ _ = mzero

sum_eta :: Rule
sum_eta a (EITHER (COMP b1 k1 INL) (COMP b2 k2 INR)) = do
    Eq <- teq b1 b2
    guard (geq (Pf a) k1 k2)
    success "sum-Eta" k1
sum_eta _ _ = mzero

sum_functor_id :: Rule
sum_functor_id _ (EITHER INL INR) =
    success "sum-Functor-Id" ID
sum_functor_id _ (SUM ID ID) =
    success "sum-Functor-Id" ID
sum_functor_id _ _ = mzero

sum_functor_comp = comp sum_functor_comp'
sum_functor_comp' :: Rule
sum_functor_comp' (Fun _ _) (COMP (Either c d) (f `SUM` g) (h `SUM` i)) =
    success "sum-Functor-Comp" $ COMP c f h -|-= COMP d g i
sum_functor_comp' _ _ = mzero

sum_cancel = comp sum_cancel'
sum_cancel' :: Rule
sum_cancel' t (COMP _ (EITHER f g) INL) =
    success "sum-Cancel" f
sum_cancel' (Fun _ (Either c d)) (COMP _ (f `SUM` g) INL) =
    success "sum-Cancel" $ COMP c INL f
sum_cancel' t (COMP _ (EITHER f g) INR) =
    success "sum-Cancel" g
sum_cancel' (Fun _ (Either c d)) (COMP _ (f `SUM` g) INR) =
    success "sum-Cancel" $ COMP d INR g
sum_cancel' _ _ = mzero

sum_fusion = comp sum_fusion'
sum_fusion' :: Rule
sum_fusion' t (COMP a f (EITHER g h)) =
    success "sum-Fusion" $ EITHER (COMP a f g) (COMP a f h)
sum_fusion' _ _ = mzero

sum_absor = comp sum_absor'
sum_absor' :: Rule
sum_absor' (Fun _ _) (COMP (Either c d) (f `EITHER` g) (h `SUM` i)) = 
    success "sum-Absor" $ (COMP c f h) \/= (COMP d g i)
sum_absor' _ _ = mzero

-- ** Relating sums with products

--abides = abides' ||| (sum_unfusion >>> comp2 abides')
abides = abides'
abides' :: Rule
abides' (Fun _ _) ((f `SPLIT` g) `EITHER` (h `SPLIT` i)) =
    success "abides" $ (f \/= h) /\= (g \/= i)
abides' _ _ = mzero

-- ** Isomorphisms

coswap_def :: Rule
coswap_def (Fun (Either a b) _) COSWAP =
    success "coswap-Def" $ INR \/= INL
coswap_def _ _ = mzero

coassocl_def :: Rule
coassocl_def (Fun (Either a (Either b c)) _) COASSOCL =
    success "coassocl-Def" $ (COMP (Either a b) INL INL) \/= (INR -|-= ID)
coassocl_def _ _ = mzero

coassocr_def :: Rule
coassocr_def (Fun (Either (Either a b) c) _) COASSOCR =
    success "coassocr-Def" $ (ID -|-= INL) \/= (COMP (Either b c) INR INR)
coassocr_def _ _ = mzero