-----------------------------------------------------------------------------
-- |
-- 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.Bifunctors
import Generics.Pointless.Examples.Examples
import Generics.Pointless.Lenses
import Generics.Pointless.Lenses.Combinators
import Generics.Pointless.Lenses.RecursionPatterns

{-# RULES
  "mapId"
  map_lns id_lns = id_lns
  #-}
{-# RULES
  "mapFusion" forall l1 l2.
  map_lns l1 .< map_lns l2 = map_lns (l1 .< l2)
  #-}
{-# RULES
  "mapCat" forall l1.
  map_lns l1 .< cat_lns = cat_lns .< (map_lns l1 ><< map_lns l1)
  #-}
{-# RULES
  "mapConcat" forall l1.
  map_lns l1 .< concat_lns = concat_lns .< map_lns (map_lns l1)
  #-}
{-# RULES
  "filterLeftMap" forall l1 l2.
  filter_left_lns .< map_lns (l1 -|-< l2) = map_lns l1 .< filter_left_lns
  #-}
{-# RULES
  "filterLeftMap" forall l1 l2.
  filter_left_lns .< map_lns (l1 -|-< l2) = map_lns l1 .< filter_left_lns
  #-}
{-# RULES
  "lengthCat" forall c.
  length_lns c .< cat_lns = plus_lns .< (length_lns c ><< length_lns c)
  #-}
{-# RULES
  "lengthMap" forall c l1.
  length_lns c .< map_lns l1 = length_lns (create l1 c)
  #-}
{-# RULES
  "lengthConcat" forall c.
  length_lns c .< concat_lns = suml_lns .< map_lns (length_lns c)
  #-}
{-# RULES
  "filterMap"  forall l1 l2.
  filter_left_lns .< (map_lns (l1 -|-< l2)) = (map_lns l1) .< filter_left_lns
  #-}
{-# RULES
  "filterMap"  forall l1 l2.
  filter_left_lns .< (map_lns (l1 -|-< l2)) = (map_lns l1) .< filter_left_lns
  #-}

-- * Lenses over trees

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

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

-- | Flatten a tree into a list.
postOrd_lns :: Lens (Tree a) [a]
postOrd_lns = cata_lns _L (eitherNilSnoc .< (id_lns -|-< id_lns ><< cat_lns))

-- * Lenses over lists and natural numbers

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

zipWith_lns :: Lens (a,b) c -> Lens ([a],[b]) [c]
zipWith_lns f = ana_lns _L (((!<) c -|-< (f ><< id_lns) .< distp_lns) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns))
    where 
          -- 1st option: do nothing
          -- 2nd option: append to the left source list
          -- 3rd option: append to right source list
          c = const $ Left (Left (_L,_L))

-- | List zipping lens.
zip_lns :: Lens ([a],[b]) [(a,b)]
zip_lns = ana_lns _L (((!<) c -|-< distp_lns) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns))
    where 
          -- 1st option: do nothing
          -- 2nd option: append to the left source list
          -- 3rd option: append to right source list
          c = const $ Left (Left (_L,_L))

-- | Take the first n elements from a list
take_lns :: Lens (Nat,[a]) [a]
take_lns = ana_lns _L h
   where h = ((!<) c -|-< subr_lns) .< coassocl_lns .< dists_lns .< (out_lns ><< out_lns)
         --c :: One -> 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 = const $ Left (Left (_L,_L))     

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

filter_right_lns :: Lens [Either a b] [b]
filter_right_lns = cata_lns _L ((inn_lns .\/< snd_lns _L) .< coassocl_lns .< (id_lns -|-< coswap_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 \/$< id_lns)
          h = (snd_lns bang -|-< 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 \/$< id_lns)
          h = (snd_lns _L -|-< (id_lns ><< swap_lns) .< assocr_lns) .< distl_lns .< (out_lns ><< id_lns)
          t = _L :: K [a] :+!: (K a :*!: I)

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

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

concatMap_lns :: Lens a [b] -> Lens [a] [b]
concatMap_lns l = cata_lns _L f
    where f = inn_lns .< (id_lns #\/< out_lns .< cat_lns .< (l ><< id_lns))

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

-- | Partitions a list of options into two lists.
-- Note that this imposes some redefinement of the traditional definition in order to fit our framework.
partition_lns :: Lens [Either a b] ([a],[b])
partition_lns = cata_lns _L f where
        f = (inn_lns ><< id_lns) .< undistl_lns .< ((!/\<) id_lns -|-< (id_lns ><< g) .< undistr_lns) .< coassocr_lns
          .< ((inn_lns -|-< id_lns) .< coassocl_lns .< (id_lns -|-< (snd_lns _L -|-< id_lns) .< distl_lns .< (out_lns ><< id_lns) .< subr_lns) -|-< assocl_lns)
          .< coswap_lns .< cosubr_lns .< (id_lns -|-< distl_lns)
        g = inn_lns .< (out_lns \/$< id_lns) .< coswap_lns

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

head_lns :: [a] -> Lens [a] (Either One a)
head_lns l = (id_lns -|-< fst_lns (l!)) .< out_lns

tail_lns :: a -> Lens [a] (Either One [a])
tail_lns v = (id_lns -|-< snd_lns (v!)) .< out_lns

-- ** Reverse

-- | Inserts an element at the end of a list, thus making it non-empty.
snoc_lns :: Lens (a,[a]) (Some a)
snoc_lns = hylo_lns (_L :: NeList a a) f g
   where f = inn_lns
         g = (fst_lns _L -|-< subr_lns) .< distr_lns .< (id_lns ><< out_lns)

-- | Isomorphism between a list and an optional non-empty list.
toSome_lns :: Lens [a] (Either One (Some a))
toSome_lns = cata_lns _L f
    where f = (id_lns -|-< inn_lns) .< (id_lns -|-< (fst_lns _L -|-< id_lns) .< distr_lns)

-- | Converts a list into a non-empty list.
some_lns :: Eq a => a -> Lens [a] (Some a)
some_lns c = (Wrap c !\/< id_lns) _L .< toSome_lns

-- | Isomorphism between a list and an optional non-empty list.
fromSome_lns :: Lens (Either One (Some a)) [a]
fromSome_lns = ana_lns _L g
    where g = (id_lns -|-< undistr_lns) .< (id_lns -|-< ((/\!<) id_lns  -|-< id_lns)) .< (id_lns -|-< out_lns)

eitherNilSnoc :: Lens (Either One (a,[a])) [a]
eitherNilSnoc = fromSome_lns .< (id_lns -|-< snoc_lns)

-- | The list reversal lens is an isomorphism.
reverse_lns :: Lens [a] [a]
reverse_lns = cata_lns _L eitherNilSnoc

-- * Non-natural lenses

-- | 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 ([a],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 ><< inc_lns)) .< distl_lns .< (out_lns ><< id_lns)
          t = _L :: K Int :+!: I

-- Integer addition
add_lns :: Lens (Int,Int) Int
add_lns = Lens get' put' create'
    where get' (x,y) = x+y
          put' (x,(a,_)) = (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)

-- | Incremental summation of a list.
-- Since general splitting is not a lens, we need to provide user-defined put and create functions that serve our purpose and construct a valid lens.
isum_lns :: Lens [Int] [Int]
isum_lns = cata_lns _L f
    where f = inn_lns .< (id_lns -|-< fstmapadd)
          fstmapadd :: Lens (Int,[Int]) (Int,[Int])
          fstmapadd = Lens get' put' create'
            where get' = fst /\ (\(i,l) -> map (+i) l)
                  put' = create' . fst
                  create' (i,l) = (i,map (\x -> x-i) l)