-----------------------------------------------------------------------------
-- |
-- Module      :  Transform.Rules.Lenses
-- 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
-- 
-- Generic strategy for the rewriting of point-free lenses.
--
-----------------------------------------------------------------------------

module Transform.Rules.Lenses where

import Data.Type
import Data.Equal
import Data.Lens
import Transform.Rewriting
import Transform.Rules.Lenses.Combinators
import Transform.Rules.Lenses.Products
import Transform.Rules.Lenses.Sums
import Transform.Rules.Lenses.Dists
import Transform.Rules.Lenses.Rec
import Transform.Rules.Lenses.Lists
import {-# SOURCE #-} qualified Transform.Rules.PF as PF

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

import Generics.Pointless.Lenses

-- * Strategies

optimise_lns :: Rule
optimise_lns = step1
    where
    step1, right, rules, prot, undef, prods, sums, bangs, dists, convs, recs, lists, fuse :: Rule
    step1 = outermost (top comp_assocr_lns ||| rules) >>> right >>> try (once fuse >>> optimise_lns)
    right = many (once (top comp_assocr_lns))
    rules = top nat_id_lns ||| prot ||| undef ||| prods ||| sums ||| bangs ||| dists ||| convs ||| lists ||| recs
    prot  = top unprotect_lns
    undef = top top_fusion_lns
    prods = top prod_functor_id_lns ||| top prod_functor_comp_lns
        ||| top fst_nat_lns ||| top snd_nat_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 ||| top assocl_snd_cancel_lns
        ||| top bangl_cancel_lns ||| top bangr_cancel_lns
    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
    bangs = top bang_reflex_lns ||| top bang_fusion_lns ||| top bang_uniq_lns
    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
    convs = top rconv_cancel_lns ||| top lconv_cancel_lns ||| top conv_conv_lns ||| top conv_iso_lns
        ||| top conv_comp_lns ||| top conv_prod_lns ||| top conv_sum_lns
    recs  = top in_iso_lns ||| top out_iso_lns
        ||| top functor_id_lns ||| top functor_comp_lns ||| top functor_def_lns
        ||| top cata_reflex_lns ||| top cata_cancel_lns
        ||| top ana_reflex_lns ||| top ana_cancel_lns
    lists = top map_id_lns ||| top map_fusion_lns ||| top map_cat_lns ||| top map_concat_lns
        ||| top filter_cat_lns ||| top filter_map_lns ||| top filter_concat_lns
        ||| top sum_cat_lns ||| top sum_concat_lns
        ||| top length_cat_lns ||| top length_map_lns ||| top length_concat_lns
        ||| top cata_map_fusion_lns ||| top ana_map_fusion_lns
    fuse  = top sum_fusion_lns ||| top distl_fusion_lns ||| top distl_nat_lns ||| top distl_sum_nat_lns
        ||| top hylo_id_lns ||| top cata_fusion_lns ||| top ana_fusion_lns
        ||| top hylo_shift_lns
        ||| {-top sumw_def_lns ||| -}top sumw_functor_comp_lns

-- * Proofs

proveLns :: Type (Lens c a) -> Pf (Lens c a) -> IO ()
proveLns t@(Lns c a) l = do
    putStr "Proving CreateGet"
    eq1 <- reduceIO PF.optimise_pf (Fun a a) (COMP c (getof t l) (createof t l))
    print $ geq (Pf $ Fun a a) eq1 ID
    putStr "Proving PutGet"
    eq2 <- reduceIO PF.optimise_pf (Fun (Prod a c) a) (COMP c (getof t l) (putof t l))
    print $ geq (Pf $ Fun (Prod a c) a) eq2 FST
    putStr "Proving GetPut"
    eq3 <- reduceIO PF.optimise_pf (Fun c c) (COMP (Prod a c) (putof t l) ((getof t l) /\= ID))
    print $ geq (Pf $ Fun c c) eq3 ID

proveLnsRule :: Type (Lens c a) -> Pf (Lens c a) -> Rule -> IO ()
proveLnsRule t@(Lns c a) l r = case (evalRWST (r t l) [0] (Dyn (Pf t) l)) of
    { Just (l',_)   -> do
                        putStr "Proving get: \n"
                        getl <- reduceIO PF.optimise_pf (Fun c a) $ getof t l
                        putStrLn "="
                        getl' <- reduceIO PF.optimise_pf (Fun c a) $ getof t l'
                        print $ geq (Pf $ Fun c a) getl getl'
                        putStr "Proving create: \n"
                        createl <- reduceIO PF.optimise_pf (Fun a c) $ createof t l
                        putStrLn "="
                        createl' <- reduceIO PF.optimise_pf (Fun a c) $ createof t l'
                        print $ geq (Pf $ Fun a c) createl createl'
                        putStr "Proving put: \n"
                        putl <- writeIO "put.txt" nop (Fun (Prod a c) c) $ putof t l
                        putStrLn "="
                        putl' <- writeIO "put2.txt" nop (Fun (Prod a c) c) $ putof t l'
                        print $ geq (Pf $ Fun (Prod a c) c) putl putl'
    ; otherwise -> putStrLn "non-matching rule" }