{-# LANGUAGE BlockArguments, TupleSections #-}
{-# LANGUAGE DataKinds, TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.List.Length (
	-- * LENGTHED LIST LEFT
	-- ** Type
	LengthL, RangeL(NilL, (:.)),
	-- ** AddL
	AddL, (++.),
	-- ** Unfoldr
	-- *** class
	Unfoldr,
	-- *** without monad
	repeatL, fillL, unfoldr, unfoldrWithBase,
	-- *** with monad
	unfoldrM, unfoldrMWithBase,
	-- ** ZipL
	ZipL, zipL, zipWithL, zipWithML,
	-- ** ListToLengthL
	ListToLengthL, splitL, chunksL, chunksL',
	-- * LENGTHED LIST RIGHT
	-- ** Type
	LengthR, RangeR(NilR, (:+)),
	-- ** AddR
	AddR, (+++),
	-- ** Unfoldl
	-- *** class
	Unfoldl,
	-- *** without monad
	repeatR, fillR, unfoldl, unfoldlWithBase,
	-- *** with monad
	unfoldlM, unfoldlMWithBase,
	-- ** ZipR
	ZipR, zipR, zipWithR, zipWithMR,
	-- ** ListToLengthR
	ListToLengthR, listToLengthR, chunksR, chunksR',
	-- * LEFT TO RIGHT
	LeftToRight, (++.+), leftToRight,
	-- * RIGHT TO LEFT
	RightToLeft, (++..), rightToLeft ) where

import Control.Arrow (first, (***))
import Data.List.Range (
	RangeL(..), AddL, (++.), LoosenLMax, loosenLMax, Unfoldr,
	ZipL, zipL, zipWithL, zipWithML,
	RangeR(..), AddR, (+++), LoosenRMax, loosenRMax, Unfoldl,
	ZipR, zipR, zipWithR, zipWithMR,
	LeftToRight, (++.+), leftToRight, RightToLeft, (++..), rightToLeft )
import Data.List.Length.LengthL (
	LengthL, unfoldr, unfoldrWithBase, unfoldrM, unfoldrMWithBase,
	ListToLengthL, splitL )
import Data.List.Length.LengthR (
	LengthR, unfoldl, unfoldlWithBase, unfoldlM, unfoldlMWithBase,
	ListToLengthR, listToLengthR )

import GHC.TypeNats

---------------------------------------------------------------------------

-- LENGTH LEFT
-- LENGTH RIGHT

---------------------------------------------------------------------------
-- LENGTH LEFT
---------------------------------------------------------------------------

repeatL :: (0 <= n, Unfoldr 0 n n) => a -> LengthL n a
repeatL :: a -> LengthL n a
repeatL = RangeL 0 n a -> a -> LengthL n a
forall (n :: Nat) (m :: Nat) a.
Unfoldr n m m =>
RangeL n m a -> a -> LengthL m a
fillL RangeL 0 n a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL

{-^

To repeat a value of type @a@ to construct a list of type @LengthL n a@.

>>> :set -XDataKinds
>>> repeatL 'c' :: LengthL 5 Char
'c' :. ('c' :. ('c' :. ('c' :. ('c' :. NilL))))

-}

fillL :: Unfoldr n m m => RangeL n m a -> a -> LengthL m a
fillL :: RangeL n m a -> a -> LengthL m a
fillL = (RangeL n m a -> (a -> (a, a)) -> a -> LengthL m a
forall (n :: Nat) (m :: Nat) a s.
Unfoldr n m m =>
RangeL n m a -> (s -> (a, s)) -> s -> LengthL m a
`unfoldrWithBase` \a
x -> (a
x, a
x))

{-^

To fill a list of type @LengthL n a@ with a value of type @a@.

>>> :set -XDataKinds
>>> fillL ('a' :. 'b' :.. NilL) 'c' :: LengthL 5 Char
'a' :. ('b' :. ('c' :. ('c' :. ('c' :. NilL))))

-}

chunksL :: ListToLengthL n => [a] -> ([LengthL n a], RangeL 0 (n - 1) a)
chunksL :: [a] -> ([LengthL n a], RangeL 0 (n - 1) a)
chunksL = (RangeL 0 (n - 1) a -> ([LengthL n a], RangeL 0 (n - 1) a))
-> ((LengthL n a, [a]) -> ([LengthL n a], RangeL 0 (n - 1) a))
-> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
-> ([LengthL n a], RangeL 0 (n - 1) a)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([] ,) ((([LengthL n a] -> [LengthL n a])
 -> ([LengthL n a], RangeL 0 (n - 1) a)
 -> ([LengthL n a], RangeL 0 (n - 1) a))
-> ([LengthL n a] -> [LengthL n a],
    ([LengthL n a], RangeL 0 (n - 1) a))
-> ([LengthL n a], RangeL 0 (n - 1) a)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ([LengthL n a] -> [LengthL n a])
-> ([LengthL n a], RangeL 0 (n - 1) a)
-> ([LengthL n a], RangeL 0 (n - 1) a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (([LengthL n a] -> [LengthL n a],
  ([LengthL n a], RangeL 0 (n - 1) a))
 -> ([LengthL n a], RangeL 0 (n - 1) a))
-> ((LengthL n a, [a])
    -> ([LengthL n a] -> [LengthL n a],
        ([LengthL n a], RangeL 0 (n - 1) a)))
-> (LengthL n a, [a])
-> ([LengthL n a], RangeL 0 (n - 1) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((:) (LengthL n a -> [LengthL n a] -> [LengthL n a])
-> ([a] -> ([LengthL n a], RangeL 0 (n - 1) a))
-> (LengthL n a, [a])
-> ([LengthL n a] -> [LengthL n a],
    ([LengthL n a], RangeL 0 (n - 1) a))
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [a] -> ([LengthL n a], RangeL 0 (n - 1) a)
forall (n :: Nat) a.
ListToLengthL n =>
[a] -> ([LengthL n a], RangeL 0 (n - 1) a)
chunksL)) (Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
 -> ([LengthL n a], RangeL 0 (n - 1) a))
-> ([a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a]))
-> [a]
-> ([LengthL n a], RangeL 0 (n - 1) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
forall (n :: Nat) a.
ListToLengthL n =>
[a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
splitL

{-^

To separate a list to multiple lengthed lists.
It return separeted lengthed lists and a not enough length fragment.

>>> :set -XTypeApplications -XDataKinds
>>> chunksL @3 "foo bar"
(['f' :. ('o' :. ('o' :. NilL)),' ' :. ('b' :. ('a' :. NilL))],'r' :.. NilL)

-}

chunksL' :: (Unfoldr 0 n n, LoosenLMax 0 (n - 1) n, ListToLengthL n) =>
	a -> [a] -> [LengthL n a]
chunksL' :: a -> [a] -> [LengthL n a]
chunksL' a
z [a]
xs = case [a] -> ([LengthL n a], RangeL 0 (n - 1) a)
forall (n :: Nat) a.
ListToLengthL n =>
[a] -> ([LengthL n a], RangeL 0 (n - 1) a)
chunksL [a]
xs of
	([LengthL n a]
cs, RangeL 0 (n - 1) a
NilL) -> [LengthL n a]
cs; ([LengthL n a]
cs, RangeL 0 (n - 1) a
rs) -> [LengthL n a]
cs [LengthL n a] -> [LengthL n a] -> [LengthL n a]
forall a. [a] -> [a] -> [a]
++ [RangeL 0 (n - 1) a -> RangeL 0 n a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenLMax n m w =>
RangeL n m a -> RangeL n w a
loosenLMax RangeL 0 (n - 1) a
rs RangeL 0 n a -> a -> LengthL n a
forall (n :: Nat) (m :: Nat) a.
Unfoldr n m m =>
RangeL n m a -> a -> LengthL m a
`fillL` a
z]

{-^

It is like chunksL.
But if there is a not enough length fragment, then it fill with a default value.

>>> :set -XTypeApplications -XDataKinds
>>> print `mapM_` chunksL' @3 '@' "foo bar"
'f' :. ('o' :. ('o' :. NilL))
' ' :. ('b' :. ('a' :. NilL))
'r' :. ('@' :. ('@' :. NilL))

-}

---------------------------------------------------------------------------
-- LENGTH RIGHT
---------------------------------------------------------------------------

repeatR :: (0 <= n, Unfoldl 0 n n) => a -> LengthR n a
repeatR :: a -> LengthR n a
repeatR = (a -> RangeR 0 n a -> LengthR n a
forall (n :: Nat) (m :: Nat) a.
Unfoldl n m m =>
a -> RangeR n m a -> LengthR m a
`fillR` RangeR 0 n a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR)

{-^

To repeat a value of type @a@ to construct a list of type @LengthR n a@.

>>> :set -XDataKinds
>>> repeatR 'c' :: LengthR 5 Char
((((NilR :+ 'c') :+ 'c') :+ 'c') :+ 'c') :+ 'c'

-}

fillR :: Unfoldl n m m => a -> RangeR n m a -> LengthR m a
fillR :: a -> RangeR n m a -> LengthR m a
fillR = (a -> (a, a)) -> a -> RangeR n m a -> LengthR m a
forall (n :: Nat) (m :: Nat) s a.
Unfoldl n m m =>
(s -> (s, a)) -> s -> RangeR n m a -> LengthR m a
unfoldlWithBase \a
x -> (a
x, a
x)

{-^

To fill a list of type @LengthR n a@ with a default value.

>>> :set -XDataKinds
>>> fillR 'c' (NilR :++ 'a' :+ 'b') :: LengthR 5 Char
((((NilR :+ 'c') :+ 'c') :+ 'c') :+ 'a') :+ 'b'

-}

chunksR :: ListToLengthR n => [a] -> ([LengthR n a], RangeR 0 (n - 1) a)
chunksR :: [a] -> ([LengthR n a], RangeR 0 (n - 1) a)
chunksR = (RangeR 0 (n - 1) a -> ([LengthR n a], RangeR 0 (n - 1) a))
-> ((LengthR n a, [a]) -> ([LengthR n a], RangeR 0 (n - 1) a))
-> Either (RangeR 0 (n - 1) a) (LengthR n a, [a])
-> ([LengthR n a], RangeR 0 (n - 1) a)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([] ,) ((([LengthR n a] -> [LengthR n a])
 -> ([LengthR n a], RangeR 0 (n - 1) a)
 -> ([LengthR n a], RangeR 0 (n - 1) a))
-> ([LengthR n a] -> [LengthR n a],
    ([LengthR n a], RangeR 0 (n - 1) a))
-> ([LengthR n a], RangeR 0 (n - 1) a)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ([LengthR n a] -> [LengthR n a])
-> ([LengthR n a], RangeR 0 (n - 1) a)
-> ([LengthR n a], RangeR 0 (n - 1) a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (([LengthR n a] -> [LengthR n a],
  ([LengthR n a], RangeR 0 (n - 1) a))
 -> ([LengthR n a], RangeR 0 (n - 1) a))
-> ((LengthR n a, [a])
    -> ([LengthR n a] -> [LengthR n a],
        ([LengthR n a], RangeR 0 (n - 1) a)))
-> (LengthR n a, [a])
-> ([LengthR n a], RangeR 0 (n - 1) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((:) (LengthR n a -> [LengthR n a] -> [LengthR n a])
-> ([a] -> ([LengthR n a], RangeR 0 (n - 1) a))
-> (LengthR n a, [a])
-> ([LengthR n a] -> [LengthR n a],
    ([LengthR n a], RangeR 0 (n - 1) a))
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [a] -> ([LengthR n a], RangeR 0 (n - 1) a)
forall (n :: Nat) a.
ListToLengthR n =>
[a] -> ([LengthR n a], RangeR 0 (n - 1) a)
chunksR)) (Either (RangeR 0 (n - 1) a) (LengthR n a, [a])
 -> ([LengthR n a], RangeR 0 (n - 1) a))
-> ([a] -> Either (RangeR 0 (n - 1) a) (LengthR n a, [a]))
-> [a]
-> ([LengthR n a], RangeR 0 (n - 1) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Either (RangeR 0 (n - 1) a) (LengthR n a, [a])
forall (n :: Nat) a.
ListToLengthR n =>
[a] -> Either (RangeR 0 (n - 1) a) (LengthR n a, [a])
listToLengthR

{-^

To separate a list to multiple lengthed lists.
It return separated lengthed lists and a not enough length fragment.

>>> :set -XTypeApplications -XDataKinds
>>> chunksR @3 "foo bar"
([((NilR :+ 'o') :+ 'o') :+ 'f',((NilR :+ 'a') :+ 'b') :+ ' '],NilR :++ 'r')

-}

chunksR' :: (Unfoldl 0 n n, LoosenRMax 0 (n - 1) n, ListToLengthR n) =>
	a -> [a] -> [LengthR n a]
chunksR' :: a -> [a] -> [LengthR n a]
chunksR' a
z [a]
xs = case [a] -> ([LengthR n a], RangeR 0 (n - 1) a)
forall (n :: Nat) a.
ListToLengthR n =>
[a] -> ([LengthR n a], RangeR 0 (n - 1) a)
chunksR [a]
xs of
	([LengthR n a]
cs, RangeR 0 (n - 1) a
NilR) -> [LengthR n a]
cs; ([LengthR n a]
cs, RangeR 0 (n - 1) a
rs) -> [LengthR n a]
cs [LengthR n a] -> [LengthR n a] -> [LengthR n a]
forall a. [a] -> [a] -> [a]
++ [a
z a -> RangeR 0 n a -> LengthR n a
forall (n :: Nat) (m :: Nat) a.
Unfoldl n m m =>
a -> RangeR n m a -> LengthR m a
`fillR` RangeR 0 (n - 1) a -> RangeR 0 n a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax RangeR 0 (n - 1) a
rs]

{-^

It is like @chunksR@.
But if there is a not enough length fragment, then it fill with a default value.

>>> :set -XTypeApplications -XDataKinds
>>> print `mapM_` chunksR' @3 '@' "foo bar"
((NilR :+ 'o') :+ 'o') :+ 'f'
((NilR :+ 'a') :+ 'b') :+ ' '
((NilR :+ '@') :+ '@') :+ 'r'

-}