-----------------------------------------------------------------------------
-- |
-- Module      :  Generics.Pointless.Lenses.Examples.Examples
-- Copyright   :  (c) 2011 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.RecursionPatterns
import Generics.Pointless.Bifunctors
import Generics.Pointless.Examples.Examples
import Generics.Pointless.Lenses
import Generics.Pointless.Lenses.Combinators
import Generics.Pointless.Lenses.PartialCombinators
import Generics.Pointless.Lenses.RecursionPatterns
import Prelude

{-# 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 = sumn_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 (efficient version using primitive integers)
length_lns :: a -> Lens [a] Nat
length_lns a = Lens get' put' create'
	where get' xs = Nat $ Prelude.length xs
	      put' (Nat n,xs) = Prelude.take n (xs ++ repeat a)
	      create' (Nat n) = Prelude.replicate n a

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

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

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

-- | Right list filtering lens.
-- The argument passed to @snd_lns@ can be undefined because it will never be used
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' :: ((a,[a]) -> Bool) -> Lens ([a],[a]) [a]
cat_lns' p = hylo_lns (ann :: Ann (NeList [a] a)) g h
    where g = inn_lns .< (id_lns -|-< ((\/<) f id_lns id_lns)) .< coassocr_lns .< (out_lns -|-< id_lns)
          h = (snd_lns bang -|-< assocr_lns) .< distl_lns .< (out_lns ><< id_lns)
          f = (bang -|- bang) . coswap . (p?)
cat_lns = cat_lns' (const False)

-- | Binary list transposition.
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 = ann :: Ann (K [a] :+!: (K a :*!: I))

-- | Addition of two natural (efficient version using integers)
plus_lns :: Lens (Nat,Nat) Nat
plus_lns = Lens get' put' create'
	where get' (Nat x,Nat y) = Nat (x + y)
	      put' (Nat z,(Nat x,Nat y)) | z > x = (Nat z,Nat (z-x))
	                                 | otherwise = (Nat z,nzero)
	      create' (Nat z) = (Nat z,nzero)

-- | Addition of two natural numbers using an hylomorphism on naturals.
plus_lns' :: Lens (Nat,Nat) Nat
plus_lns' = hylo_lns (ann::Ann (From Nat)) f g
   where f = inn_lns .< (out_lns \/$< id_lns)
         g = (snd_lns bang -|-< id_lns) .< distl_lns .< (out_lns ><< id_lns)

-- | Sums a list of natural numbers.
sumn_lns :: Lens [Nat] Nat
sumn_lns = cata_lns _L g
    where g = inn_lns .< (id_lns #\/< (out_lns .< plus_lns))

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

-- | @concat_lns .< map_lns l@
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))

-- | Partitions a list of options into two lists.
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)

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

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

-- ** Halve

-- | Splits a list in half.
halve_lns :: a -> Lens [a] [a]
halve_lns v = ana_lns _L g
    where g = (id_lns -|-< id_lns ><< nil_lns .< (id_lns -|-< fst_lns (const v)) .< last_lns) .< out_lns

nil_lns :: Lens (Either One [a]) [a]
nil_lns = inn_lns .< (id_lns #\/< id_lns) .< (id_lns -|-< out_lns)

last_lns :: Lens [a] (Either One ([a],a))
last_lns = cata_lns _L g
    where g = (id_lns -|-< (inn_lns ><< id_lns) .< undistl_lns .< (swap_lns -|-< assocl_lns) .< distr_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 (ann :: Ann (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 = ann :: Ann (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)

-- * Partial lenses

-- | Replicate a value n times.
-- Fails when the target list is not a replication.
replicate_lns :: Eq a => a -> Lens (a,Nat) [a]
replicate_lns v = varlens l v gen
  where l x = ana_lns _L $ (snd_lns (const x) -|-< assocr_lns .< ((id_lns /\< id_lns) ><< id_lns)) .< distr_lns .< (id_lns ><< out_lns)
        gen [] = v
        gen (x:xs) = x

-- Concatenates lists of replicated values.
replicatel_lns :: (Show a,Eq a) => Lens [(a,Nat)] [a]
replicatel_lns = hylo_lns (ann :: Ann (NeList One [a])) g h
    where g = inn_lns .< (id_lns #\/< out_lns) .< (id_lns -|-< catrep_lns)
          h = (id_lns -|-< replicate_lns _L ><< id_lns) .< out_lns

-- | List concatenation with a special create.
-- For create, split to the left all equal values from the beginning of the list
catrep_lns :: Eq a => Lens ([a],[a]) [a]
catrep_lns = varlens l _L gen
    where l x = cat_lns' ((==x) . fst)
          gen [] = _L
          gen (x:xs) = x

-- ** Sieving to keep only each second element of a list

sieve_lns :: a -> Lens [a] [a]
sieve_lns x = ana_lns _L g
    where g = ((id_lns .\/< snd_lns _L) -|-< snd_lns (const x)) .< coassocl_lns .< (id_lns -|-< distr_lns .< (id_lns ><< out_lns)) .< out_lns

-- ** Insertion sort

-- | Sorts a list.
-- Fails when the target list is not sorted.
isort_lns :: Ord a => Lens [a] [a]
isort_lns = cata_lns _L f
    where f = inn_lns .< (id_lns -|-< insert_lns)

insert_lns :: Ord a => Lens (a,[a]) (a,[a])
insert_lns = hylo_lns (ann :: Ann (NeList (a,[a]) a)) g h
    where g = (id_lns ><< neecons_lns) .< undistr_lns
        --inn_lns .< inr_lns .< (id_lns .\/< id_lns)
          h = ((id_lns ><< inn_lns) .< undistr_lns -|-< subr_lns) .< coassocl_lns
            .< (id_lns -|-< (?.<) p) .< distr_lns .< (id_lns ><< out_lns)
          p = le . (id >< fst)
          le = uncurry (<=)

neecons_lns :: Lens (Either [a] (a,[a])) [a]
neecons_lns = inn_lns .< (id_lns -|-< (id_lns .\/< id_lns)) .< coassocr_lns .< (out_lns -|-< id_lns)