-----------------------------------------------------------------------------
-- |
-- Module      :  Generics.Pointless.Lenses.Examples.Examples
-- 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 examples, examples and more examples.
--
-----------------------------------------------------------------------------

module Generics.Pointless.Lenses.Examples.Examples where

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

-- | Integer successor lens.
succ_lns :: Lens Int Int
succ_lns = Lens succ (pred . fst) pred

-- | List length lens.
length_lns :: a -> Lens [a] Nat
length_lns a = nat_lns _L (\x -> id_lns -|-< snd_lns a)

-- | List length using an accumulation (after simplification into an hylomorphism).
-- Uses @Int@ instead of @Nat@ because @succ@ on @Nat@ is not a valid lens.
len_lns :: Lens ([Char],Int) Int
len_lns = hylo_lns t g h
    where g = id_lns .\/< id_lns
          h = (snd_lns _L -|-< snd_lns _L .< assocr_lns .< (id_lns ><< succ_lns)) .< distl_lns .< (out_lns ><< id_lns)
          t = _L :: K Int :+!: I

-- | List zipping lens.
-- The aux transformation is merely for simplifying the constant argument
zip_lns :: Lens ([a],[a]) [(a,a)]
zip_lns = ana_lns _L (((!<) c .< aux -|-< distp_lns) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns))
    where aux = (fst_lns _L -|-< snd_lns _L) -|-< fst_lns _L
          c :: Either (Either One (b,[b])) (a,[a])
          -- 1st option: do nothing
          -- 2nd option: append to the left source list
          -- 3rd option: append to right source list
          c = Left (Left _L)

-- | Take the first n elements from a list
take_lns :: Lens (Nat,[a]) [a]
take_lns = ana_lns _L h
   where h = ((!<) c -|-< aux) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns)
         aux = assocr_lns .< (swap_lns ><< id_lns) .< assocl_lns
         c :: Either (Either (One, One) (One,(a,[a]))) (Nat,One)
         -- 1st option: do nothing
         -- 2nd option: append to the source list
         -- 3rd option: increment the source number by
         c = Left (Left (_L,_L))

-- | List filtering lens.
-- The argument passed to @snd_lns@ can be undefined because it will never be used
filter_lns :: Lens [Either a b] [a]
filter_lns = cata_lns _L ((inn_lns .\/< snd_lns _L) .< coassocl_lns .< (id_lns -|-< distl_lns))

-- | Binary list concatenation.
-- Lens hylomorphisms can be defined as the composition of a catamorphism after an anamorphism.
cat_lns :: Lens ([a],[a]) [a]
cat_lns = hylo_lns (_L :: NeList [a] a) g h
    where g = inn_lns .< ((\/$<) out_lns)
          h = (snd_lns _L -|-< assocr_lns) .< distl_lns .< (out_lns ><< id_lns)

-- | Binary list transposition.
-- Binary version of @transpose@.
transpose_lns :: Lens ([a],[a]) [a]
transpose_lns = hylo_lns t g h
    where g = inn_lns .< ((\/$<) out_lns)
          h = (snd_lns _L -|-< (id_lns ><< swap_lns) .< assocr_lns) .< distl_lns .< (out_lns ><< id_lns)
          t = _L :: K [a] :+!: (K a :*!: I)

-- Integer addition
add_lns :: Lens (Int,Int) Int
add_lns = Lens get' put' create'
    where get' (x,y) = x+y
          put' (x,(a,b)) = (a,x-a)
          -- needs to be strictly decreasing in the first argument, that will be the recursive argument of sumInt_lns
          create' x | x > 0 = (div x 2 + mod x 2,div x 2)
                    | otherwise = (div x 2,div x 2 + mod x 2)

-- | Sum of a list of integers.
sumInt_lns :: Lens [Int] Int
sumInt_lns = cata_lns _L ((0 !\/< add_lns) _L)

plus_lns :: Lens (Nat,Nat) Nat
plus_lns = hylo_lns (_L::From Nat) f g
   where f = inn_lns .< ((\/$<) out_lns)
         g = (snd_lns _L -|-< id_lns) .< distl_lns .< (out_lns ><< id_lns)

sumNat_lns :: Lens [Nat] Nat
sumNat_lns = cata_lns _L g
    where g = inn_lns .< ((#\/<) (out_lns .< plus_lns))

type instance BF Tree = BConst One :+| (BPar :*| (BId :*| BId))

-- | Flatten a tree.
flatten_lns :: Lens (Tree a) [a]
flatten_lns = cata_lns _L (inn_lns .< (id_lns -|-< id_lns ><< cat_lns))

-- | List concatenation.
concat_lns :: Lens [[a]] [a]
concat_lns = cata_lns _L (inn_lns .< (((id_lns .\/< id_lns) -|-< id_lns) .< coassocl_lns .< (id_lns -|-< out_lns .< cat_lns)))

-- | List mapping lens.
map_lns :: Lens c a -> Lens [c] [a]
map_lns f = nat_lns _L (\x -> id_lns -|-< f ><< id_lns)

-- | Generic mapping example using user-defined concrete generators
data T a = Fst a | Next (T a) deriving (Eq,Show)

type instance BF T = BPar :+| BId
type instance PF (T a) = Const a :+: Id

instance Mu (T a) where
    inn (Left x) = Fst x
    inn (Right x) = Next x
    out (Fst x) = Left x
    out (Next x) = Right x

aux :: T a -> a
aux (Fst x) = x
aux (Next x) = aux x

tmap_lns l = gmap_lns' (aux . snd) snd l

exampleT = put (tmap_lns (fst_lns 'c')) (Fst 1,(Next (Fst (2,'a'))))