{-# 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)
unfoldr :: (0 <= n, Unfoldr 0 n n) => (s -> (a, s)) -> s -> LengthL n a
unfoldr :: (s -> (a, s)) -> s -> LengthL n a
unfoldr = RangeL 0 n a -> (s -> (a, s)) -> s -> LengthL n a
forall (n :: Nat) (m :: Nat) a s.
Unfoldr n m m =>
RangeL n m a -> (s -> (a, s)) -> s -> LengthL m a
unfoldrWithBase RangeL 0 n a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL
unfoldrWithBase ::
Unfoldr n m m => RangeL n m a -> (s -> (a, s)) -> s -> LengthL m a
unfoldrWithBase :: RangeL n m a -> (s -> (a, s)) -> s -> LengthL m a
unfoldrWithBase RangeL n m a
xs = ((LengthL m a, s) -> LengthL m a
forall a b. (a, b) -> a
fst ((LengthL m a, s) -> LengthL m a)
-> (s -> (LengthL m a, s)) -> s -> LengthL m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((s -> (LengthL m a, s)) -> s -> LengthL m a)
-> ((s -> (a, s)) -> s -> (LengthL m a, s))
-> (s -> (a, s))
-> s
-> LengthL m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateL s (LengthL m a) -> s -> (LengthL m a, s)
forall s a. StateL s a -> s -> (a, s)
runStateL (StateL s (LengthL m a) -> s -> (LengthL m a, s))
-> ((s -> (a, s)) -> StateL s (LengthL m a))
-> (s -> (a, s))
-> s
-> (LengthL m a, s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RangeL n m a -> StateL s a -> StateL s (LengthL m a)
forall (m :: * -> *) (n :: Nat) (w :: Nat) a.
(Monad m, Unfoldr n w w) =>
RangeL n w a -> m a -> m (LengthL w a)
unfoldrMWithBase RangeL n m a
xs (StateL s a -> StateL s (LengthL m a))
-> ((s -> (a, s)) -> StateL s a)
-> (s -> (a, s))
-> StateL s (LengthL m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s -> (a, s)) -> StateL s a
forall s a. (s -> (a, s)) -> StateL s a
StateL
unfoldrM :: (Monad m, 0 <= n, Unfoldr 0 n n) => m a -> m (LengthL n a)
unfoldrM :: m a -> m (LengthL n a)
unfoldrM = RangeL 0 n a -> m a -> m (LengthL n a)
forall (m :: * -> *) (n :: Nat) (w :: Nat) a.
(Monad m, Unfoldr n w w) =>
RangeL n w a -> m a -> m (LengthL w a)
unfoldrMWithBase RangeL 0 n a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL
unfoldrMWithBase ::
(Monad m, Unfoldr n w w) => RangeL n w a -> m a -> m (LengthL w a)
unfoldrMWithBase :: RangeL n w a -> m a -> m (LengthL w a)
unfoldrMWithBase = (RangeL n w a -> m Bool -> m a -> m (LengthL w a)
forall (n :: Nat) (v :: Nat) (w :: Nat) (m :: * -> *) a.
(Unfoldr n v w, Monad m) =>
RangeL n w a -> m Bool -> m a -> m (RangeL v w a)
`unfoldrMRangeWithBase` m Bool
forall a. HasCallStack => a
undefined)
class ListToLengthL n where
splitL :: [a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
instance ListToLengthL 1 where
splitL :: [a] -> Either (RangeL 0 (1 - 1) a) (LengthL 1 a, [a])
splitL = \case [] -> RangeL 0 0 a -> Either (RangeL 0 0 a) (LengthL 1 a, [a])
forall a b. a -> Either a b
Left RangeL 0 0 a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL; a
x : [a]
xs -> (LengthL 1 a, [a]) -> Either (RangeL 0 0 a) (LengthL 1 a, [a])
forall a b. b -> Either a b
Right (a
x a -> RangeL (1 - 1) (1 - 1) a -> LengthL 1 a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:. RangeL (1 - 1) (1 - 1) a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL, [a]
xs)
instance {-# OVERLAPPABLE #-}
(1 <= n, 1 <= (n - 1), 0 <= (n - 1), ListToLengthL (n - 1)) => ListToLengthL n where
splitL :: [a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
splitL = \case
[] -> RangeL 0 (n - 1) a
-> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
forall a b. a -> Either a b
Left RangeL 0 (n - 1) a
forall (m :: Nat) a. (0 <= m) => RangeL 0 m a
NilL
a
x : [a]
xs -> (a
x a -> RangeL 0 ((n - 1) - 1) a -> RangeL 0 (n - 1) a
forall (m :: Nat) a.
(1 <= m) =>
a -> RangeL 0 (m - 1) a -> RangeL 0 m a
:..) (RangeL 0 ((n - 1) - 1) a -> RangeL 0 (n - 1) a)
-> ((RangeL (n - 1) (n - 1) a, [a]) -> (LengthL n a, [a]))
-> Either
(RangeL 0 ((n - 1) - 1) a) (RangeL (n - 1) (n - 1) a, [a])
-> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
forall (a :: * -> * -> *) b c b' c'.
ArrowChoice a =>
a b c -> a b' c' -> a (Either b b') (Either c c')
+++ ((a
x a -> RangeL (n - 1) (n - 1) a -> LengthL n a
forall (n :: Nat) (m :: Nat) a.
(1 <= n, 1 <= m) =>
a -> RangeL (n - 1) (m - 1) a -> RangeL n m a
:.) (RangeL (n - 1) (n - 1) a -> LengthL n a)
-> (RangeL (n - 1) (n - 1) a, [a]) -> (LengthL n a, [a])
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
`first`) (Either (RangeL 0 ((n - 1) - 1) a) (RangeL (n - 1) (n - 1) a, [a])
-> Either (RangeL 0 (n - 1) a) (LengthL n a, [a]))
-> Either
(RangeL 0 ((n - 1) - 1) a) (RangeL (n - 1) (n - 1) a, [a])
-> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
forall a b. (a -> b) -> a -> b
$ [a]
-> Either
(RangeL 0 ((n - 1) - 1) a) (RangeL (n - 1) (n - 1) a, [a])
forall (n :: Nat) a.
ListToLengthL n =>
[a] -> Either (RangeL 0 (n - 1) a) (LengthL n a, [a])
splitL [a]
xs