{-# 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 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
9) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
      String -> ShowS
P.showString String
"SomeSized _ " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Sized f n a -> ShowS
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 f a -> f a -> Bool
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 :: Sized f n a -> Int
length = Int -> Sized f n a -> Int
forall a b. a -> b -> a
const (Int -> Sized f n a -> Int) -> Int -> Sized f n a -> Int
forall a b. (a -> b) -> a -> b
$ Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural (SNat n -> Natural) -> SNat n -> Natural
forall a b. (a -> b) -> a -> b
$ KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat @n
{-# INLINE CONLIKE [1] length #-}

lengthTLZero :: Sized f 0 a -> Int
lengthTLZero :: Sized f 0 a -> Int
lengthTLZero = Int -> Sized f 0 a -> Int
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 :: Sized f n a -> SNat n
sLength Sized f n a
_ = KnownNat n => SNat n
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 :: Sized f n a -> Bool
null = (f a -> Bool) -> Sized f n a -> Bool
coerce ((f a -> Bool) -> Sized f n a -> Bool)
-> (f a -> Bool) -> Sized f n a -> Bool
forall a b. (a -> b) -> a -> b
$ Dom f a => f a -> Bool
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 :: Sized f 0 a -> Bool
nullTL0 = Bool -> Sized f 0 a -> Bool
forall a b. a -> b -> a
P.const Bool
True
{-# INLINE nullTL0 #-}

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

nullTLSucc :: Sized f (n + 1) a -> Bool
nullTLSucc :: Sized f (n + 1) a -> Bool
nullTLSucc = Bool -> Sized f (n + 1) a -> Bool
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
!! :: 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
{-# 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
%!! :: Sized f n c -> Ordinal n -> c
(%!!) = (f c -> Ordinal n -> c) -> Sized f n c -> Ordinal n -> c
coerce ((f c -> Ordinal n -> c) -> Sized f n c -> Ordinal n -> c)
-> (f c -> Ordinal n -> c) -> Sized f n c -> Ordinal n -> c
forall a b. (a -> b) -> a -> b
$ ((Int -> c) -> (Ordinal n -> Int) -> Ordinal n -> c
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) -> (Ordinal n -> Natural) -> Ordinal n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ordinal n -> Natural
forall (n :: Nat). Ordinal n -> Natural
ordToNatural)) ((Int -> c) -> Ordinal n -> c)
-> (f c -> Int -> c) -> f c -> Ordinal n -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom f c => f c -> Int -> 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 :: 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
flip 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
(!!)
{-# 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 :: Ordinal n -> Sized f n c -> c
sIndex = (Sized f n c -> Ordinal n -> c) -> Ordinal n -> Sized f n c -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Sized f n c -> Ordinal n -> c) -> Ordinal n -> Sized f n c -> c)
-> (Sized f n c -> Ordinal n -> c) -> Ordinal n -> Sized f n c -> c
forall a b. (a -> b) -> a -> b
$ (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
(%!!) @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 :: 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
{-# 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 :: 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
{-# 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 :: Sized f n a -> Uncons f n a
uncons =
  SNat (n - 1)
-> (KnownNat (n - 1) => Sized f n a -> Uncons f n a)
-> Sized f n a
-> Uncons f n a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat
    (SNat n -> SNat (n - 1)
forall (n :: Nat). SNat n -> SNat (Pred n)
sPred (SNat n -> SNat (n - 1)) -> SNat n -> SNat (n - 1)
forall a b. (a -> b) -> a -> b
$ KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat @n)
    ((KnownNat (n - 1) => Sized f n a -> Uncons f n a)
 -> Sized f n a -> Uncons f n a)
-> (KnownNat (n - 1) => Sized f n a -> Uncons f n a)
-> Sized f n a
-> Uncons f n a
forall a b. (a -> b) -> a -> b
$ (a -> Sized f (n - 1) a -> Uncons f (1 + (n - 1)) a)
-> (a, Sized f (n - 1) a) -> Uncons f (1 + (n - 1)) a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (KnownNat (n - 1) =>
a -> Sized f (n - 1) a -> Uncons f (1 + (n - 1)) 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 (1 + (n - 1)) a)
-> (Sized f n a -> (a, Sized f (n - 1) a))
-> Sized f n a
-> Uncons f (1 + (n - 1)) 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' ::
  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' :: proxy n -> Sized f (Succ n) a -> Uncons f (Succ n) a
uncons' proxy n
_ =
  SNat (Succ n)
-> (KnownNat (Succ n) => Sized f (Succ n) a -> Uncons f (Succ n) a)
-> Sized f (Succ n) a
-> Uncons f (Succ n) a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (Succ n)) -> SNat n -> SNat (Succ n)
forall a b. (a -> b) -> a -> b
$ KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat @n) KnownNat (Succ n) => Sized f (Succ n) a -> Uncons f (Succ n) a
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 :: Sized f n a -> Unsnoc f n a
unsnoc =
  SNat (n - 1)
-> (KnownNat (n - 1) => Sized f n a -> Unsnoc f n a)
-> Sized f n a
-> Unsnoc f n a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat
    (SNat n -> SNat (n - 1)
forall (n :: Nat). SNat n -> SNat (Pred n)
sPred (SNat n -> SNat (n - 1)) -> SNat n -> SNat (n - 1)
forall a b. (a -> b) -> a -> b
$ KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat @n)
    ((KnownNat (n - 1) => Sized f n a -> Unsnoc f n a)
 -> Sized f n a -> Unsnoc f n a)
-> (KnownNat (n - 1) => Sized f n a -> Unsnoc f n a)
-> Sized f n a
-> Unsnoc f n a
forall a b. (a -> b) -> a -> b
$ (Sized f (n - 1) a -> a -> Unsnoc f ((n - 1) + 1) a)
-> (Sized f (n - 1) a, a) -> Unsnoc f ((n - 1) + 1) a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall a. Sized f (n - 1) a -> a -> Unsnoc f ((n - 1) + 1) a
forall (f :: Type -> Type) (n :: Nat) a.
Sized f n a -> a -> Unsnoc f (Succ n) a
Unsnoc @f @(Pred n)) ((Sized f (n - 1) a, a) -> Unsnoc f ((n - 1) + 1) a)
-> (Sized f n a -> (Sized f (n - 1) a, a))
-> Sized f n a
-> Unsnoc f ((n - 1) + 1) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a -> (f a, a)) -> Sized f n a -> (Sized f (n - 1) a, a)
coerce (Maybe (f a, a) -> (f a, a)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (f a, a) -> (f a, a))
-> (f a -> Maybe (f a, a)) -> f a -> (f a, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom f a => f a -> Maybe (f a, a)
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' :: proxy n -> Sized f (Succ n) a -> Unsnoc f (Succ n) a
unsnoc' proxy n
_ =
  SNat (Succ n)
-> (KnownNat (Succ n) => Sized f (Succ n) a -> Unsnoc f (Succ n) a)
-> Sized f (Succ n) a
-> Unsnoc f (Succ n) a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (SNat n -> SNat (Succ n)
forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc (SNat n -> SNat (Succ n)) -> SNat n -> SNat (Succ n)
forall a b. (a -> b) -> a -> b
$ KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat @n) KnownNat (Succ n) => Sized f (Succ n) a -> Unsnoc f (Succ n) a
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 :: Sized f (1 + n) a -> Sized f n a
tail = (f a -> f a) -> Sized f (1 + n) a -> Sized f n a
coerce ((f a -> f a) -> Sized f (1 + n) a -> Sized f n a)
-> (f a -> f a) -> Sized f (1 + n) a -> Sized f n a
forall a b. (a -> b) -> a -> b
$ Dom f a => f a -> f a
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 :: Sized f (n + 1) a -> Sized f n a
init = (f a -> f a) -> Sized f (n + 1) a -> Sized f n a
coerce ((f a -> f a) -> Sized f (n + 1) a -> Sized f n a)
-> (f a -> f a) -> Sized f (n + 1) a -> Sized f n a
forall a b. (a -> b) -> a -> b
$ Dom f a => f a -> f a
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 :: 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
. SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
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 :: SNat n -> Sized f m a -> Sized f (Min n m) a
takeAtMost = (SNat n -> f a -> f a)
-> SNat n -> Sized f m a -> Sized f (Min n m) a
coerce ((SNat n -> f a -> f a)
 -> SNat n -> Sized f m a -> Sized f (Min n m) a)
-> (SNat n -> f a -> f a)
-> SNat n
-> Sized f m a
-> Sized f (Min n m) 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
. SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
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 :: 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
. SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
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 :: 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
. SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
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 :: SNat n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a)
splitAtMost =
  (SNat n -> f a -> (f a, f a))
-> SNat n
-> Sized f m a
-> (Sized f (Min n m) a, Sized f (m -. n) a)
coerce ((SNat n -> f a -> (f a, f a))
 -> SNat n
 -> Sized f m a
 -> (Sized f (Min n m) a, Sized f (m -. n) a))
-> (SNat n -> f a -> (f a, f a))
-> SNat n
-> Sized f m a
-> (Sized f (Min n m) 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
. SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
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 :: Sized f 0 a
empty = f a -> Sized f 0 a
coerce (f a -> Sized f 0 a) -> f a -> Sized f 0 a
forall a b. (a -> b) -> a -> b
$ Monoid (f a) => f a
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 :: a -> Sized f 1 a
singleton = (a -> f a) -> a -> Sized f 1 a
coerce ((a -> f a) -> a -> Sized f 1 a) -> (a -> f a) -> a -> Sized f 1 a
forall a b. (a -> b) -> a -> b
$ Dom f a => a -> f a
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 :: f a -> SomeSized f a
toSomeSized = \f a
xs ->
  case Natural -> SomeSNat
toSomeSNat (Natural -> SomeSNat) -> Natural -> SomeSNat
forall a b. (a -> b) -> a -> b
$ Int -> Natural
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Int -> Natural) -> Int -> Natural
forall a b. (a -> b) -> a -> b
$ f a -> Int
forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> Int
clength f a
xs of
    SomeSNat SNat n
sn -> SNat n -> (KnownNat n => SomeSized f a) -> SomeSized f a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn ((KnownNat n => SomeSized f a) -> SomeSized f a)
-> (KnownNat n => SomeSized f a) -> SomeSized f a
forall a b. (a -> b) -> a -> b
$ SNat n -> Sized f n a -> SomeSized f a
forall (n :: Nat) (f :: Type -> Type) a.
SNat n -> Sized f n a -> SomeSized f a
SomeSized SNat n
sn (Sized f n a -> SomeSized f a) -> Sized f n a -> SomeSized f a
forall a b. (a -> b) -> a -> b
$ SNat n -> f a -> Sized f n a
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 :: SNat n -> a -> Sized f n a
replicate = (SNat n -> a -> f a) -> SNat n -> a -> Sized f n a
coerce ((SNat n -> a -> f a) -> SNat n -> a -> Sized f n a)
-> (SNat n -> a -> f a) -> SNat n -> a -> Sized f n a
forall a b. (a -> b) -> a -> b
$ Dom f a => Int -> a -> f a
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> a -> f a
creplicate @f @a (Int -> a -> f a) -> (SNat n -> Int) -> SNat n -> 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
. SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
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' :: a -> Sized f n a
replicate' = SNat n -> a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> Sized f n a
replicate (KnownNat n => SNat n
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 :: SNat n -> (Ordinal n -> a) -> Sized f n a
generate = (SNat n -> (Ordinal n -> a) -> f a)
-> SNat n -> (Ordinal n -> a) -> Sized f n a
coerce ((SNat n -> (Ordinal n -> a) -> f a)
 -> SNat n -> (Ordinal n -> a) -> Sized f n a)
-> (SNat n -> (Ordinal n -> a) -> f a)
-> SNat n
-> (Ordinal n -> a)
-> Sized f n a
forall a b. (a -> b) -> a -> b
$ \SNat n
sn ->
  SNat n
-> (KnownNat n => (Ordinal n -> a) -> f a)
-> (Ordinal n -> a)
-> f a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn ((KnownNat n => (Ordinal n -> a) -> f a)
 -> (Ordinal n -> a) -> f a)
-> (KnownNat n => (Ordinal n -> a) -> f a)
-> (Ordinal n -> a)
-> f a
forall a b. (a -> b) -> a -> b
$
    Int -> (Int -> a) -> f a
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> (Int -> a) -> f a
cgenerate @f @a (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural @n SNat n
sn)
      ((Int -> a) -> f a)
-> ((Ordinal n -> a) -> Int -> a) -> (Ordinal n -> a) -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Ordinal n -> a) -> (Int -> Ordinal n) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Enum (Ordinal n) => Int -> Ordinal n
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' :: (Ordinal n -> a) -> Sized f n a
generate' = SNat n -> (Ordinal n -> a) -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> (Ordinal n -> a) -> Sized f n a
generate SNat n
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 :: SNat n -> (Ordinal n -> a) -> Sized Vector n a
genVector SNat n
n Ordinal n -> a
f = SNat n -> (KnownNat n => Sized Vector n a) -> Sized Vector n a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n ((KnownNat n => Sized Vector n a) -> Sized Vector n a)
-> (KnownNat n => Sized Vector n a) -> Sized Vector n a
forall a b. (a -> b) -> a -> b
$ Vector a -> Sized Vector n a
forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized (Vector a -> Sized Vector n a) -> Vector a -> Sized Vector n a
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> a) -> Vector a
forall a. Int -> (Int -> a) -> Vector a
V.generate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural SNat n
n) (Ordinal n -> a
f (Ordinal n -> a) -> (Int -> Ordinal n) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Ordinal n
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 :: SNat n -> (Ordinal n -> a) -> Sized Vector n a
genSVector SNat n
n Ordinal n -> a
f = SNat n -> (KnownNat n => Sized Vector n a) -> Sized Vector n a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n ((KnownNat n => Sized Vector n a) -> Sized Vector n a)
-> (KnownNat n => Sized Vector n a) -> Sized Vector n a
forall a b. (a -> b) -> a -> b
$ Vector a -> Sized Vector n a
forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized (Vector a -> Sized Vector n a) -> Vector a -> Sized Vector n a
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> a) -> Vector a
forall a. Storable a => Int -> (Int -> a) -> Vector a
SV.generate (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural SNat n
n) (Ordinal n -> a
f (Ordinal n -> a) -> (Int -> Ordinal n) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Ordinal n
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 :: SNat n -> (Ordinal n -> a) -> Sized Seq n a
genSeq SNat n
n Ordinal n -> a
f = SNat n -> (KnownNat n => Sized Seq n a) -> Sized Seq n a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n ((KnownNat n => Sized Seq n a) -> Sized Seq n a)
-> (KnownNat n => Sized Seq n a) -> Sized Seq n a
forall a b. (a -> b) -> a -> b
$ Seq a -> Sized Seq n a
forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized (Seq a -> Sized Seq n a) -> Seq a -> Sized Seq n a
forall a b. (a -> b) -> a -> b
$ Int -> (Int -> a) -> Seq a
forall a. Int -> (Int -> a) -> Seq a
Seq.fromFunction (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural SNat n
n) (Ordinal n -> a
f (Ordinal n -> a) -> (Int -> Ordinal n) -> Int -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Ordinal n
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 :: a -> Sized f n a -> Sized f (1 + n) a
cons = (a -> f a -> f a) -> a -> Sized f n a -> Sized f (1 + n) a
coerce ((a -> f a -> f a) -> a -> Sized f n a -> Sized f (1 + n) a)
-> (a -> f a -> f a) -> a -> Sized f n a -> Sized f (1 + n) a
forall a b. (a -> b) -> a -> b
$ Dom f a => a -> f a -> f a
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
<| :: a -> Sized f n a -> Sized f (1 + n) 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 :: Sized f n a -> a -> Sized f (n + 1) a
snoc (Sized f a
xs) a
a = f a -> Sized f (n + 1) a
forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized (f a -> Sized f (n + 1) a) -> f a -> Sized f (n + 1) a
forall a b. (a -> b) -> a -> b
$ f a -> a -> f a
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
|> :: Sized f n a -> a -> Sized f (n + 1) 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 :: Sized f n a -> Sized f m a -> Sized f (n + m) a
append = (f a -> f a -> f a)
-> Sized f n a -> Sized f m a -> Sized f (n + m) a
coerce ((f a -> f a -> f a)
 -> Sized f n a -> Sized f m a -> Sized f (n + m) a)
-> (f a -> f a -> f a)
-> Sized f n a
-> Sized f m a
-> Sized f (n + m) a
forall a b. (a -> b) -> a -> b
$ Monoid (f a) => f a -> f a -> f a
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
++ :: Sized f n a -> Sized f m a -> Sized f (n + m) a
(++) = Sized f n a -> Sized f m a -> Sized f (n + m) a
forall (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 :: Sized f' m (Sized f n a) -> Sized f (m * n) a
concat = (f' (Sized f n a) -> f a)
-> Sized f' m (Sized f n a) -> Sized f (m * n) a
coerce ((f' (Sized f n a) -> f a)
 -> Sized f' m (Sized f n a) -> Sized f (m * n) a)
-> (f' (Sized f n a) -> f a)
-> Sized f' m (Sized f n a)
-> Sized f (m * n) a
forall a b. (a -> b) -> a -> b
$ (Sized f n a -> f a) -> f' (Sized f n a) -> f a
forall (f :: Type -> Type) a w.
(CFoldable f, Dom f a, Monoid w) =>
(a -> w) -> f a -> w
cfoldMap @f' @(Sized f n a) Sized f n a -> f 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 :: Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)
zip = (f a -> f b -> f (a, b))
-> Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)
coerce ((f a -> f b -> f (a, b))
 -> Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b))
-> (f a -> f b -> f (a, b))
-> Sized f n a
-> Sized f m b
-> Sized f (Min n m) (a, b)
forall a b. (a -> b) -> a -> b
$ (Dom f a, Dom f b, Dom f (a, b)) => f a -> f b -> f (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 :: Sized f n a -> Sized f n b -> Sized f n (a, b)
zipSame = (f a -> f b -> f (a, b))
-> Sized f n a -> Sized f n b -> Sized f n (a, b)
coerce ((f a -> f b -> f (a, b))
 -> Sized f n a -> Sized f n b -> Sized f n (a, b))
-> (f a -> f b -> f (a, b))
-> Sized f n a
-> Sized f n b
-> Sized f n (a, b)
forall a b. (a -> b) -> a -> b
$ (Dom f a, Dom f b, Dom f (a, b)) => f a -> f b -> f (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 :: (a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c
zipWith = ((a -> b -> c) -> f a -> f b -> f c)
-> (a -> b -> c)
-> Sized f n a
-> Sized f m b
-> Sized f (Min n m) c
coerce (((a -> b -> c) -> f a -> f b -> f c)
 -> (a -> b -> c)
 -> Sized f n a
 -> Sized f m b
 -> Sized f (Min n m) c)
-> ((a -> b -> c) -> f a -> f b -> f c)
-> (a -> b -> c)
-> Sized f n a
-> Sized f m b
-> Sized f (Min n m) c
forall a b. (a -> b) -> a -> b
$ (Dom f a, Dom f b, Dom f c) => (a -> b -> c) -> f a -> f b -> f c
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 :: (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
zipWithSame = ((a -> b -> c) -> f a -> f b -> f c)
-> (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
coerce (((a -> b -> c) -> f a -> f b -> f c)
 -> (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c)
-> ((a -> b -> c) -> f a -> f b -> f c)
-> (a -> b -> c)
-> Sized f n a
-> Sized f n b
-> Sized f n c
forall a b. (a -> b) -> a -> b
$ (Dom f a, Dom f b, Dom f c) => (a -> b -> c) -> f a -> f b -> f c
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 :: Sized f n (a, b) -> (Sized f n a, Sized f n b)
unzip = (f (a, b) -> (f a, f b))
-> Sized f n (a, b) -> (Sized f n a, Sized f n b)
coerce ((f (a, b) -> (f a, f b))
 -> Sized f n (a, b) -> (Sized f n a, Sized f n b))
-> (f (a, b) -> (f a, f b))
-> Sized f n (a, b)
-> (Sized f n a, Sized f n b)
forall a b. (a -> b) -> a -> b
$ (Dom f (a, b), Dom f a, Dom f b) => f (a, b) -> (f a, f 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 :: (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c)
unzipWith = ((a -> (b, c)) -> f a -> (f b, f c))
-> (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c)
coerce (((a -> (b, c)) -> f a -> (f b, f c))
 -> (a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c))
-> ((a -> (b, c)) -> f a -> (f b, f c))
-> (a -> (b, c))
-> Sized f n a
-> (Sized f n b, Sized f n c)
forall a b. (a -> b) -> a -> b
$ (Dom f a, Dom f b, Dom f c) => (a -> (b, c)) -> f a -> (f b, f c)
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 :: (a -> b) -> Sized f n a -> Sized f n b
map a -> b
f = f b -> Sized f n b
forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized (f b -> Sized f n b)
-> (Sized f n a -> f b) -> Sized f n a -> Sized f n b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b.
(CFunctor f, Dom f a, Dom f b) =>
(a -> b) -> f a -> f b
cmap a -> b
f (f a -> f b) -> (Sized f n a -> f a) -> Sized f n a -> f b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized f n a -> f a
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 :: Sized f n a -> Sized f n a
reverse = (f a -> f a) -> Sized f n a -> Sized f n a
coerce ((f a -> f a) -> Sized f n a -> Sized f n a)
-> (f a -> f a) -> Sized f n a -> Sized f n a
forall a b. (a -> b) -> a -> b
$ Dom f a => f a -> f a
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 :: a -> Sized f n a -> Sized f ((2 * n) -. 1) a
intersperse = (a -> f a -> f a) -> a -> Sized f n a -> Sized f ((2 * n) -. 1) a
coerce ((a -> f a -> f a) -> a -> Sized f n a -> Sized f ((2 * n) -. 1) a)
-> (a -> f a -> f a)
-> a
-> Sized f n a
-> Sized f ((2 * n) -. 1) a
forall a b. (a -> b) -> a -> b
$ Dom f a => a -> f a -> f a
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 :: Sized f n a -> SomeSized f a
nub = f a -> SomeSized f a
forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized (f a -> SomeSized f a)
-> (Sized f n a -> f a) -> Sized f n a -> SomeSized f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a -> f a) -> Sized f n a -> f a
coerce ((Dom f a, Eq a) => f a -> f a
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 :: Sized f n a -> Sized f n a
sort = (f a -> f a) -> Sized f n a -> Sized f n a
coerce ((f a -> f a) -> Sized f n a -> Sized f n a)
-> (f a -> f a) -> Sized f n a -> Sized f n a
forall a b. (a -> b) -> a -> b
$ (Dom f a, Ord a) => f a -> f a
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 :: (a -> a -> Ordering) -> Sized f n a -> Sized f n a
sortBy = ((a -> a -> Ordering) -> f a -> f a)
-> (a -> a -> Ordering) -> Sized f n a -> Sized f n a
coerce (((a -> a -> Ordering) -> f a -> f a)
 -> (a -> a -> Ordering) -> Sized f n a -> Sized f n a)
-> ((a -> a -> Ordering) -> f a -> f a)
-> (a -> a -> Ordering)
-> Sized f n a
-> Sized f n a
forall a b. (a -> b) -> a -> b
$ Dom f a => (a -> a -> Ordering) -> f a -> f a
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 :: a -> Sized f n a -> Sized f (Succ n) a
insert = (a -> f a -> f a) -> a -> Sized f n a -> Sized f (Succ n) a
coerce ((a -> f a -> f a) -> a -> Sized f n a -> Sized f (Succ n) a)
-> (a -> f a -> f a) -> a -> Sized f n a -> Sized f (Succ n) a
forall a b. (a -> b) -> a -> b
$ (Dom f a, Ord a) => a -> f a -> f a
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 :: (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a
insertBy = ((a -> a -> Ordering) -> a -> f a -> f a)
-> (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a
coerce (((a -> a -> Ordering) -> a -> f a -> f a)
 -> (a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a)
-> ((a -> a -> Ordering) -> a -> f a -> f a)
-> (a -> a -> Ordering)
-> a
-> Sized f n a
-> Sized f (Succ n) a
forall a b. (a -> b) -> a -> b
$ Dom f a => (a -> a -> Ordering) -> a -> f a -> f a
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 :: Sized f n a -> [a]
toList = (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
$ (CFoldable f, Dom f a) => f a -> [a]
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 :: SNat n -> [a] -> Maybe (Sized f n a)
fromList SNat n
Zero [a]
_ = Sized f n a -> Maybe (Sized f n a)
forall a. a -> Maybe a
Just (Sized f n a -> Maybe (Sized f n a))
-> Sized f n a -> Maybe (Sized f n a)
forall a b. (a -> b) -> a -> b
$ f a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized (f a
forall a. Monoid a => a
mempty :: f a)
fromList SNat n
sn [a]
xs =
  let len :: Int
len = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural SNat n
sn
   in if [a] -> Int
forall (t :: Type -> Type) a. Foldable t => t a -> Int
P.length [a]
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
len
        then Maybe (Sized f n a)
forall a. Maybe a
Nothing
        else Sized f n a -> Maybe (Sized f n a)
forall a. a -> Maybe a
Just (Sized f n a -> Maybe (Sized f n a))
-> Sized f n a -> Maybe (Sized f n a)
forall a b. (a -> b) -> a -> b
$ f a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized (f a -> Sized f n a) -> f a -> Sized f n a
forall a b. (a -> b) -> a -> b
$ Int -> f a -> f a
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake Int
len (f a -> f a) -> f a -> f a
forall a b. (a -> b) -> a -> b
$ [a] -> f a
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' :: [a] -> Maybe (Sized f n a)
fromList' = SNat n -> [a] -> Maybe (Sized f n a)
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> [a] -> Maybe (Sized f n a)
fromList SNat n
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 :: SNat n -> [a] -> Sized f n a
unsafeFromList = ([a] -> Sized f n a) -> SNat n -> [a] -> Sized f n a
forall a b. a -> b -> a
const (([a] -> Sized f n a) -> SNat n -> [a] -> Sized f n a)
-> ([a] -> Sized f n a) -> SNat n -> [a] -> Sized f n a
forall a b. (a -> b) -> a -> b
$ ([a] -> f a) -> [a] -> Sized f n a
coerce (([a] -> f a) -> [a] -> Sized f n a)
-> ([a] -> f a) -> [a] -> Sized f n a
forall a b. (a -> b) -> a -> b
$ (CFreeMonoid f, Dom f a) => [a] -> f a
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' :: [a] -> Sized f n a
unsafeFromList' = SNat n -> [a] -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> [a] -> Sized f n a
unsafeFromList SNat n
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 :: SNat n -> a -> [a] -> Sized f n a
fromListWithDefault SNat n
sn a
def [a]
xs =
  let len :: Int
len = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural SNat n
sn
   in f a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized (f a -> Sized f n a) -> f a -> Sized f n a
forall a b. (a -> b) -> a -> b
$
        [a] -> f a
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
[a] -> f a
cfromList (Int -> [a] -> [a]
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake Int
len [a]
xs)
          f a -> f a -> f a
forall a. Semigroup a => a -> a -> a
<> Int -> a -> f a
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> a -> f a
creplicate (Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- [a] -> Int
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' :: a -> [a] -> Sized f n a
fromListWithDefault' = SNat n -> a -> [a] -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
SNat n -> a -> [a] -> Sized f n a
fromListWithDefault SNat n
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 :: Sized f n a -> f a
unsized = Sized f n a -> f a
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 :: SNat n -> f a -> Maybe (Sized f n a)
toSized SNat n
sn f a
xs =
  let len :: Int
len = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural SNat n
sn
   in if f a -> Int
forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> Int
clength f a
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
len
        then Maybe (Sized f n a)
forall a. Maybe a
Nothing
        else Sized f n a -> Maybe (Sized f n a)
forall a. a -> Maybe a
Just (Sized f n a -> Maybe (Sized f n a))
-> Sized f n a -> Maybe (Sized f n a)
forall a b. (a -> b) -> a -> b
$ SNat n -> f a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
SNat n -> f a -> Sized f n a
unsafeToSized SNat n
sn (f a -> Sized f n a) -> f a -> Sized f n a
forall a b. (a -> b) -> a -> b
$ Int -> f a -> f a
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' :: f a -> Maybe (Sized f n a)
toSized' = SNat n -> f a -> Maybe (Sized f n a)
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> f a -> Maybe (Sized f n a)
toSized SNat n
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 :: SNat n -> f a -> Sized f n a
unsafeToSized SNat n
_ = f a -> Sized f n a
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' :: f a -> Sized f n a
unsafeToSized' = SNat n -> f a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
SNat n -> f a -> Sized f n a
unsafeToSized SNat n
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 :: SNat n -> a -> f a -> Sized f n a
toSizedWithDefault SNat n
sn a
def f a
xs =
  let len :: Int
len = Natural -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ SNat n -> Natural
forall (n :: Nat). SNat n -> Natural
toNatural SNat n
sn
   in f a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized (f a -> Sized f n a) -> f a -> Sized f n a
forall a b. (a -> b) -> a -> b
$ Int -> f a -> f a
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake Int
len f a
xs f a -> f a -> f a
forall a. Semigroup a => a -> a -> a
<> Int -> a -> f a
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> a -> f a
creplicate (Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- f a -> Int
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' :: a -> f a -> Sized f n a
toSizedWithDefault' = SNat n -> a -> f a -> Sized f n a
forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> f a -> Sized f n a
toSizedWithDefault SNat n
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 :: (a -> Bool) -> Sized f n a -> SomeSized f a
takeWhile = (f a -> SomeSized f a
forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized (f a -> SomeSized f a)
-> (Sized f n a -> f a) -> Sized f n a -> SomeSized f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Sized f n a -> f a) -> Sized f n a -> SomeSized f a)
-> ((a -> Bool) -> Sized f n a -> f a)
-> (a -> Bool)
-> Sized f n a
-> SomeSized f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a -> Bool) -> f a -> f a) -> (a -> Bool) -> Sized f n a -> f a
coerce (Dom f a => (a -> Bool) -> f a -> f a
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 :: (a -> Bool) -> Sized f n a -> SomeSized f a
dropWhile = (f a -> SomeSized f a
forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized (f a -> SomeSized f a)
-> (Sized f n a -> f a) -> Sized f n a -> SomeSized f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Sized f n a -> f a) -> Sized f n a -> SomeSized f a)
-> ((a -> Bool) -> Sized f n a -> f a)
-> (a -> Bool)
-> Sized f n a
-> SomeSized f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a -> Bool) -> f a -> f a) -> (a -> Bool) -> Sized f n a -> f a
coerce (Dom f a => (a -> Bool) -> f a -> f a
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 :: (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
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned @n ((f a, f a) -> Partitioned f n a)
-> (Sized f n a -> (f a, f a)) -> Sized f n a -> Partitioned f n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Sized f n a -> (f a, f a)) -> Sized f n a -> Partitioned f n a)
-> ((a -> Bool) -> Sized f n a -> (f a, f a))
-> (a -> Bool)
-> Sized f n a
-> Partitioned f n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a -> Bool) -> f a -> (f a, f a))
-> (a -> Bool) -> Sized f n a -> (f a, f a)
coerce (Dom f a => (a -> Bool) -> f a -> (f a, f a)
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 :: (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
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned @n ((f a, f a) -> Partitioned f n a)
-> (Sized f n a -> (f a, f a)) -> Sized f n a -> Partitioned f n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Sized f n a -> (f a, f a)) -> Sized f n a -> Partitioned f n a)
-> ((a -> Bool) -> Sized f n a -> (f a, f a))
-> (a -> Bool)
-> Sized f n a
-> Partitioned f n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a -> Bool) -> f a -> (f a, f a))
-> (a -> Bool) -> Sized f n a -> (f a, f a)
coerce (Dom f a => (a -> Bool) -> f a -> (f a, f a)
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 :: (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
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned @n ((f a, f a) -> Partitioned f n a)
-> (Sized f n a -> (f a, f a)) -> Sized f n a -> Partitioned f n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Sized f n a -> (f a, f a)) -> Sized f n a -> Partitioned f n a)
-> ((a -> Bool) -> Sized f n a -> (f a, f a))
-> (a -> Bool)
-> Sized f n a
-> Partitioned f n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a -> Bool) -> f a -> (f a, f a))
-> (a -> Bool) -> Sized f n a -> (f a, f a)
coerce (Dom f a => (a -> Bool) -> f a -> (f a, f a)
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 :: (f a, f a) -> Partitioned f n a
unsafePartitioned (f a
l, f a
r) =
  case (f a -> SomeSized f a
forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized f a
l, f a -> SomeSized f a
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
      ) ->
        (n :~: (n + n))
-> ((n ~ (n + n)) => Partitioned f n a) -> Partitioned f n a
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith
          ( (() :~: ()) -> n :~: (n + n)
forall a b. a -> b
unsafeCoerce ((() :~: ()) -> n :~: (n + n)) -> (() :~: ()) -> n :~: (n + n)
forall a b. (a -> b) -> a -> b
$ () :~: ()
forall k (a :: k). a :~: a
Refl @() ::
              n :~: nl + nr
          )
          (((n ~ (n + n)) => Partitioned f n a) -> Partitioned f n a)
-> ((n ~ (n + n)) => Partitioned f n a) -> Partitioned f n a
forall a b. (a -> b) -> a -> b
$ SNat n
-> Sized f n a -> SNat n -> Sized f n a -> Partitioned f (n + n) a
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 :: a -> Sized f n a -> Bool
elem = (a -> f a -> Bool) -> a -> Sized f n a -> Bool
coerce ((a -> f a -> Bool) -> a -> Sized f n a -> Bool)
-> (a -> f a -> Bool) -> a -> Sized f n a -> Bool
forall a b. (a -> b) -> a -> b
$ (Eq a, Dom f a) => a -> f a -> Bool
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 :: a -> Sized f n a -> Bool
notElem = (a -> f a -> Bool) -> a -> Sized f n a -> Bool
coerce ((a -> f a -> Bool) -> a -> Sized f n a -> Bool)
-> (a -> f a -> Bool) -> a -> Sized f n a -> Bool
forall a b. (a -> b) -> a -> b
$ (Eq a, Dom f a) => a -> f a -> Bool
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 :: (a -> Bool) -> Sized f n a -> Maybe a
find = ((a -> Bool) -> f a -> Maybe a)
-> (a -> Bool) -> Sized f n a -> Maybe a
coerce (((a -> Bool) -> f a -> Maybe a)
 -> (a -> Bool) -> Sized f n a -> Maybe a)
-> ((a -> Bool) -> f a -> Maybe a)
-> (a -> Bool)
-> Sized f n a
-> Maybe a
forall a b. (a -> b) -> a -> b
$ Dom f a => (a -> Bool) -> f a -> Maybe a
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 :: (a -> Bool) -> Sized f n a -> Maybe Int
findIndex = ((a -> Bool) -> f a -> Maybe Int)
-> (a -> Bool) -> Sized f n a -> Maybe Int
coerce (((a -> Bool) -> f a -> Maybe Int)
 -> (a -> Bool) -> Sized f n a -> Maybe Int)
-> ((a -> Bool) -> f a -> Maybe Int)
-> (a -> Bool)
-> Sized f n a
-> Maybe Int
forall a b. (a -> b) -> a -> b
$ Dom f a => (a -> Bool) -> f a -> Maybe Int
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 :: (a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
sFindIndex = ((Int -> Ordinal n) -> Maybe Int -> Maybe (Ordinal n)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Ordinal n
forall a. Enum a => Int -> a
toEnum (Maybe Int -> Maybe (Ordinal n))
-> (Sized f n a -> Maybe Int) -> Sized f n a -> Maybe (Ordinal n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Sized f n a -> Maybe Int) -> Sized f n a -> Maybe (Ordinal n))
-> ((a -> Bool) -> Sized f n a -> Maybe Int)
-> (a -> Bool)
-> Sized f n a
-> Maybe (Ordinal n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a -> Bool) -> f a -> Maybe Int)
-> (a -> Bool) -> Sized f n a -> Maybe Int
coerce (Dom f a => (a -> Bool) -> f a -> Maybe Int
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 :: (a -> Bool) -> Sized f n a -> [Int]
findIndices = ((a -> Bool) -> f a -> [Int])
-> (a -> Bool) -> Sized f n a -> [Int]
coerce (((a -> Bool) -> f a -> [Int])
 -> (a -> Bool) -> Sized f n a -> [Int])
-> ((a -> Bool) -> f a -> [Int])
-> (a -> Bool)
-> Sized f n a
-> [Int]
forall a b. (a -> b) -> a -> b
$ Dom f a => (a -> Bool) -> f a -> [Int]
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 :: (a -> Bool) -> Sized f n a -> [Ordinal n]
sFindIndices a -> Bool
p = (Int -> Ordinal n) -> [Int] -> [Ordinal n]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (Int -> Ordinal n
forall a. Enum a => Int -> a
toEnum (Int -> Ordinal n) -> (Int -> Int) -> Int -> Ordinal n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int
forall a b. (Integral a, Num b) => a -> b
P.fromIntegral) ([Int] -> [Ordinal n])
-> (Sized f n a -> [Int]) -> Sized f n a -> [Ordinal n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (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]
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 :: a -> Sized f n a -> Maybe Int
elemIndex = (a -> f a -> Maybe Int) -> a -> Sized f n a -> Maybe Int
coerce ((a -> f a -> Maybe Int) -> a -> Sized f n a -> Maybe Int)
-> (a -> f a -> Maybe Int) -> a -> Sized f n a -> Maybe Int
forall a b. (a -> b) -> a -> b
$ (Dom f a, Eq a) => a -> f a -> Maybe Int
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 :: a -> Sized f n a -> Maybe (Ordinal n)
sElemIndex = ((Int -> Ordinal n) -> Maybe Int -> Maybe (Ordinal n)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Ordinal n
forall a. Enum a => Int -> a
toEnum (Maybe Int -> Maybe (Ordinal n))
-> (Sized f n a -> Maybe Int) -> Sized f n a -> Maybe (Ordinal n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Sized f n a -> Maybe Int) -> Sized f n a -> Maybe (Ordinal n))
-> (a -> Sized f n a -> Maybe Int)
-> a
-> Sized f n a
-> Maybe (Ordinal n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> f a -> Maybe Int) -> a -> Sized f n a -> Maybe Int
coerce ((Dom f a, Eq a) => a -> f a -> Maybe Int
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 :: a -> Sized f n a -> Maybe (Ordinal n)
sUnsafeElemIndex = a -> Sized f n a -> Maybe (Ordinal n)
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 :: a -> Sized f n a -> [Int]
elemIndices = (a -> f a -> [Int]) -> a -> Sized f n a -> [Int]
coerce ((a -> f a -> [Int]) -> a -> Sized f n a -> [Int])
-> (a -> f a -> [Int]) -> a -> Sized f n a -> [Int]
forall a b. (a -> b) -> a -> b
$ (Dom f a, Eq a) => a -> f a -> [Int]
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 :: a -> Sized f n a -> [Ordinal n]
sElemIndices = ((Int -> Ordinal n) -> [Int] -> [Ordinal n]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Ordinal n
forall a. Enum a => Int -> a
toEnum ([Int] -> [Ordinal n])
-> (Sized f n a -> [Int]) -> Sized f n a -> [Ordinal n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Sized f n a -> [Int]) -> Sized f n a -> [Ordinal n])
-> (a -> Sized f n a -> [Int]) -> a -> Sized f n a -> [Ordinal n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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]
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 :: Sized f n a -> ConsView f n a
viewCons Sized f n a
sz = case SNat n -> ZeroOrSucc n
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc (SNat n -> ZeroOrSucc n) -> SNat n -> ZeroOrSucc n
forall a b. (a -> b) -> a -> b
$ KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat @n of
  ZeroOrSucc n
IsZero -> ConsView f n a
forall (f :: Type -> Type) a. ConsView f 0 a
NilCV
  IsSucc SNat n1
n' ->
    SNat n1 -> (KnownNat n1 => ConsView f n a) -> ConsView f n a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat 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
$
      SNat (1 + n1)
-> (KnownNat (1 + n1) => ConsView f n a) -> ConsView f n a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (SNat 1
sOne SNat 1 -> SNat n1 -> SNat (1 + n1)
forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat 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 SNat n1 -> Sized f (Succ n1) a -> Uncons f (Succ n1) a
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
Sized f (Succ n1) 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
-}
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 :: Sized f n a -> SnocView f n a
viewSnoc Sized f n a
sz = case SNat n -> ZeroOrSucc n
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc (KnownNat n => SNat n
forall (n :: Nat). KnownNat n => SNat n
sNat @n) of
  ZeroOrSucc n
IsZero -> SnocView f n a
forall (f :: Type -> Type) a. SnocView f 0 a
NilSV
  IsSucc (SNat n1
n' :: SNat n') ->
    SNat n1 -> (KnownNat n1 => SnocView f n a) -> SnocView f n a
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n1
n' ((KnownNat n1 => SnocView f n a) -> SnocView f n a)
-> (KnownNat n1 => SnocView f n a) -> SnocView f n a
forall a b. (a -> b) -> a -> b
$
      case SNat n1 -> Sized f (Succ n1) a -> Unsnoc f (Succ n1) a
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
Sized f (Succ n1) a
sz of
        Unsnoc (Sized f n a
xs :: Sized f m a) a
a ->
          (n1 :~: n) -> ((n1 ~ n) => SnocView f n a) -> SnocView f n a
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith
            ((() :~: ()) -> n1 :~: n
forall a b. a -> b
unsafeCoerce (() :~: ()
forall k (a :: k). a :~: a
Refl @()) :: n' :~: m)
            (((n1 ~ n) => SnocView f n a) -> SnocView f n a)
-> ((n1 ~ n) => SnocView f n a) -> SnocView f n a
forall a b. (a -> b) -> a -> b
$ Sized f n a
xs Sized f n a -> a -> SnocView f (n + 1) a
forall (n :: Nat) (f :: Type -> Type) a.
KnownNat n =>
Sized f n a -> a -> SnocView f (n + 1) 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:< :: 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)
-> (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) (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 :: 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
$ SNat n -> ZeroOrSucc n
forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc (SNat n -> ZeroOrSucc n) -> SNat n -> ZeroOrSucc n
forall a b. (a -> b) -> a -> b
$ KnownNat n => SNat n
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 :: 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) -> (Void# -> r) -> r
Nil <-
  (chkNil -> IsZero)
  where
    Nil = Sized f n a
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:> :: 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)
-> (Void# -> r)
-> r
:> b <-
  (viewSnoc -> a :-:: b)
  where
    Sized f n1 a
a :> a
b = Sized f n1 a
a Sized f n1 a -> a -> Sized f (n1 + 1) 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 :: a -> Sized f n a
pure (a
x :: a) =
    Dict (DomC f a) -> (DomC f a => Sized f n a) -> Sized f n a
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (DomC f a => Dict (DomC f a)
forall (a :: Constraint). a => Dict a
Dict @(DomC f a)) ((DomC f a => Sized f n a) -> Sized f n a)
-> (DomC f a => Sized f n a) -> Sized f n a
forall a b. (a -> b) -> a -> b
$
      a -> Sized f n a
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)) <*> :: Sized f n (a -> b) -> Sized f n a -> Sized f n b
<*> (Sized f n a
xs :: Sized f n a) =
    Dict (DomC f b) -> (DomC f b => Sized f n b) -> Sized f n b
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (DomC f b => Dict (DomC f b)
forall (a :: Constraint). a => Dict a
Dict @(DomC f b)) ((DomC f b => Sized f n b) -> Sized f n b)
-> (DomC f b => Sized f n b) -> Sized f n b
forall a b. (a -> b) -> a -> b
$
      Dict (DomC f a) -> (DomC f a => Sized f n b) -> Sized f n b
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (DomC f a => Dict (DomC f a)
forall (a :: Constraint). a => Dict a
Dict @(DomC f a)) ((DomC f a => Sized f n b) -> Sized f n b)
-> (DomC f a => Sized f n b) -> Sized f n b
forall a b. (a -> b) -> a -> b
$
        Dict (DomC f (a -> b))
-> (DomC f (a -> b) => Sized f n b) -> Sized f n b
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (DomC f (a -> b) => Dict (DomC f (a -> b))
forall (a :: Constraint). a => Dict a
Dict @(DomC f (a -> b))) ((DomC f (a -> b) => Sized f n b) -> Sized f n b)
-> (DomC f (a -> b) => Sized f n b) -> Sized f n b
forall a b. (a -> b) -> a -> b
$
          ((a -> b) -> 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 (a -> b) -> a -> b
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 :: a -> Sized f n a
cpure = a -> Sized f n a
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 :: Sized f n a -> Sized f n b -> Sized f n (a, b)
pair = 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)
zipSame
  <.> :: Sized f n (a -> b) -> Sized f n a -> Sized f n b
(<.>) = ((a -> b) -> 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 (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
($)
  <. :: Sized f n a -> Sized f n b -> Sized f n a
(<.) = Sized f n a -> Sized f n b -> Sized f n a
forall a b. a -> b -> a
P.const
  .> :: Sized f n a -> Sized f n b -> Sized f n b
(.>) = (Sized f n b -> Sized f n a -> 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 Sized f n b -> Sized f n a -> Sized f n b
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 :: (These a b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
calignWith =
    ((These a b -> c) -> f a -> f b -> f c)
-> (These a b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
coerce (\These a b -> c
f -> (a -> b -> c) -> f a -> f b -> f c
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 (These a b -> c) -> (b -> These a b) -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((b -> These a b) -> b -> c)
-> (a -> b -> These a b) -> a -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b -> These a b
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 :: Sized f n a -> Sized f n b -> Sized f n (These a b)
calign =
    (f a -> f b -> f (These a b))
-> Sized f n a -> Sized f n b -> Sized f n (These a b)
coerce ((f a -> f b -> f (These a b))
 -> Sized f n a -> Sized f n b -> Sized f n (These a b))
-> (f a -> f b -> f (These a b))
-> Sized f n a
-> Sized f n b
-> Sized f n (These a b)
forall a b. (a -> b) -> a -> b
$ (a -> b -> These a b) -> f a -> f b -> f (These 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 a -> b -> These 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 :: (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
czipWith =
    ((a -> b -> c) -> f a -> f b -> f c)
-> (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
coerce (((a -> b -> c) -> f a -> f b -> f c)
 -> (a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c)
-> ((a -> b -> c) -> f a -> f b -> f c)
-> (a -> b -> c)
-> Sized f n a
-> Sized f n b
-> Sized f n c
forall a b. (a -> b) -> a -> b
$ (Dom f a, Dom f b, Dom f c) => (a -> b -> c) -> f a -> f b -> f c
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 :: Sized f n a -> Sized f n b -> Sized f n (a, b)
czip =
    (f a -> f b -> f (a, b))
-> Sized f n a -> Sized f n b -> Sized f n (a, b)
coerce ((f a -> f b -> f (a, b))
 -> Sized f n a -> Sized f n b -> Sized f n (a, b))
-> (f a -> f b -> f (a, b))
-> Sized f n a
-> Sized f n b
-> Sized f n (a, b)
forall a b. (a -> b) -> a -> b
$ (Dom f a, Dom f b, Dom f (a, b)) => f a -> f b -> f (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 :: a -> Sized f n a
crepeat = a -> Sized f n a
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 :: (a -> g b) -> Sized f n a -> g (Sized f n b)
ctraverse = \a -> g b
f -> (f b -> Sized f n b) -> g (f b) -> g (Sized f n b)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap f b -> Sized f n b
coerce (g (f b) -> g (Sized f n b))
-> (Sized f n a -> g (f b)) -> Sized f n a -> g (Sized f n b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> g b) -> f a -> g (f b)
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 (f a -> g (f b)) -> (Sized f n a -> f a) -> Sized f n a -> g (f b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized f n a -> f a
forall (f :: Type -> Type) (n :: Nat) a. Sized f n a -> f a
runSized
  {-# INLINE ctraverse #-}