{-# 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 (
module Data.List.Range.RangeL,
repeatLMin, repeatLMax,
unfoldrMin, unfoldrMax,
unfoldrMMin, unfoldrMMax,
module Data.List.Range.RangeR,
repeatRMin, repeatRMax,
unfoldlMin, unfoldlMax,
unfoldlMMin, unfoldlMMax,
LeftToRight, (++.+), leftToRight,
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
repeatLMin :: (LoosenLMax n n m, Unfoldr 0 n n) => a -> RangeL n m a
repeatLMin :: a -> RangeL n m a
repeatLMin = (a -> (a, a)) -> a -> RangeL n m a
forall (n :: Nat) (m :: Nat) s a.
(LoosenLMax n n m, Unfoldr 0 n n) =>
(s -> (a, s)) -> s -> RangeL n m a
unfoldrMin \a
x -> (a
x, a
x)
unfoldrMin ::
(LoosenLMax n n m, Unfoldr 0 n n) => (s -> (a, s)) -> s -> RangeL n m a
unfoldrMin :: (s -> (a, s)) -> s -> RangeL n m a
unfoldrMin s -> (a, s)
f = RangeL n n a -> RangeL n m a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenLMax n m w =>
RangeL n m a -> RangeL n w a
loosenLMax (RangeL n n a -> RangeL n m a)
-> (s -> RangeL n n a) -> s -> RangeL n m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s -> (a, s)) -> s -> RangeL n n a
forall (n :: Nat) s a.
(0 <= n, Unfoldr 0 n n) =>
(s -> (a, s)) -> s -> LengthL n a
unfoldr s -> (a, s)
f
unfoldrMMin ::
(Monad m, LoosenLMax n n w, Unfoldr 0 n n) => m a -> m (RangeL n w a)
unfoldrMMin :: m a -> m (RangeL n w a)
unfoldrMMin m a
f = RangeL n n a -> RangeL n w a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenLMax n m w =>
RangeL n m a -> RangeL n w a
loosenLMax (RangeL n n a -> RangeL n w a)
-> m (RangeL n n a) -> m (RangeL n w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> m (RangeL n n a)
forall (m :: * -> *) (n :: Nat) a.
(Monad m, 0 <= n, Unfoldr 0 n n) =>
m a -> m (LengthL n a)
unfoldrM m a
f
repeatLMax :: (LoosenLMin m m n, Unfoldr 0 m m) => a -> RangeL n m a
repeatLMax :: a -> RangeL n m a
repeatLMax = (a -> (a, a)) -> a -> RangeL n m a
forall (m :: Nat) (n :: Nat) s a.
(LoosenLMin m m n, Unfoldr 0 m m) =>
(s -> (a, s)) -> s -> RangeL n m a
unfoldrMax \a
x -> (a
x, a
x)
unfoldrMax ::
(LoosenLMin m m n, Unfoldr 0 m m) => (s -> (a, s)) -> s -> RangeL n m a
unfoldrMax :: (s -> (a, s)) -> s -> RangeL n m a
unfoldrMax s -> (a, s)
f = RangeL m m a -> RangeL n m a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenLMin n m v =>
RangeL n m a -> RangeL v m a
loosenLMin (RangeL m m a -> RangeL n m a)
-> (s -> RangeL m m a) -> s -> RangeL n m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s -> (a, s)) -> s -> RangeL m m a
forall (n :: Nat) s a.
(0 <= n, Unfoldr 0 n n) =>
(s -> (a, s)) -> s -> LengthL n a
unfoldr s -> (a, s)
f
unfoldrMMax ::
(Monad m, LoosenLMin w w n, Unfoldr 0 w w) => m a -> m (RangeL n w a)
unfoldrMMax :: m a -> m (RangeL n w a)
unfoldrMMax m a
f = RangeL w w a -> RangeL n w a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenLMin n m v =>
RangeL n m a -> RangeL v m a
loosenLMin (RangeL w w a -> RangeL n w a)
-> m (RangeL w w a) -> m (RangeL n w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> m (RangeL w w a)
forall (m :: * -> *) (n :: Nat) a.
(Monad m, 0 <= n, Unfoldr 0 n n) =>
m a -> m (LengthL n a)
unfoldrM m a
f
repeatRMin :: (LoosenRMax n n m, Unfoldl 0 n n) => a -> RangeR n m a
repeatRMin :: a -> RangeR n m a
repeatRMin = (a -> (a, a)) -> a -> RangeR n m a
forall (n :: Nat) (m :: Nat) s a.
(LoosenRMax n n m, Unfoldl 0 n n) =>
(s -> (s, a)) -> s -> RangeR n m a
unfoldlMin \a
x -> (a
x, a
x)
unfoldlMin ::
(LoosenRMax n n m, Unfoldl 0 n n) => (s -> (s, a)) -> s -> RangeR n m a
unfoldlMin :: (s -> (s, a)) -> s -> RangeR n m a
unfoldlMin s -> (s, a)
f = RangeR n n a -> RangeR n m a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax (RangeR n n a -> RangeR n m a)
-> (s -> RangeR n n a) -> s -> RangeR n m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s -> (s, a)) -> s -> RangeR n n a
forall (n :: Nat) s a.
(0 <= n, Unfoldl 0 n n) =>
(s -> (s, a)) -> s -> LengthR n a
unfoldl s -> (s, a)
f
unfoldlMMin ::
(Monad m, LoosenRMax n n w, Unfoldl 0 n n) => m a -> m (RangeR n w a)
unfoldlMMin :: m a -> m (RangeR n w a)
unfoldlMMin m a
f = RangeR n n a -> RangeR n w a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax (RangeR n n a -> RangeR n w a)
-> m (RangeR n n a) -> m (RangeR n w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> m (RangeR n n a)
forall (m :: * -> *) (n :: Nat) a.
(Monad m, 0 <= n, Unfoldl 0 n n) =>
m a -> m (LengthR n a)
unfoldlM m a
f
repeatRMax :: (LoosenRMin m m n, Unfoldl 0 m m) => a -> RangeR n m a
repeatRMax :: a -> RangeR n m a
repeatRMax = (a -> (a, a)) -> a -> RangeR n m a
forall (m :: Nat) (n :: Nat) s a.
(LoosenRMin m m n, Unfoldl 0 m m) =>
(s -> (s, a)) -> s -> RangeR n m a
unfoldlMax \a
x -> (a
x, a
x)
unfoldlMax ::
(LoosenRMin m m n, Unfoldl 0 m m) => (s -> (s, a)) -> s -> RangeR n m a
unfoldlMax :: (s -> (s, a)) -> s -> RangeR n m a
unfoldlMax s -> (s, a)
f = RangeR m m a -> RangeR n m a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenRMin n m v =>
RangeR n m a -> RangeR v m a
loosenRMin (RangeR m m a -> RangeR n m a)
-> (s -> RangeR m m a) -> s -> RangeR n m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s -> (s, a)) -> s -> RangeR m m a
forall (n :: Nat) s a.
(0 <= n, Unfoldl 0 n n) =>
(s -> (s, a)) -> s -> LengthR n a
unfoldl s -> (s, a)
f
unfoldlMMax ::
(Monad m, LoosenRMin w w n, Unfoldl 0 w w) => m a -> m (RangeR n w a)
unfoldlMMax :: m a -> m (RangeR n w a)
unfoldlMMax m a
f = RangeR w w a -> RangeR n w a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenRMin n m v =>
RangeR n m a -> RangeR v m a
loosenRMin (RangeR w w a -> RangeR n w a)
-> m (RangeR w w a) -> m (RangeR n w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m a -> m (RangeR w w a)
forall (m :: * -> *) (n :: Nat) a.
(Monad m, 0 <= n, Unfoldl 0 n n) =>
m a -> m (LengthR n a)
unfoldlM m a
f
infixl 5 ++.+
class LeftToRight n m v w where
(++.+) :: RangeR n m a -> RangeL v w a -> RangeR (n + v) (m + w) a
instance LeftToRight n m 0 0 where RangeR n m a
n ++.+ :: RangeR n m a -> RangeL 0 0 a -> RangeR (n + 0) (m + 0) a
++.+ RangeL 0 0 a
_ = RangeR n m a
RangeR (n + 0) (m + 0) a
n
instance {-# OVERLAPPABLE #-} (
1 <= n, PushR (n - 1) (m - 1), LoosenRMax n m (m + w),
LeftToRight n (m + 1) 0 (w - 1) ) => LeftToRight n m 0 w where
++.+ :: RangeR n m a -> RangeL 0 w a -> RangeR (n + 0) (m + w) a
(++.+) RangeR n m a
n = \case RangeL 0 w a
NilL -> RangeR n m a -> RangeR n (m + w) a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax RangeR n m a
n; a
x :.. RangeL 0 (w - 1) a
v -> RangeR n m a
n RangeR n m a -> a -> RangeR n (m + 1) a
forall (n :: Nat) (m :: Nat) a.
PushR n m =>
RangeR n m a -> a -> RangeR n (m + 1) a
.:++ a
x RangeR n (m + 1) a
-> RangeL 0 (w - 1) a -> RangeR (n + 0) ((m + 1) + (w - 1)) a
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a.
LeftToRight n m v w =>
RangeR n m a -> RangeL v w a -> RangeR (n + v) (m + w) a
++.+ RangeL 0 (w - 1) a
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
RangeR n m a
n ++.+ :: RangeR n m a -> RangeL v w a -> RangeR (n + v) (m + w) a
++.+ a
x :. RangeL (v - 1) (w - 1) a
v = (RangeR n m a
RangeR ((n + 1) - 1) ((m + 1) - 1) a
n RangeR ((n + 1) - 1) ((m + 1) - 1) a
-> a -> RangeR (n + 1) (m + 1) a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
x :: RangeR (n + 1) (m + 1) a) RangeR (n + 1) (m + 1) a
-> RangeL (v - 1) (w - 1) a
-> RangeR ((n + 1) + (v - 1)) ((m + 1) + (w - 1)) a
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a.
LeftToRight n m v w =>
RangeR n m a -> RangeL v w a -> RangeR (n + v) (m + w) a
++.+ RangeL (v - 1) (w - 1) a
v
leftToRight ::
forall v w a . LeftToRight 0 0 v w => RangeL v w a -> RangeR v w a
leftToRight :: RangeL v w a -> RangeR v w a
leftToRight = ((RangeR 0 0 a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR :: RangeR 0 0 a) RangeR 0 0 a -> RangeL v w a -> RangeR (0 + v) (0 + w) a
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a.
LeftToRight n m v w =>
RangeR n m a -> RangeL v w a -> RangeR (n + v) (m + w) a
++.+)
infixr 5 ++..
class RightToLeft n m v w where
(++..) :: RangeR n m a -> RangeL v w a -> RangeL (n + v) (m + w) a
instance RightToLeft 0 0 v w where RangeR 0 0 a
_ ++.. :: RangeR 0 0 a -> RangeL v w a -> RangeL (0 + v) (0 + w) a
++.. RangeL v w a
v = RangeL v w a
RangeL (0 + v) (0 + w) a
v
instance {-# OVERLAPPABLE #-} (
1 <= v, PushL (v - 1) (w - 1), LoosenLMax v w (m + w),
RightToLeft 0 (m - 1) v (w + 1) ) => RightToLeft 0 m v w where
++.. :: RangeR 0 m a -> RangeL v w a -> RangeL (0 + v) (m + w) a
(++..) = \case RangeR 0 m a
NilR -> RangeL v w a -> RangeL (0 + v) (m + w) a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenLMax n m w =>
RangeL n m a -> RangeL n w a
loosenLMax; RangeR 0 (m - 1) a
n :++ a
x -> (RangeR 0 (m - 1) a
n RangeR 0 (m - 1) a
-> RangeL v (w + 1) a -> RangeL (0 + v) ((m - 1) + (w + 1)) a
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a.
RightToLeft n m v w =>
RangeR n m a -> RangeL v w a -> RangeL (n + v) (m + w) a
++..) (RangeL v (w + 1) a -> RangeL v ((m - 1) + (w + 1)) a)
-> (RangeL v w a -> RangeL v (w + 1) a)
-> RangeL v w a
-> RangeL v ((m - 1) + (w + 1)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
x a -> RangeL v w a -> RangeL v (w + 1) a
forall (n :: Nat) (m :: Nat) a.
PushL n m =>
a -> RangeL n m a -> RangeL n (m + 1) a
.:..)
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
RangeR (n - 1) (m - 1) a
n :+ a
x ++.. :: RangeR n m a -> RangeL v w a -> RangeL (n + v) (m + w) a
++.. RangeL v w a
v = RangeR (n - 1) (m - 1) a
n RangeR (n - 1) (m - 1) a
-> RangeL (v + 1) (w + 1) a
-> RangeL ((n - 1) + (v + 1)) ((m - 1) + (w + 1)) a
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a.
RightToLeft n m v w =>
RangeR n m a -> RangeL v w a -> RangeL (n + v) (m + w) a
++.. (a
x a
-> RangeL ((v + 1) - 1) ((w + 1) - 1) a -> RangeL (v + 1) (w + 1) a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:. RangeL v w a
RangeL ((v + 1) - 1) ((w + 1) - 1) a
v :: RangeL (v + 1) (w + 1) a)
rightToLeft ::
forall n m a . RightToLeft n m 0 0 => RangeR n m a -> RangeL n m a
rightToLeft :: RangeR n m a -> RangeL n m a
rightToLeft = (RangeR n m a -> RangeL 0 0 a -> RangeL (n + 0) (m + 0) a
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a.
RightToLeft n m v w =>
RangeR n m a -> RangeL v w a -> RangeL (n + v) (m + w) a
++.. (RangeL 0 0 a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL :: RangeL 0 0 a))