{-# LANGUAGE BlockArguments, LambdaCase, TupleSections #-}
{-# LANGUAGE ScopedTypeVariables, InstanceSigs #-}
{-# LANGUAGE DataKinds, KindSignatures, TypeOperators #-}
{-# LANGUAGE GADTs, TypeFamilies #-}
{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,
	UndecidableInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}

module Data.List.Range.RangeL (
	LengthL,
	-- ** Type
	RangeL(..),
	-- ** PushL
	PushL, (.:..),
	-- ** AddL
	AddL, (++.),
	-- ** LoosenLMin and LoosenLMax
	-- *** loosenL
	loosenL,
	-- *** loosenLMin
	LoosenLMin, loosenLMin,
	-- *** loosenLMax
	LoosenLMax, loosenLMax,
	-- ** Unfoldr
	-- *** class
	Unfoldr,
	-- *** unfoldrRange
	-- **** without monad
	unfoldrRange, unfoldrRangeWithBase, unfoldrRangeWithBaseWithS,
	-- **** with monad
	unfoldrMRange, unfoldrMRangeWithBase,
	-- *** unfoldrRangeMaybe
	-- **** without monad
	unfoldrRangeMaybe, unfoldrRangeMaybeWithBase,
	-- **** with monad
	unfoldrMRangeMaybe, unfoldrMRangeMaybeWithBase,
	-- ** ZipL
	ZipL, zipL, zipWithL, zipWithML ) where

import GHC.TypeNats (Nat, type (+), type (-), type (<=))
import GHC.Exts (IsList(..))
import Control.Arrow (first, second, (***), (&&&))
import Control.Monad.Identity (Identity(..))
import Control.Monad.State (StateL(..))
import Data.Kind (Type)
import Data.Foldable (toList)
import Data.Bool (bool)
import Data.Maybe (isJust, fromMaybe)
import Data.String

type LengthL n = RangeL n n

{-^

The value of @LengthL n a@ is a list which have just @n@ members of type @a@.
You can push and pop an element from left.

>>> :set -XDataKinds
>>> sampleLengthL = 'h' :. 'e' :. 'l' :. 'l' :. 'o' :. NilL :: LengthL 5 Char

-}

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

-- * TYPE
--	+ RANGE LEFT
--	+ INSTANCE FUNCTOR
--	+ INSTANCE FOLDABLE
-- * PUSH
-- * ADD
-- * LOOSEN
-- 	+ LOOSEN LEFT
-- 	+ LOOSEN LEFT MIN
-- 	+ LOOSEN LEFT MAX
-- * UNFOLDR
-- 	+ CLASS
-- 	+ INSTANCE
-- 	+ UNFOLDR RANGE
-- 	+ UNFOLDR RANGE MAYBE
-- * ZIP
--	+ CLASS
--	+ FUNCTION

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

-- RANGE LEFT

data RangeL :: Nat -> Nat -> Type -> Type where
	NilL :: 0 <= m => RangeL 0 m a
	(:..) :: 1 <= m => a -> RangeL 0 (m - 1) a -> RangeL 0 m a
	(:.) :: (1 <= n, 1 <= m) =>
		a -> RangeL (n - 1) (m - 1) a -> RangeL n m a

{-^

The value of @RangeL n m a@ is a list of type @a@ values whose element number is
at minimum @n@, and at maximum @m@.
You can push and pop an element from left.

>>> :set -XDataKinds
>>> sampleRangeL = 'h' :. 'e' :. 'l' :. 'l' :.. 'o' :.. NilL :: RangeL 3 8 Char

-}

infixr 6 :., :..

deriving instance Show a => Show (RangeL n m a)

-- INSTANCE FUNCTOR

instance Functor (RangeL 0 0) where a -> b
_ fmap :: (a -> b) -> RangeL 0 0 a -> RangeL 0 0 b
`fmap` RangeL 0 0 a
NilL = RangeL 0 0 b
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL

instance {-# OVERLAPPABLE #-}
	Functor (RangeL 0 (m - 1)) => Functor (RangeL 0 m) where
	fmap :: (a -> b) -> RangeL 0 m a -> RangeL 0 m b
fmap a -> b
f = \case RangeL 0 m a
NilL -> RangeL 0 m b
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL; a
x :.. RangeL 0 (m - 1) a
xs -> a -> b
f a
x b -> RangeL 0 (m - 1) b -> RangeL 0 m b
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
:.. (a -> b
f (a -> b) -> RangeL 0 (m - 1) a -> RangeL 0 (m - 1) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeL 0 (m - 1) a
xs)

instance {-# OVERLAPPABLE #-}
	(1 <= n, Functor (RangeL (n - 1) (m - 1))) => Functor (RangeL n m) where
	a -> b
f fmap :: (a -> b) -> RangeL n m a -> RangeL n m b
`fmap` (a
x :. RangeL (n - 1) (m - 1) a
xs) = a -> b
f a
x b -> RangeL (n - 1) (m - 1) b -> RangeL n m b
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:. (a -> b
f (a -> b) -> RangeL (n - 1) (m - 1) a -> RangeL (n - 1) (m - 1) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeL (n - 1) (m - 1) a
xs)

-- INSTANCE FOLDABLE

instance Foldable (RangeL 0 0) where foldr :: (a -> b -> b) -> b -> RangeL 0 0 a -> b
foldr a -> b -> b
_ b
z RangeL 0 0 a
NilL = b
z

instance {-# OVERLAPPABLE #-}
	Foldable (RangeL 0 (m - 1)) => Foldable (RangeL 0 m) where
	foldr :: (a -> b -> b) -> b -> RangeL 0 m a -> b
foldr a -> b -> b
(-<) b
z = \case RangeL 0 m a
NilL -> b
z; a
x :.. RangeL 0 (m - 1) a
xs -> a
x a -> b -> b
-< (a -> b -> b) -> b -> RangeL 0 (m - 1) a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
(-<) b
z RangeL 0 (m - 1) a
xs

instance {-# OVERLAPPABLE #-} (1 <= n, Foldable (RangeL (n - 1) (m - 1))) =>
	Foldable (RangeL n m) where
	foldr :: (a -> b -> b) -> b -> RangeL n m a -> b
foldr a -> b -> b
(-<) b
z (a
x :. RangeL (n - 1) (m - 1) a
xs) = a
x a -> b -> b
-< (a -> b -> b) -> b -> RangeL (n - 1) (m - 1) a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
(-<) b
z RangeL (n - 1) (m - 1) a
xs

-- INSTANCE TRAVERSABLE

instance Traversable (RangeL 0 0) where traverse :: (a -> f b) -> RangeL 0 0 a -> f (RangeL 0 0 b)
traverse a -> f b
_ RangeL 0 0 a
NilL = RangeL 0 0 b -> f (RangeL 0 0 b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure RangeL 0 0 b
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL

instance {-# OVERLAPPABLE #-}
	Traversable (RangeL 0 (m - 1)) => Traversable (RangeL 0 m) where
	traverse :: (a -> f b) -> RangeL 0 m a -> f (RangeL 0 m b)
traverse a -> f b
f = \case
		RangeL 0 m a
NilL -> RangeL 0 m b -> f (RangeL 0 m b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure RangeL 0 m b
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL; a
x :.. RangeL 0 (m - 1) a
xs -> b -> RangeL 0 (m - 1) b -> RangeL 0 m b
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
(:..) (b -> RangeL 0 (m - 1) b -> RangeL 0 m b)
-> f b -> f (RangeL 0 (m - 1) b -> RangeL 0 m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x f (RangeL 0 (m - 1) b -> RangeL 0 m b)
-> f (RangeL 0 (m - 1) b) -> f (RangeL 0 m b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f b) -> RangeL 0 (m - 1) a -> f (RangeL 0 (m - 1) b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f RangeL 0 (m - 1) a
xs

instance {-# OVERLAPPABLE #-} (1 <= n, Traversable (RangeL (n - 1) (m - 1))) =>
	Traversable (RangeL n m) where
	traverse :: (a -> f b) -> RangeL n m a -> f (RangeL n m b)
traverse a -> f b
f (a
x :. RangeL (n - 1) (m - 1) a
xs) = b -> RangeL (n - 1) (m - 1) b -> RangeL n m b
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
(:.) (b -> RangeL (n - 1) (m - 1) b -> RangeL n m b)
-> f b -> f (RangeL (n - 1) (m - 1) b -> RangeL n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
f a
x f (RangeL (n - 1) (m - 1) b -> RangeL n m b)
-> f (RangeL (n - 1) (m - 1) b) -> f (RangeL n m b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (a -> f b)
-> RangeL (n - 1) (m - 1) a -> f (RangeL (n - 1) (m - 1) b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f RangeL (n - 1) (m - 1) a
xs

-- INSTANCE APPLICATIVE

instance Applicative (LengthL 0) where pure :: a -> LengthL 0 a
pure a
_ = LengthL 0 a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL; LengthL 0 (a -> b)
_ <*> :: LengthL 0 (a -> b) -> LengthL 0 a -> LengthL 0 b
<*> LengthL 0 a
_ = LengthL 0 b
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL

instance {-# OVERLAPPABLE #-} (Functor (RangeL 0 m), Applicative (RangeL 0 (m - 1)), Unfoldr 0 0 m) => Applicative (RangeL 0 m) where
	pure :: a -> RangeL 0 m a
pure = (a -> Bool) -> (a -> (a, a)) -> a -> RangeL 0 m a
forall (v :: Nat) (w :: Nat) s a.
Unfoldr 0 v w =>
(s -> Bool) -> (s -> (a, s)) -> s -> RangeL v w a
unfoldrRange (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
True) (\a
x -> (a
x, a
x))
	RangeL 0 m (a -> b)
NilL <*> :: RangeL 0 m (a -> b) -> RangeL 0 m a -> RangeL 0 m b
<*> RangeL 0 m a
_ = RangeL 0 m b
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL
	RangeL 0 m (a -> b)
_ <*> RangeL 0 m a
NilL = RangeL 0 m b
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL
	a -> b
f :.. RangeL 0 (m - 1) (a -> b)
fs <*> a
x :.. RangeL 0 (m - 1) a
xs = a -> b
f a
x b -> RangeL 0 (m - 1) b -> RangeL 0 m b
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
:.. (RangeL 0 (m - 1) (a -> b)
fs RangeL 0 (m - 1) (a -> b)
-> RangeL 0 (m - 1) a -> RangeL 0 (m - 1) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RangeL 0 (m - 1) a
xs)

instance {-# OVERLAPPABLE #-} (1 <= n, Functor (RangeL n m), Applicative (RangeL (n - 1) (m - 1)), Unfoldr 0 n m) => Applicative (RangeL n m) where
	pure :: a -> RangeL n m a
pure = (a -> Bool) -> (a -> (a, a)) -> a -> RangeL n m a
forall (v :: Nat) (w :: Nat) s a.
Unfoldr 0 v w =>
(s -> Bool) -> (s -> (a, s)) -> s -> RangeL v w a
unfoldrRange (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
True) (\a
x -> (a
x, a
x))
	a -> b
f :. RangeL (n - 1) (m - 1) (a -> b)
fs <*> :: RangeL n m (a -> b) -> RangeL n m a -> RangeL n m b
<*> a
x :. RangeL (n - 1) (m - 1) a
xs = a -> b
f a
x b -> RangeL (n - 1) (m - 1) b -> RangeL n m b
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:. (RangeL (n - 1) (m - 1) (a -> b)
fs RangeL (n - 1) (m - 1) (a -> b)
-> RangeL (n - 1) (m - 1) a -> RangeL (n - 1) (m - 1) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RangeL (n - 1) (m - 1) a
xs)

instance Applicative (LengthL 0) => Monad (LengthL 0) where
	LengthL 0 a
NilL >>= :: LengthL 0 a -> (a -> LengthL 0 b) -> LengthL 0 b
>>= a -> LengthL 0 b
_ = LengthL 0 b
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL

instance {-# OVERLAPPABLE #-} (1 <= n, Applicative (LengthL n), Monad (LengthL (n - 1))) => Monad (LengthL n) where
	a
x :. RangeL (n - 1) (n - 1) a
xs >>= :: LengthL n a -> (a -> LengthL n b) -> LengthL n b
>>= a -> LengthL n b
f = b
y b -> RangeL (n - 1) (n - 1) b -> LengthL n b
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
xs RangeL (n - 1) (n - 1) a
-> (a -> RangeL (n - 1) (n - 1) b) -> RangeL (n - 1) (n - 1) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
z -> case a -> LengthL n b
f a
z of b
_ :. RangeL (n - 1) (n - 1) b
zs -> RangeL (n - 1) (n - 1) b
zs)
		where b
y :. RangeL (n - 1) (n - 1) b
_ = a -> LengthL n b
f a
x

-- INSTANCE ISSTRING

instance Unfoldr 0 n m => IsString (RangeL n m Char) where
	fromString :: String -> RangeL n m Char
fromString String
s = RangeL n m Char -> Maybe (RangeL n m Char) -> RangeL n m Char
forall a. a -> Maybe a -> a
fromMaybe (String -> RangeL n m Char
forall a. HasCallStack => String -> a
error (String -> RangeL n m Char) -> String -> RangeL n m Char
forall a b. (a -> b) -> a -> b
$ String
"The string " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not within range.")
		(Maybe (RangeL n m Char) -> RangeL n m Char)
-> Maybe (RangeL n m Char) -> RangeL n m Char
forall a b. (a -> b) -> a -> b
$ (String -> Maybe (Char, String))
-> String -> Maybe (RangeL n m Char)
forall (v :: Nat) (w :: Nat) s a.
Unfoldr 0 v w =>
(s -> Maybe (a, s)) -> s -> Maybe (RangeL v w a)
unfoldrRangeMaybe (\case String
"" -> Maybe (Char, String)
forall a. Maybe a
Nothing; Char
c : String
cs -> (Char, String) -> Maybe (Char, String)
forall a. a -> Maybe a
Just (Char
c, String
cs)) String
s

instance (Foldable (RangeL n m), Unfoldr 0 n m) => IsList (RangeL n m a) where
	type Item (RangeL n m a) = a
	fromList :: [Item (RangeL n m a)] -> RangeL n m a
fromList [Item (RangeL n m a)]
lst = RangeL n m a -> Maybe (RangeL n m a) -> RangeL n m a
forall a. a -> Maybe a -> a
fromMaybe (String -> RangeL n m a
forall a. HasCallStack => String -> a
error (String -> RangeL n m a) -> String -> RangeL n m a
forall a b. (a -> b) -> a -> b
$ String
"The list is not within range.")
		(Maybe (RangeL n m a) -> RangeL n m a)
-> Maybe (RangeL n m a) -> RangeL n m a
forall a b. (a -> b) -> a -> b
$ ([a] -> Maybe (a, [a])) -> [a] -> Maybe (RangeL n m a)
forall (v :: Nat) (w :: Nat) s a.
Unfoldr 0 v w =>
(s -> Maybe (a, s)) -> s -> Maybe (RangeL v w a)
unfoldrRangeMaybe (\case [] -> Maybe (a, [a])
forall a. Maybe a
Nothing; a
x : [a]
xs -> (a, [a]) -> Maybe (a, [a])
forall a. a -> Maybe a
Just (a
x, [a]
xs)) [a]
[Item (RangeL n m a)]
lst
	toList :: RangeL n m a -> [Item (RangeL n m a)]
toList = RangeL n m a -> [Item (RangeL n m a)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Data.Foldable.toList

---------------------------------------------------------------------------
-- PUSH
---------------------------------------------------------------------------

infixr 5 .:..

class PushL n m where
	(.:..) :: a -> RangeL n m a -> RangeL n (m + 1) a

	{-^

	To push an optional element.

	>>> :set -XDataKinds
	>>> samplePushL = 'e' :. 'l' :. 'l' :. 'o' :.. NilL :: RangeL 3 7 Char
	>>> 'h' .:.. samplePushL
	'h' :. ('e' :. ('l' :. ('l' :.. ('o' :.. NilL))))
	>>> :type 'h' .:.. samplePushL
	'h' .:.. samplePushL :: RangeL 3 8 Char

	-}

instance PushL 0 m where
	.:.. :: a -> RangeL 0 m a -> RangeL 0 (m + 1) a
(.:..) a
x = \case RangeL 0 m a
NilL -> a
x a -> RangeL 0 ((m + 1) - 1) a -> RangeL 0 (m + 1) a
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
:.. RangeL 0 ((m + 1) - 1) a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL; xs :: RangeL 0 m a
xs@(a
_ :.. RangeL 0 (m - 1) a
_) -> a
x a -> RangeL 0 ((m + 1) - 1) a -> RangeL 0 (m + 1) a
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
:.. RangeL 0 m a
RangeL 0 ((m + 1) - 1) a
xs

instance {-# OVERLAPPABLE #-} (1 <= n, PushL (n - 1) (m - 1)) => PushL n m where
	a
x .:.. :: a -> RangeL n m a -> RangeL n (m + 1) a
.:.. a
y :. RangeL (n - 1) (m - 1) a
ys = a
x a -> RangeL (n - 1) ((m + 1) - 1) a -> RangeL n (m + 1) a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:. (a
y a -> RangeL (n - 1) (m - 1) a -> RangeL (n - 1) ((m - 1) + 1) a
forall (n :: Nat) (m :: Nat) a.
PushL n m =>
a -> RangeL n m a -> RangeL n (m + 1) a
.:.. RangeL (n - 1) (m - 1) a
ys)

---------------------------------------------------------------------------
-- ADD
---------------------------------------------------------------------------

infixr 5 ++.

class AddL n m v w where
	(++.) :: RangeL n m a -> RangeL v w a -> RangeL (n + v) (m + w) a

	{-^

	To concatenate two lists
	whose types are @RangeL n m a@ and @RangeL v w a@.

	>>> :set -XDataKinds
	>>> sampleAddL1 = 'f' :. 'o' :. 'o' :.. NilL :: RangeL 2 5 Char
	>>> sampleAddL2 = 'b' :. 'a' :.. 'r' :.. NilL :: RangeL 1 6 Char
	>>> sampleAddL1 ++. sampleAddL2
	'f' :. ('o' :. ('o' :. ('b' :.. ('a' :.. ('r' :.. NilL)))))
	>>> :type sampleAddL1 ++. sampleAddL2
	sampleAddL1 ++. sampleAddL2 :: RangeL 3 11 Char

	-}

instance AddL 0 0 v w where RangeL 0 0 a
NilL ++. :: RangeL 0 0 a -> RangeL v w a -> RangeL (0 + v) (0 + w) a
++. RangeL v w a
ys = RangeL v w a
RangeL (0 + v) (0 + w) a
ys

instance {-# OVERLAPPABLE #-}
	(PushL v (m + w - 1), AddL 0 (m - 1) v w, LoosenLMax v w (m + w)) =>
	AddL 0 m v w where
	(++.) :: forall a .  RangeL 0 m a -> RangeL v w a -> RangeL v (m + w) a
	RangeL 0 m a
NilL ++. :: RangeL 0 m a -> RangeL v w a -> RangeL v (m + w) a
++. RangeL v w a
ys = RangeL v w a -> RangeL v (m + w) a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenLMax n m w =>
RangeL n m a -> RangeL n w a
loosenLMax RangeL v w a
ys
	a
x :.. RangeL 0 (m - 1) a
xs ++. RangeL v w a
ys = a
x a -> RangeL v ((m + w) - 1) a -> RangeL v (((m + w) - 1) + 1) a
forall (n :: Nat) (m :: Nat) a.
PushL n m =>
a -> RangeL n m a -> RangeL n (m + 1) a
.:.. (RangeL 0 (m - 1) a
xs RangeL 0 (m - 1) a
-> RangeL v w a -> RangeL (0 + v) ((m - 1) + w) a
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a.
AddL n m v w =>
RangeL n m a -> RangeL v w a -> RangeL (n + v) (m + w) a
++. RangeL v w a
ys :: RangeL v (m + w - 1) a)

instance {-# OVERLAPPABLE #-}
	(1 <= n, AddL (n - 1) (m - 1) v w) => AddL n m v w where
	a
x :. RangeL (n - 1) (m - 1) a
xs ++. :: RangeL n m a -> RangeL v w a -> RangeL (n + v) (m + w) a
++. RangeL v w a
ys = a
x a
-> RangeL ((n + v) - 1) ((m + w) - 1) a -> RangeL (n + v) (m + w) 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) (m - 1) a
xs RangeL (n - 1) (m - 1) a
-> RangeL v w a -> RangeL ((n - 1) + v) ((m - 1) + w) a
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a.
AddL n m v w =>
RangeL n m a -> RangeL v w a -> RangeL (n + v) (m + w) a
++. RangeL v w a
ys)

---------------------------------------------------------------------------
-- LOOSEN
---------------------------------------------------------------------------

-- LOOSEN LEFT

loosenL :: (LoosenLMin n m v, LoosenLMax v m w) => RangeL n m a -> RangeL v w a
loosenL :: RangeL n m a -> RangeL v w a
loosenL = RangeL v m a -> RangeL v w a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenLMax n m w =>
RangeL n m a -> RangeL n w a
loosenLMax (RangeL v m a -> RangeL v w a)
-> (RangeL n m a -> RangeL v m a) -> RangeL n m a -> RangeL v w a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangeL n m a -> RangeL v m a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenLMin n m v =>
RangeL n m a -> RangeL v m a
loosenLMin

{-^

To loosen a range of an element number.

>>> :set -XDataKinds
>>> sampleLoosenL = 'h' :. 'e' :. 'l' :. 'l' :. 'o' :.. NilL :: RangeL 4 6 Char
>>> loosenL sampleLoosenL :: RangeL 2 8 Char
'h' :. ('e' :. ('l' :.. ('l' :.. ('o' :.. NilL))))

-}

-- LOOSEN LEFT MIN

class LoosenLMin n m v where
	loosenLMin :: RangeL n m a -> RangeL v m a

	{-^

	To loosen a lower bound of an element number.

	>>> :set -XDataKinds -fno-warn-tabs
	>>> :{
		sampleLoosenLMin :: RangeL 4 6 Char
		sampleLoosenLMin = 'h' :. 'e' :. 'l' :. 'l' :. 'o' :.. NilL
	:}

	>>> loosenLMin sampleLoosenLMin :: RangeL 2 6 Char
	'h' :. ('e' :. ('l' :.. ('l' :.. ('o' :.. NilL))))

	-}

instance LoosenLMin 0 m 0 where
	loosenLMin :: RangeL 0 m a -> RangeL 0 m a
loosenLMin = \case RangeL 0 m a
NilL -> RangeL 0 m a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL; xs :: RangeL 0 m a
xs@(a
_ :.. RangeL 0 (m - 1) a
_) -> RangeL 0 m a
xs

instance {-# OVERLAPPABLE #-}
	(1 <= n, LoosenLMin (n - 1) (m - 1) 0) => LoosenLMin n m 0 where
	loosenLMin :: RangeL n m a -> RangeL 0 m a
loosenLMin (a
x :. RangeL (n - 1) (m - 1) a
xs) = a
x a -> RangeL 0 (m - 1) a -> RangeL 0 m a
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
:.. RangeL (n - 1) (m - 1) a -> RangeL 0 (m - 1) a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenLMin n m v =>
RangeL n m a -> RangeL v m a
loosenLMin RangeL (n - 1) (m - 1) a
xs
	
instance {-# OVERLAPPABLE #-}
	(1 <= n, 1 <= v, LoosenLMin (n - 1) (m - 1) (v - 1)) => LoosenLMin n m v where
	loosenLMin :: RangeL n m a -> RangeL v m a
loosenLMin (a
x :. RangeL (n - 1) (m - 1) a
xs) = a
x a -> RangeL (v - 1) (m - 1) a -> RangeL v m 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) (m - 1) a -> RangeL (v - 1) (m - 1) a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenLMin n m v =>
RangeL n m a -> RangeL v m a
loosenLMin RangeL (n - 1) (m - 1) a
xs

-- LOOSEN LEFT MAX

class LoosenLMax n m w where
	loosenLMax :: RangeL n m a -> RangeL n w a

	{-^

	To loosen an upper bound of an element number.

	>>> :set -XDataKinds -fno-warn-tabs
	>>> :{
		sampleLoosenLMax :: RangeL 4 6 Char
		sampleLoosenLMax = 'h' :. 'e' :. 'l' :. 'l' :. 'o' :.. NilL
	:}

	>>> loosenLMax sampleLoosenLMax :: RangeL 4 8 Char
	'h' :. ('e' :. ('l' :. ('l' :. ('o' :.. NilL))))

	-}

instance LoosenLMax 0 0 w where loosenLMax :: RangeL 0 0 a -> RangeL 0 w a
loosenLMax RangeL 0 0 a
NilL = RangeL 0 w a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL

instance {-# OVERLAPPABLE #-}
	(1 <= w, LoosenLMax 0 (m - 1) (w - 1)) => LoosenLMax 0 m w where
	loosenLMax :: RangeL 0 m a -> RangeL 0 w a
loosenLMax = \case RangeL 0 m a
NilL -> RangeL 0 w a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL; (a
x :.. RangeL 0 (m - 1) a
xs) -> a
x a -> RangeL 0 (w - 1) a -> RangeL 0 w a
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
:.. RangeL 0 (m - 1) a -> RangeL 0 (w - 1) a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenLMax n m w =>
RangeL n m a -> RangeL n w a
loosenLMax RangeL 0 (m - 1) a
xs

instance {-# OVERLAPPABLE #-}
	(1 <= n, 1 <= w, LoosenLMax (n - 1) (m - 1) (w - 1)) => LoosenLMax n m w where
	loosenLMax :: RangeL n m a -> RangeL n w a
loosenLMax (a
x :. RangeL (n - 1) (m - 1) a
xs) = a
x a -> RangeL (n - 1) (w - 1) a -> RangeL n w 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) (m - 1) a -> RangeL (n - 1) (w - 1) a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenLMax n m w =>
RangeL n m a -> RangeL n w a
loosenLMax RangeL (n - 1) (m - 1) a
xs

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

-- CLASS

class Unfoldr n v w where
	unfoldrMRangeWithBase :: Monad m =>
		RangeL n w a -> m Bool -> m a -> m (RangeL v w a)

	{-^
	
	It is like @unfoldrMRange@. But it has already prepared values.

	>>> :set -XDataKinds
	>>> :module + Data.IORef
	>>> r <- newIORef 1
	>>> check = (< 3) <$> readIORef r
	>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
	>>> xs = 123 :. 456 :.. NilL :: RangeL 1 5 Integer
	>>> unfoldrMRangeWithBase xs check count :: IO (RangeL 3 5 Integer)
	123 :. (456 :. (3 :. (6 :.. NilL)))
	
	-}

	unfoldrMRangeMaybeWithBase :: Monad m =>
		RangeL n w a -> m Bool -> m a -> m (Maybe (RangeL v w a))

	{-^
	
	It is like @unfoldrMRangeMaybe@.
	But it has already prepared values.

	>>> :set -XDataKinds -fno-warn-tabs
	>>> :module + Data.IORef
	>>> r <- newIORef 1
	>>> check = (< 3) <$> readIORef r
	>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
	>>> xs = 123 :. 456 :.. NilL :: RangeL 1 5 Integer
	>>> :{
		unfoldrMRangeMaybeWithBase xs check count
			:: IO (Maybe (RangeL 3 5 Integer))
	:}
	Just (123 :. (456 :. (3 :. (6 :.. NilL))))
	
	-}

-- INSTANCE

instance Unfoldr 0 0 0 where
	unfoldrMRangeWithBase :: RangeL 0 0 a -> m Bool -> m a -> m (RangeL 0 0 a)
unfoldrMRangeWithBase RangeL 0 0 a
NilL m Bool
_ m a
_ = RangeL 0 0 a -> m (RangeL 0 0 a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure RangeL 0 0 a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL
	unfoldrMRangeMaybeWithBase :: RangeL 0 0 a -> m Bool -> m a -> m (Maybe (RangeL 0 0 a))
unfoldrMRangeMaybeWithBase RangeL 0 0 a
NilL m Bool
p m a
_ = Maybe (RangeL 0 0 a)
-> Maybe (RangeL 0 0 a) -> Bool -> Maybe (RangeL 0 0 a)
forall a. a -> a -> Bool -> a
bool (RangeL 0 0 a -> Maybe (RangeL 0 0 a)
forall a. a -> Maybe a
Just RangeL 0 0 a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL) Maybe (RangeL 0 0 a)
forall a. Maybe a
Nothing (Bool -> Maybe (RangeL 0 0 a))
-> m Bool -> m (Maybe (RangeL 0 0 a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool
p

instance {-# OVERLAPPABLE #-} (1 <= w, Unfoldr 0 0 (w - 1)) => Unfoldr 0 0 w where
	unfoldrMRangeWithBase :: RangeL 0 w a -> m Bool -> m a -> m (RangeL 0 w a)
unfoldrMRangeWithBase RangeL 0 w a
NilL m Bool
p m a
f =
		(m Bool
p m Bool -> (Bool -> m (RangeL 0 w a)) -> m (RangeL 0 w a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=) ((Bool -> m (RangeL 0 w a)) -> m (RangeL 0 w a))
-> (m (RangeL 0 w a) -> Bool -> m (RangeL 0 w a))
-> m (RangeL 0 w a)
-> m (RangeL 0 w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (RangeL 0 w a) -> m (RangeL 0 w a) -> Bool -> m (RangeL 0 w a)
forall a. a -> a -> Bool -> a
bool (RangeL 0 w a -> m (RangeL 0 w a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure RangeL 0 w a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL) (m (RangeL 0 w a) -> m (RangeL 0 w a))
-> m (RangeL 0 w a) -> m (RangeL 0 w a)
forall a b. (a -> b) -> a -> b
$ m a
f m a -> (a -> m (RangeL 0 w a)) -> m (RangeL 0 w a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x ->
			(a
x a -> RangeL 0 (w - 1) a -> RangeL 0 w a
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
:..) (RangeL 0 (w - 1) a -> RangeL 0 w a)
-> m (RangeL 0 (w - 1) a) -> m (RangeL 0 w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeL 0 (w - 1) a -> m Bool -> m a -> m (RangeL 0 (w - 1) 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 RangeL 0 (w - 1) a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL m Bool
p m a
f
	unfoldrMRangeWithBase (a
x :.. RangeL 0 (w - 1) a
xs) m Bool
p m a
f =
		(a
x a -> RangeL 0 (w - 1) a -> RangeL 0 w a
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
:..) (RangeL 0 (w - 1) a -> RangeL 0 w a)
-> m (RangeL 0 (w - 1) a) -> m (RangeL 0 w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeL 0 (w - 1) a -> m Bool -> m a -> m (RangeL 0 (w - 1) 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 RangeL 0 (w - 1) a
xs m Bool
p m a
f

	unfoldrMRangeMaybeWithBase :: RangeL 0 w a -> m Bool -> m a -> m (Maybe (RangeL 0 w a))
unfoldrMRangeMaybeWithBase RangeL 0 w a
NilL m Bool
p m a
f =
		(m Bool
p m Bool
-> (Bool -> m (Maybe (RangeL 0 w a))) -> m (Maybe (RangeL 0 w a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=) ((Bool -> m (Maybe (RangeL 0 w a))) -> m (Maybe (RangeL 0 w a)))
-> (m (Maybe (RangeL 0 w a)) -> Bool -> m (Maybe (RangeL 0 w a)))
-> m (Maybe (RangeL 0 w a))
-> m (Maybe (RangeL 0 w a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (RangeL 0 w a))
-> m (Maybe (RangeL 0 w a)) -> Bool -> m (Maybe (RangeL 0 w a))
forall a. a -> a -> Bool -> a
bool (Maybe (RangeL 0 w a) -> m (Maybe (RangeL 0 w a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (RangeL 0 w a) -> m (Maybe (RangeL 0 w a)))
-> Maybe (RangeL 0 w a) -> m (Maybe (RangeL 0 w a))
forall a b. (a -> b) -> a -> b
$ RangeL 0 w a -> Maybe (RangeL 0 w a)
forall a. a -> Maybe a
Just RangeL 0 w a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL) (m (Maybe (RangeL 0 w a)) -> m (Maybe (RangeL 0 w a)))
-> m (Maybe (RangeL 0 w a)) -> m (Maybe (RangeL 0 w a))
forall a b. (a -> b) -> a -> b
$ m a
f m a -> (a -> m (Maybe (RangeL 0 w a))) -> m (Maybe (RangeL 0 w a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x ->
			((a
x a -> RangeL 0 (w - 1) a -> RangeL 0 w a
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
:..) (RangeL 0 (w - 1) a -> RangeL 0 w a)
-> Maybe (RangeL 0 (w - 1) a) -> Maybe (RangeL 0 w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (RangeL 0 (w - 1) a) -> Maybe (RangeL 0 w a))
-> m (Maybe (RangeL 0 (w - 1) a)) -> m (Maybe (RangeL 0 w a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeL 0 (w - 1) a
-> m Bool -> m a -> m (Maybe (RangeL 0 (w - 1) 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 (Maybe (RangeL v w a))
unfoldrMRangeMaybeWithBase RangeL 0 (w - 1) a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL m Bool
p m a
f
	unfoldrMRangeMaybeWithBase (a
x :.. RangeL 0 (w - 1) a
xs) m Bool
p m a
f =
		((a
x a -> RangeL 0 (w - 1) a -> RangeL 0 w a
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
:..) (RangeL 0 (w - 1) a -> RangeL 0 w a)
-> Maybe (RangeL 0 (w - 1) a) -> Maybe (RangeL 0 w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (RangeL 0 (w - 1) a) -> Maybe (RangeL 0 w a))
-> m (Maybe (RangeL 0 (w - 1) a)) -> m (Maybe (RangeL 0 w a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeL 0 (w - 1) a
-> m Bool -> m a -> m (Maybe (RangeL 0 (w - 1) 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 (Maybe (RangeL v w a))
unfoldrMRangeMaybeWithBase RangeL 0 (w - 1) a
xs m Bool
p m a
f

instance {-# OVERLAPPABLE #-}
	(1 <= v, 1 <= w, Unfoldr 0 (v - 1) (w - 1)) => Unfoldr 0 v w where
	unfoldrMRangeWithBase :: RangeL 0 w a -> m Bool -> m a -> m (RangeL v w a)
unfoldrMRangeWithBase RangeL 0 w a
NilL m Bool
p m a
f =
		m a
f m a -> (a -> m (RangeL v w a)) -> m (RangeL v w a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x -> (a
x a -> RangeL (v - 1) (w - 1) a -> RangeL v w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:.) (RangeL (v - 1) (w - 1) a -> RangeL v w a)
-> m (RangeL (v - 1) (w - 1) a) -> m (RangeL v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeL 0 (w - 1) a -> m Bool -> m a -> m (RangeL (v - 1) (w - 1) 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 RangeL 0 (w - 1) a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL m Bool
p m a
f
	unfoldrMRangeWithBase (a
x :.. RangeL 0 (w - 1) a
xs) m Bool
p m a
f =
		(a
x a -> RangeL (v - 1) (w - 1) a -> RangeL v w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:.) (RangeL (v - 1) (w - 1) a -> RangeL v w a)
-> m (RangeL (v - 1) (w - 1) a) -> m (RangeL v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeL 0 (w - 1) a -> m Bool -> m a -> m (RangeL (v - 1) (w - 1) 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 RangeL 0 (w - 1) a
xs m Bool
p m a
f

	unfoldrMRangeMaybeWithBase :: RangeL 0 w a -> m Bool -> m a -> m (Maybe (RangeL v w a))
unfoldrMRangeMaybeWithBase RangeL 0 w a
NilL m Bool
p m a
f =
		(m Bool
p m Bool
-> (Bool -> m (Maybe (RangeL v w a))) -> m (Maybe (RangeL v w a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=) ((Bool -> m (Maybe (RangeL v w a))) -> m (Maybe (RangeL v w a)))
-> (m (Maybe (RangeL v w a)) -> Bool -> m (Maybe (RangeL v w a)))
-> m (Maybe (RangeL v w a))
-> m (Maybe (RangeL v w a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (RangeL v w a))
-> m (Maybe (RangeL v w a)) -> Bool -> m (Maybe (RangeL v w a))
forall a. a -> a -> Bool -> a
bool (Maybe (RangeL v w a) -> m (Maybe (RangeL v w a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (RangeL v w a)
forall a. Maybe a
Nothing) (m (Maybe (RangeL v w a)) -> m (Maybe (RangeL v w a)))
-> m (Maybe (RangeL v w a)) -> m (Maybe (RangeL v w a))
forall a b. (a -> b) -> a -> b
$ m a
f m a -> (a -> m (Maybe (RangeL v w a))) -> m (Maybe (RangeL v w a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x ->
			((a
x a -> RangeL (v - 1) (w - 1) a -> RangeL v w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:.) (RangeL (v - 1) (w - 1) a -> RangeL v w a)
-> Maybe (RangeL (v - 1) (w - 1) a) -> Maybe (RangeL v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (RangeL (v - 1) (w - 1) a) -> Maybe (RangeL v w a))
-> m (Maybe (RangeL (v - 1) (w - 1) a)) -> m (Maybe (RangeL v w a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeL 0 (w - 1) a
-> m Bool -> m a -> m (Maybe (RangeL (v - 1) (w - 1) 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 (Maybe (RangeL v w a))
unfoldrMRangeMaybeWithBase RangeL 0 (w - 1) a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL m Bool
p m a
f
	unfoldrMRangeMaybeWithBase (a
x :.. RangeL 0 (w - 1) a
xs) m Bool
p m a
f =
		((a
x a -> RangeL (v - 1) (w - 1) a -> RangeL v w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:.) (RangeL (v - 1) (w - 1) a -> RangeL v w a)
-> Maybe (RangeL (v - 1) (w - 1) a) -> Maybe (RangeL v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (RangeL (v - 1) (w - 1) a) -> Maybe (RangeL v w a))
-> m (Maybe (RangeL (v - 1) (w - 1) a)) -> m (Maybe (RangeL v w a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeL 0 (w - 1) a
-> m Bool -> m a -> m (Maybe (RangeL (v - 1) (w - 1) 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 (Maybe (RangeL v w a))
unfoldrMRangeMaybeWithBase RangeL 0 (w - 1) a
xs m Bool
p m a
f

instance {-# OVERLAPPABLE #-}
	(1 <= n, 1 <= v, Unfoldr (n - 1) (v - 1) (w - 1)) => Unfoldr n v w where
	unfoldrMRangeWithBase :: RangeL n w a -> m Bool -> m a -> m (RangeL v w a)
unfoldrMRangeWithBase (a
x :. RangeL (n - 1) (w - 1) a
xs) m Bool
p m a
f =
		(a
x a -> RangeL (v - 1) (w - 1) a -> RangeL v w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:.) (RangeL (v - 1) (w - 1) a -> RangeL v w a)
-> m (RangeL (v - 1) (w - 1) a) -> m (RangeL v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeL (n - 1) (w - 1) a
-> m Bool -> m a -> m (RangeL (v - 1) (w - 1) 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 RangeL (n - 1) (w - 1) a
xs m Bool
p m a
f

	unfoldrMRangeMaybeWithBase :: RangeL n w a -> m Bool -> m a -> m (Maybe (RangeL v w a))
unfoldrMRangeMaybeWithBase (a
x :. RangeL (n - 1) (w - 1) a
xs) m Bool
p m a
f =
		((a
x a -> RangeL (v - 1) (w - 1) a -> RangeL v w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:.) (RangeL (v - 1) (w - 1) a -> RangeL v w a)
-> Maybe (RangeL (v - 1) (w - 1) a) -> Maybe (RangeL v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (RangeL (v - 1) (w - 1) a) -> Maybe (RangeL v w a))
-> m (Maybe (RangeL (v - 1) (w - 1) a)) -> m (Maybe (RangeL v w a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeL (n - 1) (w - 1) a
-> m Bool -> m a -> m (Maybe (RangeL (v - 1) (w - 1) 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 (Maybe (RangeL v w a))
unfoldrMRangeMaybeWithBase RangeL (n - 1) (w - 1) a
xs m Bool
p m a
f

-- UNFOLDR RANGE

unfoldrRange :: Unfoldr 0 v w =>
	(s -> Bool) -> (s -> (a, s)) -> s -> RangeL v w a
unfoldrRange :: (s -> Bool) -> (s -> (a, s)) -> s -> RangeL v w a
unfoldrRange = RangeL 0 w a -> (s -> Bool) -> (s -> (a, s)) -> s -> RangeL v w a
forall (n :: Nat) (v :: Nat) (w :: Nat) a s.
Unfoldr n v w =>
RangeL n w a -> (s -> Bool) -> (s -> (a, s)) -> s -> RangeL v w a
unfoldrRangeWithBase RangeL 0 w a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL

{-^

To evaluate a function to construct a list.
The function recieve a state and return an element and a new state.
First argument is a predication which is evaluated
when an element number is greater than a minimum and not greater than a maximum.

>>> :set -XDataKinds
>>> next n = (n * 3, n + 1)
>>> unfoldrRange (< 2) next 1 :: RangeL 3 5 Int
3 :. (6 :. (9 :. NilL))

>>> unfoldrRange (< 5) next 1 :: RangeL 3 5 Int
3 :. (6 :. (9 :. (12 :.. NilL)))

>>> unfoldrRange (< 10) next 1 :: RangeL 3 5 Int
3 :. (6 :. (9 :. (12 :.. (15 :.. NilL))))

-}

unfoldrRangeWithBase :: Unfoldr n v w =>
	RangeL n w a -> (s -> Bool) -> (s -> (a, s)) -> s -> RangeL v w a
unfoldrRangeWithBase :: RangeL n w a -> (s -> Bool) -> (s -> (a, s)) -> s -> RangeL v w a
unfoldrRangeWithBase RangeL n w a
xs s -> Bool
p s -> (a, s)
f = (RangeL v w a, s) -> RangeL v w a
forall a b. (a, b) -> a
fst ((RangeL v w a, s) -> RangeL v w a)
-> (s -> (RangeL v w a, s)) -> s -> RangeL v w a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangeL n w a
-> (s -> Bool) -> (s -> (a, s)) -> s -> (RangeL v w a, s)
forall (n :: Nat) (v :: Nat) (w :: Nat) a s.
Unfoldr n v w =>
RangeL n w a
-> (s -> Bool) -> (s -> (a, s)) -> s -> (RangeL v w a, s)
unfoldrRangeWithBaseWithS RangeL n w a
xs s -> Bool
p s -> (a, s)
f

{-^

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

>>> :set -XDataKinds
>>> xs = 123 :. 456 :.. NilL :: RangeL 1 5 Integer
>>> unfoldrRangeWithBase xs (< 3) (\n -> (n * 3, n + 1)) 1 :: RangeL 3 5 Integer
123 :. (456 :. (3 :. (6 :.. NilL)))

-}

unfoldrRangeWithBaseWithS :: Unfoldr n v w =>
	RangeL n w a -> (s -> Bool) -> (s -> (a, s)) -> s -> (RangeL v w a, s)
unfoldrRangeWithBaseWithS :: RangeL n w a
-> (s -> Bool) -> (s -> (a, s)) -> s -> (RangeL v w a, s)
unfoldrRangeWithBaseWithS RangeL n w a
xs s -> Bool
p s -> (a, s)
f =
	StateL s (RangeL v w a) -> s -> (RangeL v w a, s)
forall s a. StateL s a -> s -> (a, s)
runStateL (StateL s (RangeL v w a) -> s -> (RangeL v w a, s))
-> StateL s (RangeL v w a) -> s -> (RangeL v w a, s)
forall a b. (a -> b) -> a -> b
$ RangeL n w a
-> StateL s Bool -> StateL s a -> StateL s (RangeL v 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 RangeL n w a
xs ((s -> (Bool, s)) -> StateL s Bool
forall s a. (s -> (a, s)) -> StateL s a
StateL ((s -> (Bool, s)) -> StateL s Bool)
-> (s -> (Bool, s)) -> StateL s Bool
forall a b. (a -> b) -> a -> b
$ s -> Bool
p (s -> Bool) -> (s -> s) -> s -> (Bool, s)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& s -> s
forall a. a -> a
id) ((s -> (a, s)) -> StateL s a
forall s a. (s -> (a, s)) -> StateL s a
StateL s -> (a, s)
f)

{-^

It is like @unfoldrRangeWithBase@.
But it return not only a list but also a state value.

>>> :set -XDataKinds
>>> next n = (n * 3, n + 1)
>>> xs = 123 :. 456 :.. NilL :: RangeL 1 5 Integer
>>> unfoldrRangeWithBaseWithS xs (< 3) next 1 :: (RangeL 3 5 Integer, Integer)
(123 :. (456 :. (3 :. (6 :.. NilL))),3)

-}

unfoldrMRange :: (Unfoldr 0 v w, Monad m) => m Bool -> m a -> m (RangeL v w a)
unfoldrMRange :: m Bool -> m a -> m (RangeL v w a)
unfoldrMRange = RangeL 0 w a -> m Bool -> m a -> m (RangeL v 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 RangeL 0 w a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL

{-^

It is like @unfoldrRange@. But it use a monad instead of a function.

>>> :set -XDataKinds
>>> :module + Data.IORef
>>> r <- newIORef 1
>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
>>> unfoldrMRange ((< 5) <$> readIORef r) count :: IO (RangeL 3 5 Integer)
3 :. (6 :. (9 :. (12 :.. NilL)))

-}

-- UNFOLDR RANGE MAYBE

unfoldrRangeMaybe :: Unfoldr 0 v w =>
	(s -> Maybe (a, s)) -> s -> Maybe (RangeL v w a)
unfoldrRangeMaybe :: (s -> Maybe (a, s)) -> s -> Maybe (RangeL v w a)
unfoldrRangeMaybe = RangeL 0 w a -> (s -> Maybe (a, s)) -> s -> Maybe (RangeL v w a)
forall (n :: Nat) (v :: Nat) (w :: Nat) a s.
Unfoldr n v w =>
RangeL n w a -> (s -> Maybe (a, s)) -> s -> Maybe (RangeL v w a)
unfoldrRangeMaybeWithBase RangeL 0 w a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL

{-^

To eveluate a function to construct a list.
The function recieve a state and
return a nothing value or an element and a new state.
If number of created elements is less than a minimum number of list elements or
greater than a maximum number, then return Nothing.

>>> :set -XDataKinds
>>> next n0 n = if n < n0 then Just (n * 3, n + 1) else Nothing
>>> unfoldrRangeMaybe (next 2) 1 :: Maybe (RangeL 3 5 Int)
Nothing

>>> unfoldrRangeMaybe (next 5) 1 :: Maybe (RangeL 3 5 Int)
Just (3 :. (6 :. (9 :. (12 :.. NilL))))

>>> unfoldrRangeMaybe (next 10) 1 :: Maybe (RangeL 3 5 Int)
Nothing

-}

unfoldrRangeMaybeWithBase :: Unfoldr n v w =>
	RangeL n w a -> (s -> Maybe (a, s)) -> s -> Maybe (RangeL v w a)
unfoldrRangeMaybeWithBase :: RangeL n w a -> (s -> Maybe (a, s)) -> s -> Maybe (RangeL v w a)
unfoldrRangeMaybeWithBase RangeL n w a
xs s -> Maybe (a, s)
f =
	(Maybe (RangeL v w a), Maybe (a, s)) -> Maybe (RangeL v w a)
forall a b. (a, b) -> a
fst ((Maybe (RangeL v w a), Maybe (a, s)) -> Maybe (RangeL v w a))
-> (s -> (Maybe (RangeL v w a), Maybe (a, s)))
-> s
-> Maybe (RangeL v w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangeL n w a
-> St a s Bool -> St a s a -> St a s (Maybe (RangeL v w a))
forall (n :: Nat) (v :: Nat) (w :: Nat) a s.
Unfoldr n v w =>
RangeL n w a
-> St a s Bool -> St a s a -> St a s (Maybe (RangeL v w a))
unfoldrRangeMaybeWithBaseGen RangeL n w a
xs (Maybe (a, s) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (a, s) -> Bool)
-> (Maybe (a, s) -> Maybe (a, s)) -> St a s Bool
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Maybe (a, s) -> Maybe (a, s)
forall a. a -> a
id)
		((a, Maybe (a, s)) -> ((a, s) -> (a, Maybe (a, s))) -> St a s a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> (a, Maybe (a, s))
forall a. HasCallStack => String -> a
error String
"never occur") (s -> Maybe (a, s)
f (s -> Maybe (a, s)) -> (a, s) -> (a, Maybe (a, s))
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
`second`)) St a s (Maybe (RangeL v w a))
-> (s -> Maybe (a, s)) -> s -> (Maybe (RangeL v w a), Maybe (a, s))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> Maybe (a, s)
f

{-^

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

>>> :set -XDataKinds
>>> xs = 123 :. 456 :.. NilL :: RangeL 1 5 Int
>>> next n = if n < 3 then Just (n * 3, n + 1) else Nothing
>>> unfoldrRangeMaybeWithBase xs next 1 :: Maybe (RangeL 3 5 Int)
Just (123 :. (456 :. (3 :. (6 :.. NilL))))

-}

type St a s r = Maybe (a, s) -> (r, Maybe (a, s))

unfoldrRangeMaybeWithBaseGen :: Unfoldr n v w =>
	RangeL n w a -> St a s Bool -> St a s a -> St a s (Maybe (RangeL v w a))
unfoldrRangeMaybeWithBaseGen :: RangeL n w a
-> St a s Bool -> St a s a -> St a s (Maybe (RangeL v w a))
unfoldrRangeMaybeWithBaseGen RangeL n w a
xs St a s Bool
p St a s a
f =
	StateL (Maybe (a, s)) (Maybe (RangeL v w a))
-> St a s (Maybe (RangeL v w a))
forall s a. StateL s a -> s -> (a, s)
runStateL (StateL (Maybe (a, s)) (Maybe (RangeL v w a))
 -> St a s (Maybe (RangeL v w a)))
-> StateL (Maybe (a, s)) (Maybe (RangeL v w a))
-> St a s (Maybe (RangeL v w a))
forall a b. (a -> b) -> a -> b
$ RangeL n w a
-> StateL (Maybe (a, s)) Bool
-> StateL (Maybe (a, s)) a
-> StateL (Maybe (a, s)) (Maybe (RangeL v 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 (Maybe (RangeL v w a))
unfoldrMRangeMaybeWithBase RangeL n w a
xs (St a s Bool -> StateL (Maybe (a, s)) Bool
forall s a. (s -> (a, s)) -> StateL s a
StateL St a s Bool
p) (St a s a -> StateL (Maybe (a, s)) a
forall s a. (s -> (a, s)) -> StateL s a
StateL St a s a
f)

unfoldrMRangeMaybe :: (Unfoldr 0 v w, Monad m) =>
	m Bool -> m a -> m (Maybe (RangeL v w a))
unfoldrMRangeMaybe :: m Bool -> m a -> m (Maybe (RangeL v w a))
unfoldrMRangeMaybe = RangeL 0 w a -> m Bool -> m a -> m (Maybe (RangeL v 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 (Maybe (RangeL v w a))
unfoldrMRangeMaybeWithBase RangeL 0 w a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL

{-^

It is like @unfoldrRangeMaybe@.
But it use a monad instead of a function.
The first argument monad return boolean value.
It create values while this boolean value is True.
If this boolean value is False before to create enough values or
True after to create full values, then @unfoldrMRangeMaybe@ return Nothing.

>>> :set -XDataKinds
>>> :module + Data.IORef
>>> r <- newIORef 1
>>> check n0 = (< n0) <$> readIORef r
>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)
>>> unfoldrMRangeMaybe (check 2) count :: IO (Maybe (RangeL 3 5 Integer))
Nothing

>>> writeIORef r 1
>>> unfoldrMRangeMaybe (check 5) count :: IO (Maybe (RangeL 3 5 Integer))
Just (3 :. (6 :. (9 :. (12 :.. NilL))))

>>> writeIORef r 1
>>> unfoldrMRangeMaybe (check 10) count :: IO (Maybe (RangeL 3 5 Integer))
Nothing

-}

---------------------------------------------------------------------------
-- ZIP
---------------------------------------------------------------------------

-- CLASS

class ZipL n m v w where
	zipWithML :: Monad q =>
		(a -> b -> q c) -> RangeL n m a -> RangeL v w b ->
		q (RangeL n m c, RangeL (v - m) (w - n) b)

	{-^

	It is like @zipWithL@.
	But it use a function which return a monad instead of a simple value.

	>>> :set -XDataKinds -fno-warn-tabs
	>>> ns = 1 :. 2 :. 3 :.. NilL :: RangeL 2 4 Int
	>>> :{
		cs :: RangeL 5 7 Char
		cs = 'a' :. 'b' :. 'c' :. 'd' :. 'e' :. 'f' :.. NilL
	:}

	>>> zipWithML (\n -> putStrLn . replicate n) ns cs
	a
	bb
	ccc
	(() :. (() :. (() :.. NilL)),'d' :. ('e' :.. ('f' :.. NilL)))

	-}

instance ZipL 0 0 v w where zipWithML :: (a -> b -> q c)
-> RangeL 0 0 a
-> RangeL v w b
-> q (RangeL 0 0 c, RangeL (v - 0) (w - 0) b)
zipWithML a -> b -> q c
_ RangeL 0 0 a
NilL = (RangeL 0 0 c, RangeL v w b) -> q (RangeL 0 0 c, RangeL v w b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((RangeL 0 0 c, RangeL v w b) -> q (RangeL 0 0 c, RangeL v w b))
-> (RangeL v w b -> (RangeL 0 0 c, RangeL v w b))
-> RangeL v w b
-> q (RangeL 0 0 c, RangeL v w b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RangeL 0 0 c
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL ,)

instance {-# OVERLAPPABLE #-} (
	1 <= v, m <= v, LoosenLMin v w (v - m), LoosenLMax (v - m) (w - 1) w,
	ZipL 0 (m - 1) (v - 1) (w - 1) ) => ZipL 0 m v w where
	zipWithML :: (a -> b -> q c)
-> RangeL 0 m a
-> RangeL v w b
-> q (RangeL 0 m c, RangeL (v - m) (w - 0) b)
zipWithML a -> b -> q c
_ RangeL 0 m a
NilL RangeL v w b
ys = (RangeL 0 m c, RangeL (v - m) w b)
-> q (RangeL 0 m c, RangeL (v - m) w b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RangeL 0 m c
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL, RangeL v w b -> RangeL (v - m) w b
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenLMin n m v =>
RangeL n m a -> RangeL v m a
loosenLMin RangeL v w b
ys)
	zipWithML a -> b -> q c
(%) (a
x :.. RangeL 0 (m - 1) a
xs) (b
y :. RangeL (v - 1) (w - 1) b
ys) =
		a
x a -> b -> q c
% b
y q c
-> (c -> q (RangeL 0 m c, RangeL (v - m) w b))
-> q (RangeL 0 m c, RangeL (v - m) w b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c
z -> ((c
z c -> RangeL 0 (m - 1) c -> RangeL 0 m c
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
:..) (RangeL 0 (m - 1) c -> RangeL 0 m c)
-> (RangeL (v - m) (w - 1) b -> RangeL (v - m) w b)
-> (RangeL 0 (m - 1) c, RangeL (v - m) (w - 1) b)
-> (RangeL 0 m c, RangeL (v - m) w b)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** RangeL (v - m) (w - 1) b -> RangeL (v - m) w b
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenLMax n m w =>
RangeL n m a -> RangeL n w a
loosenLMax) ((RangeL 0 (m - 1) c, RangeL (v - m) (w - 1) b)
 -> (RangeL 0 m c, RangeL (v - m) w b))
-> q (RangeL 0 (m - 1) c, RangeL (v - m) (w - 1) b)
-> q (RangeL 0 m c, RangeL (v - m) w b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> b -> q c)
-> RangeL 0 (m - 1) a
-> RangeL (v - 1) (w - 1) b
-> q (RangeL 0 (m - 1) c,
      RangeL ((v - 1) - (m - 1)) ((w - 1) - 0) b)
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) (q :: * -> *) a
       b c.
(ZipL n m v w, Monad q) =>
(a -> b -> q c)
-> RangeL n m a
-> RangeL v w b
-> q (RangeL n m c, RangeL (v - m) (w - n) b)
zipWithML a -> b -> q c
(%) RangeL 0 (m - 1) a
xs RangeL (v - 1) (w - 1) b
ys

instance {-# OVERLAPPABLE #-} (
	1 <= n, 1 <= v, n <= w, m <= v,
	ZipL (n - 1) (m - 1) (v - 1) (w - 1) ) => ZipL n m v w where
	zipWithML :: (a -> b -> q c)
-> RangeL n m a
-> RangeL v w b
-> q (RangeL n m c, RangeL (v - m) (w - n) b)
zipWithML a -> b -> q c
(%) (a
x :. RangeL (n - 1) (m - 1) a
xs) (b
y :. RangeL (v - 1) (w - 1) b
ys) =
		a
x a -> b -> q c
% b
y q c
-> (c
    -> q (RangeL n m c,
          RangeL ((v - 1) - (m - 1)) ((w - 1) - (n - 1)) b))
-> q (RangeL n m c,
      RangeL ((v - 1) - (m - 1)) ((w - 1) - (n - 1)) b)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c
z -> ((c
z c -> RangeL (n - 1) (m - 1) c -> RangeL n m c
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:.) (RangeL (n - 1) (m - 1) c -> RangeL n m c)
-> (RangeL (n - 1) (m - 1) c,
    RangeL ((v - 1) - (m - 1)) ((w - 1) - (n - 1)) b)
-> (RangeL n m c, RangeL ((v - 1) - (m - 1)) ((w - 1) - (n - 1)) b)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
`first`) ((RangeL (n - 1) (m - 1) c,
  RangeL ((v - 1) - (m - 1)) ((w - 1) - (n - 1)) b)
 -> (RangeL n m c,
     RangeL ((v - 1) - (m - 1)) ((w - 1) - (n - 1)) b))
-> q (RangeL (n - 1) (m - 1) c,
      RangeL ((v - 1) - (m - 1)) ((w - 1) - (n - 1)) b)
-> q (RangeL n m c,
      RangeL ((v - 1) - (m - 1)) ((w - 1) - (n - 1)) b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> b -> q c)
-> RangeL (n - 1) (m - 1) a
-> RangeL (v - 1) (w - 1) b
-> q (RangeL (n - 1) (m - 1) c,
      RangeL ((v - 1) - (m - 1)) ((w - 1) - (n - 1)) b)
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) (q :: * -> *) a
       b c.
(ZipL n m v w, Monad q) =>
(a -> b -> q c)
-> RangeL n m a
-> RangeL v w b
-> q (RangeL n m c, RangeL (v - m) (w - n) b)
zipWithML a -> b -> q c
(%) RangeL (n - 1) (m - 1) a
xs RangeL (v - 1) (w - 1) b
ys

-- FUNCTION

zipL :: ZipL n m v w => RangeL n m a -> RangeL v w b ->
	(RangeL n m (a, b), RangeL (v - m) (w - n) b)
zipL :: RangeL n m a
-> RangeL v w b -> (RangeL n m (a, b), RangeL (v - m) (w - n) b)
zipL = (a -> b -> (a, b))
-> RangeL n m a
-> RangeL v w b
-> (RangeL n m (a, b), RangeL (v - m) (w - n) b)
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a b c.
ZipL n m v w =>
(a -> b -> c)
-> RangeL n m a
-> RangeL v w b
-> (RangeL n m c, RangeL (v - m) (w - n) b)
zipWithL (,)

{-^

To recieve two lists and return a tuple list and rest of the second list.
The first list must be shorter or equal than the second list.

>>> :set -XDataKinds
>>> sampleZipL1 = 1 :. 2 :. 3 :.. NilL :: RangeL 2 4 Integer
>>> sampleZipL2 = 7 :. 6 :. 5 :. 4 :. 3 :. 2 :.. NilL :: RangeL 5 7 Integer
>>> zipL sampleZipL1 sampleZipL2
((1,7) :. ((2,6) :. ((3,5) :.. NilL)),4 :. (3 :.. (2 :.. NilL)))
>>> :type zipL sampleZipL1 sampleZipL2
zipL sampleZipL1 sampleZipL2
  :: (RangeL 2 4 (Integer, Integer), RangeL 1 5 Integer)

-}

zipWithL :: ZipL n m v w => (a -> b -> c) -> RangeL n m a -> RangeL v w b ->
	(RangeL n m c, RangeL (v - m) (w - n) b)
zipWithL :: (a -> b -> c)
-> RangeL n m a
-> RangeL v w b
-> (RangeL n m c, RangeL (v - m) (w - n) b)
zipWithL a -> b -> c
op = (Identity (RangeL n m c, RangeL (v - m) (w - n) b)
-> (RangeL n m c, RangeL (v - m) (w - n) b)
forall a. Identity a -> a
runIdentity (Identity (RangeL n m c, RangeL (v - m) (w - n) b)
 -> (RangeL n m c, RangeL (v - m) (w - n) b))
-> (RangeL v w b
    -> Identity (RangeL n m c, RangeL (v - m) (w - n) b))
-> RangeL v w b
-> (RangeL n m c, RangeL (v - m) (w - n) b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((RangeL v w b
  -> Identity (RangeL n m c, RangeL (v - m) (w - n) b))
 -> RangeL v w b -> (RangeL n m c, RangeL (v - m) (w - n) b))
-> (RangeL n m a
    -> RangeL v w b
    -> Identity (RangeL n m c, RangeL (v - m) (w - n) b))
-> RangeL n m a
-> RangeL v w b
-> (RangeL n m c, RangeL (v - m) (w - n) b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b -> Identity c)
-> RangeL n m a
-> RangeL v w b
-> Identity (RangeL n m c, RangeL (v - m) (w - n) b)
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) (q :: * -> *) a
       b c.
(ZipL n m v w, Monad q) =>
(a -> b -> q c)
-> RangeL n m a
-> RangeL v w b
-> q (RangeL n m c, RangeL (v - m) (w - n) b)
zipWithML ((c -> Identity c
forall a. a -> Identity a
Identity (c -> Identity c) -> (b -> c) -> b -> Identity c
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((b -> c) -> b -> Identity c)
-> (a -> b -> c) -> a -> b -> Identity c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> c
op)

{-^

It is like @zipL@.
But it evaluate a function to make values instead of put together in tuples.

>>> :set -XDataKinds
>>> sampleZipWithL1 = 1 :. 2 :. 3 :.. NilL :: RangeL 2 4 Integer
>>> sampleZipWithL2 = 7 :. 6 :. 5 :. 4 :. 3 :. 2 :.. NilL :: RangeL 5 7 Integer
>>> zipWithL (+) sampleZipWithL1 sampleZipWithL2
(8 :. (8 :. (8 :.. NilL)),4 :. (3 :.. (2 :.. NilL)))
>>> :type zipWithL (+) sampleZipWithL1 sampleZipWithL2
zipWithL (+) sampleZipWithL1 sampleZipWithL2
  :: (RangeL 2 4 Integer, RangeL 1 5 Integer)

-}