ranged-list (empty) → 0.1.0.0

raw patch · 22 files changed

+3608/−0 lines, 22 filesdep +basedep +doctestdep +ranged-listsetup-changed

Dependencies added: base, doctest, ranged-list, typecheck-plugin-nat-simple

Files

• ChangeLog.md +3/−0
• LICENSE +30/−0
• README.md +885/−0
• Setup.hs +2/−0
• ranged-list.cabal +85/−0
• sample/LengthR.hs +9/−0
• sample/fingertree.hs +108/−0
• sample/fourPointsOfRect.hs +73/−0
• sample/password.hs +27/−0
• sample/rectangle.hs +15/−0
• sample/word64.hs +40/−0
• src/Control/Monad/Identity.hs +12/−0
• src/Control/Monad/State.hs +43/−0
• src/Data/List/Length.hs +187/−0
• src/Data/List/Length/LengthL.hs +120/−0
• src/Data/List/Length/LengthR.hs +131/−0
• src/Data/List/Range.hs +372/−0
• src/Data/List/Range/Nat.hs +152/−0
• src/Data/List/Range/RangeL.hs +643/−0
• src/Data/List/Range/RangeR.hs +627/−0
• test/doctests.hs +12/−0
• test/spec.hs +32/−0

@@ -0,0 +1,3 @@+# Changelog for ranged-list++## Unreleased changes

@@ -0,0 +1,30 @@+Copyright Yoshikuni Jujo (c) 2020++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Yoshikuni Jujo nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,885 @@+# ranged-list++## What's this++This package provides lists whose lengths are determined by the type and+lists whose ranges of lengths are determined by the type.++```haskell+sample1 :: LengthL 3 Integer+sample1 = 1 :. 2 :. 3 :. NilL++sample2 :: LengthR 3 Integer+sample2 = NilR :+ 1 :+ 2 :+ 3++sample3 :: RangeL 2 5 Integer+sample3 = 1 :. 2 :. 3 :.. 4 :.. NilL++sample4 :: RangeR 2 5 Integer+sample4 = NilR :++ 1 :++ 2 :+ 3 :+ 4+```++`LengthL 3 Integer` and `LengthR 3 Integer` are lists who have just 3 `Integer`.+`RangeL 2 5 Integer` and `RangeR 2 5 Integer` are lists whose element numbers+are 2 at minimum and 5 at maximum.+`LengthL 3 Integer` and `RangeL 2 5 Integer` are+pushed or poped a element from left.+`LengthR 3 Integer` and `RangeR 2 5 Integer` are+pushed or poped a element from right.++## Motivation++Suppose you want to take elements from list. You can use `take` like following.++```+xs = take 3 "Hello, world!"+```++The length of `xs` is lesser or equal `3`.+But you cannot use this knowledge when you write next code.+You should check the argument of a next function.++```haskell+fun :: [Char] -> ...+fun [] = ...+fun [x] = ...+fun [x, y] = ...+fun [x, y, z] = ...+fun _ = error "bad argument"+```+If you use `LengthL 3 Char`,+you don't need to mind the argument has more than 3 elements.++```haskell+fun :: LengthL 3 Char -> ...+fun (x :. y :. z :. NilL) = ...+```++## LengthL++### To make rectangles from a number list++Suppose you want to make a value which represent a rectangle.+You have a number list.+The numbers are a left border, a top border, a width and a height of+a rectangle in order.+The numbers of the first rectangle are followed by+the numbers of a second rectangle,+and the numbers of the second rectangle are followed by+the numbers of a third rectangle,+and so on.++```+[left1, top1, width1, height1, left2, top2, width2, height2, left3, ...]+```++The list of numbers defined above are covert to a following list.++```+[Rect left1 top1 width1 height1, Rect left2 top2 width2 height2, Rect left3 ...]+```++The code is following. (View `sample/rectangle.hs`)++```haskell:sample/rectangle.hs+import Data.Length.Length++data Rect = Rect {+	left :: Double, top :: Double,+	width :: Double, height :: Double } derivins Show++makeRect :: Length 4 Double -> Rect+makeRect (l :. t :. w :. h :. NilL) = Rect l t w h++main :: IO ()+main = print $ map makeRect . fst $ chunksL [3, 5, 15, 2, 8, 4, 1, 9, 3, 5]+```++The function `chunksL` return a value of type `([LengthL n a], RangeL 0 (n - 1) a)`.+The first value of this tuple is a list of `n` elements of type `a`.+And the second value of this tuple is rest elements.+The number of the rest elements is `0` at minimum and `n - 1` at maximum.++Try running.++```+% stack ghc sample/rectangle.hs+% ./sample/rectangle+[Rect {left = 3.0, top = 5.0, width = 15.0, height = 2.0},+Rect {left = 8.0, top = 4.0, width = 1.0, height = 9.0)}+```++### To take Word64 from bit list++Let's define function to take a 64 bit word from bit list. (View `sample/word64.hs`)+The language extensions and the import list are following.++```haskell:sample/word64.hs+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MonoLocalBinds #-}+{-# LANGUAGE DAtaKinds, TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++import GHC.TypeNats+import Data.Foldable+import Data.List.Length+import Data.List.Range+import Data.Bits+import Data.Word+import Numeric+```++You define function `takeL` to take `n` elements from list.++```haskell:sample/word64.hs+takeL :: (LoosenLMax 0 (n - 1) n, Unfoldr 0 n n, ListToLengthL n) =>+	a -> [a] -> LengthL n a+takeL d = either ((`fillL` d) . loosenLMax) fst . splitL+```++The function `splitL` split a list and get n element lengthed list (`LengthL n a`) and a rest of the list.+If the list does not contain enough elements, then it returns a left value. It is a list of type `RangeL 0 (n - 1) a`.+The function `loosenLMax` convert the type `RangeL 0 (n - 1)` into `RangeL 0 n`.+And the function `fillL` fill the list with default value `d` to get a list `LengthL n a`.+Try it.++```+% stack ghci sample/word64.hs+> :set -XDataKinds+> takeL '@' "Hello, world!" :: LengthL 5 Char+'H' :. ('e' :. ('l' :. ('l' :. ('o' :. NilL))))+> takeL 'W' "Hi!" :: LengthL 5 Char+'H' :. ('i' :. ('!' :. ('@' :. ('@' :. NilL))))+```++You define data type which represent a bit as follow.++```haskell:sample/word64.hs+data Bit = O | I deriving Show++boolToBit :: Bool -> Bit+boolToBit = \case False -> O; True -> I++bitToNum63 :: (Num n, Bits n) => Bit -> n+bitToNum63 = \case O -> 0; I -> 1 `shiftL` 63+```++`O` is 0 and `I` is 1.+Function `boolToBit` converts a value of `Bool` into a value of `Bit`.+Function `bitToNum63` converts a value of `Bit` into a number.+It converte the bit as a 63rd bit.++You define the function which convert a bit list into 64 bit word.++```haskell:sample/word64.hs+bitsToWord64 :: LengthL 64 Bit -> Word64+bitsToWord64 = foldl' (\w b -> w `shiftR` 1 .|. bitToNum63 b) 0+```++It gets a bit from the left end.+It put the bit on a 63rd position of a 64 bit word.+Then it gets a next bit.+It shifts 64 bit word to the right.+And it put the bit on a 63rd position of a 64 bit word.+It continue in the same way.++You define the function which take 64 bit word from a bit list expressed+as string.++```haskell:sample/word64.hs+takeWord64 :: String -> Word64+takeWord64 = bitsToWord64 . takeL O . (boolToBit . (== '*') <$>)+```++The argument of this function is a string.+The string represent a bit sequence.+Character \'\*\' is 1 and character \'.\' is 0.++You define sample string and try it in function `main`.++```haskell:sample/word64.hs+sample1, sample2 :: String+sample1 = "...*..*..*...........*...**********...*************............******"+sample2 = "...*..*..*...........*.."++main :: IO ()+main = do+	putStrLn $ takeWord64 sample1 `showHex` ""+	putStrLn $ takeWord64 sample2 `showHex` ""+```++Try it.++```+% stack ghc sample/word64.hs+% ./sample/word64+8007ffc7fe200248+200248+```++## LengthR++### To push and pop from right++A value of the type `LengthR n a` is a list of values of the type `a`.+The length of the list is `n`.+And you can push and pop an element from right.+Try it. (view `sample/LengthR.hs`)++```haskell:sample/LengthR.hs+{-# LANGUAGE DataKinds #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module LengthR where++import Data.List.Length++hello :: LengthR 5 Char+hello = NilR :+ 'h' :+ 'e' :+ 'l' :+ 'l' :+ 'o'+```++The value `hello` is a list of characters which length is `5`.+Let\'s push the character `'!'` from right.++```+% stack ghci sample/LengthR.hs+> hello+((((NilR :+ 'h') :+ 'e') :+ 'l') :+ 'l') :+ 'o'+> hello :+ '!'+(((((NilR :+ 'h') :+ 'e') :+ 'l') :+ 'l') :+ 'o') :+ '!'+```++### To show 4 points of rectangles++#### function `fourPoints` and headers++You want to calculate four points of rectangle+from the left-top point, width and height of the rectangle.+You define function `fourPoints`. (View `sample/fourPointsOfRect.hs`)++```haskell:sample/fourPointsOfRect.hs+fourPoints :: LengthR 4 Double -> LengthR 4 (Double, Double)+fourPoints (NilR :+ l :+ t :+ w :+ h) =+	NilR :+ (l, t) :+ (l + w, t) :+ (l, t + h) :+ (l + w, t + h)+```++You add language extensions and modules to import.++```haskell:sample/fourPointsOfRect.hs+{-# LANGUAGE BlockArguments, LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,+	UndecidableInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}++import GHC.TypeNats+import Control.Monad.Fix+import Control.Monad.Catch+import Data.List.Length+import Text.Read+```++Try it.++```+% stack ghci sample/fourPointsOfRect.hs+> fourPoints $ NilR :+ 300 :+ 200 :+ 50 :+ 30+(((NilR :+ (300.0,200.0)) :+ (350.0,200.0)) :+ (300.0,230.0)) :+ (350.0,230.0)+```++#### to input values interactively++You want to input values of a left bound, a top bound, a width and a height+interactively.+You want to delete the last value and reinput a new value.+First of all, you define two data type,+`DeleteOr a` and `NothingToDeleteException`.++```haskell:sample/fourPointsOfRect.hs+data DeleteOr a = Delete | Value a deriving Show+data NothingToDeleteException = NothingToDeleteException deriving Show+instance Exception NothingToDeleteException+```++And you define the function `getElems` as a class function.++```haskell:sample/fourPointsOfRect.hs+class GetElems n v where+	getElems :: MonadThrow m =>+		LengthR n a -> m (Maybe (DeleteOr a)) -> m (LengthR (n + v) a)++instance GetElems 0 0 where getElems NilR _ = pure NilR++instance {-# OVERLAPPABLE #-} 1 <= n => GetElems n 0 where+	getElems xs@(_ :+ _) _ = pure xs++instance {-# OVERLAPPABLE #-} GetElems 1 (v - 1) => GetElems 0 v where+	getElems NilR gt = gt >>= \case+		Nothing -> getElems NilR gt+		Just Delete -> throwM NothingToDeleteException+		Just (Value x) -> getElem @1 @(v - 1) (NilR :+ x) gt++instance {-# OVERLAPPABLE #-}+	(1 <= n, GetElems (n - 1) (v + 1), GetElems (n + 1) (v - 1)) =>+	GetElems n v where+	getElems xa@(xs :+ _) gt = gt >>= \case+		Nothing -> getElems xa gt+		Just Delete -> getElems @(n - 1) @(v + 1) xs gt+		Just (Value x) -> getElems @(n + 1) @(v - 1) (xa :+ x) gt+```++##### class GetElems n v++The class function `getElems` has two arguments.+The first argument is a list of values which are already inputed.+The second argument is a monad which returns 3 kinds of values,+a value which represents to delete, a new value to push to the list+or a value which represents to do nothing.++##### instance GetElems 0 0++`n == 0` and `v == 0` means that the function `getElems` get+ a list of no elements and return a list of no elements.++##### instance GetElems n 0++`v == 0` means that the function `getElems` get a list and+return the list as it is.++##### instance GetElems 0 v++`n == 0` means that there are no already inputed elements.+The monad returns 3 kind of values.+If it returns `Nothing`, then it rerun the whole as `getElems NilR gt`.+If it returns `Just Delete`, then `NothingToDeleteException` occurs.+If it returns `Just (Value x)`,+then it set the already-inputed elements to `NilR :+ x` and rerun the whole.++##### instance GetElems n v++The monad `gt` returns 3 kind of values.+If it returns `Nothing`, then rerun the whole as `getElems xa gt`.+If it returns `Just Delete`,+then it remove an element from the already-inputed list+and rerun the whole.+If it returns `Just (Value x)`,+then it set the already-inputed elements to `xa :+ x` and rerun the whole.++##### to try it++Try it.++```+% stack ghci sample/fourPointsOfRect.hs+> :set -XDataKinds -XBlockArguments -XLambdaCase+> getElems NilR (Just . Value <$> getLine) :: IO (LengthR 3 String)+foo+bar+baz+((NilR :+ "foo") :+ "bar") :+ "baz"+> gt = (<$> getLine) \case "" -> Nothing; "d' -> Just Delete; s -> Just (Value s)+> getElems NilR gt :: IO (LengthR 3 String)+foo+bar+d+boo++baz+((NilR :+ "foo") :+ "boo") :+ "baz"+> getElems NilR gt :: IO (LengthR 3 String)+foo+bar+d+d+hoge+piyo+baz+((NilR :+ "hoge") :+ "piyo") :+ "baz"+> getElems NilR gt :: IO (LengthR 3 String)+foo+bar+d+d+d+*** Exception: NothingToDeleteException+```++### function `titles`++You define the function `titles` which show values as string with title.++```haskell:sample/fourPointsOfRect.hs+titles :: (Show a, Applicative (LengthR n)) =>+	Int -> LengthR n String -> LengthR n a -> LengthR n String+titles n ts xs = (\t x -> t ++ replicate (n - length t) ' ' ++ ": " ++ show x)+	<$> ts <*> xs+```++Try it.++```+% stack ghci sample/fourPointsOfRect.hs+> titles 5 (NilR :+ "foo" :+ "bar" :+ "baz") (NilR :+ 123 :+ 456 :+ 789)+((NilR :+ "foo  : 123") :+ "bar  : 456") :+ "baz  : 789"+```++### function `printResult`++You define the function `printResult` which show values expressing a rectangle+and 4 points of rectangle.++```haskell:sample/fourPointsOfRect.hs+printResult :: LengthR 4 Double -> IO ()+printResult r = do+	putStrLn ""+	putStrLn `mapM_` titles 6 t r; putStrLn ""+	putStrLn `mapM_` titles 12 u (fourPoints r); putStrLn ""+	where+	t = NilR :+ "left :+ "top" :+ "width" :+ "height"+	u = NIlR :+ "left-top" :+ "right-top" :+ "left-bottom" :+ "right-bottom"+```++Try it.++```+% stack ghci sample/fourPointsOfRect.hs+> printResult $ NilR :+ 300 :+ 200 :+ 70 :+ 50++left  : 300.0+top   : 200.0+width : 70.0+height: 50.0++left-top    : (300.0,200.0)+right-top   : (370.0,200.0)+left-bottom : (300.0,250.0)+right-bottom: (370.0,250.0)+```++### function `getRect`++You define the function `getRect` which gets user input to make rectangle.++```haskell:sample/fourPointsOfRect.hs+getRect :: forall n . GetElems n (4 - n) =>+	LengthR n Double -> IO (LengthR 4 Double)+getRect xs = (<$) <$> id <*> printRect =<<+	getElems @n @(4 - n) xs ((<$> getLine) \case+		"d" -> Just Delete; l -> Value <*> readMaybe l)+	`catch`+	\(_ :: NothingToDeleteException) ->+		putStrLn *** Nothing to delete." >> getRect @0 NilR+```++It gets a user input with `getLine`.+If it is `"d"`, then it deletes the last input.+If there are nothing to delete, then `NothingToDeleteException` occur.+It catches this exception and shows error message and rerun `getRect`.++### function `main`++You define function `main`.++```haskell:sample/fourPointsOfRect.hs+main :: IO ()+main = getRect NilR >>= fix \go xa@(xs :+ _) -> getLine >>= \case+	"q" -> pure ()+	"d" -> go =<< getRect xs+	_ -> putStrLn "q or d" >> go xa+```++It call function `getRect` with list of `0` elements (`NilR`).+And it repeats function `getRect` with list of `4 - 1` elements (`xs`)+if you input `"d"`.++```+% stack ghc sample/fourPointsOfRect.hs+% ./sample/fourPointsOfRect+500+300+75+50++left  : 500.0+top   : 300.0+width : 75.0+height: 50.0++left-top    : (500.0,300.0)+right-top   : (575.0,300.0)+left-bottom : (500.0,350.0)+right-bottom: (575.0,350.0)++d+d+125+100++left  : 500.0+top   : 300.0+width : 125.0+height: 100.0++left-top    : (500.0,300.0)+right-top   : (625.0,300.0)+left-bottom : (500.0,400.0)+right-bottom: (625.0,400.0)++d+d+d+d+d+*** Nothing to delete.+2000+1500+90+50++left  : 2000.0+top   : 1500.0+width : 90.0+height: 50.0++left-top    : (2000.0,1500.0)+right-top   : (2090.0,1500.0)+left-bottom : (2000.0,1550.0)+right-bottom: (2090.0,1550.0)++q+```++## RangeL and RangeR++### To specify the range of a number of elements of a list++You can specify the range of a number of elements of a list.+There is a data type `RangeL n m a`.+It represents a list which have a type `a` element.+And its length is `n` at minimum and `m` at maximum.++```+% stack ghci+> :module Data.List.Range+> :set -XDataKinds+> 'h' :. 'e' :. 'l' :. 'l' :.. 'o' :.. NilL :: RangeL 3 8 Char+'h' :. ('e' :. ('l' :. ('l' :.. ('o' :.. NilL))))+```++### To get passwords++Suppose you want to get a password+whose length is 8 at minimum and 127 at maximum.+First of all, you define headers.++```haskell:sample/password.hs+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++import Data.List.Range+import System.IO++import qualified Data.ByteString.Char8 as BSC+```++You define `type Password`.++```haskell:sample/password.hs+type Password = RangeL 8 127 Char+```++It is a list of `Char`.+Its length is 8 at minimum and 127 at maximum.++You define a function `getRangedString`.+It recieves a user input.+It return a just value if the length of the input is within range.+It return a nothing value if the length of the input is out of range.++```haskell:sample/password.hs+getRangedPassword :: Unfoldr 0 n m => IO (Maybe (RangeL n m Char))+getRangedPassword = do+	e <- hGetEcho stdin+	hSetEcho stdin False+	unfoldrMRangeMaybe ((/= '\n') <$> hLookAhead stdin) getChar+		<* hSetEcho stdin e+```++It makes echo of stdin off.+It gets characters until you input `'\n'`.+And it makes echo of stdin on.++```+% stack ghci sample/password.hs+> :set -XDataKinds+> getRangedPassword :: IO (Maybe Password)+(Input "foobarbaz")+Just ('f' :. ('o' :. ('o' :. ('b' :. ('a' :. ('r' :. ('b' :. ('a' :. ('z' :..NilL)))))))))+> getRangedPassword :: IO (Maybe Password)+(Input "foo")+Nothing+> getRangedPassword :: IO (Maybe (RangeL 2 5 Char))+(Input "foobar")+Nothing+> r+```++You want to convert a value of type `Password` into a value of `ByteString`.+You can use other packages if you get password as a value of `ByteString`.++```haskell:sample/password.hs+passwordToByteString :: Password -> BSC.ByteString+passwordToByteString = foldr BSC.cons ""+```++You define function `main` to try it.++```haskell:sample/password.hs+main :: IO ()+main = do+	p <- getRangedPassword+	print p+	maybe (eror "bad password length") BSC.putStrLn $ passwordToByteString <$> p+```++Try it.++```+% stack ghc sample/password.hs+% ./sample/password+(Input "foobarbaz")+Just ('f' :. ('o' :. ('o' :. ('b' :. ('a' :. ('r' :. ('b' :. ('a' :. ('z' :.. NilL)))))))))+foobarbaz+```++### Finger Tree++The next example is Finger Tree.++[Finger Trees: A Simple General-purpose Data Structure](https://www.staff.city.ac.uk/~ross/papers/FingerTree.html)++#### Language Extension and Import List++Let's make headers.++```haskell:sample/fingertree.hs+{-# LANGUAGE ScopedTypeVariables, TypeApplications, InstanceSigs #-}+{-# LANGUAGE DataKinds, TypeOperators #-}You+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,+	UndecidableInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}++import GHC.TypeNats+import Data.List.Range+```++#### Types++You can describe Finger Tree as follows.++```haskell:sample/fingertree.hs+data FingerTree a+	= Enpty | Single a+	| Deep (DigitL a) (FingerTree (Node a)) (DigitR a)+	deriving Show++type Node = RangeL 2 3+type DigitL = RangeL 1 4+type DigitR = RangeR 1 4+```++A list of type `Node a` contains two or three elements of type `a`.+A list of type `DigitL a` contains one elements at minimum and+four elements at maximum.+A list of type `DigitR a` contains the same number of elements as `DigitL a`.+But you can push and pop a element from right.++#### To push from left++You define the function which Add a new element to the left of the sequence.+First of all you define the function to push an element to a list of type `DigitL a`.++```haskell:sample/fingertree.hs+infixr 5 <||++(<||) :: a -> DigitL a -> Either (DigitL a) (DigitL a, Node a)+a <|| b :. NilL = Left $ a :. b :.. NilL+a <|| b :. c :.. NilL = Left $ a :. b :.. c :.. NilL+a <|| b :. c :.. d :.. NilL = Left $ a :. b :.. c :.. d :.. NilL+a <|| b :. c :.. d :.. e :.. NilL =+	Right (a :. b :.. NilL, c :. d :. e :.. NilL)+```++If the original list has fewer elements than four,+then it return a left value list which contains the added value.+If the original list has just four elements,+then it returns a right value tuple which contain the value of type `DigitL a`+and the value of type `Node a`.++You can define the function which add a new element to the left of the sequence.++```haskell:sample/fingertree.hs+infixr 5 <|++(<|) :: a -> FingerTree a -> FingerTree a+a <| Empty = Single a+a <| Single a = Deep (a :. NilL) Empty (NilR :+ b)+a <| Deep pr m sf = case a <|| pr of+	Left pr' -> Deep pr' m sf+	Right (pr', n3) -> Deep pr' (n3 <| m) sf+```++It pushes three of the elements as a `Node`, leaving two behind.++You also require the liftings of `<|`.++```haskell:sample/fingertree.hs+infixr 5 <|.++(<|.) :: Foldable t => t a -> FingerTree a -> FingerTree a+(<|.) = flip $ foldr (<|)+```++To make finger tree from a list or other foldable structure,+you define a function `toTree`.++```haskell:sample/fingertree.hs+toTree :: Foldable t => t a -> FingerTree a+toTree = (<|. Empty)+```++#### To push from right++Adding to the right end of the sequence is the mirror image of the above.++```haskell:sample/fingertree.hs+infixl 5 ||>, |>, |>.++(||>) :: DigitR a -> a -> Either (DigitR a) (Node a, DigitR a)+NilR :+ a ||> b = Left $ NilR :++ a :+ b+NilR :++ a :+ b ||> c = Left $ NilR :++ a :++ b :+ c+NIlR :++ a :++ b :+ c ||> d = Left $ NilR :++ a :++ b :++ c :+ d+NilR :++ a :++ b :++ c :+ d ||> e =+	Right (a :. b :. c :.. NilL, NilR :++ d :+ e)++(|>) :: FingerTree a -> a -> FingerTree a+Empty |> a = Single a+Single a |> b = Deep (a :. NilL) Empty (NilR :+ b)+Deep pr m sf |> a = case sf ||> a of+	Left sf' -> Deep pr m sf'+	Right (n3, sf') -> Deep pr (m |> n3) sf'++(|>.) :: Foldable t => FingerTree a -> t a -> FingerTree a+(|>.) = foldl (|>)+```++#### To pop from left++To deconstruct a sequence, you define a function `uncons`.++```haskell:sample/fingertree.hs+uncons :: FingerTree a -> Maybe (a, FingerTree a)+uncons Empty = Nothing+uncons (Single x) = Just (x, Empty)+uncons (Deep (a :. pr') m sf) = Just (a, deepL pr' m sf)++deepL :: RangeL 0 3 a -> FingerTree (Node a) -> DigitR a -> FingerTree a+deepL NilL m sf = case uncons m of+	Nothing -> toTree sf+	Just (n, m') -> Deep (loosenL n) m' sf+deepL (a :.. pr) m sf = Deep (loosenL $ a :. pr) m sf+```++Since the prefix `pr` of a `Deep` tree contains at least one element,+you can get its head.+However, the tail of the prefix may be empty,+and thus unsuitable as a first argument to the Deep constructor.+Hence you define a smart constructor that differs from `Deep` by allowing the+prefix to contain zero to three elements,+and in the empty case uses a `uncons` of the middle tree to construct a tree of+the correct shape.++#### Concatenation++First of all you define a function which devide a list into a list of `Node`.+The original list has 3 elements at minimum and 12 elements at maximum.+The returned list has 1 node at minimum and 4 nodes at maximum.+The function has a type like the following.++```haskell+fun :: RangeL 3 12 a -> RangeL 1 4 (Node a)+```++You can define a more general function like the following.++```haskell+fun :: RangeL 3 m a -> RangeL 1 w (Node a)+```++`m` is 3 times `w`.++You define a class.++```haskell:sample/fingertree.hs+class Nodes m w where nodes :: RangeL 3 m a -> RangeL 1 w (Node a)+```++And you define instance when `m` is 3 and `w` is 1.++```haskell:sample/fingertree.hs+instance Nodes 3 1 where nodes = (:. NilL) . loosenL	+```++And you define instance of general case.++```haskell:sample/fingertree.hs+instance {-# OVERLAPPABLE #-} (2 <= w, Nodes (m - 3) (w - 1)) => Nodes m w where+	nodes :: forall a . RangeL 3 m a -> RangeL 1 w (Node a)+	nodes (a :. b :. c :. NilL) = (a :. b :. c :.. NilL) :. NilL+	nodes (a :. b :. c :. d :.. NilL) =+		(a :. b :. NilL) :. (c :. d :. NilL) :.. NilL+	nodes (a :. b :. c :. d :.. e :.. NilL) =+		(a :. b :. c :.. NilL) :. (d :. e :. NilL) :.. NilL+	nodes (a :. b :. c :. d :.. e :.. f :.. xs) =+		(a :. b :. c :.. NilL) .:..+			nodes @(m - 3) @(w - 1) (d :. e :. f :. xs)+```++Try it.++```+% stack ghci sample/fingertree.hs+> :set -XTypeApplications -XDataKinds+> xs = 1 :. 2 :. 3 :. 4 :.. 5 :.. 6 :.. 7 :.. 8 :.. NilL :: RangeL 3 12 Integer+> nodes @12 @4 xs+(1 :. (2 :. (3 :.. NilL))) :. ((4 :. (5 :. (6 :.. NilL))) :.. ((7 :. (8 :. NilL)) :.. NilL))+> :type it+it :: Num a => RangeL 1 4 (Node a)+```++You can combine the two digit argument into a list of Nodes+with the function `nodes`.+You can obtain a recursive function by+generalizing the concatenation function to take an additional list of elements.++```haskell:sample/fingertree.hs+app3 :: FingerTree a -> RangeL 1 4 a -> FingerTree a -> FingerTree a+app3 Empty m xs = m <|. xs+app3 xs m Empty = xs |>. m+app3 (Single x) m xs = x <| m <|. xs+app3 xs m (Single x) = xs |>. m |> x+app3 (Deep pr1 m1 sf1) m (Deep pr2 m2 sf2) =+	Deep pr1 (app3 m1 (nodes $ sf1 ++.. m ++. pr2) m2) sf2+```++To concatenate two finger trees, you take a head element from a second sequence.++```haskell:sample/fingertree.hs+(><) :: FingerTree a -> FingerTree a -> FingerTree a+l >< r = case uncons r of Nothing -> l; Just (x, r') -> app3 l (x :. NilL) r'+```

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,85 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.33.0.+--+-- see: https://github.com/sol/hpack+--+-- hash: 42c7def6fb4ed75b8b978a1de4cdf116653323fb1cee0e251bceaa00ef7be780++name:           ranged-list+version:        0.1.0.0+synopsis:       The list like structure whose length or range of length can be specified+description:    Please see the README on GitHub at <https://github.com/YoshikuniJujo/ranged-list#readme>+category:       List+homepage:       https://github.com/YoshikuniJujo/ranged-list#readme+bug-reports:    https://github.com/YoshikuniJujo/ranged-list/issues+author:         Yoshikuni Jujo+maintainer:     PAF01143@nifty.ne.jp+copyright:      Yoshikuni Jujo+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    ChangeLog.md+data-files:+    rectangle.hs+    word64.hs+    LengthR.hs+    fourPointsOfRect.hs+    password.hs+    fingertree.hs+data-dir:       sample++source-repository head+  type: git+  location: https://github.com/YoshikuniJujo/ranged-list++library+  exposed-modules:+      Data.List.Length+      Data.List.Range+      Data.List.Range.Nat+  other-modules:+      Control.Monad.Identity+      Control.Monad.State+      Data.List.Length.LengthL+      Data.List.Length.LengthR+      Data.List.Range.RangeL+      Data.List.Range.RangeR+      Paths_ranged_list+  hs-source-dirs:+      src+  build-depends:+      base >=4.7 && <5+    , typecheck-plugin-nat-simple+  default-language: Haskell2010++test-suite ranged-list-doctest+  type: exitcode-stdio-1.0+  main-is: doctests.hs+  other-modules:+      Paths_ranged_list+  hs-source-dirs:+      test+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base >=4.7 && <5+    , doctest+    , ranged-list+    , typecheck-plugin-nat-simple+  default-language: Haskell2010++test-suite ranged-list-test+  type: exitcode-stdio-1.0+  main-is: spec.hs+  other-modules:+      Paths_ranged_list+  hs-source-dirs:+      test+  ghc-options: -threaded -rtsopts -with-rtsopts=-N+  build-depends:+      base >=4.7 && <5+    , ranged-list+    , typecheck-plugin-nat-simple+  default-language: Haskell2010

@@ -0,0 +1,9 @@+{-# LANGUAGE DataKinds #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module LengthR where++import Data.List.Length++hello :: LengthR 5 Char+hello = NilR :+ 'h' :+ 'e' :+ 'l' :+ 'l' :+ 'o'

@@ -0,0 +1,108 @@+{-# LANGUAGE ScopedTypeVariables, TypeApplications, InstanceSigs #-}+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,+	UndecidableInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}++import GHC.TypeNats+import Data.List.Range++data FingerTree a+	= Empty | Single a+	| Deep (DigitL a) (FingerTree (Node a)) (DigitR a)+	deriving Show++type Node = RangeL 2 3+type DigitL = RangeL 1 4+type DigitR = RangeR 1 4++infixr 5 <||++(<||) :: a -> DigitL a -> Either (DigitL a) (DigitL a, Node a)+a <|| b :. NilL = Left $ a :. b :.. NilL+a <|| b :. c :.. NilL = Left $ a :. b :.. c :.. NilL+a <|| b :. c :.. d :.. NilL = Left $ a :. b :.. c :.. d :.. NilL+a <|| b :. c :.. d :.. e :.. NilL =+	Right (a :. b :.. NilL, c :. d :. e :.. NilL)++infixr 5 <|++(<|) :: a -> FingerTree a -> FingerTree a+a <| Empty = Single a+a <| Single b = Deep (a :. NilL) Empty (NilR :+ b)+a <| Deep pr m sf = case a <|| pr of+	Left pr' -> Deep pr' m sf+	Right (pr', n3) -> Deep pr' (n3 <| m) sf++infixr 5 <|.++(<|.) :: Foldable t => t a -> FingerTree a -> FingerTree a+(<|.) = flip $ foldr (<|)++toTree :: Foldable t => t a -> FingerTree a+toTree = (<|. Empty)++infixl 5 ||>, |>, |>.++(||>) :: DigitR a -> a -> Either (DigitR a) (Node a, DigitR a)+NilR :+ a ||> b = Left $ NilR :++ a :+ b+NilR :++ a :+ b ||> c = Left $ NilR :++ a :++ b :+ c+NilR :++ a :++ b :+ c ||> d = Left $ NilR :++ a :++ b :++ c :+ d+NilR :++ a :++ b :++ c :+ d ||> e =+	Right (a :. b :. c :.. NilL, NilR :++ d :+ e)++(|>) :: FingerTree a -> a -> FingerTree a+Empty |> a = Single a+Single a |> b = Deep (a :. NilL) Empty (NilR :+ b)+Deep pr m sf |> a = case sf ||> a of+	Left sf' -> Deep pr m sf'+	Right (n3, sf') -> Deep pr (m |> n3) sf'++(|>.) :: Foldable t => FingerTree a -> t a -> FingerTree a+(|>.) = foldl (|>)++uncons :: FingerTree a -> Maybe (a, FingerTree a)+uncons Empty = Nothing+uncons (Single x) = Just (x, Empty)+uncons (Deep (a :. pr') m sf) = Just (a, deepL pr' m sf)++deepL :: RangeL 0 3 a -> FingerTree (Node a) -> DigitR a -> FingerTree a+deepL NilL m sf = case uncons m of+	Nothing -> toTree sf+	Just (n, m') -> Deep (loosenL n) m' sf+deepL (a :.. pr) m sf = Deep (loosenL $ a :. pr) m sf++class Nodes m w where nodes :: RangeL 3 m a -> RangeL 1 w (Node a)++instance Nodes 3 1 where nodes = (:. NilL) . loosenL++instance {-# OVERLAPPABLE #-} (2 <= w, Nodes (m - 3) (w - 1)) => Nodes m w where+	nodes :: forall a . RangeL 3 m a -> RangeL 1 w (Node a)+	nodes (a :. b :. c :. NilL) = (a :. b :. c :.. NilL) :. NilL+	nodes (a :. b :. c :. d :.. NilL) =+		(a :. b :. NilL) :. (c :. d :. NilL) :.. NilL+	nodes (a :. b :. c :. d :.. e :.. NilL) =+		(a :. b :. c :.. NilL) :. (d :. e :. NilL) :.. NilL+	nodes (a :. b :. c :. d :.. e :.. f :.. xs) =+		(a :. b :. c :.. NilL) .:..+			nodes @(m - 3) @(w - 1) (d :. e :. f :. xs)++app3 :: FingerTree a -> RangeL 1 4 a -> FingerTree a -> FingerTree a+app3 Empty m xs = m <|. xs+app3 xs m Empty = xs |>. m+app3 (Single x) m xs = x <| m <|. xs+app3 xs m (Single x) = xs |>. m |> x+app3 (Deep pr1 m1 sf1) m (Deep pr2 m2 sf2) =+	Deep pr1 (app3 m1 (nodes $ sf1 ++.. m ++. pr2) m2) sf2++(><) :: FingerTree a -> FingerTree a -> FingerTree a+l >< r = case uncons r of Nothing -> l; Just (x, r') -> app3 l (x :. NilL) r'++main :: IO ()+main = do+	let	h = toTree "Hello, "+		w = toTree "world!"+	print h+	print $ uncons h+	print $ h >< w

@@ -0,0 +1,73 @@+{-# LANGUAGE BlockArguments, LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables, TypeApplications #-}+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,+	UndecidableInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}++import GHC.TypeNats+import Control.Monad.Fix+import Control.Monad.Catch+import Data.List.Length+import Text.Read++fourPoints :: LengthR 4 Double -> LengthR 4 (Double, Double)+fourPoints (NilR :+ l :+ t :+ w :+ h) =+	NilR :+ (l, t) :+ (l + w, t) :+ (l, t + h) :+ (l + w, t + h)++data DeleteOr a = Delete | Value a deriving Show+data NothingToDeleteException = NothingToDeleteException deriving Show+instance Exception NothingToDeleteException++class GetElems n v where+	getElems :: MonadThrow m =>+		LengthR n a -> m (Maybe (DeleteOr a)) -> m (LengthR (n + v) a)++instance GetElems 0 0 where getElems NilR _ = pure NilR++instance {-# OVERLAPPABLE #-} 1 <= n => GetElems n 0 where+	getElems xs@(_ :+ _) _ = pure xs++instance {-# OVERLAPPABLE #-} GetElems 1 (v - 1) => GetElems 0 v where+	getElems NilR gt = gt >>= \case+		Nothing -> getElems NilR gt+		Just Delete -> throwM NothingToDeleteException+		Just (Value x) -> getElems @1 @(v - 1) (NilR :+ x) gt++instance {-# OVERLAPPABLE #-}+	(1 <= n, GetElems (n - 1) (v + 1), GetElems (n + 1) (v - 1)) =>+	GetElems n v where+	getElems xa@(xs :+ _) gt = gt >>= \case+		Nothing -> getElems xa gt+		Just Delete -> getElems @(n - 1) @(v + 1) xs gt+		Just (Value x) -> getElems @(n + 1) @(v - 1) (xa :+ x) gt++titles :: (Show a, Applicative (LengthR n)) =>+	Int -> LengthR n String -> LengthR n a -> LengthR n String+titles n ts xs = (\t x -> t ++ replicate (n - length t) ' ' ++ ": " ++ show x)+	<$> ts <*> xs++printResult :: LengthR 4 Double -> IO ()+printResult r = do+	putStrLn ""+	putStrLn `mapM_` titles 6 t r; putStrLn ""+	putStrLn `mapM_` titles 12 u (fourPoints r); putStrLn ""+	where+	t = NilR :+ "left" :+ "top" :+ "width" :+ "height"+	u = NilR :+ "left-top" :+ "right-top" :+ "left-bottom" :+ "right-bottom"++getRect :: forall n . GetElems n (4 - n) =>+	LengthR n Double -> IO (LengthR 4 Double)+getRect xs = (<$) <$> id <*> printResult =<<+	getElems @n @(4 - n) xs ((<$> getLine) \case+		"d" -> Just Delete; l -> Value <$> readMaybe l)+	`catch`+	\(_ :: NothingToDeleteException) ->+		putStrLn "*** Nothing to delete." >> getRect @0 NilR++main :: IO ()+main = getRect NilR >>= fix \go xa@(xs :+ _) -> getLine >>= \case+	"q" -> pure ();+	"d" -> go =<< getRect xs+	_ -> putStrLn "q or d" >> go xa

@@ -0,0 +1,27 @@+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++import Data.List.Range+import System.IO++import qualified Data.ByteString.Char8 as BSC++type Password = RangeL 8 127 Char++getRangedPassword :: Unfoldr 0 n m => IO (Maybe (RangeL n m Char))+getRangedPassword = do+	e <- hGetEcho stdin+	hSetEcho stdin False+	unfoldrMRangeMaybe ((/= '\n') <$> hLookAhead stdin) getChar+		<* hSetEcho stdin e++passwordToByteString :: Password -> BSC.ByteString+passwordToByteString = foldr BSC.cons ""++main :: IO ()+main = do+	p <- getRangedPassword+	print p+	maybe (error "bad password length") BSC.putStrLn $ passwordToByteString <$> p

@@ -0,0 +1,15 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++import Data.List.Length++data Rect = Rect {+	left :: Double, top :: Double,+	width :: Double, height :: Double } deriving Show++makeRect :: LengthL 4 Double -> Rect+makeRect (l :. t :. w :. h :. NilL) = Rect l t w h++main :: IO ()+main = print $ map makeRect . fst $ chunksL [3, 5, 15, 2, 8, 4, 1, 9, 3, 5]

@@ -0,0 +1,40 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MonoLocalBinds #-}+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++import GHC.TypeNats+import Data.Foldable+import Data.List.Length+import Data.List.Range+import Data.Bits+import Data.Word+import Numeric++takeL :: (LoosenLMax 0 (n - 1) n, Unfoldr 0 n n, ListToLengthL n) =>+	a -> [a] -> LengthL n a+takeL d = either ((`fillL` d) . loosenLMax) fst . splitL++data Bit = O | I deriving Show++boolToBit :: Bool -> Bit+boolToBit = \case False -> O; True -> I++bitToNum63 :: (Num n, Bits n) => Bit -> n+bitToNum63 = \case O -> 0; I -> 1 `shiftL` 63++bitsToWord64 :: LengthL 64 Bit -> Word64+bitsToWord64 = foldl' (\w b -> w `shiftR` 1 .|. bitToNum63 b) 0++takeWord64 :: String -> Word64+takeWord64 = bitsToWord64 . takeL O . (boolToBit . (== '*') <$>)++main :: IO ()+main = do+	putStrLn $ takeWord64 sample1 `showHex` ""+	putStrLn $ takeWord64 sample2 `showHex` ""++sample1, sample2 :: String+sample1 = "...*..*..*...........*...**********...*************............******"+sample2 = "...*..*..*...........*.."

@@ -0,0 +1,12 @@+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Control.Monad.Identity (Identity(..)) where++newtype Identity a = Identity { runIdentity :: a } deriving Show++instance Functor Identity where fmap = (Identity .) . (. runIdentity)++instance Applicative Identity where+	pure = Identity; Identity f <*> Identity x = Identity $ f x++instance Monad Identity where Identity x >>= f = f x

@@ -0,0 +1,43 @@+{-# LANGUAGE BlockArguments #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Control.Monad.State (StateL(..), StateR(..)) where++import Control.Arrow (first, second)++---------------------------------------------------------------------------++-- * STATE LEFT+-- * STATE RIGHT++---------------------------------------------------------------------------+-- STATE LEFT+---------------------------------------------------------------------------++newtype StateL s a = StateL { runStateL :: s -> (a, s) }++instance Functor (StateL s) where f `fmap` StateL k = StateL $ (f `first`) . k++instance Applicative (StateL s) where+	pure = StateL . (,)+	StateL kf <*> mx =+		StateL \s -> let (f, s') = kf s in (f <$> mx) `runStateL` s'++instance Monad (StateL s) where+	StateL k >>= f = StateL \s -> let (x, s') = k s in f x `runStateL` s'++---------------------------------------------------------------------------+-- STATE RIGHT+---------------------------------------------------------------------------++newtype StateR s a = StateR { runStateR :: s -> (s, a) }++instance Functor (StateR s) where f `fmap` StateR k = StateR $ (f `second`) . k++instance Applicative (StateR s) where+	pure = StateR . flip (,)+	StateR kf <*> mx =+		StateR \s -> let (s', f) = kf s in (f <$> mx) `runStateR` s'++instance Monad (StateR s) where+	StateR k >>= f = StateR \s -> let (s', x) = k s in f x `runStateR` s'

@@ -0,0 +1,187 @@+{-# LANGUAGE BlockArguments, TupleSections #-}+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE FlexibleContexts #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.List.Length (+	-- * LENGTHED LIST LEFT+	-- ** Type+	LengthL, RangeL(NilL, (:.)),+	-- ** AddL+	AddL, (++.),+	-- ** Unfoldr+	-- *** class+	Unfoldr,+	-- *** without monad+	repeatL, fillL, unfoldr, unfoldrWithBase,+	-- *** with monad+	unfoldrM, unfoldrMWithBase,+	-- ** ZipL+	ZipL, zipL, zipWithL, zipWithML,+	-- ** ListToLengthL+	ListToLengthL, splitL, chunksL, chunksL',+	-- * LENGTHED LIST RIGHT+	-- ** Type+	LengthR, RangeR(NilR, (:+)),+	-- ** AddR+	AddR, (+++),+	-- ** Unfoldl+	-- *** class+	Unfoldl,+	-- *** without monad+	repeatR, fillR, unfoldl, unfoldlWithBase,+	-- *** with monad+	unfoldlM, unfoldlMWithBase,+	-- ** ZipR+	ZipR, zipR, zipWithR, zipWithMR,+	-- ** ListToLengthR+	ListToLengthR, listToLengthR, chunksR, chunksR',+	-- * LEFT TO RIGHT+	LeftToRight, (++.+), leftToRight,+	-- * RIGHT TO LEFT+	RightToLeft, (++..), rightToLeft ) where++import GHC.TypeNats (type (-))+import Control.Arrow (first, (***))+import Data.List.Range (+	RangeL(..), AddL, (++.), LoosenLMax, loosenLMax, Unfoldr,+	ZipL, zipL, zipWithL, zipWithML,+	RangeR(..), AddR, (+++), LoosenRMax, loosenRMax, Unfoldl,+	ZipR, zipR, zipWithR, zipWithMR,+	LeftToRight, (++.+), leftToRight, RightToLeft, (++..), rightToLeft )+import Data.List.Length.LengthL (+	LengthL, unfoldr, unfoldrWithBase, unfoldrM, unfoldrMWithBase,+	ListToLengthL, splitL )+import Data.List.Length.LengthR (+	LengthR, unfoldl, unfoldlWithBase, unfoldlM, unfoldlMWithBase,+	ListToLengthR, listToLengthR )++---------------------------------------------------------------------------++-- LENGTH LEFT+-- LENGTH RIGHT++---------------------------------------------------------------------------+-- LENGTH LEFT+---------------------------------------------------------------------------++repeatL :: Unfoldr 0 n n => a -> LengthL n a+repeatL = fillL NilL++{-^++To repeat a value of type @a@ to construct a list of type @LengthL n a@.++>>> :set -XDataKinds+>>> repeatL 'c' :: LengthL 5 Char+'c' :. ('c' :. ('c' :. ('c' :. ('c' :. NilL))))++-}++fillL :: Unfoldr n m m => RangeL n m a -> a -> LengthL m a+fillL = (`unfoldrWithBase` \x -> (x, x))++{-^++To fill a list of type @LengthL n a@ with a value of type @a@.++>>> :set -XDataKinds+>>> fillL ('a' :. 'b' :.. NilL) 'c' :: LengthL 5 Char+'a' :. ('b' :. ('c' :. ('c' :. ('c' :. NilL))))++-}++chunksL :: ListToLengthL n => [a] -> ([LengthL n a], RangeL 0 (n - 1) a)+chunksL = either ([] ,) (uncurry first . ((:) *** chunksL)) . splitL++{-^++To separate a list to multiple lengthed lists.+It return separeted lengthed lists and a not enough length fragment.++>>> :set -XTypeApplications -XDataKinds+>>> chunksL @3 "foo bar"+(['f' :. ('o' :. ('o' :. NilL)),' ' :. ('b' :. ('a' :. NilL))],'r' :.. NilL)++-}++chunksL' :: (Unfoldr 0 n n, LoosenLMax 0 (n - 1) n, ListToLengthL n) =>+	a -> [a] -> [LengthL n a]+chunksL' z xs = case chunksL xs of+	(cs, NilL) -> cs; (cs, rs) -> cs ++ [loosenLMax rs `fillL` z]++{-^++It is like chunksL.+But if there is a not enough length fragment, then it fill with a default value.++>>> :set -XTypeApplications -XDataKinds+>>> print `mapM_` chunksL' @3 '@' "foo bar"+'f' :. ('o' :. ('o' :. NilL))+' ' :. ('b' :. ('a' :. NilL))+'r' :. ('@' :. ('@' :. NilL))++-}++---------------------------------------------------------------------------+-- LENGTH RIGHT+---------------------------------------------------------------------------++repeatR :: Unfoldl 0 n n => a -> LengthR n a+repeatR = (`fillR` NilR)++{-^++To repeat a value of type @a@ to construct a list of type @LengthR n a@.++>>> :set -XDataKinds+>>> repeatR 'c' :: LengthR 5 Char+((((NilR :+ 'c') :+ 'c') :+ 'c') :+ 'c') :+ 'c'++-}++fillR :: Unfoldl n m m => a -> RangeR n m a -> LengthR m a+fillR = unfoldlWithBase \x -> (x, x)++{-^++To fill a list of type @LengthR n a@ with a default value.++>>> :set -XDataKinds+>>> fillR 'c' (NilR :++ 'a' :+ 'b') :: LengthR 5 Char+((((NilR :+ 'c') :+ 'c') :+ 'c') :+ 'a') :+ 'b'++-}++chunksR :: ListToLengthR n => [a] -> ([LengthR n a], RangeR 0 (n - 1) a)+chunksR = either ([] ,) (uncurry first . ((:) *** chunksR)) . listToLengthR++{-^++To separate a list to multiple lengthed lists.+It return separated lengthed lists and a not enough length fragment.++>>> :set -XTypeApplications -XDataKinds+>>> chunksR @3 "foo bar"+([((NilR :+ 'o') :+ 'o') :+ 'f',((NilR :+ 'a') :+ 'b') :+ ' '],NilR :++ 'r')++-}++chunksR' :: (Unfoldl 0 n n, LoosenRMax 0 (n - 1) n, ListToLengthR n) =>+	a -> [a] -> [LengthR n a]+chunksR' z xs = case chunksR xs of+	(cs, NilR) -> cs; (cs, rs) -> cs ++ [z `fillR` loosenRMax rs]++{-^++It is like @chunksR@.+But if there is a not enough length fragment, then it fill with a default value.++>>> :set -XTypeApplications -XDataKinds+>>> print `mapM_` chunksR' @3 '@' "foo bar"+((NilR :+ 'o') :+ 'o') :+ 'f'+((NilR :+ 'a') :+ 'b') :+ ' '+((NilR :+ '@') :+ '@') :+ 'r'++-}

@@ -0,0 +1,120 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.List.Length.LengthL (+	LengthL, unfoldr, unfoldrWithBase, unfoldrM, unfoldrMWithBase,+	ListToLengthL, splitL ) where++import GHC.TypeNats (type (-), type (<=))+import Control.Arrow (first, (+++))+import Control.Monad.State (StateL(..))+import Data.List.Range.RangeL (LengthL, RangeL(..), Unfoldr, unfoldrMRangeWithBase)++---------------------------------------------------------------------------++-- * TYPE+-- * UNFOLDR+-- * LIST TO LENGTH LEFT++---------------------------------------------------------------------------+-- TYPE+---------------------------------------------------------------------------++---------------------------------------------------------------------------+-- UNFOLDR+---------------------------------------------------------------------------++unfoldr :: Unfoldr 0 n n => (s -> (a, s)) -> s -> LengthL n a+unfoldr = unfoldrWithBase NilL++{-^++To evaluate function repeatedly to construct a list of type @LengthL n a@.+The function recieve a state and return an element value and a new state.++>>> :set -XDataKinds+>>> unfoldr (\n -> (2 * n, n + 1)) 0 :: LengthL 5 Integer+0 :. (2 :. (4 :. (6 :. (8 :. NilL))))++-}++unfoldrWithBase ::+	Unfoldr n m m => RangeL n m a -> (s -> (a, s)) -> s -> LengthL m a+unfoldrWithBase xs = (fst .) . runStateL . unfoldrMWithBase xs . StateL++{-^++It is like @unfoldr@. But it has already prepared values.++>>> :set -XDataKinds+>>> xs = 123 :. 456 :.. NilL :: RangeL 1 5 Integer+>>> unfoldrWithBase xs (\n -> (2 * n, n + 1)) 0 :: LengthL 5 Integer+123 :. (456 :. (0 :. (2 :. (4 :. NilL))))++-}++unfoldrM :: (Monad m, Unfoldr 0 n n) => m a -> m (LengthL n a)+unfoldrM = unfoldrMWithBase NilL++{-^++It is like @unfoldr@. But it use a monad as an argument instead of a function.++>>> :set -XDataKinds+>>> :module + Data.IORef+>>> r <- newIORef 1+>>> count = readIORef r >>= \n -> n <$ writeIORef r (n +1)+>>> unfoldrM count :: IO (LengthL 5 Integer)+1 :. (2 :. (3 :. (4 :. (5 :. NilL))))++-}++unfoldrMWithBase ::+	(Monad m, Unfoldr n w w) => RangeL n w a -> m a -> m (LengthL w a)+unfoldrMWithBase = (`unfoldrMRangeWithBase` undefined)++{-^++It is like @unfoldrM@. But it has already prepared values.++>>> :set -XDataKinds+>>> :module + Data.IORef+>>> r <- newIORef 1+>>> count = readIORef r >>= \n -> n <$ writeIORef r (n + 1)+>>> unfoldrMWithBase (123 :. 456 :.. NilL) count :: IO (LengthL 5 Integer)+123 :. (456 :. (1 :. (2 :. (3 :. NilL))))++-}++---------------------------------------------------------------------------+-- LIST TO LENGTH LEFT+---------------------------------------------------------------------------++class ListToLengthL n where+	splitL :: [a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])++	{-^++	To take a lengthed list from a list.+	If an original list has not enough elements, then it return+	a left value.++	>>> :set -XTypeApplications -XDataKinds+	>>> splitL @4 "Hi!"+	Left ('H' :.. ('i' :.. ('!' :.. NilL)))+	>>> splitL @4 "Hello!"+	Right ('H' :. ('e' :. ('l' :. ('l' :. NilL))),"o!")++	-}++instance ListToLengthL 1 where+	splitL = \case [] -> Left NilL; x : xs -> Right (x :. NilL, xs)++instance {-# OVERLAPPABLE #-}+	(1 <= n, 1 <= (n - 1), ListToLengthL (n - 1)) => ListToLengthL n where+	splitL = \case+		[] -> Left NilL+		x : xs -> (x :..) +++ ((x :.) `first`) $ splitL xs

@@ -0,0 +1,131 @@+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.List.Length.LengthR (+	LengthR, unfoldl, unfoldlWithBase, unfoldlM, unfoldlMWithBase,+	ListToLengthR, listToLengthR ) where++import GHC.TypeNats (type (-), type (<=))+import Control.Arrow (first, (+++))+import Control.Monad.State (StateR(..))+import Data.List.Range.RangeR (RangeR(..), Unfoldl, unfoldlMRangeWithBase)++---------------------------------------------------------------------------++-- TYPE+-- UNFOLDL+-- LIST TO LENGTH RIGHT++---------------------------------------------------------------------------+-- TYPE+---------------------------------------------------------------------------++type LengthR n = RangeR n n++{-^++@LengthR n a@ is a list which have just n members of type @a@.+You can push and pop an element from right.++>>> :set -XDataKinds+>>> sampleLengthR = NilR :+ 'h' :+ 'e' :+ 'l' :+ 'l' :+ 'o' :: LengthR 5 Char++-}++---------------------------------------------------------------------------+-- UNFOLDL+---------------------------------------------------------------------------++unfoldl :: Unfoldl 0 n n => (s -> (s, a)) -> s -> LengthR n a+unfoldl f s = unfoldlWithBase f s NilR++{-^++To eveluate function repeatedly to construct a list of type @LengthR n a@.+The function recieve a state and return a new state and an element value.++>>> :set -XDataKinds+>>> unfoldl (\n -> (n + 1, 2 * n)) 0 :: LengthR 5 Integer+((((NilR :+ 8) :+ 6) :+ 4) :+ 2) :+ 0++-}++unfoldlWithBase ::+	Unfoldl n m m => (s -> (s, a)) -> s -> RangeR n m a -> LengthR m a+unfoldlWithBase f = (snd .) . flip (runStateR . unfoldlMWithBase (StateR f))++{-^++It is like @unfoldl@. But it has already prepared values.++>>> :set -XDataKinds+>>> xs = NilR :++ 123 :+ 456 :: RangeR 1 5 Integer+>>> unfoldlWithBase (\n -> (n + 1, 2 * n)) 0 xs :: LengthR 5 Integer+((((NilR :+ 4) :+ 2) :+ 0) :+ 123) :+ 456++-}++unfoldlM :: (Monad m, Unfoldl 0 n n) => m a -> m (LengthR n a)+unfoldlM = (`unfoldlMWithBase` NilR)++{-^++It is like @unfoldl@. But it use monad as an argument instead of function.++>>> :set -XDataKinds+>>> :module + Data.IORef+>>> r <- newIORef 1+>>> count = readIORef r >>= \n -> n <$ writeIORef r (n + 1)+>>> unfoldlM count :: IO (LengthR 5 Integer)+((((NilR :+ 5) :+ 4) :+ 3) :+ 2) :+ 1++-}++unfoldlMWithBase ::+	(Monad m, Unfoldl n w w) => m a -> RangeR n w a -> m (LengthR w a)+unfoldlMWithBase = unfoldlMRangeWithBase undefined++{-^++It is like @unfoldlM@. But it has already prepared values.++>>> :set -XDataKinds+>>> :module + Data.IORef+>>> r <- newIORef 1+>>> count = readIORef r >>= \n -> n <$ writeIORef r (n + 1)+>>> unfoldlMWithBase count (NilR :++ 123 :+ 456) :: IO (LengthR 5 Integer)+((((NilR :+ 3) :+ 2) :+ 1) :+ 123) :+ 456++-}++---------------------------------------------------------------------------+-- LIST TO LENGTH RIGHT+---------------------------------------------------------------------------++class ListToLengthR n where+	listToLengthR :: [a] -> Either (RangeR 0 (n - 1) a) (LengthR n a, [a])++	{-^++	To take a lengthed list from a list.+	If an original list has not enough elements, then it return a left value.++	>>> :set -XTypeApplications -XDataKinds+	>>> listToLengthR @4 "Hi!"+	Left (((NilR :++ '!') :++ 'i') :++ 'H')+	>>> listToLengthR @4 "Hello!"+	Right ((((NilR :+ 'l') :+ 'l') :+ 'e') :+ 'H',"o!")++	-}++instance ListToLengthR 1 where+	listToLengthR = \case [] -> Left NilR; x : xs -> Right (NilR :+ x, xs)++instance {-# OVERLAPPABLE #-}+	(1 <= n, 1 <= (n - 1), ListToLengthR (n - 1)) => ListToLengthR n where+	listToLengthR = \case+		[] -> Left NilR+		x : xs -> (:++ x) +++ ((:+ x) `first`) $ listToLengthR xs

@@ -0,0 +1,372 @@+{-# LANGUAGE BlockArguments, LambdaCase #-}+{-# LANGUAGE ScopedTypeVariables, InstanceSigs #-}+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,+	UndecidableInstances #-}+{-# OPTIOnS_GHC -Wall -fno-warn-tabs -fplugin=Plugin.TypeCheck.Nat.Simple #-}++module Data.List.Range (+	-- * RANGED LIST LEFT+	module Data.List.Range.RangeL,+	-- ** Repeat and Unfoldr Min and Max+	-- *** repeat+	repeatLMin, repeatLMax,+	-- *** unfoldr+	unfoldrMin, unfoldrMax,+	-- *** unfoldrM+	unfoldrMMin, unfoldrMMax,+	-- * RANGED LIST RIGHT+	module Data.List.Range.RangeR,+	-- ** Repeat and Unfoldl Min and Max+	-- *** repeat+	repeatRMin, repeatRMax,+	-- *** unfoldl+	unfoldlMin, unfoldlMax,+	-- *** unfoldlM+	unfoldlMMin, unfoldlMMax,+	-- * LEFT TO RIGHT+	LeftToRight, (++.+), leftToRight,+	-- * RIGHT TO LEFT+	RightToLeft, (++..), rightToLeft ) where++import GHC.TypeNats (type (+), type (-), type (<=))+import Data.List.Length.LengthL (unfoldr, unfoldrM)+import Data.List.Length.LengthR (unfoldl, unfoldlM)+import Data.List.Range.RangeL+import Data.List.Range.RangeR++---------------------------------------------------------------------------++-- * RANGED LIST LEFT+--	+ MIN+--	+ MAX+-- * RANGED LIST RIGHT+--	+ MIN+--	+ MAX+-- * LEFT TO RIGHT+--	+ CLASS+--	+ INSTANCE+--	+ FUNCTION+-- * RIGHT TO LEFT+--	+ CLASS+--	+ INSTANCE+--	+ FUNCTION++---------------------------------------------------------------------------+-- RANGED LIST LEFT+---------------------------------------------------------------------------++-- MIN++repeatLMin :: (LoosenLMax n n m, Unfoldr 0 n n) => a -> RangeL n m a+repeatLMin = unfoldrMin \x -> (x, x)++{-^++To repeat a value minimum number of times.++>>> :set -XDataKinds+>>> repeatLMin 123 :: RangeL 3 5 Integer+123 :. (123 :. (123 :. NilL))++-}++unfoldrMin ::+	(LoosenLMax n n m, Unfoldr 0 n n) => (s -> (a, s)) -> s -> RangeL n m a+unfoldrMin f = loosenLMax . unfoldr f++{-^++To evaluate a function to construct values minimum number of times.+The function recieve a state and return a value and a new state.++>>> :set -XDataKinds+>>> unfoldrMin (\n -> (n * 3, n + 1)) 1 :: RangeL 3 5 Integer+3 :. (6 :. (9 :. NilL))++-}++unfoldrMMin ::+	(Monad m, LoosenLMax n n w, Unfoldr 0 n n) => m a -> m (RangeL n w a)+unfoldrMMin f = loosenLMax <$> unfoldrM f++{-^++It is like @unfoldrMin@. 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)+>>> unfoldrMMin count :: IO (RangeL 3 5 Integer)+3 :. (6 :. (9 :. NilL))++-}++-- MAX++repeatLMax :: (LoosenLMin m m n, Unfoldr 0 m m) => a -> RangeL n m a+repeatLMax = unfoldrMax \x -> (x, x)++{-^++To repeat a value maximum number of times.++>>> :set -XDataKinds+>>> repeatLMax 123 :: RangeL 3 5 Integer+123 :. (123 :. (123 :. (123 :.. (123 :.. NilL))))++-}++unfoldrMax ::+	(LoosenLMin m m n, Unfoldr 0 m m) => (s -> (a, s)) -> s -> RangeL n m a+unfoldrMax f = loosenLMin . unfoldr f++{-^++To evaluate a function to construct values maximum number of times.+The function recieve a state and return a value and a new state.++>>> :set -XDataKinds+>>> unfoldrMax (\n -> (n * 3, n + 1)) 1 :: RangeL 3 5 Integer+3 :. (6 :. (9 :. (12 :.. (15 :.. NilL))))++-}++unfoldrMMax ::+	(Monad m, LoosenLMin w w n, Unfoldr 0 w w) => m a -> m (RangeL n w a)+unfoldrMMax f = loosenLMin <$> unfoldrM f++{-^++It is like @unfoldrMax@. 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)+>>> unfoldrMMax count :: IO (RangeL 3 5 Integer)+3 :. (6 :. (9 :. (12 :.. (15 :.. NilL))))++-}++---------------------------------------------------------------------------+-- RANGED LIST RIGHT+---------------------------------------------------------------------------++-- MIN++repeatRMin :: (LoosenRMax n n m, Unfoldl 0 n n) => a -> RangeR n m a+repeatRMin = unfoldlMin \x -> (x, x)++{-^++To repeat a value minimum number of times.++>>> :set -XDataKinds+>>> repeatRMin 123 :: RangeR 3 5 Integer+((NilR :+ 123) :+ 123) :+ 123++-}++unfoldlMin ::+	(LoosenRMax n n m, Unfoldl 0 n n) => (s -> (s, a)) -> s -> RangeR n m a+unfoldlMin f = loosenRMax . unfoldl f++{-^++To evaluate a function to construct values minimum number of times.+The function recieves a state and return a value and a new state.++>>> :set -XDataKinds+>>> unfoldlMin (\n -> (n + 1, n * 3)) 1 :: RangeR 3 5 Integer+((NilR :+ 9) :+ 6) :+ 3++-}++unfoldlMMin ::+	(Monad m, LoosenRMax n n w, Unfoldl 0 n n) => m a -> m (RangeR n w a)+unfoldlMMin f = loosenRMax <$> unfoldlM f++{-^++It is like @unfoldlMax@. But it uses a monad instead of a function.++>>> :set -XDataKinds+>>> :module + Data.IORef+>>> r <- newIORef 1+>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)+>>> unfoldlMMin count :: IO (RangeR 3 5 Integer)+((NilR :+ 9) :+ 6) :+ 3++-}++-- MAX++repeatRMax :: (LoosenRMin m m n, Unfoldl 0 m m) => a -> RangeR n m a+repeatRMax = unfoldlMax \x -> (x, x)++{-^++To repeat a value maximum number of times.++>>> :set -XDataKinds+>>> repeatRMax 123 :: RangeR 3 5 Integer+((((NilR :++ 123) :++ 123) :+ 123) :+ 123) :+ 123++-}++unfoldlMax ::+	(LoosenRMin m m n, Unfoldl 0 m m) => (s -> (s, a)) -> s -> RangeR n m a+unfoldlMax f = loosenRMin . unfoldl f++{-^++To eveluate a function to construct values maximum number of times.+The function recieves a state and return a value and a new state.++>>> :set -XDataKinds+>>> unfoldlMax (\n -> (n + 1, n * 3)) 1 :: RangeR 3 5 Integer+((((NilR :++ 15) :++ 12) :+ 9) :+ 6) :+ 3++-}++unfoldlMMax ::+	(Monad m, LoosenRMin w w n, Unfoldl 0 w w) => m a -> m (RangeR n w a)+unfoldlMMax f = loosenRMin <$> unfoldlM f++{-^++It is like @unfoldlMax@. But it uses a monad instead of function.++>>> :set -XDataKinds+>>> :module + Data.IORef+>>> r <- newIORef 1+>>> count = readIORef r >>= \n -> n * 3 <$ writeIORef r (n + 1)+>>> unfoldlMMax count :: IO (RangeR 3 5 Integer)+((((NilR :++ 15) :++ 12) :+ 9) :+ 6) :+ 3++-}++---------------------------------------------------------------------------+-- LEFT TO RIGHT+---------------------------------------------------------------------------++-- CLASS++infixl 5 ++.+++class LeftToRight n m v w where+	(++.+) :: RangeR n m a -> RangeL v w a -> RangeR (n + v) (m + w) a++	{-^++	To concatenate a right-list and a left-list and return a right-list.++	>>> :set -XDataKinds+	>>> sampleLeftToRight1 = NilR :++ 'f' :++ 'o' :+ 'o' :: RangeR 1 4 Char+	>>> sampleLeftToRight2 = 'b' :. 'a' :. 'r' :.. NilL :: RangeL 2 3 Char+	>>> sampleLeftToRight1 ++.+ sampleLeftToRight2+	(((((NilR :++ 'f') :++ 'o') :++ 'o') :+ 'b') :+ 'a') :+ 'r'+	>>> :type sampleLeftToRight1 ++.+ sampleLeftToRight2+	sampleLeftToRight1 ++.+ sampleLeftToRight2 :: RangeR 3 7 Char++	-}++-- INSTANCE++instance LeftToRight n m 0 0 where n ++.+ _ = n++instance {-# OVERLAPPABLE #-} (+	PushR (n - 1) (m - 1), LoosenRMax n m (m + w),+	LeftToRight n (m + 1) 0 (w - 1) ) => LeftToRight n m 0 w where+	(++.+) n = \case NilL -> loosenRMax n; x :.. v -> n .:++ x ++.+ v++instance {-# OVERLAPPABLE #-}+	(1 <= v, LeftToRight (n + 1) (m + 1) (v - 1) (w - 1)) =>+	LeftToRight n m v w where+	(++.+) :: forall a .+		RangeR n m a -> RangeL v w a -> RangeR (n + v) (m + w) a+	n ++.+ x :. v = (n :+ x :: RangeR (n + 1) (m + 1) a) ++.+ v++-- FUNCTION++leftToRight ::+	forall v w a . LeftToRight 0 0 v w => RangeL v w a -> RangeR v w a+leftToRight = ((NilR :: RangeR 0 0 a) ++.+)++{-^++To convert a left-list to a right-list.++>>> :set -XDataKinds -fno-warn-tabs+>>> :{+	sampleLeftToRight :: RangeL 3 8 Char+	sampleLeftToRight = 'h' :. 'e' :. 'l' :. 'l' :.. 'o' :.. NilL+:}++>>> leftToRight sampleLeftToRight+((((NilR :++ 'h') :++ 'e') :+ 'l') :+ 'l') :+ 'o'++-}++---------------------------------------------------------------------------+-- RIGHT TO LEFT+---------------------------------------------------------------------------++-- CLASS++infixr 5 ++..++class RightToLeft n m v w where+	(++..) :: RangeR n m a -> RangeL v w a -> RangeL (n + v) (m + w) a++	{-^++	To concatenate a right-list and a left-list and return a left-list.++	>>> :set -XDataKinds+	>>> sampleRightToLeft1 = NilR :++ 'f' :++ 'o' :+ 'o' :: RangeR 1 4 Char+	>>> sampleRightToLeft2 = 'b' :. 'a' :. 'r' :.. NilL :: RangeL 2 3 Char+	>>> sampleRightToLeft1 ++.. sampleRightToLeft2+	'f' :. ('o' :. ('o' :. ('b' :.. ('a' :.. ('r' :.. NilL)))))++	-}++-- INSTANCE++instance RightToLeft 0 0 v w where _ ++.. v = v++instance {-# OVERLAPPABLE #-} (+	PushL (v - 1) (w - 1), LoosenLMax v w (m + w),+	RightToLeft 0 (m - 1) v (w + 1) ) => RightToLeft 0 m v w where+	(++..) = \case NilR -> loosenLMax; n :++ x -> (n ++..) . (x .:..)++instance {-# OVERLAPPABLE #-} (+	1 <= n, RightToLeft (n - 1) (m - 1) (v + 1) (w + 1) ) =>+	RightToLeft n m v w where+	(++..) :: forall a .+		RangeR n m a -> RangeL v w a -> RangeL (n + v) (m + w) a+	n :+ x ++.. v = n ++.. (x :. v :: RangeL (v + 1) (w + 1) a)++-- FUNCTION++rightToLeft ::+	forall n m a . RightToLeft n m 0 0 => RangeR n m a -> RangeL n m a+rightToLeft = (++.. (NilL :: RangeL 0 0 a))++{-^++To convert a right-list to a left-list.++>>> :set -XDataKinds+>>> :{+	sampleRightToLeft :: RangeR 3 8 Char+	sampleRightToLeft = NilR :++ 'h' :++ 'e' :+ 'l' :+ 'l' :+ 'o'+:}++>>> rightToLeft sampleRightToLeft+'h' :. ('e' :. ('l' :. ('l' :.. ('o' :.. NilL))))++-}

@@ -0,0 +1,152 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Data.List.Range.Nat (+	-- * RangedNatL+	RangedNatL, natL, toIntL, fromIntL, splitAtL,+	-- * RangedNatR+	RangedNatR, natR, toIntR, fromIntR, splitAtR ) where++import GHC.TypeNats (type (-))+import Data.Bool (bool)+import Data.List.Length (repeatL, repeatR)+import Data.List.Range (+	RangeL, Unfoldr, unfoldrRangeMaybe, ZipL, zipWithL,+	RangeR, Unfoldl, unfoldlRangeMaybe, ZipR, zipWithR )++---------------------------------------------------------------------------++-- * RANGED NAT LEFT+-- * RANGED NAT RIGHT++---------------------------------------------------------------------------+-- RANGED NAT LEFT+---------------------------------------------------------------------------++type RangedNatL n m = RangeL n m ()++natL :: Unfoldr 0 n n => RangedNatL n n+natL = repeatL ()++{-^++To make @RangedNatL@.++>>> :set -XTypeApplications -XDataKinds+>>> :module + Data.List.Range+>>> loosenL (natL @5) :: RangedNatL 3 8+() :. (() :. (() :. (() :.. (() :.. NilL))))++-}++toIntL :: Foldable (RangeL n m) => RangedNatL n m -> Int+toIntL = length++{-^++To convert from @RangedNatL@ to @Int@.++>>> :set -XTypeApplications -XDataKinds+>>> :module + Data.List.Range+>>> toIntL (loosenL (natL @5) :: RangedNatL 3 8)+5++-}++fromIntL :: Unfoldr 0 n m => Int -> Maybe (RangedNatL n m)+fromIntL = unfoldrRangeMaybe \s -> bool Nothing (Just ((), s - 1)) (s > 0)++{-^++To convert from @Int@ to @RangedNatL@.++>>> :set -XDataKinds+>>> fromIntL 5 :: Maybe (RangedNatL 3 8)+Just (() :. (() :. (() :. (() :.. (() :.. NilL)))))++-}++splitAtL :: ZipL n m v w => RangedNatL n m ->+	RangeL v w a -> (RangeL n m a, RangeL (v - m) (w - n) a)+splitAtL = zipWithL $ flip const++{-^++To split a list at position which is specified by number.++>>> :set -XTypeApplications -XDataKinds+>>> :module + Data.List.Range+>>> xs = 'h' :. 'e' :. 'l' :. 'l' :.. 'o' :.. NilL :: RangeL 3 8 Char+>>> splitAtL (natL @2) xs+('h' :. ('e' :. NilL),'l' :. ('l' :.. ('o' :.. NilL)))+>>> :type splitAtL (natL @2) xs+splitAtL (natL @2) xs :: (RangeL 2 2 Char, RangeL 1 6 Char)++-}++---------------------------------------------------------------------------+-- RANGED NAT RIGHT+---------------------------------------------------------------------------++type RangedNatR n m = RangeR n m ()++natR :: Unfoldl 0 n n => RangedNatR n n+natR = repeatR ()++{-^++To make @RangedNatR@.++>>> :set -XTypeApplications -XDataKinds+>>> :module + Data.List.Range+>>> loosenR (natR @5) :: RangedNatR 3 8+((((NilR :++ ()) :++ ()) :+ ()) :+ ()) :+ ()++-}++toIntR :: Foldable (RangeR n m) => RangedNatR n m -> Int+toIntR = length++{-^++To convert from @RangedNatR@ to @Int@.++>>> :set -XTypeApplications -XDataKinds+>>> :module + Data.List.Range+>>> toIntR (loosenR (natR @5) :: RangedNatR 3 8)+5++-}++fromIntR :: Unfoldl 0 n m => Int -> Maybe (RangedNatR n m)+fromIntR = unfoldlRangeMaybe \s -> bool Nothing (Just (s - 1, ())) (s > 0)++{-^++To convert @Int@ to @RangedNatR@.++>>> :set -XDataKinds+>>> fromIntR 5 :: Maybe (RangedNatR 3 8)+Just (((((NilR :++ ()) :++ ()) :+ ()) :+ ()) :+ ())++-}++splitAtR :: ZipR n m v w => RangeR n m a ->+	RangedNatR v w -> (RangeR (n - w) (m - v) a, RangeR v w a)+splitAtR = zipWithR const++{-^++To split a list at position which is specified by number.++>>> :set -XTypeApplications -XDataKinds+>>> :module + Data.List.Range+>>> xs = NilR :++ 'h' :++ 'e' :+ 'l' :+ 'l' :+ 'o' :: RangeR 3 8 Char+>>> splitAtR xs (natR @2)+(((NilR :++ 'h') :++ 'e') :+ 'l',(NilR :+ 'l') :+ 'o')+>>> :type splitAtR xs (natR @2)+splitAtR xs (natR @2) :: (RangeR 1 6 Char, RangeR 2 2 Char)++-}

@@ -0,0 +1,643 @@+{-# 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.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 -> * -> * 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 _ `fmap` NilL = NilL++instance {-# OVERLAPPABLE #-}+	Functor (RangeL 0 (m - 1)) => Functor (RangeL 0 m) where+	fmap f = \case NilL -> NilL; x :.. xs -> f x :.. (f <$> xs)++instance {-# OVERLAPPABLE #-}+	(1 <= n, Functor (RangeL (n - 1) (m - 1))) => Functor (RangeL n m) where+	f `fmap` (x :. xs) = f x :. (f <$> xs)++-- INSTANCE FOLDABLE++instance Foldable (RangeL 0 0) where foldr _ z NilL = z++instance {-# OVERLAPPABLE #-}+	Foldable (RangeL 0 (m - 1)) => Foldable (RangeL 0 m) where+	foldr (-<) z = \case NilL -> z; x :.. xs -> x -< foldr (-<) z xs++instance {-# OVERLAPPABLE #-} (1 <= n, Foldable (RangeL (n - 1) (m - 1))) =>+	Foldable (RangeL n m) where+	foldr (-<) z (x :. xs) = x -< foldr (-<) z xs++instance Applicative (LengthL 0) where pure _ = NilL; _ <*> _ = NilL++instance {-# OVERLAPPABLE #-} (Functor (RangeL 0 m), Applicative (RangeL 0 (m - 1)), Unfoldr 0 0 m) => Applicative (RangeL 0 m) where+	pure = unfoldrRange (const True) (\x -> (x, x))+	NilL <*> _ = NilL+	_ <*> NilL = NilL+	f :.. fs <*> x :.. xs = f x :.. (fs <*> 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 = unfoldrRange (const True) (\x -> (x, x))+	f :. fs <*> x :. xs = f x :. (fs <*> xs)++instance Applicative (LengthL 0) => Monad (LengthL 0) where+	NilL >>= _ = NilL++instance {-# OVERLAPPABLE #-} (1 <= n, Applicative (LengthL n), Monad (LengthL (n - 1))) => Monad (LengthL n) where+	x :. xs >>= f = y :. (xs >>= \z -> case f z of _ :. zs -> zs)+		where y :. _ = f x++-- INSTANCE ISSTRING++instance Unfoldr 0 n m => IsString (RangeL n m Char) where+	fromString s = fromMaybe (error $ "The string " ++ show s ++ " is not within range.")+		$ unfoldrRangeMaybe (\case "" -> Nothing; c : cs -> Just (c, cs)) s++instance (Foldable (RangeL n m), Unfoldr 0 n m) => IsList (RangeL n m a) where+	type Item (RangeL n m a) = a+	fromList lst = fromMaybe (error $ "The list is not within range.")+		$ unfoldrRangeMaybe (\case [] -> Nothing; x : xs -> Just (x, xs)) lst+	toList = 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+	(.:..) x = \case NilL -> x :.. NilL; xs@(_ :.. _) -> x :.. xs++instance {-# OVERLAPPABLE #-} (1 <= n, PushL (n - 1) (m - 1)) => PushL n m where+	x .:.. y :. ys = x :. (y .:.. 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 NilL ++. ys = 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+	NilL ++. ys = loosenLMax ys+	x :.. xs ++. ys = x .:.. (xs ++. ys :: RangeL v (m + w - 1) a)++instance {-# OVERLAPPABLE #-}+	(1 <= n, AddL (n - 1) (m - 1) v w) => AddL n m v w where+	x :. xs ++. ys = x :. (xs ++. ys)++---------------------------------------------------------------------------+-- LOOSEN+---------------------------------------------------------------------------++-- LOOSEN LEFT++loosenL :: (LoosenLMin n m v, LoosenLMax v m w) => RangeL n m a -> RangeL v w a+loosenL = loosenLMax . 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 = \case NilL -> NilL; xs@(_ :.. _) -> xs++instance {-# OVERLAPPABLE #-}+	(1 <= n, LoosenLMin (n - 1) (m - 1) 0) => LoosenLMin n m 0 where+	loosenLMin (x :. xs) = x :.. loosenLMin xs+	+instance {-# OVERLAPPABLE #-}+	(1 <= n, LoosenLMin (n - 1) (m - 1) (v - 1)) => LoosenLMin n m v where+	loosenLMin (x :. xs) = x :. loosenLMin 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 NilL = NilL++instance {-# OVERLAPPABLE #-}+	LoosenLMax 0 (m - 1) (w - 1) => LoosenLMax 0 m w where+	loosenLMax = \case NilL -> NilL; (x :.. xs) -> x :.. loosenLMax xs++instance {-# OVERLAPPABLE #-}+	(1 <= n, LoosenLMax (n - 1) (m - 1) (w - 1)) => LoosenLMax n m w where+	loosenLMax (x :. xs) = x :. loosenLMax 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 NilL _ _ = pure NilL+	unfoldrMRangeMaybeWithBase NilL p _ = bool (Just NilL) Nothing <$> p++instance {-# OVERLAPPABLE #-} Unfoldr 0 0 (w - 1) => Unfoldr 0 0 w where+	unfoldrMRangeWithBase NilL p f =+		(p >>=) . bool (pure NilL) $ f >>= \x ->+			(x :..) <$> unfoldrMRangeWithBase NilL p f+	unfoldrMRangeWithBase (x :.. xs) p f =+		(x :..) <$> unfoldrMRangeWithBase xs p f++	unfoldrMRangeMaybeWithBase NilL p f =+		(p >>=) . bool (pure $ Just NilL) $ f >>= \x ->+			((x :..) <$>) <$> unfoldrMRangeMaybeWithBase NilL p f+	unfoldrMRangeMaybeWithBase (x :.. xs) p f =+		((x :..) <$>) <$> unfoldrMRangeMaybeWithBase xs p f++instance {-# OVERLAPPABLE #-}+	Unfoldr 0 (v - 1) (w - 1) => Unfoldr 0 v w where+	unfoldrMRangeWithBase NilL p f =+		f >>= \x -> (x :.) <$> unfoldrMRangeWithBase NilL p f+	unfoldrMRangeWithBase (x :.. xs) p f =+		(x :.) <$> unfoldrMRangeWithBase xs p f++	unfoldrMRangeMaybeWithBase NilL p f =+		(p >>=) . bool (pure Nothing) $ f >>= \x ->+			((x :.) <$>) <$> unfoldrMRangeMaybeWithBase NilL p f+	unfoldrMRangeMaybeWithBase (x :.. xs) p f =+		((x :.) <$>) <$> unfoldrMRangeMaybeWithBase xs p f++instance {-# OVERLAPPABLE #-}+	(1 <= n, Unfoldr (n - 1) (v - 1) (w - 1)) => Unfoldr n v w where+	unfoldrMRangeWithBase (x :. xs) p f =+		(x :.) <$> unfoldrMRangeWithBase xs p f++	unfoldrMRangeMaybeWithBase (x :. xs) p f =+		((x :.) <$>) <$> unfoldrMRangeMaybeWithBase xs p f++-- UNFOLDR RANGE++unfoldrRange :: Unfoldr 0 v w =>+	(s -> Bool) -> (s -> (a, s)) -> s -> RangeL v w a+unfoldrRange = unfoldrRangeWithBase 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 xs p f = fst . unfoldrRangeWithBaseWithS xs p 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 xs p f =+	runStateL $ unfoldrMRangeWithBase xs (StateL $ p &&& id) (StateL 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 = unfoldrMRangeWithBase 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 = unfoldrRangeMaybeWithBase 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 xs f =+	fst . unfoldrRangeMaybeWithBaseGen xs (isJust &&& id)+		(maybe (error "never occur") (f `second`)) . 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 xs p f =+	runStateL $ unfoldrMRangeMaybeWithBase xs (StateL p) (StateL f)++unfoldrMRangeMaybe :: (Unfoldr 0 v w, Monad m) =>+	m Bool -> m a -> m (Maybe (RangeL v w a))+unfoldrMRangeMaybe = unfoldrMRangeMaybeWithBase 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 _ NilL = pure . (NilL ,)++instance {-# OVERLAPPABLE #-} (+	1 <= 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 _ NilL ys = pure (NilL, loosenLMin ys)+	zipWithML (%) (x :.. xs) (y :. ys) =+		x % y >>= \z -> ((z :..) *** loosenLMax) <$> zipWithML (%) xs 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 (%) (x :. xs) (y :. ys) =+		x % y >>= \z -> ((z :.) `first`) <$> zipWithML (%) xs 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 = 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 op = (runIdentity .) . zipWithML ((Identity .) . 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)++-}

@@ -0,0 +1,627 @@+{-# 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.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 -> * -> * 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 _ `fmap` NilR = NilR++instance {-# OVERLAPPABLE #-}+	Functor (RangeR 0 (m - 1)) => Functor (RangeR 0 m) where+	fmap f = \case NilR -> NilR; xs :++ x -> (f <$> xs) :++ f x++instance {-# OVERLAPPABLE #-}+	(1 <= n, Functor (RangeR (n - 1) (m - 1))) => Functor (RangeR n m) where+	f `fmap` (xs :+ x) = (f <$> xs) :+ f x++-- INSTANCE FOLDABLE++instance Foldable (RangeR 0 0) where foldr _ z NilR = z++instance {-# OVERLAPPABLE #-}+	Foldable (RangeR 0 (m - 1)) => Foldable (RangeR 0 m) where+	foldr (-<) z = \case NilR -> z; xs :++ x -> foldr (-<) (x -< z) xs++instance {-# OVERLAPPABLE #-} (1 <= n, Foldable (RangeR (n - 1) (m - 1))) =>+	Foldable (RangeR n m) where+	foldr (-<) z (xs :+ x) = foldr (-<) (x -< z) xs++instance Applicative (RangeR 0 0) where pure _ = NilR; _ <*> _ = 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 = unfoldlRange (const True) (\x -> (x, x))+	fs :+ f <*> xs :+ x = (fs <*> xs) :+ f x++instance {-# OVERLAPPABLE #-} (Functor (RangeR 0 m), Applicative (RangeR 0 (m - 1)), Unfoldl 0 0 m) => Applicative (RangeR 0 m) where+	pure = unfoldlRange (const True) (\x -> (x, x))+	NilR <*> _ = NilR+	_ <*> NilR = NilR+	fs :++ f <*> xs :++ x = (fs <*> xs) :++ f 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 = unfoldlRange (const True) (\x -> (x, x))+	fs :+ f <*> xs :+ x = (fs <*> xs) :+ f x++instance Applicative (RangeR 0 0) => Monad (RangeR 0 0) where NilR >>= _ = NilR+++instance {-# OVERLAPPABLE #-} (1 <= n, Applicative (RangeR n n), Monad (RangeR (n - 1) (n - 1))) => Monad (RangeR n n) where+	xs :+ x >>= f = (xs >>= \z -> case f z of zs :+ _ -> zs) :+ y+		where _ :+ y = f x++-- INSTANCE ISSTRING++instance Unfoldl 0 n m => IsString (RangeR n m Char) where+	fromString s = fromMaybe (error $ "The string " ++ show s ++ " is not within range.")+		. unfoldlRangeMaybe (\case "" -> Nothing; c : cs -> Just (cs, c)) $ reverse s++instance (Foldable (RangeR n m), Unfoldl 0 n m) => IsList (RangeR n m a) where+	type Item (RangeR n m a) = a+	fromList lst = fromMaybe (error $ "The list is not within range.")+		. unfoldlRangeMaybe (\case [] -> Nothing; x : xs -> Just (xs, x)) $ reverse lst+	toList = 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+	(.:++) = \case NilR -> (NilR :++); xs@(_ :++ _) -> (xs :++)++instance {-# OVERLAPPABLE #-} (1 <= n, PushR (n - 1) (m - 1)) => PushR n m where+	xs :+ x .:++ y = (xs .:++ x) :+ 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 xs +++ NilR = 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+	(+++) xs = \case+		NilR -> loosenRMax xs+		ys :++ y -> (xs +++ ys :: RangeR n (m + w - 1) a) .:++ y++instance {-# OVERLAPPABLE #-}+	(1 <= v, AddR n m (v - 1) (w - 1)) => AddR n m v w where+	xs +++ ys :+ y = (xs +++ ys) :+ y++---------------------------------------------------------------------------+-- LOOSEN+---------------------------------------------------------------------------++-- LOOSEN RIGHT++loosenR :: (LoosenRMin n m v, LoosenRMax v m w) => RangeR n m a -> RangeR v w a+loosenR = loosenRMax . 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 = \case NilR -> NilR; xs@(_ :++ _) -> xs++instance {-# OVERLAPPABLE #-}+	(1 <= n, LoosenRMin (n - 1) (m - 1) 0) => LoosenRMin n m 0 where+	loosenRMin (xs :+ x) = loosenRMin xs :++ x++instance {-# OVERLAPPABLE #-}+	(1 <= n, LoosenRMin (n - 1) (m - 1) (v - 1)) => LoosenRMin n m v where+	loosenRMin (xs :+ x) = loosenRMin xs :+ 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 NilR = NilR++instance {-# OVERLAPPABLE #-}+	LoosenRMax 0 (m - 1) (w - 1) => LoosenRMax 0 m w where+	loosenRMax = \case NilR -> NilR; xs :++ x -> loosenRMax xs :++ x++instance {-# OVERLAPPABLE #-}+	(1 <= n, LoosenRMax (n - 1) (m - 1) (w - 1)) => LoosenRMax n m w where+	loosenRMax (xs :+ x) = loosenRMax xs :+ 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 _ _ NilR = pure NilR+	unfoldlMRangeMaybeWithBase p _ NilR = bool (Just NilR) Nothing <$> p++instance {-# OVERLAPPABLE #-} Unfoldl 0 0 (w - 1) => Unfoldl 0 0 w where+	unfoldlMRangeWithBase p f = \case+		NilR -> (p >>=) . bool (pure NilR) $ f >>= \x ->+			(:++ x) <$> unfoldlMRangeWithBase p f NilR+		xs :++ x -> (:++ x) <$> unfoldlMRangeWithBase p f xs++	unfoldlMRangeMaybeWithBase p f = \case+		NilR -> (p >>=) . bool (pure $ Just NilR) $ f >>= \x ->+			((:++ x) <$>) <$> unfoldlMRangeMaybeWithBase p f NilR+		xs :++ x -> ((:++ x) <$>) <$> unfoldlMRangeMaybeWithBase p f xs++instance {-# OVERLAPPABLE #-} Unfoldl 0 (v - 1) (w - 1) => Unfoldl 0 v w where+	unfoldlMRangeWithBase p f = \case+		NilR -> f >>= \x -> (:+ x) <$> unfoldlMRangeWithBase p f NilR+		xs :++ x -> (:+ x) <$> unfoldlMRangeWithBase p f xs++	unfoldlMRangeMaybeWithBase p f = \case+		NilR -> (p >>=) . bool (pure Nothing) $ f >>= \x ->+			((:+ x) <$>) <$> unfoldlMRangeMaybeWithBase p f NilR+		xs :++ x -> ((:+ x) <$>) <$> unfoldlMRangeMaybeWithBase p f xs++instance {-# OVERLAPPABLE #-}+	(1 <= n, Unfoldl (n - 1) (v - 1) (w - 1)) => Unfoldl n v w where+	unfoldlMRangeWithBase p f (xs :+ x) =+		(:+ x) <$> unfoldlMRangeWithBase p f xs++	unfoldlMRangeMaybeWithBase p f (xs :+ x) =+		((:+ x) <$>) <$> unfoldlMRangeMaybeWithBase p f xs++-- UNFOLDL RANGE++unfoldlRange :: Unfoldl 0 v w =>+	(s -> Bool) -> (s -> (s, a)) -> s -> RangeR v w a+unfoldlRange p f s = unfoldlRangeWithBase p f s 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 p f = (snd .) . unfoldlRangeWithBaseWithS p 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 p f =+	flip $ runStateR . unfoldlMRangeWithBase (StateR $ id &&& p) (StateR 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 p f = unfoldlMRangeWithBase p f 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 f s = unfoldlRangeMaybeWithBase f s 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 f s xs =+	snd $ unfoldlRangeMaybeWithBaseGen (id &&& isJust)+		(maybe (error "never occur") (f `first`)) xs (f 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 p f =+	runStateR . unfoldlMRangeMaybeWithBase (StateR p) (StateR f)++unfoldlMRangeMaybe :: (Unfoldl 0 v w, Monad m) =>+	m Bool -> m a -> m (Maybe (RangeR v w a))+unfoldlMRangeMaybe p f = unfoldlMRangeMaybeWithBase p f 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 _ xs NilR = pure (xs, NilR)++instance {-# OVERLAPPABLE #-} (+	1 <= 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 _ xs NilR = pure (loosenRMin xs, NilR)+	zipWithMR (%) (xs :+ x) (ys :++ y) =+		x % y >>= \z -> (loosenRMax *** (:++ z)) <$> zipWithMR (%) xs 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 (%) (xs :+ x) (ys :+ y) =+		x % y >>= \z -> ((:+ z) `second`) <$> zipWithMR (%) xs 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 = 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 op = (runIdentity .) . zipWithMR ((Identity .) . 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)++-}

@@ -0,0 +1,12 @@+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++module Main (main) where++import Test.DocTest++main :: IO ()+main = doctest [+	"-isrc",+	"src/Data/List/Length.hs",+	"src/Data/List/Range.hs",+	"src/Data/List/Range/Nat.hs" ]

@@ -0,0 +1,32 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE DataKinds #-}+{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}++import Data.Bits+import Data.Word++import Data.List.Length+import Data.List.Range++main :: IO ()+main = do+	print $ foo 123; putStrLn ""+	print $ bar 123; putStrLn ""+	print baz; putStrLn ""+	print hoge; putStrLn ""++foo :: Word32 -> LengthL 32 Bool+foo = unfoldr \w -> (w `testBit` 0, w `shiftR` 1)++bar :: Word32 -> LengthR 32 Bool+bar = unfoldl \w -> (w `shiftR` 1, w `testBit` 0)++baz :: (RangeL 2 3 (Integer, Integer), RangeL 1 6 Integer)+baz = zipWithL (,)+	(1 :. 2 :. 3 :.. NilL :: RangeL 2 3 Integer)+	(1 :. 2 :. 3 :. 4 :. 5 :.. NilL :: RangeL 4 8 Integer)++hoge :: (RangeR 1 6 Integer, RangeR 2 3 (Integer, Integer))+hoge = zipWithR (,)+	(NilR :++ 1 :+ 2 :+ 3 :+ 4 :+ 5 :: RangeR 4 8 Integer)+	(NilR :++ 1 :+ 2 :+ 3 :: RangeR 2 3 Integer)