{-# LANGUAGE LambdaCase #-}
{-# 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.RangeR (
	-- ** Type
	RangeR(..),
	-- ** PushR
	PushR, (.:++),
	-- ** AddR
	AddR, (+++),
	-- ** LoosenRMin and LoosenRMax
	-- *** loosenR
	loosenR,
	-- *** loosenRMin
	LoosenRMin, loosenRMin,
	-- *** loosenRMax
	LoosenRMax, loosenRMax,
	-- ** Unfoldl
	-- *** class
	Unfoldl,
	-- *** unfoldlRange
	-- **** without monad
	unfoldlRange, unfoldlRangeWithBase, unfoldlRangeWithBaseWithS,
	-- **** with monad
	unfoldlMRange, unfoldlMRangeWithBase,
	-- *** unfoldlRangeMaybe
	-- **** without monad
	unfoldlRangeMaybe, unfoldlRangeMaybeWithBase,
	-- **** with monad
	unfoldlMRangeMaybe, unfoldlMRangeMaybeWithBase,
	-- ** ZipR
	ZipR, zipR, zipWithR, zipWithMR ) where

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

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

-- * TYPE
--	+ RANGE RIGHT
--	+ INSTANCE FUNCTOR
--	+ INSTANCE FOLDABLE
-- * PUSH
-- * ADD
-- * LOOSEN
--	+ LOOSEN RIGHT
--	+ LOOSEN RIGHT MIN
--	+ LOOSEN RIGHT MAX
-- * UNFOLDL
--	+ CLASS
--	+ INSTANCE
--	+ UNFOLDL RANGE
--	+ UNFOLDL RANGE MAYBE
-- * ZIP
--	+ CLASS AND INSTANCE
--	+ FUNCTION

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

-- RANGE RIGHT

data RangeR :: Nat -> Nat -> Type -> Type where
	NilR :: 0 <= m => RangeR 0 m a
	(:++) :: 1 <= m => RangeR 0 (m - 1) a -> a -> RangeR 0 m a
	(:+) :: (1 <= n, 1 <= m) =>
		RangeR (n - 1) (m - 1) a -> a -> RangeR n m a

{-^

@RangeR 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 right.

>>> :set -XDataKinds
>>> sampleRangeR = NilR :++ 'h' :++ 'e' :+ 'l' :+ 'l' :+ 'o' :: RangeR 3 8 Char

-}

infixl 6 :+, :++

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

-- INSTANCE FUNCTOR

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

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

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

-- INSTANCE FOLDABLE

instance Foldable (RangeR 0 0) where foldr :: (a -> b -> b) -> b -> RangeR 0 0 a -> b
foldr a -> b -> b
_ b
z RangeR 0 0 a
NilR = b
z

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

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

-- INSTANCE TRAVERSABLE

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

instance {-# OVERLAPPABLE #-}
	Traversable (RangeR 0 (m - 1)) => Traversable (RangeR 0 m) where
	traverse :: (a -> f b) -> RangeR 0 m a -> f (RangeR 0 m b)
traverse a -> f b
f = \case
		RangeR 0 m a
NilR -> RangeR 0 m b -> f (RangeR 0 m b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure RangeR 0 m b
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR; RangeR 0 (m - 1) a
xs :++ a
x -> RangeR 0 (m - 1) b -> b -> RangeR 0 m b
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
(:++) (RangeR 0 (m - 1) b -> b -> RangeR 0 m b)
-> f (RangeR 0 (m - 1) b) -> f (b -> RangeR 0 m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> RangeR 0 (m - 1) a -> f (RangeR 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 RangeR 0 (m - 1) a
xs f (b -> RangeR 0 m b) -> f b -> f (RangeR 0 m b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> f b
f a
x

instance {-# OVERLAPPABLE #-} (1 <= n, Traversable (RangeR (n - 1) (m - 1))) =>
	Traversable (RangeR n m) where
	traverse :: (a -> f b) -> RangeR n m a -> f (RangeR n m b)
traverse a -> f b
f (RangeR (n - 1) (m - 1) a
xs :+ a
x) = RangeR (n - 1) (m - 1) b -> b -> RangeR n m b
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
(:+) (RangeR (n - 1) (m - 1) b -> b -> RangeR n m b)
-> f (RangeR (n - 1) (m - 1) b) -> f (b -> RangeR n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b)
-> RangeR (n - 1) (m - 1) a -> f (RangeR (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 RangeR (n - 1) (m - 1) a
xs f (b -> RangeR n m b) -> f b -> f (RangeR n m b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> f b
f a
x

-- INSTANCE APPLICATIVE

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

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

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

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

instance Applicative (RangeR 0 0) => Monad (RangeR 0 0) where RangeR 0 0 a
NilR >>= :: RangeR 0 0 a -> (a -> RangeR 0 0 b) -> RangeR 0 0 b
>>= a -> RangeR 0 0 b
_ = RangeR 0 0 b
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR


instance {-# OVERLAPPABLE #-} (1 <= n, Applicative (RangeR n n), Monad (RangeR (n - 1) (n - 1))) => Monad (RangeR n n) where
	RangeR (n - 1) (n - 1) a
xs :+ a
x >>= :: RangeR n n a -> (a -> RangeR n n b) -> RangeR n n b
>>= a -> RangeR n n b
f = (RangeR (n - 1) (n - 1) a
xs RangeR (n - 1) (n - 1) a
-> (a -> RangeR (n - 1) (n - 1) b) -> RangeR (n - 1) (n - 1) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
z -> case a -> RangeR n n b
f a
z of RangeR (n - 1) (n - 1) b
zs :+ b
_ -> RangeR (n - 1) (n - 1) b
zs) RangeR (n - 1) (n - 1) b -> b -> RangeR n n b
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ b
y
		where RangeR (n - 1) (n - 1) b
_ :+ b
y = a -> RangeR n n b
f a
x

-- INSTANCE ISSTRING

instance Unfoldl 0 n m => IsString (RangeR n m Char) where
	fromString :: String -> RangeR n m Char
fromString String
s = RangeR n m Char -> Maybe (RangeR n m Char) -> RangeR n m Char
forall a. a -> Maybe a -> a
fromMaybe (String -> RangeR n m Char
forall a. HasCallStack => String -> a
error (String -> RangeR n m Char) -> String -> RangeR 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 (RangeR n m Char) -> RangeR n m Char)
-> (String -> Maybe (RangeR n m Char)) -> String -> RangeR n m Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Maybe (String, Char))
-> String -> Maybe (RangeR n m Char)
forall (v :: Nat) (w :: Nat) s a.
Unfoldl 0 v w =>
(s -> Maybe (s, a)) -> s -> Maybe (RangeR v w a)
unfoldlRangeMaybe (\case String
"" -> Maybe (String, Char)
forall a. Maybe a
Nothing; Char
c : String
cs -> (String, Char) -> Maybe (String, Char)
forall a. a -> Maybe a
Just (String
cs, Char
c)) (String -> RangeR n m Char) -> String -> RangeR n m Char
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. [a] -> [a]
reverse String
s

instance (Foldable (RangeR n m), Unfoldl 0 n m) => IsList (RangeR n m a) where
	type Item (RangeR n m a) = a
	fromList :: [Item (RangeR n m a)] -> RangeR n m a
fromList [Item (RangeR n m a)]
lst = RangeR n m a -> Maybe (RangeR n m a) -> RangeR n m a
forall a. a -> Maybe a -> a
fromMaybe (String -> RangeR n m a
forall a. HasCallStack => String -> a
error (String -> RangeR n m a) -> String -> RangeR n m a
forall a b. (a -> b) -> a -> b
$ String
"The list is not within range.")
		(Maybe (RangeR n m a) -> RangeR n m a)
-> ([a] -> Maybe (RangeR n m a)) -> [a] -> RangeR n m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([a] -> Maybe ([a], a)) -> [a] -> Maybe (RangeR n m a)
forall (v :: Nat) (w :: Nat) s a.
Unfoldl 0 v w =>
(s -> Maybe (s, a)) -> s -> Maybe (RangeR v w a)
unfoldlRangeMaybe (\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]
xs, a
x)) ([a] -> RangeR n m a) -> [a] -> RangeR n m a
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. [a] -> [a]
reverse [a]
[Item (RangeR n m a)]
lst
	toList :: RangeR n m a -> [Item (RangeR n m a)]
toList = RangeR n m a -> [Item (RangeR n m a)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Data.Foldable.toList

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

infixl 5 .:++

class PushR n m where
	(.:++) :: RangeR n m a -> a -> RangeR n (m + 1) a

	{-^

	To push an optional element.

	>>> :set -XDataKinds
	>>> samplePushR = NilR :++ 'h' :+ 'e' :+ 'l' :+ 'l' :: RangeR 3 7 Char
	>>> samplePushR .:++ 'o'
	((((NilR :++ 'h') :++ 'e') :+ 'l') :+ 'l') :+ 'o'
	>>> :type samplePushR .:++ 'o'
	samplePushR .:++ 'o' :: RangeR 3 8 Char

	-}

instance PushR 0 m where
	.:++ :: RangeR 0 m a -> a -> RangeR 0 (m + 1) a
(.:++) = \case RangeR 0 m a
NilR -> (RangeR 0 ((m + 1) - 1) a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR RangeR 0 ((m + 1) - 1) a -> a -> RangeR 0 (m + 1) a
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++); xs :: RangeR 0 m a
xs@(RangeR 0 (m - 1) a
_ :++ a
_) -> (RangeR 0 m a
RangeR 0 ((m + 1) - 1) a
xs RangeR 0 ((m + 1) - 1) a -> a -> RangeR 0 (m + 1) a
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++)

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

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

infixl 5 +++

class AddR n m v w where
	(+++) :: RangeR n m a -> RangeR v w a -> RangeR (n + v) (m + w) a

	{-^

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

	>>> :set -XDataKinds
	>>> sampleRangeR1 = NilR :++ 'f' :+ 'o' :+ 'o' :: RangeR 2 5 Char
	>>> sampleRangeR2 = NilR :++ 'b' :++ 'a' :+ 'r' :: RangeR 1 6 Char
	>>> sampleRangeR1 +++ sampleRangeR2
	(((((NilR :++ 'f') :++ 'o') :++ 'o') :+ 'b') :+ 'a') :+ 'r'
	>>> :type sampleRangeR1 +++ sampleRangeR2
	sampleRangeR1 +++ sampleRangeR2 :: RangeR 3 11 Char

	-}

instance AddR n m 0 0 where RangeR n m a
xs +++ :: RangeR n m a -> RangeR 0 0 a -> RangeR (n + 0) (m + 0) a
+++ RangeR 0 0 a
NilR = RangeR n m a
RangeR (n + 0) (m + 0) a
xs

instance {-# OVERLAPPABLE #-}
	(PushR n (m + w - 1), AddR n m 0 (w - 1), LoosenRMax n m (m + w)) =>
	AddR n m 0 w where
	(+++) :: forall a . RangeR n m a -> RangeR 0 w a -> RangeR n (m + w) a
	+++ :: RangeR n m a -> RangeR 0 w a -> RangeR n (m + w) a
(+++) RangeR n m a
xs = \case
		RangeR 0 w a
NilR -> RangeR n m a -> RangeR n (m + w) a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax RangeR n m a
xs
		RangeR 0 (w - 1) a
ys :++ a
y -> (RangeR n m a
xs RangeR n m a
-> RangeR 0 (w - 1) a -> RangeR (n + 0) (m + (w - 1)) a
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a.
AddR n m v w =>
RangeR n m a -> RangeR v w a -> RangeR (n + v) (m + w) a
+++ RangeR 0 (w - 1) a
ys :: RangeR n (m + w - 1) a) RangeR n ((m + w) - 1) a -> a -> RangeR n (((m + w) - 1) + 1) a
forall (n :: Nat) (m :: Nat) a.
PushR n m =>
RangeR n m a -> a -> RangeR n (m + 1) a
.:++ a
y

instance {-# OVERLAPPABLE #-}
	(1 <= v, AddR n m (v - 1) (w - 1)) => AddR n m v w where
	RangeR n m a
xs +++ :: RangeR n m a -> RangeR v w a -> RangeR (n + v) (m + w) a
+++ RangeR (v - 1) (w - 1) a
ys :+ a
y = (RangeR n m a
xs RangeR n m a
-> RangeR (v - 1) (w - 1) a -> RangeR (n + (v - 1)) (m + (w - 1)) a
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a.
AddR n m v w =>
RangeR n m a -> RangeR v w a -> RangeR (n + v) (m + w) a
+++ RangeR (v - 1) (w - 1) a
ys) RangeR ((n + v) - 1) ((m + w) - 1) a
-> a -> RangeR (n + v) (m + w) a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
y

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

-- LOOSEN RIGHT

loosenR :: (LoosenRMin n m v, LoosenRMax v m w) => RangeR n m a -> RangeR v w a
loosenR :: RangeR n m a -> RangeR v w a
loosenR = RangeR v m a -> RangeR v w a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax (RangeR v m a -> RangeR v w a)
-> (RangeR n m a -> RangeR v m a) -> RangeR n m a -> RangeR v w a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangeR n m a -> RangeR v m a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenRMin n m v =>
RangeR n m a -> RangeR v m a
loosenRMin

{-^

To loosen a range of element number.

>>> :set -XDataKinds
>>> sampleLoosenR = NilR :++ 'h' :+ 'e' :+ 'l' :+ 'l' :+ 'o' :: RangeR 4 6 Char
>>> loosenR sampleLoosenR :: RangeR 2 8 Char
((((NilR :++ 'h') :++ 'e') :++ 'l') :+ 'l') :+ 'o'

-}

-- LOOSEN RIGHT MIN

class LoosenRMin n m v where
	loosenRMin :: RangeR n m a -> RangeR v m a

	{-^

	To loosen a lower bound of element number.

	>>> :set -XDataKinds -fno-warn-tabs
	>>> :{
		sampleLoosenRMin :: RangeR 4 6 Char
		sampleLoosenRMin = NilR :++ 'h' :+ 'e' :+ 'l' :+ 'l' :+ 'o'
	:}

	>>> loosenRMin sampleLoosenRMin :: RangeR 2 6 Char
	((((NilR :++ 'h') :++ 'e') :++ 'l') :+ 'l') :+ 'o'

	-}

instance LoosenRMin 0 m 0 where
	loosenRMin :: RangeR 0 m a -> RangeR 0 m a
loosenRMin = \case RangeR 0 m a
NilR -> RangeR 0 m a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR; xs :: RangeR 0 m a
xs@(RangeR 0 (m - 1) a
_ :++ a
_) -> RangeR 0 m a
xs

instance {-# OVERLAPPABLE #-}
	(1 <= n, LoosenRMin (n - 1) (m - 1) 0) => LoosenRMin n m 0 where
	loosenRMin :: RangeR n m a -> RangeR 0 m a
loosenRMin (RangeR (n - 1) (m - 1) a
xs :+ a
x) = RangeR (n - 1) (m - 1) a -> RangeR 0 (m - 1) a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenRMin n m v =>
RangeR n m a -> RangeR v m a
loosenRMin RangeR (n - 1) (m - 1) a
xs RangeR 0 (m - 1) a -> a -> RangeR 0 m a
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++ a
x

instance {-# OVERLAPPABLE #-}
	(1 <= n, 1 <= v, LoosenRMin (n - 1) (m - 1) (v - 1)) => LoosenRMin n m v where
	loosenRMin :: RangeR n m a -> RangeR v m a
loosenRMin (RangeR (n - 1) (m - 1) a
xs :+ a
x) = RangeR (n - 1) (m - 1) a -> RangeR (v - 1) (m - 1) a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenRMin n m v =>
RangeR n m a -> RangeR v m a
loosenRMin RangeR (n - 1) (m - 1) a
xs RangeR (v - 1) (m - 1) a -> a -> RangeR v m a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
x

-- LOOSEN RIGHT MAX

class LoosenRMax n m w where
	loosenRMax :: RangeR n m a -> RangeR n w a

	{-^

	To loosen an upper bound of element number.

	>>> :set -XDataKinds -fno-warn-tabs
	>>> :{
		sampleLoosenRMax :: RangeR 4 6 Char
		sampleLoosenRMax = NilR :++ 'h' :+ 'e' :+ 'l' :+ 'l' :+ 'o'
	:}

	>>> loosenRMax sampleLoosenRMax :: RangeR 4 8 Char
	((((NilR :++ 'h') :+ 'e') :+ 'l') :+ 'l') :+ 'o'

	-}

instance LoosenRMax 0 0 m where loosenRMax :: RangeR 0 0 a -> RangeR 0 m a
loosenRMax RangeR 0 0 a
NilR = RangeR 0 m a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR

instance {-# OVERLAPPABLE #-}
	(1 <= w, LoosenRMax 0 (m - 1) (w - 1)) => LoosenRMax 0 m w where
	loosenRMax :: RangeR 0 m a -> RangeR 0 w a
loosenRMax = \case RangeR 0 m a
NilR -> RangeR 0 w a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR; RangeR 0 (m - 1) a
xs :++ a
x -> RangeR 0 (m - 1) a -> RangeR 0 (w - 1) a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax RangeR 0 (m - 1) a
xs RangeR 0 (w - 1) a -> a -> RangeR 0 w a
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++ a
x

instance {-# OVERLAPPABLE #-}
	(1 <= n, 1 <= w, LoosenRMax (n - 1) (m - 1) (w - 1)) => LoosenRMax n m w where
	loosenRMax :: RangeR n m a -> RangeR n w a
loosenRMax (RangeR (n - 1) (m - 1) a
xs :+ a
x) = RangeR (n - 1) (m - 1) a -> RangeR (n - 1) (w - 1) a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax RangeR (n - 1) (m - 1) a
xs RangeR (n - 1) (w - 1) a -> a -> RangeR n w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
x

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

-- CLASS

class Unfoldl n v w where
	unfoldlMRangeWithBase :: Monad m =>
		m Bool -> m a -> RangeR n w a -> m (RangeR v w a)

	{-^

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

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

	-}

	unfoldlMRangeMaybeWithBase :: Monad m =>
		m Bool -> m a -> RangeR n w a -> m (Maybe (RangeR v w a))

	{-^

	It is like @unfoldrMRangeMaybe@. 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 = NilR :++ 123 :+ 456 :: RangeR 1 5 Integer
	>>> :{
		unfoldlMRangeMaybeWithBase check count xs
			:: IO (Maybe (RangeR 3 5 Integer))
	:}
	Just ((((NilR :++ 6) :+ 3) :+ 123) :+ 456)

	-}

-- INSTANCE

instance Unfoldl 0 0 0 where
	unfoldlMRangeWithBase :: m Bool -> m a -> RangeR 0 0 a -> m (RangeR 0 0 a)
unfoldlMRangeWithBase m Bool
_ m a
_ RangeR 0 0 a
NilR = RangeR 0 0 a -> m (RangeR 0 0 a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure RangeR 0 0 a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
	unfoldlMRangeMaybeWithBase :: m Bool -> m a -> RangeR 0 0 a -> m (Maybe (RangeR 0 0 a))
unfoldlMRangeMaybeWithBase m Bool
p m a
_ RangeR 0 0 a
NilR = Maybe (RangeR 0 0 a)
-> Maybe (RangeR 0 0 a) -> Bool -> Maybe (RangeR 0 0 a)
forall a. a -> a -> Bool -> a
bool (RangeR 0 0 a -> Maybe (RangeR 0 0 a)
forall a. a -> Maybe a
Just RangeR 0 0 a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR) Maybe (RangeR 0 0 a)
forall a. Maybe a
Nothing (Bool -> Maybe (RangeR 0 0 a))
-> m Bool -> m (Maybe (RangeR 0 0 a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool
p

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

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

instance {-# OVERLAPPABLE #-} (1 <= v, 1 <= w, Unfoldl 0 (v - 1) (w - 1)) => Unfoldl 0 v w where
	unfoldlMRangeWithBase :: m Bool -> m a -> RangeR 0 w a -> m (RangeR v w a)
unfoldlMRangeWithBase m Bool
p m a
f = \case
		RangeR 0 w a
NilR -> m a
f m a -> (a -> m (RangeR v w a)) -> m (RangeR v w a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x -> (RangeR (v - 1) (w - 1) a -> a -> RangeR v w 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 (v - 1) (w - 1) a -> RangeR v w a)
-> m (RangeR (v - 1) (w - 1) a) -> m (RangeR v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool -> m a -> RangeR 0 (w - 1) a -> m (RangeR (v - 1) (w - 1) 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
p m a
f RangeR 0 (w - 1) a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
		RangeR 0 (w - 1) a
xs :++ a
x -> (RangeR (v - 1) (w - 1) a -> a -> RangeR v w 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 (v - 1) (w - 1) a -> RangeR v w a)
-> m (RangeR (v - 1) (w - 1) a) -> m (RangeR v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool -> m a -> RangeR 0 (w - 1) a -> m (RangeR (v - 1) (w - 1) 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
p m a
f RangeR 0 (w - 1) a
xs

	unfoldlMRangeMaybeWithBase :: m Bool -> m a -> RangeR 0 w a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase m Bool
p m a
f = \case
		RangeR 0 w a
NilR -> (m Bool
p m Bool
-> (Bool -> m (Maybe (RangeR v w a))) -> m (Maybe (RangeR v w a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=) ((Bool -> m (Maybe (RangeR v w a))) -> m (Maybe (RangeR v w a)))
-> (m (Maybe (RangeR v w a)) -> Bool -> m (Maybe (RangeR v w a)))
-> m (Maybe (RangeR v w a))
-> m (Maybe (RangeR v w a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (RangeR v w a))
-> m (Maybe (RangeR v w a)) -> Bool -> m (Maybe (RangeR v w a))
forall a. a -> a -> Bool -> a
bool (Maybe (RangeR v w a) -> m (Maybe (RangeR v w a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (RangeR v w a)
forall a. Maybe a
Nothing) (m (Maybe (RangeR v w a)) -> m (Maybe (RangeR v w a)))
-> m (Maybe (RangeR v w a)) -> m (Maybe (RangeR v w a))
forall a b. (a -> b) -> a -> b
$ m a
f m a -> (a -> m (Maybe (RangeR v w a))) -> m (Maybe (RangeR v w a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x ->
			((RangeR (v - 1) (w - 1) a -> a -> RangeR v w 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 (v - 1) (w - 1) a -> RangeR v w a)
-> Maybe (RangeR (v - 1) (w - 1) a) -> Maybe (RangeR v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (RangeR (v - 1) (w - 1) a) -> Maybe (RangeR v w a))
-> m (Maybe (RangeR (v - 1) (w - 1) a)) -> m (Maybe (RangeR v w a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool
-> m a
-> RangeR 0 (w - 1) a
-> m (Maybe (RangeR (v - 1) (w - 1) 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 (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase m Bool
p m a
f RangeR 0 (w - 1) a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
		RangeR 0 (w - 1) a
xs :++ a
x -> ((RangeR (v - 1) (w - 1) a -> a -> RangeR v w 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 (v - 1) (w - 1) a -> RangeR v w a)
-> Maybe (RangeR (v - 1) (w - 1) a) -> Maybe (RangeR v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (RangeR (v - 1) (w - 1) a) -> Maybe (RangeR v w a))
-> m (Maybe (RangeR (v - 1) (w - 1) a)) -> m (Maybe (RangeR v w a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool
-> m a
-> RangeR 0 (w - 1) a
-> m (Maybe (RangeR (v - 1) (w - 1) 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 (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase m Bool
p m a
f RangeR 0 (w - 1) a
xs

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

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

-- UNFOLDL RANGE

unfoldlRange :: Unfoldl 0 v w =>
	(s -> Bool) -> (s -> (s, a)) -> s -> RangeR v w a
unfoldlRange :: (s -> Bool) -> (s -> (s, a)) -> s -> RangeR v w a
unfoldlRange s -> Bool
p s -> (s, a)
f s
s = (s -> Bool) -> (s -> (s, a)) -> s -> RangeR 0 w a -> RangeR v w a
forall (n :: Nat) (v :: Nat) (w :: Nat) s a.
Unfoldl n v w =>
(s -> Bool) -> (s -> (s, a)) -> s -> RangeR n w a -> RangeR v w a
unfoldlRangeWithBase s -> Bool
p s -> (s, a)
f s
s RangeR 0 w a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR

{-^

To eveluate a function to construct a list.
The function recieve a state and return an element and a new state.
The 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
>>> unfoldlRange (< 2) (\n -> (n + 1, n * 3)) 1 :: RangeR 3 5 Int
((NilR :+ 9) :+ 6) :+ 3

>>> unfoldlRange (< 5) (\n -> (n + 1, n * 3)) 1 :: RangeR 3 5 Int
(((NilR :++ 12) :+ 9) :+ 6) :+ 3

>>> unfoldlRange (< 10) (\n -> (n + 1, n * 3)) 1 :: RangeR 3 5 Int
((((NilR :++ 15) :++ 12) :+ 9) :+ 6) :+ 3

-}

unfoldlRangeWithBase :: Unfoldl n v w =>
	(s -> Bool) -> (s -> (s, a)) -> s -> RangeR n w a -> RangeR v w a
unfoldlRangeWithBase :: (s -> Bool) -> (s -> (s, a)) -> s -> RangeR n w a -> RangeR v w a
unfoldlRangeWithBase s -> Bool
p s -> (s, a)
f = ((s, RangeR v w a) -> RangeR v w a
forall a b. (a, b) -> b
snd ((s, RangeR v w a) -> RangeR v w a)
-> (RangeR n w a -> (s, RangeR v w a))
-> RangeR n w a
-> RangeR v w a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((RangeR n w a -> (s, RangeR v w a))
 -> RangeR n w a -> RangeR v w a)
-> (s -> RangeR n w a -> (s, RangeR v w a))
-> s
-> RangeR n w a
-> RangeR v w a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s -> Bool)
-> (s -> (s, a)) -> s -> RangeR n w a -> (s, RangeR v w a)
forall (n :: Nat) (v :: Nat) (w :: Nat) s a.
Unfoldl n v w =>
(s -> Bool)
-> (s -> (s, a)) -> s -> RangeR n w a -> (s, RangeR v w a)
unfoldlRangeWithBaseWithS s -> Bool
p s -> (s, a)
f

{-^

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

>>> :set -XDataKinds
>>> xs = NilR :++ 123 :+ 456 :: RangeR 1 5 Integer
>>> unfoldlRangeWithBase (< 3) (\n -> (n + 1, n * 3)) 1 xs :: RangeR 3 5 Integer
(((NilR :++ 6) :+ 3) :+ 123) :+ 456

-}

unfoldlRangeWithBaseWithS :: Unfoldl n v w =>
	(s -> Bool) -> (s -> (s, a)) -> s -> RangeR n w a -> (s, RangeR v w a)
unfoldlRangeWithBaseWithS :: (s -> Bool)
-> (s -> (s, a)) -> s -> RangeR n w a -> (s, RangeR v w a)
unfoldlRangeWithBaseWithS s -> Bool
p s -> (s, a)
f =
	(RangeR n w a -> s -> (s, RangeR v w a))
-> s -> RangeR n w a -> (s, RangeR v w a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((RangeR n w a -> s -> (s, RangeR v w a))
 -> s -> RangeR n w a -> (s, RangeR v w a))
-> (RangeR n w a -> s -> (s, RangeR v w a))
-> s
-> RangeR n w a
-> (s, RangeR v w a)
forall a b. (a -> b) -> a -> b
$ StateR s (RangeR v w a) -> s -> (s, RangeR v w a)
forall s a. StateR s a -> s -> (s, a)
runStateR (StateR s (RangeR v w a) -> s -> (s, RangeR v w a))
-> (RangeR n w a -> StateR s (RangeR v w a))
-> RangeR n w a
-> s
-> (s, RangeR v w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateR s Bool
-> StateR s a -> RangeR n w a -> StateR s (RangeR v 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 ((s -> (s, Bool)) -> StateR s Bool
forall s a. (s -> (s, a)) -> StateR s a
StateR ((s -> (s, Bool)) -> StateR s Bool)
-> (s -> (s, Bool)) -> StateR s Bool
forall a b. (a -> b) -> a -> b
$ s -> s
forall a. a -> a
id (s -> s) -> (s -> Bool) -> s -> (s, Bool)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& s -> Bool
p) ((s -> (s, a)) -> StateR s a
forall s a. (s -> (s, a)) -> StateR s a
StateR s -> (s, a)
f)

{-^

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

>>> :set -XDataKinds -fno-warn-tabs
>>> xs = NilR :++ 123 :+ 456 :: RangeR 1 5 Integer
>>> :{
	unfoldlRangeWithBaseWithS (< 3) (\n -> (n + 1, n * 3)) 1 xs
		:: (Integer, RangeR 3 5 Integer)
:}
(3,(((NilR :++ 6) :+ 3) :+ 123) :+ 456)

-}

unfoldlMRange :: (Unfoldl 0 v w, Monad m) => m Bool -> m a -> m (RangeR v w a)
unfoldlMRange :: m Bool -> m a -> m (RangeR v w a)
unfoldlMRange m Bool
p m a
f = m Bool -> m a -> RangeR 0 w a -> m (RangeR v 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
p m a
f RangeR 0 w a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR

{-^

It is like @unfoldlRange@. 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)
>>> unfoldlMRange ((< 5) <$> readIORef r) count :: IO (RangeR 3 5 Integer)
(((NilR :++ 12) :+ 9) :+ 6) :+ 3

-}

-- UNFOLDL RANGE MAYBE

unfoldlRangeMaybe ::
	Unfoldl 0 v w => (s -> Maybe (s, a)) -> s -> Maybe (RangeR v w a)
unfoldlRangeMaybe :: (s -> Maybe (s, a)) -> s -> Maybe (RangeR v w a)
unfoldlRangeMaybe s -> Maybe (s, a)
f s
s = (s -> Maybe (s, a)) -> s -> RangeR 0 w a -> Maybe (RangeR v w a)
forall (n :: Nat) (v :: Nat) (w :: Nat) s a.
Unfoldl n v w =>
(s -> Maybe (s, a)) -> s -> RangeR n w a -> Maybe (RangeR v w a)
unfoldlRangeMaybeWithBase s -> Maybe (s, a)
f s
s RangeR 0 w a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR

{-^

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

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

>>> unfoldlRangeMaybe (count 5) 1 :: Maybe (RangeR 3 5 Int)
Just ((((NilR :++ 12) :+ 9) :+ 6) :+ 3)

>>> unfoldlRangeMaybe (count 10) 1 :: Maybe (RangeR 3 5 Int)
Nothing

-}

unfoldlRangeMaybeWithBase :: Unfoldl n v w =>
	(s -> Maybe (s, a)) -> s -> RangeR n w a -> Maybe (RangeR v w a)
unfoldlRangeMaybeWithBase :: (s -> Maybe (s, a)) -> s -> RangeR n w a -> Maybe (RangeR v w a)
unfoldlRangeMaybeWithBase s -> Maybe (s, a)
f s
s RangeR n w a
xs =
	(Maybe (s, a), Maybe (RangeR v w a)) -> Maybe (RangeR v w a)
forall a b. (a, b) -> b
snd ((Maybe (s, a), Maybe (RangeR v w a)) -> Maybe (RangeR v w a))
-> (Maybe (s, a), Maybe (RangeR v w a)) -> Maybe (RangeR v w a)
forall a b. (a -> b) -> a -> b
$ St s a Bool
-> St s a a -> RangeR n w a -> St s a (Maybe (RangeR v w a))
forall (n :: Nat) (v :: Nat) (w :: Nat) s a.
Unfoldl n v w =>
St s a Bool
-> St s a a -> RangeR n w a -> St s a (Maybe (RangeR v w a))
unfoldlRangeMaybeWithBaseGen (Maybe (s, a) -> Maybe (s, a)
forall a. a -> a
id (Maybe (s, a) -> Maybe (s, a))
-> (Maybe (s, a) -> Bool) -> St s a Bool
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Maybe (s, a) -> Bool
forall a. Maybe a -> Bool
isJust)
		((Maybe (s, a), a) -> ((s, a) -> (Maybe (s, a), a)) -> St s a a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> (Maybe (s, a), a)
forall a. HasCallStack => String -> a
error String
"never occur") (s -> Maybe (s, a)
f (s -> Maybe (s, a)) -> (s, a) -> (Maybe (s, a), a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
`first`)) RangeR n w a
xs (s -> Maybe (s, a)
f s
s)

{-^

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

>>> :set -XDataKinds
>>> count n = if n < 3 then Just (n + 1, n * 3) else Nothing
>>> xs = NilR :++ 123 :+ 456 :: RangeR 1 5 Int
>>> unfoldlRangeMaybeWithBase count 1 xs :: Maybe (RangeR 3 5 Int)
Just ((((NilR :++ 6) :+ 3) :+ 123) :+ 456)

-}

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

unfoldlRangeMaybeWithBaseGen :: Unfoldl n v w =>
	St s a Bool -> St s a a -> RangeR n w a -> St s a (Maybe (RangeR v w a))
unfoldlRangeMaybeWithBaseGen :: St s a Bool
-> St s a a -> RangeR n w a -> St s a (Maybe (RangeR v w a))
unfoldlRangeMaybeWithBaseGen St s a Bool
p St s a a
f =
	StateR (Maybe (s, a)) (Maybe (RangeR v w a))
-> St s a (Maybe (RangeR v w a))
forall s a. StateR s a -> s -> (s, a)
runStateR (StateR (Maybe (s, a)) (Maybe (RangeR v w a))
 -> St s a (Maybe (RangeR v w a)))
-> (RangeR n w a -> StateR (Maybe (s, a)) (Maybe (RangeR v w a)))
-> RangeR n w a
-> St s a (Maybe (RangeR v w a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateR (Maybe (s, a)) Bool
-> StateR (Maybe (s, a)) a
-> RangeR n w a
-> StateR (Maybe (s, a)) (Maybe (RangeR v 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 (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase (St s a Bool -> StateR (Maybe (s, a)) Bool
forall s a. (s -> (s, a)) -> StateR s a
StateR St s a Bool
p) (St s a a -> StateR (Maybe (s, a)) a
forall s a. (s -> (s, a)) -> StateR s a
StateR St s a a
f)

unfoldlMRangeMaybe :: (Unfoldl 0 v w, Monad m) =>
	m Bool -> m a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybe :: m Bool -> m a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybe m Bool
p m a
f = m Bool -> m a -> RangeR 0 w a -> m (Maybe (RangeR v 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 (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase m Bool
p m a
f RangeR 0 w a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR

{-^

It is like @unfoldlRangeMaybe@. But it use a monad instead of a function.
The first argument monad returns a boolean value.
It creates 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 @unfoldlMRangeMaybe@ returns Nothing.

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

>>> writeIORef r 1
>>> unfoldlMRangeMaybe (check 5) count :: IO (Maybe (RangeR 3 5 Integer))
Just ((((NilR :++ 12) :+ 9) :+ 6) :+ 3)

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

-}

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

-- CLASS AND INSTANCE

class ZipR n m v w where
	zipWithMR :: Monad q =>
		(a -> b -> q c) -> RangeR n m a -> RangeR v w b ->
		q (RangeR (n - w) (m - v) a, RangeR v w c)

	{-^

	It is like @zipWithR@.
	But it uses a function which returns a monad instead of a simple value.

	>>> :set -XDataKinds
	>>> ns = NilR :++ 1 :+ 2 :+ 3 :+ 4 :+ 5 :+ 6 :: RangeR 5 7 Int
	>>> cs = NilR :++ 'a' :+ 'b' :+ 'c' :: RangeR 2 4 Char
	>>> zipWithMR (\n -> putStrLn . replicate n) ns cs
	cccccc
	bbbbb
	aaaa
	(((NilR :++ 1) :++ 2) :+ 3,((NilR :++ ()) :+ ()) :+ ())

	-}

instance ZipR n m 0 0 where zipWithMR :: (a -> b -> q c)
-> RangeR n m a
-> RangeR 0 0 b
-> q (RangeR (n - 0) (m - 0) a, RangeR 0 0 c)
zipWithMR a -> b -> q c
_ RangeR n m a
xs RangeR 0 0 b
NilR = (RangeR n m a, RangeR 0 0 c) -> q (RangeR n m a, RangeR 0 0 c)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RangeR n m a
xs, RangeR 0 0 c
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR)

instance {-# OVERLAPPABLE #-} (
	1 <= n, 1 <= m, w <= n, LoosenRMin n m (n - w), LoosenRMax (n - w) (m - 1) m,
	ZipR (n - 1) (m - 1) 0 (w - 1) ) => ZipR n m 0 w where
	zipWithMR :: (a -> b -> q c)
-> RangeR n m a
-> RangeR 0 w b
-> q (RangeR (n - w) (m - 0) a, RangeR 0 w c)
zipWithMR a -> b -> q c
_ RangeR n m a
xs RangeR 0 w b
NilR = (RangeR (n - w) m a, RangeR 0 w c)
-> q (RangeR (n - w) m a, RangeR 0 w c)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RangeR n m a -> RangeR (n - w) m a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenRMin n m v =>
RangeR n m a -> RangeR v m a
loosenRMin RangeR n m a
xs, RangeR 0 w c
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR)
	zipWithMR a -> b -> q c
(%) (RangeR (n - 1) (m - 1) a
xs :+ a
x) (RangeR 0 (w - 1) b
ys :++ b
y) =
		a
x a -> b -> q c
% b
y q c
-> (c -> q (RangeR (n - w) m a, RangeR 0 w c))
-> q (RangeR (n - w) m a, RangeR 0 w c)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c
z -> (RangeR (n - w) (m - 1) a -> RangeR (n - w) m a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax (RangeR (n - w) (m - 1) a -> RangeR (n - w) m a)
-> (RangeR 0 (w - 1) c -> RangeR 0 w c)
-> (RangeR (n - w) (m - 1) a, RangeR 0 (w - 1) c)
-> (RangeR (n - w) m a, RangeR 0 w c)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (RangeR 0 (w - 1) c -> c -> RangeR 0 w c
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++ c
z)) ((RangeR (n - w) (m - 1) a, RangeR 0 (w - 1) c)
 -> (RangeR (n - w) m a, RangeR 0 w c))
-> q (RangeR (n - w) (m - 1) a, RangeR 0 (w - 1) c)
-> q (RangeR (n - w) m a, RangeR 0 w c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> b -> q c)
-> RangeR (n - 1) (m - 1) a
-> RangeR 0 (w - 1) b
-> q (RangeR ((n - 1) - (w - 1)) ((m - 1) - 0) a,
      RangeR 0 (w - 1) c)
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) (q :: * -> *) a
       b c.
(ZipR n m v w, Monad q) =>
(a -> b -> q c)
-> RangeR n m a
-> RangeR v w b
-> q (RangeR (n - w) (m - v) a, RangeR v w c)
zipWithMR a -> b -> q c
(%) RangeR (n - 1) (m - 1) a
xs RangeR 0 (w - 1) b
ys

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

-- FUNCTION

zipR :: ZipR n m v w => RangeR n m a -> RangeR v w b ->
	(RangeR (n - w) (m - v) a, RangeR v w (a, b))
zipR :: RangeR n m a
-> RangeR v w b -> (RangeR (n - w) (m - v) a, RangeR v w (a, b))
zipR = (a -> b -> (a, b))
-> RangeR n m a
-> RangeR v w b
-> (RangeR (n - w) (m - v) a, RangeR v w (a, b))
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a b c.
ZipR n m v w =>
(a -> b -> c)
-> RangeR n m a
-> RangeR v w b
-> (RangeR (n - w) (m - v) a, RangeR v w c)
zipWithR (,)

{-^

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

>>> :set -XDataKinds
>>> sampleZipR1 = NilR :++ 1 :+ 2 :+ 3 :+ 4 :+ 5 :+ 6 :: RangeR 5 7 Integer
>>> sampleZipR2 = NilR :++ 3 :+ 2 :+ 1 :: RangeR 2 4 Integer
>>> zipR sampleZipR1 sampleZipR2
(((NilR :++ 1) :++ 2) :+ 3,((NilR :++ (4,3)) :+ (5,2)) :+ (6,1))
>>> :type zipR sampleZipR1 sampleZipR2
zipR sampleZipR1 sampleZipR2
  :: (RangeR 1 5 Integer, RangeR 2 4 (Integer, Integer))

-}

zipWithR :: ZipR n m v w => (a -> b -> c) -> RangeR n m a -> RangeR v w b ->
	(RangeR (n - w) (m - v) a, RangeR v w c)
zipWithR :: (a -> b -> c)
-> RangeR n m a
-> RangeR v w b
-> (RangeR (n - w) (m - v) a, RangeR v w c)
zipWithR a -> b -> c
op = (Identity (RangeR (n - w) (m - v) a, RangeR v w c)
-> (RangeR (n - w) (m - v) a, RangeR v w c)
forall a. Identity a -> a
runIdentity (Identity (RangeR (n - w) (m - v) a, RangeR v w c)
 -> (RangeR (n - w) (m - v) a, RangeR v w c))
-> (RangeR v w b
    -> Identity (RangeR (n - w) (m - v) a, RangeR v w c))
-> RangeR v w b
-> (RangeR (n - w) (m - v) a, RangeR v w c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((RangeR v w b
  -> Identity (RangeR (n - w) (m - v) a, RangeR v w c))
 -> RangeR v w b -> (RangeR (n - w) (m - v) a, RangeR v w c))
-> (RangeR n m a
    -> RangeR v w b
    -> Identity (RangeR (n - w) (m - v) a, RangeR v w c))
-> RangeR n m a
-> RangeR v w b
-> (RangeR (n - w) (m - v) a, RangeR v w c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b -> Identity c)
-> RangeR n m a
-> RangeR v w b
-> Identity (RangeR (n - w) (m - v) a, RangeR v w c)
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) (q :: * -> *) a
       b c.
(ZipR n m v w, Monad q) =>
(a -> b -> q c)
-> RangeR n m a
-> RangeR v w b
-> q (RangeR (n - w) (m - v) a, RangeR v w c)
zipWithMR ((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 @zipR@.
But it evaluates a function to make values instead of puts together in tuples.

>>> :set -XDataKinds
>>> sampleZipWithR1 = NilR :++ 1 :+ 2 :+ 3 :+ 4 :+ 5 :+ 6 :: RangeR 5 7 Integer
>>> sampleZipWithR2 = NilR :++ 7 :+ 6 :+ 5 :: RangeR 2 4 Integer
>>> zipWithR (+) sampleZipWithR1 sampleZipWithR2
(((NilR :++ 1) :++ 2) :+ 3,((NilR :++ 11) :+ 11) :+ 11)
>>> :type zipWithR (+) sampleZipWithR1 sampleZipWithR2
zipWithR (+) sampleZipWithR1 sampleZipWithR2
  :: (RangeR 1 5 Integer, RangeR 2 4 Integer)

-}