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

module Transform.Rules.Lenses.Dists where

import Data.Type
import Data.Pf
import Data.Lens
import Transform.Rewriting
import Transform.Rules.Lenses.Combinators
import {-# SOURCE #-} qualified Transform.Rules.PF as PF

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

-- ** Distr

distr_def_lns :: Rule
distr_def_lns (Lns (Prod c (Either a b)) _) DISTR_LNS = do
    let t  = Either (Prod a c) (Prod b c)
        t' = Prod (Either a b) c
    success "distr-Def-Lns" $ COMP_LNS t (SWAP_LNS -|-<< SWAP_LNS) $ COMP_LNS t' DISTL_LNS SWAP_LNS
distr_def_lns _ _ = mzero

undistr_def_lns :: Rule
undistr_def_lns (Lns _ (Prod c (Either a b))) UNDISTR_LNS = do
    let t  = Prod (Either a b) c
        t' = Either (Prod a c) (Prod b c)
    success "undistr-Def-Lns" $ COMP_LNS t SWAP_LNS $ COMP_LNS t' UNDISTL_LNS $ (SWAP_LNS -|-<< SWAP_LNS)
undistr_def_lns _ _ = mzero

-- ** Distl

distl_iso_lns = comp_lns distl_iso_lns'
distl_iso_lns' :: Rule
distl_iso_lns' _ (COMP_LNS _ DISTL_LNS UNDISTL_LNS) =
    success "distl-Iso-Lns" ID_LNS
distl_iso_lns' _ _ = mzero

undistl_iso_lns = comp_lns undistl_iso_lns'
undistl_iso_lns' :: Rule
undistl_iso_lns' _ (COMP_LNS _ UNDISTL_LNS DISTL_LNS) =
    success "undistl-Iso-Lns" ID_LNS
undistl_iso_lns' _ _ = mzero

distl_fst_cancel_lns = comp_lns distl_fst_cancel_lns'
distl_fst_cancel_lns' :: Rule
distl_fst_cancel_lns' (Lns (Prod _ c) _) (COMP_LNS _ (SUMW_LNS (ID `PROD` SND) (ID `PROD` SND) (FST_LNS f) (FST_LNS g)) DISTL_LNS) =
    success "distl-Fst-Cancel-Lns" $ FST_LNS (f \/= g)
distl_fst_cancel_lns' _ _ = mzero

distl_snd_cancel_lns = comp_lns distl_snd_cancel_lns'
distl_snd_cancel_lns' :: Rule
distl_snd_cancel_lns' q@(Lns (Prod (Either a b) c) _) v@(COMP_LNS _ (EITHER_LNS p (SND_LNS f) (SND_LNS g)) DISTL_LNS) = do
    debug "distl-Snd-Cancel-Lns" (Pf q) v
    let h = COMP (Either c c) (f -|-= g) $ (?=) c p
    h' <- PF.optimise_pf (Fun c (Either a b)) h    
    success "distl-Snd-Cancel-Lns" $ SND_LNS h'
distl_snd_cancel_lns' _ _ = mzero

distl_id_cancel_lns = comp_lns distl_id_cancel_lns'
distl_id_cancel_lns' :: Rule
distl_id_cancel_lns' (Lns _ _) (COMP_LNS _ (EITHER_LNS (COMP _ p FST) ID_LNS ID_LNS) DISTL_LNS) = do
    success "distl-Id-Cancel-Lns" $ (EITHER_LNS p ID_LNS ID_LNS) ><<< ID_LNS
distl_id_cancel_lns' _ _ = mzero

distl_fusion_lns = comp_lns distl_fusion_lns'
distl_fusion_lns' :: Rule
distl_fusion_lns' (Lns _ _) (COMP_LNS _ DISTL_LNS (f `PROD_LNS` ID_LNS)) = mzero
distl_fusion_lns' q@(Lns (Prod a c) _) v@(COMP_LNS (Prod (Either a' b') c') DISTL_LNS (l1 `PROD_LNS` l3)) = (do
    let (t,t') = (Either (Prod a' c) (Prod b' c),Prod (Either a' b') c)
    inv (Lns c c') l3
    debug "distl-Fusion-Lns" (Pf q) v
    success "distl-Fusion-Lns" $ COMP_LNS t (ID_LNS ><<< l3 -|-<< ID_LNS ><<< l3) $ COMP_LNS t' DISTL_LNS $ (l1 ><<< ID_LNS))
    `mplus` (do
    debug "distl-Fusion-Lns" (Pf q) v
    let (t,t') = (Either (Prod a' c) (Prod b' c),Prod (Either a' b') c)
        h = COMP (Prod (Prod a' b') (Prod c' c)) (FST ><= putof (Lns c c') l3) distp_pf
        i = COMP (Prod (Prod b' a') (Prod c' c)) (FST ><= putof (Lns c c') l3) distp_pf
    debug "distlFusionH" (Pf $ (Fun (Prod (Prod a' c') (Prod b' c)) (Prod a' c))) h
    h' <- PF.optimise_pf (Fun (Prod (Prod a' c') (Prod b' c)) (Prod a' c)) h
    i' <- PF.optimise_pf (Fun (Prod (Prod b' c') (Prod a' c)) (Prod b' c)) i
    success "distl-Fusion-Lns" $ COMP_LNS t (SUMW_LNS h' i' (ID_LNS ><<< l3) (ID_LNS ><<< l3)) $ COMP_LNS t' DISTL_LNS $ l1 ><<< ID_LNS
    )
distl_fusion_lns' _ _ = mzero

distl_nat_lns = postcomp_lns leftmost_prod_lns distl_nat_lns'
distl_nat_lns' :: Rule
distl_nat_lns' (Lns _ _) (COMP_LNS _ DISTL_LNS (ID_LNS `PROD_LNS` ID_LNS)) = mzero
--distl_nat_lns' (Lns a c) (COMP_LNS b DISTL_LNS (ID_LNS `PROD_LNS` f)) =
--    distl_nat_lns' (Lns a c) (COMP_LNS b DISTL_LNS ((ID_LNS `SUM_LNS` ID_LNS) `PROD_LNS` f))
distl_nat_lns' q@(Lns (Prod (Either a b) c) _) v@(COMP_LNS (Prod (Either a' b') c') DISTL_LNS ((SUM_LNS l1 l2) `PROD_LNS` l3)) = (do
    debug "distl-Nat-Lns" (Pf q) v
    inv (Lns c c') l3
    success "distl-Nat-Lns" $ COMP_LNS (Either (Prod a c) (Prod b c)) ((l1 ><<< l3) -|-<< (l2 ><<< l3)) DISTL_LNS)
    `mplus` (do
    debug "distl-Nat-Lns" (Pf q) v
    let h = COMP (Prod (Prod a' b) (Prod c' c)) (COMP a' (createof (Lns a a') l1) FST ><= (putof (Lns c c') l3)) distp_pf
        i = COMP (Prod (Prod b' a) (Prod c' c)) (COMP b' (createof (Lns b b') l2) FST ><= (putof (Lns c c') l3)) distp_pf
    h' <- PF.optimise_pf (Fun (Prod (Prod a' c') (Prod b c)) (Prod a c)) h
    i' <- PF.optimise_pf (Fun (Prod (Prod b' c') (Prod a c)) (Prod b c)) i
    success "distl-Nat-Lns" $ COMP_LNS (Either (Prod a c) (Prod b c)) (SUMW_LNS h' i' (l1 ><<< l3) (l2 ><<< l3)) DISTL_LNS)
distl_nat_lns' q@(Lns (Prod (Either a b) c) _) v@(COMP_LNS (Prod (Either a' b') c') DISTL_LNS ((SUMW_LNS f g l1 l2) `PROD_LNS` l3)) = do
    debug "distl-Nat-Lns" (Pf q) v
    let h = COMP (Prod (Prod a' b) (Prod c' c)) (f ><= (putof (Lns c c') l3)) distp_pf
        i = COMP (Prod (Prod b' a) (Prod c' c)) (g ><= (putof (Lns c c') l3)) distp_pf
    h' <- PF.optimise_pf (Fun (Prod (Prod a' c') (Prod b c)) (Prod a c)) h
    i' <- PF.optimise_pf (Fun (Prod (Prod b' c') (Prod a c)) (Prod b c)) i
    success "distl-Nat-Lns" $ COMP_LNS (Either (Prod a c) (Prod b c)) (SUMW_LNS h' i' (l1 ><<< l3) (l2 ><<< l3)) DISTL_LNS
distl_nat_lns' _ _ = mzero

distl_sum_nat_lns = comp_lns distl_sum_nat_lns'
distl_sum_nat_lns' :: Rule
distl_sum_nat_lns' (Lns (Prod (Either a b) c) _) (COMP_LNS (Prod (Either d e) f) DISTL_LNS ((EITHER_LNS p l1 l2) `PROD_LNS` l3)) = do
    let (t,t') = (Prod (Either d e) f,Either (Prod a c) (Prod b c))
        p' = COMP (Either d e) p FST
    success "distl-Sum-Nat-Lns" $ COMP_LNS t DISTL_LNS $ COMP_LNS t' (EITHER_LNS p' (l1 ><<< l3) (l2 ><<< l3)) DISTL_LNS
distl_sum_nat_lns' _ _ = mzero

dists :: Rule
dists = top distr_def_lns ||| top undistr_def_lns
    ||| top distl_iso_lns ||| top undistl_iso_lns
    ||| top distl_fst_cancel_lns ||| top distl_snd_cancel_lns ||| top distl_id_cancel_lns