-----------------------------------------------------------------------------
-- |
-- Module      :  Generics.Pointless.Lenses.Reader.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.
-- The implementations use a monad reader so that each lens combinator permits a more flexible environment.
--
-----------------------------------------------------------------------------

module Generics.Pointless.Lenses.Reader.RecursionPatterns where

import Prelude hiding (Functor(..),fmap)
import Control.Monad hiding (Functor(..),fmap)
import Control.Monad.Instances hiding (Functor(..),fmap)
import Generics.Pointless.Combinators
import Generics.Pointless.MonadCombinators
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
import Generics.Pointless.Lenses.RecursionPatterns

-- | The functor mapping function @fmap@ as a more relaxed lens.
-- The extra function allows user-defined behavior when creating default concrete F-values.
fmap_lns' :: Fctrable f => Fix f -> ((a,Rep f c) -> c) -> Lens c a -> Lens (Rep f c) (Rep f a)
fmap_lns' (f::Fix f) h l = Lens get' put' create'
    where get' = fmap f (get l)
          put' = fmap f (put l) . uncurry (fzip' (fctr :: Fctr f) h) . (id /\ snd)
          create' = fmap f (create l)

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

-- | The polytypic auxiliary function for @fzip'@.
-- Similar to @fmap (id /\ create)@ but using a monad reader for the concrete reconstruction function.
fcre' :: Fctr f -> ((a,e) -> c) -> Rep f a -> (e -> Rep f (a,c))
fcre' I create = return /|\ curry create
fcre' K create = return
fcre' (f :*!: g) create = fcre' f create >|< fcre' g create
fcre' (f :+!: g) create = fcre' f create -||- fcre' g create

-- | The @ana@ recursion pattern as a more relaxed 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,a) -> a) -> Lens a (F b a) -> Lens a b
ana_lns' (h::(b,a) -> a) l = Lens get' put' create'
    where get' = ana b (get l)
          put' = accum b  (put l) (uncurry gene)
          gene = fzip' g h <=< curry (id >< get l)
          create' = cata b (create l)
          b = _L :: b
          g = fctr :: Fctr (PF b)

-- | The @cata@ recursion pattern as a more relaxed 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)) => ((b,a) -> a) -> (Lens (F a b) b) -> Lens a b
cata_lns' (h::(b,a) -> a) l = Lens get' put' create'
    where get' = cata a (get l)
          put' = ana a (uncurry gene)
          gene = fzip' f h <=< (lexp (fmap (fixF f) get' . out) . curry (put l) /|\ const out)
          create' = ana a (create l)
          a = _L :: a
          f = fctr :: Fctr (PF a)

-- | A more relaxed version of 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)) => ((b,a) -> a) -> NatLens (PF a) (PF b) -> Lens a b
nat_lns' (h::(b,a) -> a) l = ana_lns' h (l a .< out_lns)
    where a = _L :: a

-- | A more relaxed version of the bifunctor mapping function @bmap@ as a lens.
-- Cannot employ @NatLens@ because the extra function depends on the polymorphic type argument.
bmap_lns' :: Bifctrable f => x -> BFix f -> ((a,Rep (BRep f c) x) -> c) -> Lens c a -> Lens (Rep (BRep f c) x) (Rep (BRep f a) x)
bmap_lns' (x::x) (f::BFix f) h l = Lens get' put' create'
    where get' = bmap f (get l) idx
          put' = bmap f (put l) idx . uncurry (bzip' x (bctr :: Bifctr f) h) . (id /\ snd)
          create' = bmap f (create l) idx
          idx = id :: x -> x

-- | A more relaxed version of the the polytypic bifunctor zipping combinator.
bzip' :: x -> Bifctr f -> ((a,e) -> c) -> (Rep (BRep f a) x,Rep (BRep f c) x) -> (e -> Rep (BRep f (a,c)) x)
bzip' x BI create = return . fst
bzip' x BP create = return
bzip' x BK create = return . 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 \/ bcre' x f create . fst
          r = bcre' x g create . fst \/ bzip' x g create
          idx = id :: x -> x

bcre' :: x -> Bifctr f -> ((a,e) -> c) -> Rep (BRep f a) x -> (e -> (Rep (BRep f (a,c)) x))
bcre' x BI create = return
bcre' x BP create = return /|\ curry create
bcre' x BK create = return
bcre' x (f :*!| g) create = bcre' x f create >|< bcre' x g create
bcre' x (f :+!| g) create = bcre' x f create -||- bcre' x g create

-- | A more relaxed version of the generic mapping lens for parametric types with one polymorphic parameter.
-- We do not define @gmap_lns'@ as a recursion pattern lens because we want to provide more control in the auxiliary functions.
-- Using @bmap_lns'@ we would not get @(a,d c) -> c@ but instead @(a,B d c (d a)) -> c@.
gmap_lns' :: (Mu (d a),Mu (d c),Fctrable (PF (d c)),Fctrable (PF (d a)),Bifctrable (BF d),
              F (d a) (d c) ~ B d a (d c), F (d c) (d c) ~ B d c (d c),
              F (d a) (d a) ~ B d a (d a),F (d c) (d a) ~ B d c (d a))
          => ((a,d c) -> c) -> ((d a,d c) -> d c) -> Lens c a -> Lens (d c) (d a)
gmap_lns' (h::(a,d c) -> c) i l = Lens get' put' create'
    where get' = cata dc (inn . bmap (fixB b) (get l) idda)
          put' = accum da gene (uncurry tau)
          gene = inn . bmap (fixB b) (put l) iddc . uncurry (bzip' dc b h <=< curry (id >< out))
          tau = fzip' f i <=< curry (id >< bmap (fixB b) (get l) iddc . out)
          create' = cata da (inn . bmap (fixB b) (create l) iddc)
          b = bctr :: Bifctr (BF d)
          f = fctr :: Fctr (PF (d a))
          da = _L :: d a
          dc = _L :: d c
          idda = id :: d a -> d a
          iddc = id :: d c -> d c