-----------------------------------------------------------------------------
-- |
-- Module      :  Transform.Rules.Lenses.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 lenses involving sums.
--
-----------------------------------------------------------------------------

module Transform.Rules.Lenses.Sums 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(..))

-- ** Sum combinators

sum_functor_id_lns :: Rule
sum_functor_id_lns (Lns _ _) (SUM_LNS ID_LNS ID_LNS) =
    success "sum-Functor-Id-Lns" ID_LNS
sum_functor_id_lns _ _ = mzero

sum_functor_comp_lns = comp_lns sum_functor_comp_lns'
sum_functor_comp_lns' :: Rule
sum_functor_comp_lns' (Lns _ _) (COMP_LNS (Either c d) (f `SUM_LNS` g) (h `SUM_LNS` i)) =
    success "sum-Functor-Comp-Lns" $ (COMP_LNS c f h) `SUM_LNS` (COMP_LNS d g i)
sum_functor_comp_lns' _ _ = mzero

sum_absor_lns = comp_lns sum_absor_lns'
sum_absor_lns' :: Rule
sum_absor_lns' (Lns (Either a b) e) (COMP_LNS (Either c d) (EITHER_LNS p f g) (h `SUM_LNS` i)) =
    success "sum-Absor-Lns" $ EITHER_LNS p (COMP_LNS c f h) (COMP_LNS d g i)
sum_absor_lns' _ _ = mzero

sum_fusion_lns = comp_lns sum_fusion_lns'
sum_fusion_lns' :: Rule
sum_fusion_lns' q@(Lns _ d) v@(COMP_LNS c l1 (EITHER_LNS p l2 l3)) = do
    debug "sum-Fusion-Lns" (Pf q) v
    let p' = COMP c p $ createof (Lns c d) l1
    p'' <- PF.optimise_pf (Fun d (Either One One)) p'
    success "sum-Fusion-Lns" $ EITHER_LNS p'' (COMP_LNS c l1 l2) (COMP_LNS c l1 l3)
sum_fusion_lns' _ _ = mzero

-- ** Lifted sum combinators

sumw_def_lns :: Rule
sumw_def_lns t@(Lns (Either c d) (Either a b)) v@(SUMW_LNS f g l1 l2) = do
    debug "sumw-Def-Lns" (Pf t) v
    proof_strat PF.optimise_pf (Fun (Prod a d) c) f (COMP a (createof (Lns c a) l1) FST)
    proof_strat PF.optimise_pf (Fun (Prod b c) d) g (COMP b (createof (Lns d b) l2) FST)
    success "sumw-Def-Lns" $ SUM_LNS l1 l2
sumw_def_lns _ _ = mzero

sumw_functor_id_lns :: Rule
sumw_functor_id_lns (Lns _ _) (SUMW_LNS _ _ ID_LNS ID_LNS) =
    success "sumw-Functor-Id-Lns" ID_LNS
sumw_functor_id_lns _ _ = mzero

sumw_functor_comp_lns = comp_lns sumw_functor_comp_lns'
sumw_functor_comp_lns' :: Rule
sumw_functor_comp_lns' t@(Lns (Either ta tb) (Either te tf)) v@(COMP_LNS (Either tc td) (SUM_LNS l1 l2) (SUMW_LNS h i l3 l4)) = do
    debug "sumw-Functor-Comp-Lns" (Pf t) v
    let j = COMP (Prod tc tb) h $ ((createof (Lns tc te) l1) ><= ID)
        k = COMP (Prod td ta) i $ ((createof (Lns td tf) l2) ><= ID)
    j' <- PF.optimise_pf (Fun (Prod te tb) ta) j
    k' <- PF.optimise_pf (Fun (Prod tf ta) tb) k
    success "sumw-Functor-Comp" $ SUMW_LNS j' k' (COMP_LNS tc l1 l3) (COMP_LNS td l2 l4)
sumw_functor_comp_lns' t@(Lns (Either ta tb) (Either te tf)) v@(COMP_LNS (Either tc td) (SUMW_LNS f g l1 l2) (SUM_LNS l3 l4)) = do
    debug "sumw-Functor-Comp-Lns" (Pf t) v
    let j = COMP tc (createof (Lns ta tc) l3) $ COMP (Prod te td) f $ ID ><= (getof (Lns tb td) l4)
        k = COMP td (createof (Lns tb td) l4) $ COMP (Prod tf tc) g $ ID ><= (getof (Lns ta tc) l3)
    j' <- PF.optimise_pf (Fun (Prod te tb) ta) j
    k' <- PF.optimise_pf (Fun (Prod tf ta) tb) k
    success "sumw-Functor-Comp" $ SUMW_LNS j' k' (COMP_LNS tc l1 l3) (COMP_LNS td l2 l4)
sumw_functor_comp_lns' t@(Lns (Either ta tb) (Either te tf)) v@(COMP_LNS (Either tc td) (SUMW_LNS f g l1 l2) (SUMW_LNS h i l3 l4)) = do
    debug "sumw-Functor-Comp-Lns" (Pf t) v
    let j = COMP (Prod tc tb) h $ (COMP (Prod te td) f (ID ><= (getof (Lns tb td) l4))) /\= SND
        k = COMP (Prod td ta) i $ (COMP (Prod tf tc) g (ID ><= (getof (Lns ta tc) l3))) /\= SND
    j' <- PF.optimise_pf (Fun (Prod te tb) ta) j
    k' <- PF.optimise_pf (Fun (Prod tf ta) tb) k
    success "sumw-Functor-Comp" $ SUMW_LNS j' k' (COMP_LNS tc l1 l3) (COMP_LNS td l2 l4)
sumw_functor_comp_lns' _ _ = mzero

sumw_absor_lns = comp_lns sumw_absor_lns'
sumw_absor_lns' :: Rule
sumw_absor_lns' (Lns (Either a b) e) (COMP_LNS (Either c d) (EITHER_LNS p f g) (SUMW_LNS x y h i)) =
    success "sumw-Absor-Lns" $ EITHER_LNS p (COMP_LNS c f h) (COMP_LNS d g i)
sumw_absor_lns' _ _ = mzero

-- ** Isomorphisms involving sums

coswap_nat_lns = comp_lns coswap_nat_lns'
coswap_nat_lns' :: Rule
coswap_nat_lns' (Lns (Either a b) _) (COMP_LNS _ COSWAP_LNS (SUM_LNS l1 l2)) = do
    success "coswap-Nat-Lns" $ COMP_LNS (Either b a) (SUM_LNS l2 l1) COSWAP_LNS
coswap_nat_lns' (Lns (Either a b) _) (COMP_LNS _ COSWAP_LNS (SUMW_LNS f g l1 l2)) = do
    success "coswap-Nat-Lns" $ COMP_LNS (Either b a) (SUMW_LNS g f l2 l1) COSWAP_LNS
coswap_nat_lns' _ _ = mzero

coswap_iso_lns = comp_lns coswap_iso_lns'
coswap_iso_lns' :: Rule
coswap_iso_lns' (Lns _ _) (COMP_LNS _ COSWAP_LNS COSWAP_LNS) = do
    success "coswap-Iso-Lns" $ ID_LNS
coswap_iso_lns' _ _ = mzero

coswap_cancel_lns = comp_lns coswap_cancel_lns'
coswap_cancel_lns' :: Rule
coswap_cancel_lns' (Lns _ _) (COMP_LNS _ (EITHER_LNS p l1 l2) COSWAP_LNS) = do
    let p' = COMP (Either One One) COSWAP p
    success "coswap-Cancel-Lns" $ EITHER_LNS p' l2 l1
coswap_cancel_lns' _ _ = mzero

coassocr_nat_lns = postcomp_lns leftmost_sum_lns coassocr_nat_lns'
coassocr_nat_lns' :: Rule
coassocr_nat_lns' (Lns (Either (Either a b) c) _) (COMP_LNS _ COASSOCR_LNS ((f `SUM_LNS` g) `SUM_LNS` h)) = do
    success "coassocr-Nat-Lns" $ COMP_LNS (Either a (Either b c)) (f `SUM_LNS` (g `SUM_LNS` h)) COASSOCR_LNS
coassocr_nat_lns' (Lns _ _) (COMP_LNS _ COASSOCR_LNS (f `SUM_LNS` ID_LNS)) = mzero
coassocr_nat_lns' q@(Lns (Either a b) _) v@(COMP_LNS (Either (Either c d) e) COASSOCR_LNS (f `SUM_LNS` g)) = do
    debug "coassocr-Nat-Lns" (Pf q) v
    let t  = Either c (Either d b)
        t' = Either (Either c d) b
    success "coassocr-Nat-Lns" $ COMP_LNS t (ID_LNS -|-<< (ID_LNS -|-<< g)) $ COMP_LNS t' COASSOCR_LNS (f -|-<< ID_LNS)
coassocr_nat_lns' _ _ = mzero

coassocr_iso_lns = comp_lns coassocr_iso_lns'
coassocr_iso_lns' :: Rule
coassocr_iso_lns' (Lns _ _) (COMP_LNS _ COASSOCR_LNS COASSOCL_LNS) =
    success "coassocr-Iso-Lns" ID_LNS
coassocr_iso_lns' _ _ = mzero

coassocl_nat_lns = postcomp_lns leftmost_sum_lns coassocl_nat_lns'
coassocl_nat_lns' :: Rule
coassocl_nat_lns' (Lns (Either a (Either b c)) _) (COMP_LNS _ COASSOCL_LNS (f `SUM_LNS` (g `SUM_LNS` h))) = do
    success "coassocl-Nat-Lns" $ COMP_LNS (Either (Either a b) c) ((f `SUM_LNS` g) `SUM_LNS` h) COASSOCL_LNS
coassocl_nat_lns' q@(Lns (Either a (Either b c)) _) v@(COMP_LNS (Either a' (Either b' c')) COASSOCL_LNS (f `SUM_LNS` (SUMW_LNS x y g h))) = do
    debug "coassocl-Nat-Lns" (Pf q) v
    let z' = COMP (Either (Prod a' c) (Prod b' c)) ((COMP a' (createof (Lns a a') f) FST) -|-= x) DISTL
        w' = COMP (Either (Prod c' a) (Prod c' b)) ((COMP c' (createof (Lns c c') h) FST) \/=  y) DISTR
    z'' <- PF.optimise_pf (Fun (Prod (Either a' b') c) (Either a b)) z'
    w'' <- PF.optimise_pf (Fun (Prod c' (Either a b)) c) w'
    success "coassocl-Nat-Lns" $ COMP_LNS (Either (Either a b) c) (SUMW_LNS z'' w'' (f `SUM_LNS` g) h) COASSOCL_LNS
coassocl_nat_lns' _ _ = mzero

coassocl_iso_lns = comp_lns coassocl_iso_lns'
coassocl_iso_lns' :: Rule
coassocl_iso_lns' (Lns _ _) (COMP_LNS _ COASSOCL_LNS COASSOCR_LNS) =
    success "coassocl-Iso-Lns" ID_LNS
coassocl_iso_lns' _ _ = mzero

sums :: Rule
sums  = top sum_functor_id_lns ||| top sum_functor_comp_lns ||| top sum_absor_lns
    ||| top sumw_functor_id_lns ||| top sumw_absor_lns
    ||| top coswap_nat_lns ||| top coswap_iso_lns ||| top coswap_cancel_lns
    ||| top coassocr_nat_lns ||| top coassocr_iso_lns ||| top coassocl_nat_lns ||| top coassocl_iso_lns