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

module Transform.Rules.Lenses.Products where

import Data.Type
import Data.Pf
import Data.Lens
import Data.Equal
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(..))

-- ** Product combinators

prod_functor_id_lns :: Rule
prod_functor_id_lns _ (PROD_LNS ID_LNS ID_LNS) =
    success "prod-Functor-Id-Lns" ID_LNS
prod_functor_id_lns _ _ = mzero

prod_functor_comp_lns = comp_lns prod_functor_comp_lns'
prod_functor_comp_lns' :: Rule
prod_functor_comp_lns' (Lns _ _) (COMP_LNS (Prod c d) (f `PROD_LNS` g) (h `PROD_LNS` i)) =
    success "prod-Functor-Comp-Lns" $ (COMP_LNS c f h) `PROD_LNS` (COMP_LNS d g i)
prod_functor_comp_lns' _ _ = mzero

fst_nat_lns = comp_lns fst_nat_lns'
fst_nat_lns' :: Rule
fst_nat_lns' q@(Lns (Prod c d) _ ) v@(COMP_LNS (Prod a b) (FST_LNS f) (l1 `PROD_LNS` l2)) = do
    debug "fst-Nat-Lns" (Pf q) v
    let g = COMP b (createof (Lns d b) l2) $ COMP a f (getof (Lns c a) l1)
    g' <- PF.optimise_pf (Fun c d) g
    success "fst-Nat-Lns" $ COMP_LNS c l1 $ FST_LNS g'
fst_nat_lns' _ _ = mzero

snd_nat_lns = comp_lns snd_nat_lns'
snd_nat_lns' :: Rule
snd_nat_lns' q@(Lns (Prod c d) _ ) v@(COMP_LNS (Prod a b) (SND_LNS f) (l1 `PROD_LNS` l2)) = do
    debug "Snd-Nat-Lns" (Pf q) v
    let g = COMP a (createof (Lns c a) l1) $ COMP b f (getof (Lns d b) l2)
    g' <- PF.optimise_pf (Fun d c) g
    success "snd-Nat-Lns" $ COMP_LNS d l2 $ SND_LNS g'
snd_nat_lns' _ _ = mzero
    
-- ** Isomorphisms involving products

bangl_cancel_lns = comp_lns bangl_cancel_lns'
bangl_cancel_lns' :: Rule
bangl_cancel_lns' (Lns _ _) (COMP_LNS _ (SND_LNS f) BANGL_LNS) =
    success "bangl-Cancel-Lns" ID_LNS
bangl_cancel_lns' _ _ = mzero
    
bangr_cancel_lns = comp_lns bangr_cancel_lns'
bangr_cancel_lns' :: Rule
bangr_cancel_lns' (Lns _ _) (COMP_LNS _ (FST_LNS f) BANGR_LNS) =
    success "bangr-Cancel-Lns" ID_LNS
bangr_cancel_lns' _ _ = mzero

swap_nat_lns = comp_lns swap_nat_lns'
swap_nat_lns' :: Rule
swap_nat_lns' (Lns (Prod a b) _) (COMP_LNS _ SWAP_LNS (PROD_LNS f g)) =
    success "swap-Nat-Lns" $ COMP_LNS (Prod b a) (g `PROD_LNS` f) SWAP_LNS
swap_nat_lns' _ _ = mzero

swap_iso_lns = comp_lns swap_iso_lns'
swap_iso_lns' :: Rule
swap_iso_lns' (Lns _ _) (COMP_LNS _ SWAP_LNS SWAP_LNS) =
    success "swap-Iso-Lns" ID_LNS
swap_iso_lns' _ _ = mzero

swap_cancel_lns = comp_lns swap_cancel_lns'
swap_cancel_lns' :: Rule
swap_cancel_lns' (Lns _ _) (COMP_LNS _ (FST_LNS f) SWAP_LNS) = 
    success "swap-Cancel-Lns" $ SND_LNS f
swap_cancel_lns' (Lns _ _) (COMP_LNS _ (SND_LNS f) SWAP_LNS) = 
    success "swap-Cancel-Lns" $ FST_LNS f
swap_cancel_lns' _ _ = mzero

assocr_nat_lns = comp_lns assocr_nat_lns'
assocr_nat_lns' :: Rule
assocr_nat_lns' (Lns _ (Prod a (Prod b c))) (COMP_LNS _ (f `PROD_LNS` (g `PROD_LNS` h)) ASSOCR_LNS) =
    success "assocr-Nat-Lns" $ COMP_LNS (Prod (Prod a b) c) ASSOCR_LNS $ (f ><<< g) ><<< h
assocr_nat_lns' _ _ = mzero

assocr_iso_lns = comp_lns assocr_iso_lns'
assocr_iso_lns' :: Rule
assocr_iso_lns' (Lns _ _) (COMP_LNS _ ASSOCR_LNS ASSOCL_LNS) =
    success "assocr-Iso-Lns" ID_LNS
assocr_iso_lns' _ _ = mzero

assocr_fst_cancel_lns = comp_lns assocr_fst_cancel_lns'
assocr_fst_cancel_lns' :: Rule
assocr_fst_cancel_lns' q@(Lns _ _) v@(COMP_LNS (Prod a (Prod b c)) (FST_LNS f) ASSOCR_LNS) = do
    debug "assocr-Fst-Cancel-Lns" (Pf q) v
    let h = COMP (Prod b c) SND $ COMP a f FST
        g = COMP (Prod b c) FST f
    h' <- PF.optimise_pf (Fun (Prod a b) c) h
    g' <- PF.optimise_pf (Fun a b) g
    success "assocr-Fst-Cancel-Lns" $ COMP_LNS (Prod a b) (FST_LNS g') (FST_LNS h')
assocr_fst_cancel_lns' (Lns _ _) (COMP_LNS (Prod a (Prod b c)) (ID_LNS `PROD_LNS` (FST_LNS f)) ASSOCR_LNS) = do
    let g = COMP b f SND
    success "assocr-Fst-Cancel-Lns" $ FST_LNS g
assocr_fst_cancel_lns' _ _ = mzero

assocr_snd_cancel_lns = comp_lns assocr_snd_cancel_lns'
assocr_snd_cancel_lns' :: Rule
assocr_snd_cancel_lns' (Lns _ _) (COMP_LNS _ (SND_LNS (COMP _ g FST)) ASSOCR_LNS) =
    success "assocr-Snd-Cancel-Lns" $ (SND_LNS g) ><<< ID_LNS
assocr_snd_cancel_lns' (Lns _ _) (COMP_LNS (Prod a (Prod b c)) (ID_LNS `PROD_LNS` (SND_LNS (COMP _ f BANG))) ASSOCR_LNS) = do
    let g = COMP One f BANG
    success "assocr-Snd-Cancel-Lns" $ (FST_LNS g) ><<< ID_LNS
assocr_snd_cancel_lns' (Lns _ _) (COMP_LNS (Prod a (Prod b c)) (ID_LNS `PROD_LNS` (SND_LNS f)) ASSOCR_LNS) = do
    Eq <- teq c a
    success "assocr-Snd-Cancel-Lns" $ (FST_LNS f) ><<< ID_LNS
assocr_snd_cancel_lns' _ _ = mzero

assocl_nat_lns = comp_lns assocl_nat_lns'
assocl_nat_lns' :: Rule
assocl_nat_lns' (Lns _ (Prod (Prod a b) c)) (COMP_LNS _ ((f `PROD_LNS` g) `PROD_LNS` h) ASSOCL_LNS) =
    success "assocl-Nat-Lns" $ COMP_LNS (Prod a (Prod b c)) ASSOCL_LNS $ f ><<< (g ><<< h)
assocl_nat_lns' _ _ = mzero

assocl_iso_lns = comp_lns assocl_iso_lns'
assocl_iso_lns' :: Rule
assocl_iso_lns' (Lns _ _) (COMP_LNS _ ASSOCL_LNS ASSOCR_LNS) =
    success "assocl-Iso-Lns" ID_LNS
assocl_iso_lns' _ _ = mzero

assocl_fst_cancel_lns = comp_lns assocl_fst_cancel_lns'
assocl_fst_cancel_lns' :: Rule
assocl_fst_cancel_lns' (Lns _ _) (COMP_LNS _ (FST_LNS (COMP _ g SND)) ASSOCL_LNS) =
    success "assocl-Fst-Cancel-Lns" $ ID_LNS ><<< FST_LNS g
assocl_fst_cancel_lns' (Lns _ _) (COMP_LNS _ ((FST_LNS (COMP _ f BANG)) `PROD_LNS` ID_LNS) ASSOCL_LNS) = do
    let g = COMP One f BANG
    success "assocl-Fst-Cancel-Lns" $ ID_LNS ><<< SND_LNS g
assocl_fst_cancel_lns' (Lns _ _) (COMP_LNS (Prod (Prod a b) c) ((FST_LNS f) `PROD_LNS` ID_LNS) ASSOCL_LNS) = do
    Eq <- teq a c
    success "assocl-Fst-Cancel-Lns" $ ID_LNS ><<< SND_LNS f
assocl_fst_cancel_lns' _ _ = mzero

assocl_snd_cancel_lns = comp_lns assocl_snd_cancel_lns'
assocl_snd_cancel_lns' :: Rule
assocl_snd_cancel_lns' q@(Lns _ _) v@(COMP_LNS (Prod (Prod a b) c) (SND_LNS f) ASSOCL_LNS) = do
    debug "assocl-Snd-Cancel-Lns" (Pf q) v
    let h = COMP (Prod a b) FST $ COMP c f SND
        g = COMP (Prod a b) SND f
    h' <- PF.optimise_pf (Fun (Prod b c) a) h
    g' <- PF.optimise_pf (Fun c b) g
    success "assocl-Snd-Cancel-Lns" $ COMP_LNS (Prod b c) (SND_LNS g') (SND_LNS h')
assocl_snd_cancel_lns' (Lns _ _) (COMP_LNS (Prod (Prod a b) c) ((SND_LNS f) `PROD_LNS` ID_LNS) ASSOCL_LNS) = do
    let g = COMP b f FST
    success "assocl-Snd-Cancel-Lns" $ SND_LNS g
assocl_snd_cancel_lns' _ _ = mzero

prods :: Rule
prods = top prod_functor_id_lns ||| top prod_functor_comp_lns
    ||| top fst_nat_lns ||| top snd_nat_lns ||| top bangl_cancel_lns ||| top bangr_cancel_lns
    ||| top swap_nat_lns ||| top swap_iso_lns ||| top swap_cancel_lns
    ||| top assocr_nat_lns ||| top assocr_iso_lns ||| top assocr_fst_cancel_lns ||| top assocr_snd_cancel_lns
    ||| top assocl_nat_lns ||| top assocl_iso_lns ||| top assocl_fst_cancel_lns ||| assocl_snd_cancel_lns