-----------------------------------------------------------------------------
-- |
-- Module      :  Generics.Pointless.Lenses.RecursionPatterns
-- Copyright   :  (c) 2009 University of Minho
-- License     :  BSD3
--
-- Maintainer  :  hpacheco@di.uminho.pt
-- Stability   :  experimental
-- Portability :  non-portable
--
-- Pointless Lenses:
-- bidirectional lenses with point-free programming
-- 
-- This module provides catamorphism and anamorphism bidirectional combinators for the definition of recursive lenses.
--
-----------------------------------------------------------------------------

module Generics.Pointless.Lenses.RecursionPatterns where

import Prelude hiding (Functor(..),fmap)

import Generics.Pointless.Combinators
import Generics.Pointless.Functors
import Generics.Pointless.Fctrable
import Generics.Pointless.Bifunctors
import Generics.Pointless.Bifctrable
import Generics.Pointless.RecursionPatterns
import Generics.Pointless.Lenses
import Generics.Pointless.Lenses.Combinators

-- | The @inn@ point-free combinator.
inn_lns :: Mu a => Lens (F a a) a
inn_lns = Lens inn (out . fst) out

-- | The @out@ point-free combinator.
out_lns :: Mu a => Lens a (F a a)
out_lns = Lens out (inn . fst) inn

-- | The functor mapping function @fmap@ as a lens.
fmap_lns :: Fctrable f => Fix f -> Lens c a -> Lens (Rep f c) (Rep f a)
fmap_lns (f::Fix f) l = Lens get' put' create'
    where get' = fmap f (get l)
          put' = fmap f (put l) . fzip (fctr :: Fctr f) (create l)
          create' = fmap f (create l)

-- | The polytypic functor zipping combinator.
-- Gives preference to the abstract (first) F-structure.
fzip :: Fctr f -> (a -> c) -> (Rep f a,Rep f c) -> Rep f (a,c)
fzip I create = id
fzip K create = fst
fzip (f :*!: g) create = (fzip f create >< fzip g create) . distp
fzip (f :+!: g) create = (l -|- r) . dists
    where l = fzip f create \/ fmap (fixF f) (id /\ create) . fst
          r = fmap (fixF g) (id /\ create) . fst \/ fzip g create

-- | The @hylo@ recursion pattern as the composition of a lens catamorphism after a lens anamorphism .
hylo_lns :: (Mu b,Fctrable (PF b)) => b -> Lens (F b c) c -> Lens a (F b a) -> Lens a c
hylo_lns b g h = cata_lns b g .< ana_lns b h

-- | The @ana@ recursion pattern as a lens.
-- For @ana_lns@ to be a well-behaved lens, we MUST prove termination of |get| for each instance.
ana_lns :: (Mu b,Fctrable (PF b)) => b -> Lens a (F b a) -> Lens a b
ana_lns (b::b) l = Lens get' put' create'
    where get' = ana b (get l)
          put' = accum b  (put l) (fzip g create' . (id >< get l))
          create' = cata b (create l)
          g = fctr :: Fctr (PF b)

-- | The @cata@ recursion pattern as a lens.
-- For @cata_lns@ to be a well-behaved lens, we MUST prove termination of |put| and |create| for each instance.
cata_lns :: (Mu a,Fctrable (PF a)) => a -> (Lens (F a b) b) -> Lens a b
cata_lns (a::a) l = Lens get' put' create'
    where get' = cata a (get l)
          put' = ana a (fzip f create' . (put l . (id >< fmap (fixF f) get') /\ snd) . (id >< out))
          create' = ana a (create l)
          f = fctr :: Fctr (PF a)

-- | The recursion pattern for recursive functions that can be expressed both as anamorphisms and catamorphisms.
-- Proofs of termination are dismissed.
nat_lns :: (Mu a,Mu b,Fctrable (PF b)) => a -> NatLens (PF a) (PF b) -> Lens a b
nat_lns a l = ana_lns _L (l a .< out_lns)

binn_lns :: Bimu d => Lens (B d a (d a)) (d a)
binn_lns = Lens binn (bout . fst) bout

bout_lns :: Bimu d => Lens (d a) (B d a (d a))
bout_lns = Lens bout (binn . fst) binn

-- | The bifunctor mapping function @bmap@ as a lens.
bmap_lns :: Bifctrable f => BFix f -> Lens c a -> NatLens (BRep f c) (BRep f a)
bmap_lns (f::BFix f) l (x::x) = Lens get' put' create'
    where get' = bmap f (get l) idx
          put' = bmap f (put l) idx . bzip x (bctr :: Bifctr f) (create l)
          create' = bmap f (create l) idx
          idx = id :: x -> x

-- | The polytypic bifunctor zipping combinator.
-- Just maps over the polymorphic parameter. To map over the recursive parameter we can use @fzip@.
bzip :: x -> Bifctr f -> (a -> c) -> (Rep (BRep f a) x,Rep (BRep f c) x) -> Rep (BRep f (a,c)) x
bzip x BI create = fst
bzip x BP create = id
bzip x BK create = fst
bzip x (f :*!| g) create = (bzip x f create >< bzip x g create) . distp
bzip (x::x) (f :+!| g) create = (l -|- r) . dists
    where l = bzip x f create \/ bmap (fixB f) (id /\ create) idx . fst
          r = bmap (fixB g) (id /\ create) idx . fst \/ bzip x g create
          idx = id :: x -> x

-- | Generic mapping lens for parametric types with one polymorphic parameter.
-- Cannot be defined using @nat_lns@ because of the required equality constraints between functors and bifunctors.
-- This could, however, be overcome by defining specific recursive combinators for bifunctors.
gmap_lns :: (Mu (d c),Mu (d a),Fctrable (PF (d c)),Bifctrable (BF d),
             F (d a) (d a) ~ B d a (d a),
             F (d c) (d a) ~ B d c (d a))
         => d a -> Lens c a -> Lens (d c) (d a)
gmap_lns (da::d a) l = cata_lns _L (inn_lns .< (bmap_lns (fixB f) l) da)
    where f = bctr :: Bifctr (BF d)