{-# LANGUAGE CPP, DataKinds, GADTs, KindSignatures, MultiParamTypeClasses #-}
{-# LANGUAGE NoImplicitPrelude, NoMonomorphismRestriction, NoStarIsType   #-}
{-# LANGUAGE PatternSynonyms, PolyKinds, RankNTypes, TypeApplications     #-}
{-# LANGUAGE TypeInType, TypeOperators, ViewPatterns                      #-}
-- | This module exports provides the functionality to make length-parametrized types
--   from existing 'CFreeMonoid' sequential types,
--   parametrised with peano numeral 'PN.Nat' kind.
--
--   Most of the complexity of operations on @'Sized' f n a@ are the same as
--   original operations on @f@. For example, '!!' is O(1) for
--   @Sized Vector n a@ but O(i) for @Sized [] n a@.
--
--  This module also provides powerful view types and pattern synonyms to
--  inspect the sized sequence. See <#ViewsAndPatterns Views and Patterns> for more detail.
module Data.Sized.Peano {-# DEPRECATED "Removed in future release" #-}
  ( -- * Main Data-types
    Sized(), SomeSized, pattern SomeSized, Ordinal,
    DomC(),
    -- * Accessors
    -- ** Length information
    length, sLength, null,
    -- ** Indexing
    (!!), (%!!), index, sIndex, head, last,
    uncons, uncons', Uncons, pattern Uncons,
    unsnoc, unsnoc', Unsnoc, pattern Unsnoc,
    -- ** Slicing
    tail, init, take, takeAtMost, drop, splitAt, splitAtMost,
    -- * Construction
    -- ** Initialisation
    empty, singleton, toSomeSized, replicate, replicate', generate, generate',
    -- ** Concatenation
    cons, (<|), snoc, (|>), append, (++), concat,
    -- ** Zips
    zip, zipSame, zipWith, zipWithSame, unzip, unzipWith,
    -- * Transformation
    map, reverse, intersperse, nub, sort, sortBy, insert, insertBy,
    -- * Conversion
    -- ** List
    toList, fromList, fromList', unsafeFromList, unsafeFromList',
    fromListWithDefault, fromListWithDefault',
    -- ** Base container
    unsized,
    toSized, toSized', unsafeToSized, unsafeToSized',
    toSizedWithDefault, toSizedWithDefault',
    -- * Querying
    -- ** Partitioning
    Partitioned(), pattern Partitioned,
    takeWhile, dropWhile, span, break, partition,
    -- ** Searching
    elem, notElem, find, findIndex, sFindIndex,
    findIndices, sFindIndices,
    elemIndex, sElemIndex, sUnsafeElemIndex, elemIndices, sElemIndices,
    -- * Views and Patterns
    -- $ViewsAndPatterns

    -- ** Views
    -- $views

    -- ** Patterns
    -- $patterns

    -- ** Definitions
    viewCons, ConsView,
    pattern (:-), pattern NilCV,
    viewSnoc, SnocView,
    pattern (:-::), pattern NilSV,

    pattern Nil, pattern (:<), pattern NilL , pattern (:>), pattern NilR,
  ) where
import           Data.Sized (DomC)
import qualified Data.Sized as S

import           Control.Subcategory
import           Data.Kind                    (Type)
import           Data.Singletons.Prelude      (POrd ((<=)), SingI)
import           Data.Singletons.Prelude.Enum (PEnum (..))
import           Data.Type.Natural            (Min, Nat (..), One, SNat, Two,
                                               type (*), type (+), type (-))
import           Data.Type.Natural.Class      (type (-.), type (<))
import qualified Data.Type.Ordinal            as O
import           Prelude                      (Bool (..), Eq, Int, Maybe,
                                               Monoid, Ord, Ordering)

type Ordinal = (O.Ordinal :: Nat -> Type)

-- | @Sized@ wraps a sequential type 'f' and makes length-parametrized version.
--
-- Here, 'f' must satisfy @'CFreeMonoid' f@ and @Dom f a@.
--
-- Since 0.2.0.0
type Sized = (S.Sized :: (Type -> Type) -> Nat -> Type -> Type)


-- | 'Sized' sequence with the length is existentially quantified.
--   This type is used mostly when the return type's length cannot
--   be statically determined beforehand.
--
-- @SomeSized' sn xs :: SomeSized' f a@ stands for the 'Sized' sequence
-- @xs@ of element type @a@ and length @sn@.
--
-- Since 0.7.0.0
type SomeSized f a = S.SomeSized' f Nat a

pattern SomeSized
  :: forall (f :: Type -> Type) a. ()
  => forall (n :: Nat). SNat n
  -> Sized f n a -> SomeSized f a
{-# COMPLETE SomeSized #-}
pattern $bSomeSized :: SNat n -> Sized f n a -> SomeSized f a
$mSomeSized :: forall r (f :: Type -> Type) a.
SomeSized f a
-> (forall (n :: Nat). SNat n -> Sized f n a -> r)
-> (Void# -> r)
-> r
SomeSized n s = S.SomeSized'  n s

-- | Returns the length of wrapped containers.
--   If you use @unsafeFromList@ or similar unsafe functions,
--   this function may return different value from type-parameterized length.
--
-- Since 0.8.0.0 (type changed)
{-# INLINE length #-}
length :: (Dom f a, SingI n) => Sized f n a -> Int
length :: Sized f n a -> Int
length = forall nat (f :: Type -> Type) (n :: nat) a.
(IsPeano nat, Dom f a, SingI n) =>
Sized f n a -> Int
forall (f :: Type -> Type) (n :: Nat) a.
(IsPeano Nat, Dom f a, SingI n) =>
Sized f n a -> Int
S.length @Nat

-- | @Sing@ version of 'length'.
--
-- Since 0.8.0.0 (type changed)
{-# INLINE sLength #-}
sLength :: (Dom f a, SingI n) => Sized f n a -> SNat n
sLength :: Sized f n a -> SNat n
sLength = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, Dom f a, SingI n) =>
Sized f n a -> Sing n
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, Dom f a, SingI n) =>
Sized f n a -> Sing n
S.sLength @Nat

-- | Test if the sequence is empty or not.
--
-- Since 0.7.0.0
{-# INLINE null #-}
null :: (Dom f a, CFoldable f) => Sized f n a -> Bool
null :: Sized f n a -> Bool
null = forall nat (f :: Type -> Type) (n :: nat) a.
(CFoldable f, Dom f a) =>
Sized f n a -> Bool
forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
Sized f n a -> Bool
S.null @Nat

--------------------------------------------------------------------------------
--- Indexing
--------------------------------------------------------------------------------

-- | (Unsafe) indexing with @Int@s.
--   If you want to check boundary statically, use '%!!' or 'sIndex'.
--
-- Since 0.7.0.0
{-# INLINE (!!) #-}
(!!) :: (Dom f a, CFoldable f, (One <= m) ~ 'True) => Sized f m a -> Int -> a
!! :: Sized f m a -> Int -> a
(!!) = forall nat (f :: Type -> Type) (m :: nat) a.
(CFoldable f, Dom f a, (One nat <= m) ~ 'True) =>
Sized f m a -> Int -> a
forall (f :: Type -> Type) (m :: Nat) a.
(CFoldable f, Dom f a, (One Nat <= m) ~ 'True) =>
Sized f m a -> Int -> a
(S.!!) @Nat

-- | Safe indexing with 'Ordinal's.
--
-- Since 0.7.0.0
{-# INLINE (%!!) #-}
(%!!) :: (Dom f c, CFoldable f) => Sized f n c -> Ordinal n -> c
%!! :: Sized f n c -> Ordinal n -> c
(%!!) = forall nat (f :: Type -> Type) (n :: nat) c.
(HasOrdinal nat, CFoldable f, Dom f c) =>
Sized f n c -> Ordinal n -> c
forall (f :: Type -> Type) (n :: Nat) c.
(HasOrdinal Nat, CFoldable f, Dom f c) =>
Sized f n c -> Ordinal n -> c
(S.%!!) @Nat

-- | Flipped version of '!!'.
--
-- Since 0.7.0.0
{-# INLINE index #-}
index
  :: (Dom f a, CFoldable f, (One <= m) ~ 'True)
  => Int -> Sized f m a -> a
index :: Int -> Sized f m a -> a
index = forall nat (f :: Type -> Type) (m :: nat) a.
(CFoldable f, Dom f a, (One nat <= m) ~ 'True) =>
Int -> Sized f m a -> a
forall (f :: Type -> Type) (m :: Nat) a.
(CFoldable f, Dom f a, (One Nat <= m) ~ 'True) =>
Int -> Sized f m a -> a
S.index @Nat

-- | Flipped version of '%!!'.
--
-- Since 0.7.0.0
{-# INLINE sIndex #-}
sIndex :: (Dom f c, CFoldable f) => Ordinal n -> Sized f n c -> c
sIndex :: Ordinal n -> Sized f n c -> c
sIndex = forall nat (f :: Type -> Type) (n :: nat) c.
(HasOrdinal nat, CFoldable f, Dom f c) =>
Ordinal n -> Sized f n c -> c
forall (f :: Type -> Type) (n :: Nat) c.
(HasOrdinal Nat, CFoldable f, Dom f c) =>
Ordinal n -> Sized f n c -> c
S.sIndex @Nat

-- | Take the first element of non-empty sequence.
--   If you want to make case-analysis for general sequence,
--   see  <#ViewsAndPatterns Views and Patterns> section.
--
-- Since 0.7.0.0
{-# INLINE head #-}
head :: (Dom f a, CFoldable f, ('Z < n) ~ 'True) => Sized f n a -> a
head :: Sized f n a -> a
head = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFoldable f, Dom f a, (Zero nat < n) ~ 'True) =>
Sized f n a -> a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, CFoldable f, Dom f a, (Zero Nat < n) ~ 'True) =>
Sized f n a -> a
S.head @Nat

-- | Take the last element of non-empty sequence.
--   If you want to make case-analysis for general sequence,
--   see  <#ViewsAndPatterns Views and Patterns> section.
--
-- Since 0.7.0.0
{-# INLINE last #-}
last :: (Dom f a, CFoldable f, ('Z < n) ~ 'True) => Sized f n a -> a
last :: Sized f n a -> a
last = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, (Zero nat < n) ~ 'True, CFoldable f, Dom f a) =>
Sized f n a -> a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, (Zero Nat < n) ~ 'True, CFoldable f, Dom f a) =>
Sized f n a -> a
S.last @Nat

-- | Take the 'head' and 'tail' of non-empty sequence.
--   If you want to make case-analysis for general sequence,
--   see  <#ViewsAndPatterns Views and Patterns> section.
--
-- Since 0.7.0.0
{-# INLINE uncons #-}
uncons
  :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True)
  => Sized f n a -> Uncons f n a
uncons :: Sized f n a -> Uncons f n a
uncons = forall nat (f :: Type -> Type) (n :: nat) a.
(PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a,
 (Zero nat < n) ~ 'True) =>
Sized f n a -> Uncons f n a
forall (f :: Type -> Type) (n :: Nat) a.
(PeanoOrder Nat, SingI n, CFreeMonoid f, Dom f a,
 (Zero Nat < n) ~ 'True) =>
Sized f n a -> Uncons f n a
S.uncons @Nat

-- | 'uncons' with explicit specified length @n@
--
--   Since 0.7.0.0
{-# INLINE uncons' #-}
uncons'
  :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True)
  => Sized f n a
  -> Uncons f n a
uncons' :: Sized f n a -> Uncons f n a
uncons' = forall nat (f :: Type -> Type) (n :: nat) a.
(PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a,
 (Zero nat < n) ~ 'True) =>
Sized f n a -> Uncons f n a
forall (f :: Type -> Type) (n :: Nat) a.
(PeanoOrder Nat, SingI n, CFreeMonoid f, Dom f a,
 (Zero Nat < n) ~ 'True) =>
Sized f n a -> Uncons f n a
S.uncons @Nat

-- | Take the 'init' and 'last' of non-empty sequence.
--   If you want to make case-analysis for general sequence,
--   see  <#ViewsAndPatterns Views and Patterns> section.
--
-- Since 0.7.0.0
{-# INLINE unsnoc #-}
unsnoc
  :: (Dom f a, SingI n, CFreeMonoid f, ('Z < n) ~ 'True)
  => Sized f n a -> Unsnoc f n a
unsnoc :: Sized f n a -> Unsnoc f n a
unsnoc = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a,
 (Zero nat < n) ~ 'True) =>
Sized f n a -> Unsnoc f n a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, SingI n, CFreeMonoid f, Dom f a,
 (Zero Nat < n) ~ 'True) =>
Sized f n a -> Unsnoc f n a
S.unsnoc @Nat

-- | 'unsnoc'' with explicit specified length @n@
--
--   Since 0.7.0.0
{-# INLINE unsnoc' #-}
unsnoc' :: (Dom f a, SingI n, CFreeMonoid f) => proxy n -> Sized f ('S n) a -> Unsnoc f ('S n) a
unsnoc' :: proxy n -> Sized f ('S n) a -> Unsnoc f ('S n) a
unsnoc' = forall nat (f :: Type -> Type) (n :: nat) a (proxy :: nat -> Type).
(HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) =>
proxy n -> Sized f (Succ n) a -> Unsnoc f (Succ n) a
forall (f :: Type -> Type) (n :: Nat) a (proxy :: Nat -> Type).
(HasOrdinal Nat, SingI n, CFreeMonoid f, Dom f a) =>
proxy n -> Sized f (Succ n) a -> Unsnoc f (Succ n) a
S.unsnoc' @Nat

type Uncons f (n :: Nat) a = S.Uncons f n a
pattern Uncons
  :: forall (f :: Type -> Type) (n :: Nat) a. ()
  => forall (n1 :: Nat). (n ~ Succ n1, SingI n1)
  => a -> Sized f n1 a -> Uncons f n a
pattern $bUncons :: a -> Sized f n1 a -> Uncons f n a
$mUncons :: forall r (f :: Type -> Type) (n :: Nat) a.
Uncons f n a
-> (forall (n1 :: Nat).
    (n ~ Succ n1, SingI n1) =>
    a -> Sized f n1 a -> r)
-> (Void# -> r)
-> r
Uncons a as = S.Uncons a as

type Unsnoc f (n :: Nat) a = S.Unsnoc f n a

pattern Unsnoc
  :: forall (f :: Type -> Type) (n :: Nat) a. ()
  => forall (n1 :: Nat). (n ~ Succ n1)
  => Sized f n1 a -> a -> Unsnoc f n a
pattern $bUnsnoc :: Sized f n1 a -> a -> Unsnoc f n a
$mUnsnoc :: forall r (f :: Type -> Type) (n :: Nat) a.
Unsnoc f n a
-> (forall (n1 :: Nat). (n ~ Succ n1) => Sized f n1 a -> a -> r)
-> (Void# -> r)
-> r
Unsnoc xs x = S.Unsnoc xs x

-- | Take the tail of non-empty sequence.
--   If you want to make case-analysis for general sequence,
--   see  <#ViewsAndPatterns Views and Patterns> section.
--
-- Since 0.7.0.0
{-# INLINE tail #-}
tail :: (Dom f a, CFreeMonoid f) => Sized f (One + n) a -> Sized f n a
tail :: Sized f (One + n) a -> Sized f n a
tail = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
Sized f (One nat + n) a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, CFreeMonoid f, Dom f a) =>
Sized f (One Nat + n) a -> Sized f n a
S.tail @Nat


-- | Take the initial segment of non-empty sequence.
--   If you want to make case-analysis for general sequence,
--   see  <#ViewsAndPatterns Views and Patterns> section.
--
-- Since 0.7.0.0
{-# INLINE init #-}
init :: (Dom f a, CFreeMonoid f) => Sized f (n + One) a -> Sized f n a
init :: Sized f (n + One) a -> Sized f n a
init = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
Sized f (n + One nat) a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, CFreeMonoid f, Dom f a) =>
Sized f (n + One Nat) a -> Sized f n a
S.init @Nat

-- | @take k xs@ takes first @k@ element of @xs@ where
-- the length of @xs@ should be larger than @k@.
--
-- Since 0.7.0.0
{-# INLINE take #-}
take
  :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True)
  => SNat n -> Sized f m a -> Sized f n a
take :: SNat n -> Sized f m a -> Sized f n a
take = forall nat (n :: nat) (f :: Type -> Type) (m :: nat) a.
(CFreeMonoid f, Dom f a, (n <= m) ~ 'True, HasOrdinal nat) =>
Sing n -> Sized f m a -> Sized f n a
forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(CFreeMonoid f, Dom f a, (n <= m) ~ 'True, HasOrdinal Nat) =>
Sing n -> Sized f m a -> Sized f n a
S.take @Nat

-- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@.
--
-- Since 0.7.0.0
{-# INLINE takeAtMost #-}
takeAtMost
  :: (Dom f a, CFreeMonoid f)
  => SNat n -> Sized f m a -> Sized f (Min n m) a
takeAtMost :: SNat n -> Sized f m a -> Sized f (Min n m) a
takeAtMost = forall nat (n :: nat) (f :: Type -> Type) (m :: nat) a.
(CFreeMonoid f, Dom f a, HasOrdinal nat) =>
Sing n -> Sized f m a -> Sized f (Min n m) a
forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(CFreeMonoid f, Dom f a, HasOrdinal Nat) =>
Sing n -> Sized f m a -> Sized f (Min n m) a
S.takeAtMost @Nat

-- | @drop k xs@ drops first @k@ element of @xs@ and returns
-- the rest of sequence, where the length of @xs@ should be larger than @k@.
--
-- Since 0.7.0.0
{-# INLINE drop #-}
drop
  :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True)
  => SNat n -> Sized f m a -> Sized f (m - n) a
drop :: SNat n -> Sized f m a -> Sized f (m - n) a
drop = forall nat (n :: nat) (f :: Type -> Type) (m :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a, (n <= m) ~ 'True) =>
Sing n -> Sized f m a -> Sized f (m - n) a
forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(HasOrdinal Nat, CFreeMonoid f, Dom f a, (n <= m) ~ 'True) =>
Sing n -> Sized f m a -> Sized f (m - n) a
S.drop @Nat

-- | @splitAt k xs@ split @xs@ at @k@, where
-- the length of @xs@ should be less than or equal to @k@.
--
-- Since 0.7.0.0
{-# INLINE splitAt #-}
splitAt
  :: (Dom f a, CFreeMonoid f, (n <= m) ~ 'True)
  => SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a)
splitAt :: SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a)
splitAt = forall nat (n :: nat) (f :: Type -> Type) (m :: nat) a.
(CFreeMonoid f, Dom f a, (n <= m) ~ 'True, HasOrdinal nat) =>
Sing n -> Sized f m a -> (Sized f n a, Sized f (m -. n) a)
forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(CFreeMonoid f, Dom f a, (n <= m) ~ 'True, HasOrdinal Nat) =>
Sing n -> Sized f m a -> (Sized f n a, Sized f (m -. n) a)
S.splitAt @Nat

-- | @splitAtMost k xs@ split @xs@ at @k@.
--   If @k@ exceeds the length of @xs@, then the second result value become empty.
--
-- Since 0.7.0.0
{-# INLINE splitAtMost #-}
splitAtMost
  :: (Dom f a, CFreeMonoid f)
  => SNat n -> Sized f m a
  -> (Sized f (Min n m) a, Sized f (m -. n) a)
splitAtMost :: SNat n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a)
splitAtMost = forall nat (n :: nat) (f :: Type -> Type) (m :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
Sing n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a)
forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(HasOrdinal Nat, CFreeMonoid f, Dom f a) =>
Sing n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a)
S.splitAtMost @Nat

--------------------------------------------------------------------------------
-- Construction
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
--- Initialisation
--------------------------------------------------------------------------------

-- | Empty sequence.
--
-- Since 0.7.0.0 (type changed)
{-# INLINE empty #-}
empty :: (Dom f a, Monoid (f a)) => Sized f 'Z a
empty :: Sized f 'Z a
empty = forall nat (f :: Type -> Type) a.
(Monoid (f a), HasOrdinal nat, Dom f a) =>
Sized f (Zero nat) a
forall (f :: Type -> Type) a.
(Monoid (f a), HasOrdinal Nat, Dom f a) =>
Sized f (Zero Nat) a
S.empty @Nat

-- | Sequence with one element.
--
-- Since 0.7.0.0
{-# INLINE singleton #-}
singleton :: (Dom f a, CFreeMonoid f) => a -> Sized f One a
singleton :: a -> Sized f One a
singleton = forall nat (f :: Type -> Type) a.
(CPointed f, Dom f a) =>
a -> Sized f (One nat) a
forall (f :: Type -> Type) a.
(CPointed f, Dom f a) =>
a -> Sized f (One Nat) a
S.singleton @Nat

-- | Consruct the 'Sized' sequence from base type, but
--   the length parameter is dynamically determined and
--   existentially quantified; see also 'SomeSized''.
--
-- Since 0.7.0.0
{-# INLINE toSomeSized #-}
toSomeSized :: (Dom f a, CFoldable f) => f a -> SomeSized f a
toSomeSized :: f a -> SomeSized f a
toSomeSized = forall nat (f :: Type -> Type) a.
(HasOrdinal nat, Dom f a, CFoldable f) =>
f a -> SomeSized' f nat a
forall (f :: Type -> Type) a.
(HasOrdinal Nat, Dom f a, CFoldable f) =>
f a -> SomeSized' f Nat a
S.toSomeSized @Nat

-- | Replicates the same value.
--
-- Since 0.7.0.0
{-# INLINE replicate #-}
replicate :: (Dom f a, CFreeMonoid f) => SNat n -> a -> Sized f n a
replicate :: SNat n -> a -> Sized f n a
replicate = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
Sing n -> a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, CFreeMonoid f, Dom f a) =>
Sing n -> a -> Sized f n a
S.replicate @Nat

-- | 'replicate' with the length inferred.
--
-- Since 0.7.0.0
{-# INLINE replicate' #-}
replicate' :: (Dom f a, CFreeMonoid f, SingI n) => a -> Sized f n a
replicate' :: a -> Sized f n a
replicate' = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) =>
a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, SingI n, CFreeMonoid f, Dom f a) =>
a -> Sized f n a
S.replicate' @Nat

-- | Construct a sequence of the given length by applying the function to each index.
--
-- Since 0.7.0.0
{-# INLINE generate #-}
generate :: (Dom f a, CFreeMonoid f) => SNat n -> (Ordinal n -> a) -> Sized f n a
generate :: SNat n -> (Ordinal n -> a) -> Sized f n a
generate = forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a, HasOrdinal nat) =>
Sing n -> (Ordinal n -> a) -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a, HasOrdinal Nat) =>
Sing n -> (Ordinal n -> a) -> Sized f n a
S.generate @Nat

-- | 'generate' with length inferred.
--
--   Since 0.8.0.0
{-# INLINE generate' #-}
generate' :: forall f n a.
  (SingI n, Dom f a, CFreeMonoid f)
  => (Ordinal n -> a) -> Sized f n a
generate' :: (Ordinal n -> a) -> Sized f n a
generate' = forall nat (f :: Type -> Type) (n :: nat) a.
(SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat) =>
(Ordinal n -> a) -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(SingI n, CFreeMonoid f, Dom f a, HasOrdinal Nat) =>
(Ordinal n -> a) -> Sized f n a
S.generate' @Nat

--------------------------------------------------------------------------------
--- Concatenation
--------------------------------------------------------------------------------

-- | Append an element to the head of sequence.
--
-- Since 0.7.0.0
{-# INLINE cons #-}
cons :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f ('S n) a
cons :: a -> Sized f n a -> Sized f ('S n) a
cons = forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (One nat + n) a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (One Nat + n) a
S.cons @Nat

-- | Append an element to the tail of sequence.
--
-- Since 0.7.0.0
{-# INLINE snoc #-}
snoc :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + One) a
snoc :: Sized f n a -> a -> Sized f (n + One) a
snoc = forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + One nat) a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + One Nat) a
S.snoc @Nat

-- | Infix version of 'snoc'.
--
-- Since 0.7.0.0
{-# INLINE (<|) #-}
(<|) :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f ('S n) a
<| :: a -> Sized f n a -> Sized f ('S n) a
(<|) = forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (One nat + n) a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (One Nat + n) a
(S.<|) @Nat

-- | Append an element to the tail of sequence.
--
-- Since 0.7.0.0
{-# INLINE (|>) #-}
(|>) :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + One) a
|> :: Sized f n a -> a -> Sized f (n + One) a
(|>) = forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + One nat) a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + One Nat) a
(S.|>) @Nat

-- | Infix version of 'append'.
--
-- Since 0.7.0.0
{-# INLINE (++) #-}
(++) :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a
++ :: Sized f n a -> Sized f m a -> Sized f (n + m) a
(++) = forall nat (f :: Type -> Type) (n :: nat) (m :: nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> Sized f m a -> Sized f (n + m) a
forall (f :: Type -> Type) (n :: Nat) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> Sized f m a -> Sized f (n + m) a
(S.++) @Nat

-- | Append two lists.
--
-- Since 0.7.0.0
{-# INLINE append #-}
append :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a
append :: Sized f n a -> Sized f m a -> Sized f (n + m) a
append = forall nat (f :: Type -> Type) (n :: nat) (m :: nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> Sized f m a -> Sized f (n + m) a
forall (f :: Type -> Type) (n :: Nat) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> Sized f m a -> Sized f (n + m) a
S.append @Nat

-- | Concatenates multiple sequences into one.
--
-- Since 0.7.0.0
{-# INLINE concat #-}
concat
  :: (Dom f a, Dom f' (f a), Dom f' (Sized f n a),
      CFreeMonoid f, CFunctor f', CFoldable f'
    ) => Sized f' m (Sized f n a) -> Sized f (m * n) a
concat :: Sized f' m (Sized f n a) -> Sized f (m * n) a
concat = forall nat (f' :: Type -> Type) (m :: nat) (f :: Type -> Type)
       (n :: nat) a.
(CFreeMonoid f, CFunctor f', CFoldable f', Dom f a, Dom f' (f a),
 Dom f' (Sized f n a)) =>
Sized f' m (Sized f n a) -> Sized f (m * n) a
forall (f' :: Type -> Type) (m :: Nat) (f :: Type -> Type)
       (n :: Nat) a.
(CFreeMonoid f, CFunctor f', CFoldable f', Dom f a, Dom f' (f a),
 Dom f' (Sized f n a)) =>
Sized f' m (Sized f n a) -> Sized f (m * n) a
S.concat @Nat

--------------------------------------------------------------------------------
--- Zips
--------------------------------------------------------------------------------

-- | Zipping two sequences. Length is adjusted to shorter one.
--
-- Since 0.7.0.0
{-# INLINE zip #-}
zip :: (Dom f a, Dom f b, Dom f (a, b), CZip f)
  => Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)
zip :: Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)
zip = forall nat (f :: Type -> Type) (n :: nat) a (m :: nat) b.
(Dom f a, CZip f, Dom f b, Dom f (a, b)) =>
Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)
forall (f :: Type -> Type) (n :: Nat) a (m :: Nat) b.
(Dom f a, CZip f, Dom f b, Dom f (a, b)) =>
Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)
S.zip @Nat

-- | 'zip' for the sequences of the same length.
--
-- Since 0.7.0.0
{-# INLINE zipSame #-}
zipSame :: (Dom f a, Dom f b, Dom f (a, b), CZip f)
  => Sized f n a -> Sized f n b -> Sized f n (a, b)
zipSame :: Sized f n a -> Sized f n b -> Sized f n (a, b)
zipSame = forall nat (f :: Type -> Type) (n :: nat) a b.
(Dom f a, CZip f, Dom f b, Dom f (a, b)) =>
Sized f n a -> Sized f n b -> Sized f n (a, b)
forall (f :: Type -> Type) (n :: Nat) a b.
(Dom f a, CZip f, Dom f b, Dom f (a, b)) =>
Sized f n a -> Sized f n b -> Sized f n (a, b)
S.zipSame @Nat

-- | Zipping two sequences with funtion. Length is adjusted to shorter one.
--
-- Since 0.7.0.0
{-# INLINE zipWith #-}
zipWith :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f)
  => (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c
zipWith :: (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c
zipWith = forall nat (f :: Type -> Type) (n :: nat) a (m :: nat) b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c
forall (f :: Type -> Type) (n :: Nat) a (m :: Nat) b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c
S.zipWith @Nat

-- | 'zipWith' for the sequences of the same length.
--
-- Since 0.7.0.0
{-# INLINE zipWithSame #-}
zipWithSame
  :: (Dom f a, Dom f b, Dom f c, CZip f, CFreeMonoid f)
  => (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
zipWithSame :: (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
zipWithSame = forall nat (f :: Type -> Type) (n :: nat) a b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
forall (f :: Type -> Type) (n :: Nat) a b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
S.zipWithSame @Nat

-- | Unzipping the sequence of tuples.
--
-- Since 0.7.0.0
{-# INLINE unzip #-}
unzip
  :: (Dom f a, Dom f b, Dom f (a, b), CUnzip f)
  => Sized f n (a, b) -> (Sized f n a, Sized f n b)
unzip :: Sized f n (a, b) -> (Sized f n a, Sized f n b)
unzip = forall nat (f :: Type -> Type) (n :: nat) a b.
(CUnzip f, Dom f a, Dom f b, Dom f (a, b)) =>
Sized f n (a, b) -> (Sized f n a, Sized f n b)
forall (f :: Type -> Type) (n :: Nat) a b.
(CUnzip f, Dom f a, Dom f b, Dom f (a, b)) =>
Sized f n (a, b) -> (Sized f n a, Sized f n b)
S.unzip @Nat

-- | Unzipping the sequence of tuples.
--
-- Since 0.7.0.0
{-# INLINE unzipWith #-}
unzipWith
  :: (Dom f a, Dom f b, Dom f c, CUnzip f)
  => (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c)
unzipWith :: (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c)
unzipWith = forall nat (f :: Type -> Type) (n :: nat) a b c.
(CUnzip f, Dom f a, Dom f b, Dom f c) =>
(a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c)
forall (f :: Type -> Type) (n :: Nat) a b c.
(CUnzip f, Dom f a, Dom f b, Dom f c) =>
(a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c)
S.unzipWith @Nat

--------------------------------------------------------------------------------
-- Transformation
--------------------------------------------------------------------------------

-- | Map function.
--
-- Since 0.7.0.0
{-# INLINE map #-}
map
  :: (Dom f a, Dom f b, CFreeMonoid f)
  => (a -> b) -> Sized f n a -> Sized f n b
map :: (a -> b) -> Sized f n a -> Sized f n b
map = forall nat (f :: Type -> Type) (n :: nat) a b.
(CFreeMonoid f, Dom f a, Dom f b) =>
(a -> b) -> Sized f n a -> Sized f n b
forall (f :: Type -> Type) (n :: Nat) a b.
(CFreeMonoid f, Dom f a, Dom f b) =>
(a -> b) -> Sized f n a -> Sized f n b
S.map @Nat

-- | Reverse function.
--
-- Since 0.7.0.0
{-# INLINE reverse #-}
reverse :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f n a
reverse :: Sized f n a -> Sized f n a
reverse = forall nat (f :: Type -> Type) (n :: nat) a.
(Dom f a, CFreeMonoid f) =>
Sized f n a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
Sized f n a -> Sized f n a
S.reverse @Nat

-- | Intersperces.
--
-- Since 0.7.0.0
{-# INLINE intersperse #-}
intersperse
  :: (Dom f a, CFreeMonoid f)
  => a -> Sized f n a -> Sized f ((Two * n) -. One) a
intersperse :: a -> Sized f n a -> Sized f ((Two * n) -. One) a
intersperse = forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f ((FromInteger 2 * n) -. One nat) a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f ((FromInteger 2 * n) -. One Nat) a
S.intersperse @Nat

-- | Remove all duplicates.
--
-- Since 0.7.0.0
{-# INLINE nub #-}
nub :: (Dom f a, Eq a, CFreeMonoid f) => Sized f n a -> SomeSized f a
nub :: Sized f n a -> SomeSized f a
nub = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, Dom f a, Eq a, CFreeMonoid f) =>
Sized f n a -> SomeSized' f nat a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, Dom f a, Eq a, CFreeMonoid f) =>
Sized f n a -> SomeSized' f Nat a
S.nub @Nat

-- | Sorting sequence by ascending order.
--
-- Since 0.7.0.0
{-# INLINE sort #-}
sort :: (Dom f a, CFreeMonoid f, Ord a) => Sized f n a -> Sized f n a
sort :: Sized f n a -> Sized f n a
sort = forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a, Ord a) =>
Sized f n a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a, Ord a) =>
Sized f n a -> Sized f n a
S.sort @Nat

-- | Generalized version of 'sort'.
--
-- Since 0.7.0.0
{-# INLINE sortBy #-}
sortBy
  :: (Dom f a, CFreeMonoid f)
  => (a -> a -> Ordering)
  -> Sized f n a -> Sized f n a
sortBy :: (a -> a -> Ordering) -> Sized f n a -> Sized f n a
sortBy = forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> a -> Ordering) -> Sized f n a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> a -> Ordering) -> Sized f n a -> Sized f n a
S.sortBy @Nat

-- | Insert new element into the presorted sequence.
--
-- Since 0.7.0.0
{-# INLINE insert #-}
insert
  :: (Dom f a, CFreeMonoid f, Ord a)
  => a -> Sized f n a -> Sized f ('S n) a
insert :: a -> Sized f n a -> Sized f ('S n) a
insert = forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a, Ord a) =>
a -> Sized f n a -> Sized f (Succ n) a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a, Ord a) =>
a -> Sized f n a -> Sized f (Succ n) a
S.insert @Nat

-- | Generalized version of 'insert'.
--
-- Since 0.7.0.0
{-# INLINE insertBy #-}
insertBy
  :: (Dom f a, CFreeMonoid f)
  => (a -> a -> Ordering) -> a -> Sized f n a -> Sized f ('S n) a
insertBy :: (a -> a -> Ordering) -> a -> Sized f n a -> Sized f ('S n) a
insertBy = forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a
S.insertBy @Nat

--------------------------------------------------------------------------------
-- Conversion
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
--- List
--------------------------------------------------------------------------------

-- | Convert to list.
--
-- Since 0.7.0.0
{-# INLINE toList #-}
toList :: (Dom f a, CFoldable f) => Sized f n a -> [a]
toList :: Sized f n a -> [a]
toList = forall nat (f :: Type -> Type) (n :: nat) a.
(CFoldable f, Dom f a) =>
Sized f n a -> [a]
forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
Sized f n a -> [a]
S.toList @Nat

-- | If the given list is shorter than @n@, then returns @Nothing@
--   Otherwise returns @Sized f n a@ consisting of initial @n@ element
--   of given list.
--
--   Since 0.7.0.0 (type changed)
{-# INLINE fromList #-}
fromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Maybe (Sized f n a)
fromList :: SNat n -> [a] -> Maybe (Sized f n a)
fromList = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
Sing n -> [a] -> Maybe (Sized f n a)
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, CFreeMonoid f, Dom f a) =>
Sing n -> [a] -> Maybe (Sized f n a)
S.fromList @Nat

-- | 'fromList' with the result length inferred.
--
-- Since 0.7.0.0
{-# INLINE fromList' #-}
fromList' :: (Dom f a, CFreeMonoid f, SingI n) => [a] -> Maybe (Sized f n a)
fromList' :: [a] -> Maybe (Sized f n a)
fromList' = forall nat (f :: Type -> Type) (n :: nat) a.
(PeanoOrder nat, Dom f a, CFreeMonoid f, SingI n) =>
[a] -> Maybe (Sized f n a)
forall (f :: Type -> Type) (n :: Nat) a.
(PeanoOrder Nat, Dom f a, CFreeMonoid f, SingI n) =>
[a] -> Maybe (Sized f n a)
S.fromList' @Nat

-- | Unsafe version of 'fromList'. If the length of the given list does not
--   equal to @n@, then something unusual happens.
--
-- Since 0.7.0.0
{-# INLINE unsafeFromList #-}
unsafeFromList :: (Dom f a, CFreeMonoid f) => SNat n -> [a] -> Sized f n a
unsafeFromList :: SNat n -> [a] -> Sized f n a
unsafeFromList = forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a) =>
Sing n -> [a] -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sing n -> [a] -> Sized f n a
S.unsafeFromList @Nat

-- | 'unsafeFromList' with the result length inferred.
--
-- Since 0.7.0.0
{-# INLINE unsafeFromList' #-}
unsafeFromList' :: (Dom f a, SingI n, CFreeMonoid f) => [a] -> Sized f n a
unsafeFromList' :: [a] -> Sized f n a
unsafeFromList' = forall nat (f :: Type -> Type) (n :: nat) a.
(SingI n, CFreeMonoid f, Dom f a) =>
[a] -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(SingI n, CFreeMonoid f, Dom f a) =>
[a] -> Sized f n a
S.unsafeFromList' @Nat

-- | Construct a @Sized f n a@ by padding default value if the given list is short.
--
--   Since 0.5.0.0 (type changed)
{-# INLINE fromListWithDefault #-}
fromListWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> [a] -> Sized f n a
fromListWithDefault :: SNat n -> a -> [a] -> Sized f n a
fromListWithDefault = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, Dom f a, CFreeMonoid f) =>
Sing n -> a -> [a] -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, Dom f a, CFreeMonoid f) =>
Sing n -> a -> [a] -> Sized f n a
S.fromListWithDefault @Nat

-- | 'fromListWithDefault' with the result length inferred.
--
-- Since 0.7.0.0
{-# INLINE fromListWithDefault' #-}
fromListWithDefault' :: (Dom f a, SingI n, CFreeMonoid f)
  => a -> [a] -> Sized f n a
fromListWithDefault' :: a -> [a] -> Sized f n a
fromListWithDefault' = forall nat (f :: Type -> Type) (n :: nat) a.
(PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a) =>
a -> [a] -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(PeanoOrder Nat, SingI n, CFreeMonoid f, Dom f a) =>
a -> [a] -> Sized f n a
S.fromListWithDefault' @Nat

--------------------------------------------------------------------------------
--- Base containes
--------------------------------------------------------------------------------

-- | Forget the length and obtain the wrapped base container.
--
-- Since 0.7.0.0
{-# INLINE unsized #-}
unsized :: Sized f n a -> f a
unsized :: Sized f n a -> f a
unsized = forall nat (f :: Type -> Type) (n :: nat) a. Sized f n a -> f a
forall (f :: Type -> Type) (n :: Nat) a. Sized f n a -> f a
S.unsized @Nat

-- | If the length of the input is shorter than @n@, then returns @Nothing@.
--   Otherwise returns @Sized f n a@ consisting of initial @n@ element
--   of the input.
--
-- Since 0.7.0.0
{-# INLINE toSized #-}
toSized :: (Dom f a, CFreeMonoid f) => SNat n -> f a -> Maybe (Sized f n a)
toSized :: SNat n -> f a -> Maybe (Sized f n a)
toSized = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
Sing n -> f a -> Maybe (Sized f n a)
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, CFreeMonoid f, Dom f a) =>
Sing n -> f a -> Maybe (Sized f n a)
S.toSized @Nat

-- | 'toSized' with the result length inferred.
--
-- Since 0.7.0.0
{-# INLINE toSized' #-}
toSized' :: (Dom f a, CFreeMonoid f, SingI n) => f a -> Maybe (Sized f n a)
toSized' :: f a -> Maybe (Sized f n a)
toSized' = forall nat (f :: Type -> Type) (n :: nat) a.
(PeanoOrder nat, Dom f a, CFreeMonoid f, SingI n) =>
f a -> Maybe (Sized f n a)
forall (f :: Type -> Type) (n :: Nat) a.
(PeanoOrder Nat, Dom f a, CFreeMonoid f, SingI n) =>
f a -> Maybe (Sized f n a)
S.toSized' @Nat

-- | Unsafe version of 'toSized'. If the length of the given list does not
--   equal to @n@, then something unusual happens.
--
-- Since 0.7.0.0
{-# INLINE unsafeToSized #-}
unsafeToSized :: SNat n -> f a -> Sized f n a
unsafeToSized :: SNat n -> f a -> Sized f n a
unsafeToSized = forall nat (f :: Type -> Type) (n :: nat) a.
Sing n -> f a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
Sing n -> f a -> Sized f n a
S.unsafeToSized @Nat

-- | 'unsafeToSized' with the result length inferred.
--
-- Since 0.7.0.0
{-# INLINE unsafeToSized' #-}
unsafeToSized' :: (Dom f a, SingI n) => f a -> Sized f n a
unsafeToSized' :: f a -> Sized f n a
unsafeToSized' = forall nat (f :: Type -> Type) (n :: nat) a.
(SingI n, Dom f a) =>
f a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(SingI n, Dom f a) =>
f a -> Sized f n a
S.unsafeToSized' @Nat

-- | Construct a @Sized f n a@ by padding default value if the given list is short.
--
-- Since 0.7.0.0
{-# INLINE toSizedWithDefault #-}
toSizedWithDefault :: (Dom f a, CFreeMonoid f) => SNat n -> a -> f a -> Sized f n a
toSizedWithDefault :: SNat n -> a -> f a -> Sized f n a
toSizedWithDefault = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
Sing n -> a -> f a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, CFreeMonoid f, Dom f a) =>
Sing n -> a -> f a -> Sized f n a
S.toSizedWithDefault @Nat

-- | 'toSizedWithDefault' with the result length inferred.
--
-- Since 0.7.0.0
{-# INLINE toSizedWithDefault' #-}
toSizedWithDefault' :: (Dom f a, SingI n, CFreeMonoid f)
  => a -> f a -> Sized f n a
toSizedWithDefault' :: a -> f a -> Sized f n a
toSizedWithDefault' = forall nat (f :: Type -> Type) (n :: nat) a.
(PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a) =>
a -> f a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(PeanoOrder Nat, SingI n, CFreeMonoid f, Dom f a) =>
a -> f a -> Sized f n a
S.toSizedWithDefault' @Nat

--------------------------------------------------------------------------------
-- Querying
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
--- Partitioning
--------------------------------------------------------------------------------

-- | The type @Partitioned f n a@ represents partitioned sequence of length @n@.
--   Value @Partitioned lenL ls lenR rs@ stands for:
--
--   * Entire sequence is divided into @ls@ and @rs@, and their length
--     are @lenL@ and @lenR@ resp.
--
--   * @lenL + lenR = n@
--
-- Since 0.7.0.0
type Partitioned f (n :: Nat) a = S.Partitioned f n a

pattern Partitioned
  :: forall (f :: Type -> Type) (n :: Nat) a. ()
  => forall (n1 :: Nat) (m :: Nat). (n ~ (n1 + m), Dom f a)
  => SNat n1 -> Sized f n1 a -> SNat m
  -> Sized f m a -> Partitioned f n a
{-# COMPLETE Partitioned #-}
pattern $bPartitioned :: SNat n1
-> Sized f n1 a -> SNat m -> Sized f m a -> Partitioned f n a
$mPartitioned :: forall r (f :: Type -> Type) (n :: Nat) a.
Partitioned f n a
-> (forall (n1 :: Nat) (m :: Nat).
    (n ~ (n1 + m), Dom f a) =>
    SNat n1 -> Sized f n1 a -> SNat m -> Sized f m a -> r)
-> (Void# -> r)
-> r
Partitioned ls l rs r = S.Partitioned ls l rs r

-- | Take the initial segment as long as elements satisfys the predicate.
--
-- Since 0.7.0.0
{-# INLINE takeWhile #-}
takeWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a
takeWhile :: (a -> Bool) -> Sized f n a -> SomeSized f a
takeWhile = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, Dom f a, CFreeMonoid f) =>
(a -> Bool) -> Sized f n a -> SomeSized' f nat a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, Dom f a, CFreeMonoid f) =>
(a -> Bool) -> Sized f n a -> SomeSized' f Nat a
S.takeWhile @Nat

-- | Drop the initial segment as long as elements satisfys the predicate.
--
-- Since 0.7.0.0
{-# INLINE dropWhile #-}
dropWhile :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> SomeSized f a
dropWhile :: (a -> Bool) -> Sized f n a -> SomeSized f a
dropWhile = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> SomeSized' f nat a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> SomeSized' f Nat a
S.dropWhile @Nat

-- | Split the sequence into the longest prefix
--   of elements that satisfy the predicate
--   and the rest.
--
-- Since 0.7.0.0
{-# INLINE span #-}
span :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
span :: (a -> Bool) -> Sized f n a -> Partitioned f n a
span = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Partitioned f n a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Partitioned f n a
S.span @Nat


-- | Split the sequence into the longest prefix
--   of elements that do not satisfy the
--   predicate and the rest.
--
-- Since 0.7.0.0
{-# INLINE break #-}
break :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
break :: (a -> Bool) -> Sized f n a -> Partitioned f n a
break = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Partitioned f n a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Partitioned f n a
S.break @Nat

-- | Split the sequence in two parts, the first one containing those elements that satisfy the predicate and the second one those that don't.
--
-- Since 0.7.0.0
{-# INLINE partition #-}
partition :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
partition :: (a -> Bool) -> Sized f n a -> Partitioned f n a
partition = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Partitioned f n a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Partitioned f n a
S.partition @Nat

--------------------------------------------------------------------------------
--- Searching
--------------------------------------------------------------------------------
-- | Membership test; see also 'notElem'.
--
-- Since 0.7.0.0
{-# INLINE elem #-}
elem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool
elem :: a -> Sized f n a -> Bool
elem = forall nat (f :: Type -> Type) (n :: nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Bool
forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Bool
S.elem @Nat

-- | Negation of 'elem'.
--
-- Since 0.7.0.0
{-# INLINE notElem #-}
notElem :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Bool
notElem :: a -> Sized f n a -> Bool
notElem = forall nat (f :: Type -> Type) (n :: nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Bool
forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Bool
S.notElem @Nat

-- | Find the element satisfying the predicate.
--
-- Since 0.7.0.0
{-# INLINE find #-}
find :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe a
find :: (a -> Bool) -> Sized f n a -> Maybe a
find = forall nat (f :: Type -> Type) (n :: nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Maybe a
forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Maybe a
S.find @Nat

-- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists.
--
-- Since 0.7.0.0
{-# INLINE findIndex #-}
findIndex :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe Int
findIndex :: (a -> Bool) -> Sized f n a -> Maybe Int
findIndex = forall nat (f :: Type -> Type) (n :: nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Maybe Int
forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Maybe Int
S.findIndex @Nat

-- | 'Ordinal' version of 'findIndex'.
--
-- Since 0.7.0.0
{-# INLINE sFindIndex #-}
sFindIndex :: (Dom f a, SingI n, CFoldable f) => (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
sFindIndex :: (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
sFindIndex = forall nat (f :: Type -> Type) (n :: nat) a.
(SingI n, CFoldable f, Dom f a, HasOrdinal nat) =>
(a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
forall (f :: Type -> Type) (n :: Nat) a.
(SingI n, CFoldable f, Dom f a, HasOrdinal Nat) =>
(a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
S.sFindIndex @Nat

-- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices.
--
-- Since 0.7.0.0
{-# INLINE findIndices #-}
findIndices :: (Dom f a, CFoldable f) => (a -> Bool) -> Sized f n a -> [Int]
findIndices :: (a -> Bool) -> Sized f n a -> [Int]
findIndices = forall nat (f :: Type -> Type) (n :: nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> [Int]
forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> [Int]
S.findIndices @Nat

-- | 'Ordinal' version of 'findIndices'.
--
-- Since 0.7.0.0
{-# INLINE sFindIndices #-}
sFindIndices :: (Dom f a, CFoldable f, SingI n) => (a -> Bool) -> Sized f n a -> [Ordinal n]
sFindIndices :: (a -> Bool) -> Sized f n a -> [Ordinal n]
sFindIndices = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFoldable f, Dom f a, SingI n) =>
(a -> Bool) -> Sized f n a -> [Ordinal n]
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, CFoldable f, Dom f a, SingI n) =>
(a -> Bool) -> Sized f n a -> [Ordinal n]
S.sFindIndices @Nat

-- | Returns the index of the given element in the list, if exists.
--
-- Since 0.7.0.0
{-# INLINE elemIndex #-}
elemIndex :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> Maybe Int
elemIndex :: a -> Sized f n a -> Maybe Int
elemIndex = forall nat (f :: Type -> Type) (n :: nat) a.
(CFoldable f, Eq a, Dom f a) =>
a -> Sized f n a -> Maybe Int
forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Eq a, Dom f a) =>
a -> Sized f n a -> Maybe Int
S.elemIndex @Nat

sElemIndex, sUnsafeElemIndex :: (Dom f a, SingI n, CFoldable f, Eq a) => a -> Sized f n a -> Maybe (Ordinal n)
{-# DEPRECATED sUnsafeElemIndex "Use sElemIndex instead" #-}

-- | Ordinal version of 'elemIndex'.
--   Since 0.7.0.0, we no longer do boundary check inside the definition.
--
--   Since 0.7.0.0
sUnsafeElemIndex :: a -> Sized f n a -> Maybe (Ordinal n)
sUnsafeElemIndex = forall nat (f :: Type -> Type) (n :: nat) a.
(SingI n, CFoldable f, Dom f a, Eq a, HasOrdinal nat) =>
a -> Sized f n a -> Maybe (Ordinal n)
forall (f :: Type -> Type) (n :: Nat) a.
(SingI n, CFoldable f, Dom f a, Eq a, HasOrdinal Nat) =>
a -> Sized f n a -> Maybe (Ordinal n)
S.sElemIndex @Nat

-- | Ordinal version of 'elemIndex'.
--   Since 0.7.0.0, we no longer do boundary check inside the definition.
--
--   Since 0.7.0.0
sElemIndex :: a -> Sized f n a -> Maybe (Ordinal n)
sElemIndex = forall nat (f :: Type -> Type) (n :: nat) a.
(SingI n, CFoldable f, Dom f a, Eq a, HasOrdinal nat) =>
a -> Sized f n a -> Maybe (Ordinal n)
forall (f :: Type -> Type) (n :: Nat) a.
(SingI n, CFoldable f, Dom f a, Eq a, HasOrdinal Nat) =>
a -> Sized f n a -> Maybe (Ordinal n)
S.sElemIndex @Nat

-- | Returns all indices of the given element in the list.
--
-- Since 0.8.0.0
{-# INLINE elemIndices #-}
elemIndices :: (Dom f a, CFoldable f, Eq a) => a -> Sized f n a -> [Int]
elemIndices :: a -> Sized f n a -> [Int]
elemIndices = forall nat (f :: Type -> Type) (n :: nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> [Int]
forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> [Int]
S.elemIndices @Nat

-- | Ordinal version of 'elemIndices'
--
-- Since 0.8.0.0
{-# INLINE sElemIndices #-}
sElemIndices
  :: (Dom f a, CFoldable f, SingI n, Eq a)
  => a -> Sized f n a -> [Ordinal n]
sElemIndices :: a -> Sized f n a -> [Ordinal n]
sElemIndices = forall nat (f :: Type -> Type) (n :: nat) a.
(CFoldable f, HasOrdinal nat, SingI n, Dom f a, Eq a) =>
a -> Sized f n a -> [Ordinal n]
forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, HasOrdinal Nat, SingI n, Dom f a, Eq a) =>
a -> Sized f n a -> [Ordinal n]
S.sElemIndices @Nat


--------------------------------------------------------------------------------
-- Views and Patterns
--------------------------------------------------------------------------------

{-$ViewsAndPatterns #ViewsAndPatterns#

   With GHC's @ViewPatterns@ and @PatternSynonym@ extensions,
   we can pattern-match on arbitrary @Sized f n a@ if @f@ is list-like functor.
   Curretnly, there are two direction view and patterns: Cons and Snoc.
   Assuming underlying sequence type @f@ has O(1) implementation for 'cnull', 'chead'
   (resp. 'clast') and 'ctail' (resp. 'cinit'), We can view and pattern-match on
   cons (resp. snoc) of @Sized f n a@ in O(1).
-}

{-$views #views#

   With @ViewPatterns@ extension, we can pattern-match on 'Sized' value as follows:

@
slen :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n
slen ('viewCons' -> 'NilCV')    = 'SZ'
slen ('viewCons' -> _ ':-' as) = 'SS' (slen as)
slen _                          = error "impossible"
@

   The constraint @('KnownNat' n, 'Dom f a' f)@ is needed for view function.
   In the above, we have extra wildcard pattern (@_@) at the last.
   Code compiles if we removed it, but current GHC warns for incomplete pattern,
   although we know first two patterns exhausts all the case.

   Equivalently, we can use snoc-style pattern-matching:

@
slen :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n
slen ('viewSnoc' -> 'NilSV')     = 'SZ'
slen ('viewSnoc' -> as '-::' _) = 'SS' (slen as)
@
-}


-- | View of the left end of sequence (cons-side).
--
-- Since 0.7.0.0
type ConsView f (n :: Nat) a = S.ConsView f n a

-- | Since 0.8.0.0
pattern NilCV
  :: forall (f :: Type -> Type) n a. ()
  => (n ~ 'Z)
  => ConsView f n a
pattern $bNilCV :: ConsView f n a
$mNilCV :: forall r (f :: Type -> Type) (n :: Nat) a.
ConsView f n a -> ((n ~ 'Z) => r) -> (Void# -> r) -> r
NilCV = S.NilCV

-- | Since 0.8.0.0
pattern (:-)
  :: forall (f :: Type -> Type) n a. ()
  => forall n1. (n ~ (One + n1), SingI n1)
  => a -> Sized f n1 a -> ConsView f n a
pattern l $b:- :: a -> Sized f n1 a -> ConsView f n a
$m:- :: forall r (f :: Type -> Type) (n :: Nat) a.
ConsView f n a
-> (forall (n1 :: Nat).
    (n ~ (One + n1), SingI n1) =>
    a -> Sized f n1 a -> r)
-> (Void# -> r)
-> r
:- ls = l S.:- ls

infixr 9 :-
{-# COMPLETE NilCV, (:-) #-}

-- | Case analysis for the cons-side of sequence.
--
-- Since 0.5.0.0 (type changed)
viewCons :: (Dom f a, SingI n, CFreeMonoid f) => Sized f n a -> ConsView f n a
viewCons :: Sized f n a -> ConsView f n a
viewCons = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) =>
Sized f n a -> ConsView f n a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, SingI n, CFreeMonoid f, Dom f a) =>
Sized f n a -> ConsView f n a
S.viewCons @Nat

-- | View of the left end of sequence (snoc-side).
--
-- Since 0.7.0.0
type SnocView f (n :: Nat) a = S.SnocView f n a

-- | Since 0.8.0.0
pattern NilSV
  :: forall (f :: Type -> Type) n a. ()
  => (n ~ 'Z)
  => SnocView f n a
pattern $bNilSV :: SnocView f n a
$mNilSV :: forall r (f :: Type -> Type) (n :: Nat) a.
SnocView f n a -> ((n ~ 'Z) => r) -> (Void# -> r) -> r
NilSV = S.NilSV

infixl 9 :-::
-- | Since 0.8.0.0
pattern (:-::)
  :: forall (f :: Type -> Type) n a. ()
  => forall n1. (n ~ (n1 + One), SingI n1)
  => Sized f n1 a -> a -> SnocView f n a
pattern ls $b:-:: :: Sized f n1 a -> a -> SnocView f n a
$m:-:: :: forall r (f :: Type -> Type) (n :: Nat) a.
SnocView f n a
-> (forall (n1 :: Nat).
    (n ~ (n1 + One), SingI n1) =>
    Sized f n1 a -> a -> r)
-> (Void# -> r)
-> r
:-:: l = ls S.:-:: l
{-# COMPLETE NilSV, (:-::) #-}

-- | Case analysis for the snoc-side of sequence.
--
-- Since 0.8.0.0 (type changed)
viewSnoc :: (Dom f a, SingI n, CFreeMonoid f) => Sized f n a -> ConsView f n a
viewSnoc :: Sized f n a -> ConsView f n a
viewSnoc = forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) =>
Sized f n a -> ConsView f n a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, SingI n, CFreeMonoid f, Dom f a) =>
Sized f n a -> ConsView f n a
S.viewCons @Nat


{-$patterns #patterns#

   So we can pattern match on both end of sequence via views, but
   it is rather clumsy to nest it. For example:

@
nextToHead :: ('Dom f a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a
nextToHead ('viewCons' -> _ ':-' ('viewCons' -> a ':-' _)) = a
@

   In such a case, with @PatternSynonyms@ extension we can write as follows:

@
nextToHead :: ('Dom f a' f, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a
nextToHead (_ ':<' a ':<' _) = a
@

   Of course, we can also rewrite above @slen@ example using @PatternSynonyms@:

@
slen :: ('SingI' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n
slen 'Nil'      = 'SZ'
slen (_ ':<' as) = 'SS' (slen as)
slen _           = error "impossible"
@

   So, we can use @':<'@ and @'Nil'@ (resp. @':>'@ and @'Nil'@) to
   pattern-match directly on cons-side (resp. snoc-side) as we usually do for lists.
   @'Nil'@, @':<'@, and @':>'@ are neither functions nor data constructors,
   but pattern synonyms so we cannot use them in expression contexts.
   For more detail on pattern synonyms, see
   <http://www.haskell.org/ghc/docs/latest/html/users_guide/syntax-extns.html#pattern-synonyms GHC Users Guide>
   and
   <https://ghc.haskell.org/trac/ghc/wiki/PatternSynonyms HaskellWiki>.
-}

-- | Pattern synonym for cons-side uncons.
pattern (:<)
  :: forall (f :: Type -> Type) a (n :: Nat).
      (Dom f a, SingI n, CFreeMonoid f)
  => forall (n1 :: Nat). (n ~ Succ n1, SingI n1)
  => a -> Sized f n1 a -> Sized f n a
pattern a $b:< :: a -> Sized f n1 a -> Sized f n a
$m:< :: forall r (f :: Type -> Type) a (n :: Nat).
(Dom f a, SingI n, CFreeMonoid f) =>
Sized f n a
-> (forall (n1 :: Nat).
    (n ~ Succ n1, SingI n1) =>
    a -> Sized f n1 a -> r)
-> (Void# -> r)
-> r
:< b = a S.:< b
infixr 5 :<

-- | Pattern synonym for a nil sequence.
pattern Nil
  :: forall (f :: Type -> Type) a n.
      (Dom f a, SingI n, CFreeMonoid f)
  => (n ~ 'Z) => Sized f n a
pattern $bNil :: Sized f n a
$mNil :: forall r (f :: Type -> Type) a (n :: Nat).
(Dom f a, SingI n, CFreeMonoid f) =>
Sized f n a -> ((n ~ 'Z) => r) -> (Void# -> r) -> r
Nil = S.Nil

-- | Pattern synonym for cons-side nil.
pattern NilL :: forall f (n :: Nat) a.
                (SingI n, CFreeMonoid f, Dom f a)
             => n ~ 'Z => Sized f n a
pattern $bNilL :: Sized f n a
$mNilL :: forall r (f :: Type -> Type) (n :: Nat) a.
(SingI n, CFreeMonoid f, Dom f a) =>
Sized f n a -> ((n ~ 'Z) => r) -> (Void# -> r) -> r
NilL = Nil

-- | Pattern synonym for snoc-side unsnoc.
pattern (:>)
  :: forall (f :: Type -> Type) a (n :: Nat).
      (Dom f a, SingI n, CFreeMonoid f)
  => forall (n1 :: Nat). (n ~ (n1 + One), SingI n1)
  => Sized f n1 a -> a -> Sized f n a
pattern a $b:> :: Sized f n1 a -> a -> Sized f n a
$m:> :: forall r (f :: Type -> Type) a (n :: Nat).
(Dom f a, SingI n, CFreeMonoid f) =>
Sized f n a
-> (forall (n1 :: Nat).
    (n ~ (n1 + One), SingI n1) =>
    Sized f n1 a -> a -> r)
-> (Void# -> r)
-> r
:> b = a S.:> b
infixl 5 :>

-- | Pattern synonym for snoc-side nil.
pattern NilR :: forall f (n :: Nat) a.
                (CFreeMonoid f, Dom f a,  SingI n)
             => n ~ 'Z => Sized f n a
pattern $bNilR :: Sized f n a
$mNilR :: forall r (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a, SingI n) =>
Sized f n a -> ((n ~ 'Z) => r) -> (Void# -> r) -> r
NilR = Nil
{-# COMPLETE (:<), NilL #-}
{-# COMPLETE (:<), NilR #-}
{-# COMPLETE (:<), Nil #-}
{-# COMPLETE (:>), NilL #-}
{-# COMPLETE (:>), NilR #-}
{-# COMPLETE (:>), Nil #-}