-----------------------------------------------------------------------------
-- |
-- Module      :  Transform.Rules.Lenses.Combinators
-- 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.
--
-----------------------------------------------------------------------------

module Transform.Rules.Lenses.Combinators where

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

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

-- ** Combinators

-- | Applies a rule inside a composition
comp_lns :: Rule -> Rule
comp_lns r (Lns d a) (COMP_LNS b f (COMP_LNS c g h)) = do
    fg <- r (Lns c a) (COMP_LNS b f g)
    return $ COMP_LNS c fg h
comp_lns r (Lns d a) (COMP_LNS c (COMP_LNS b f g) h) = do
    gh <- r (Lns d b) (COMP_LNS c g h)
    return $ COMP_LNS b f gh
comp_lns r t f = r t f

-- | Applies a rule to the left of a composition
comp1_lns :: Rule -> Rule
comp1_lns r (Lns a c) (COMP_LNS b f g) = do
    f' <- r (Lns b c) f
    return $ COMP_LNS b f' g
comp1_lns _ _ _ = mzero

-- | Applies a rule to the right of a composition
comp2_lns :: Rule -> Rule
comp2_lns r (Lns a c) (COMP_LNS b f g) = do
    g' <- r (Lns a b) g
    return $ COMP_LNS b f g'
comp2_lns _ _ _ = mzero

prod1_lns :: Rule -> Rule
prod1_lns r (Lns (Prod a b) (Prod c d)) (f `PROD_LNS` g) = do
    f' <- r (Lns a c) f
    return $ f' `PROD_LNS` g
prod1_lns _ _ _ = mzero

prod2_lns :: Rule -> Rule
prod2_lns r (Lns (Prod a b) (Prod c d)) (f `PROD_LNS` g) = do
    g' <- r (Lns b d) g
    return $ f `PROD_LNS` g'
prod2_lns _ _ _ = mzero

sum1_lns :: Rule -> Rule
sum1_lns r (Lns (Either a b) (Either c d)) (f `SUM_LNS` g) = do
    f' <- r (Lns a c) f
    return $ f' `SUM_LNS` g
sum1_lns r (Lns (Either a b) (Either c d)) (SUMW_LNS f g l1 l2) = do
    l1' <- r (Lns a c) l1
    return $ SUMW_LNS f g l1' l2
sum1_lns _ _ _ = mzero

sum2_lns :: Rule -> Rule
sum2_lns r (Lns (Either a b) (Either c d)) (f `SUM_LNS` g) = do
    g' <- r (Lns b d) g
    return $ f `SUM_LNS` g'
sum2_lns r (Lns (Either a b) (Either c d)) (SUMW_LNS f g l1 l2) = do
    l2' <- r (Lns b d) l2
    return $ SUMW_LNS f g l1 l2'
sum2_lns _ _ _ = mzero

-- | Rearranges the left of a composition before applying a rule
precomp_lns :: Rule -> Rule -> Rule
precomp_lns r1 r2 = comp_lns $ r2 ||| (comp1_lns r1 >>> comp_assocr_lns >>> comp2_lns r2)

-- | Rearranges the right of a composition before applying a rule
postcomp_lns :: Rule -> Rule -> Rule
postcomp_lns r1 r2 = comp_lns $ r2 ||| (comp2_lns r1 >>> comp_assocl_lns >>> comp1_lns r2)

-- | Extracts the leftmost element of a nested composition
leftmost_lns :: Rule
leftmost_lns (Lns a c) (COMP_LNS b f g) = do
    f' <- leftmost_lns' (Lns b c) f
    try comp_assocr_lns (Lns a c) $ COMP_LNS b f' g
leftmost_lns (Lns a c) f =
    return $ COMP_LNS a f ID_LNS
leftmost_lns _ _ = mzero
leftmost_lns' :: Rule
leftmost_lns' (Lns a c) (COMP_LNS b f g) = do
    f' <- leftmost_lns' (Lns b c) f
    try comp_assocr_lns (Lns a c) $ COMP_LNS b f' g
leftmost_lns' (Lns a c) f = return f
leftmost_lns' _ _ = mzero

-- | Extracts the rightmost element of a nested composition
rightmost_lns :: Rule
rightmost_lns (Lns a c) (COMP_LNS b f g) = do
    g' <- rightmost_lns' (Lns a b) g
    try comp_assocl_lns (Lns a c) $ COMP_LNS b f g'
rightmost_lns (Lns a c) f =
    return $ COMP_LNS c ID_LNS f
rightmost_lns _ _ = mzero
rightmost_lns' :: Rule
rightmost_lns' (Lns a c) (COMP_LNS b f g) = do
    g' <- rightmost_lns' (Lns a b) g
    try comp_assocl_lns (Lns a c) $ COMP_LNS b f g'
rightmost_lns' (Lns a c) f = return f
rightmost_lns' _ _ = mzero

leftmost_sum_lns :: Rule
leftmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS ID_LNS ID_LNS) = mzero
leftmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS ID_LNS g) = do
    COMP_LNS y g' g'' <- leftmost_lns' (Lns b d) g
    return $ COMP_LNS (Either a y) (ID_LNS -|-<< g') (ID_LNS -|-<< g'')
leftmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS f ID_LNS) = do
    COMP_LNS x f' f'' <- leftmost_lns' (Lns a c) f
    return $ COMP_LNS (Either x b) (f' -|-<< ID_LNS) (f'' -|-<< ID_LNS)
leftmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS f g) = do
    COMP_LNS x f' f'' <- leftmost_lns' (Lns a c) f
    COMP_LNS y g' g'' <- leftmost_lns' (Lns b d) g
    return $ COMP_LNS (Either x y) (f' -|-<< g') (f'' -|-<< g'')
leftmost_sum_lns _ _ = mzero

rightmost_sum_lns :: Rule
rightmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS ID_LNS ID_LNS) = mzero
rightmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS ID_LNS g) = do
    COMP_LNS y g' g'' <- rightmost_lns' (Lns b d) g
    return $ COMP_LNS (Either a y) (ID_LNS -|-<< g') (ID_LNS -|-<< g'')
rightmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS f ID_LNS) = do
    COMP_LNS x f' f'' <- rightmost_lns' (Lns a c) f
    return $ COMP_LNS (Either x b) (f' -|-<< ID_LNS) (f'' -|-<< ID_LNS)
rightmost_sum_lns (Lns (Either a b) (Either c d)) (SUM_LNS f g) = do
    COMP_LNS x f' f'' <- rightmost_lns' (Lns a c) f
    COMP_LNS y g' g'' <- rightmost_lns' (Lns b d) g
    return $ COMP_LNS (Either x y) (f' -|-<< g') (f'' -|-<< g'')
rightmost_sum_lns _ _ = mzero

leftmost_prod_lns :: Rule
leftmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS ID_LNS ID_LNS) = mzero
leftmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS ID_LNS g) = do
    COMP_LNS y g' g'' <- leftmost_lns' (Lns b d) g
    return $ COMP_LNS (Prod a y) (ID_LNS ><<< g') (ID_LNS ><<< g'')
leftmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS f ID_LNS) = do
    COMP_LNS x f' f'' <- leftmost_lns' (Lns a c) f
    return $ COMP_LNS (Prod x b) (f' ><<< ID_LNS) (f'' ><<< ID_LNS)
leftmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS f g) = do
    COMP_LNS x f' f'' <- leftmost_lns' (Lns a c) f
    COMP_LNS y g' g'' <- leftmost_lns' (Lns b d) g
    return $ COMP_LNS (Prod x y) (f' ><<< g') (f'' ><<< g'')
leftmost_prod_lns _ _ = mzero

rightmost_prod_lns :: Rule
rightmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS ID_LNS ID_LNS) = mzero
rightmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS ID_LNS g) = do
    COMP_LNS y g' g'' <- rightmost_lns' (Lns b d) g
    return $ COMP_LNS (Prod a y) (ID_LNS ><<< g') (ID_LNS ><<< g'')
rightmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS f ID_LNS) = do
    COMP_LNS x f' f'' <- rightmost_lns' (Lns a c) f
    return $ COMP_LNS (Prod x b) (f' ><<< ID_LNS) (f'' ><<< ID_LNS)
rightmost_prod_lns (Lns (Prod a b) (Prod c d)) (PROD_LNS f g) = do
    COMP_LNS x f' f'' <- rightmost_lns' (Lns a c) f
    COMP_LNS y g' g'' <- rightmost_lns' (Lns b d) g
    return $ COMP_LNS (Prod x y) (f' ><<< g') (f'' ><<< g'')
rightmost_prod_lns _ _ = mzero

-- ** Identity and Composition

nat_id_lns = comp_lns nat_id_lns'
nat_id_lns' :: Rule
nat_id_lns' (Lns _ _) (COMP_LNS _ f ID_LNS) =
    return f
nat_id_lns' (Lns _ _) (COMP_LNS _ ID_LNS f) =
    return f
nat_id_lns' _ _ = mzero

comp_assocr_lns :: Rule
comp_assocr_lns _ (COMP_LNS a (COMP_LNS b l1 l2) l3) =
    return $ COMP_LNS b l1 (COMP_LNS a l2 l3)
comp_assocr_lns _ _ = mzero

comp_assocl_lns :: Rule
comp_assocl_lns _ (COMP_LNS a l1 (COMP_LNS b l2 l3)) =
    return $ COMP_LNS b (COMP_LNS a l1 l2) l3
comp_assocl_lns _ _ = mzero

-- ** Bangs

bang_reflex_lns :: Rule
bang_reflex_lns (Lns One One) (BANG_LNS f) =
    success "bang-Reflex-Lns" ID_LNS
bang_reflex_lns _ _ = mzero

bang_fusion_lns = comp_lns bang_fusion_lns'
bang_fusion_lns' :: Rule
bang_fusion_lns' t@(Lns a One) v@(COMP_LNS b (BANG_LNS f) l1) = do
    debug "bang-Fusion-Lns" (Pf t) v
    g <- PF.optimise_pf (Fun One a) $ COMP b (createof (Lns a b) l1) f
    success "bang-Fusion-Lns" $ BANG_LNS g
bang_fusion_lns' _ _ = mzero

bang_uniq_lns :: Rule
bang_uniq_lns (Lns _ _) ID_LNS = mzero
bang_uniq_lns (Lns _ _) (BANG_LNS _) = mzero
bang_uniq_lns t@(Lns a One) l1 = do
    debug "bang-Uniq-Lns" (Pf t) l1
    g <- PF.optimise_pf (Fun One a) $ createof (Lns a One) l1
    success "bang-Uniq-Lns" $ BANG_LNS g
bang_uniq_lns _ _ = mzero

-- ** Backtracking sums and products

sum_unreflex_lns :: Rule
sum_unreflex_lns (Lns (Either a b) (Either c d)) ID_LNS =
    success "sum-UnReflex-Lns" $ ID_LNS -|-<< ID_LNS
sum_unreflex_lns _ _ = mzero

-- ** Tops and Bottoms

top_fusion_lns = comp_lns top_fusion_lns'
top_fusion_lns' :: Rule
top_fusion_lns' (Lns _ _) (COMP_LNS _ TOP f) =
    success "top-Fusion-Lns" TOP
top_fusion_lns' (Lns _ _) (COMP_LNS _ f TOP) =
    success "top-Fusion-Lns" TOP
top_fusion_lns' _ _ = mzero

primitives :: Rule
primitives = top comp_assocr_lns ||| top nat_id_lns ||| top top_fusion_lns

bangs :: Rule
bangs = top bang_reflex_lns ||| top bang_fusion_lns ||| top bang_uniq_lns