{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds, TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}
module Data.List.Range.Nat (
RangedNatL, natL, toIntL, fromIntL, splitAtL,
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 )
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 ()
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
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)
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
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 ()
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
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)
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