{-# 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 (
RangeR(..),
PushR, (.:++),
AddR, (+++),
loosenR,
LoosenRMin, loosenRMin,
LoosenRMax, loosenRMax,
Unfoldl,
unfoldlRange, unfoldlRangeWithBase, unfoldlRangeWithBaseWithS,
unfoldlMRange, unfoldlMRangeWithBase,
unfoldlRangeMaybe, unfoldlRangeMaybeWithBase,
unfoldlMRangeMaybe, unfoldlMRangeMaybeWithBase,
ZipR, zipR, zipWithR, zipWithMR ) where
import GHC.TypeNats (Nat, type (+), type (-), type (<=))
import GHC.Exts
import Control.Arrow (first, second, (***), (&&&))
import Control.Monad.Identity (Identity(..))
import Control.Monad.State (StateR(..))
import Data.Kind (Type)
import Data.Foldable
import Data.Bool (bool)
import Data.Maybe (isJust, fromMaybe)
data RangeR :: Nat -> Nat -> Type -> Type where
NilR :: 0 <= m => RangeR 0 m a
(:++) :: 1 <= m => RangeR 0 (m - 1) a -> a -> RangeR 0 m a
(:+) :: (1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
infixl 6 :+, :++
deriving instance Show a => Show (RangeR n m a)
instance Functor (RangeR 0 0) where a -> b
_ fmap :: (a -> b) -> RangeR 0 0 a -> RangeR 0 0 b
`fmap` RangeR 0 0 a
NilR = RangeR 0 0 b
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
instance {-# OVERLAPPABLE #-}
Functor (RangeR 0 (m - 1)) => Functor (RangeR 0 m) where
fmap :: (a -> b) -> RangeR 0 m a -> RangeR 0 m b
fmap a -> b
f = \case RangeR 0 m a
NilR -> RangeR 0 m b
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR; RangeR 0 (m - 1) a
xs :++ a
x -> (a -> b
f (a -> b) -> RangeR 0 (m - 1) a -> RangeR 0 (m - 1) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeR 0 (m - 1) a
xs) RangeR 0 (m - 1) b -> b -> RangeR 0 m b
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++ a -> b
f a
x
instance {-# OVERLAPPABLE #-}
(1 <= n, Functor (RangeR (n - 1) (m - 1))) => Functor (RangeR n m) where
a -> b
f fmap :: (a -> b) -> RangeR n m a -> RangeR n m b
`fmap` (RangeR (n - 1) (m - 1) a
xs :+ a
x) = (a -> b
f (a -> b) -> RangeR (n - 1) (m - 1) a -> RangeR (n - 1) (m - 1) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> RangeR (n - 1) (m - 1) a
xs) RangeR (n - 1) (m - 1) b -> b -> RangeR n m b
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a -> b
f a
x
instance Foldable (RangeR 0 0) where foldr :: (a -> b -> b) -> b -> RangeR 0 0 a -> b
foldr a -> b -> b
_ b
z RangeR 0 0 a
NilR = b
z
instance {-# OVERLAPPABLE #-}
Foldable (RangeR 0 (m - 1)) => Foldable (RangeR 0 m) where
foldr :: (a -> b -> b) -> b -> RangeR 0 m a -> b
foldr a -> b -> b
(-<) b
z = \case RangeR 0 m a
NilR -> b
z; RangeR 0 (m - 1) a
xs :++ a
x -> (a -> b -> b) -> b -> RangeR 0 (m - 1) a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
(-<) (a
x a -> b -> b
-< b
z) RangeR 0 (m - 1) a
xs
instance {-# OVERLAPPABLE #-} (1 <= n, Foldable (RangeR (n - 1) (m - 1))) =>
Foldable (RangeR n m) where
foldr :: (a -> b -> b) -> b -> RangeR n m a -> b
foldr a -> b -> b
(-<) b
z (RangeR (n - 1) (m - 1) a
xs :+ a
x) = (a -> b -> b) -> b -> RangeR (n - 1) (m - 1) a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> b -> b
(-<) (a
x a -> b -> b
-< b
z) RangeR (n - 1) (m - 1) a
xs
instance Traversable (RangeR 0 0) where traverse :: (a -> f b) -> RangeR 0 0 a -> f (RangeR 0 0 b)
traverse a -> f b
_ RangeR 0 0 a
NilR = RangeR 0 0 b -> f (RangeR 0 0 b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure RangeR 0 0 b
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
instance {-# OVERLAPPABLE #-}
Traversable (RangeR 0 (m - 1)) => Traversable (RangeR 0 m) where
traverse :: (a -> f b) -> RangeR 0 m a -> f (RangeR 0 m b)
traverse a -> f b
f = \case
RangeR 0 m a
NilR -> RangeR 0 m b -> f (RangeR 0 m b)
forall (f :: * -> *) a. Applicative f => a -> f a
pure RangeR 0 m b
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR; RangeR 0 (m - 1) a
xs :++ a
x -> RangeR 0 (m - 1) b -> b -> RangeR 0 m b
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
(:++) (RangeR 0 (m - 1) b -> b -> RangeR 0 m b)
-> f (RangeR 0 (m - 1) b) -> f (b -> RangeR 0 m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> RangeR 0 (m - 1) a -> f (RangeR 0 (m - 1) b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f RangeR 0 (m - 1) a
xs f (b -> RangeR 0 m b) -> f b -> f (RangeR 0 m b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> f b
f a
x
instance {-# OVERLAPPABLE #-} (1 <= n, Traversable (RangeR (n - 1) (m - 1))) =>
Traversable (RangeR n m) where
traverse :: (a -> f b) -> RangeR n m a -> f (RangeR n m b)
traverse a -> f b
f (RangeR (n - 1) (m - 1) a
xs :+ a
x) = RangeR (n - 1) (m - 1) b -> b -> RangeR n m b
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
(:+) (RangeR (n - 1) (m - 1) b -> b -> RangeR n m b)
-> f (RangeR (n - 1) (m - 1) b) -> f (b -> RangeR n m b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b)
-> RangeR (n - 1) (m - 1) a -> f (RangeR (n - 1) (m - 1) b)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse a -> f b
f RangeR (n - 1) (m - 1) a
xs f (b -> RangeR n m b) -> f b -> f (RangeR n m b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> a -> f b
f a
x
instance Applicative (RangeR 0 0) where pure :: a -> RangeR 0 0 a
pure a
_ = RangeR 0 0 a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR; RangeR 0 0 (a -> b)
_ <*> :: RangeR 0 0 (a -> b) -> RangeR 0 0 a -> RangeR 0 0 b
<*> RangeR 0 0 a
_ = RangeR 0 0 b
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
instance {-# OVERLAPPABLE #-} (1 <= n, Functor (RangeR n n), Applicative (RangeR (n - 1) (n - 1)), Unfoldl 0 n n) => Applicative (RangeR n n) where
pure :: a -> RangeR n n a
pure = (a -> Bool) -> (a -> (a, a)) -> a -> RangeR n n a
forall (v :: Nat) (w :: Nat) s a.
Unfoldl 0 v w =>
(s -> Bool) -> (s -> (s, a)) -> s -> RangeR v w a
unfoldlRange (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
True) (\a
x -> (a
x, a
x))
RangeR (n - 1) (n - 1) (a -> b)
fs :+ a -> b
f <*> :: RangeR n n (a -> b) -> RangeR n n a -> RangeR n n b
<*> RangeR (n - 1) (n - 1) a
xs :+ a
x = (RangeR (n - 1) (n - 1) (a -> b)
fs RangeR (n - 1) (n - 1) (a -> b)
-> RangeR (n - 1) (n - 1) a -> RangeR (n - 1) (n - 1) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RangeR (n - 1) (n - 1) a
xs) RangeR (n - 1) (n - 1) b -> b -> RangeR n n b
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a -> b
f a
x
instance {-# OVERLAPPABLE #-} (Functor (RangeR 0 m), Applicative (RangeR 0 (m - 1)), Unfoldl 0 0 m) => Applicative (RangeR 0 m) where
pure :: a -> RangeR 0 m a
pure = (a -> Bool) -> (a -> (a, a)) -> a -> RangeR 0 m a
forall (v :: Nat) (w :: Nat) s a.
Unfoldl 0 v w =>
(s -> Bool) -> (s -> (s, a)) -> s -> RangeR v w a
unfoldlRange (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
True) (\a
x -> (a
x, a
x))
RangeR 0 m (a -> b)
NilR <*> :: RangeR 0 m (a -> b) -> RangeR 0 m a -> RangeR 0 m b
<*> RangeR 0 m a
_ = RangeR 0 m b
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
RangeR 0 m (a -> b)
_ <*> RangeR 0 m a
NilR = RangeR 0 m b
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
RangeR 0 (m - 1) (a -> b)
fs :++ a -> b
f <*> RangeR 0 (m - 1) a
xs :++ a
x = (RangeR 0 (m - 1) (a -> b)
fs RangeR 0 (m - 1) (a -> b)
-> RangeR 0 (m - 1) a -> RangeR 0 (m - 1) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RangeR 0 (m - 1) a
xs) RangeR 0 (m - 1) b -> b -> RangeR 0 m b
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++ a -> b
f a
x
instance {-# OVERLAPPABLE #-} (1 <= n, Functor (RangeR n m), Applicative (RangeR (n - 1) (m - 1)), Unfoldl 0 n m) => Applicative (RangeR n m) where
pure :: a -> RangeR n m a
pure = (a -> Bool) -> (a -> (a, a)) -> a -> RangeR n m a
forall (v :: Nat) (w :: Nat) s a.
Unfoldl 0 v w =>
(s -> Bool) -> (s -> (s, a)) -> s -> RangeR v w a
unfoldlRange (Bool -> a -> Bool
forall a b. a -> b -> a
const Bool
True) (\a
x -> (a
x, a
x))
RangeR (n - 1) (m - 1) (a -> b)
fs :+ a -> b
f <*> :: RangeR n m (a -> b) -> RangeR n m a -> RangeR n m b
<*> RangeR (n - 1) (m - 1) a
xs :+ a
x = (RangeR (n - 1) (m - 1) (a -> b)
fs RangeR (n - 1) (m - 1) (a -> b)
-> RangeR (n - 1) (m - 1) a -> RangeR (n - 1) (m - 1) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> RangeR (n - 1) (m - 1) a
xs) RangeR (n - 1) (m - 1) b -> b -> RangeR n m b
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a -> b
f a
x
instance Applicative (RangeR 0 0) => Monad (RangeR 0 0) where RangeR 0 0 a
NilR >>= :: RangeR 0 0 a -> (a -> RangeR 0 0 b) -> RangeR 0 0 b
>>= a -> RangeR 0 0 b
_ = RangeR 0 0 b
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
instance {-# OVERLAPPABLE #-} (1 <= n, Applicative (RangeR n n), Monad (RangeR (n - 1) (n - 1))) => Monad (RangeR n n) where
RangeR (n - 1) (n - 1) a
xs :+ a
x >>= :: RangeR n n a -> (a -> RangeR n n b) -> RangeR n n b
>>= a -> RangeR n n b
f = (RangeR (n - 1) (n - 1) a
xs RangeR (n - 1) (n - 1) a
-> (a -> RangeR (n - 1) (n - 1) b) -> RangeR (n - 1) (n - 1) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
z -> case a -> RangeR n n b
f a
z of RangeR (n - 1) (n - 1) b
zs :+ b
_ -> RangeR (n - 1) (n - 1) b
zs) RangeR (n - 1) (n - 1) b -> b -> RangeR n n b
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ b
y
where RangeR (n - 1) (n - 1) b
_ :+ b
y = a -> RangeR n n b
f a
x
instance Unfoldl 0 n m => IsString (RangeR n m Char) where
fromString :: String -> RangeR n m Char
fromString String
s = RangeR n m Char -> Maybe (RangeR n m Char) -> RangeR n m Char
forall a. a -> Maybe a -> a
fromMaybe (String -> RangeR n m Char
forall a. HasCallStack => String -> a
error (String -> RangeR n m Char) -> String -> RangeR n m Char
forall a b. (a -> b) -> a -> b
$ String
"The string " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is not within range.")
(Maybe (RangeR n m Char) -> RangeR n m Char)
-> (String -> Maybe (RangeR n m Char)) -> String -> RangeR n m Char
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Maybe (String, Char))
-> String -> Maybe (RangeR n m Char)
forall (v :: Nat) (w :: Nat) s a.
Unfoldl 0 v w =>
(s -> Maybe (s, a)) -> s -> Maybe (RangeR v w a)
unfoldlRangeMaybe (\case String
"" -> Maybe (String, Char)
forall a. Maybe a
Nothing; Char
c : String
cs -> (String, Char) -> Maybe (String, Char)
forall a. a -> Maybe a
Just (String
cs, Char
c)) (String -> RangeR n m Char) -> String -> RangeR n m Char
forall a b. (a -> b) -> a -> b
$ ShowS
forall a. [a] -> [a]
reverse String
s
instance (Foldable (RangeR n m), Unfoldl 0 n m) => IsList (RangeR n m a) where
type Item (RangeR n m a) = a
fromList :: [Item (RangeR n m a)] -> RangeR n m a
fromList [Item (RangeR n m a)]
lst = RangeR n m a -> Maybe (RangeR n m a) -> RangeR n m a
forall a. a -> Maybe a -> a
fromMaybe (String -> RangeR n m a
forall a. HasCallStack => String -> a
error (String -> RangeR n m a) -> String -> RangeR n m a
forall a b. (a -> b) -> a -> b
$ String
"The list is not within range.")
(Maybe (RangeR n m a) -> RangeR n m a)
-> ([a] -> Maybe (RangeR n m a)) -> [a] -> RangeR n m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([a] -> Maybe ([a], a)) -> [a] -> Maybe (RangeR n m a)
forall (v :: Nat) (w :: Nat) s a.
Unfoldl 0 v w =>
(s -> Maybe (s, a)) -> s -> Maybe (RangeR v w a)
unfoldlRangeMaybe (\case [] -> Maybe ([a], a)
forall a. Maybe a
Nothing; a
x : [a]
xs -> ([a], a) -> Maybe ([a], a)
forall a. a -> Maybe a
Just ([a]
xs, a
x)) ([a] -> RangeR n m a) -> [a] -> RangeR n m a
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. [a] -> [a]
reverse [a]
[Item (RangeR n m a)]
lst
toList :: RangeR n m a -> [Item (RangeR n m a)]
toList = RangeR n m a -> [Item (RangeR n m a)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Data.Foldable.toList
infixl 5 .:++
class PushR n m where
(.:++) :: RangeR n m a -> a -> RangeR n (m + 1) a
instance PushR 0 m where
.:++ :: RangeR 0 m a -> a -> RangeR 0 (m + 1) a
(.:++) = \case RangeR 0 m a
NilR -> (RangeR 0 ((m + 1) - 1) a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR RangeR 0 ((m + 1) - 1) a -> a -> RangeR 0 (m + 1) a
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++); xs :: RangeR 0 m a
xs@(RangeR 0 (m - 1) a
_ :++ a
_) -> (RangeR 0 m a
RangeR 0 ((m + 1) - 1) a
xs RangeR 0 ((m + 1) - 1) a -> a -> RangeR 0 (m + 1) a
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++)
instance {-# OVERLAPPABLE #-} (1 <= n, PushR (n - 1) (m - 1)) => PushR n m where
RangeR (n - 1) (m - 1) a
xs :+ a
x .:++ :: RangeR n m a -> a -> RangeR n (m + 1) a
.:++ a
y = (RangeR (n - 1) (m - 1) a
xs RangeR (n - 1) (m - 1) a -> a -> RangeR (n - 1) ((m - 1) + 1) a
forall (n :: Nat) (m :: Nat) a.
PushR n m =>
RangeR n m a -> a -> RangeR n (m + 1) a
.:++ a
x) RangeR (n - 1) ((m + 1) - 1) a -> a -> RangeR n (m + 1) a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
y
infixl 5 +++
class AddR n m v w where
(+++) :: RangeR n m a -> RangeR v w a -> RangeR (n + v) (m + w) a
instance AddR n m 0 0 where RangeR n m a
xs +++ :: RangeR n m a -> RangeR 0 0 a -> RangeR (n + 0) (m + 0) a
+++ RangeR 0 0 a
NilR = RangeR n m a
RangeR (n + 0) (m + 0) a
xs
instance {-# OVERLAPPABLE #-}
(PushR n (m + w - 1), AddR n m 0 (w - 1), LoosenRMax n m (m + w)) =>
AddR n m 0 w where
(+++) :: forall a . RangeR n m a -> RangeR 0 w a -> RangeR n (m + w) a
+++ :: RangeR n m a -> RangeR 0 w a -> RangeR n (m + w) a
(+++) RangeR n m a
xs = \case
RangeR 0 w a
NilR -> RangeR n m a -> RangeR n (m + w) a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax RangeR n m a
xs
RangeR 0 (w - 1) a
ys :++ a
y -> (RangeR n m a
xs RangeR n m a
-> RangeR 0 (w - 1) a -> RangeR (n + 0) (m + (w - 1)) a
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a.
AddR n m v w =>
RangeR n m a -> RangeR v w a -> RangeR (n + v) (m + w) a
+++ RangeR 0 (w - 1) a
ys :: RangeR n (m + w - 1) a) RangeR n ((m + w) - 1) a -> a -> RangeR n (((m + w) - 1) + 1) a
forall (n :: Nat) (m :: Nat) a.
PushR n m =>
RangeR n m a -> a -> RangeR n (m + 1) a
.:++ a
y
instance {-# OVERLAPPABLE #-}
(1 <= v, AddR n m (v - 1) (w - 1)) => AddR n m v w where
RangeR n m a
xs +++ :: RangeR n m a -> RangeR v w a -> RangeR (n + v) (m + w) a
+++ RangeR (v - 1) (w - 1) a
ys :+ a
y = (RangeR n m a
xs RangeR n m a
-> RangeR (v - 1) (w - 1) a -> RangeR (n + (v - 1)) (m + (w - 1)) a
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a.
AddR n m v w =>
RangeR n m a -> RangeR v w a -> RangeR (n + v) (m + w) a
+++ RangeR (v - 1) (w - 1) a
ys) RangeR ((n + v) - 1) ((m + w) - 1) a
-> a -> RangeR (n + v) (m + w) a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
y
loosenR :: (LoosenRMin n m v, LoosenRMax v m w) => RangeR n m a -> RangeR v w a
loosenR :: RangeR n m a -> RangeR v w a
loosenR = RangeR v m a -> RangeR v w a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax (RangeR v m a -> RangeR v w a)
-> (RangeR n m a -> RangeR v m a) -> RangeR n m a -> RangeR v w a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangeR n m a -> RangeR v m a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenRMin n m v =>
RangeR n m a -> RangeR v m a
loosenRMin
class LoosenRMin n m v where
loosenRMin :: RangeR n m a -> RangeR v m a
instance LoosenRMin 0 m 0 where
loosenRMin :: RangeR 0 m a -> RangeR 0 m a
loosenRMin = \case RangeR 0 m a
NilR -> RangeR 0 m a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR; xs :: RangeR 0 m a
xs@(RangeR 0 (m - 1) a
_ :++ a
_) -> RangeR 0 m a
xs
instance {-# OVERLAPPABLE #-}
(1 <= n, LoosenRMin (n - 1) (m - 1) 0) => LoosenRMin n m 0 where
loosenRMin :: RangeR n m a -> RangeR 0 m a
loosenRMin (RangeR (n - 1) (m - 1) a
xs :+ a
x) = RangeR (n - 1) (m - 1) a -> RangeR 0 (m - 1) a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenRMin n m v =>
RangeR n m a -> RangeR v m a
loosenRMin RangeR (n - 1) (m - 1) a
xs RangeR 0 (m - 1) a -> a -> RangeR 0 m a
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++ a
x
instance {-# OVERLAPPABLE #-}
(1 <= n, 1 <= v, LoosenRMin (n - 1) (m - 1) (v - 1)) => LoosenRMin n m v where
loosenRMin :: RangeR n m a -> RangeR v m a
loosenRMin (RangeR (n - 1) (m - 1) a
xs :+ a
x) = RangeR (n - 1) (m - 1) a -> RangeR (v - 1) (m - 1) a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenRMin n m v =>
RangeR n m a -> RangeR v m a
loosenRMin RangeR (n - 1) (m - 1) a
xs RangeR (v - 1) (m - 1) a -> a -> RangeR v m a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
x
class LoosenRMax n m w where
loosenRMax :: RangeR n m a -> RangeR n w a
instance LoosenRMax 0 0 m where loosenRMax :: RangeR 0 0 a -> RangeR 0 m a
loosenRMax RangeR 0 0 a
NilR = RangeR 0 m a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
instance {-# OVERLAPPABLE #-}
(1 <= w, LoosenRMax 0 (m - 1) (w - 1)) => LoosenRMax 0 m w where
loosenRMax :: RangeR 0 m a -> RangeR 0 w a
loosenRMax = \case RangeR 0 m a
NilR -> RangeR 0 w a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR; RangeR 0 (m - 1) a
xs :++ a
x -> RangeR 0 (m - 1) a -> RangeR 0 (w - 1) a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax RangeR 0 (m - 1) a
xs RangeR 0 (w - 1) a -> a -> RangeR 0 w a
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++ a
x
instance {-# OVERLAPPABLE #-}
(1 <= n, 1 <= w, LoosenRMax (n - 1) (m - 1) (w - 1)) => LoosenRMax n m w where
loosenRMax :: RangeR n m a -> RangeR n w a
loosenRMax (RangeR (n - 1) (m - 1) a
xs :+ a
x) = RangeR (n - 1) (m - 1) a -> RangeR (n - 1) (w - 1) a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax RangeR (n - 1) (m - 1) a
xs RangeR (n - 1) (w - 1) a -> a -> RangeR n w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
x
class Unfoldl n v w where
unfoldlMRangeWithBase :: Monad m =>
m Bool -> m a -> RangeR n w a -> m (RangeR v w a)
unfoldlMRangeMaybeWithBase :: Monad m =>
m Bool -> m a -> RangeR n w a -> m (Maybe (RangeR v w a))
instance Unfoldl 0 0 0 where
unfoldlMRangeWithBase :: m Bool -> m a -> RangeR 0 0 a -> m (RangeR 0 0 a)
unfoldlMRangeWithBase m Bool
_ m a
_ RangeR 0 0 a
NilR = RangeR 0 0 a -> m (RangeR 0 0 a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure RangeR 0 0 a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
unfoldlMRangeMaybeWithBase :: m Bool -> m a -> RangeR 0 0 a -> m (Maybe (RangeR 0 0 a))
unfoldlMRangeMaybeWithBase m Bool
p m a
_ RangeR 0 0 a
NilR = Maybe (RangeR 0 0 a)
-> Maybe (RangeR 0 0 a) -> Bool -> Maybe (RangeR 0 0 a)
forall a. a -> a -> Bool -> a
bool (RangeR 0 0 a -> Maybe (RangeR 0 0 a)
forall a. a -> Maybe a
Just RangeR 0 0 a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR) Maybe (RangeR 0 0 a)
forall a. Maybe a
Nothing (Bool -> Maybe (RangeR 0 0 a))
-> m Bool -> m (Maybe (RangeR 0 0 a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool
p
instance {-# OVERLAPPABLE #-} (1 <= w, Unfoldl 0 0 (w - 1)) => Unfoldl 0 0 w where
unfoldlMRangeWithBase :: m Bool -> m a -> RangeR 0 w a -> m (RangeR 0 w a)
unfoldlMRangeWithBase m Bool
p m a
f = \case
RangeR 0 w a
NilR -> (m Bool
p m Bool -> (Bool -> m (RangeR 0 w a)) -> m (RangeR 0 w a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=) ((Bool -> m (RangeR 0 w a)) -> m (RangeR 0 w a))
-> (m (RangeR 0 w a) -> Bool -> m (RangeR 0 w a))
-> m (RangeR 0 w a)
-> m (RangeR 0 w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (RangeR 0 w a) -> m (RangeR 0 w a) -> Bool -> m (RangeR 0 w a)
forall a. a -> a -> Bool -> a
bool (RangeR 0 w a -> m (RangeR 0 w a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure RangeR 0 w a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR) (m (RangeR 0 w a) -> m (RangeR 0 w a))
-> m (RangeR 0 w a) -> m (RangeR 0 w a)
forall a b. (a -> b) -> a -> b
$ m a
f m a -> (a -> m (RangeR 0 w a)) -> m (RangeR 0 w a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x ->
(RangeR 0 (w - 1) a -> a -> RangeR 0 w a
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++ a
x) (RangeR 0 (w - 1) a -> RangeR 0 w a)
-> m (RangeR 0 (w - 1) a) -> m (RangeR 0 w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool -> m a -> RangeR 0 (w - 1) a -> m (RangeR 0 (w - 1) a)
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (RangeR v w a)
unfoldlMRangeWithBase m Bool
p m a
f RangeR 0 (w - 1) a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
RangeR 0 (w - 1) a
xs :++ a
x -> (RangeR 0 (w - 1) a -> a -> RangeR 0 w a
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++ a
x) (RangeR 0 (w - 1) a -> RangeR 0 w a)
-> m (RangeR 0 (w - 1) a) -> m (RangeR 0 w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool -> m a -> RangeR 0 (w - 1) a -> m (RangeR 0 (w - 1) a)
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (RangeR v w a)
unfoldlMRangeWithBase m Bool
p m a
f RangeR 0 (w - 1) a
xs
unfoldlMRangeMaybeWithBase :: m Bool -> m a -> RangeR 0 w a -> m (Maybe (RangeR 0 w a))
unfoldlMRangeMaybeWithBase m Bool
p m a
f = \case
RangeR 0 w a
NilR -> (m Bool
p m Bool
-> (Bool -> m (Maybe (RangeR 0 w a))) -> m (Maybe (RangeR 0 w a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=) ((Bool -> m (Maybe (RangeR 0 w a))) -> m (Maybe (RangeR 0 w a)))
-> (m (Maybe (RangeR 0 w a)) -> Bool -> m (Maybe (RangeR 0 w a)))
-> m (Maybe (RangeR 0 w a))
-> m (Maybe (RangeR 0 w a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (RangeR 0 w a))
-> m (Maybe (RangeR 0 w a)) -> Bool -> m (Maybe (RangeR 0 w a))
forall a. a -> a -> Bool -> a
bool (Maybe (RangeR 0 w a) -> m (Maybe (RangeR 0 w a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe (RangeR 0 w a) -> m (Maybe (RangeR 0 w a)))
-> Maybe (RangeR 0 w a) -> m (Maybe (RangeR 0 w a))
forall a b. (a -> b) -> a -> b
$ RangeR 0 w a -> Maybe (RangeR 0 w a)
forall a. a -> Maybe a
Just RangeR 0 w a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR) (m (Maybe (RangeR 0 w a)) -> m (Maybe (RangeR 0 w a)))
-> m (Maybe (RangeR 0 w a)) -> m (Maybe (RangeR 0 w a))
forall a b. (a -> b) -> a -> b
$ m a
f m a -> (a -> m (Maybe (RangeR 0 w a))) -> m (Maybe (RangeR 0 w a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x ->
((RangeR 0 (w - 1) a -> a -> RangeR 0 w a
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++ a
x) (RangeR 0 (w - 1) a -> RangeR 0 w a)
-> Maybe (RangeR 0 (w - 1) a) -> Maybe (RangeR 0 w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (RangeR 0 (w - 1) a) -> Maybe (RangeR 0 w a))
-> m (Maybe (RangeR 0 (w - 1) a)) -> m (Maybe (RangeR 0 w a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool
-> m a -> RangeR 0 (w - 1) a -> m (Maybe (RangeR 0 (w - 1) a))
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase m Bool
p m a
f RangeR 0 (w - 1) a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
RangeR 0 (w - 1) a
xs :++ a
x -> ((RangeR 0 (w - 1) a -> a -> RangeR 0 w a
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++ a
x) (RangeR 0 (w - 1) a -> RangeR 0 w a)
-> Maybe (RangeR 0 (w - 1) a) -> Maybe (RangeR 0 w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (RangeR 0 (w - 1) a) -> Maybe (RangeR 0 w a))
-> m (Maybe (RangeR 0 (w - 1) a)) -> m (Maybe (RangeR 0 w a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool
-> m a -> RangeR 0 (w - 1) a -> m (Maybe (RangeR 0 (w - 1) a))
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase m Bool
p m a
f RangeR 0 (w - 1) a
xs
instance {-# OVERLAPPABLE #-} (1 <= v, 1 <= w, Unfoldl 0 (v - 1) (w - 1)) => Unfoldl 0 v w where
unfoldlMRangeWithBase :: m Bool -> m a -> RangeR 0 w a -> m (RangeR v w a)
unfoldlMRangeWithBase m Bool
p m a
f = \case
RangeR 0 w a
NilR -> m a
f m a -> (a -> m (RangeR v w a)) -> m (RangeR v w a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x -> (RangeR (v - 1) (w - 1) a -> a -> RangeR v w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
x) (RangeR (v - 1) (w - 1) a -> RangeR v w a)
-> m (RangeR (v - 1) (w - 1) a) -> m (RangeR v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool -> m a -> RangeR 0 (w - 1) a -> m (RangeR (v - 1) (w - 1) a)
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (RangeR v w a)
unfoldlMRangeWithBase m Bool
p m a
f RangeR 0 (w - 1) a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
RangeR 0 (w - 1) a
xs :++ a
x -> (RangeR (v - 1) (w - 1) a -> a -> RangeR v w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
x) (RangeR (v - 1) (w - 1) a -> RangeR v w a)
-> m (RangeR (v - 1) (w - 1) a) -> m (RangeR v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool -> m a -> RangeR 0 (w - 1) a -> m (RangeR (v - 1) (w - 1) a)
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (RangeR v w a)
unfoldlMRangeWithBase m Bool
p m a
f RangeR 0 (w - 1) a
xs
unfoldlMRangeMaybeWithBase :: m Bool -> m a -> RangeR 0 w a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase m Bool
p m a
f = \case
RangeR 0 w a
NilR -> (m Bool
p m Bool
-> (Bool -> m (Maybe (RangeR v w a))) -> m (Maybe (RangeR v w a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=) ((Bool -> m (Maybe (RangeR v w a))) -> m (Maybe (RangeR v w a)))
-> (m (Maybe (RangeR v w a)) -> Bool -> m (Maybe (RangeR v w a)))
-> m (Maybe (RangeR v w a))
-> m (Maybe (RangeR v w a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (Maybe (RangeR v w a))
-> m (Maybe (RangeR v w a)) -> Bool -> m (Maybe (RangeR v w a))
forall a. a -> a -> Bool -> a
bool (Maybe (RangeR v w a) -> m (Maybe (RangeR v w a))
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (RangeR v w a)
forall a. Maybe a
Nothing) (m (Maybe (RangeR v w a)) -> m (Maybe (RangeR v w a)))
-> m (Maybe (RangeR v w a)) -> m (Maybe (RangeR v w a))
forall a b. (a -> b) -> a -> b
$ m a
f m a -> (a -> m (Maybe (RangeR v w a))) -> m (Maybe (RangeR v w a))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
x ->
((RangeR (v - 1) (w - 1) a -> a -> RangeR v w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
x) (RangeR (v - 1) (w - 1) a -> RangeR v w a)
-> Maybe (RangeR (v - 1) (w - 1) a) -> Maybe (RangeR v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (RangeR (v - 1) (w - 1) a) -> Maybe (RangeR v w a))
-> m (Maybe (RangeR (v - 1) (w - 1) a)) -> m (Maybe (RangeR v w a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool
-> m a
-> RangeR 0 (w - 1) a
-> m (Maybe (RangeR (v - 1) (w - 1) a))
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase m Bool
p m a
f RangeR 0 (w - 1) a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
RangeR 0 (w - 1) a
xs :++ a
x -> ((RangeR (v - 1) (w - 1) a -> a -> RangeR v w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
x) (RangeR (v - 1) (w - 1) a -> RangeR v w a)
-> Maybe (RangeR (v - 1) (w - 1) a) -> Maybe (RangeR v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (RangeR (v - 1) (w - 1) a) -> Maybe (RangeR v w a))
-> m (Maybe (RangeR (v - 1) (w - 1) a)) -> m (Maybe (RangeR v w a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool
-> m a
-> RangeR 0 (w - 1) a
-> m (Maybe (RangeR (v - 1) (w - 1) a))
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase m Bool
p m a
f RangeR 0 (w - 1) a
xs
instance {-# OVERLAPPABLE #-}
(1 <= n, 1 <= v, Unfoldl (n - 1) (v - 1) (w - 1)) => Unfoldl n v w where
unfoldlMRangeWithBase :: m Bool -> m a -> RangeR n w a -> m (RangeR v w a)
unfoldlMRangeWithBase m Bool
p m a
f (RangeR (n - 1) (w - 1) a
xs :+ a
x) =
(RangeR (v - 1) (w - 1) a -> a -> RangeR v w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
x) (RangeR (v - 1) (w - 1) a -> RangeR v w a)
-> m (RangeR (v - 1) (w - 1) a) -> m (RangeR v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool
-> m a -> RangeR (n - 1) (w - 1) a -> m (RangeR (v - 1) (w - 1) a)
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (RangeR v w a)
unfoldlMRangeWithBase m Bool
p m a
f RangeR (n - 1) (w - 1) a
xs
unfoldlMRangeMaybeWithBase :: m Bool -> m a -> RangeR n w a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase m Bool
p m a
f (RangeR (n - 1) (w - 1) a
xs :+ a
x) =
((RangeR (v - 1) (w - 1) a -> a -> RangeR v w a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ a
x) (RangeR (v - 1) (w - 1) a -> RangeR v w a)
-> Maybe (RangeR (v - 1) (w - 1) a) -> Maybe (RangeR v w a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (RangeR (v - 1) (w - 1) a) -> Maybe (RangeR v w a))
-> m (Maybe (RangeR (v - 1) (w - 1) a)) -> m (Maybe (RangeR v w a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Bool
-> m a
-> RangeR (n - 1) (w - 1) a
-> m (Maybe (RangeR (v - 1) (w - 1) a))
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase m Bool
p m a
f RangeR (n - 1) (w - 1) a
xs
unfoldlRange :: Unfoldl 0 v w =>
(s -> Bool) -> (s -> (s, a)) -> s -> RangeR v w a
unfoldlRange :: (s -> Bool) -> (s -> (s, a)) -> s -> RangeR v w a
unfoldlRange s -> Bool
p s -> (s, a)
f s
s = (s -> Bool) -> (s -> (s, a)) -> s -> RangeR 0 w a -> RangeR v w a
forall (n :: Nat) (v :: Nat) (w :: Nat) s a.
Unfoldl n v w =>
(s -> Bool) -> (s -> (s, a)) -> s -> RangeR n w a -> RangeR v w a
unfoldlRangeWithBase s -> Bool
p s -> (s, a)
f s
s RangeR 0 w a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
unfoldlRangeWithBase :: Unfoldl n v w =>
(s -> Bool) -> (s -> (s, a)) -> s -> RangeR n w a -> RangeR v w a
unfoldlRangeWithBase :: (s -> Bool) -> (s -> (s, a)) -> s -> RangeR n w a -> RangeR v w a
unfoldlRangeWithBase s -> Bool
p s -> (s, a)
f = ((s, RangeR v w a) -> RangeR v w a
forall a b. (a, b) -> b
snd ((s, RangeR v w a) -> RangeR v w a)
-> (RangeR n w a -> (s, RangeR v w a))
-> RangeR n w a
-> RangeR v w a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((RangeR n w a -> (s, RangeR v w a))
-> RangeR n w a -> RangeR v w a)
-> (s -> RangeR n w a -> (s, RangeR v w a))
-> s
-> RangeR n w a
-> RangeR v w a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s -> Bool)
-> (s -> (s, a)) -> s -> RangeR n w a -> (s, RangeR v w a)
forall (n :: Nat) (v :: Nat) (w :: Nat) s a.
Unfoldl n v w =>
(s -> Bool)
-> (s -> (s, a)) -> s -> RangeR n w a -> (s, RangeR v w a)
unfoldlRangeWithBaseWithS s -> Bool
p s -> (s, a)
f
unfoldlRangeWithBaseWithS :: Unfoldl n v w =>
(s -> Bool) -> (s -> (s, a)) -> s -> RangeR n w a -> (s, RangeR v w a)
unfoldlRangeWithBaseWithS :: (s -> Bool)
-> (s -> (s, a)) -> s -> RangeR n w a -> (s, RangeR v w a)
unfoldlRangeWithBaseWithS s -> Bool
p s -> (s, a)
f =
(RangeR n w a -> s -> (s, RangeR v w a))
-> s -> RangeR n w a -> (s, RangeR v w a)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((RangeR n w a -> s -> (s, RangeR v w a))
-> s -> RangeR n w a -> (s, RangeR v w a))
-> (RangeR n w a -> s -> (s, RangeR v w a))
-> s
-> RangeR n w a
-> (s, RangeR v w a)
forall a b. (a -> b) -> a -> b
$ StateR s (RangeR v w a) -> s -> (s, RangeR v w a)
forall s a. StateR s a -> s -> (s, a)
runStateR (StateR s (RangeR v w a) -> s -> (s, RangeR v w a))
-> (RangeR n w a -> StateR s (RangeR v w a))
-> RangeR n w a
-> s
-> (s, RangeR v w a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateR s Bool
-> StateR s a -> RangeR n w a -> StateR s (RangeR v w a)
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (RangeR v w a)
unfoldlMRangeWithBase ((s -> (s, Bool)) -> StateR s Bool
forall s a. (s -> (s, a)) -> StateR s a
StateR ((s -> (s, Bool)) -> StateR s Bool)
-> (s -> (s, Bool)) -> StateR s Bool
forall a b. (a -> b) -> a -> b
$ s -> s
forall a. a -> a
id (s -> s) -> (s -> Bool) -> s -> (s, Bool)
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& s -> Bool
p) ((s -> (s, a)) -> StateR s a
forall s a. (s -> (s, a)) -> StateR s a
StateR s -> (s, a)
f)
unfoldlMRange :: (Unfoldl 0 v w, Monad m) => m Bool -> m a -> m (RangeR v w a)
unfoldlMRange :: m Bool -> m a -> m (RangeR v w a)
unfoldlMRange m Bool
p m a
f = m Bool -> m a -> RangeR 0 w a -> m (RangeR v w a)
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (RangeR v w a)
unfoldlMRangeWithBase m Bool
p m a
f RangeR 0 w a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
unfoldlRangeMaybe ::
Unfoldl 0 v w => (s -> Maybe (s, a)) -> s -> Maybe (RangeR v w a)
unfoldlRangeMaybe :: (s -> Maybe (s, a)) -> s -> Maybe (RangeR v w a)
unfoldlRangeMaybe s -> Maybe (s, a)
f s
s = (s -> Maybe (s, a)) -> s -> RangeR 0 w a -> Maybe (RangeR v w a)
forall (n :: Nat) (v :: Nat) (w :: Nat) s a.
Unfoldl n v w =>
(s -> Maybe (s, a)) -> s -> RangeR n w a -> Maybe (RangeR v w a)
unfoldlRangeMaybeWithBase s -> Maybe (s, a)
f s
s RangeR 0 w a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
unfoldlRangeMaybeWithBase :: Unfoldl n v w =>
(s -> Maybe (s, a)) -> s -> RangeR n w a -> Maybe (RangeR v w a)
unfoldlRangeMaybeWithBase :: (s -> Maybe (s, a)) -> s -> RangeR n w a -> Maybe (RangeR v w a)
unfoldlRangeMaybeWithBase s -> Maybe (s, a)
f s
s RangeR n w a
xs =
(Maybe (s, a), Maybe (RangeR v w a)) -> Maybe (RangeR v w a)
forall a b. (a, b) -> b
snd ((Maybe (s, a), Maybe (RangeR v w a)) -> Maybe (RangeR v w a))
-> (Maybe (s, a), Maybe (RangeR v w a)) -> Maybe (RangeR v w a)
forall a b. (a -> b) -> a -> b
$ St s a Bool
-> St s a a -> RangeR n w a -> St s a (Maybe (RangeR v w a))
forall (n :: Nat) (v :: Nat) (w :: Nat) s a.
Unfoldl n v w =>
St s a Bool
-> St s a a -> RangeR n w a -> St s a (Maybe (RangeR v w a))
unfoldlRangeMaybeWithBaseGen (Maybe (s, a) -> Maybe (s, a)
forall a. a -> a
id (Maybe (s, a) -> Maybe (s, a))
-> (Maybe (s, a) -> Bool) -> St s a Bool
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Maybe (s, a) -> Bool
forall a. Maybe a -> Bool
isJust)
((Maybe (s, a), a) -> ((s, a) -> (Maybe (s, a), a)) -> St s a a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> (Maybe (s, a), a)
forall a. HasCallStack => String -> a
error String
"never occur") (s -> Maybe (s, a)
f (s -> Maybe (s, a)) -> (s, a) -> (Maybe (s, a), a)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
`first`)) RangeR n w a
xs (s -> Maybe (s, a)
f s
s)
type St s a r = Maybe (s, a) -> (Maybe (s, a), r)
unfoldlRangeMaybeWithBaseGen :: Unfoldl n v w =>
St s a Bool -> St s a a -> RangeR n w a -> St s a (Maybe (RangeR v w a))
unfoldlRangeMaybeWithBaseGen :: St s a Bool
-> St s a a -> RangeR n w a -> St s a (Maybe (RangeR v w a))
unfoldlRangeMaybeWithBaseGen St s a Bool
p St s a a
f =
StateR (Maybe (s, a)) (Maybe (RangeR v w a))
-> St s a (Maybe (RangeR v w a))
forall s a. StateR s a -> s -> (s, a)
runStateR (StateR (Maybe (s, a)) (Maybe (RangeR v w a))
-> St s a (Maybe (RangeR v w a)))
-> (RangeR n w a -> StateR (Maybe (s, a)) (Maybe (RangeR v w a)))
-> RangeR n w a
-> St s a (Maybe (RangeR v w a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateR (Maybe (s, a)) Bool
-> StateR (Maybe (s, a)) a
-> RangeR n w a
-> StateR (Maybe (s, a)) (Maybe (RangeR v w a))
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase (St s a Bool -> StateR (Maybe (s, a)) Bool
forall s a. (s -> (s, a)) -> StateR s a
StateR St s a Bool
p) (St s a a -> StateR (Maybe (s, a)) a
forall s a. (s -> (s, a)) -> StateR s a
StateR St s a a
f)
unfoldlMRangeMaybe :: (Unfoldl 0 v w, Monad m) =>
m Bool -> m a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybe :: m Bool -> m a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybe m Bool
p m a
f = m Bool -> m a -> RangeR 0 w a -> m (Maybe (RangeR v w a))
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldl n v w, Monad m) =>
m Bool -> m a -> RangeR n w a -> m (Maybe (RangeR v w a))
unfoldlMRangeMaybeWithBase m Bool
p m a
f RangeR 0 w a
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR
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)
instance ZipR n m 0 0 where zipWithMR :: (a -> b -> q c)
-> RangeR n m a
-> RangeR 0 0 b
-> q (RangeR (n - 0) (m - 0) a, RangeR 0 0 c)
zipWithMR a -> b -> q c
_ RangeR n m a
xs RangeR 0 0 b
NilR = (RangeR n m a, RangeR 0 0 c) -> q (RangeR n m a, RangeR 0 0 c)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RangeR n m a
xs, RangeR 0 0 c
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR)
instance {-# OVERLAPPABLE #-} (
1 <= n, 1 <= m, w <= n, LoosenRMin n m (n - w), LoosenRMax (n - w) (m - 1) m,
ZipR (n - 1) (m - 1) 0 (w - 1) ) => ZipR n m 0 w where
zipWithMR :: (a -> b -> q c)
-> RangeR n m a
-> RangeR 0 w b
-> q (RangeR (n - w) (m - 0) a, RangeR 0 w c)
zipWithMR a -> b -> q c
_ RangeR n m a
xs RangeR 0 w b
NilR = (RangeR (n - w) m a, RangeR 0 w c)
-> q (RangeR (n - w) m a, RangeR 0 w c)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (RangeR n m a -> RangeR (n - w) m a
forall (n :: Nat) (m :: Nat) (v :: Nat) a.
LoosenRMin n m v =>
RangeR n m a -> RangeR v m a
loosenRMin RangeR n m a
xs, RangeR 0 w c
forall (m :: Nat) a. (0 <= m) => RangeR 0 m a
NilR)
zipWithMR a -> b -> q c
(%) (RangeR (n - 1) (m - 1) a
xs :+ a
x) (RangeR 0 (w - 1) b
ys :++ b
y) =
a
x a -> b -> q c
% b
y q c
-> (c -> q (RangeR (n - w) m a, RangeR 0 w c))
-> q (RangeR (n - w) m a, RangeR 0 w c)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c
z -> (RangeR (n - w) (m - 1) a -> RangeR (n - w) m a
forall (n :: Nat) (m :: Nat) (w :: Nat) a.
LoosenRMax n m w =>
RangeR n m a -> RangeR n w a
loosenRMax (RangeR (n - w) (m - 1) a -> RangeR (n - w) m a)
-> (RangeR 0 (w - 1) c -> RangeR 0 w c)
-> (RangeR (n - w) (m - 1) a, RangeR 0 (w - 1) c)
-> (RangeR (n - w) m a, RangeR 0 w c)
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** (RangeR 0 (w - 1) c -> c -> RangeR 0 w c
forall (m :: Nat) a.
(1 <= m) =>
RangeR 0 (m - 1) a -> a -> RangeR 0 m a
:++ c
z)) ((RangeR (n - w) (m - 1) a, RangeR 0 (w - 1) c)
-> (RangeR (n - w) m a, RangeR 0 w c))
-> q (RangeR (n - w) (m - 1) a, RangeR 0 (w - 1) c)
-> q (RangeR (n - w) m a, RangeR 0 w c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> b -> q c)
-> RangeR (n - 1) (m - 1) a
-> RangeR 0 (w - 1) b
-> q (RangeR ((n - 1) - (w - 1)) ((m - 1) - 0) a,
RangeR 0 (w - 1) c)
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) (q :: * -> *) a
b c.
(ZipR n m v w, Monad q) =>
(a -> b -> q c)
-> RangeR n m a
-> RangeR v w b
-> q (RangeR (n - w) (m - v) a, RangeR v w c)
zipWithMR a -> b -> q c
(%) RangeR (n - 1) (m - 1) a
xs RangeR 0 (w - 1) b
ys
instance {-# OVERLAPPABLE #-} (
1 <= n, 1 <= v, v <= m, w <= n,
ZipR (n - 1) (m - 1) (v - 1) (w - 1) ) => ZipR n m v w where
zipWithMR :: (a -> b -> q c)
-> RangeR n m a
-> RangeR v w b
-> q (RangeR (n - w) (m - v) a, RangeR v w c)
zipWithMR a -> b -> q c
(%) (RangeR (n - 1) (m - 1) a
xs :+ a
x) (RangeR (v - 1) (w - 1) b
ys :+ b
y) =
a
x a -> b -> q c
% b
y q c
-> (c
-> q (RangeR ((n - 1) - (w - 1)) ((m - 1) - (v - 1)) a,
RangeR v w c))
-> q (RangeR ((n - 1) - (w - 1)) ((m - 1) - (v - 1)) a,
RangeR v w c)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \c
z -> ((RangeR (v - 1) (w - 1) c -> c -> RangeR v w c
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
RangeR (n - 1) (m - 1) a -> a -> RangeR n m a
:+ c
z) (RangeR (v - 1) (w - 1) c -> RangeR v w c)
-> (RangeR ((n - 1) - (w - 1)) ((m - 1) - (v - 1)) a,
RangeR (v - 1) (w - 1) c)
-> (RangeR ((n - 1) - (w - 1)) ((m - 1) - (v - 1)) a, RangeR v w c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
`second`) ((RangeR ((n - 1) - (w - 1)) ((m - 1) - (v - 1)) a,
RangeR (v - 1) (w - 1) c)
-> (RangeR ((n - 1) - (w - 1)) ((m - 1) - (v - 1)) a,
RangeR v w c))
-> q (RangeR ((n - 1) - (w - 1)) ((m - 1) - (v - 1)) a,
RangeR (v - 1) (w - 1) c)
-> q (RangeR ((n - 1) - (w - 1)) ((m - 1) - (v - 1)) a,
RangeR v w c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> b -> q c)
-> RangeR (n - 1) (m - 1) a
-> RangeR (v - 1) (w - 1) b
-> q (RangeR ((n - 1) - (w - 1)) ((m - 1) - (v - 1)) a,
RangeR (v - 1) (w - 1) c)
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) (q :: * -> *) a
b c.
(ZipR n m v w, Monad q) =>
(a -> b -> q c)
-> RangeR n m a
-> RangeR v w b
-> q (RangeR (n - w) (m - v) a, RangeR v w c)
zipWithMR a -> b -> q c
(%) RangeR (n - 1) (m - 1) a
xs RangeR (v - 1) (w - 1) b
ys
zipR :: ZipR n m v w => RangeR n m a -> RangeR v w b ->
(RangeR (n - w) (m - v) a, RangeR v w (a, b))
zipR :: RangeR n m a
-> RangeR v w b -> (RangeR (n - w) (m - v) a, RangeR v w (a, b))
zipR = (a -> b -> (a, b))
-> RangeR n m a
-> RangeR v w b
-> (RangeR (n - w) (m - v) a, RangeR v w (a, b))
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a b c.
ZipR n m v w =>
(a -> b -> c)
-> RangeR n m a
-> RangeR v w b
-> (RangeR (n - w) (m - v) a, RangeR v w c)
zipWithR (,)
zipWithR :: ZipR n m v w => (a -> b -> c) -> RangeR n m a -> RangeR v w b ->
(RangeR (n - w) (m - v) a, RangeR v w c)
zipWithR :: (a -> b -> c)
-> RangeR n m a
-> RangeR v w b
-> (RangeR (n - w) (m - v) a, RangeR v w c)
zipWithR a -> b -> c
op = (Identity (RangeR (n - w) (m - v) a, RangeR v w c)
-> (RangeR (n - w) (m - v) a, RangeR v w c)
forall a. Identity a -> a
runIdentity (Identity (RangeR (n - w) (m - v) a, RangeR v w c)
-> (RangeR (n - w) (m - v) a, RangeR v w c))
-> (RangeR v w b
-> Identity (RangeR (n - w) (m - v) a, RangeR v w c))
-> RangeR v w b
-> (RangeR (n - w) (m - v) a, RangeR v w c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((RangeR v w b
-> Identity (RangeR (n - w) (m - v) a, RangeR v w c))
-> RangeR v w b -> (RangeR (n - w) (m - v) a, RangeR v w c))
-> (RangeR n m a
-> RangeR v w b
-> Identity (RangeR (n - w) (m - v) a, RangeR v w c))
-> RangeR n m a
-> RangeR v w b
-> (RangeR (n - w) (m - v) a, RangeR v w c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b -> Identity c)
-> RangeR n m a
-> RangeR v w b
-> Identity (RangeR (n - w) (m - v) a, RangeR v w c)
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) (q :: * -> *) a
b c.
(ZipR n m v w, Monad q) =>
(a -> b -> q c)
-> RangeR n m a
-> RangeR v w b
-> q (RangeR (n - w) (m - v) a, RangeR v w c)
zipWithMR ((c -> Identity c
forall a. a -> Identity a
Identity (c -> Identity c) -> (b -> c) -> b -> Identity c
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((b -> c) -> b -> Identity c)
-> (a -> b -> c) -> a -> b -> Identity c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> c
op)