-----------------------------------------------------------------------------
-- |
-- 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

inn_lns' :: Mu a => Ann 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

out_lns' :: Mu a => Ann 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 => Ann (Fix f) -> Lens c a -> Lens (Rep f c) (Rep f a)
fmap_lns f l = Lens get' put' create'
    where get' = fmap f (get l)
          put' = fmap f (put l) . fzip f (create l)
          create' = fmap f (create l)

-- | The @hylo@ recursion pattern as the composition of a lens catamorphism after a lens anamorphism .
hylo_lns :: (Mu b,Fctrable (PF b)) => Ann 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)) => Ann b -> Lens a (F b a) -> Lens a b
ana_lns (b::Ann 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 = ann :: Ann (Fix (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)) => Ann a -> (Lens (F a b) b) -> Lens a b
cata_lns (a::Ann a) l = Lens get' put' create'
    where get' = cata a (get l)
          put' = ana a (fzip f create' . (put l . (id >< fmap f get') /\ snd) . (id >< out))
          create' = ana a (create l)
          f = ann :: Ann (Fix (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)) => Ann 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 => Ann (BFix f) -> Lens c a -> NatLens (BRep f c) (BRep f a)
bmap_lns (f::Ann (BFix f)) l (x::Ann x) = Lens get' put' create'
    where get' = bmap f (get l) idx
          put' = bmap f (put l) idx . bzip x f (create l)
          create' = bmap f (create l) idx
          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))
         => Ann (d a) -> Lens c a -> Lens (d c) (d a)
gmap_lns (da::Ann (d a)) l = cata_lns _L (inn_lns .< (bmap_lns f l) da)
    where f = ann :: Ann (BFix (BF d))