{-# LANGUAGE AllowAmbiguousTypes, CPP, ConstraintKinds, DataKinds          #-}
{-# LANGUAGE DeriveDataTypeable, DeriveFoldable, DeriveFunctor             #-}
{-# LANGUAGE DeriveTraversable, DerivingStrategies, ExplicitNamespaces     #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs                    #-}
{-# LANGUAGE GeneralizedNewtypeDeriving, InstanceSigs, KindSignatures      #-}
{-# LANGUAGE LambdaCase, LiberalTypeSynonyms, MultiParamTypeClasses        #-}
{-# LANGUAGE NoMonomorphismRestriction, NoStarIsType, PatternSynonyms      #-}
{-# LANGUAGE PolyKinds, QuantifiedConstraints, RankNTypes                  #-}
{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeApplications     #-}
{-# LANGUAGE TypeFamilies, TypeInType, TypeOperators, UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses, ViewPatterns                         #-}

{-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-}
{-# OPTIONS_GHC -fenable-rewrite-rules #-}
-- | 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 Data.Sized.Internal

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.Singletons.Prelude      (SingI (..), SomeSing (..),
                                               withSing, withSingI)
import           Data.Singletons.Prelude.Bool (Sing)
import           Data.Singletons.Prelude.Enum (PEnum (..), sPred, sSucc)
import           Data.These                   (These (..))
import           Data.Type.Equality           (gcastWith, (:~:) (..))
import qualified Data.Type.Natural            as Peano
import           Data.Type.Natural.Class      (IsPeano (..), One, PNum (..),
                                               POrd (..), PeanoOrder (..), S,
                                               SNum (..), Zero, ZeroOrSucc (..),
                                               pattern Zero, sOne, sZero,
                                               type (-.))
import           Data.Type.Ordinal            (HasOrdinal, 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 qualified GHC.TypeLits                 as TL
import           Prelude                      (Bool (..), Enum (..), Eq (..),
                                               Functor, Int, Maybe (..),
                                               Num (..), Ord (..), Ordering,
                                               Show (..), const, flip, fmap,
                                               fromIntegral, uncurry, ($), (.))
import qualified Prelude                      as P
import           Proof.Propositional          (IsTrue (..), withWitness)
import           Unsafe.Coerce                (unsafeCoerce)

--------------------------------------------------------------------------------
-- 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 nat a where
  SomeSized' :: Sing n
            -> Sized f (n :: nat) a
            -> SomeSized' f nat a

deriving instance Typeable SomeSized'

instance Show (f a) => Show (SomeSized' f nat a) where
  showsPrec :: Int -> SomeSized' f nat a -> ShowS
showsPrec Int
d (SomeSized' Sing 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 nat a) where
  (SomeSized' Sing n
_ (Sized f a
xs)) == :: SomeSized' f nat a -> SomeSized' f nat a -> Bool
== (SomeSized' Sing 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 nat f (n :: nat) a.
    (IsPeano nat, Dom f a, SingI 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
$ Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural (Sing n -> Natural) -> Sing n -> Natural
forall a b. (a -> b) -> a -> b
$ SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @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 #-}

lengthPeanoZero :: Sized f 'Peano.Z a -> Int
lengthPeanoZero :: Sized f 'Z a -> Int
lengthPeanoZero = Int -> Sized f 'Z a -> Int
forall a b. a -> b -> a
P.const Int
0
{-# INLINE lengthPeanoZero #-}

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

-- | @Sing@ version of 'length'.
--
-- Since 0.8.0.0 (type changed)
sLength :: forall nat f (n :: nat) a.
            (HasOrdinal nat, Dom f a, SingI n)
        => Sized f n a -> Sing n
sLength :: Sized f n a -> Sing n
sLength Sized f n a
_ = SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n
{-# INLINE[2] sLength #-}

-- | Test if the sequence is empty or not.
--
-- Since 0.7.0.0
null
  :: forall nat 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 #-}

nullPeano0 :: Sized f 'Peano.Z a -> Bool
nullPeano0 :: Sized f 'Z a -> Bool
nullPeano0 = Bool -> Sized f 'Z a -> Bool
forall a b. a -> b -> a
P.const Bool
True
{-# INLINE nullPeano0 #-}

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 TL.<= n => Sized f n a).
  null vec = False
"null/Z"  [~2] null = nullPeano0
"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 nat f (m :: nat) a. (CFoldable f, Dom f a, (One nat <= m) ~ 'True)
  => 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 nat f (n :: nat) c.
    (HasOrdinal nat, 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 nat (n :: nat). HasOrdinal 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 (%!!) #-}
{-# SPECIALISE (%!!) :: Sized [] (n :: TL.Nat) a -> Ordinal n -> a #-}
{-# SPECIALISE (%!!) :: Sized [] (n :: Peano.Nat) a -> Ordinal n -> a #-}
{-# SPECIALISE (%!!) :: Sized V.Vector (n :: TL.Nat) a -> Ordinal n -> a #-}
{-# SPECIALISE (%!!) :: Sized V.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-}
{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-}
{-# SPECIALISE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-}
{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: TL.Nat) a -> Ordinal n -> a #-}
{-# SPECIALISE (%!!) :: SV.Storable a => Sized SV.Vector (n :: Peano.Nat) a -> Ordinal n -> a #-}
{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: TL.Nat) a -> Ordinal n -> a #-}
{-# SPECIALISE (%!!) :: Sized Seq.Seq (n :: Peano.Nat) a -> Ordinal n -> a #-}

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

-- | Flipped version of '%!!'.
--
-- Since 0.7.0.0
sIndex
  :: forall nat f (n :: nat) c. (HasOrdinal nat, 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
$ (HasOrdinal nat, CFoldable f, Dom f c) =>
Sized f n c -> Ordinal n -> c
forall nat (f :: Type -> Type) (n :: nat) c.
(HasOrdinal nat, CFoldable f, Dom f c) =>
Sized f n c -> Ordinal n -> c
(%!!) @nat @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 nat f (n :: nat) a.
      (HasOrdinal nat, CFoldable f, Dom f a, (Zero nat < n) ~ 'True)
  => 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 nat f (n :: nat) a.
  (HasOrdinal nat, (Zero nat < n) ~ 'True, 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 nat f (n :: nat) a.
  (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a, (Zero nat < n) ~ 'True)
  => Sized f n a -> Uncons f n a
uncons :: Sized f n a -> Uncons f n a
uncons =
  Sing (Pred n)
-> (SingI (Pred n) => Sized f n a -> Uncons f n a)
-> Sized f n a
-> Uncons f n a
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI
    (Sing n -> Sing (Apply PredSym0 n)
forall a (t :: a). SEnum a => Sing t -> Sing (Apply PredSym0 t)
sPred (Sing n -> Sing (Apply PredSym0 n))
-> Sing n -> Sing (Apply PredSym0 n)
forall a b. (a -> b) -> a -> b
$ SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n)
  ((SingI (Pred n) => Sized f n a -> Uncons f n a)
 -> Sized f n a -> Uncons f n a)
-> (SingI (Pred n) => Sized f n a -> Uncons f n a)
-> Sized f n a
-> Uncons f n a
forall a b. (a -> b) -> a -> b
$ (Succ (Pred n) :~: (FromInteger 1 + Pred n))
-> ((Succ (Pred n) ~ (FromInteger 1 + Pred n)) =>
    Sized f n a -> Uncons f n a)
-> Sized f n a
-> Uncons f n a
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith
      (Sing (Pred n) -> Succ (Pred n) :~: (One nat + Pred n)
forall nat (n :: nat).
IsPeano nat =>
Sing n -> Succ n :~: (One nat + n)
succAndPlusOneL (Sing (Pred n) -> Succ (Pred n) :~: (One nat + Pred n))
-> Sing (Pred n) -> Succ (Pred n) :~: (One nat + Pred n)
forall a b. (a -> b) -> a -> b
$ Sing n -> Sing (Apply PredSym0 n)
forall a (t :: a). SEnum a => Sing t -> Sing (Apply PredSym0 t)
sPred (Sing n -> Sing (Apply PredSym0 n))
-> Sing n -> Sing (Apply PredSym0 n)
forall a b. (a -> b) -> a -> b
$ SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n)
  (((Succ (Pred n) ~ (FromInteger 1 + Pred n)) =>
  Sized f n a -> Uncons f n a)
 -> Sized f n a -> Uncons f n a)
-> ((Succ (Pred n) ~ (FromInteger 1 + Pred n)) =>
    Sized f n a -> Uncons f n a)
-> Sized f n a
-> Uncons f n a
forall a b. (a -> b) -> a -> b
$ (n :~: (FromInteger 1 + Pred n))
-> ((n ~ (FromInteger 1 + Pred n)) => Sized f n a -> Uncons f n a)
-> Sized f n a
-> Uncons f n a
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith
      (Sing (FromInteger 0)
-> Sing n -> IsTrue (FromInteger 0 < n) -> n :~: Succ (Pred n)
forall nat (n :: nat) (m :: nat).
PeanoOrder nat =>
Sing n -> Sing m -> IsTrue (n < m) -> m :~: Succ (Pred m)
lneqRightPredSucc Sing (FromInteger 0)
forall nat. SNum nat => Sing (Zero nat)
sZero (SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n) IsTrue 'True
IsTrue (FromInteger 0 < n)
Witness
      )
  (((n ~ (FromInteger 1 + Pred n)) => Sized f n a -> Uncons f n a)
 -> Sized f n a -> Uncons f n a)
-> ((n ~ (FromInteger 1 + Pred n)) => 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 (Pred n) a -> Uncons f n a)
-> (a, Sized f (Pred n) a) -> Uncons f n a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (SingI (Pred n) =>
a -> Sized f (Pred n) a -> Uncons f (One nat + Pred n) a
forall nat (f :: Type -> Type) (n :: nat) a.
SingI n =>
a -> Sized f n a -> Uncons f (One nat + n) a
Uncons @nat @f @(Pred n) @a) ((a, Sized f (Pred n) a) -> Uncons f n a)
-> (Sized f n a -> (a, Sized f (Pred n) a))
-> Sized f n a
-> Uncons f n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a -> (a, f a)) -> Sized f n a -> (a, Sized f (Pred n) 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 nat f (n :: nat) a proxy.
    (HasOrdinal nat, SingI 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
_  = Sing (Succ n)
-> (SingI (Succ n) => Sized f (Succ n) a -> Uncons f (Succ n) a)
-> Sized f (Succ n) a
-> Uncons f (Succ n) a
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI (Sing n -> Sing (Apply SuccSym0 n)
forall a (t :: a). SEnum a => Sing t -> Sing (Apply SuccSym0 t)
sSucc (Sing n -> Sing (Apply SuccSym0 n))
-> Sing n -> Sing (Apply SuccSym0 n)
forall a b. (a -> b) -> a -> b
$ SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n)
  ((SingI (Succ n) => Sized f (Succ n) a -> Uncons f (Succ n) a)
 -> Sized f (Succ n) a -> Uncons f (Succ n) a)
-> (SingI (Succ n) => Sized f (Succ n) a -> Uncons f (Succ n) a)
-> Sized f (Succ n) a
-> Uncons f (Succ n) a
forall a b. (a -> b) -> a -> b
$ IsTrue (FromInteger 0 < Succ n)
-> (((FromInteger 0 < Succ n) ~ 'True) =>
    Sized f (Succ n) a -> Uncons f (Succ n) a)
-> Sized f (Succ n) a
-> Uncons f (Succ n) a
forall (b :: Bool) r. IsTrue b -> ((b ~ 'True) => r) -> r
withWitness (Sing n -> IsTrue (Zero nat < Succ n)
forall nat (a :: nat).
PeanoOrder nat =>
Sing a -> IsTrue (Zero nat < Succ a)
lneqZero (Sing n -> IsTrue (Zero nat < Succ n))
-> Sing n -> IsTrue (Zero nat < Succ n)
forall a b. (a -> b) -> a -> b
$ SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n) ((FromInteger 0 < Succ n) ~ 'True) =>
Sized f (Succ n) a -> Uncons f (Succ n) a
forall nat (f :: Type -> Type) (n :: nat) a.
(PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a,
 (Zero nat < n) ~ 'True) =>
Sized f n a -> Uncons f n a
uncons
{-# INLINE uncons' #-}

data Uncons f (n :: nat) a where
  Uncons :: forall nat f (n :: nat) a. SingI n
    => a -> Sized f n a -> Uncons f (One nat + 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 nat f (n :: nat) a.
    (HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a, (Zero nat < n) ~ 'True)
  => Sized f n a -> Unsnoc f n a
unsnoc :: Sized f n a -> Unsnoc f n a
unsnoc = Sing (Pred n)
-> (SingI (Pred n) => Sized f n a -> Unsnoc f n a)
-> Sized f n a
-> Unsnoc f n a
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI
    (Sing n -> Sing (Apply PredSym0 n)
forall a (t :: a). SEnum a => Sing t -> Sing (Apply PredSym0 t)
sPred (Sing n -> Sing (Apply PredSym0 n))
-> Sing n -> Sing (Apply PredSym0 n)
forall a b. (a -> b) -> a -> b
$ SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n)
  ((SingI (Pred n) => Sized f n a -> Unsnoc f n a)
 -> Sized f n a -> Unsnoc f n a)
-> (SingI (Pred n) => Sized f n a -> Unsnoc f n a)
-> Sized f n a
-> Unsnoc f n a
forall a b. (a -> b) -> a -> b
$ (n :~: Succ (Pred n))
-> ((n ~ Succ (Pred n)) => Sized f n a -> Unsnoc f n a)
-> Sized f n a
-> Unsnoc f n a
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith
      (Sing (FromInteger 0)
-> Sing n -> IsTrue (FromInteger 0 < n) -> n :~: Succ (Pred n)
forall nat (n :: nat) (m :: nat).
PeanoOrder nat =>
Sing n -> Sing m -> IsTrue (n < m) -> m :~: Succ (Pred m)
lneqRightPredSucc Sing (FromInteger 0)
forall nat. SNum nat => Sing (Zero nat)
sZero (SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n) IsTrue 'True
IsTrue (FromInteger 0 < n)
Witness
      )
  (((n ~ Succ (Pred n)) => Sized f n a -> Unsnoc f n a)
 -> Sized f n a -> Unsnoc f n a)
-> ((n ~ Succ (Pred n)) => 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 (Pred n) a -> a -> Unsnoc f n a)
-> (Sized f (Pred n) a, a) -> Unsnoc f n a
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall a. Sized f (Pred n) a -> a -> Unsnoc f (Succ (Pred n)) a
forall nat (f :: Type -> Type) (n :: nat) a.
Sized f n a -> a -> Unsnoc f (Succ n) a
Unsnoc @nat @f @(Pred n)) ((Sized f (Pred n) a, a) -> Unsnoc f n a)
-> (Sized f n a -> (Sized f (Pred n) a, a))
-> Sized f n a
-> Unsnoc f n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a -> (f a, a)) -> Sized f n a -> (Sized f (Pred n) 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 nat 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 nat f (n :: nat) a proxy.
    (HasOrdinal nat, SingI 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
_  =
  Sing (Succ n)
-> (SingI (Succ n) => Sized f (Succ n) a -> Unsnoc f (Succ n) a)
-> Sized f (Succ n) a
-> Unsnoc f (Succ n) a
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI (Sing n -> Sing (Apply SuccSym0 n)
forall a (t :: a). SEnum a => Sing t -> Sing (Apply SuccSym0 t)
sSucc (Sing n -> Sing (Apply SuccSym0 n))
-> Sing n -> Sing (Apply SuccSym0 n)
forall a b. (a -> b) -> a -> b
$ SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n)
  ((SingI (Succ n) => Sized f (Succ n) a -> Unsnoc f (Succ n) a)
 -> Sized f (Succ n) a -> Unsnoc f (Succ n) a)
-> (SingI (Succ n) => Sized f (Succ n) a -> Unsnoc f (Succ n) a)
-> Sized f (Succ n) a
-> Unsnoc f (Succ n) a
forall a b. (a -> b) -> a -> b
$ IsTrue (FromInteger 0 < Succ n)
-> (((FromInteger 0 < Succ n) ~ 'True) =>
    Sized f (Succ n) a -> Unsnoc f (Succ n) a)
-> Sized f (Succ n) a
-> Unsnoc f (Succ n) a
forall (b :: Bool) r. IsTrue b -> ((b ~ 'True) => r) -> r
withWitness (Sing n -> IsTrue (Zero nat < Succ n)
forall nat (a :: nat).
PeanoOrder nat =>
Sing a -> IsTrue (Zero nat < Succ a)
lneqZero (Sing n -> IsTrue (Zero nat < Succ n))
-> Sing n -> IsTrue (Zero nat < Succ n)
forall a b. (a -> b) -> a -> b
$ SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n) ((FromInteger 0 < Succ n) ~ 'True) =>
Sized f (Succ n) a -> Unsnoc f (Succ n) a
forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a,
 (Zero nat < n) ~ 'True) =>
Sized f n a -> Unsnoc f n a
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 nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a)
  => Sized f (One nat + n) a -> Sized f n a
tail :: Sized f (One nat + n) a -> Sized f n a
tail = (f a -> f a) -> Sized f (FromInteger 1 + n) a -> Sized f n a
coerce ((f a -> f a) -> Sized f (FromInteger 1 + n) a -> Sized f n a)
-> (f a -> f a) -> Sized f (FromInteger 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 nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a)
  => Sized f (n + One nat) a -> Sized f n a
init :: Sized f (n + One nat) a -> Sized f n a
init = (f a -> f a) -> Sized f (n + FromInteger 1) a -> Sized f n a
coerce ((f a -> f a) -> Sized f (n + FromInteger 1) a -> Sized f n a)
-> (f a -> f a) -> Sized f (n + FromInteger 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 nat (n :: nat) f (m :: nat) a.
    (CFreeMonoid f, Dom f a, (n <= m) ~ 'True, HasOrdinal nat)
  => Sing n -> Sized f m a -> Sized f n a
take :: Sing n -> Sized f m a -> Sized f n a
take = (Sing n -> f a -> f a) -> Sing n -> Sized f m a -> Sized f n a
coerce ((Sing n -> f a -> f a) -> Sing n -> Sized f m a -> Sized f n a)
-> (Sing n -> f a -> f a) -> Sing 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) -> (Sing n -> Int) -> Sing 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) -> (Sing n -> Natural) -> Sing n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural @nat @n
{-# INLINE take #-}

-- | @'takeAtMost' k xs@ takes first at most @k@ elements of @xs@.
--
-- Since 0.7.0.0
takeAtMost
  :: forall nat (n :: nat) f m a.
      (CFreeMonoid f, Dom f a, HasOrdinal nat)
  => Sing n -> Sized f m a -> Sized f (Min n m) a
takeAtMost :: Sing n -> Sized f m a -> Sized f (Min n m) a
takeAtMost = (Sing n -> f a -> f a)
-> Sing n -> Sized f m a -> Sized f (Min n m) a
coerce ((Sing n -> f a -> f a)
 -> Sing n -> Sized f m a -> Sized f (Min n m) a)
-> (Sing n -> f a -> f a)
-> Sing 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) -> (Sing n -> Int) -> Sing 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) -> (Sing n -> Natural) -> Sing n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural @nat @n
{-# 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 nat (n :: nat) f (m :: nat) a.
    (HasOrdinal nat, CFreeMonoid f, Dom f a, (n <= m) ~ 'True)
  => Sing n -> Sized f m a -> Sized f (m - n) a
drop :: Sing n -> Sized f m a -> Sized f (m - n) a
drop = (Sing n -> f a -> f a)
-> Sing n -> Sized f m a -> Sized f (m - n) a
coerce ((Sing n -> f a -> f a)
 -> Sing n -> Sized f m a -> Sized f (m - n) a)
-> (Sing n -> f a -> f a)
-> Sing 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) -> (Sing n -> Int) -> Sing 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) -> (Sing n -> Natural) -> Sing n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural @nat @n
{-# 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 nat (n :: nat) f m a.
      (CFreeMonoid f, Dom f a , (n <= m) ~ 'True, HasOrdinal nat)
  => Sing n -> Sized f m a -> (Sized f n a, Sized f (m -. n) a)
splitAt :: Sing n -> Sized f m a -> (Sized f n a, Sized f (m -. n) a)
splitAt =
  (Sing n -> f a -> (f a, f a))
-> Sing n -> Sized f m a -> (Sized f n a, Sized f (m - n) a)
coerce ((Sing n -> f a -> (f a, f a))
 -> Sing n -> Sized f m a -> (Sized f n a, Sized f (m - n) a))
-> (Sing n -> f a -> (f a, f a))
-> Sing 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))
-> (Sing n -> Int) -> Sing 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) -> (Sing n -> Natural) -> Sing n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural @nat @n
{-# 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 nat (n :: nat) f (m :: nat) a.
      (HasOrdinal nat, CFreeMonoid f, Dom f a)
  => Sing n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a)
splitAtMost :: Sing n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a)
splitAtMost =
  (Sing n -> f a -> (f a, f a))
-> Sing n
-> Sized f m a
-> (Sized f (Min n m) a, Sized f (m -. n) a)
coerce ((Sing n -> f a -> (f a, f a))
 -> Sing n
 -> Sized f m a
 -> (Sized f (Min n m) a, Sized f (m -. n) a))
-> (Sing n -> f a -> (f a, f a))
-> Sing 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))
-> (Sing n -> Int) -> Sing 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) -> (Sing n -> Natural) -> Sing n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural @nat @n
{-# INLINE splitAtMost #-}


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

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

-- | Empty sequence.
--
-- Since 0.7.0.0 (type changed)
empty
  :: forall nat f a. (Monoid (f a), HasOrdinal nat, Dom f a)
  => Sized f (Zero nat) a
empty :: Sized f (Zero nat) a
empty = f a -> Sized f (FromInteger 0) a
coerce (f a -> Sized f (FromInteger 0) a)
-> f a -> Sized f (FromInteger 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 nat f a. (CPointed f, Dom f a) => a -> Sized f (One nat) a
singleton :: a -> Sized f (One nat) a
singleton = (a -> f a) -> a -> Sized f (FromInteger 1) a
coerce ((a -> f a) -> a -> Sized f (FromInteger 1) a)
-> (a -> f a) -> a -> Sized f (FromInteger 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 nat f a. (HasOrdinal nat, Dom f a, CFoldable f)
  => f a -> SomeSized' f nat a
toSomeSized :: f a -> SomeSized' f nat a
toSomeSized = \f a
xs ->
  case Natural -> SomeSing nat
forall nat. IsPeano nat => Natural -> SomeSing nat
fromNatural (Natural -> SomeSing nat) -> Natural -> SomeSing nat
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
    SomeSing Sing a
sn -> Sing a -> (SingI a => SomeSized' f nat a) -> SomeSized' f nat a
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing a
sn ((SingI a => SomeSized' f nat a) -> SomeSized' f nat a)
-> (SingI a => SomeSized' f nat a) -> SomeSized' f nat a
forall a b. (a -> b) -> a -> b
$ Sing a -> Sized f a a -> SomeSized' f nat a
forall nat (n :: nat) (f :: Type -> Type) a.
Sing n -> Sized f n a -> SomeSized' f nat a
SomeSized' Sing a
sn (Sized f a a -> SomeSized' f nat a)
-> Sized f a a -> SomeSized' f nat a
forall a b. (a -> b) -> a -> b
$ Sing a -> f a -> Sized f a a
forall nat (f :: Type -> Type) (n :: nat) a.
Sing n -> f a -> Sized f n a
unsafeToSized Sing a
sn f a
xs

-- | Replicates the same value.
--
-- Since 0.7.0.0
replicate :: forall nat f (n :: nat) a. (HasOrdinal nat, CFreeMonoid f, Dom f a)
          => Sing n -> a -> Sized f n a
replicate :: Sing n -> a -> Sized f n a
replicate = (Sing n -> a -> f a) -> Sing n -> a -> Sized f n a
coerce ((Sing n -> a -> f a) -> Sing n -> a -> Sized f n a)
-> (Sing n -> a -> f a) -> Sing 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) -> (Sing n -> Int) -> Sing 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) -> (Sing n -> Natural) -> Sing n -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural @nat @n
{-# INLINE replicate #-}

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

-- | Construct a sequence of the given length by applying the function to each index.
--
-- Since 0.7.0.0
generate
  :: forall (nat :: Type) f (n :: nat) (a :: Type).
      (CFreeMonoid f, Dom f a, HasOrdinal nat)
  => Sing n -> (Ordinal n -> a) -> Sized f n a
generate :: Sing n -> (Ordinal n -> a) -> Sized f n a
generate = (Sing n -> (Ordinal n -> a) -> f a)
-> Sing n -> (Ordinal n -> a) -> Sized f n a
coerce ((Sing n -> (Ordinal n -> a) -> f a)
 -> Sing n -> (Ordinal n -> a) -> Sized f n a)
-> (Sing n -> (Ordinal n -> a) -> f a)
-> Sing n
-> (Ordinal n -> a)
-> Sized f n a
forall a b. (a -> b) -> a -> b
$ \Sing n
sn -> Sing n
-> (SingI n => (Ordinal n -> a) -> f a) -> (Ordinal n -> a) -> f a
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
sn ((SingI n => (Ordinal n -> a) -> f a) -> (Ordinal n -> a) -> f a)
-> (SingI 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
$ Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural @nat @n Sing 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 (nat :: Type) f (n :: nat) (a :: Type).
      (SingI n, CFreeMonoid f, Dom f a, HasOrdinal nat)
  => (Ordinal n -> a) -> Sized f n a
generate' :: (Ordinal n -> a) -> Sized f n a
generate' = Sing n -> (Ordinal n -> a) -> Sized f n a
forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a, HasOrdinal nat) =>
Sing n -> (Ordinal n -> a) -> Sized f n a
generate Sing n
forall k (a :: k). SingI a => Sing a
sing
{-# INLINE [1] generate' #-}

genVector :: forall nat (n :: nat) a.
            (HasOrdinal nat)
          => Sing n -> (Ordinal n -> a) -> Sized V.Vector n a
genVector :: Sing n -> (Ordinal n -> a) -> Sized Vector n a
genVector Sing n
n Ordinal n -> a
f = Sing n -> (SingI n => Sized Vector n a) -> Sized Vector n a
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
n ((SingI n => Sized Vector n a) -> Sized Vector n a)
-> (SingI n => Sized Vector n a) -> Sized Vector n a
forall a b. (a -> b) -> a -> b
$ Vector a -> Sized Vector n a
forall nat (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
$ Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural Sing 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 nat (n :: nat) a.
             (HasOrdinal nat, SV.Storable a)
           => Sing n -> (Ordinal n -> a) -> Sized SV.Vector n a
genSVector :: Sing n -> (Ordinal n -> a) -> Sized Vector n a
genSVector Sing n
n Ordinal n -> a
f = Sing n -> (SingI n => Sized Vector n a) -> Sized Vector n a
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
n ((SingI n => Sized Vector n a) -> Sized Vector n a)
-> (SingI n => Sized Vector n a) -> Sized Vector n a
forall a b. (a -> b) -> a -> b
$ Vector a -> Sized Vector n a
forall nat (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
$ Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural Sing 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 nat (n :: nat) a.
          (HasOrdinal nat)
       => Sing n -> (Ordinal n -> a) -> Sized Seq.Seq n a
genSeq :: Sing n -> (Ordinal n -> a) -> Sized Seq n a
genSeq Sing n
n Ordinal n -> a
f = Sing n -> (SingI n => Sized Seq n a) -> Sized Seq n a
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n
n ((SingI n => Sized Seq n a) -> Sized Seq n a)
-> (SingI n => Sized Seq n a) -> Sized Seq n a
forall a b. (a -> b) -> a -> b
$ Seq a -> Sized Seq n a
forall nat (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
$ Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural Sing 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 :: HasOrdinal nat => Sing (n :: nat))
                       (f :: SV.Storable a => Ordinal n -> a).
  generate n f = genSVector n f
"generate/UVector" [~1] forall (n :: HasOrdinal nat => Sing (n :: nat))
                       (f :: UV.Unbox a => Ordinal n -> a).
  generate n f = withSingI 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 nat f (n :: nat) a.
    (CFreeMonoid f, Dom f a)
  => a -> Sized f n a -> Sized f (One nat + n) a
cons :: a -> Sized f n a -> Sized f (One nat + n) a
cons = (a -> f a -> f a)
-> a -> Sized f n a -> Sized f (FromInteger 1 + n) a
coerce ((a -> f a -> f a)
 -> a -> Sized f n a -> Sized f (FromInteger 1 + n) a)
-> (a -> f a -> f a)
-> a
-> Sized f n a
-> Sized f (FromInteger 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 nat f (n :: nat) a. (CFreeMonoid f, Dom f a)
  => a -> Sized f n a -> Sized f (One nat + n) a
<| :: a -> Sized f n a -> Sized f (One nat + n) a
(<|) = a -> Sized f n a -> Sized f (One nat + n) a
forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (One nat + n) a
cons
{-# INLINE (<|) #-}
infixr 5 <|

-- | Append an element to the tail of sequence.
--
-- Since 0.7.0.0
snoc
  :: forall nat f (n :: nat) a.
      (CFreeMonoid f, Dom f a)
  => Sized f n a -> a -> Sized f (n + One nat) a
snoc :: Sized f n a -> a -> Sized f (n + One nat) a
snoc (Sized f a
xs) a
a = f a -> Sized f (n + FromInteger 1) a
forall nat (f :: Type -> Type) (n :: nat) a. f a -> Sized f n a
Sized (f a -> Sized f (n + FromInteger 1) a)
-> f a -> Sized f (n + FromInteger 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 nat f (n :: nat) a.
  (CFreeMonoid f, Dom f a) => Sized f n a -> a -> Sized f (n + One nat) a
|> :: Sized f n a -> a -> Sized f (n + One nat) a
(|>) = Sized f n a -> a -> Sized f (n + One nat) a
forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + One nat) a
snoc
{-# INLINE (|>) #-}
infixl 5 |>

-- | Append two lists.
--
-- Since 0.7.0.0
append
  :: forall nat 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 nat 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 nat (f :: Type -> Type) (n :: nat) (m :: nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> Sized f m a -> Sized f (n + m) a
append
infixr 5 ++

-- | Concatenates multiple sequences into one.
--
-- Since 0.7.0.0
concat :: forall nat 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) nat (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 nat 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 nat 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 nat 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 nat 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 nat 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 nat 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 nat 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 nat (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) nat (n :: nat) a. Sized f n a -> f a
runSized
{-# INLINE map #-}

-- | Reverse function.
--
-- Since 0.7.0.0
reverse
  :: forall nat 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 nat f (n :: nat) a.
    (CFreeMonoid f, Dom f a)
  => a -> Sized f n a -> Sized f ((FromInteger 2 * n) -. One nat) a
intersperse :: a -> Sized f n a -> Sized f ((FromInteger 2 * n) -. One nat) a
intersperse = (a -> f a -> f a)
-> a
-> Sized f n a
-> Sized
     f
     (Subt
        (FromInteger 2 * n)
        (FromInteger 1)
        (FromInteger 1 <= (FromInteger 2 * n)))
     a
coerce ((a -> f a -> f a)
 -> a
 -> Sized f n a
 -> Sized
      f
      (Subt
         (FromInteger 2 * n)
         (FromInteger 1)
         (FromInteger 1 <= (FromInteger 2 * n)))
      a)
-> (a -> f a -> f a)
-> a
-> Sized f n a
-> Sized
     f
     (Subt
        (FromInteger 2 * n)
        (FromInteger 1)
        (FromInteger 1 <= (FromInteger 2 * 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
cintersperse @f @a
{-# INLINE intersperse #-}

-- | Remove all duplicates.
--
-- Since 0.7.0.0
nub
  :: forall nat f (n :: nat) a.
      (HasOrdinal nat, Dom f a, Eq a, CFreeMonoid f)
  => Sized f n a -> SomeSized' f nat a
nub :: Sized f n a -> SomeSized' f nat a
nub = f a -> SomeSized' f nat a
forall nat (f :: Type -> Type) a.
(HasOrdinal nat, Dom f a, CFoldable f) =>
f a -> SomeSized' f nat a
toSomeSized (f a -> SomeSized' f nat a)
-> (Sized f n a -> f a) -> Sized f n a -> SomeSized' f nat 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 nat 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 nat 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 nat 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 nat 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 nat 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 nat f (n :: nat) a.
      (HasOrdinal nat, CFreeMonoid f, Dom f a)
  => Sing n -> [a] -> Maybe (Sized f n a)
fromList :: Sing n -> [a] -> Maybe (Sized f n a)
fromList Sing 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 nat (f :: Type -> Type) (n :: nat) a. f a -> Sized f n a
Sized (f a
forall a. Monoid a => a
mempty :: f a)
fromList Sing 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
$ Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural Sing 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 nat (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
{-# INLINABLE [2] fromList #-}

-- | 'fromList' with the result length inferred.
--
-- Since 0.7.0.0
fromList'
  :: forall nat f (n :: nat) a.
    (PeanoOrder nat, Dom f a, CFreeMonoid f, SingI n)
  => [a] -> Maybe (Sized f n a)
fromList' :: [a] -> Maybe (Sized f n a)
fromList' = (Sing n -> [a] -> Maybe (Sized f n a))
-> [a] -> Maybe (Sized f n a)
forall k (a :: k) b. SingI a => (Sing a -> b) -> b
withSing Sing n -> [a] -> Maybe (Sized f n a)
forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
Sing n -> [a] -> Maybe (Sized f n a)
fromList
{-# 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 (nat :: Type) f (n :: nat) a.
    (CFreeMonoid f, Dom f a)
  => Sing n -> [a] -> Sized f n a
unsafeFromList :: Sing n -> [a] -> Sized f n a
unsafeFromList = ([a] -> Sized f n a) -> Sing n -> [a] -> Sized f n a
forall a b. a -> b -> a
const (([a] -> Sized f n a) -> Sing n -> [a] -> Sized f n a)
-> ([a] -> Sized f n a) -> Sing 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 nat f (n :: nat) a.
      (SingI n, CFreeMonoid f, Dom f a)
  => [a] -> Sized f n a
unsafeFromList' :: [a] -> Sized f n a
unsafeFromList' = (Sing n -> [a] -> Sized f n a) -> [a] -> Sized f n a
forall k (a :: k) b. SingI a => (Sing a -> b) -> b
withSing Sing n -> [a] -> Sized f n a
forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a) =>
Sing n -> [a] -> Sized f n a
unsafeFromList
{-# 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 nat f (n :: nat) a.
      (HasOrdinal nat, Dom f a, CFreeMonoid f)
  => Sing n -> a -> [a] -> Sized f n a
fromListWithDefault :: Sing n -> a -> [a] -> Sized f n a
fromListWithDefault Sing 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
$ Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural Sing n
sn
  in f a -> Sized f n a
forall nat (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
{-# INLINABLE fromListWithDefault #-}

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

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

-- | Forget the length and obtain the wrapped base container.
--
-- Since 0.7.0.0
unsized :: forall nat 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) nat (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 nat f (n :: nat) a.
      (HasOrdinal nat, CFreeMonoid f, Dom f a)
  => Sing (n :: nat) -> f a -> Maybe (Sized f n a)
toSized :: Sing n -> f a -> Maybe (Sized f n a)
toSized Sing 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
$ Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural Sing 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
$ Sing n -> f a -> Sized f n a
forall nat (f :: Type -> Type) (n :: nat) a.
Sing n -> f a -> Sized f n a
unsafeToSized Sing 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
{-# INLINABLE [2] toSized #-}

-- | 'toSized' with the result length inferred.
--
-- Since 0.7.0.0
toSized'
  :: forall nat f (n :: nat) a.
    (PeanoOrder nat, Dom f a, CFreeMonoid f, SingI n)
  => f a -> Maybe (Sized f n a)
toSized' :: f a -> Maybe (Sized f n a)
toSized' = (Sing n -> f a -> Maybe (Sized f n a))
-> f a -> Maybe (Sized f n a)
forall k (a :: k) b. SingI a => (Sing a -> b) -> b
withSing Sing n -> f a -> Maybe (Sized f n a)
forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
Sing n -> f a -> Maybe (Sized f n a)
toSized
{-# 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 nat f (n :: nat) a. Sing n -> f a -> Sized f n a
unsafeToSized :: Sing n -> f a -> Sized f n a
unsafeToSized Sing n
_ = f a -> Sized f n a
forall nat (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 nat f (n :: nat) a.
    (SingI n, Dom f a)
  => f a -> Sized f n a
unsafeToSized' :: f a -> Sized f n a
unsafeToSized' = (Sing n -> f a -> Sized f n a) -> f a -> Sized f n a
forall k (a :: k) b. SingI a => (Sing a -> b) -> b
withSing Sing n -> f a -> Sized f n a
forall nat (f :: Type -> Type) (n :: nat) a.
Sing n -> f a -> Sized f n a
unsafeToSized
{-# 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 nat f (n :: nat) a.
    (HasOrdinal nat, CFreeMonoid f, Dom f a)
  => Sing (n :: nat) -> a -> f a -> Sized f n a
toSizedWithDefault :: Sing n -> a -> f a -> Sized f n a
toSizedWithDefault Sing 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
$ Sing n -> Natural
forall nat (n :: nat). IsPeano nat => Sing n -> Natural
toNatural Sing n
sn
  in f a -> Sized f n a
forall nat (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
{-# INLINABLE toSizedWithDefault #-}

-- | 'toSizedWithDefault' with the result length inferred.
--
-- Since 0.7.0.0
toSizedWithDefault'
  :: forall nat f (n :: nat) a.
      (PeanoOrder nat, SingI n, CFreeMonoid f, Dom f a)
  => a -> f a -> Sized f n a
toSizedWithDefault' :: a -> f a -> Sized f n a
toSizedWithDefault' = (Sing n -> a -> f a -> Sized f n a) -> a -> f a -> Sized f n a
forall k (a :: k) b. SingI a => (Sing a -> b) -> b
withSing Sing n -> a -> f a -> Sized f n a
forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
Sing n -> a -> f a -> Sized f n a
toSizedWithDefault
{-# 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)
              => Sing n
              -> Sized f n a
              -> Sing 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 nat f (n :: nat) a.
    (HasOrdinal nat, Dom f a, CFreeMonoid f)
  => (a -> Bool) -> Sized f n a -> SomeSized' f nat a
takeWhile :: (a -> Bool) -> Sized f n a -> SomeSized' f nat a
takeWhile = (f a -> SomeSized' f nat a
forall nat (f :: Type -> Type) a.
(HasOrdinal nat, Dom f a, CFoldable f) =>
f a -> SomeSized' f nat a
toSomeSized (f a -> SomeSized' f nat a)
-> (Sized f n a -> f a) -> Sized f n a -> SomeSized' f nat a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Sized f n a -> f a) -> Sized f n a -> SomeSized' f nat a)
-> ((a -> Bool) -> Sized f n a -> f a)
-> (a -> Bool)
-> Sized f n a
-> SomeSized' f nat 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 nat f (n :: nat) a.
      (HasOrdinal nat, CFreeMonoid f, Dom f a)
  => (a -> Bool) -> Sized f n a -> SomeSized' f nat a
dropWhile :: (a -> Bool) -> Sized f n a -> SomeSized' f nat a
dropWhile = (f a -> SomeSized' f nat a
forall nat (f :: Type -> Type) a.
(HasOrdinal nat, Dom f a, CFoldable f) =>
f a -> SomeSized' f nat a
toSomeSized (f a -> SomeSized' f nat a)
-> (Sized f n a -> f a) -> Sized f n a -> SomeSized' f nat a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.) ((Sized f n a -> f a) -> Sized f n a -> SomeSized' f nat a)
-> ((a -> Bool) -> Sized f n a -> f a)
-> (a -> Bool)
-> Sized f n a
-> SomeSized' f nat 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 nat f (n :: nat) a.
      (HasOrdinal nat, 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 nat (n :: nat) (f :: Type -> Type) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
forall (f :: Type -> Type) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned @nat @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 nat f (n :: nat) a.
      (HasOrdinal nat, 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 nat (n :: nat) (f :: Type -> Type) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
forall (f :: Type -> Type) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned @nat @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 nat f (n :: nat) a.
      (HasOrdinal nat, 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 nat (n :: nat) (f :: Type -> Type) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
forall (f :: Type -> Type) a.
(HasOrdinal nat, CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned @nat @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 nat (n :: nat) f a.
    (HasOrdinal nat, 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 nat a
forall nat (f :: Type -> Type) a.
(HasOrdinal nat, Dom f a, CFoldable f) =>
f a -> SomeSized' f nat a
toSomeSized @nat f a
l, f a -> SomeSized' f nat a
forall nat (f :: Type -> Type) a.
(HasOrdinal nat, Dom f a, CFoldable f) =>
f a -> SomeSized' f nat a
toSomeSized @nat f a
r) of
    ( SomeSized' (lenL :: Sing nl) Sized f n a
ls,
      SomeSized' (lenR :: Sing 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
$ Sing n
-> Sized f n a -> Sing n -> Sized f n a -> Partitioned f (n + n) a
forall k (f :: Type -> Type) a (n :: k) (m :: k).
Dom f a =>
Sing n
-> Sized f n a -> Sing m -> Sized f m a -> Partitioned f (n + m) a
Partitioned Sing n
lenL Sized f n a
ls Sing n
lenR Sized f n a
rs

--------------------------------------------------------------------------------
--- Searching
--------------------------------------------------------------------------------
-- | Membership test; see also 'notElem'.
--
-- Since 0.7.0.0
elem
  :: forall nat 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 nat 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 nat 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 nat 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 nat f (n :: nat) a .
    (SingI (n :: nat), CFoldable f, Dom f a, HasOrdinal nat)
  => (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 nat 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 #-}
{-# SPECIALISE findIndices :: (a -> Bool) -> Sized [] n a -> [Int] #-}

-- | 'Ordinal' version of 'findIndices'.
--
-- Since 0.7.0.0
sFindIndices
  :: forall nat f (n :: nat) a .
    (HasOrdinal nat, CFoldable f, Dom f a, SingI (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 nat (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 nat 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 nat f (n :: nat) a.
              (SingI n, CFoldable f, Dom f a, Eq a, HasOrdinal nat)
           => 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 nat (f :: Type -> Type) (n :: nat) a.
(SingI n, CFoldable f, Dom f a, Eq a, HasOrdinal nat) =>
a -> Sized f n a -> Maybe (Ordinal n)
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 nat 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 nat f (n :: nat) a .
    (CFoldable f, HasOrdinal nat, SingI (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 nat (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 :: ('SingI' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n
slen ('viewCons' -> 'NilCV')    = 'SZ'
slen ('viewCons' -> _ ':-' as) = 'SS' (slen as)
slen _                          = error "impossible"
@

   The constraint @('SingI' 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 :: ('SingI' n, 'Dom f a' f) => 'Sized' f n a -> 'Sing' n
slen ('viewSnoc' -> 'NilSV')     = 'SZ'
slen ('viewSnoc' -> as '-::' _) = 'SS' (slen as)
@
-}

-- | View of the left end of sequence (cons-side).
--
-- Since 0.7.0.0
data ConsView f n a where
  NilCV :: ConsView f (Zero nat) a
  (:-)
    :: (SingI n, SingI (One nat + n))
    => a -> Sized f n a -> ConsView f (One nat + n) a

infixr 5 :-

-- | Case analysis for the cons-side of sequence.
--
-- Since 0.5.0.0 (type changed)
viewCons :: forall nat f (n :: nat) a .
  (HasOrdinal nat, SingI 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 Sing n -> ZeroOrSucc n
forall nat (n :: nat). IsPeano nat => Sing n -> ZeroOrSucc n
zeroOrSucc (Sing n -> ZeroOrSucc n) -> Sing n -> ZeroOrSucc n
forall a b. (a -> b) -> a -> b
$ SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n of
  ZeroOrSucc n
IsZero -> ConsView f n a
forall (f :: Type -> Type) nat a. ConsView f (Zero nat) a
NilCV
  IsSucc Sing n1
n' ->
    Sing n1 -> (SingI n1 => ConsView f n a) -> ConsView f n a
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
n'
    ((SingI n1 => ConsView f n a) -> ConsView f n a)
-> (SingI n1 => ConsView f n a) -> ConsView f n a
forall a b. (a -> b) -> a -> b
$ Sing (FromInteger 1 + n1)
-> (SingI (FromInteger 1 + n1) => ConsView f n a) -> ConsView f n a
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI (Sing (FromInteger 1)
forall nat. SNum nat => Sing (One nat)
sOne Sing (FromInteger 1)
-> Sing n1 -> Sing (Apply (Apply (+@#@$) (FromInteger 1)) n1)
forall a (t1 :: a) (t2 :: a).
SNum a =>
Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2)
%+ Sing n1
n')
    ((SingI (FromInteger 1 + n1) => ConsView f n a) -> ConsView f n a)
-> (SingI (FromInteger 1 + n1) => ConsView f n a) -> ConsView f n a
forall a b. (a -> b) -> a -> b
$ case Sing n1 -> Sized f (Succ n1) a -> Uncons f (Succ n1) a
forall nat (f :: Type -> Type) (n :: nat) a (proxy :: nat -> Type).
(HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) =>
proxy n -> Sized f (Succ n) a -> Uncons f (Succ n) a
uncons' Sing 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 (One nat + n) a
forall nat (n :: nat) a (f :: Type -> Type).
(SingI n, SingI (One nat + n)) =>
a -> Sized f n a -> ConsView f (One nat + 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 (Zero nat) a
  (:-::) :: SingI (n :: nat) => Sized f n a -> a -> SnocView f (n + One nat) a
infixl 5 :-::

-- | Case analysis for the snoc-side of sequence.
--
-- Since 0.5.0.0 (type changed)
viewSnoc :: forall nat f (n :: nat) a.
    (HasOrdinal nat, SingI 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 Sing n -> ZeroOrSucc n
forall nat (n :: nat). IsPeano nat => Sing n -> ZeroOrSucc n
zeroOrSucc (SingI n => Sing n
forall k (a :: k). SingI a => Sing a
sing @n) of
  ZeroOrSucc n
IsZero   -> SnocView f n a
forall (f :: Type -> Type) nat a. SnocView f (Zero nat) a
NilSV
  IsSucc (n' :: Sing n') ->
    Sing n1 -> (SingI n1 => SnocView f n a) -> SnocView f n a
forall k (n :: k) r. Sing n -> (SingI n => r) -> r
withSingI Sing n1
n' ((SingI n1 => SnocView f n a) -> SnocView f n a)
-> (SingI n1 => SnocView f n a) -> SnocView f n a
forall a b. (a -> b) -> a -> b
$
    (n :~: (n1 + FromInteger 1))
-> ((n ~ (n1 + FromInteger 1)) => SnocView f n a) -> SnocView f n a
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Sing n1 -> Succ n1 :~: (n1 + One nat)
forall nat (n :: nat).
IsPeano nat =>
Sing n -> Succ n :~: (n + One nat)
succAndPlusOneR Sing n1
n') (((n ~ (n1 + FromInteger 1)) => SnocView f n a) -> SnocView f n a)
-> ((n ~ (n1 + FromInteger 1)) => SnocView f n a) -> SnocView f n a
forall a b. (a -> b) -> a -> b
$
    case Sing n1 -> Sized f (Succ n1) a -> Unsnoc f (Succ n1) a
forall nat (f :: Type -> Type) (n :: nat) a (proxy :: nat -> Type).
(HasOrdinal nat, SingI n, CFreeMonoid f, Dom f a) =>
proxy n -> Sized f (Succ n) a -> Unsnoc f (Succ n) a
unsnoc' Sing 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 + One nat) a
forall nat (n :: nat) (f :: Type -> Type) a.
SingI n =>
Sized f n a -> a -> SnocView f (n + One nat) 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, 'SingI' n) => 'Sized' f ('S' ('S' n)) a -> a
nextToHead ('viewCons' -> _ ':-' ('viewCons' -> a ':-' _)) = a
@

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

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

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

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

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

infixr 5 :<
-- | Pattern synonym for cons-side uncons.
pattern (:<)
  :: forall nat (f :: Type -> Type) a (n :: nat).
      (Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f)
  => forall (n1 :: nat). (n ~ (One nat + n1), SingI n1)
  => a -> Sized f n1 a -> Sized f n a
pattern a $b:< :: a -> Sized f n1 a -> Sized f n a
$m:< :: forall r nat (f :: Type -> Type) a (n :: nat).
(Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f) =>
Sized f n a
-> (forall (n1 :: nat).
    (n ~ (One nat + n1), SingI 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 (One nat + n1) a
forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (One nat + n) a
<| Sized f n1 a
as

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

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

infixl 5 :>

-- | Pattern synonym for snoc-side unsnoc.
pattern (:>)
  :: forall nat (f :: Type -> Type) a (n :: nat).
      (Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f)
  => forall (n1 :: nat). (n ~ (n1 + One nat), SingI n1)
  => Sized f n1 a -> a -> Sized f n a
pattern a $b:> :: Sized f n1 a -> a -> Sized f n a
$m:> :: forall r nat (f :: Type -> Type) a (n :: nat).
(Dom f a, PeanoOrder nat, SingI n, CFreeMonoid f) =>
Sized f n a
-> (forall (n1 :: nat).
    (n ~ (n1 + One nat), SingI 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 + One nat) a
forall nat (f :: Type -> Type) (n :: nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + One nat) a
|> 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,
    HasOrdinal nat, SingI n, forall a. DomC f a)
      => P.Applicative (Sized f (n :: nat)) where
  {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized [] (n :: TL.Nat)) #-}
  {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized Seq.Seq (n :: TL.Nat)) #-}
  {-# SPECIALISE instance TL.KnownNat n => P.Applicative (Sized V.Vector (n :: TL.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 nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, SingI 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 nat (f :: Type -> Type) (n :: nat) a b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
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, PeanoOrder nat, SingI (n :: nat))
      => CPointed (Sized f n) where
  cpure :: a -> Sized f n a
cpure = a -> Sized f n a
forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, SingI 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 nat (f :: Type -> Type) (n :: nat) a b.
(Dom f a, CZip f, Dom f b, Dom f (a, b)) =>
Sized f n a -> Sized f n b -> Sized f n (a, b)
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 nat (f :: Type -> Type) (n :: nat) a b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
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
  (PeanoOrder nat, SingI (n :: nat), CZip f, CFreeMonoid f)
  => CRepeat (Sized f n) where
  crepeat :: a -> Sized f n a
crepeat = a -> Sized f n a
forall nat (f :: Type -> Type) (n :: nat) a.
(HasOrdinal nat, SingI 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) nat (n :: nat) a. Sized f n a -> f a
runSized
  {-# INLINE ctraverse #-}