{-# 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 :: RangedNatL n n
natL = () -> RangedNatL n n
forall (n :: Nat) a. Unfoldr 0 n n => a -> LengthL n a
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 :: RangedNatL n m -> Int
toIntL = RangedNatL n m -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
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 :: Int -> Maybe (RangedNatL n m)
fromIntL = (Int -> Maybe ((), Int)) -> Int -> Maybe (RangedNatL n m)
forall (v :: Nat) (w :: Nat) s a.
Unfoldr 0 v w =>
(s -> Maybe (a, s)) -> s -> Maybe (RangeL v w a)
unfoldrRangeMaybe \Int
s -> Maybe ((), Int) -> Maybe ((), Int) -> Bool -> Maybe ((), Int)
forall a. a -> a -> Bool -> a
bool Maybe ((), Int)
forall a. Maybe a
Nothing (((), Int) -> Maybe ((), Int)
forall a. a -> Maybe a
Just ((), Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) (Int
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
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 :: RangedNatL n m
-> RangeL v w a -> (RangeL n m a, RangeL (v - m) (w - n) a)
splitAtL = (() -> a -> a)
-> RangedNatL n m
-> RangeL v w a
-> (RangeL n m a, RangeL (v - m) (w - n) a)
forall (n :: Nat) (m :: Nat) (v :: Nat) (w :: Nat) a b c.
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 ((() -> a -> a)
 -> RangedNatL n m
 -> RangeL v w a
 -> (RangeL n m a, RangeL (v - m) (w - n) a))
-> (() -> a -> a)
-> RangedNatL n m
-> RangeL v w a
-> (RangeL n m a, RangeL (v - m) (w - n) a)
forall a b. (a -> b) -> a -> b
$ (a -> () -> a) -> () -> a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> () -> a
forall a b. a -> b -> a
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 :: RangedNatR n n
natR = () -> RangedNatR n n
forall (n :: Nat) a. Unfoldl 0 n n => a -> LengthR n a
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 :: RangedNatR n m -> Int
toIntR = RangedNatR n m -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
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 :: Int -> Maybe (RangedNatR n m)
fromIntR = (Int -> Maybe (Int, ())) -> Int -> Maybe (RangedNatR n m)
forall (v :: Nat) (w :: Nat) s a.
Unfoldl 0 v w =>
(s -> Maybe (s, a)) -> s -> Maybe (RangeR v w a)
unfoldlRangeMaybe \Int
s -> Maybe (Int, ()) -> Maybe (Int, ()) -> Bool -> Maybe (Int, ())
forall a. a -> a -> Bool -> a
bool Maybe (Int, ())
forall a. Maybe a
Nothing ((Int, ()) -> Maybe (Int, ())
forall a. a -> Maybe a
Just (Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1, ())) (Int
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
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 :: RangeR n m a
-> RangedNatR v w -> (RangeR (n - w) (m - v) a, RangeR v w a)
splitAtR = (a -> () -> a)
-> RangeR n m a
-> RangedNatR v w
-> (RangeR (n - w) (m - v) a, RangeR v w a)
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 a -> () -> a
forall a b. a -> b -> a
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)

-}