{-# LANGUAGE CPP, ConstraintKinds, DataKinds, FlexibleContexts             #-}
{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures                      #-}
{-# LANGUAGE MultiParamTypeClasses, NoImplicitPrelude                      #-}
{-# LANGUAGE NoMonomorphismRestriction, NoStarIsType, PatternSynonyms      #-}
{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables, TypeApplications  #-}
{-# LANGUAGE TypeInType, TypeOperators, UndecidableInstances, ViewPatterns #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}
{-# OPTIONS_GHC -fplugin Data.Singletons.TypeNats.Presburger #-}
-- | This module exports provides the functionality to make length-parametrized types
--   from existing 'CFreeMonoid' sequential types,
--   parametrised with GHC's built in '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.Builtin
  ( -- * 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 (:>),
  ) where
import           Data.Sized (DomC)
import qualified Data.Sized as S

import           Control.Subcategory
import           Data.Coerce                  (coerce)
import           Data.Kind                    (Type)
import           Data.Maybe                   (fromJust)
import           Data.Singletons.Prelude      (SNum ((%+)), SingI (sing))
import           Data.Singletons.Prelude.Enum (PEnum (..))
import           Data.Singletons.TypeLits     (SNat, withKnownNat)
import qualified Data.Sized.Internal          as Internal
import           Data.Type.Natural            (IsPeano (toNatural, zeroOrSucc),
                                               Min, PeanoOrder (plusMonotoneR))
import           Data.Type.Natural.Class      (ZeroOrSucc (IsSucc, IsZero),
                                               type (-.))
import qualified Data.Type.Ordinal            as O
import           GHC.TypeNats                 (KnownNat, Nat, type (*),
                                               type (+), type (-), type (<=))
import           Prelude                      (Bool (..), Eq, Int, Maybe,
                                               Monoid, Ord, Ordering, const,
                                               uncurry, ($), (.))
import qualified Prelude                      as P
import           Proof.Propositional          (IsTrue (Witness), withWitness)

type Ordinal = (O.Ordinal :: Nat -> Type)
type a < b = a + 1 <= b

-- | @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 = (Internal.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, KnownNat 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)
sLength :: (Dom f a, KnownNat n) => Sized f n a -> SNat n
{-# INLINE sLength #-}
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
null :: (Dom f a, CFoldable f) => Sized f n a -> Bool
{-# INLINE null #-}
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
(!!) :: forall f m a. (Dom f a, CFoldable f, (1 <= m)) => Sized f m a -> Int -> a
{-# INLINE (!!) #-}
!! :: Sized f m a -> Int -> a
(!!) = (f a -> Int -> a) -> Sized f m a -> Int -> a
coerce ((f a -> Int -> a) -> Sized f m a -> Int -> a)
-> (f a -> Int -> a) -> Sized f m a -> Int -> a
forall a b. (a -> b) -> a -> b
$ Dom f a => f a -> Int -> a
forall (f :: Type -> Type) a.
(CFoldable f, Dom f a) =>
f a -> Int -> a
cindex @f @a

-- | Safe indexing with 'Ordinal's.
--
-- Since 0.7.0.0
(%!!) :: (Dom f c, CFoldable f) => Sized f n c -> Ordinal n -> c
{-# INLINE (%!!) #-}
%!! :: 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
index
  :: (Dom f a, CFoldable f, (1 <= m))
  => Int -> Sized f m a -> a
{-# INLINE index #-}
index :: Int -> Sized f m a -> a
index = (Sized f m a -> Int -> a) -> Int -> Sized f m a -> a
forall a b c. (a -> b -> c) -> b -> a -> c
P.flip Sized f m a -> Int -> a
forall (f :: Type -> Type) (m :: Nat) a.
(Dom f a, CFoldable f, 1 <= m) =>
Sized f m a -> Int -> a
(!!)

-- | Flipped version of '%!!'.
--
-- Since 0.7.0.0
sIndex :: (Dom f c, CFoldable f) => Ordinal n -> Sized f n c -> c
{-# INLINE sIndex #-}
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
head :: forall f n a. (Dom f a, CFoldable f, (1 <= n)) => Sized f n a -> a
{-# INLINE head #-}
head :: Sized f n a -> a
head = (f a -> a) -> Sized f n a -> a
coerce ((f a -> a) -> Sized f n a -> a) -> (f a -> a) -> Sized f n a -> a
forall a b. (a -> b) -> a -> b
$ Dom f a => f a -> a
forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> a
chead @f @a

-- | 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
last :: forall f n a. (Dom f a, CFoldable f, (0 < n)) => Sized f n a -> a
{-# INLINE last #-}
last :: Sized f n a -> a
last = (f a -> a) -> Sized f n a -> a
coerce ((f a -> a) -> Sized f n a -> a) -> (f a -> a) -> Sized f n a -> a
forall a b. (a -> b) -> a -> b
$ Dom f a => f a -> a
forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> a
clast @f @a

-- | 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
uncons
  :: forall f n a.
    (Dom f a, KnownNat n, CFreeMonoid f, (0 < n))
  => Sized f n a -> Uncons f n a
{-# INLINE uncons #-}
uncons :: Sized f n a -> Uncons f n a
uncons =
  (a -> Sized f (n - 1) a -> Uncons f n a)
-> (a, Sized f (n - 1) a) -> Uncons f n a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (KnownNat (Pred n) =>
a -> Sized f (Pred n) a -> Uncons f (1 + Pred n) a
forall (f :: Type -> Type) (n :: Nat) a.
KnownNat n =>
a -> Sized f n a -> Uncons f (1 + n) a
Uncons @f @(Pred n) @a) ((a, Sized f (n - 1) a) -> Uncons f n a)
-> (Sized f n a -> (a, Sized f (n - 1) a))
-> Sized f n a
-> Uncons f n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a -> (a, f a)) -> Sized f n a -> (a, Sized f (n - 1) a)
coerce (Maybe (a, f a) -> (a, f a)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (a, f a) -> (a, f a))
-> (f a -> Maybe (a, f a)) -> f a -> (a, f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom f a => f a -> Maybe (a, f a)
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
f a -> Maybe (a, f a)
cuncons @f @a)

-- | 'uncons' with explicit specified length @n@
--
--   Since 0.7.0.0
uncons'
  :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n))
  => Sized f n a
  -> Uncons f n a
{-# INLINE uncons' #-}
uncons' :: Sized f n a -> Uncons f n a
uncons' = Sized f n a -> Uncons f n a
forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, KnownNat n, CFreeMonoid f, 0 < n) =>
Sized f n a -> Uncons f n a
uncons

-- | 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
unsnoc
  :: (Dom f a, KnownNat n, CFreeMonoid f, (0 < n))
  => Sized f n a -> Unsnoc f n a
{-# INLINE unsnoc #-}
unsnoc :: Sized f n a -> Unsnoc f n a
unsnoc = Sized f n a -> Unsnoc f n a
forall a. HasCallStack => a
P.undefined

-- | 'unsnoc'' with explicit specified length @n@
--
--   Since 0.7.0.0
unsnoc' :: (Dom f a, KnownNat n, CFreeMonoid f) => proxy n -> Sized f (n + 1) a -> Unsnoc f (n + 1) a
{-# INLINE unsnoc' #-}
unsnoc' :: proxy n -> Sized f (n + 1) a -> Unsnoc f (n + 1) 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

data Uncons f n a where
  Uncons :: forall f n a. KnownNat n
    => a -> Sized f n a -> Uncons f (1 + n) a


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
tail :: (Dom f a, CFreeMonoid f) => Sized f (1 + n) a -> Sized f n a
{-# INLINE tail #-}
tail :: Sized f (1 + 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
init :: (Dom f a, CFreeMonoid f) => Sized f (n + 1) a -> Sized f n a
{-# INLINE init #-}
init :: Sized f (n + 1) 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
take
  :: forall n f m a. (Dom f a, CFreeMonoid f, (n <= m))
  => SNat n -> Sized f m a -> Sized f n a
{-# INLINE take #-}
take :: SNat n -> Sized f m a -> Sized f n a
take = (SNat n -> f a -> f a) -> SNat n -> Sized f m a -> Sized f n a
coerce ((SNat n -> f a -> f a) -> SNat n -> Sized f m a -> Sized f n a)
-> (SNat n -> f a -> f a) -> SNat n -> Sized f m a -> Sized f n a
forall a b. (a -> b) -> a -> b
$ Dom f a => Int -> f a -> f a
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake @f @a (Int -> f a -> f a) -> (SNat n -> Int) -> SNat n -> f a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Natural -> Int) -> (SNat n -> Natural) -> SNat n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural @Nat @n

-- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@.
--
-- Since 0.7.0.0
takeAtMost
  :: (Dom f a, CFreeMonoid f)
  => SNat n -> Sized f m a -> Sized f (Min n m) a
{-# INLINE takeAtMost #-}
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
drop
  :: forall n f m a. (Dom f a, CFreeMonoid f, (n <= m))
  => SNat n -> Sized f m a -> Sized f (m - n) a
{-# INLINE drop #-}
drop :: SNat n -> Sized f m a -> Sized f (m - n) a
drop = (SNat n -> f a -> f a)
-> SNat n -> Sized f m a -> Sized f (m - n) a
coerce ((SNat n -> f a -> f a)
 -> SNat n -> Sized f m a -> Sized f (m - n) a)
-> (SNat n -> f a -> f a)
-> SNat n
-> Sized f m a
-> Sized f (m - n) a
forall a b. (a -> b) -> a -> b
$ Dom f a => Int -> f a -> f a
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
cdrop @f @a (Int -> f a -> f a) -> (SNat n -> Int) -> SNat n -> f a -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Natural -> Int) -> (SNat n -> Natural) -> SNat n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural @Nat @n

-- | @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
splitAt
  :: forall n f m a. (Dom f a, CFreeMonoid f, (n <= m))
  => SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a)
{-# INLINE splitAt #-}
splitAt :: SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a)
splitAt = (SNat n -> f a -> (f a, f a))
-> SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a)
coerce ((SNat n -> f a -> (f a, f a))
 -> SNat n -> Sized f m a -> (Sized f n a, Sized f (m - n) a))
-> (SNat n -> f a -> (f a, f a))
-> SNat n
-> Sized f m a
-> (Sized f n a, Sized f (m - n) a)
forall a b. (a -> b) -> a -> b
$ Dom f a => Int -> f a -> (f a, f a)
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> (f a, f a)
csplitAt @f @a (Int -> f a -> (f a, f a))
-> (SNat n -> Int) -> SNat n -> f a -> (f a, f a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Natural -> Int) -> (SNat n -> Natural) -> SNat n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). IsPeano Nat => Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural @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
splitAtMost
  :: (Dom f a, CFreeMonoid f)
  => SNat n -> Sized f m a
  -> (Sized f (Min n m) a, Sized f (m -. n) a)
{-# INLINE splitAtMost #-}
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)
empty :: (Dom f a, Monoid (f a)) => Sized f 0 a
{-# INLINE empty #-}
empty :: Sized f 0 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
singleton :: (Dom f a, CFreeMonoid f) => a -> Sized f 1 a
{-# INLINE singleton #-}
singleton :: a -> Sized f 1 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
toSomeSized :: (Dom f a, CFoldable f) => f a -> SomeSized f a
{-# INLINE toSomeSized #-}
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
replicate :: (Dom f a, CFreeMonoid f) => SNat n -> a -> Sized f n a
{-# INLINE replicate #-}
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
replicate' :: (Dom f a, KnownNat n, CFreeMonoid f) => a -> Sized f n a
{-# INLINE replicate' #-}
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
generate :: (Dom f a, CFreeMonoid f) => SNat n -> (Ordinal n -> a) -> Sized f n a
{-# INLINE generate #-}
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
generate'
  :: forall f n a. (KnownNat n, Dom f a, CFreeMonoid f) => (Ordinal n -> a) -> Sized f n a
{-# INLINE generate' #-}
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
cons :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (1 + n) a
{-# INLINE cons #-}
cons :: a -> Sized f n a -> Sized f (1 + 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
snoc :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + 1) a
{-# INLINE snoc #-}
snoc :: Sized f n a -> a -> Sized f (n + 1) 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
(<|) :: (Dom f a, CFreeMonoid f) => a -> Sized f n a -> Sized f (1 + n) a
{-# INLINE (<|) #-}
<| :: a -> Sized f n a -> Sized f (1 + 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
(|>) :: (Dom f a, CFreeMonoid f) => Sized f n a -> a -> Sized f (n + 1) a
{-# INLINE (|>) #-}
|> :: Sized f n a -> a -> Sized f (n + 1) 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
(++) :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a
{-# INLINE (++) #-}
++ :: 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
append :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f m a -> Sized f (n + m) a
{-# INLINE append #-}
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
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
{-# INLINE concat #-}
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
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)
{-# INLINE zip #-}
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
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)
{-# INLINE zipSame #-}
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
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
{-# INLINE zipWith #-}
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
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
{-# INLINE zipWithSame #-}
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
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)
{-# INLINE unzip #-}
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
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)
{-# INLINE unzipWith #-}
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
map
  :: (Dom f a, Dom f b, CFreeMonoid f)
  => (a -> b) -> Sized f n a -> Sized f n b
{-# INLINE map #-}
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
reverse :: (Dom f a, CFreeMonoid f) => Sized f n a -> Sized f n a
{-# INLINE reverse #-}
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
intersperse
  :: (Dom f a, CFreeMonoid f)
  => a -> Sized f n a -> Sized f ((2 * n) -. 1) a
{-# INLINE intersperse #-}
intersperse :: a -> Sized f n a -> Sized f ((2 * n) -. 1) 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
nub :: (Dom f a, Eq a, CFreeMonoid f) => Sized f n a -> SomeSized f a
{-# INLINE nub #-}
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
sort :: (Dom f a, CFreeMonoid f, Ord a) => Sized f n a -> Sized f n a
{-# INLINE sort #-}
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
sortBy
  :: (Dom f a, CFreeMonoid f)
  => (a -> a -> Ordering)
  -> Sized f n a -> Sized f n a
{-# INLINE sortBy #-}
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
insert
  :: (Dom f a, CFreeMonoid f, Ord a)
  => a -> Sized f n a -> Sized f (n + 1) a
{-# INLINE insert #-}
insert :: a -> Sized f n a -> Sized f (n + 1) 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 (n + 1) a
insertBy :: (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (n + 1) 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, KnownNat 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, KnownNat 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, KnownNat 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, KnownNat 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, KnownNat 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, KnownNat 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
span :: (Dom f a, CFreeMonoid f) => (a -> Bool) -> Sized f n a -> Partitioned f n a
{-# INLINE span #-}
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, KnownNat 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, KnownNat 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.8.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, KnownNat 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, KnownNat 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.9.0.0
data ConsView f n a where
  NilCV :: ConsView f 0 a
  (:-)
    :: (KnownNat n, KnownNat (1 + n))
    => a -> Sized f n a -> ConsView f (1 + n) a


infixr 9 :-

-- | Case analysis for the cons-side of sequence.
--
-- Since 0.5.0.0 (type changed)
viewCons :: forall f n a. (Dom f a, KnownNat n, CFreeMonoid f) => Sized f n a -> ConsView f n a
viewCons :: Sized f n a -> ConsView f n a
viewCons Sized f n a
sz = case Sing n -> ZeroOrSucc n
forall nat (n :: nat). IsPeano nat => Sing n -> ZeroOrSucc n
zeroOrSucc (Sing n -> ZeroOrSucc n) -> Sing n -> ZeroOrSucc n
forall a b. (a -> b) -> a -> b
$ SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n of
  ZeroOrSucc n
IsZero -> ConsView f n a
forall (f :: Type -> Type) a. ConsView f 0 a
NilCV
  IsSucc Sing n1
n' ->
    IsTrue (Case_6989586621679392761 1 (1 + n1) (CmpNat 1 (1 + n1)))
-> ((Case_6989586621679392761 1 (1 + n1) (CmpNat 1 (1 + n1))
     ~ 'True) =>
    ConsView f n a)
-> ConsView f n a
forall (b :: Bool) r. IsTrue b -> ((b ~ 'True) => r) -> r
withWitness (Sing 1
-> Sing 0
-> Sing n1
-> IsTrue (0 <= n1)
-> IsTrue ((1 + 0) <= (1 + n1))
forall nat (n :: nat) (m :: nat) (l :: nat).
PeanoOrder nat =>
Sing n
-> Sing m
-> Sing l
-> IsTrue (m <= l)
-> IsTrue ((n + m) <= (n + l))
plusMonotoneR (SingI 1 => Sing 1
forall k (a :: k). SingI a => Sing a
sing @1) (SingI 0 => Sing 0
forall k (a :: k). SingI a => Sing a
sing @0) Sing n1
n' IsTrue 'True
IsTrue (0 <= n1)
Witness) (((Case_6989586621679392761 1 (1 + n1) (CmpNat 1 (1 + n1))
   ~ 'True) =>
  ConsView f n a)
 -> ConsView f n a)
-> ((Case_6989586621679392761 1 (1 + n1) (CmpNat 1 (1 + n1))
     ~ 'True) =>
    ConsView f n a)
-> ConsView f n a
forall a b. (a -> b) -> a -> b
$
    Sing n1 -> (KnownNat n1 => ConsView f n a) -> ConsView f n a
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat Sing n1
n'
    ((KnownNat n1 => ConsView f n a) -> ConsView f n a)
-> (KnownNat n1 => ConsView f n a) -> ConsView f n a
forall a b. (a -> b) -> a -> b
$ Sing (1 + n1)
-> (KnownNat (1 + n1) => ConsView f n a) -> ConsView f n a
forall (n :: Nat) r. Sing n -> (KnownNat n => r) -> r
withKnownNat (SingI 1 => Sing 1
forall k (a :: k). SingI a => Sing a
sing @1 Sing 1 -> Sing n1 -> Sing (Apply (Apply (+@#@$) 1) n1)
forall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)
%+ Sing n1
n')
    ((KnownNat (1 + n1) => ConsView f n a) -> ConsView f n a)
-> (KnownNat (1 + n1) => ConsView f n a) -> ConsView f n a
forall a b. (a -> b) -> a -> b
$ case Sized f n a -> Uncons f n a
forall (f :: Type -> Type) a (n :: Nat).
(Dom f a, KnownNat n, CFreeMonoid f, 0 < n) =>
Sized f n a -> Uncons f n a
uncons' Sized f n a
sz of
        Uncons a
a Sized f n a
xs -> a
a a -> Sized f n a -> ConsView f (1 + n) a
forall (n :: Nat) a (f :: Type -> Type).
(KnownNat n, KnownNat (1 + n)) =>
a -> Sized f n a -> ConsView f (1 + n) a
:- Sized f n a
xs

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

-- | Since 0.8.0.0
pattern NilSV
  :: forall (f :: Type -> Type) n a. ()
  => (n ~ 0)
  => SnocView f n a
pattern $bNilSV :: SnocView f n a
$mNilSV :: forall r (f :: Type -> Type) (n :: Nat) a.
SnocView f n a -> ((n ~ 0) => 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 + 1), 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 + 1), 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, KnownNat n, CFreeMonoid f) => Sized f n a -> SnocView f n a
viewSnoc :: Sized f n a -> SnocView 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 -> SnocView f n a
forall (f :: Type -> Type) (n :: Nat) a.
(HasOrdinal Nat, SingI n, CFreeMonoid f, Dom f a) =>
Sized f n a -> SnocView f n a
S.viewSnoc @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)
@

   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, KnownNat n, CFreeMonoid f)
  => forall (n1 :: Nat). (n ~ (1 + n1), KnownNat n1, KnownNat n)
  => 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, KnownNat n, CFreeMonoid f) =>
Sized f n a
-> (forall (n1 :: Nat).
    (n ~ (1 + n1), KnownNat n1, KnownNat n) =>
    a -> Sized f n1 a -> r)
-> (Void# -> r)
-> r
:< as <- (viewCons -> a :- as) where
   a
a :< Sized f n1 a
as = a
a a -> Sized f n1 a -> Sized f (1 + n1) a
forall (f :: Type -> Type) a (n :: Nat).
(Dom f a, CFreeMonoid f) =>
a -> Sized f n a -> Sized f (1 + n) a
<| Sized f n1 a
as
infixr 5 :<

chkNil
  :: forall f n a.
      (KnownNat n)
  => Sized f n a -> ZeroOrSucc n
chkNil :: Sized f n a -> ZeroOrSucc n
chkNil = ZeroOrSucc n -> Sized f n a -> ZeroOrSucc n
forall a b. a -> b -> a
const (ZeroOrSucc n -> Sized f n a -> ZeroOrSucc n)
-> ZeroOrSucc n -> Sized f n a -> ZeroOrSucc n
forall a b. (a -> b) -> a -> b
$ Sing n -> ZeroOrSucc n
forall nat (n :: nat). IsPeano nat => Sing n -> ZeroOrSucc n
zeroOrSucc (Sing n -> ZeroOrSucc n) -> Sing n -> ZeroOrSucc n
forall a b. (a -> b) -> a -> b
$ SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n

-- | Pattern synonym for a nil sequence.
pattern Nil
  :: forall (f :: Type -> Type) n a.
      (Dom f a, KnownNat n, CFreeMonoid f)
  => (n ~ 0) => Sized f n a
pattern $bNil :: Sized f n a
$mNil :: forall r (f :: Type -> Type) (n :: Nat) a.
(Dom f a, KnownNat n, CFreeMonoid f) =>
Sized f n a -> ((n ~ 0) => r) -> (Void# -> r) -> r
Nil <- (chkNil -> IsZero) where
  Nil = Sized f n a
forall (f :: Type -> Type) a.
(Dom f a, Monoid (f a)) =>
Sized f 0 a
empty

-- | Pattern synonym for snoc-side unsnoc.
pattern (:>)
  :: forall (f :: Type -> Type) a (n :: Nat).
      (Dom f a, KnownNat n, CFreeMonoid f)
  => forall (n1 :: Nat). (n ~ (n1 + 1), 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, KnownNat n, CFreeMonoid f) =>
Sized f n a
-> (forall (n1 :: Nat).
    (n ~ (n1 + 1), SingI n1) =>
    Sized f n1 a -> a -> r)
-> (Void# -> r)
-> r
:> b = a S.:> b
infixl 5 :>

{-# COMPLETE (:<), Nil #-}
{-# COMPLETE (:>), Nil #-}