Dists.hs

-----------------------------------------------------------------------------
-- |
-- Module      :  Transform.Rules.PF.Dists
-- 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 distribution of sums over products and vice-versa.
--
-----------------------------------------------------------------------------

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

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

-- ** Distr

distr_def :: Rule
distr_def t@(Fun (Prod c (Either a b)) _) v@DISTR = do
    success "distr-Def" $ COMP (Either (Prod a c) (Prod b c)) (SWAP -|-= SWAP) $ COMP (Prod (Either a b) c) DISTL SWAP
distr_def _ _ = mzero

undistr_def :: Rule
undistr_def (Fun _ _) UNDISTR =
    success "undistr-Def" $ (ID ><= INL) \/= (ID ><= INR)
undistr_def _ _ = mzero
    
-- ** Distl
    
undistl_def :: Rule
undistl_def (Fun _ _) UNDISTL =
    success "undistl-Def" $ INL ><= ID \/= INR ><= ID
undistl_def _ _ = mzero

distl_iso = comp distl_iso'
distl_iso' :: Rule
distl_iso' _ (COMP _ DISTL UNDISTL) =
    success "distl-Iso" ID
distl_iso' _ _ = mzero

undistl_iso = comp distl_iso'
undistl_iso' :: Rule
undistl_iso' _ (COMP _ UNDISTL DISTL) =
    success "distl-Iso" ID
undistl_iso' _ _ = mzero

distl_fst_cancel = comp distl_fst_cancel'
distl_fst_cancel' :: Rule
distl_fst_cancel' (Fun (Prod (Either a b) c) d) (COMP _ (FST `SUM` FST) DISTL) = do
    success "distl-Fst-Cancel" FST
distl_fst_cancel' _ _ = mzero

distl_snd_cancel = comp distl_snd_cancel'
distl_snd_cancel' :: Rule
distl_snd_cancel' (Fun _ _) (COMP _ (SND `EITHER` SND) DISTL) =
    success "distl-Snd-Cancel" SND
distl_snd_cancel' _ _ = mzero

distl_id_cancel = comp distl_id_cancel'
distl_id_cancel' :: Rule
distl_id_cancel' t@(Fun (Prod (Either a b) c) d) x@(COMP y (f `EITHER` g) DISTL) = (do
    Eq <- teq a b
    guard $ geq (Pf (Fun (Prod a c) d)) f g
    success "distl-Id-Cancel" $ COMP (Prod a c) f $ (ID \/= ID) ><= ID)
distl_id_cancel' _ _ = mzero

distl_sum_cancel = comp distl_sum_cancel'
distl_sum_cancel' :: Rule
distl_sum_cancel' (Fun _ _) (COMP _ DISTL ((f `SUM` g) `SPLIT` (h `EITHER` i))) =
    success "distl-Sum-Cancel" $ (f /\= h) -|-= (g /\= i)
distl_sum_cancel' (Fun _ _) (COMP _ DISTL (((COMP _ INL f) `EITHER` (COMP _ INR g)) `SPLIT` (h `EITHER` i))) =
    success "distl-Sum-Cancel" $ (f /\= h) -|-= (g /\= i)
distl_sum_cancel' _ _ = mzero

distl_bang_cancel = comp distl_bang_cancel'
distl_bang_cancel' :: Rule
distl_bang_cancel' (Fun _ _) (COMP _ DISTL (ID `SPLIT` (COMP c h BANG))) =
    success "distl-Bang-Cancel" $ ID /\= (COMP c h BANG) -|-= ID /\= (COMP c h BANG)
distl_bang_cancel' (Fun _ _) (COMP _ DISTL ((f `SUM` g) `SPLIT` (COMP c h BANG))) =
    success "distl-Bang-Cancel" $ f /\= (COMP c h BANG) -|-= g /\= (COMP c h BANG)
distl_bang_cancel' _ _ = mzero

distl_cancel = comp distl_cancel'
distl_cancel' :: Rule
distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL (INL `SPLIT` g)) =
    success "distl-Cancel" $ COMP (Prod a c) INL (ID /\= g)
distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL ((COMP _ INL f) `SPLIT` g)) =
    success "distl-Cancel" $ COMP (Prod a c) INL (f /\= g)
distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL (INR `SPLIT` g)) =
    success "distl-Cancel" $ COMP (Prod b c) INR (ID /\= g)
distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL ((COMP _ INR f) `SPLIT` g)) =
    success "distl-Cancel" $ COMP (Prod b c) INR (f /\= g)
distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL (INL `PROD` g)) =
    success "distl-Cancel" $ COMP (Prod a c) INL (ID ><= g)
distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL ((COMP _ INL f) `PROD` g)) =
    success "distl-Cancel" $ COMP (Prod a c) INL (f ><= g)
distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL (INR `PROD` g)) =
    success "distl-Cancel" $ COMP (Prod b c) INR (ID ><= g)
distl_cancel' (Fun _ _) (COMP (Prod (Either a b) c) DISTL ((COMP _ INR f) `PROD` g)) =
    success "distl-Cancel" $ COMP (Prod b c) INR (f ><= g)
distl_cancel' _ _ = mzero

proj :: Pf (a -> b) -> Bool
proj (f `SPLIT` g) = True
proj FST = True
proj SND = True
proj _ = False

distl_fusion = comp distl_fusion'
distl_fusion' :: Rule
distl_fusion' (Fun _ _) (COMP _ DISTL (f `SPLIT` ID)) = mzero
distl_fusion' (Fun a _) (COMP (Prod (Either b1 b2) d) DISTL (f `SPLIT` c)) = do
    COMP c g h <- leftmost (Fun a d) c
    guard $ not $ proj g
    let t  = Either (Prod b1 c) (Prod b2 c)
        t' = Prod (Either b1 b2) c
    success "distl-Fusion" $ COMP t (ID ><= g -|-= ID ><= g) $ COMP t' DISTL $ f /\= h
distl_fusion' (Fun _ _) (COMP _ DISTL (f `PROD` ID)) = mzero
distl_fusion' (Fun (Prod a c) _) (COMP (Prod (Either a' b') c') DISTL (f `PROD` h)) = do
    let t = Either (Prod a' c) (Prod b' c)
    success "distl-Fusion" $ COMP t (ID ><= h -|-= ID ><= h) $ COMP (Prod (Either a' b') c) DISTL $ f ><= ID
distl_fusion' _ _ = mzero

distl_nat = comp $ comp2 ((try prod_undef) >>> prod1 (try sum_undef)) >>> distl_nat'
distl_nat' :: Rule
distl_nat' (Fun _ _) (COMP _ DISTL (ID `PROD` ID)) = mzero
distl_nat' (Fun (Prod (Either a b) c) _) (COMP _ DISTL ((f `SUM` g) `PROD` h)) = do
    let t = Either (Prod a c) (Prod b c)
    success "distl-Nat" $ COMP t (f ><= h -|-= g ><= h) DISTL
distl_nat' (Fun (Prod (Either a b) c) _) (COMP (Prod (Either a' b') c') DISTL ((f `EITHER` g) `PROD` h)) = do
    let t   = Prod (Either a' b') c'
        t'  = Either (Prod a c) (Prod b c)
    success "distl-Sum-Nat" $ COMP t DISTL $ COMP t' ((f ><= h) \/= (g ><= h)) DISTL
distl_nat' _ _ = mzero

distl_distl_fusion = comp distl_distl_fusion'
distl_distl_fusion' :: Rule
distl_distl_fusion' (Fun x@(Prod (Either a b) c) _) (COMP _ DISTL (SPLIT DISTL f)) = do
    let t = Either (Prod a c) (Prod b c)
    success "distl-Distl-Fusion" $ COMP t ((ID /\= (COMP x f (INL ><= ID))) -|-= (ID /\= (COMP x f (INR ><= ID)))) DISTL
distl_distl_fusion' _ _ = mzero

dists :: Rule
dists = top distr_def ||| top undistr_def ||| top undistl_def 
    ||| top distl_iso ||| top undistl_iso
    ||| top distl_fst_cancel ||| top distl_snd_cancel ||| top distl_id_cancel
    ||| top distl_sum_cancel ||| top distl_bang_cancel ||| top distl_cancel
    ||| top distl_distl_fusion