-----------------------------------------------------------------------------
-- |
-- 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.Pf
import Data.Equal
import Data.Lens
import Transform.Rewriting
import {-# SOURCE #-} qualified Transform.Rules.PF as PF
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 Prelude hiding (Functor(..))
import Control.Monad.RWS hiding (Functor(..))

import Generics.Pointless.Lenses

-- * Strategies

optimise_all_lns :: Rule
optimise_all_lns = optimise_lns >>> optimise_list_lns

optimise_list_lns :: Rule
optimise_list_lns = outermost listrules >>> optimise_lns >>> try (once listfuse >>> optimise_list_lns)
    where listrules, listfuse :: Rule
          listrules = top list_cata_cancel_lns ||| top list_ana_cancel_lns
          listfuse = top list_cata_fusion_lns ||| top list_ana_fusion_lns ||| list_hylo_fusion_lns

optimise_lns :: Rule
optimise_lns = outermost rules >>> try ((once fuse1 ||| once fuse2 ||| once fuse3 ||| once fuse4) >>> optimise_lns)
    where rules, fuse1, fuse2, fuse3, fuse4 :: Rule
          rules = primitives ||| prods ||| sums ||| lists ||| bangs ||| convs ||| dists ||| recs
          fuse1 = top cata_fusion_lns ||| top ana_fusion_lns
          fuse2 = top distl_fusion_lns ||| top distl_nat_lns ||| top distl_sum_nat_lns
          fuse3 = top hylo_id_lns ||| top hylo_shift_lns
          fuse4 = top sum_fusion_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" }