{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DataKinds, TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Data.List.Length.LengthL (
	LengthL, unfoldr, unfoldrWithBase, unfoldrM, unfoldrMWithBase,
	ListToLengthL, splitL ) where

import GHC.TypeNats (type (-), type (<=))
import Control.Arrow (first, (+++))
import Control.Monad.State (StateL(..))
import Data.List.Range.RangeL (LengthL, RangeL(..), Unfoldr, unfoldrMRangeWithBase)

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

-- * TYPE
-- * UNFOLDR
-- * LIST TO LENGTH LEFT

---------------------------------------------------------------------------
-- TYPE
---------------------------------------------------------------------------

---------------------------------------------------------------------------
-- UNFOLDR
---------------------------------------------------------------------------

unfoldr :: (0 <= n, Unfoldr 0 n n) => (s -> (a, s)) -> s -> LengthL n a
unfoldr :: (s -> (a, s)) -> s -> LengthL n a
unfoldr = RangeL 0 n a -> (s -> (a, s)) -> s -> LengthL n a
forall (n :: Nat) (m :: Nat) a s.
Unfoldr n m m =>
RangeL n m a -> (s -> (a, s)) -> s -> LengthL m a
unfoldrWithBase RangeL 0 n a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL

{-^

To evaluate function repeatedly to construct a list of type @LengthL n a@.
The function recieve a state and return an element value and a new state.

>>> :set -XDataKinds
>>> unfoldr (\n -> (2 * n, n + 1)) 0 :: LengthL 5 Integer
0 :. (2 :. (4 :. (6 :. (8 :. NilL))))

-}

unfoldrWithBase ::
	Unfoldr n m m => RangeL n m a -> (s -> (a, s)) -> s -> LengthL m a
unfoldrWithBase :: RangeL n m a -> (s -> (a, s)) -> s -> LengthL m a
unfoldrWithBase RangeL n m a
xs = ((LengthL m a, s) -> LengthL m a
forall a b. (a, b) -> a
fst ((LengthL m a, s) -> LengthL m a)
-> (s -> (LengthL m a, s)) -> s -> LengthL m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((s -> (LengthL m a, s)) -> s -> LengthL m a)
-> ((s -> (a, s)) -> s -> (LengthL m a, s))
-> (s -> (a, s))
-> s
-> LengthL m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateL s (LengthL m a) -> s -> (LengthL m a, s)
forall s a. StateL s a -> s -> (a, s)
runStateL (StateL s (LengthL m a) -> s -> (LengthL m a, s))
-> ((s -> (a, s)) -> StateL s (LengthL m a))
-> (s -> (a, s))
-> s
-> (LengthL m a, s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangeL n m a -> StateL s a -> StateL s (LengthL m a)
forall (m :: * -> *) (n :: Nat) (w :: Nat) a.
(Monad m, Unfoldr n w w) =>
RangeL n w a -> m a -> m (LengthL w a)
unfoldrMWithBase RangeL n m a
xs (StateL s a -> StateL s (LengthL m a))
-> ((s -> (a, s)) -> StateL s a)
-> (s -> (a, s))
-> StateL s (LengthL m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s -> (a, s)) -> StateL s a
forall s a. (s -> (a, s)) -> StateL s a
StateL

{-^

It is like @unfoldr@. But it has already prepared values.

>>> :set -XDataKinds
>>> xs = 123 :. 456 :.. NilL :: RangeL 1 5 Integer
>>> unfoldrWithBase xs (\n -> (2 * n, n + 1)) 0 :: LengthL 5 Integer
123 :. (456 :. (0 :. (2 :. (4 :. NilL))))

-}

unfoldrM :: (Monad m, 0 <= n, Unfoldr 0 n n) => m a -> m (LengthL n a)
unfoldrM :: m a -> m (LengthL n a)
unfoldrM = RangeL 0 n a -> m a -> m (LengthL n a)
forall (m :: * -> *) (n :: Nat) (w :: Nat) a.
(Monad m, Unfoldr n w w) =>
RangeL n w a -> m a -> m (LengthL w a)
unfoldrMWithBase RangeL 0 n a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL

{-^

It is like @unfoldr@. But it use a monad as an argument instead of a function.

>>> :set -XDataKinds
>>> :module + Data.IORef
>>> r <- newIORef 1
>>> count = readIORef r >>= \n -> n <$ writeIORef r (n +1)
>>> unfoldrM count :: IO (LengthL 5 Integer)
1 :. (2 :. (3 :. (4 :. (5 :. NilL))))

-}

unfoldrMWithBase ::
	(Monad m, Unfoldr n w w) => RangeL n w a -> m a -> m (LengthL w a)
unfoldrMWithBase :: RangeL n w a -> m a -> m (LengthL w a)
unfoldrMWithBase = (RangeL n w a -> m Bool -> m a -> m (LengthL w a)
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldr n v w, Monad m) =>
RangeL n w a -> m Bool -> m a -> m (RangeL v w a)
`unfoldrMRangeWithBase` m Bool
forall a. HasCallStack => a
undefined)

{-^

It is like @unfoldrM@. But it has already prepared values.

>>> :set -XDataKinds
>>> :module + Data.IORef
>>> r <- newIORef 1
>>> count = readIORef r >>= \n -> n <$ writeIORef r (n + 1)
>>> unfoldrMWithBase (123 :. 456 :.. NilL) count :: IO (LengthL 5 Integer)
123 :. (456 :. (1 :. (2 :. (3 :. NilL))))

-}

---------------------------------------------------------------------------
-- LIST TO LENGTH LEFT
---------------------------------------------------------------------------

class ListToLengthL n where
	splitL :: [a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])

	{-^

	To take a lengthed list from a list.
	If an original list has not enough elements, then it return
	a left value.

	>>> :set -XTypeApplications -XDataKinds
	>>> splitL @4 "Hi!"
	Left ('H' :.. ('i' :.. ('!' :.. NilL)))
	>>> splitL @4 "Hello!"
	Right ('H' :. ('e' :. ('l' :. ('l' :. NilL))),"o!")

	-}

instance ListToLengthL 1 where
	splitL :: [a] -> Either (RangeL 0 (1 - 1) a) (LengthL 1 a, [a])
splitL = \case [] -> RangeL 0 0 a -> Either (RangeL 0 0 a) (LengthL 1 a, [a])
forall a b. a -> Either a b
Left RangeL 0 0 a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL; a
x : [a]
xs -> (LengthL 1 a, [a]) -> Either (RangeL 0 0 a) (LengthL 1 a, [a])
forall a b. b -> Either a b
Right (a
x a -> RangeL (1 - 1) (1 - 1) a -> LengthL 1 a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:. RangeL (1 - 1) (1 - 1) a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL, [a]
xs)

instance {-# OVERLAPPABLE #-}
	(1 <= n, 1 <= (n - 1), 0 <= (n - 1), ListToLengthL (n - 1)) => ListToLengthL n where
	splitL :: [a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
splitL = \case
		[] -> RangeL 0 (n - 1) a
-> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
forall a b. a -> Either a b
Left RangeL 0 (n - 1) a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL
		a
x : [a]
xs -> (a
x a -> RangeL 0 ((n - 1) - 1) a -> RangeL 0 (n - 1) a
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
:..) (RangeL 0 ((n - 1) - 1) a -> RangeL 0 (n - 1) a)
-> ((RangeL (n - 1) (n - 1) a, [a]) -> (LengthL n a, [a]))
-> Either
     (RangeL 0 ((n - 1) - 1) a) (RangeL (n - 1) (n - 1) a, [a])
-> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ ((a
x a -> RangeL (n - 1) (n - 1) a -> LengthL n a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:.) (RangeL (n - 1) (n - 1) a -> LengthL n a)
-> (RangeL (n - 1) (n - 1) a, [a]) -> (LengthL n a, [a])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
`first`) (Either (RangeL 0 ((n - 1) - 1) a) (RangeL (n - 1) (n - 1) a, [a])
 -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a]))
-> Either
     (RangeL 0 ((n - 1) - 1) a) (RangeL (n - 1) (n - 1) a, [a])
-> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
forall a b. (a -> b) -> a -> b
$ [a]
-> Either
     (RangeL 0 ((n - 1) - 1) a) (RangeL (n - 1) (n - 1) a, [a])
forall (n :: Nat) a.
ListToLengthL n =>
[a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
splitL [a]
xs