{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE NoStarIsType #-}
{-# OPTIONS_GHC -fenable-rewrite-rules #-}
{-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-}

{- | This module provides the functionality to make length-parametrized types
   from existing 'CFreeMonoid' sequential types.

   Most of the complexity of operations for @Sized f n a@ are the same as
   original operations for @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
  ( -- * Main Data-types
    Sized (),
    SomeSized (..),
    DomC (),

    -- * Accessors

    -- ** Length information
    length,
    sLength,
    null,

    -- ** Indexing
    (!!),
    (%!!),
    index,
    sIndex,
    head,
    last,
    uncons,
    uncons',
    Uncons (..),
    unsnoc,
    unsnoc',
    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 (..),
    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 (..),
    viewSnoc,
    SnocView (..),
    pattern Nil,
    pattern (:<),
    pattern (:>),
  )
where

import Control.Applicative (ZipList (..), (<*>))
import Control.Subcategory
  ( CApplicative (..),
    CFoldable (..),
    CFreeMonoid (..),
    CFunctor (..),
    CPointed (..),
    CRepeat (..),
    CSemialign (..),
    CTraversable (..),
    CUnzip (..),
    CZip (..),
    Constrained (Dom),
    cfromList,
    ctoList,
  )
import Data.Coerce (coerce)
import Data.Constraint (Dict (..), withDict)
import qualified Data.Foldable as F
import Data.Kind (Type)
import qualified Data.List as L
import Data.Maybe (fromJust)
import Data.Monoid (Monoid (..), (<>))
import qualified Data.Sequence as Seq
import Data.Sized.Internal
import Data.These (These (..))
import Data.Type.Equality (gcastWith, (:~:) (..))
import Data.Type.Natural
import Data.Type.Ordinal (Ordinal (..), ordToNatural)
import Data.Typeable (Typeable)
import qualified Data.Vector as V
import qualified Data.Vector.Storable as SV
import qualified Data.Vector.Unboxed as UV
import Unsafe.Coerce (unsafeCoerce)
import Prelude
  ( Bool (..),
    Enum (..),
    Eq (..),
    Functor,
    Int,
    Maybe (..),
    Num (..),
    Ord (..),
    Ordering,
    Show (..),
    const,
    flip,
    fmap,
    fromIntegral,
    uncurry,
    ($),
    (.),
  )
import qualified Prelude as P

--------------------------------------------------------------------------------
-- Main data-types
--------------------------------------------------------------------------------

{- | 'Sized' vector 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
-}
data SomeSized f a where
  SomeSized ::
    SNat n ->
    Sized f n a ->
    SomeSized f a

deriving instance Typeable SomeSized

instance Show (f a) => Show (SomeSized f a) where
  showsPrec :: Int -> SomeSized f a -> ShowS
showsPrec Int
d (SomeSized SNat n
_ Sized f n a
s) =
    Bool -> ShowS -> ShowS
P.showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$
      String -> ShowS
P.showString String
"SomeSized _ " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 Sized f n a
s

instance Eq (f a) => Eq (SomeSized f a) where
  (SomeSized SNat n
_ (Sized f a
xs)) == :: SomeSized f a -> SomeSized f a -> Bool
== (SomeSized SNat n
_ (Sized f a
ys)) = f a
xs forall a. Eq a => a -> a -> Bool
== f a
ys

--------------------------------------------------------------------------------
-- Accessors
--------------------------------------------------------------------------------

--------------------------------------------------------------------------------
--- Length infromation
--------------------------------------------------------------------------------

{- | 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)
-}
length ::
  forall f (n :: Nat) a.
  (Dom f a, KnownNat n) =>
  Sized f n a ->
  Int
length :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, KnownNat n) =>
Sized f n a -> Int
length = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
toNatural forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n
{-# INLINE CONLIKE [1] length #-}

lengthTLZero :: Sized f 0 a -> Int
lengthTLZero :: forall (f :: Type -> Type) a. Sized f 0 a -> Int
lengthTLZero = forall a b. a -> b -> a
P.const Int
0
{-# INLINE lengthTLZero #-}

{-# RULES
"length/0" [~1] length = lengthTLZero
  #-}

{- | @SNat@ version of 'length'.

 Since 0.8.0.0 (type changed)
-}
sLength ::
  forall f (n :: Nat) a.
  (Dom f a, KnownNat n) =>
  Sized f n a ->
  SNat n
sLength :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, KnownNat n) =>
Sized f n a -> SNat n
sLength Sized f n a
_ = forall (n :: Nat). KnownNat n => SNat n
sNat @n
{-# INLINE [2] sLength #-}

{- | Test if the sequence is empty or not.

 Since 0.7.0.0
-}
null ::
  forall f (n :: Nat) a.
  (CFoldable f, Dom f a) =>
  Sized f n a ->
  Bool
null :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
Sized f n a -> Bool
null = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> Bool
cnull @f @a
{-# INLINE CONLIKE [2] null #-}

nullTL0 :: Sized f 0 a -> Bool
nullTL0 :: forall (f :: Type -> Type) a. Sized f 0 a -> Bool
nullTL0 = forall a b. a -> b -> a
P.const Bool
True
{-# INLINE nullTL0 #-}

nullPeanoSucc :: Sized f (S n) a -> Bool
nullPeanoSucc :: forall (f :: Type -> Type) (n :: Nat) a. Sized f (S n) a -> Bool
nullPeanoSucc = forall a b. a -> b -> a
P.const Bool
False
{-# INLINE nullPeanoSucc #-}

nullTLSucc :: Sized f (n + 1) a -> Bool
nullTLSucc :: forall (f :: Type -> Type) (n :: Nat) a. Sized f (S n) a -> Bool
nullTLSucc = forall a b. a -> b -> a
P.const Bool
False
{-# INLINE nullTLSucc #-}

{-# RULES
"null/0" [~2] null = nullTL0
"null/0" [~2] null = nullTLSucc
"null/0" [~1] forall (vec :: 1 <= n => Sized f n a).
  null vec =
    False
"null/Sn" [~2] null = nullPeanoSucc
  #-}

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

{- | (Unsafe) indexing with @Int@s.
   If you want to check boundary statically, use '%!!' or 'sIndex'.

 Since 0.7.0.0
-}
(!!) ::
  forall f (m :: Nat) a.
  (CFoldable f, Dom f a, (1 <= m)) =>
  Sized f m a ->
  Int ->
  a
!! :: forall (f :: Type -> Type) (m :: Nat) a.
(CFoldable f, Dom f a, 1 <= m) =>
Sized f m a -> Int -> a
(!!) = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Dom f a) =>
f a -> Int -> a
cindex @f @a
{-# INLINE (!!) #-}

{- | Safe indexing with 'Ordinal's.

 Since 0.7.0.0
-}
(%!!) ::
  forall f (n :: Nat) c.
  (CFoldable f, Dom f c) =>
  Sized f n c ->
  Ordinal n ->
  c
%!! :: forall (f :: Type -> Type) (n :: Nat) c.
(CFoldable f, Dom f c) =>
Sized f n c -> Ordinal n -> c
(%!!) = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ (forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). Ordinal n -> Nat
ordToNatural)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) a.
(CFoldable f, Dom f a) =>
f a -> Int -> a
cindex @f @c
{-# INLINE (%!!) #-}
{-# SPECIALIZE (%!!) :: Sized [] (n :: Nat) a -> Ordinal n -> a #-}
{-# SPECIALIZE (%!!) :: Sized V.Vector (n :: Nat) a -> Ordinal n -> a #-}
{-# SPECIALIZE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: Nat) a -> Ordinal n -> a #-}
{-# SPECIALIZE (%!!) :: SV.Storable a => Sized SV.Vector (n :: Nat) a -> Ordinal n -> a #-}
{-# SPECIALIZE (%!!) :: Sized Seq.Seq (n :: Nat) a -> Ordinal n -> a #-}

{- | Flipped version of '!!'.

 Since 0.7.0.0
-}
index ::
  forall f (m :: Nat) a.
  (CFoldable f, Dom f a, (1 <= m)) =>
  Int ->
  Sized f m a ->
  a
index :: forall (f :: Type -> Type) (m :: Nat) a.
(CFoldable f, Dom f a, 1 <= m) =>
Int -> Sized f m a -> a
index = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: Type -> Type) (m :: Nat) a.
(CFoldable f, Dom f a, 1 <= m) =>
Sized f m a -> Int -> a
(!!)
{-# INLINE index #-}

{- | Flipped version of '%!!'.

 Since 0.7.0.0
-}
sIndex ::
  forall f (n :: Nat) c.
  (CFoldable f, Dom f c) =>
  Ordinal n ->
  Sized f n c ->
  c
sIndex :: forall (f :: Type -> Type) (n :: Nat) c.
(CFoldable f, Dom f c) =>
Ordinal n -> Sized f n c -> c
sIndex = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) c.
(CFoldable f, Dom f c) =>
Sized f n c -> Ordinal n -> c
(%!!) @f @n @c
{-# INLINE sIndex #-}

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

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

{- | 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 :: Nat) a.
  (KnownNat n, CFreeMonoid f, Dom f a, (1 <= n)) =>
  Sized f n a ->
  Uncons f n a
uncons :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a, 1 <= n) =>
Sized f n a -> Uncons f n a
uncons =
  forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat
    (forall (n :: Nat). SNat n -> SNat (Pred n)
sPred forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n)
    forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall (f :: Type -> Type) (n :: Nat) a.
KnownNat n =>
a -> Sized f n a -> Uncons f (1 + n) a
Uncons @f @(Pred n) @a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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' ::
  forall f (n :: Nat) a proxy.
  (KnownNat n, CFreeMonoid f, Dom f a) =>
  proxy n ->
  Sized f (Succ n) a ->
  Uncons f (Succ n) a
uncons' :: forall (f :: Type -> Type) (n :: Nat) a (proxy :: Nat -> Type).
(KnownNat n, CFreeMonoid f, Dom f a) =>
proxy n -> Sized f (Succ n) a -> Uncons f (Succ n) a
uncons' proxy n
_ =
  forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n) forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a, 1 <= n) =>
Sized f n a -> Uncons f n a
uncons
{-# INLINE uncons' #-}

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

{- | 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 ::
  forall f (n :: Nat) a.
  (KnownNat n, CFreeMonoid f, Dom f a, (0 < n)) =>
  Sized f n a ->
  Unsnoc f n a
unsnoc :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a, 0 < n) =>
Sized f n a -> Unsnoc f n a
unsnoc =
  forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat
    (forall (n :: Nat). SNat n -> SNat (Pred n)
sPred forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n)
    forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall (f :: Type -> Type) (n :: Nat) a.
Sized f n a -> a -> Unsnoc f (Succ n) a
Unsnoc @f @(Pred n)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
f a -> Maybe (f a, a)
cunsnoc @f @a)
{-# NOINLINE [1] unsnoc #-}

data Unsnoc f n a where
  Unsnoc :: forall f n a. Sized f (n :: Nat) a -> a -> Unsnoc f (Succ n) a

{- | 'unsnoc'' with explicit specified length @n@

   Since 0.7.0.0
-}
unsnoc' ::
  forall f (n :: Nat) a proxy.
  (KnownNat n, CFreeMonoid f, Dom f a) =>
  proxy n ->
  Sized f (Succ n) a ->
  Unsnoc f (Succ n) a
unsnoc' :: forall (f :: Type -> Type) (n :: Nat) a (proxy :: Nat -> Type).
(KnownNat n, CFreeMonoid f, Dom f a) =>
proxy n -> Sized f (Succ n) a -> Unsnoc f (Succ n) a
unsnoc' proxy n
_ =
  forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n) forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a, 0 < n) =>
Sized f n a -> Unsnoc f n a
unsnoc
{-# INLINE unsnoc' #-}

--------------------------------------------------------------------------------
--- Slicing
--------------------------------------------------------------------------------

{- | 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 ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  Sized f (1 + n) a ->
  Sized f n a
tail :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f (1 + n) a -> Sized f n a
tail = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
f a -> f a
ctail @f @a
{-# INLINE tail #-}

{- | 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 ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  Sized f (n + 1) a ->
  Sized f n a
init :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f (n + 1) a -> Sized f n a
init = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
f a -> f a
cinit @f @a
{-# INLINE init #-}

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

{- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@.

 Since 0.7.0.0
-}
takeAtMost ::
  forall (n :: Nat) f m a.
  (CFreeMonoid f, Dom f a) =>
  SNat n ->
  Sized f m a ->
  Sized f (Min n m) a
takeAtMost :: forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> Sized f m a -> Sized f (Min n m) a
takeAtMost = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake @f @a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SNat n -> Nat
toNatural @n
{-# INLINE takeAtMost #-}

{- | @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 :: Nat) f (m :: Nat) a.
  (CFreeMonoid f, Dom f a, (n <= m)) =>
  SNat n ->
  Sized f m a ->
  Sized f (m - n) a
drop :: forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(CFreeMonoid f, Dom f a, n <= m) =>
SNat n -> Sized f m a -> Sized f (m - n) a
drop = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
cdrop @f @a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SNat n -> Nat
toNatural @n
{-# INLINE drop #-}

{- | @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 :: Nat) f m a.
  (CFreeMonoid f, Dom f a, (n <= m)) =>
  SNat n ->
  Sized f m a ->
  (Sized f n a, Sized f (m -. n) a)
splitAt :: forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(CFreeMonoid f, Dom f a, n <= m) =>
SNat n -> Sized f m a -> (Sized f n a, Sized f (m -. n) a)
splitAt =
  coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> (f a, f a)
csplitAt @f @a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SNat n -> Nat
toNatural @n
{-# INLINE splitAt #-}

{- | @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 ::
  forall (n :: Nat) f (m :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  SNat n ->
  Sized f m a ->
  (Sized f (Min n m) a, Sized f (m -. n) a)
splitAtMost :: forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a)
splitAtMost =
  coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> (f a, f a)
csplitAt @f @a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SNat n -> Nat
toNatural @n
{-# INLINE splitAtMost #-}

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

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

{- | Empty sequence.

 Since 0.7.0.0 (type changed)
-}
empty ::
  forall f a.
  (Monoid (f a), Dom f a) =>
  Sized f (0) a
empty :: forall (f :: Type -> Type) a.
(Monoid (f a), Dom f a) =>
Sized f 0 a
empty = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => a
mempty @(f a)
{-# INLINE empty #-}

{- | Sequence with one element.

 Since 0.7.0.0
-}
singleton :: forall f a. (CPointed f, Dom f a) => a -> Sized f (1) a
singleton :: forall (f :: Type -> Type) a.
(CPointed f, Dom f a) =>
a -> Sized f 1 a
singleton = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. (CPointed f, Dom f a) => a -> f a
cpure @f @a
{-# INLINE singleton #-}

{- | 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 ::
  forall f a.
  (Dom f a, CFoldable f) =>
  f a ->
  SomeSized f a
{-# INLINE toSomeSized #-}
toSomeSized :: forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized = \f a
xs ->
  case Nat -> SomeSNat
toSomeSNat forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> Int
clength f a
xs of
    SomeSNat SNat n
sn -> forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Type -> Type) a.
SNat n -> Sized f n a -> SomeSized f a
SomeSized SNat n
sn forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a.
SNat n -> f a -> Sized f n a
unsafeToSized SNat n
sn f a
xs

{- | Replicates the same value.

 Since 0.7.0.0
-}
replicate ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  SNat n ->
  a ->
  Sized f n a
replicate :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> Sized f n a
replicate = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> a -> f a
creplicate @f @a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SNat n -> Nat
toNatural @n
{-# INLINE replicate #-}

{- | 'replicate' with the length inferred.

 Since 0.7.0.0
-}
replicate' ::
  forall f (n :: Nat) a.
  (KnownNat (n :: Nat), CFreeMonoid f, Dom f a) =>
  a ->
  Sized f n a
replicate' :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> Sized f n a
replicate' = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> Sized f n a
replicate (forall (n :: Nat). KnownNat n => SNat n
sNat @n)
{-# INLINE replicate' #-}

{- | Construct a sequence of the given length by applying the function to each index.

 Since 0.7.0.0
-}
generate ::
  forall f (n :: Nat) (a :: Type).
  (CFreeMonoid f, Dom f a) =>
  SNat n ->
  (Ordinal n -> a) ->
  Sized f n a
generate :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> (Ordinal n -> a) -> Sized f n a
generate = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ \SNat n
sn ->
  forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn forall a b. (a -> b) -> a -> b
$
    forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> (Int -> a) -> f a
cgenerate @f @a (forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
toNatural @n SNat n
sn)
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => Int -> a
toEnum @(Ordinal n))
{-# INLINE [1] generate #-}

{- | 'generate' with length inferred.

   Since 0.8.0.0
-}
generate' ::
  forall f (n :: Nat) (a :: Type).
  (KnownNat n, CFreeMonoid f, Dom f a) =>
  (Ordinal n -> a) ->
  Sized f n a
generate' :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
(Ordinal n -> a) -> Sized f n a
generate' = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> (Ordinal n -> a) -> Sized f n a
generate forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE [1] generate' #-}

genVector ::
  forall (n :: Nat) a.
  SNat n ->
  (Ordinal n -> a) ->
  Sized V.Vector n a
genVector :: forall (n :: Nat) a. SNat n -> (Ordinal n -> a) -> Sized Vector n a
genVector SNat n
n Ordinal n -> a
f = forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$ forall a. Int -> (Int -> a) -> Vector a
V.generate (forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
toNatural SNat n
n) (Ordinal n -> a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => Int -> a
toEnum)
{-# INLINE genVector #-}

genSVector ::
  forall (n :: Nat) a.
  (SV.Storable a) =>
  SNat n ->
  (Ordinal n -> a) ->
  Sized SV.Vector n a
genSVector :: forall (n :: Nat) a.
Storable a =>
SNat n -> (Ordinal n -> a) -> Sized Vector n a
genSVector SNat n
n Ordinal n -> a
f = forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$ forall a. Storable a => Int -> (Int -> a) -> Vector a
SV.generate (forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
toNatural SNat n
n) (Ordinal n -> a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => Int -> a
toEnum)
{-# INLINE genSVector #-}

genSeq ::
  forall (n :: Nat) a.
  SNat n ->
  (Ordinal n -> a) ->
  Sized Seq.Seq n a
genSeq :: forall (n :: Nat) a. SNat n -> (Ordinal n -> a) -> Sized Seq n a
genSeq SNat n
n Ordinal n -> a
f = forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$ forall a. Int -> (Int -> a) -> Seq a
Seq.fromFunction (forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
toNatural SNat n
n) (Ordinal n -> a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => Int -> a
toEnum)
{-# INLINE genSeq #-}

{-# RULES
"generate/Vector" [~1] generate = genVector
"generate/SVector" [~1] forall
  (n :: SNat (n :: Nat))
  (f :: SV.Storable a => Ordinal n -> a).
  generate n f =
    genSVector n f
"generate/UVector" [~1] forall
  (n :: SNat (n :: Nat))
  (f :: UV.Unbox a => Ordinal n -> a).
  generate n f =
    withKnownNat n $ Sized (UV.generate (P.fromIntegral $ toNatural n) (f . toEnum))
"generate/Seq" [~1] generate = genSeq
  #-}

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

{- | Append an element to the head of sequence.

 Since 0.8.0.0
-}
cons ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  a ->
  Sized f n a ->
  Sized f (1 + n) a
cons :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (1 + n) a
cons = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
a -> f a -> f a
ccons @f @a
{-# INLINE cons #-}

{- | Infix version of 'cons'.

 Since 0.8.0.0
-}
(<|) ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  a ->
  Sized f n a ->
  Sized f (1 + n) a
<| :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (1 + n) a
(<|) = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (1 + n) a
cons
{-# INLINE (<|) #-}

infixr 5 <|

{- | Append an element to the tail of sequence.

 Since 0.7.0.0
-}
snoc ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  Sized f n a ->
  a ->
  Sized f (n + 1) a
snoc :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + 1) a
snoc (Sized f a
xs) a
a = forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
f a -> a -> f a
csnoc f a
xs a
a
{-# INLINE snoc #-}

{- | Infix version of 'snoc'.

 Since 0.7.0.0
-}
(|>) ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  Sized f n a ->
  a ->
  Sized f (n + 1) a
|> :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + 1) a
(|>) = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + 1) a
snoc
{-# INLINE (|>) #-}

infixl 5 |>

{- | Append two lists.

 Since 0.7.0.0
-}
append ::
  forall f (n :: Nat) (m :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  Sized f n a ->
  Sized f m a ->
  Sized f (n + m) a
append :: 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
append = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => a -> a -> a
mappend @(f a)
{-# INLINE append #-}

{- | Infix version of 'append'.

 Since 0.7.0.0
-}
(++) ::
  forall f (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
(++) = 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
append

infixr 5 ++

{- | Concatenates multiple sequences into one.

 Since 0.7.0.0
-}
concat ::
  forall f' (m :: Nat) f (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
concat :: 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
concat = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a w.
(CFoldable f, Dom f a, Monoid w) =>
(a -> w) -> f a -> w
cfoldMap @f' @(Sized f n a) forall (f :: Type -> Type) (n :: Nat) a. Sized f n a -> f a
runSized
{-# INLINE [2] concat #-}

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

{- | Zipping two sequences. Length is adjusted to shorter one.

 Since 0.7.0.0
-}
zip ::
  forall f (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)
zip :: 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)
zip = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b.
(CZip f, Dom f a, Dom f b, Dom f (a, b)) =>
f a -> f b -> f (a, b)
czip @f @a @b

{- | 'zip' for the sequences of the same length.

 Since 0.7.0.0
-}
zipSame ::
  forall f (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)
zipSame :: 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)
zipSame = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b.
(CZip f, Dom f a, Dom f b, Dom f (a, b)) =>
f a -> f b -> f (a, b)
czip @f @a @b
{-# INLINE [1] zipSame #-}

{- | Zipping two sequences with funtion. Length is adjusted to shorter one.

 Since 0.7.0.0
-}
zipWith ::
  forall f (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
zipWith :: 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
zipWith = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b c.
(CZip f, Dom f a, Dom f b, Dom f c) =>
(a -> b -> c) -> f a -> f b -> f c
czipWith @f @a @b @c
{-# INLINE [1] zipWith #-}

{- | 'zipWith' for the sequences of the same length.

 Since 0.7.0.0
-}
zipWithSame ::
  forall f (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
zipWithSame :: 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
zipWithSame = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b c.
(CZip f, Dom f a, Dom f b, Dom f c) =>
(a -> b -> c) -> f a -> f b -> f c
czipWith @f @a @b @c
{-# INLINE [1] zipWithSame #-}

{- | Unzipping the sequence of tuples.

 Since 0.7.0.0
-}
unzip ::
  forall f (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)
unzip :: 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)
unzip = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b.
(CUnzip f, Dom f (a, b), Dom f a, Dom f b) =>
f (a, b) -> (f a, f b)
cunzip @f @a @b
{-# INLINE unzip #-}

{- | Unzipping the sequence of tuples.

 Since 0.7.0.0
-}
unzipWith ::
  forall f (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)
unzipWith :: 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)
unzipWith = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) c a b.
(CUnzip f, Dom f c, Dom f a, Dom f b) =>
(c -> (a, b)) -> f c -> (f a, f b)
cunzipWith @f @a @b @c
{-# INLINE unzipWith #-}

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

{- | Map function.

 Since 0.7.0.0
-}
map ::
  forall f (n :: Nat) a b.
  (CFreeMonoid f, Dom f a, Dom f b) =>
  (a -> b) ->
  Sized f n a ->
  Sized f n b
map :: 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
map a -> b
f = forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) a b.
(CFunctor f, Dom f a, Dom f b) =>
(a -> b) -> f a -> f b
cmap a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) (n :: Nat) a. Sized f n a -> f a
runSized
{-# INLINE map #-}

{- | Reverse function.

 Since 0.7.0.0
-}
reverse ::
  forall f (n :: Nat) a.
  (Dom f a, CFreeMonoid f) =>
  Sized f n a ->
  Sized f n a
reverse :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
Sized f n a -> Sized f n a
reverse = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
f a -> f a
creverse @f @a
{-# INLINE reverse #-}

{- | Intersperces.

 Since 0.7.0.0
-}
intersperse ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  a ->
  Sized f n a ->
  Sized f ((2 * n) -. 1) a
intersperse :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f ((2 * n) -. 1) a
intersperse = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
a -> f a -> f a
cintersperse @f @a
{-# INLINE intersperse #-}

{- | Remove all duplicates.

 Since 0.7.0.0
-}
nub ::
  forall f (n :: Nat) a.
  (Dom f a, Eq a, CFreeMonoid f) =>
  Sized f n a ->
  SomeSized f a
nub :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, Eq a, CFreeMonoid f) =>
Sized f n a -> SomeSized f a
nub = forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a, Eq a) =>
f a -> f a
cnub @f @a)

{- | Sorting sequence by ascending order.

 Since 0.7.0.0
-}
sort ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a, Ord a) =>
  Sized f n a ->
  Sized f n a
sort :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a, Ord a) =>
Sized f n a -> Sized f n a
sort = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a, Ord a) =>
f a -> f a
csort @f @a

{- | Generalized version of 'sort'.

 Since 0.7.0.0
-}
sortBy ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  (a -> a -> Ordering) ->
  Sized f n a ->
  Sized f n a
sortBy :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> a -> Ordering) -> Sized f n a -> Sized f n a
sortBy = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> a -> Ordering) -> f a -> f a
csortBy @f @a

{- | Insert new element into the presorted sequence.

 Since 0.7.0.0
-}
insert ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a, Ord a) =>
  a ->
  Sized f n a ->
  Sized f (Succ n) a
insert :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a, Ord a) =>
a -> Sized f n a -> Sized f (Succ n) a
insert = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a, Ord a) =>
a -> f a -> f a
cinsert @f @a

{- | Generalized version of 'insert'.

 Since 0.7.0.0
-}
insertBy ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  (a -> a -> Ordering) ->
  a ->
  Sized f n a ->
  Sized f (Succ n) a
insertBy :: 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
insertBy = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> a -> Ordering) -> a -> f a -> f a
cinsertBy @f @a

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

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

{- | Convert to list.

 Since 0.7.0.0
-}
toList ::
  forall f (n :: Nat) a.
  (CFoldable f, Dom f a) =>
  Sized f n a ->
  [a]
toList :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
Sized f n a -> [a]
toList = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> [a]
ctoList @f @a
{-# INLINE [2] toList #-}

{-# RULES
"toList/List"
  Data.Sized.toList =
    runSized
  #-}

{- | 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)
-}
fromList ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  SNat n ->
  [a] ->
  Maybe (Sized f n a)
fromList :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> [a] -> Maybe (Sized f n a)
fromList SNat n
Zero [a]
_ = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized (forall a. Monoid a => a
mempty :: f a)
fromList SNat n
sn [a]
xs =
  let len :: Int
len = forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
toNatural SNat n
sn
   in if forall (t :: Type -> Type) a. Foldable t => t a -> Int
P.length [a]
xs forall a. Ord a => a -> a -> Bool
< Int
len
        then forall a. Maybe a
Nothing
        else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake Int
len forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
[a] -> f a
cfromList [a]
xs
{-# INLINEABLE [2] fromList #-}

{- | 'fromList' with the result length inferred.

 Since 0.7.0.0
-}
fromList' ::
  forall f (n :: Nat) a.
  (Dom f a, CFreeMonoid f, KnownNat n) =>
  [a] ->
  Maybe (Sized f n a)
fromList' :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f, KnownNat n) =>
[a] -> Maybe (Sized f n a)
fromList' = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> [a] -> Maybe (Sized f n a)
fromList forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE fromList' #-}

{- | 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
-}
unsafeFromList ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  SNat n ->
  [a] ->
  Sized f n a
unsafeFromList :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> [a] -> Sized f n a
unsafeFromList = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
[a] -> f a
cfromList @f @a
{-# INLINE [1] unsafeFromList #-}

{- | 'unsafeFromList' with the result length inferred.

 Since 0.7.0.0
-}
unsafeFromList' ::
  forall f (n :: Nat) a.
  (KnownNat n, CFreeMonoid f, Dom f a) =>
  [a] ->
  Sized f n a
unsafeFromList' :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
[a] -> Sized f n a
unsafeFromList' = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> [a] -> Sized f n a
unsafeFromList forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE [1] unsafeFromList' #-}

{-# RULES
"unsafeFromList'/List" [~1]
  unsafeFromList' =
    Sized
"unsafeFromList'/Vector" [~1]
  unsafeFromList' =
    Sized . V.fromList
"unsafeFromList'/Seq" [~1]
  unsafeFromList' =
    Sized . Seq.fromList
"unsafeFromList'/SVector" [~1] forall (xs :: SV.Storable a => [a]).
  unsafeFromList' xs =
    Sized (SV.fromList xs)
"unsafeFromList'/UVector" [~1] forall (xs :: UV.Unbox a => [a]).
  unsafeFromList' xs =
    Sized (UV.fromList xs)
  #-}

{- | Construct a @Sized f n a@ by padding default value if the given list is short.

   Since 0.5.0.0 (type changed)
-}
fromListWithDefault ::
  forall f (n :: Nat) a.
  (Dom f a, CFreeMonoid f) =>
  SNat n ->
  a ->
  [a] ->
  Sized f n a
fromListWithDefault :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
SNat n -> a -> [a] -> Sized f n a
fromListWithDefault SNat n
sn a
def [a]
xs =
  let len :: Int
len = forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
toNatural SNat n
sn
   in forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$
        forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
[a] -> f a
cfromList (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake Int
len [a]
xs)
          forall a. Semigroup a => a -> a -> a
<> forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> a -> f a
creplicate (Int
len forall a. Num a => a -> a -> a
- forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> Int
clength [a]
xs) a
def
{-# INLINEABLE fromListWithDefault #-}

{- | 'fromListWithDefault' with the result length inferred.

 Since 0.7.0.0
-}
fromListWithDefault' ::
  forall f (n :: Nat) a.
  (KnownNat n, CFreeMonoid f, Dom f a) =>
  a ->
  [a] ->
  Sized f n a
fromListWithDefault' :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> [a] -> Sized f n a
fromListWithDefault' = forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
SNat n -> a -> [a] -> Sized f n a
fromListWithDefault forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE fromListWithDefault' #-}

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

{- | Forget the length and obtain the wrapped base container.

 Since 0.7.0.0
-}
unsized :: forall f (n :: Nat) a. Sized f n a -> f a
unsized :: forall (f :: Type -> Type) (n :: Nat) a. Sized f n a -> f a
unsized = forall (f :: Type -> Type) (n :: Nat) a. Sized f n a -> f a
runSized
{-# INLINE unsized #-}

{- | 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
-}
toSized ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  SNat (n :: Nat) ->
  f a ->
  Maybe (Sized f n a)
toSized :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> f a -> Maybe (Sized f n a)
toSized SNat n
sn f a
xs =
  let len :: Int
len = forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
toNatural SNat n
sn
   in if forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> Int
clength f a
xs forall a. Ord a => a -> a -> Bool
< Int
len
        then forall a. Maybe a
Nothing
        else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a.
SNat n -> f a -> Sized f n a
unsafeToSized SNat n
sn forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake Int
len f a
xs
{-# INLINEABLE [2] toSized #-}

{- | 'toSized' with the result length inferred.

 Since 0.7.0.0
-}
toSized' ::
  forall f (n :: Nat) a.
  (Dom f a, CFreeMonoid f, KnownNat n) =>
  f a ->
  Maybe (Sized f n a)
toSized' :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f, KnownNat n) =>
f a -> Maybe (Sized f n a)
toSized' = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> f a -> Maybe (Sized f n a)
toSized forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE toSized' #-}

{- | 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
-}
unsafeToSized :: forall f (n :: Nat) a. SNat n -> f a -> Sized f n a
unsafeToSized :: forall (f :: Type -> Type) (n :: Nat) a.
SNat n -> f a -> Sized f n a
unsafeToSized SNat n
_ = forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized
{-# INLINE [2] unsafeToSized #-}

{- | 'unsafeToSized' with the result length inferred.

 Since 0.7.0.0
-}
unsafeToSized' ::
  forall f (n :: Nat) a.
  (KnownNat n, Dom f a) =>
  f a ->
  Sized f n a
unsafeToSized' :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, Dom f a) =>
f a -> Sized f n a
unsafeToSized' = forall (f :: Type -> Type) (n :: Nat) a.
SNat n -> f a -> Sized f n a
unsafeToSized forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE unsafeToSized' #-}

{- | Construct a @Sized f n a@ by padding default value if the given list is short.

 Since 0.7.0.0
-}
toSizedWithDefault ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  SNat (n :: Nat) ->
  a ->
  f a ->
  Sized f n a
toSizedWithDefault :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> f a -> Sized f n a
toSizedWithDefault SNat n
sn a
def f a
xs =
  let len :: Int
len = forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
toNatural SNat n
sn
   in forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake Int
len f a
xs forall a. Semigroup a => a -> a -> a
<> forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> a -> f a
creplicate (Int
len forall a. Num a => a -> a -> a
- forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> Int
clength f a
xs) a
def
{-# INLINEABLE toSizedWithDefault #-}

{- | 'toSizedWithDefault' with the result length inferred.

 Since 0.7.0.0
-}
toSizedWithDefault' ::
  forall f (n :: Nat) a.
  (KnownNat n, CFreeMonoid f, Dom f a) =>
  a ->
  f a ->
  Sized f n a
toSizedWithDefault' :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> f a -> Sized f n a
toSizedWithDefault' = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> f a -> Sized f n a
toSizedWithDefault forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE toSizedWithDefault' #-}

--------------------------------------------------------------------------------
-- 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
-}
data Partitioned f n a where
  Partitioned ::
    (Dom f a) =>
    SNat n ->
    Sized f n a ->
    SNat m ->
    Sized f m a ->
    Partitioned f (n + m) a

{- | Take the initial segment as long as elements satisfys the predicate.

 Since 0.7.0.0
-}
takeWhile ::
  forall f (n :: Nat) a.
  (Dom f a, CFreeMonoid f) =>
  (a -> Bool) ->
  Sized f n a ->
  SomeSized f a
takeWhile :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
(a -> Bool) -> Sized f n a -> SomeSized f a
takeWhile = (forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> f a -> f a
ctakeWhile @f @a)
{-# INLINE takeWhile #-}

{- | Drop the initial segment as long as elements satisfys the predicate.

 Since 0.7.0.0
-}
dropWhile ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  (a -> Bool) ->
  Sized f n a ->
  SomeSized f a
dropWhile :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> SomeSized f a
dropWhile = (forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> f a -> f a
cdropWhile @f @a)
{-# INLINE dropWhile #-}

{- | Split the sequence into the longest prefix
   of elements that satisfy the predicate
   and the rest.

 Since 0.7.0.0
-}
span ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  (a -> Bool) ->
  Sized f n a ->
  Partitioned f n a
span :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Partitioned f n a
span = (forall (n :: Nat) (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned @n forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> f a -> (f a, f a)
cspan @f @a)
{-# INLINE span #-}

{- | Split the sequence into the longest prefix
   of elements that do not satisfy the
   predicate and the rest.

 Since 0.7.0.0
-}
break ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  (a -> Bool) ->
  Sized f n a ->
  Partitioned f n a
break :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Partitioned f n a
break = (forall (n :: Nat) (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned @n forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> f a -> (f a, f a)
cbreak @f @a)
{-# INLINE break #-}

{- | 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
-}
partition ::
  forall f (n :: Nat) a.
  (CFreeMonoid f, Dom f a) =>
  (a -> Bool) ->
  Sized f n a ->
  Partitioned f n a
partition :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Partitioned f n a
partition = (forall (n :: Nat) (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned @n forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> f a -> (f a, f a)
cpartition @f @a)
{-# INLINE partition #-}

unsafePartitioned ::
  forall (n :: Nat) f a.
  (CFreeMonoid f, Dom f a) =>
  (f a, f a) ->
  Partitioned f n a
unsafePartitioned :: forall (n :: Nat) (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned (f a
l, f a
r) =
  case (forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized f a
l, forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized f a
r) of
    ( SomeSized (SNat n
lenL :: SNat nl) Sized f n a
ls
      , SomeSized (SNat n
lenR :: SNat nr) Sized f n a
rs
      ) ->
        forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith
          ( forall a b. a -> b
unsafeCoerce forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl @() ::
              n :~: nl + nr
          )
          forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a (n :: Nat) (m :: Nat).
Dom f a =>
SNat n
-> Sized f n a -> SNat m -> Sized f m a -> Partitioned f (n + m) a
Partitioned SNat n
lenL Sized f n a
ls SNat n
lenR Sized f n a
rs

--------------------------------------------------------------------------------
--- Searching
--------------------------------------------------------------------------------

{- | Membership test; see also 'notElem'.

 Since 0.7.0.0
-}
elem ::
  forall f (n :: Nat) a.
  (CFoldable f, Dom f a, Eq a) =>
  a ->
  Sized f n a ->
  Bool
elem :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Bool
elem = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Eq a, Dom f a) =>
a -> f a -> Bool
celem @f @a
{-# INLINE elem #-}

{- | Negation of 'elem'.

 Since 0.7.0.0
-}
notElem ::
  forall f (n :: Nat) a.
  (CFoldable f, Dom f a, Eq a) =>
  a ->
  Sized f n a ->
  Bool
notElem :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Bool
notElem = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Eq a, Dom f a) =>
a -> f a -> Bool
cnotElem @f @a
{-# INLINE notElem #-}

{- | Find the element satisfying the predicate.

 Since 0.7.0.0
-}
find ::
  forall f (n :: Nat) a.
  (CFoldable f, Dom f a) =>
  (a -> Bool) ->
  Sized f n a ->
  Maybe a
find :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Maybe a
find = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> f a -> Maybe a
cfind @f @a
{-# INLINE [1] find #-}

{-# RULES
"find/List" [~1] forall p.
  find p =
    L.find @[] p . runSized
"find/Vector" [~1] forall p.
  find p =
    V.find p . runSized
"find/Storable Vector" [~1] forall (p :: SV.Storable a => a -> Bool).
  find p =
    SV.find p . runSized
"find/Unboxed Vector" [~1] forall (p :: UV.Unbox a => a -> Bool).
  find p =
    UV.find p . runSized
  #-}

{- | @'findIndex' p xs@ find the element satisfying @p@ and returns its index if exists.

 Since 0.7.0.0
-}
findIndex ::
  forall f (n :: Nat) a.
  (CFoldable f, Dom f a) =>
  (a -> Bool) ->
  Sized f n a ->
  Maybe Int
findIndex :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Maybe Int
findIndex = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> f a -> Maybe Int
cfindIndex @f @a
{-# INLINE findIndex #-}

{- | 'Ordinal' version of 'findIndex'.

 Since 0.7.0.0
-}
sFindIndex ::
  forall f (n :: Nat) a.
  (KnownNat (n :: Nat), CFoldable f, Dom f a) =>
  (a -> Bool) ->
  Sized f n a ->
  Maybe (Ordinal n)
sFindIndex :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
sFindIndex = (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Enum a => Int -> a
toEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> f a -> Maybe Int
cfindIndex @f @a)
{-# INLINE sFindIndex #-}

{- | @'findIndices' p xs@ find all elements satisfying @p@ and returns their indices.

 Since 0.7.0.0
-}
findIndices ::
  forall f (n :: Nat) a.
  (CFoldable f, Dom f a) =>
  (a -> Bool) ->
  Sized f n a ->
  [Int]
findIndices :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> [Int]
findIndices = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> f a -> [Int]
cfindIndices @f @a
{-# INLINE findIndices #-}
{-# SPECIALIZE findIndices :: (a -> Bool) -> Sized [] n a -> [Int] #-}

{- | 'Ordinal' version of 'findIndices'.

 Since 0.7.0.0
-}
sFindIndices ::
  forall f (n :: Nat) a.
  (CFoldable f, Dom f a, KnownNat (n :: Nat)) =>
  (a -> Bool) ->
  Sized f n a ->
  [Ordinal n]
sFindIndices :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, KnownNat n) =>
(a -> Bool) -> Sized f n a -> [Ordinal n]
sFindIndices a -> Bool
p = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (forall a. Enum a => Int -> a
toEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
P.fromIntegral) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> [Int]
findIndices a -> Bool
p
{-# INLINE sFindIndices #-}

{-# RULES
"Foldable.sum/Vector"
  F.sum =
    V.sum . runSized
  #-}

{- | Returns the index of the given element in the list, if exists.

 Since 0.7.0.0
-}
elemIndex ::
  forall f (n :: Nat) a.
  (CFoldable f, Eq a, Dom f a) =>
  a ->
  Sized f n a ->
  Maybe Int
elemIndex :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Eq a, Dom f a) =>
a -> Sized f n a -> Maybe Int
elemIndex = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Dom f a, Eq a) =>
a -> f a -> Maybe Int
celemIndex @f @a
{-# INLINE elemIndex #-}

{- | Ordinal version of 'elemIndex'.
   Since 0.7.0.0, we no longer do boundary check inside the definition.

   Since 0.7.0.0
-}
sElemIndex
  , sUnsafeElemIndex ::
    forall f (n :: Nat) a.
    (KnownNat n, CFoldable f, Dom f a, Eq a) =>
    a ->
    Sized f n a ->
    Maybe (Ordinal n)
sElemIndex :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Maybe (Ordinal n)
sElemIndex = (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Enum a => Int -> a
toEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFoldable f, Dom f a, Eq a) =>
a -> f a -> Maybe Int
celemIndex @f @a)
{-# INLINE sElemIndex #-}

-- | Since 0.5.0.0 (type changed)
sUnsafeElemIndex :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Maybe (Ordinal n)
sUnsafeElemIndex = forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Maybe (Ordinal n)
sElemIndex
{-# DEPRECATED sUnsafeElemIndex "No difference with sElemIndex; use sElemIndex instead." #-}

{- | Returns all indices of the given element in the list.

 Since 0.7.0.0
-}
elemIndices ::
  forall f (n :: Nat) a.
  (CFoldable f, Dom f a, Eq a) =>
  a ->
  Sized f n a ->
  [Int]
elemIndices :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> [Int]
elemIndices = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Dom f a, Eq a) =>
a -> f a -> [Int]
celemIndices @f @a
{-# INLINE elemIndices #-}

{- | Ordinal version of 'elemIndices'

 Since 0.7.0.0
-}
sElemIndices ::
  forall f (n :: Nat) a.
  (CFoldable f, KnownNat (n :: Nat), Dom f a, Eq a) =>
  a ->
  Sized f n a ->
  [Ordinal n]
sElemIndices :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, KnownNat n, Dom f a, Eq a) =>
a -> Sized f n a -> [Ordinal n]
sElemIndices = (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Enum a => Int -> a
toEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> [Int]
elemIndices
{-# INLINE sElemIndices #-}

--------------------------------------------------------------------------------
-- 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 -> 'SNat' 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 -> 'SNat' 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
-}
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 5 :-

{- | Case analysis for the cons-side of sequence.

 Since 0.5.0.0 (type changed)
-}
viewCons ::
  forall f (n :: Nat) a.
  (KnownNat n, CFreeMonoid f, Dom f a) =>
  Sized f n a ->
  ConsView f n a
viewCons :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
Sized f n a -> ConsView f n a
viewCons Sized f n a
sz = case forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n of
  ZeroOrSucc n
IsZero -> forall (f :: Type -> Type) a. ConsView f 0 a
NilCV
  IsSucc SNat n1
n' ->
    forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n1
n' forall a b. (a -> b) -> a -> b
$
      forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (SNat 1
sOne forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n1
n') forall a b. (a -> b) -> a -> b
$
        case forall (f :: Type -> Type) (n :: Nat) a (proxy :: Nat -> Type).
(KnownNat n, CFreeMonoid f, Dom f a) =>
proxy n -> Sized f (Succ n) a -> Uncons f (Succ n) a
uncons' SNat n1
n' Sized f n a
sz of
          Uncons a
a Sized f n a
xs -> a
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
-}
data SnocView f n a where
  NilSV :: SnocView f (0) a
  (:-::) :: KnownNat (n :: Nat) => Sized f n a -> a -> SnocView f (n + 1) a

infixl 5 :-::

{- | Case analysis for the snoc-side of sequence.

 Since 0.5.0.0 (type changed)
-}
viewSnoc ::
  forall f (n :: Nat) a.
  (KnownNat n, CFreeMonoid f, Dom f a) =>
  Sized f n a ->
  SnocView f n a
viewSnoc :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
Sized f n a -> SnocView f n a
viewSnoc Sized f n a
sz = case forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc (forall (n :: Nat). KnownNat n => SNat n
sNat @n) of
  ZeroOrSucc n
IsZero -> forall (f :: Type -> Type) a. SnocView f 0 a
NilSV
  IsSucc (SNat n1
n' :: SNat n') ->
    forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n1
n' forall a b. (a -> b) -> a -> b
$
      case forall (f :: Type -> Type) (n :: Nat) a (proxy :: Nat -> Type).
(KnownNat n, CFreeMonoid f, Dom f a) =>
proxy n -> Sized f (Succ n) a -> Unsnoc f (Succ n) a
unsnoc' SNat n1
n' Sized f n a
sz of
        Unsnoc (Sized f n a
xs :: Sized f m a) a
a ->
          forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith
            (forall a b. a -> b
unsafeCoerce (forall {k} (a :: k). a :~: a
Refl @()) :: n' :~: m)
            forall a b. (a -> b) -> a -> b
$ Sized f n a
xs forall (n :: Nat) (f :: Type -> Type) a.
KnownNat n =>
Sized f n a -> a -> SnocView f (Succ n) a
:-:: a
a

{- $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, 'KnownNat' 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, 'KnownNat' n) => 'Sized' f ('S' ('S' n)) a -> a
nextToHead (_ ':<' a ':<' _) = a
@

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

@
slen :: ('KnownNat' n, 'Dom f a' f) => 'Sized' f n a -> 'SNat' 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>.
-}

infixr 5 :<

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

chkNil ::
  forall f (n :: Nat) a.
  (KnownNat n) =>
  Sized f n a ->
  ZeroOrSucc n
chkNil :: forall (f :: Type -> Type) (n :: Nat) a.
KnownNat n =>
Sized f n a -> ZeroOrSucc n
chkNil = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n

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

infixl 5 :>

-- | 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), KnownNat n1) =>
  Sized f n1 a ->
  a ->
  Sized f n a
pattern a $b:> :: forall (f :: Type -> Type) a (n :: Nat) (n1 :: Nat).
(Dom f a, KnownNat n, CFreeMonoid f, n ~ (n1 + 1), KnownNat n1) =>
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), KnownNat n1) =>
    Sized f n1 a -> a -> r)
-> ((# #) -> r)
-> r
:> b <-
  (viewSnoc -> a :-:: b)
  where
    Sized f n1 a
a :> a
b = Sized f n1 a
a forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + 1) a
|> a
b

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

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

class Dom f a => DomC f a

instance Dom f a => DomC f a

-- | Applicative instance, generalizing @'Data.Monoid.ZipList'@.
instance
  ( Functor f
  , CFreeMonoid f
  , CZip f
  , KnownNat n
  , forall a. DomC f a
  ) =>
  P.Applicative (Sized f (n :: Nat))
  where
  {-# SPECIALIZE instance KnownNat n => P.Applicative (Sized [] (n :: Nat)) #-}
  {-# SPECIALIZE instance KnownNat n => P.Applicative (Sized Seq.Seq (n :: Nat)) #-}
  {-# SPECIALIZE instance KnownNat n => P.Applicative (Sized V.Vector (n :: Nat)) #-}

  pure :: forall a. a -> Sized f n a
pure (a
x :: a) =
    forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: Constraint). a => Dict a
Dict @(DomC f a)) forall a b. (a -> b) -> a -> b
$
      forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> Sized f n a
replicate' a
x
  {-# INLINE pure #-}

  (Sized f n (a -> b)
fs :: Sized f n (a -> b)) <*> :: forall a b. Sized f n (a -> b) -> Sized f n a -> Sized f n b
<*> (Sized f n a
xs :: Sized f n a) =
    forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: Constraint). a => Dict a
Dict @(DomC f b)) forall a b. (a -> b) -> a -> b
$
      forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: Constraint). a => Dict a
Dict @(DomC f a)) forall a b. (a -> b) -> a -> b
$
        forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: Constraint). a => Dict a
Dict @(DomC f (a -> b))) forall a b. (a -> b) -> a -> b
$
          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
zipWithSame forall a b. (a -> b) -> a -> b
($) Sized f n (a -> b)
fs Sized f n a
xs
  {-# INLINE [1] (<*>) #-}

{-# RULES
"<*>/List" [~1] forall fs xs.
  Sized fs <*> Sized xs =
    Sized (getZipList (ZipList fs <*> ZipList xs))
"<*>/Seq" [~1] forall fs xs.
  Sized fs <*> Sized xs =
    Sized (Seq.zipWith ($) fs xs)
"<*>/Vector" [~1] forall fs xs.
  Sized fs <*> Sized xs =
    Sized (V.zipWith ($) fs xs)
  #-}

instance
  (CFreeMonoid f, KnownNat (n :: Nat)) =>
  CPointed (Sized f n)
  where
  cpure :: forall a. Dom (Sized f n) a => a -> Sized f n a
cpure = forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> Sized f n a
replicate'

instance
  (CFreeMonoid f, CZip f) =>
  CApplicative (Sized f n)
  where
  pair :: forall a b.
(Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (a, b)) =>
Sized f n a -> Sized f n b -> Sized f n (a, b)
pair = 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)
zipSame
  <.> :: forall a b.
(Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (a -> b)) =>
Sized f n (a -> b) -> Sized f n a -> Sized f n b
(<.>) = 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
zipWithSame forall a b. (a -> b) -> a -> b
($)
  <. :: forall a b.
(Dom (Sized f n) a, Dom (Sized f n) b) =>
Sized f n a -> Sized f n b -> Sized f n a
(<.) = forall a b. a -> b -> a
P.const
  .> :: forall a b.
(Dom (Sized f n) a, Dom (Sized f n) b) =>
Sized f n a -> Sized f n b -> Sized f n b
(.>) = forall a b c. (a -> b -> c) -> b -> a -> c
P.flip forall a b. a -> b -> a
P.const

{- | __N.B.__ Since @calign@ is just zipping for fixed @n@,
   we require more strong 'CZip' constraint here.
-}
instance (CZip f, CFreeMonoid f) => CSemialign (Sized f n) where
  calignWith :: forall a b c.
(Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) c) =>
(These a b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
calignWith =
    coerce :: forall a b. Coercible a b => a -> b
coerce (\These a b -> c
f -> forall (f :: Type -> Type) a b c.
(CZip f, Dom f a, Dom f b, Dom f c) =>
(a -> b -> c) -> f a -> f b -> f c
czipWith @f @a @b @c ((These a b -> c
f forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> These a b
These)) ::
      forall a b c.
      (Dom f a, Dom f b, Dom f c) =>
      (These a b -> c) ->
      Sized f n a ->
      Sized f n b ->
      Sized f n c
  {-# INLINE [1] calignWith #-}
  calign :: forall a b.
(Dom (Sized f n) a, Dom (Sized f n) b,
 Dom (Sized f n) (These a b)) =>
Sized f n a -> Sized f n b -> Sized f n (These a b)
calign =
    coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b c.
(CZip f, Dom f a, Dom f b, Dom f c) =>
(a -> b -> c) -> f a -> f b -> f c
czipWith @f @a @b forall a b. a -> b -> These a b
These ::
      forall a b.
      (Dom f a, Dom f b, Dom f (These a b)) =>
      Sized f n a ->
      Sized f n b ->
      Sized f n (These a b)
  {-# INLINE [1] calign #-}

instance (CZip f, CFreeMonoid f) => CZip (Sized f n) where
  czipWith :: forall a b c.
(Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) c) =>
(a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
czipWith =
    coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b c.
(CZip f, Dom f a, Dom f b, Dom f c) =>
(a -> b -> c) -> f a -> f b -> f c
czipWith @f @a @b @c ::
      forall a b c.
      (Dom f a, Dom f b, Dom f c) =>
      (a -> b -> c) ->
      Sized f n a ->
      Sized f n b ->
      Sized f n c
  {-# INLINE [1] czipWith #-}
  czip :: forall a b.
(Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (a, b)) =>
Sized f n a -> Sized f n b -> Sized f n (a, b)
czip =
    coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b.
(CZip f, Dom f a, Dom f b, Dom f (a, b)) =>
f a -> f b -> f (a, b)
czip @f @a @b ::
      forall a b.
      (Dom f a, Dom f b, Dom f (a, b)) =>
      Sized f n a ->
      Sized f n b ->
      Sized f n (a, b)
  {-# INLINE [1] czip #-}

instance
  (KnownNat (n :: Nat), CZip f, CFreeMonoid f) =>
  CRepeat (Sized f n)
  where
  crepeat :: forall a. Dom (Sized f n) a => a -> Sized f n a
crepeat = forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> Sized f n a
replicate'
  {-# INLINE [1] crepeat #-}

instance CTraversable f => CTraversable (Sized f n) where
  ctraverse :: forall a b (g :: Type -> Type).
(Dom (Sized f n) a, Dom (Sized f n) b, Applicative g) =>
(a -> g b) -> Sized f n a -> g (Sized f n b)
ctraverse = \a -> g b
f -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap coerce :: forall a b. Coercible a b => a -> b
coerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) a b (g :: Type -> Type).
(CTraversable f, Dom f a, Dom f b, Applicative g) =>
(a -> g b) -> f a -> g (f b)
ctraverse a -> g b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) (n :: Nat) a. Sized f n a -> f a
runSized
  {-# INLINE ctraverse #-}