{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE NoStarIsType #-}
{-# OPTIONS_GHC -fenable-rewrite-rules #-}
{-# OPTIONS_GHC -fno-warn-type-defaults -fno-warn-orphans #-}
{-# OPTIONS_GHC -fplugin Data.Type.Natural.Presburger.MinMaxSolver #-}
module Data.Sized
(
Sized (),
SomeSized (..),
DomC (),
length,
sLength,
null,
(!!),
(%!!),
index,
sIndex,
head,
last,
uncons,
uncons',
Uncons (..),
unsnoc,
unsnoc',
Unsnoc (..),
tail,
init,
take,
takeAtMost,
drop,
splitAt,
splitAtMost,
empty,
singleton,
toSomeSized,
replicate,
replicate',
generate,
generate',
cons,
(<|),
snoc,
(|>),
append,
(++),
concat,
zip,
zipSame,
zipWith,
zipWithSame,
unzip,
unzipWith,
map,
reverse,
intersperse,
nub,
sort,
sortBy,
insert,
insertBy,
toList,
fromList,
fromList',
unsafeFromList,
unsafeFromList',
fromListWithDefault,
fromListWithDefault',
unsized,
toSized,
toSized',
unsafeToSized,
unsafeToSized',
toSizedWithDefault,
toSizedWithDefault',
Partitioned (..),
takeWhile,
dropWhile,
span,
break,
partition,
elem,
notElem,
find,
findIndex,
sFindIndex,
findIndices,
sFindIndices,
elemIndex,
sElemIndex,
sUnsafeElemIndex,
elemIndices,
sElemIndices,
viewCons,
ConsView (..),
viewSnoc,
SnocView (..),
pattern Nil,
pattern (:<),
pattern (:>),
)
where
import Control.Applicative (ZipList (..), (<*>))
import Control.Subcategory
( CApplicative (..),
CFoldable (..),
CFreeMonoid (..),
CFunctor (..),
CPointed (..),
CRepeat (..),
CSemialign (..),
CTraversable (..),
CUnzip (..),
CZip (..),
Constrained (Dom),
cfromList,
ctoList,
)
import Data.Coerce (coerce)
import Data.Constraint (Dict (..), withDict)
import qualified Data.Foldable as F
import Data.Kind (Type)
import qualified Data.List as L
import Data.Maybe (fromJust)
import Data.Monoid (Monoid (..), (<>))
import qualified Data.Sequence as Seq
import Data.Sized.Internal
import Data.These (These (..))
import Data.Type.Equality (gcastWith, (:~:) (..))
import Data.Type.Natural
import Data.Type.Ordinal (Ordinal (..), ordToNatural)
import Data.Typeable (Typeable)
import qualified Data.Vector as V
import qualified Data.Vector.Storable as SV
import qualified Data.Vector.Unboxed as UV
import Unsafe.Coerce (unsafeCoerce)
import Prelude
( Bool (..),
Enum (..),
Eq (..),
Functor,
Int,
Maybe (..),
Num (..),
Ord (..),
Ordering,
Show (..),
const,
flip,
fmap,
fromIntegral,
uncurry,
($),
(.),
)
import qualified Prelude as P
data SomeSized f a where
SomeSized ::
SNat n ->
Sized f n a ->
SomeSized f a
deriving instance Typeable SomeSized
instance Show (f a) => Show (SomeSized f a) where
showsPrec :: Int -> SomeSized f a -> ShowS
showsPrec Int
d (SomeSized SNat n
_ Sized f n a
s) =
Bool -> ShowS -> ShowS
P.showParen (Int
d forall a. Ord a => a -> a -> Bool
> Int
9) forall a b. (a -> b) -> a -> b
$
String -> ShowS
P.showString String
"SomeSized _ " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => Int -> a -> ShowS
showsPrec Int
10 Sized f n a
s
instance Eq (f a) => Eq (SomeSized f a) where
(SomeSized SNat n
_ (Sized f a
xs)) == :: SomeSized f a -> SomeSized f a -> Bool
== (SomeSized SNat n
_ (Sized f a
ys)) = f a
xs forall a. Eq a => a -> a -> Bool
== f a
ys
length ::
forall f (n :: Nat) a.
(Dom f a, KnownNat n) =>
Sized f n a ->
Int
length :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, KnownNat n) =>
Sized f n a -> Int
length = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
fromSNat forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n
{-# INLINE CONLIKE [1] length #-}
lengthTLZero :: Sized f 0 a -> Int
lengthTLZero :: forall (f :: Type -> Type) a. Sized f 0 a -> Int
lengthTLZero = forall a b. a -> b -> a
P.const Int
0
{-# INLINE lengthTLZero #-}
{-# RULES
"length/0" [~1] length = lengthTLZero
#-}
sLength ::
forall f (n :: Nat) a.
(Dom f a, KnownNat n) =>
Sized f n a ->
SNat n
sLength :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, KnownNat n) =>
Sized f n a -> SNat n
sLength Sized f n a
_ = forall (n :: Nat). KnownNat n => SNat n
sNat @n
{-# INLINE [2] sLength #-}
null ::
forall f (n :: Nat) a.
(CFoldable f, Dom f a) =>
Sized f n a ->
Bool
null :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
Sized f n a -> Bool
null = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> Bool
cnull @f @a
{-# INLINE CONLIKE [2] null #-}
nullTL0 :: Sized f 0 a -> Bool
nullTL0 :: forall (f :: Type -> Type) a. Sized f 0 a -> Bool
nullTL0 = forall a b. a -> b -> a
P.const Bool
True
{-# INLINE nullTL0 #-}
nullPeanoSucc :: Sized f (S n) a -> Bool
nullPeanoSucc :: forall (f :: Type -> Type) (n :: Nat) a. Sized f (S n) a -> Bool
nullPeanoSucc = forall a b. a -> b -> a
P.const Bool
False
{-# INLINE nullPeanoSucc #-}
nullTLSucc :: Sized f (n + 1) a -> Bool
nullTLSucc :: forall (f :: Type -> Type) (n :: Nat) a. Sized f (S n) a -> Bool
nullTLSucc = forall a b. a -> b -> a
P.const Bool
False
{-# INLINE nullTLSucc #-}
{-# RULES
"null/0" [~2] null = nullTL0
"null/0" [~2] null = nullTLSucc
"null/0" [~1] forall (vec :: 1 <= n => Sized f n a).
null vec =
False
"null/Sn" [~2] null = nullPeanoSucc
#-}
(!!) ::
forall f (m :: Nat) a.
(CFoldable f, Dom f a, (1 <= m)) =>
Sized f m a ->
Int ->
a
!! :: forall (f :: Type -> Type) (m :: Nat) a.
(CFoldable f, Dom f a, 1 <= m) =>
Sized f m a -> Int -> a
(!!) = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Dom f a) =>
f a -> Int -> a
cindex @f @a
{-# INLINE (!!) #-}
(%!!) ::
forall f (n :: Nat) c.
(CFoldable f, Dom f c) =>
Sized f n c ->
Ordinal n ->
c
%!! :: forall (f :: Type -> Type) (n :: Nat) c.
(CFoldable f, Dom f c) =>
Sized f n c -> Ordinal n -> c
(%!!) = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ (forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). Ordinal n -> Nat
ordToNatural)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) a.
(CFoldable f, Dom f a) =>
f a -> Int -> a
cindex @f @c
{-# INLINE (%!!) #-}
{-# SPECIALIZE (%!!) :: Sized [] (n :: Nat) a -> Ordinal n -> a #-}
{-# SPECIALIZE (%!!) :: Sized V.Vector (n :: Nat) a -> Ordinal n -> a #-}
{-# SPECIALIZE (%!!) :: UV.Unbox a => Sized UV.Vector (n :: Nat) a -> Ordinal n -> a #-}
{-# SPECIALIZE (%!!) :: SV.Storable a => Sized SV.Vector (n :: Nat) a -> Ordinal n -> a #-}
{-# SPECIALIZE (%!!) :: Sized Seq.Seq (n :: Nat) a -> Ordinal n -> a #-}
index ::
forall f (m :: Nat) a.
(CFoldable f, Dom f a, (1 <= m)) =>
Int ->
Sized f m a ->
a
index :: forall (f :: Type -> Type) (m :: Nat) a.
(CFoldable f, Dom f a, 1 <= m) =>
Int -> Sized f m a -> a
index = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (f :: Type -> Type) (m :: Nat) a.
(CFoldable f, Dom f a, 1 <= m) =>
Sized f m a -> Int -> a
(!!)
{-# INLINE index #-}
sIndex ::
forall f (n :: Nat) c.
(CFoldable f, Dom f c) =>
Ordinal n ->
Sized f n c ->
c
sIndex :: forall (f :: Type -> Type) (n :: Nat) c.
(CFoldable f, Dom f c) =>
Ordinal n -> Sized f n c -> c
sIndex = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) c.
(CFoldable f, Dom f c) =>
Sized f n c -> Ordinal n -> c
(%!!) @f @n @c
{-# INLINE sIndex #-}
head ::
forall f (n :: Nat) a.
(CFoldable f, Dom f a, (0 < n)) =>
Sized f n a ->
a
head :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, 0 < n) =>
Sized f n a -> a
head = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> a
chead @f @a
{-# INLINE head #-}
last ::
forall f (n :: Nat) a.
((0 < n), CFoldable f, Dom f a) =>
Sized f n a ->
a
last :: forall (f :: Type -> Type) (n :: Nat) a.
(0 < n, CFoldable f, Dom f a) =>
Sized f n a -> a
last = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> a
clast @f @a
{-# INLINE last #-}
uncons ::
forall f (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a, (1 <= n)) =>
Sized f n a ->
Uncons f n a
uncons :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a, 1 <= n) =>
Sized f n a -> Uncons f n a
uncons =
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat
(forall (n :: Nat). SNat n -> SNat (Pred n)
sPred forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n)
forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall (f :: Type -> Type) (n :: Nat) a.
KnownNat n =>
a -> Sized f n a -> Uncons f (1 + n) a
Uncons @f @(Pred n) @a) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
f a -> Maybe (a, f a)
cuncons @f @a)
uncons' ::
forall f (n :: Nat) a proxy.
(KnownNat n, CFreeMonoid f, Dom f a) =>
proxy n ->
Sized f (Succ n) a ->
Uncons f (Succ n) a
uncons' :: forall (f :: Type -> Type) (n :: Nat) a (proxy :: Nat -> Type).
(KnownNat n, CFreeMonoid f, Dom f a) =>
proxy n -> Sized f (Succ n) a -> Uncons f (Succ n) a
uncons' proxy n
_ =
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n) forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a, 1 <= n) =>
Sized f n a -> Uncons f n a
uncons
{-# INLINE uncons' #-}
data Uncons f (n :: Nat) a where
Uncons ::
forall f (n :: Nat) a.
KnownNat n =>
a ->
Sized f n a ->
Uncons f (1 + n) a
unsnoc ::
forall f (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a, (0 < n)) =>
Sized f n a ->
Unsnoc f n a
unsnoc :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a, 0 < n) =>
Sized f n a -> Unsnoc f n a
unsnoc =
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat
(forall (n :: Nat). SNat n -> SNat (Pred n)
sPred forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n)
forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (forall (f :: Type -> Type) (n :: Nat) a.
Sized f n a -> a -> Unsnoc f (Succ n) a
Unsnoc @f @(Pred n)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall a. HasCallStack => Maybe a -> a
fromJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
f a -> Maybe (f a, a)
cunsnoc @f @a)
{-# NOINLINE [1] unsnoc #-}
data Unsnoc f n a where
Unsnoc :: forall f n a. Sized f (n :: Nat) a -> a -> Unsnoc f (Succ n) a
unsnoc' ::
forall f (n :: Nat) a proxy.
(KnownNat n, CFreeMonoid f, Dom f a) =>
proxy n ->
Sized f (Succ n) a ->
Unsnoc f (Succ n) a
unsnoc' :: forall (f :: Type -> Type) (n :: Nat) a (proxy :: Nat -> Type).
(KnownNat n, CFreeMonoid f, Dom f a) =>
proxy n -> Sized f (Succ n) a -> Unsnoc f (Succ n) a
unsnoc' proxy n
_ =
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (forall (n :: Nat). SNat n -> SNat (Succ n)
sSucc forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n) forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a, 0 < n) =>
Sized f n a -> Unsnoc f n a
unsnoc
{-# INLINE unsnoc' #-}
tail ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f (1 + n) a ->
Sized f n a
tail :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f (1 + n) a -> Sized f n a
tail = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
f a -> f a
ctail @f @a
{-# INLINE tail #-}
init ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f (n + 1) a ->
Sized f n a
init :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f (n + 1) a -> Sized f n a
init = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
f a -> f a
cinit @f @a
{-# INLINE init #-}
take ::
forall (n :: Nat) f (m :: Nat) a.
(CFreeMonoid f, Dom f a, (n <= m)) =>
SNat n ->
Sized f m a ->
Sized f n a
take :: forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(CFreeMonoid f, Dom f a, n <= m) =>
SNat n -> Sized f m a -> Sized f n a
take = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake @f @a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SNat n -> Nat
fromSNat @n
{-# INLINE take #-}
takeAtMost ::
forall (n :: Nat) f m a.
(CFreeMonoid f, Dom f a) =>
SNat n ->
Sized f m a ->
Sized f (Min n m) a
takeAtMost :: forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> Sized f m a -> Sized f (Min n m) a
takeAtMost = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake @f @a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SNat n -> Nat
fromSNat @n
{-# INLINE takeAtMost #-}
drop ::
forall (n :: Nat) f (m :: Nat) a.
(CFreeMonoid f, Dom f a, (n <= m)) =>
SNat n ->
Sized f m a ->
Sized f (m - n) a
drop :: forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(CFreeMonoid f, Dom f a, n <= m) =>
SNat n -> Sized f m a -> Sized f (m - n) a
drop = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
cdrop @f @a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SNat n -> Nat
fromSNat @n
{-# INLINE drop #-}
splitAt ::
forall (n :: Nat) f m a.
(CFreeMonoid f, Dom f a, (n <= m)) =>
SNat n ->
Sized f m a ->
(Sized f n a, Sized f (m -. n) a)
splitAt :: forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(CFreeMonoid f, Dom f a, n <= m) =>
SNat n -> Sized f m a -> (Sized f n a, Sized f (m -. n) a)
splitAt =
coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> (f a, f a)
csplitAt @f @a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SNat n -> Nat
fromSNat @n
{-# INLINE splitAt #-}
splitAtMost ::
forall (n :: Nat) f (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n ->
Sized f m a ->
(Sized f (Min n m) a, Sized f (m -. n) a)
splitAtMost :: forall (n :: Nat) (f :: Type -> Type) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> Sized f m a -> (Sized f (Min n m) a, Sized f (m -. n) a)
splitAtMost =
coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> (f a, f a)
csplitAt @f @a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SNat n -> Nat
fromSNat @n
{-# INLINE splitAtMost #-}
empty ::
forall f a.
(Monoid (f a), Dom f a) =>
Sized f (0) a
empty :: forall (f :: Type -> Type) a.
(Monoid (f a), Dom f a) =>
Sized f 0 a
empty = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => a
mempty @(f a)
{-# INLINE empty #-}
singleton :: forall f a. (CPointed f, Dom f a) => a -> Sized f (1) a
singleton :: forall (f :: Type -> Type) a.
(CPointed f, Dom f a) =>
a -> Sized f 1 a
singleton = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. (CPointed f, Dom f a) => a -> f a
cpure @f @a
{-# INLINE singleton #-}
toSomeSized ::
forall f a.
(Dom f a, CFoldable f) =>
f a ->
SomeSized f a
{-# INLINE toSomeSized #-}
toSomeSized :: forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized = \f a
xs ->
case Nat -> SomeSNat
toSomeSNat forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> Int
clength f a
xs of
SomeSNat SNat n
sn -> forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) (f :: Type -> Type) a.
SNat n -> Sized f n a -> SomeSized f a
SomeSized SNat n
sn forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a.
SNat n -> f a -> Sized f n a
unsafeToSized SNat n
sn f a
xs
replicate ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n ->
a ->
Sized f n a
replicate :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> Sized f n a
replicate = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> a -> f a
creplicate @f @a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat). SNat n -> Nat
fromSNat @n
{-# INLINE replicate #-}
replicate' ::
forall f (n :: Nat) a.
(KnownNat (n :: Nat), CFreeMonoid f, Dom f a) =>
a ->
Sized f n a
replicate' :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> Sized f n a
replicate' = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> Sized f n a
replicate (forall (n :: Nat). KnownNat n => SNat n
sNat @n)
{-# INLINE replicate' #-}
generate ::
forall f (n :: Nat) (a :: Type).
(CFreeMonoid f, Dom f a) =>
SNat n ->
(Ordinal n -> a) ->
Sized f n a
generate :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> (Ordinal n -> a) -> Sized f n a
generate = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ \SNat n
sn ->
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
sn forall a b. (a -> b) -> a -> b
$
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> (Int -> a) -> f a
cgenerate @f @a (forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
fromSNat @n SNat n
sn)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => Int -> a
toEnum @(Ordinal n))
{-# INLINE [1] generate #-}
generate' ::
forall f (n :: Nat) (a :: Type).
(KnownNat n, CFreeMonoid f, Dom f a) =>
(Ordinal n -> a) ->
Sized f n a
generate' :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
(Ordinal n -> a) -> Sized f n a
generate' = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> (Ordinal n -> a) -> Sized f n a
generate forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE [1] generate' #-}
genVector ::
forall (n :: Nat) a.
SNat n ->
(Ordinal n -> a) ->
Sized V.Vector n a
genVector :: forall (n :: Nat) a. SNat n -> (Ordinal n -> a) -> Sized Vector n a
genVector SNat n
n Ordinal n -> a
f = forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$ forall a. Int -> (Int -> a) -> Vector a
V.generate (forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
n) (Ordinal n -> a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => Int -> a
toEnum)
{-# INLINE genVector #-}
genSVector ::
forall (n :: Nat) a.
(SV.Storable a) =>
SNat n ->
(Ordinal n -> a) ->
Sized SV.Vector n a
genSVector :: forall (n :: Nat) a.
Storable a =>
SNat n -> (Ordinal n -> a) -> Sized Vector n a
genSVector SNat n
n Ordinal n -> a
f = forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$ forall a. Storable a => Int -> (Int -> a) -> Vector a
SV.generate (forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
n) (Ordinal n -> a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => Int -> a
toEnum)
{-# INLINE genSVector #-}
genSeq ::
forall (n :: Nat) a.
SNat n ->
(Ordinal n -> a) ->
Sized Seq.Seq n a
genSeq :: forall (n :: Nat) a. SNat n -> (Ordinal n -> a) -> Sized Seq n a
genSeq SNat n
n Ordinal n -> a
f = forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n
n forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$ forall a. Int -> (Int -> a) -> Seq a
Seq.fromFunction (forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
n) (Ordinal n -> a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Enum a => Int -> a
toEnum)
{-# INLINE genSeq #-}
{-# RULES
"generate/Vector" [~1] generate = genVector
"generate/SVector" [~1] forall
(n :: SNat (n :: Nat))
(f :: SV.Storable a => Ordinal n -> a).
generate n f =
genSVector n f
"generate/UVector" [~1] forall
(n :: SNat (n :: Nat))
(f :: UV.Unbox a => Ordinal n -> a).
generate n f =
withKnownNat n $ Sized (UV.generate (P.fromIntegral $ fromSNat n) (f . toEnum))
"generate/Seq" [~1] generate = genSeq
#-}
cons ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a ->
Sized f n a ->
Sized f (1 + n) a
cons :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (1 + n) a
cons = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
a -> f a -> f a
ccons @f @a
{-# INLINE cons #-}
(<|) ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a ->
Sized f n a ->
Sized f (1 + n) a
<| :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (1 + n) a
(<|) = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (1 + n) a
cons
{-# INLINE (<|) #-}
infixr 5 <|
snoc ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a ->
a ->
Sized f (n + 1) a
snoc :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + 1) a
snoc (Sized f a
xs) a
a = forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
f a -> a -> f a
csnoc f a
xs a
a
{-# INLINE snoc #-}
(|>) ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a ->
a ->
Sized f (n + 1) a
|> :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + 1) a
(|>) = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + 1) a
snoc
{-# INLINE (|>) #-}
infixl 5 |>
append ::
forall f (n :: Nat) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a ->
Sized f m a ->
Sized f (n + m) a
append :: forall (f :: Type -> Type) (n :: Nat) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> Sized f m a -> Sized f (n + m) a
append = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall a. Monoid a => a -> a -> a
mappend @(f a)
{-# INLINE append #-}
(++) ::
forall f (n :: Nat) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a ->
Sized f m a ->
Sized f (n + m) a
++ :: forall (f :: Type -> Type) (n :: Nat) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> Sized f m a -> Sized f (n + m) a
(++) = forall (f :: Type -> Type) (n :: Nat) (m :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> Sized f m a -> Sized f (n + m) a
append
infixr 5 ++
concat ::
forall f' (m :: Nat) f (n :: Nat) a.
( CFreeMonoid f
, CFunctor f'
, CFoldable f'
, Dom f a
, Dom f' (f a)
, Dom f' (Sized f n a)
) =>
Sized f' m (Sized f n a) ->
Sized f (m * n) a
concat :: forall (f' :: Type -> Type) (m :: Nat) (f :: Type -> Type)
(n :: Nat) a.
(CFreeMonoid f, CFunctor f', CFoldable f', Dom f a, Dom f' (f a),
Dom f' (Sized f n a)) =>
Sized f' m (Sized f n a) -> Sized f (m * n) a
concat = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a w.
(CFoldable f, Dom f a, Monoid w) =>
(a -> w) -> f a -> w
cfoldMap @f' @(Sized f n a) forall (f :: Type -> Type) (n :: Nat) a. Sized f n a -> f a
runSized
{-# INLINE [2] concat #-}
zip ::
forall f (n :: Nat) a (m :: Nat) b.
(Dom f a, CZip f, Dom f b, Dom f (a, b)) =>
Sized f n a ->
Sized f m b ->
Sized f (Min n m) (a, b)
zip :: forall (f :: Type -> Type) (n :: Nat) a (m :: Nat) b.
(Dom f a, CZip f, Dom f b, Dom f (a, b)) =>
Sized f n a -> Sized f m b -> Sized f (Min n m) (a, b)
zip = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b.
(CZip f, Dom f a, Dom f b, Dom f (a, b)) =>
f a -> f b -> f (a, b)
czip @f @a @b
zipSame ::
forall f (n :: Nat) a b.
(Dom f a, CZip f, Dom f b, Dom f (a, b)) =>
Sized f n a ->
Sized f n b ->
Sized f n (a, b)
zipSame :: forall (f :: Type -> Type) (n :: Nat) a b.
(Dom f a, CZip f, Dom f b, Dom f (a, b)) =>
Sized f n a -> Sized f n b -> Sized f n (a, b)
zipSame = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b.
(CZip f, Dom f a, Dom f b, Dom f (a, b)) =>
f a -> f b -> f (a, b)
czip @f @a @b
{-# INLINE [1] zipSame #-}
zipWith ::
forall f (n :: Nat) a (m :: Nat) b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) ->
Sized f n a ->
Sized f m b ->
Sized f (Min n m) c
zipWith :: forall (f :: Type -> Type) (n :: Nat) a (m :: Nat) b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) -> Sized f n a -> Sized f m b -> Sized f (Min n m) c
zipWith = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b c.
(CZip f, Dom f a, Dom f b, Dom f c) =>
(a -> b -> c) -> f a -> f b -> f c
czipWith @f @a @b @c
{-# INLINE [1] zipWith #-}
zipWithSame ::
forall f (n :: Nat) a b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) ->
Sized f n a ->
Sized f n b ->
Sized f n c
zipWithSame :: forall (f :: Type -> Type) (n :: Nat) a b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
zipWithSame = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b c.
(CZip f, Dom f a, Dom f b, Dom f c) =>
(a -> b -> c) -> f a -> f b -> f c
czipWith @f @a @b @c
{-# INLINE [1] zipWithSame #-}
unzip ::
forall f (n :: Nat) a b.
(CUnzip f, Dom f a, Dom f b, Dom f (a, b)) =>
Sized f n (a, b) ->
(Sized f n a, Sized f n b)
unzip :: forall (f :: Type -> Type) (n :: Nat) a b.
(CUnzip f, Dom f a, Dom f b, Dom f (a, b)) =>
Sized f n (a, b) -> (Sized f n a, Sized f n b)
unzip = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b.
(CUnzip f, Dom f (a, b), Dom f a, Dom f b) =>
f (a, b) -> (f a, f b)
cunzip @f @a @b
{-# INLINE unzip #-}
unzipWith ::
forall f (n :: Nat) a b c.
(CUnzip f, Dom f a, Dom f b, Dom f c) =>
(a -> (b, c)) ->
Sized f n a ->
(Sized f n b, Sized f n c)
unzipWith :: forall (f :: Type -> Type) (n :: Nat) a b c.
(CUnzip f, Dom f a, Dom f b, Dom f c) =>
(a -> (b, c)) -> Sized f n a -> (Sized f n b, Sized f n c)
unzipWith = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) c a b.
(CUnzip f, Dom f c, Dom f a, Dom f b) =>
(c -> (a, b)) -> f c -> (f a, f b)
cunzipWith @f @a @b @c
{-# INLINE unzipWith #-}
map ::
forall f (n :: Nat) a b.
(CFreeMonoid f, Dom f a, Dom f b) =>
(a -> b) ->
Sized f n a ->
Sized f n b
map :: forall (f :: Type -> Type) (n :: Nat) a b.
(CFreeMonoid f, Dom f a, Dom f b) =>
(a -> b) -> Sized f n a -> Sized f n b
map a -> b
f = forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) a b.
(CFunctor f, Dom f a, Dom f b) =>
(a -> b) -> f a -> f b
cmap a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) (n :: Nat) a. Sized f n a -> f a
runSized
{-# INLINE map #-}
reverse ::
forall f (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
Sized f n a ->
Sized f n a
reverse :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
Sized f n a -> Sized f n a
reverse = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
f a -> f a
creverse @f @a
{-# INLINE reverse #-}
intersperse ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a ->
Sized f n a ->
Sized f ((2 * n) -. 1) a
intersperse :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f ((2 * n) -. 1) a
intersperse = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
a -> f a -> f a
cintersperse @f @a
{-# INLINE intersperse #-}
nub ::
forall f (n :: Nat) a.
(Dom f a, Eq a, CFreeMonoid f) =>
Sized f n a ->
SomeSized f a
nub :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, Eq a, CFreeMonoid f) =>
Sized f n a -> SomeSized f a
nub = forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a, Eq a) =>
f a -> f a
cnub @f @a)
sort ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a, Ord a) =>
Sized f n a ->
Sized f n a
sort :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a, Ord a) =>
Sized f n a -> Sized f n a
sort = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a, Ord a) =>
f a -> f a
csort @f @a
sortBy ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> a -> Ordering) ->
Sized f n a ->
Sized f n a
sortBy :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> a -> Ordering) -> Sized f n a -> Sized f n a
sortBy = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> a -> Ordering) -> f a -> f a
csortBy @f @a
insert ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a, Ord a) =>
a ->
Sized f n a ->
Sized f (Succ n) a
insert :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a, Ord a) =>
a -> Sized f n a -> Sized f (Succ n) a
insert = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a, Ord a) =>
a -> f a -> f a
cinsert @f @a
insertBy ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> a -> Ordering) ->
a ->
Sized f n a ->
Sized f (Succ n) a
insertBy :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> a -> Ordering) -> a -> Sized f n a -> Sized f (Succ n) a
insertBy = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> a -> Ordering) -> a -> f a -> f a
cinsertBy @f @a
toList ::
forall f (n :: Nat) a.
(CFoldable f, Dom f a) =>
Sized f n a ->
[a]
toList :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
Sized f n a -> [a]
toList = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> [a]
ctoList @f @a
{-# INLINE [2] toList #-}
{-# RULES
"toList/List"
Data.Sized.toList =
runSized
#-}
fromList ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n ->
[a] ->
Maybe (Sized f n a)
fromList :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> [a] -> Maybe (Sized f n a)
fromList SNat n
Zero [a]
_ = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized (forall a. Monoid a => a
mempty :: f a)
fromList SNat n
sn [a]
xs =
let len :: Int
len = forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
sn
in if forall (t :: Type -> Type) a. Foldable t => t a -> Int
P.length [a]
xs forall a. Ord a => a -> a -> Bool
< Int
len
then forall a. Maybe a
Nothing
else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake Int
len forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
[a] -> f a
cfromList [a]
xs
{-# INLINEABLE [2] fromList #-}
fromList' ::
forall f (n :: Nat) a.
(Dom f a, CFreeMonoid f, KnownNat n) =>
[a] ->
Maybe (Sized f n a)
fromList' :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f, KnownNat n) =>
[a] -> Maybe (Sized f n a)
fromList' = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> [a] -> Maybe (Sized f n a)
fromList forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE fromList' #-}
unsafeFromList ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n ->
[a] ->
Sized f n a
unsafeFromList :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> [a] -> Sized f n a
unsafeFromList = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
[a] -> f a
cfromList @f @a
{-# INLINE [1] unsafeFromList #-}
unsafeFromList' ::
forall f (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
[a] ->
Sized f n a
unsafeFromList' :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
[a] -> Sized f n a
unsafeFromList' = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> [a] -> Sized f n a
unsafeFromList forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE [1] unsafeFromList' #-}
{-# RULES
"unsafeFromList'/List" [~1]
unsafeFromList' =
Sized
"unsafeFromList'/Vector" [~1]
unsafeFromList' =
Sized . V.fromList
"unsafeFromList'/Seq" [~1]
unsafeFromList' =
Sized . Seq.fromList
"unsafeFromList'/SVector" [~1] forall (xs :: SV.Storable a => [a]).
unsafeFromList' xs =
Sized (SV.fromList xs)
"unsafeFromList'/UVector" [~1] forall (xs :: UV.Unbox a => [a]).
unsafeFromList' xs =
Sized (UV.fromList xs)
#-}
fromListWithDefault ::
forall f (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
SNat n ->
a ->
[a] ->
Sized f n a
fromListWithDefault :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
SNat n -> a -> [a] -> Sized f n a
fromListWithDefault SNat n
sn a
def [a]
xs =
let len :: Int
len = forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
sn
in forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$
forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
[a] -> f a
cfromList (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake Int
len [a]
xs)
forall a. Semigroup a => a -> a -> a
<> forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> a -> f a
creplicate (Int
len forall a. Num a => a -> a -> a
- forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> Int
clength [a]
xs) a
def
{-# INLINEABLE fromListWithDefault #-}
fromListWithDefault' ::
forall f (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a ->
[a] ->
Sized f n a
fromListWithDefault' :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> [a] -> Sized f n a
fromListWithDefault' = forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
SNat n -> a -> [a] -> Sized f n a
fromListWithDefault forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE fromListWithDefault' #-}
unsized :: forall f (n :: Nat) a. Sized f n a -> f a
unsized :: forall (f :: Type -> Type) (n :: Nat) a. Sized f n a -> f a
unsized = forall (f :: Type -> Type) (n :: Nat) a. Sized f n a -> f a
runSized
{-# INLINE unsized #-}
toSized ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat (n :: Nat) ->
f a ->
Maybe (Sized f n a)
toSized :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> f a -> Maybe (Sized f n a)
toSized SNat n
sn f a
xs =
let len :: Int
len = forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
sn
in if forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> Int
clength f a
xs forall a. Ord a => a -> a -> Bool
< Int
len
then forall a. Maybe a
Nothing
else forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) (n :: Nat) a.
SNat n -> f a -> Sized f n a
unsafeToSized SNat n
sn forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake Int
len f a
xs
{-# INLINEABLE [2] toSized #-}
toSized' ::
forall f (n :: Nat) a.
(Dom f a, CFreeMonoid f, KnownNat n) =>
f a ->
Maybe (Sized f n a)
toSized' :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f, KnownNat n) =>
f a -> Maybe (Sized f n a)
toSized' = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> f a -> Maybe (Sized f n a)
toSized forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE toSized' #-}
unsafeToSized :: forall f (n :: Nat) a. SNat n -> f a -> Sized f n a
unsafeToSized :: forall (f :: Type -> Type) (n :: Nat) a.
SNat n -> f a -> Sized f n a
unsafeToSized SNat n
_ = forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized
{-# INLINE [2] unsafeToSized #-}
unsafeToSized' ::
forall f (n :: Nat) a.
(KnownNat n, Dom f a) =>
f a ->
Sized f n a
unsafeToSized' :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, Dom f a) =>
f a -> Sized f n a
unsafeToSized' = forall (f :: Type -> Type) (n :: Nat) a.
SNat n -> f a -> Sized f n a
unsafeToSized forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE unsafeToSized' #-}
toSizedWithDefault ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat (n :: Nat) ->
a ->
f a ->
Sized f n a
toSizedWithDefault :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> f a -> Sized f n a
toSizedWithDefault SNat n
sn a
def f a
xs =
let len :: Int
len = forall a b. (Integral a, Num b) => a -> b
P.fromIntegral forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
sn
in forall (f :: Type -> Type) (n :: Nat) a. f a -> Sized f n a
Sized forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> f a -> f a
ctake Int
len f a
xs forall a. Semigroup a => a -> a -> a
<> forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
Int -> a -> f a
creplicate (Int
len forall a. Num a => a -> a -> a
- forall (f :: Type -> Type) a. (CFoldable f, Dom f a) => f a -> Int
clength f a
xs) a
def
{-# INLINEABLE toSizedWithDefault #-}
toSizedWithDefault' ::
forall f (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a ->
f a ->
Sized f n a
toSizedWithDefault' :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> f a -> Sized f n a
toSizedWithDefault' = forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
SNat n -> a -> f a -> Sized f n a
toSizedWithDefault forall (n :: Nat). KnownNat n => SNat n
sNat
{-# INLINE toSizedWithDefault' #-}
data Partitioned f n a where
Partitioned ::
(Dom f a) =>
SNat n ->
Sized f n a ->
SNat m ->
Sized f m a ->
Partitioned f (n + m) a
takeWhile ::
forall f (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
(a -> Bool) ->
Sized f n a ->
SomeSized f a
takeWhile :: forall (f :: Type -> Type) (n :: Nat) a.
(Dom f a, CFreeMonoid f) =>
(a -> Bool) -> Sized f n a -> SomeSized f a
takeWhile = (forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> f a -> f a
ctakeWhile @f @a)
{-# INLINE takeWhile #-}
dropWhile ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) ->
Sized f n a ->
SomeSized f a
dropWhile :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> SomeSized f a
dropWhile = (forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> f a -> f a
cdropWhile @f @a)
{-# INLINE dropWhile #-}
span ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) ->
Sized f n a ->
Partitioned f n a
span :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Partitioned f n a
span = (forall (n :: Nat) (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned @n forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> f a -> (f a, f a)
cspan @f @a)
{-# INLINE span #-}
break ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) ->
Sized f n a ->
Partitioned f n a
break :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Partitioned f n a
break = (forall (n :: Nat) (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned @n forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> f a -> (f a, f a)
cbreak @f @a)
{-# INLINE break #-}
partition ::
forall f (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) ->
Sized f n a ->
Partitioned f n a
partition :: forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Partitioned f n a
partition = (forall (n :: Nat) (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned @n forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(a -> Bool) -> f a -> (f a, f a)
cpartition @f @a)
{-# INLINE partition #-}
unsafePartitioned ::
forall (n :: Nat) f a.
(CFreeMonoid f, Dom f a) =>
(f a, f a) ->
Partitioned f n a
unsafePartitioned :: forall (n :: Nat) (f :: Type -> Type) a.
(CFreeMonoid f, Dom f a) =>
(f a, f a) -> Partitioned f n a
unsafePartitioned (f a
l, f a
r) =
case (forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized f a
l, forall (f :: Type -> Type) a.
(Dom f a, CFoldable f) =>
f a -> SomeSized f a
toSomeSized f a
r) of
( SomeSized (SNat n
lenL :: SNat nl) Sized f n a
ls
, SomeSized (SNat n
lenR :: SNat nr) Sized f n a
rs
) ->
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith
( forall a b. a -> b
unsafeCoerce forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k). a :~: a
Refl @() ::
n :~: nl + nr
)
forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a (n :: Nat) (m :: Nat).
Dom f a =>
SNat n
-> Sized f n a -> SNat m -> Sized f m a -> Partitioned f (n + m) a
Partitioned SNat n
lenL Sized f n a
ls SNat n
lenR Sized f n a
rs
elem ::
forall f (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a ->
Sized f n a ->
Bool
elem :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Bool
elem = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Eq a, Dom f a) =>
a -> f a -> Bool
celem @f @a
{-# INLINE elem #-}
notElem ::
forall f (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a ->
Sized f n a ->
Bool
notElem :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Bool
notElem = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Eq a, Dom f a) =>
a -> f a -> Bool
cnotElem @f @a
{-# INLINE notElem #-}
find ::
forall f (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) ->
Sized f n a ->
Maybe a
find :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Maybe a
find = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> f a -> Maybe a
cfind @f @a
{-# INLINE [1] find #-}
{-# RULES
"find/List" [~1] forall p.
find p =
L.find @[] p . runSized
"find/Vector" [~1] forall p.
find p =
V.find p . runSized
"find/Storable Vector" [~1] forall (p :: SV.Storable a => a -> Bool).
find p =
SV.find p . runSized
"find/Unboxed Vector" [~1] forall (p :: UV.Unbox a => a -> Bool).
find p =
UV.find p . runSized
#-}
findIndex ::
forall f (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) ->
Sized f n a ->
Maybe Int
findIndex :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Maybe Int
findIndex = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> f a -> Maybe Int
cfindIndex @f @a
{-# INLINE findIndex #-}
sFindIndex ::
forall f (n :: Nat) a.
(KnownNat (n :: Nat), CFoldable f, Dom f a) =>
(a -> Bool) ->
Sized f n a ->
Maybe (Ordinal n)
sFindIndex :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> Maybe (Ordinal n)
sFindIndex = (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Enum a => Int -> a
toEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> f a -> Maybe Int
cfindIndex @f @a)
{-# INLINE sFindIndex #-}
findIndices ::
forall f (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) ->
Sized f n a ->
[Int]
findIndices :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> [Int]
findIndices = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> f a -> [Int]
cfindIndices @f @a
{-# INLINE findIndices #-}
{-# SPECIALIZE findIndices :: (a -> Bool) -> Sized [] n a -> [Int] #-}
sFindIndices ::
forall f (n :: Nat) a.
(CFoldable f, Dom f a, KnownNat (n :: Nat)) =>
(a -> Bool) ->
Sized f n a ->
[Ordinal n]
sFindIndices :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, KnownNat n) =>
(a -> Bool) -> Sized f n a -> [Ordinal n]
sFindIndices a -> Bool
p = forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
P.fmap (forall a. Enum a => Int -> a
toEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (Integral a, Num b) => a -> b
P.fromIntegral) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a) =>
(a -> Bool) -> Sized f n a -> [Int]
findIndices a -> Bool
p
{-# INLINE sFindIndices #-}
{-# RULES
"Foldable.sum/Vector"
F.sum =
V.sum . runSized
#-}
elemIndex ::
forall f (n :: Nat) a.
(CFoldable f, Eq a, Dom f a) =>
a ->
Sized f n a ->
Maybe Int
elemIndex :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Eq a, Dom f a) =>
a -> Sized f n a -> Maybe Int
elemIndex = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Dom f a, Eq a) =>
a -> f a -> Maybe Int
celemIndex @f @a
{-# INLINE elemIndex #-}
sElemIndex
, sUnsafeElemIndex ::
forall f (n :: Nat) a.
(KnownNat n, CFoldable f, Dom f a, Eq a) =>
a ->
Sized f n a ->
Maybe (Ordinal n)
sElemIndex :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Maybe (Ordinal n)
sElemIndex = (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Enum a => Int -> a
toEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. coerce :: forall a b. Coercible a b => a -> b
coerce (forall (f :: Type -> Type) a.
(CFoldable f, Dom f a, Eq a) =>
a -> f a -> Maybe Int
celemIndex @f @a)
{-# INLINE sElemIndex #-}
sUnsafeElemIndex :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Maybe (Ordinal n)
sUnsafeElemIndex = forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> Maybe (Ordinal n)
sElemIndex
{-# DEPRECATED sUnsafeElemIndex "No difference with sElemIndex; use sElemIndex instead." #-}
elemIndices ::
forall f (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a ->
Sized f n a ->
[Int]
elemIndices :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> [Int]
elemIndices = coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a.
(CFoldable f, Dom f a, Eq a) =>
a -> f a -> [Int]
celemIndices @f @a
{-# INLINE elemIndices #-}
sElemIndices ::
forall f (n :: Nat) a.
(CFoldable f, KnownNat (n :: Nat), Dom f a, Eq a) =>
a ->
Sized f n a ->
[Ordinal n]
sElemIndices :: forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, KnownNat n, Dom f a, Eq a) =>
a -> Sized f n a -> [Ordinal n]
sElemIndices = (forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Enum a => Int -> a
toEnum forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) (n :: Nat) a.
(CFoldable f, Dom f a, Eq a) =>
a -> Sized f n a -> [Int]
elemIndices
{-# INLINE sElemIndices #-}
data ConsView f n a where
NilCV :: ConsView f (0) a
(:-) ::
(KnownNat n, KnownNat (1 + n)) =>
a ->
Sized f n a ->
ConsView f (1 + n) a
infixr 5 :-
viewCons ::
forall f (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
Sized f n a ->
ConsView f n a
viewCons :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
Sized f n a -> ConsView f n a
viewCons Sized f n a
sz = case forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n of
ZeroOrSucc n
IsZero -> forall (f :: Type -> Type) a. ConsView f 0 a
NilCV
IsSucc SNat n1
n' ->
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n1
n' forall a b. (a -> b) -> a -> b
$
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat (SNat 1
sOne forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat n1
n') forall a b. (a -> b) -> a -> b
$
case forall (f :: Type -> Type) (n :: Nat) a (proxy :: Nat -> Type).
(KnownNat n, CFreeMonoid f, Dom f a) =>
proxy n -> Sized f (Succ n) a -> Uncons f (Succ n) a
uncons' SNat n1
n' Sized f n a
sz of
Uncons a
a Sized f n a
xs -> a
a forall (n :: Nat) a (f :: Type -> Type).
(KnownNat n, KnownNat (1 + n)) =>
a -> Sized f n a -> ConsView f (1 + n) a
:- Sized f n a
xs
data SnocView f n a where
NilSV :: SnocView f (0) a
(:-::) :: KnownNat (n :: Nat) => Sized f n a -> a -> SnocView f (n + 1) a
infixl 5 :-::
viewSnoc ::
forall f (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
Sized f n a ->
SnocView f n a
viewSnoc :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
Sized f n a -> SnocView f n a
viewSnoc Sized f n a
sz = case forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc (forall (n :: Nat). KnownNat n => SNat n
sNat @n) of
ZeroOrSucc n
IsZero -> forall (f :: Type -> Type) a. SnocView f 0 a
NilSV
IsSucc (SNat n1
n' :: SNat n') ->
forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
withKnownNat SNat n1
n' forall a b. (a -> b) -> a -> b
$
case forall (f :: Type -> Type) (n :: Nat) a (proxy :: Nat -> Type).
(KnownNat n, CFreeMonoid f, Dom f a) =>
proxy n -> Sized f (Succ n) a -> Unsnoc f (Succ n) a
unsnoc' SNat n1
n' Sized f n a
sz of
Unsnoc (Sized f n a
xs :: Sized f m a) a
a ->
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith
(forall a b. a -> b
unsafeCoerce (forall {k} (a :: k). a :~: a
Refl @()) :: n' :~: m)
forall a b. (a -> b) -> a -> b
$ Sized f n a
xs forall (n :: Nat) (f :: Type -> Type) a.
KnownNat n =>
Sized f n a -> a -> SnocView f (Succ n) a
:-:: a
a
infixr 5 :<
pattern (:<) ::
forall (f :: Type -> Type) a (n :: Nat).
(Dom f a, KnownNat n, CFreeMonoid f) =>
forall (n1 :: Nat).
(n ~ (1 + n1), KnownNat n1) =>
a ->
Sized f n1 a ->
Sized f n a
pattern a $b:< :: forall (f :: Type -> Type) a (n :: Nat) (n1 :: Nat).
(Dom f a, KnownNat n, CFreeMonoid f, n ~ (1 + n1), KnownNat n1) =>
a -> Sized f n1 a -> Sized f n a
$m:< :: forall {r} {f :: Type -> Type} {a} {n :: Nat}.
(Dom f a, KnownNat n, CFreeMonoid f) =>
Sized f n a
-> (forall {n1 :: Nat}.
(n ~ (1 + n1), KnownNat n1) =>
a -> Sized f n1 a -> r)
-> ((# #) -> r)
-> r
:< as <-
(viewCons -> a :- as)
where
a
a :< Sized f n1 a
as = a
a forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
a -> Sized f n a -> Sized f (1 + n) a
<| Sized f n1 a
as
chkNil ::
forall f (n :: Nat) a.
(KnownNat n) =>
Sized f n a ->
ZeroOrSucc n
chkNil :: forall (f :: Type -> Type) (n :: Nat) a.
KnownNat n =>
Sized f n a -> ZeroOrSucc n
chkNil = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => SNat n
sNat @n
pattern Nil ::
forall f (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
(n ~ 0) =>
Sized f n a
pattern $bNil :: forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a, n ~ 0) =>
Sized f n a
$mNil :: forall {r} {f :: Type -> Type} {n :: Nat} {a}.
(KnownNat n, CFreeMonoid f, Dom f a) =>
Sized f n a -> ((n ~ 0) => r) -> ((# #) -> r) -> r
Nil <-
(chkNil -> IsZero)
where
Nil = forall (f :: Type -> Type) a.
(Monoid (f a), Dom f a) =>
Sized f 0 a
empty
infixl 5 :>
pattern (:>) ::
forall (f :: Type -> Type) a (n :: Nat).
(Dom f a, KnownNat n, CFreeMonoid f) =>
forall (n1 :: Nat).
(n ~ (n1 + 1), KnownNat n1) =>
Sized f n1 a ->
a ->
Sized f n a
pattern a $b:> :: forall (f :: Type -> Type) a (n :: Nat) (n1 :: Nat).
(Dom f a, KnownNat n, CFreeMonoid f, n ~ (n1 + 1), KnownNat n1) =>
Sized f n1 a -> a -> Sized f n a
$m:> :: forall {r} {f :: Type -> Type} {a} {n :: Nat}.
(Dom f a, KnownNat n, CFreeMonoid f) =>
Sized f n a
-> (forall {n1 :: Nat}.
(n ~ (n1 + 1), KnownNat n1) =>
Sized f n1 a -> a -> r)
-> ((# #) -> r)
-> r
:> b <-
(viewSnoc -> a :-:: b)
where
Sized f n1 a
a :> a
b = Sized f n1 a
a forall (f :: Type -> Type) (n :: Nat) a.
(CFreeMonoid f, Dom f a) =>
Sized f n a -> a -> Sized f (n + 1) a
|> a
b
{-# COMPLETE (:<), Nil #-}
{-# COMPLETE (:>), Nil #-}
class Dom f a => DomC f a
instance Dom f a => DomC f a
instance
( Functor f
, CFreeMonoid f
, CZip f
, KnownNat n
, forall a. DomC f a
) =>
P.Applicative (Sized f (n :: Nat))
where
{-# SPECIALIZE instance KnownNat n => P.Applicative (Sized [] (n :: Nat)) #-}
{-# SPECIALIZE instance KnownNat n => P.Applicative (Sized Seq.Seq (n :: Nat)) #-}
{-# SPECIALIZE instance KnownNat n => P.Applicative (Sized V.Vector (n :: Nat)) #-}
pure :: forall a. a -> Sized f n a
pure (a
x :: a) =
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: Constraint). a => Dict a
Dict @(DomC f a)) forall a b. (a -> b) -> a -> b
$
forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> Sized f n a
replicate' a
x
{-# INLINE pure #-}
(Sized f n (a -> b)
fs :: Sized f n (a -> b)) <*> :: forall a b. Sized f n (a -> b) -> Sized f n a -> Sized f n b
<*> (Sized f n a
xs :: Sized f n a) =
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: Constraint). a => Dict a
Dict @(DomC f b)) forall a b. (a -> b) -> a -> b
$
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: Constraint). a => Dict a
Dict @(DomC f a)) forall a b. (a -> b) -> a -> b
$
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (a :: Constraint). a => Dict a
Dict @(DomC f (a -> b))) forall a b. (a -> b) -> a -> b
$
forall (f :: Type -> Type) (n :: Nat) a b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
zipWithSame forall a b. (a -> b) -> a -> b
($) Sized f n (a -> b)
fs Sized f n a
xs
{-# INLINE [1] (<*>) #-}
{-# RULES
"<*>/List" [~1] forall fs xs.
Sized fs <*> Sized xs =
Sized (getZipList (ZipList fs <*> ZipList xs))
"<*>/Seq" [~1] forall fs xs.
Sized fs <*> Sized xs =
Sized (Seq.zipWith ($) fs xs)
"<*>/Vector" [~1] forall fs xs.
Sized fs <*> Sized xs =
Sized (V.zipWith ($) fs xs)
#-}
instance
(CFreeMonoid f, KnownNat (n :: Nat)) =>
CPointed (Sized f n)
where
cpure :: forall a. Dom (Sized f n) a => a -> Sized f n a
cpure = forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> Sized f n a
replicate'
instance
(CFreeMonoid f, CZip f) =>
CApplicative (Sized f n)
where
pair :: forall a b.
(Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (a, b)) =>
Sized f n a -> Sized f n b -> Sized f n (a, b)
pair = forall (f :: Type -> Type) (n :: Nat) a b.
(Dom f a, CZip f, Dom f b, Dom f (a, b)) =>
Sized f n a -> Sized f n b -> Sized f n (a, b)
zipSame
<.> :: forall a b.
(Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (a -> b)) =>
Sized f n (a -> b) -> Sized f n a -> Sized f n b
(<.>) = forall (f :: Type -> Type) (n :: Nat) a b c.
(Dom f a, CZip f, Dom f b, CFreeMonoid f, Dom f c) =>
(a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
zipWithSame forall a b. (a -> b) -> a -> b
($)
<. :: forall a b.
(Dom (Sized f n) a, Dom (Sized f n) b) =>
Sized f n a -> Sized f n b -> Sized f n a
(<.) = forall a b. a -> b -> a
P.const
.> :: forall a b.
(Dom (Sized f n) a, Dom (Sized f n) b) =>
Sized f n a -> Sized f n b -> Sized f n b
(.>) = forall a b c. (a -> b -> c) -> b -> a -> c
P.flip forall a b. a -> b -> a
P.const
instance (CZip f, CFreeMonoid f) => CSemialign (Sized f n) where
calignWith :: forall a b c.
(Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) c) =>
(These a b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
calignWith =
coerce :: forall a b. Coercible a b => a -> b
coerce (\These a b -> c
f -> forall (f :: Type -> Type) a b c.
(CZip f, Dom f a, Dom f b, Dom f c) =>
(a -> b -> c) -> f a -> f b -> f c
czipWith @f @a @b @c ((These a b -> c
f forall b c a. (b -> c) -> (a -> b) -> a -> c
.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> b -> These a b
These)) ::
forall a b c.
(Dom f a, Dom f b, Dom f c) =>
(These a b -> c) ->
Sized f n a ->
Sized f n b ->
Sized f n c
{-# INLINE [1] calignWith #-}
calign :: forall a b.
(Dom (Sized f n) a, Dom (Sized f n) b,
Dom (Sized f n) (These a b)) =>
Sized f n a -> Sized f n b -> Sized f n (These a b)
calign =
coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b c.
(CZip f, Dom f a, Dom f b, Dom f c) =>
(a -> b -> c) -> f a -> f b -> f c
czipWith @f @a @b forall a b. a -> b -> These a b
These ::
forall a b.
(Dom f a, Dom f b, Dom f (These a b)) =>
Sized f n a ->
Sized f n b ->
Sized f n (These a b)
{-# INLINE [1] calign #-}
instance (CZip f, CFreeMonoid f) => CZip (Sized f n) where
czipWith :: forall a b c.
(Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) c) =>
(a -> b -> c) -> Sized f n a -> Sized f n b -> Sized f n c
czipWith =
coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b c.
(CZip f, Dom f a, Dom f b, Dom f c) =>
(a -> b -> c) -> f a -> f b -> f c
czipWith @f @a @b @c ::
forall a b c.
(Dom f a, Dom f b, Dom f c) =>
(a -> b -> c) ->
Sized f n a ->
Sized f n b ->
Sized f n c
{-# INLINE [1] czipWith #-}
czip :: forall a b.
(Dom (Sized f n) a, Dom (Sized f n) b, Dom (Sized f n) (a, b)) =>
Sized f n a -> Sized f n b -> Sized f n (a, b)
czip =
coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall (f :: Type -> Type) a b.
(CZip f, Dom f a, Dom f b, Dom f (a, b)) =>
f a -> f b -> f (a, b)
czip @f @a @b ::
forall a b.
(Dom f a, Dom f b, Dom f (a, b)) =>
Sized f n a ->
Sized f n b ->
Sized f n (a, b)
{-# INLINE [1] czip #-}
instance
(KnownNat (n :: Nat), CZip f, CFreeMonoid f) =>
CRepeat (Sized f n)
where
crepeat :: forall a. Dom (Sized f n) a => a -> Sized f n a
crepeat = forall (f :: Type -> Type) (n :: Nat) a.
(KnownNat n, CFreeMonoid f, Dom f a) =>
a -> Sized f n a
replicate'
{-# INLINE [1] crepeat #-}
instance CTraversable f => CTraversable (Sized f n) where
ctraverse :: forall a b (g :: Type -> Type).
(Dom (Sized f n) a, Dom (Sized f n) b, Applicative g) =>
(a -> g b) -> Sized f n a -> g (Sized f n b)
ctraverse = \a -> g b
f -> forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap coerce :: forall a b. Coercible a b => a -> b
coerce forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) a b (g :: Type -> Type).
(CTraversable f, Dom f a, Dom f b, Applicative g) =>
(a -> g b) -> f a -> g (f b)
ctraverse a -> g b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: Type -> Type) (n :: Nat) a. Sized f n a -> f a
runSized
{-# INLINE ctraverse #-}