{-# LANGUAGE BlockArguments, TupleSections #-}
{-# LANGUAGE DataKinds, TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleContexts #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
module Data.List.Length (
LengthL, RangeL(NilL, (:.)),
AddL, (++.),
Unfoldr,
repeatL, fillL, unfoldr, unfoldrWithBase,
unfoldrM, unfoldrMWithBase,
ZipL, zipL, zipWithL, zipWithML,
ListToLengthL, splitL, chunksL, chunksL',
LengthR, RangeR(NilR, (:+)),
AddR, (+++),
Unfoldl,
repeatR, fillR, unfoldl, unfoldlWithBase,
unfoldlM, unfoldlMWithBase,
ZipR, zipR, zipWithR, zipWithMR,
ListToLengthR, listToLengthR, chunksR, chunksR',
LeftToRight, (++.+), leftToRight,
RightToLeft, (++..), rightToLeft ) where
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 )
import GHC.TypeNats
repeatL :: (0 <= n, Unfoldr 0 n n) => a -> LengthL n a
repeatL :: a -> LengthL n a
repeatL = RangeL 0 n a -> a -> LengthL n a
forall (n :: Nat) (m :: Nat) a.
Unfoldr n m m =>
RangeL n m a -> a -> LengthL m a
fillL RangeL 0 n a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL
fillL :: Unfoldr n m m => RangeL n m a -> a -> LengthL m a
fillL :: RangeL n m a -> a -> LengthL m a
fillL = (RangeL n m a -> (a -> (a, a)) -> a -> LengthL m a
forall (n :: Nat) (m :: Nat) a s.
Unfoldr n m m =>
RangeL n m a -> (s -> (a, s)) -> s -> LengthL m a
`unfoldrWithBase` \a
x -> (a
x, a
x))
chunksL :: ListToLengthL n => [a] -> ([LengthL n a], RangeL 0 (n - 1) a)
chunksL :: [a] -> ([LengthL n a], RangeL 0 (n - 1) a)
chunksL = (RangeL 0 (n - 1) a -> ([LengthL n a], RangeL 0 (n - 1) a))
-> ((LengthL n a, [a]) -> ([LengthL n a], RangeL 0 (n - 1) a))
-> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
-> ([LengthL n a], RangeL 0 (n - 1) a)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([] ,) ((([LengthL n a] -> [LengthL n a])
-> ([LengthL n a], RangeL 0 (n - 1) a)
-> ([LengthL n a], RangeL 0 (n - 1) a))
-> ([LengthL n a] -> [LengthL n a],
([LengthL n a], RangeL 0 (n - 1) a))
-> ([LengthL n a], RangeL 0 (n - 1) a)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ([LengthL n a] -> [LengthL n a])
-> ([LengthL n a], RangeL 0 (n - 1) a)
-> ([LengthL n a], RangeL 0 (n - 1) a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (([LengthL n a] -> [LengthL n a],
([LengthL n a], RangeL 0 (n - 1) a))
-> ([LengthL n a], RangeL 0 (n - 1) a))
-> ((LengthL n a, [a])
-> ([LengthL n a] -> [LengthL n a],
([LengthL n a], RangeL 0 (n - 1) a)))
-> (LengthL n a, [a])
-> ([LengthL n a], RangeL 0 (n - 1) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((:) (LengthL n a -> [LengthL n a] -> [LengthL n a])
-> ([a] -> ([LengthL n a], RangeL 0 (n - 1) a))
-> (LengthL n a, [a])
-> ([LengthL n a] -> [LengthL n a],
([LengthL n a], RangeL 0 (n - 1) a))
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [a] -> ([LengthL n a], RangeL 0 (n - 1) a)
forall (n :: Nat) a.
ListToLengthL n =>
[a] -> ([LengthL n a], RangeL 0 (n - 1) a)
chunksL)) (Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
-> ([LengthL n a], RangeL 0 (n - 1) a))
-> ([a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a]))
-> [a]
-> ([LengthL n a], RangeL 0 (n - 1) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
forall (n :: Nat) a.
ListToLengthL n =>
[a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
splitL
chunksL' :: (Unfoldr 0 n n, LoosenLMax 0 (n - 1) n, ListToLengthL n) =>
a -> [a] -> [LengthL n a]
chunksL' :: a -> [a] -> [LengthL n a]
chunksL' a
z [a]
xs = case [a] -> ([LengthL n a], RangeL 0 (n - 1) a)
forall (n :: Nat) a.
ListToLengthL n =>
[a] -> ([LengthL n a], RangeL 0 (n - 1) a)
chunksL [a]
xs of
([LengthL n a]
cs, RangeL 0 (n - 1) a
NilL) -> [LengthL n a]
cs; ([LengthL n a]
cs, RangeL 0 (n - 1) a
rs) -> [LengthL n a]
cs [LengthL n a] -> [LengthL n a] -> [LengthL n a]
forall a. [a] -> [a] -> [a]
++ [RangeL 0 (n - 1) a -> RangeL 0 n a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenLMax n m w =>
RangeL n m a -> RangeL n w a
loosenLMax RangeL 0 (n - 1) a
rs RangeL 0 n a -> a -> LengthL n a
forall (n :: Nat) (m :: Nat) a.
Unfoldr n m m =>
RangeL n m a -> a -> LengthL m a
`fillL` a
z]
repeatR :: (0 <= n, Unfoldl 0 n n) => a -> LengthR n a
repeatR :: a -> LengthR n a
repeatR = (a -> RangeR 0 n a -> LengthR n a
forall (n :: Nat) (m :: Nat) a.
Unfoldl n m m =>
a -> RangeR n m a -> LengthR m a
`fillR` RangeR 0 n a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR)
fillR :: Unfoldl n m m => a -> RangeR n m a -> LengthR m a
fillR :: a -> RangeR n m a -> LengthR m a
fillR = (a -> (a, a)) -> a -> RangeR n m a -> LengthR m a
forall (n :: Nat) (m :: Nat) s a.
Unfoldl n m m =>
(s -> (s, a)) -> s -> RangeR n m a -> LengthR m a
unfoldlWithBase \a
x -> (a
x, a
x)
chunksR :: ListToLengthR n => [a] -> ([LengthR n a], RangeR 0 (n - 1) a)
chunksR :: [a] -> ([LengthR n a], RangeR 0 (n - 1) a)
chunksR = (RangeR 0 (n - 1) a -> ([LengthR n a], RangeR 0 (n - 1) a))
-> ((LengthR n a, [a]) -> ([LengthR n a], RangeR 0 (n - 1) a))
-> Either (RangeR 0 (n - 1) a) (LengthR n a, [a])
-> ([LengthR n a], RangeR 0 (n - 1) a)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([] ,) ((([LengthR n a] -> [LengthR n a])
-> ([LengthR n a], RangeR 0 (n - 1) a)
-> ([LengthR n a], RangeR 0 (n - 1) a))
-> ([LengthR n a] -> [LengthR n a],
([LengthR n a], RangeR 0 (n - 1) a))
-> ([LengthR n a], RangeR 0 (n - 1) a)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ([LengthR n a] -> [LengthR n a])
-> ([LengthR n a], RangeR 0 (n - 1) a)
-> ([LengthR n a], RangeR 0 (n - 1) a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (([LengthR n a] -> [LengthR n a],
([LengthR n a], RangeR 0 (n - 1) a))
-> ([LengthR n a], RangeR 0 (n - 1) a))
-> ((LengthR n a, [a])
-> ([LengthR n a] -> [LengthR n a],
([LengthR n a], RangeR 0 (n - 1) a)))
-> (LengthR n a, [a])
-> ([LengthR n a], RangeR 0 (n - 1) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((:) (LengthR n a -> [LengthR n a] -> [LengthR n a])
-> ([a] -> ([LengthR n a], RangeR 0 (n - 1) a))
-> (LengthR n a, [a])
-> ([LengthR n a] -> [LengthR n a],
([LengthR n a], RangeR 0 (n - 1) a))
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [a] -> ([LengthR n a], RangeR 0 (n - 1) a)
forall (n :: Nat) a.
ListToLengthR n =>
[a] -> ([LengthR n a], RangeR 0 (n - 1) a)
chunksR)) (Either (RangeR 0 (n - 1) a) (LengthR n a, [a])
-> ([LengthR n a], RangeR 0 (n - 1) a))
-> ([a] -> Either (RangeR 0 (n - 1) a) (LengthR n a, [a]))
-> [a]
-> ([LengthR n a], RangeR 0 (n - 1) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Either (RangeR 0 (n - 1) a) (LengthR n a, [a])
forall (n :: Nat) a.
ListToLengthR n =>
[a] -> Either (RangeR 0 (n - 1) a) (LengthR n a, [a])
listToLengthR
chunksR' :: (Unfoldl 0 n n, LoosenRMax 0 (n - 1) n, ListToLengthR n) =>
a -> [a] -> [LengthR n a]
chunksR' :: a -> [a] -> [LengthR n a]
chunksR' a
z [a]
xs = case [a] -> ([LengthR n a], RangeR 0 (n - 1) a)
forall (n :: Nat) a.
ListToLengthR n =>
[a] -> ([LengthR n a], RangeR 0 (n - 1) a)
chunksR [a]
xs of
([LengthR n a]
cs, RangeR 0 (n - 1) a
NilR) -> [LengthR n a]
cs; ([LengthR n a]
cs, RangeR 0 (n - 1) a
rs) -> [LengthR n a]
cs [LengthR n a] -> [LengthR n a] -> [LengthR n a]
forall a. [a] -> [a] -> [a]
++ [a
z a -> RangeR 0 n a -> LengthR n a
forall (n :: Nat) (m :: Nat) a.
Unfoldl n m m =>
a -> RangeR n m a -> LengthR m a
`fillR` RangeR 0 (n - 1) a -> RangeR 0 n a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax RangeR 0 (n - 1) a
rs]