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

module Data.List.Length.LengthR (
	LengthR, unfoldl, unfoldlWithBase, unfoldlM, unfoldlMWithBase,
	ListToLengthR, listToLengthR ) where

import GHC.TypeNats (type (-), type (<=))
import Control.Arrow (first, (+++))
import Control.Monad.State (StateR(..))
import Data.List.Range.RangeR (RangeR(..), Unfoldl, unfoldlMRangeWithBase)

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

-- TYPE
-- UNFOLDL
-- LIST TO LENGTH RIGHT

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

type LengthR n = RangeR n n

{-^

@LengthR n a@ is a list which have just n members of type @a@.
You can push and pop an element from right.

>>> :set -XDataKinds
>>> sampleLengthR = NilR :+ 'h' :+ 'e' :+ 'l' :+ 'l' :+ 'o' :: LengthR 5 Char

-}

---------------------------------------------------------------------------
-- UNFOLDL
---------------------------------------------------------------------------

unfoldl :: (0 <= n, Unfoldl 0 n n) => (s -> (s, a)) -> s -> LengthR n a
unfoldl :: (s -> (s, a)) -> s -> LengthR n a
unfoldl s -> (s, a)
f s
s = (s -> (s, a)) -> s -> RangeR 0 n a -> LengthR n a
forall (n :: Nat) (m :: Nat) s a.
Unfoldl n m m =>
(s -> (s, a)) -> s -> RangeR n m a -> LengthR m a
unfoldlWithBase s -> (s, a)
f s
s RangeR 0 n a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR

{-^

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

>>> :set -XDataKinds
>>> unfoldl (\n -> (n + 1, 2 * n)) 0 :: LengthR 5 Integer
((((NilR :+ 8) :+ 6) :+ 4) :+ 2) :+ 0

-}

unfoldlWithBase ::
	Unfoldl n m m => (s -> (s, a)) -> s -> RangeR n m a -> LengthR m a
unfoldlWithBase :: (s -> (s, a)) -> s -> RangeR n m a -> LengthR m a
unfoldlWithBase s -> (s, a)
f = ((s, LengthR m a) -> LengthR m a
forall a b. (a, b) -> b
snd ((s, LengthR m a) -> LengthR m a)
-> (RangeR n m a -> (s, LengthR m a))
-> RangeR n m a
-> LengthR m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((RangeR n m a -> (s, LengthR m a)) -> RangeR n m a -> LengthR m a)
-> (s -> RangeR n m a -> (s, LengthR m a))
-> s
-> RangeR n m a
-> LengthR m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RangeR n m a -> s -> (s, LengthR m a))
-> s -> RangeR n m a -> (s, LengthR m a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (StateR s (LengthR m a) -> s -> (s, LengthR m a)
forall s a. StateR s a -> s -> (s, a)
runStateR (StateR s (LengthR m a) -> s -> (s, LengthR m a))
-> (RangeR n m a -> StateR s (LengthR m a))
-> RangeR n m a
-> s
-> (s, LengthR m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateR s a -> RangeR n m a -> StateR s (LengthR m a)
forall (m :: * -> *) (n :: Nat) (w :: Nat) a.
(Monad m, Unfoldl n w w) =>
m a -> RangeR n w a -> m (LengthR w a)
unfoldlMWithBase ((s -> (s, a)) -> StateR s a
forall s a. (s -> (s, a)) -> StateR s a
StateR s -> (s, a)
f))

{-^

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

>>> :set -XDataKinds
>>> xs = NilR :++ 123 :+ 456 :: RangeR 1 5 Integer
>>> unfoldlWithBase (\n -> (n + 1, 2 * n)) 0 xs :: LengthR 5 Integer
((((NilR :+ 4) :+ 2) :+ 0) :+ 123) :+ 456

-}

unfoldlM :: (Monad m, 0 <= n, Unfoldl 0 n n) => m a -> m (LengthR n a)
unfoldlM :: m a -> m (LengthR n a)
unfoldlM = (m a -> RangeR 0 n a -> m (LengthR n a)
forall (m :: * -> *) (n :: Nat) (w :: Nat) a.
(Monad m, Unfoldl n w w) =>
m a -> RangeR n w a -> m (LengthR w a)
`unfoldlMWithBase` RangeR 0 n a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR)

{-^

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

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

-}

unfoldlMWithBase ::
	(Monad m, Unfoldl n w w) => m a -> RangeR n w a -> m (LengthR w a)
unfoldlMWithBase :: m a -> RangeR n w a -> m (LengthR w a)
unfoldlMWithBase = m Bool -> m a -> RangeR n w a -> m (LengthR w a)
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (RangeR v w a)
unfoldlMRangeWithBase m Bool
forall a. HasCallStack => a
undefined

{-^

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

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

-}

---------------------------------------------------------------------------
-- LIST TO LENGTH RIGHT
---------------------------------------------------------------------------

class ListToLengthR n where
	listToLengthR :: [a] -> Either (RangeR 0 (n - 1) a) (LengthR 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
	>>> listToLengthR @4 "Hi!"
	Left (((NilR :++ '!') :++ 'i') :++ 'H')
	>>> listToLengthR @4 "Hello!"
	Right ((((NilR :+ 'l') :+ 'l') :+ 'e') :+ 'H',"o!")

	-}

instance ListToLengthR 1 where
	listToLengthR :: [a] -> Either (RangeR 0 (1 - 1) a) (LengthR 1 a, [a])
listToLengthR = \case [] -> RangeR 0 0 a -> Either (RangeR 0 0 a) (LengthR 1 a, [a])
forall a b. a -> Either a b
Left RangeR 0 0 a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR; a
x : [a]
xs -> (LengthR 1 a, [a]) -> Either (RangeR 0 0 a) (LengthR 1 a, [a])
forall a b. b -> Either a b
Right (RangeR (1 - 1) (1 - 1) a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR RangeR (1 - 1) (1 - 1) a -> a -> LengthR 1 a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
x, [a]
xs)

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