Sums.hs

-----------------------------------------------------------------------------
-- |
-- 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.Pf
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_undef :: Rule
sum_undef t@(Fun (Either a b) c) v@(f `EITHER` g) = do
    COMP _ INL f' <- leftmost (Fun a c) f
    COMP _ INR g' <- leftmost (Fun b c) g
    success "sum-UnDef" $ f' -|-= g'
sum_undef _ _ = 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' t@(Fun _ _) v@(COMP (Either c d) (f `SUM` g) (h `SUM` i)) = do
    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 $ try (comp2 unabides) >>> sum_fusion'
sum_fusion' :: Rule
sum_fusion' t (COMP a f (EITHER g h)) =
    success "sum-Fusion" $ COMP a f g `EITHER`COMP a f h
sum_fusion' _ _ = mzero

sum_absor = comp sum_absor'
sum_absor' :: Rule
sum_absor' t@(Fun _ _) v@(COMP (Either c d) (f `EITHER` g) (h `SUM` i)) = do
    success "sum-Absor" $ (COMP c f h) \/= (COMP d g i)
sum_absor' _ _ = 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 t@(Fun (Either a (Either b c)) _) v@COASSOCL = do
    success "coassocl-Def" $ (COMP (Either a b) INL INL) \/= (INR -|-= ID)
coassocl_def _ _ = mzero

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

sums :: Rule
sums  = top sum_functor_id ||| top sum_functor_comp ||| top sum_eta
    ||| top sum_cancel ||| top sum_absor
    ||| top coswap_def ||| top coassocl_def ||| top coassocr_def