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